Hi, beginner user here! I'm trying to implement a typeclass hierarchy with this structure:

A

/ \

B C

\ /

D

I'm getting an error defining D. I've recreated the error as simply as possible:

```
Class A (T : Type) : Type := {
func1 : T -> T -> Type
}.
Class B (T : Type) `{A T} : Type := {
func2 : T -> T -> T;
func3 {a b c d} : (func1 a b) -> (func1 c d) ->
(func1 (func2 a c) (func2 b d))
}.
Class C (T : Type) `{A T} : Type := {
func4 {a b} : (func1 a b) -> (func1 b a)
}.
Class D (T : Type) `{B T} `{C T} : Type := {
func5 {a b c d : T} {f : func1 a b} {g : func1 c d} :
func3 (func4 f) (func4 g) = func4 (func3 f g);
}.
```

The error is

```
Errors:
Unable to satisfy the following constraints:
In environment:
D : forall (T : Type) (H : A T), B T -> forall H1 : A T, C T -> Type
T : Type
H : A T
H0 : B T
H1 : A T
H2 : C T
a, b, c, d : T
f : func1 a b
g : func1 c d
?B : "B T"
?C : "C T"
?C0 : "C T"
?C1 : "C T"
?H : "A T";
```

I think the issue is that Coq doesn't know that B and C inherit from the same instance of A. I tried passing in explicit parameters, like this:

```
func5 {a b c d : T} {f : func1 a b} {g : func1 c d} :
@func3 T H H0 b a d c (@func4 T H1 H2 a b f) (func4 g) = func4 (func3 f g);
```

and I get messages like:

```
Errors:
In environment
D : forall (T : Type) (H : A T), B T -> forall H1 : A T, C T -> Type
T : Type
H : A T
H0 : B T
H1 : A T
H2 : C T
a : T
b : T
c : T
d : T
f : func1 a b
g : func1 c d
The term "func4 f" has type "@func1 T H1 b a" while it is expected to have type
"@func1 T H b a".;
```

But of course, if I pass in H instead of H1, I get another error. Is there a way around this?

` Class D (T : Type) `{B T} `{C T} `

will not share the genralized arguments between B and T, so it's equivalent to `Class D T H (b : @B T H) H' (c : @C T H')`

use ` Class D (T : Type) `{B T} `{!C T} `

to tell Coq that you don't want to explicitly give a name to the C argument but it should get its arguments from the context

https://coq.inria.fr/doc/master/refman/language/extensions/implicit-arguments.html#implicit-generalization (the "When generalizing a binder whose type is a typeclass" paragragh)

Thank you!! Works now.

Last updated: Jun 22 2024 at 15:01 UTC