Handling "partial matches" when unifying two terms

Stream: metaprogramming / tactics

[Anton Gusev]

"Metaprogramming in Lean 4" states that, when using isDefEq:

The unification ?m₁ + ?m₂ + ?m₃ =?= m + n - k fails and no metavariables are assigned (even though there is a 'partial match' between the expressions).

Are there any unification methods that do distinguish between the two terms being certainly definitionally unequal to each other (i.e. mismatched types or constructor calls) and being (currently) unable to make them definitionally equal, like with the term above or (forgive my Idris-ism) Vect (.cons x) Nat =?= Vect (?a + ?b) Nat?

In the second case, ideally, I'd like to also somehow get the metavariable assigments it successfully made (for the quoted example, that'd be ?m1 = m) and the constraint(s) it can't resolve further (for the quoted example, ?m2 + ?m3 =?= n - k, for my example, ?a + ?b = .cons x). If this is impossible, then I need to at least be able to distinguish the two categories. I know that in Idris, such a distinction can be made (if somewhat non-trivially, owing to the quirks of its elaborator): when typechecking Refl as a value of type a = b (where a and b are the expressions being unified), it will fail outright if the unification is impossible, and "successfully" return ?postpone if it's merely stalled. However, I don't know if Lean has any parallels to this behavior.

Distinguishing between those two kinds of results seems crucial for my task (checking which constructors can produce a value given certain parameters and indices of that value's type, and, if so, what values their arguments have to be for that to happen), since definitional un-equality means the constructor can never produce such a value, while the unification stalling means there are non-trivial conditions under which the constructor may produce a value.

[Aaron Liu]

I know we have three-state instance synthesis but I don't see an isDefEq function that can return "maybe"

[Jovan Gerbscheid]

Indeed, type class synthesis can get "stuck" when there are metavariables that it isn't allowed to instantiate, but that is different from what you want. I don't think there is such an isDefEq function. Could you give an example of your use case?

[Anton Gusev]

I'm going to start with a synthetic example that demonstrates the problem I'm trying to solve at the lowest level. Let's say we've got a type that looks like this:

inductive Example : Nat -> Type
  | e0 : Example 0
  | eS : (n : Nat) -> Example (.succ n)
  | eSum : (a b : Nat) -> Example (a + b)

Starting off, we'd like to know which constructors may produce a value of type Example 0, and which ones a value of type Example 1.

Intuitively, we can see that Example 0 can be produced by .e0 and .eSum:

example : Example 0 := .e0 -- e0 always creates Example 0
example : Example 0 := .eSum 0 0 -- eSum creates Example 0 so long as a + b = 0

And Example 1 - by .eS and .eSum:

example : Example 1 := .eS 0 -- eS creates Example 1 if n = 0
example : Example 1 := .eSum 0 1 -- eSum creates Example 1 if a + b = 1
example : Example 1 := .eSum 1 0

The problem, then, is performing such analysis programmatically, rather than by hand. The way I did it in Idris was by performing unifications like this:

Example 0 =?= Example 0 -- Succeeds
Example (.succ ?n) =?= Example 0 -- Fails, since .succ and .zero are different constructors
Example (?a + ?b) =?= Example 0 -- Postpones, since there are constraints it can't solve

Example 0 =?= Example 1 -- Fails, since .succ and .zero are different constructors
Example (.succ ?n) =?= Example 0 -- Succeeds, metavariable n is assigned 0
Example (?a + ?b) =?= Example 0 -- Postpones

However, when performing unification with isDefEq, Example (.succ ?n) =?= Example 0 and Example (?a + ?b) =?= Example 0 both simply return false.

[Jovan Gerbscheid]

All right, for this simple example you could write your own unification algorithm, which would first run whnf on both sides. If the sides get the same head, recursively continue. If they have different heads, check if they are both constructors, in which case you fail, and otherwise you postpone.

How are you planning on dealing with the postponed cases? Because isDefEq won't solve them for you. Is it to try every possible constructor?

[Anton Gusev]

Jovan Gerbscheid said:

How are you planning on dealing with the postponed cases? Because isDefEq won't solve them for you. Is it to try every possible constructor?

This depends on what information I get. If I only know that they're postponed (as is the case with Idris), I'll have to write my own primitive unifier that does its best to extract whatever constraints it can. If I receive those constraints (?a + ?b = 0 in case of Example (?a + ?b) =?= Example 0) right away, then I don't really have to do anything further.

[Anton Gusev]

To explain a bit, the (current) use-case for all this constructor unification is deriving specialized variants of types.

For instance, a specialized variant of Example corresponding to Example 0 would be

inductive Example0 : Type
  | e0 : Example0
  | eSum (a b : Nat) (prf: a + b = 0) : Example0

def toPoly : Example0 -> Example 0
  | .e0 => .e0
  | .eSum a b prf => prf ▸ .eSum a b

def ofPoly (e : Example 0) : Example0 :=
  match p : 0, e with
  | .(a) + .(b), .eSum a b => .eSum a b p.symm
  | _, .e0 => .e0
  | _, .eS n => by grind;

instance : Coe (Example 0) Example0 where
  coe := ofPoly

instance : Coe Example0 (Example 0) where
  coe := toPoly

So all those unresolved-during-unification constraints are "simply" included in the signatures of specialized constructors.