The Coq mailing list

[Yao Li <liyao AT seas.upenn.edu>]

It’s probably because of the difference between {|…|} and {…}.

The following code would work:

   Instance instance3 : Class option := 
          { field1 := fun {a} => option_field1 ;
            field2 := @option_field2 }.

I remember hearing from Benjamin that type inference works differently in 
{|…|} and {…}, but I’m not knowledgable enough to explain what exactly is 
going on here.

Best,
Yao

> On 8 Nov 2017, at 11:37 PM, Joachim Breitner 
> <mail AT joachim-breitner.de>
>  wrote:
> 
> Dear list,
> 
> here is a curious puzzle. Consider this file:
> 
>    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.
> 
>    Instance instance1 : Class option :=
>          {| field1 := fun {a} => option_field1 ;
>             field2 := _ |}.
>    exact @option_field2.
>    Defined.
>    Print instance1.
> 
>    Instance instance2 : Class option :=
>          {| field1 := @option_field1;
>             field2 := @option_field2 |}.
> 
>    Instance instance3 : Class option := 
>           {| field1 := fun {a} => option_field1 ;
>              field2 := @option_field2 |}.
> 
> 
> The first two instance declarations go through, the third one fails with 
> this error messagE:
> 
>    Error:
>    The term "@option_field2" has type "forall a : Type, option (a -> a) -> 
> unit"
>    while it is expected to have type
>     "forall a : Type, option ?a@{a:=a -> a} -> unit" (cannot instantiate 
>    "?a" because "a" is not in its scope: available arguments are "a -> a").
> 
>    This looks very fishy to me. Why should a change in how I implement
>    field1 change the typing of my assignment of field2?
> 
>    It looks almost as if the [fun {a} =>] of the field1 somehow leaks into
>    the type-checking of field2...
> 
>    Or maybe the problem is somewhere else… any insight is appreciated!
> 
>    This is The Coq Proof Assistant, version 8.6 (July 2017), compiled on
>    Jul 20 2017 12:59:58 with OCaml 4.02.3
> 
>    Thanks,
>    Joachim
> 
>    -- 
>    Joachim Breitner
>  
> mail AT joachim-breitner.de
>  http://www.joachim-breitner.de/