[Coq-Club] Canonical structure resolution ignores coercions

[Erkki Luuk]

Hi

I'm probably not the first to notice that..

(*Canonical structure resolution ignores coercions*)
Parameter T S0: Prop.
Parameter s_base: S0 -> S0 -> S0.
Structure CON := mCON {dom_con:Type; ran_con:Type; con: dom_con -> ran_con}.
Canonical Structure con_s := mCON _ _ s_base.
Definition variad := T -> S0.
Parameter variad_S0:> variad -> S0.
Parameter v: variad.
Check v: S0.
Check con _ (_:S0) (_:S0).
Check con con_s v v.
Check con _ (v:S0) v.
Fail Check con _ v v.

Does anyone know how to make canonical structure resolution work w/
coercions? I need the resolution for notation overloading (and need the
coercion, too)

Best
Erkki

[Enrico Tassi]

Post by Erkki Luuk
Hi
I'm probably not the first to notice that..
(*Canonical structure resolution ignores coercions*)
Parameter T S0: Prop.
Parameter s_base: S0 -> S0 -> S0.
Structure CON := mCON {dom_con:Type; ran_con:Type; con: dom_con -> ran_con}.
Canonical Structure con_s := mCON _ _ s_base.
Definition variad := T -> S0.
Parameter variad_S0:> variad -> S0.
Parameter v: variad.
Check v: S0.
Check con _ (_:S0) (_:S0).
Check con con_s v v.
Check con _ (v:S0) v.
Fail Check con _ v v.
Does anyone know how to make canonical structure resolution work w/
coercions? I need the resolution for notation overloading (and need the
coercion, too)

since v has (inferred) type variad you need a Canonical Structure indexed on variad,
but you only have one indexed on S0. I'm not sure this declaration makes
sense in your context, but makes your example work.

Canonical Structure variad_s := mCON variad _ s_base.
Check con _ v v.

Best,