open import Relation.Binary.PropositionalEquality
open import Data.Integer

record Group {G : Set} (_⋄_ : G → G → G) (e : G) (_⁻¹ : G → G) : Set where
  field
    assoc : (x y z : G) → (x ⋄ y) ⋄ z ≡ x ⋄ (y ⋄ z)
    neutral-l : (g : G) → e ⋄ g ≡ g
    inverse-l : (g : G) → (g ⁻¹) ⋄ g ≡ e

instance
  ⟨ℤ,+⟩ : Group _+_ (ℤ.pos 0) -_
  ⟨ℤ,+⟩ = ?

---------------------------------------------------------------------------
Parser Error
---------------------------------------------------------------------------

Don't know how to parse Group _+_ (ℤ.pos 0) -_. Could mean any one
of:
  ((Group _+_) (ℤ.pos 0)) -_
  ((Group _+_) (ℤ.pos 0)) -_
Operators used in the grammar:
  -_ (postfix operator section, level 6) [_-_ (/nix/store/y9wqjp24ws1xzhnvr11khjdb0qwdldks-agda-stdlib-0.13/share/agda/Data/Integer/Base.agda:94,1-4)]
(the treatment of operators was changed in Agda 2.5.1, so code that
used to parse may have to be changed)
when scope checking Group _+_ (ℤ.pos 0) -_