In the development below, I get a strange error when trying to define an instance of a single-method typeclass:
Universe ARG. Definition ARG := Type@{ARG}.
Universe ARG0. Definition ARG0 := Type@{ARG0}.
Universe ARG1. Definition ARG1 := Type@{ARG1}.
Universe ARG2. Definition ARG2 := Type@{ARG2}.
Constraint ARG<ARG0, ARG0<ARG1, ARG1<ARG2.
Inductive SR: ARG := Phy | Sen | Inf | Lim.
Parameter CA: Prop.
Parameter X: SR -> CA -> ARG -> ARG.
Parameter X': SR -> CA -> ARG -> ARG0.
Parameter XP: SR -> CA -> ARG -> ARG1.
Parameter XP': SR -> CA -> ARG -> ARG2.
Inductive tri:Set := one | two | three.
Definition iX' (t:tri): SR -> CA -> ARG -> ARG2 := match t with one => X' | two => XP | three => XP' end.
Parameter gk:> forall (b:SR)(d:CA)(c:ARG), X' b d c -> iX' one b d c.
Parameter gl:> forall (b:SR)(d:CA)(c:ARG), XP b d c -> iX' two b d c.
Parameter gm:> forall (b:SR)(d:CA)(c:ARG), XP' b d c -> iX' three b d c.
Definition iX'bsko {b:tri}{s:SR}{k:CA}{o:ARG} := iX' b s k o.
Parameter foo: forall {b:tri}{s:SR}{k:CA}{o:ARG}, iX' b s k o.
Fail Check foo: forall {b:tri}{s:SR}{k:CA}{o:ARG}, iX' b s k o. (*Why?*)
Check foo: iX'bsko.
Class CONN := p5 (x y z:ARG): x -> y -> z.
Instance cco: CONN := fun x y iX'bsko (_:x) (_:y) => foo.
(* Error: "foo" has type "iX' ?b@{y0:=x0; y1:=y0} ?s@{y0:=x0; y1:=y0} ?k@{y0:=x0; y1:=y0} ?o@{y0:=x0; y1:=y0}"
while it is expected to have type "iX'bsko". *)
The cause of the error seems to be that foo
doesn't have type iX'bsko
, while 2 lines above foo: iX'bsko
type checked. How do I solve this problem?