Apparently calling evarconv on `proj ?X = v`

or `(?X).(proj) = v`

is not the same if `?X : ?Y`

or `?X : i`

for some inductive `i`

with primitive projection `proj`

. If the type of `?X`

is know, both work. If it is an evar, then only the non-primitive projection works.

Does this ring a bell?

This is hard to reproduce in plain Coq, one needs Coq-Elpi or (I guess) some ltac and uconstr.

Hmm indeed, we certainly rely on `?X : i ?pars ?inds`

as that's usually given by (pre)typing

Maybe we're missing a bit of "imitation", refining the evar ?V to `i ?pars ?inds`

in some cases

What I don't get is why the compat constant works even if ?X was not typed before

The only extra piece of info is the number of params (that are all _)

but I guess that is statically known also for primproj, somehow...

I'll look at the code of evarconv tomorrow...

The code is well documented for once:

```
(* Knowing the structure and hence its number of arguments, I can cut sk1 into pieces. *)
let params1, c1, extra_args1 =
match arg with
| Some c -> (* A primitive projection applied to c *)
let ty =
try Retyping.get_type_of ~lax:true env sigma c with
| Retyping.RetypeError _ -> raise Not_found
in let (i, u), ind_args =
(* Are we sure that ty is not an evar? *)
Inductiveops.find_mrectype env sigma ty
in ind_args, c, sk1
```

The comment questions that if ty is an evar (my exact case) then things go wrong (`Inductiveops.find_mrectype`

raises `Not_found`

that corresponds to no canonical solution being available).

Enrico Tassi said:

Apparently calling evarconv on

`proj ?X = v`

or`(?X).(proj) = v`

is not the same if`?X : ?Y`

or`?X : i`

for some inductive`i`

with primitive projection`proj`

. If the type of`?X`

is know, both work. If it is an evar, then only the non-primitive projection works.Does this ring a bell?

if the type of ?X is an evar then `proj ?X`

is ill typed no?

It is not typed yet. If I type it, then ?Y has to become the inductive applied to unknown parameters.

The code above synthesizes/recovers the inductive parameters only to unify them with the ones of the canonical solution. If they can't be recovered, then we should just not perform that unification.

I mean `fun c : i _ _ => (c).(proj)`

does not fail but has the same info at hand than `fun c : _ => (c).(proj)`

.

Yep, we can fix this

I have a fix, but I have an hard time writing a test.

I can test it with Elpi, but with Ltac2 I can't find a way, In particular:

```
Module U.
#[projections(primitive=yes)] Record r := R { r_car : Type }.
#[projections(primitive=yes)] Record s := S { s_car : Type }.
Canonical Structure foo (x : s) := R (s_car x).
Axiom a : s.
Ltac2 Eval
let t1 := open_constr:( ( _ ).(r_car) ) in
let t2 := constr:( (a).(s_car) ) in
match (Constr.Unsafe.kind t1) with
| Constr.Unsafe.Proj _ _ _ => ()
| _ => fail
end;
match (Constr.Unsafe.kind t2) with
| Constr.Unsafe.Proj _ _ _ => ()
| _ => fail
end;
printf "%t = %t" t1 t2;
unify_with_full_ts t1 t2;
printf "%t = %t" t1 t2.
```

succeeds (with or without my paths) and the second print tells me that the evar is still unassigned

This is my first Ltac2 program, so I probably misusing the API/language.

The preliminary patch is here: https://github.com/coq/coq/pull/19358

(the test above is not sufficient, since the _ is typed anyway, but how to build a term without typing it would be the next question)

unify_with_full_ts does Goal.enter (https://github.com/coq/coq/blob/65ff3388b4076eed7720a45b21be13515deb54fc/tactics/tactics.ml#L3404) so when there is no goal it does nothing

if you do Goal True before Ltac2 Eval you get

```
(r_car ?r) = (s_car a)
(r_car (foo a)) = (s_car a)
- : unit = ()
```

(you also need

```
Require Import Ltac2.Ltac2.
Import Printf.
Import Unification.
```

)

(the test above is not sufficient, since the _ is typed anyway, but how to build a term without typing it would be the next question)

do we really want evarconv to work on untyped terms?

Thanks:

```
Goal True.
Ltac2 Eval
let t1 := open_constr:( ( _ : _ r ).(r_car) ) in
let t2 := constr:( (a).(s_car) ) in
match (Constr.Unsafe.kind t1) with
| Constr.Unsafe.Proj _ _ _ => ()
| _ => fail
end;
match (Constr.Unsafe.kind t2) with
| Constr.Unsafe.Proj _ _ _ => ()
| _ => fail
end;
printf "%t = %t" t1 t2;
unify_with_full_ts t1 t2;
printf "%t = %t" t1 t2.
Abort.
```

it is not about typed or not, it is about having a type that is syntactically an inductive

```
Error: Unable to unify "r_car (?y : ?T r)" with "s_car a".
```

But my patch needs amending, now that I can quickly test it.

Thanks for the help!

unify_with_full_ts does Goal.enter ... no goal does nothing

Not sure this is a user friendly API, but this is not my garden.

https://github.com/coq/coq/issues/19359

it is not about typed or not, it is about having a type that is syntactically an inductive

because of delayed constraints I guess? if you do `ltac1:(solve_constraints)`

before the unify it fails with

```
Unable to unify "?T r" with "r" (cannot satisfy constraint "?T r" == "r").
```

(why is this even delayed, isn't there a unique solution `?T := fun x => x`

?)

No it is not, `fun _ => r`

is another one. Anyway, I just wanted to prove that even if the terms are typed it may be that the type of the projected is not syntactically an inductive, not to defend the unif candidates business.

Here my final tests, it works with my patch, it does not work without:

```
Module U.
#[projections(primitive=yes)] Record r := R { r_car : Type }.
#[projections(primitive=yes)] Record s := S { s_car : Type }.
Canonical Structure foo (x : s): (fun x=>x) r := R (s_car x).
Axiom a : s.
Set Debug "unification".
Goal True.
Ltac2 Eval
let t1 := open_constr:( ( _ : _ r ).(r_car) ) in
let t2 := constr:( (a).(s_car) ) in
match (Constr.Unsafe.kind t1) with
| Constr.Unsafe.Proj _ _ _ => ()
| _ => fail
end;
match (Constr.Unsafe.kind t2) with
| Constr.Unsafe.Proj _ _ _ => ()
| _ => fail
end;
printf "%t = %t" t1 t2;
unify_with_full_ts t1 t2;
printf "%t = %t" t1 t2.
Abort.
End U.
```

I'll polish my PR and ask for a review

even if the terms are typed

I'm not sure I consider "typed up to delayed constraints" to be the same as "typed"

I don't really trust delayed constraints to not break random things

I totally agree. This PR fixes one of these cases ;-)

Last updated: Oct 13 2024 at 01:02 UTC