Stream: Coq users

Topic: Inheriting from multiple typeclasses error


view this post on Zulip Laura Zielinski (Dec 02 2023 at 02:03):

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?

view this post on Zulip Gaëtan Gilbert (Dec 02 2023 at 09:20):

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

view this post on Zulip Gaëtan Gilbert (Dec 02 2023 at 09:21):

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)

view this post on Zulip Laura Zielinski (Dec 03 2023 at 05:23):

Thank you!! Works now.


Last updated: Jun 22 2024 at 15:01 UTC