The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Jul 02, 2018 at 01:07:10AM +0300, Erkki Luuk wrote:
> 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,
-- 
Enrico Tassi