The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

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/

Attachment: signature.asc
Description: This is a digitally signed message part