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?

`Arguments Build_T _ &.`

(bidi hints)

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

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: Feb 27 2024 at 23:01 UTC