[Agda] Simple monoid instance based on monoid instance of underlying type

[Mateusz Kowalczyk]

Hi all,

I'm struggling with something that seemed like an easy task. Consider:

```
open import Algebra

record Input (τ : Set) : Set where
  constructor I
  field
    unI : τ
```

I now want to give a monoid instance to this type, as long as τ can
give me one. That is, in Haskell I could say

```
import Data.Monoid

newtype I t = I t

instance Monoid t => Monoid (I t) where
  mempty = I mempty
  I x `mappend` I y = I $ x `mappend` y
```

In fact, I could use the GHC extension to derive this for me. I
thought writing an instance like this in Agda should not be a problem
at all but I seem to be struggling. In the snippet below is my failed
attempt to replicate what the Haskell code does. I had hoped that I
can simply pass the Monoid (or should I be using RawMonoid?) instance
of the underlying type and use that. My problem with this is that I
don't seem to be able to get out anything meaningful out of the passed
in Monoid. For example, opening the ‘m’ and trying to use ε in my
‘binOp’ function quickly shoots me down with the message that ‘Carrier
≠ τ’. I'm unsure how to tell Agda that I only want to pass in the
Monoid instances with τ as a Carrier or how to get the value out once
I do: the Monoid type doesn't seem to be parametrised by anything but
Level. I struggle to find any examples in standard lib or elsewhere of
how to use passed in instances of Monoid from Data.Algebra: all I can
find are either usages of monoids from other libraries or short
documents which show off Agda by rolling their own.

Here's the snippet. I imagine that the ‘monoid’ type needs fixing up
so that I can actually use ‘m’ somehow.

I'd appreciate if someone can point me in the right direction.

```
module InputMonoid where
  open import Level using (zero)
  open import Relation.Binary.PropositionalEquality

  monoid : (τ : Set) → (m : Monoid {!!} {!!}) → Monoid zero zero
  monoid τ m = record
    { Carrier = Input τ
    ; _≈_      = _≡_
    ; _∙_      = binOp
    ; ε        = {!!}
    ; isMonoid = record
      { isSemigroup = record
        { isEquivalence = {!!}
        ; assoc         = {!!}
        ; ∙-cong        = {!!}
        }
      ; identity = {!!}
      }
    }
    where
      open Monoid m

      binOp : ∀ {τ} → Input τ → Input τ → Input τ
      binOp (I unI) (I unI₁) = {!!}
```

--
Mateusz K.