Hugo Herbelin (Sep 22 2021 at 14:25): 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?
Gaëtan Gilbert (Sep 22 2021 at 14:27):Arguments Build_T _ &. (bidi hints)
Gaëtan Gilbert (Sep 22 2021 at 14:28):see also https://github.com/coq/coq/pull/13107#issuecomment-870566806
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: Jun 04 2023 at 19:30 UTC