Inheriting Typeclasses of different Kinds in Coq

Question

This is kind of a follow-up to my previous question: Multiple Typeclass Inheritance in Coq, but this is about typeclasses that expect different Kinds (in Haskell terms, I guess?).

I have a typeclass, Collection, that expects a Type -> Type and a typeclass, Monoid, that expects a Type, and I thought I knew how to reconcile both of them, but I'm having trouble using the Monoid functions.

Class Sequence (S : Type -> Type)
  foldr empty insert append
  `{C : Collection S foldr empty insert}
  `{M : Monoid (forall A, S A) append empty} :=
{
  insert_append_id :
    forall (A : Type) (h : S A) (x : A),
    append A (insert A x (empty A)) h = insert A x h
}.

And the (trimmed down) error is:

Error:
In environment
Sequence :
forall (S : Type -> Type)
  (append : (forall A : Type, S A) ->
            (forall A : Type, S A) -> forall A : Type, S A)
[...]
S : Type -> Type
empty : forall A : Type, S A
append :
(forall A : Type, S A) -> (forall A : Type, S A) -> forall A : Type, S A
[...]
M : Monoid (forall A : Type, S A) append empty
A : Type
h : S A
x : A
The term "A" has type "Type" while it is expected to have type
 "forall A : Type, S A".

I thought that I was really clever, figuring out to have (forall A, S A) in the Monoid inheritance, but now I'm not so sure. The type of Monoid empty looks correct, but append's type doesn't make any sense to me.

It seems to me that I either made a mistake with the Monoid inheritance type or there is some way to give append the correct type that I'm not seeing. Or is there some error somewhere else that is causing this problem?

---

Edit: I came up with a different Monoid declaration that seems closer to what I want, but still does not work.

Class Sequence (S : Type -> Type)
  foldr empty insert (append : forall A, S A -> S A -> S A)
  `{C : Collection S foldr empty insert}
  `{M : forall (A : Type), Monoid (S A) (append A) (empty A)} :=
{
  insert_append_eq :
    forall (A : Type) (h : S A) (x : A),
    append A (insert A x (empty A)) h = insert A x h
}.

And the new error:

Error:
Could not find an instance for "Semigroup (S A) (append A)" in environment:

S : Type -> Type
foldr : forall A B : Type, (A -> B -> B) -> B -> S A -> B
empty : forall A : Type, S A
insert : forall A : Type, A -> S A -> S A
append : forall A : Type, S A -> S A -> S A
F : Foldable S foldr
U : Unfoldable S empty insert
C : Collection S foldr empty insert
A : Type

Answer 1

After banging on this problem for a few more days, I have typeclass inheritance of different Kinds that, as far as I can tell, is correct.

I was on the right track in my question update. All I needed to do was add an explicit inheritance of Semigroup. I am still not sure why it must be explicit when inheriting from collection implicitly inherits from foldable and unfoldable. Maybe it's because of the forall as part of the inheritance.

Also, I learned that including the functions in the type declaration is incorrect or at least unnecessary. I found out by reading the paper by the author of typeclasses in Coq and the Coq reference manual. (If you scroll down to the EqDec typeclass, you'll see that eqb is typed in the curly brackets.)

So, here is what my Sequence typeclass looks like now:

Class Sequence (S : Type -> Type)
  `{C : Collection S}
  `{G : forall (A : Type), Semigroup (S A)}
  `{M : forall (A : Type), Monoid (S A)} :=
{
  insert_append_eq :
    forall (A : Type) (h : S A) (x : A),
    op (insert A x (empty A)) h = insert A x h
}.

To be sure that this actually created the typeclass correctly, I defined a List type and made it an instance of Sequence. This involved making it an instance of every parent typeclass first, unfortunately. I wonder if there is an easier way.

And just to include more code examples, because I find them easier to understand than natural language explanations, here is my Semigroup typeclass and List instance of it:

Class Semigroup (S : Type) :=
{
  op :
    S -> S -> S;
  semigroup_assoc :
    forall x y z : S,
    op x (op y z) = op (op x y) z
}.

Inductive List (A : Type) : Type :=
  | Nil : List A
  | Cons : A -> List A -> List A
.

Instance semigroup_list : forall A, Semigroup (List A) :=
{
  op := fix append l l' :=
    match l with
      | Nil => l'
      | Cons x xs => Cons A x (append xs l')
    end
}.
Proof.
intros.
induction x.
apply eq_refl.
rewrite IHx.
apply eq_refl.
Defined.

Thanks for the help, Perce. This sounds mean, but your answer was so disappointing that I had to figure out if you were actually wrong. :)

Answer 2

No, the monoid is a particular S applied to a particular A. You can't generalize it further. The code below should work though I can't test it.

Class Sequence (S : Type -> Type) (A : Type)
  foldr empty insert append
  `{C : Collection S foldr empty insert}
  `{M : Monoid (S A) (append A) (empty A)} :=
{
  insert_append_id :
    forall (h : S A) (x : A),
    append _ (insert _ x (empty _)) h = insert _ x h
}.

Alternatively, you can have a different kind of monoid.

Class Mon (F : Type -> Type) (mul : forall X, F X -> F X -> F X)
  (one : forall X, F X) : Type :=
{
  idl : forall X x, mul X (one X) x = x;
  idr : forall X x, mul X x (one X) = x;
  asc : forall X x y z, mul X x (mul X y z) = mul X (mul X x y) z;
}.