The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

The issue is that you made the unification problem more difficult until 
Coq could not solve it anymore. TLDR try Program Definition.

After replacing holes with evars, the definition of instance3 looks like

Build_Class ?f (fun a => @option_field1 ?x@{a:=a}) @option_field2.
(plus an evar for the type of the fun a binding)

typechecking it involves a first unification problem checking that the 
type of (fun a => @option_field1 ?x@{a:=a}) is the expected type:

(forall a, ?f a -> unit) == (forall a, option ?x@{a:=a} -> unit).

which simplifies to
a |- ?f a == option ?x{a:=a}

This is solved by taking ?f := fun a => option ?x@{a:=a}.

Then there is a second unification problem for the type of @option_field2:

(forall a, ?f (a -> a) -> unit) == (forall a, option (a -> a) -> unit).
substituting our definition for ?f:
(forall a, option ?x@{a:=a -> a} -> unit) == (forall a, option (a -> a) 
   -> unit).

Coq is incapable of solving this so it fails.

If Coq used bidirectional typechecking the constraint that the whole 
must have type Class option would be used earlier to set ?f := option. I 
believe Program does this and indeed

        Require Import Program.
        Program Definition instance3 : Class option :=
          Build_Class _ (fun {a} => option_field1 ) (@option_field2).

succeeds.

This has come up before, see eg 
https://sympa.inria.fr/sympa/arc/coq-club/2017-06/msg00083.html 
mentioning a similar issue.

Gaëtan Gilbert

On 11/11/2017 00:40, Joachim Breitner wrote:
> Hi,
>
> good point. In the real code, however, I have to use {|…|} because it
> is a Definition, not an Instance, so I believe I cannot use {…}.
>
> I learned that using Build_ and instantiating the argument works
> better:
>
>      Class Class f := {
>        field1 : forall {a}, f a -> unit ;
>        field2 : forall {a}, f (a -> a) -> unit  }.
>
>      Definition option_field1 : forall {a}, option a -> unit :=
>        fun {a} => fun _ => tt.
>
>      Definition option_field2 : forall {a}, option (a -> a) -> unit:=
>        fun {a} => fun _  => tt.
>
>
>      Definition instance1 : Class option :=
>           Build_Class _ (@option_field1) (@option_field2).
>
>      Definition instance2 : Class option :=
>           Build_Class option (fun {a} => option_field1 )
> (@option_field2).
>
>      Definition instance3 : Class option :=
>           Build_Class _ (fun {a} => option_field1 ) (@option_field2).
>
> instance1 and instance2 work, instance3 does not.
>
> Joachim