incomplete behaviour of unification / canonical structure inference ?

[damien-pous]

Description of the problem

With the attached code, I fail to automatically infer some canonical structures.

• I believe they should be inferred (or let's say I wish they were...)
• given the error messages I get, I suspect there are actually bugs in the unification algorithm

Rocq 9.0.0, same problem with 8.20.1.

Small Rocq / Coq file to reproduce the bug

Set Implicit Arguments.
Unset Strict Implicit.
(* Set Primitive Projections. *) (* same problems with and without primitive projections *)

Structure T X (x: X) := mk {TT: Type}.
Arguments TT {_}. 

Canonical Tunit := mk tt unit.
Canonical Teq X (x y: X) := mk x (x = y).
Canonical Tprod A X (x: forall a: A, X a) (X: forall a: A, T (x a)) a := mk (x a) (forall a, TT _ (X a)).

(* simple inferences work (with zero or one quantification) *)
Check eq_refl: TT _ _ = (unit).
Check eq_refl: TT _ _ = (nat -> unit). (* with an evar, fine *)


(* FIRST PROBLEM: I would expect the following line to work (generating two evars) *)
Fail Check eq_refl: TT _ _ = (nat -> bool -> unit).
(* Indeed, one can easily produce the required element of T (with two evars): *)
Check eq_refl: TT _ (Tprod (fun _: nat => Tprod (fun _: bool => Tunit) _) _) = (nat -> bool -> unit).
(* one can provide slightly less information: *)
Check eq_refl: TT _ (Tprod (fun _: nat => Tprod (fun _: bool => _) _) _) = (nat -> bool -> unit).
(* but if we remove one of the two type annotations, we get unexpected errors
   (why should it ever try to unify [bool] and [nat] ?): *)
Fail Check eq_refl: TT _ (Tprod (fun _ => Tprod (fun _: bool => _) _) _) = (nat -> bool -> unit).
Fail Check eq_refl: TT _ (Tprod (fun _: nat => Tprod (fun _ => _) _) _) = (nat -> bool -> unit).


Parameter X: Type.
Parameters (z: X) (f: X -> X) (g: X -> X -> X).
(* simple inferrence works (here, only one quantification) *)
Check eq_refl: TT (f z) _ = (forall t, f t = t).


(* SECOND PROBLEM: I would expect the following line to work *)
Fail Check eq_refl: TT (g z z) _ = (forall x y, g x y = g y x).
(* Indeed, one can easily produce the required element of T: *)
Check eq_refl: TT (g z z) (Tprod (fun x => Tprod (fun y => Teq (g x y) (g y x)) z) z)
               = (forall x y, g x y = g y x).
(* one can provide slightly less information: *)
Check eq_refl: TT (g z z) (Tprod (fun x => Tprod (fun y => Teq (g x y) (g y x)) _) _)
               = (forall x y, g x y = g y x).
Check eq_refl: TT (g z z) (Tprod (fun _ => Tprod (fun _ => Teq _ _) z) _)
               = (forall x y, g x y = g y x).
Check eq_refl: TT (g z z) (Tprod (fun _ => Tprod _ z) _)
               = (forall x y, g x y = g y x).
(* if we don't provide [z] in the inner [Tprod], it fails to instantiate
   an evar for an apparently wrong reason 
   (``cannot instantiate "?x" because "a" is not in its scope'', while "a" is in scope) *)
Fail Check eq_refl: TT (g z z) (Tprod (fun _ => Tprod (fun _ => Teq _ _) _) _)
               = (forall x y, g x y = g y x).

Version of Rocq / Coq where this bug occurs

9.0.0

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[CohenCyril]

I wonder if it's related to #19822

[damien-pous]

I've just tried with @Tragicus "evd-inst" version of rocq but I get the same behaviour...

[Tragicus]

Regarding the first one, the first canonical structure problem succeeds and reduces to the following failing problem

Fail Check fun (a : nat) => eq_refl : TT (_ a) _ = (bool -> unit).

This fails because the Tprod instance expects a parameter of the form ?T1 ?y1 that gets unified with the given ?T a. This makes ?T1 be unified with ?T and ?y1 with a, so ?T1 gets type nat -> _ instead of bool -> _. The following works:

Check fun (a : nat) => eq_refl : TT (_ a) (Tprod (fun _ : bool => Tunit) _) = (bool -> unit).

with the bool annotation being mandatory.