Problem in the generation of fresh metavariables in unification rule applications

[fblanqui]

symbol A:TYPE;
symbol B:TYPE;
symbol C:TYPE;
symbol a:A;

unif_rule A ≡ B ↪ [ A ≡ Π x:C, $m[x] ];

symbol b : B ≔
begin
  print;
  refine a;
  // the goal is now A ≡ C → ?2 instead of Π x:C, ?2[x]

Fresh metavariables are not generated in the right context.

[fblanqui]

The problem is in https://github.com/Deducteam/lambdapi/blob/08755211c073f4216c34f8dd7864ce3b874415b4/src/core/eval.ml#L221-L227

[fblanqui]

Note that this kind of unification rule could be used to invert π:Prop → TYPE:

rule π (∀ x, $f[x]) ↪ Π x, π $f[x];
unif_rule π $p ≡ Π x, $_[x] ↪ [ $p ≡ ∀ x, $_[x] ];

[fblanqui]

The problem is that an extra pattern variable must be replaced by a fresh metavariable but, to create a fresh metavariable, you need to give it a type. The type of such a metavariable, and its arity, should not be given by the context where the rule is applied but by the context of the pattern variable in the rule itself. For instance, with $p ≡ ∀ x:A, $q[x] the extra pattern variable application $q[x] should be replaced at rule application time by a fresh metavariable application ?Q[x] of type Π x:A,?R[x] and arity 1, where ?R is a fresh metavariable of type Π x:A,TYPE and arity 1 (assuming that ?Q is an object metavariable, see (*) below). So the context in the rule itself of each extra pattern variable must be known at rule application time unless perhaps if we use fresh metavariables for the domains too, that is, take ?Q of type Π x:?S,?R[x] with ?S a fresh metavariable of type TYPE and arity 0. In this case indeed, no need to know the context but just the arity which is the the same as the pattern variable.

(*) Additional problem: how to eventually handle pattern variables of type TYPE which can only appear in unification rules (in this case, ?R should be of type Π x:A,KIND)?

[gabrielhdt]

For this issue (as for coercions), a possible solution is to have the rewrite engine generate holes, and then infer the type of the generated term in order to replace these holes by proper and fresh existential variables.

[fblanqui]

The RHS extra variables lack information about their sort, which makes unification fails. In Eval.tree_walk, case Leaf, a TEnv is replaced by a Plac false, that is, not a type. We should record the sort of extra variables.

Remark: we might be tempted to replace in rhs every P_Wild by some Plac, and every linear extra P_Patt by some Plac too.