Stream: Coq devs & plugin devs

Topic: Using known parameters to type arguments of a constructor


view this post on Zulip Hugo Herbelin (Sep 22 2021 at 14:25):

Hi, I vaguely remember that this was discussed at some time, maybe in relation to bidirectionality. Wasn't the following example requiring to extract information from the type of a constructor to infer the type of the non-parameter arguments of a constructor intended to work:

Record V := { a : Type -> Type }.
Record T (f : V) := { b : f.(a) nat }.
Fail Definition t : T {|a:=fun x=>x|} := {| b := 0 |}.

The following simpler example works though:

Record T (f : Set -> Set) := { b : f nat }.
Definition t T id := {| b := 0 |}.

Providing the type helps also:

Record V := { a : Type -> Type }.
Record T (f : V) := { b : f.(a) nat }.
Definition t : T {|a:=fun x=>x|} := {| b := 0 : {|a:=fun x=>x|}.(a) nat|}.

Is it worth to investigate or has someone already a solution to improve the inference?

view this post on Zulip Gaëtan Gilbert (Sep 22 2021 at 14:27):

Arguments Build_T _ &. (bidi hints)

view this post on Zulip Gaëtan Gilbert (Sep 22 2021 at 14:28):

see also https://github.com/coq/coq/pull/13107#issuecomment-870566806

view this post on Zulip Hugo Herbelin (Sep 22 2021 at 14:54):

Ah thanks!

I'm getting confused though, shouldn't it be independent of the directionality. That is, isn't it just that typing currently fails too early, without having considered yet all the pending unification constraints?

Otherwise, in #13107 which looks promising (since we clearly want that Coq knows alone what directionality to use and when), what is blocking?


Last updated: Oct 16 2021 at 07:02 UTC