Unification bug

Stream: lean4

[Jovan Gerbscheid]

When working on #lean4 > Exponential blowup in unification with metavariables, I discovered that unification doesn't correctly revert the metavariable context when unifying projections. So when unifying a.1 =?= b.1, it first tries a =?= b, and if that fails then it tries to reduce the expressions. But it forgets to reset the metavariable context. #mwe:

import Lean

structure A (α : Type) where
  x : Type
  y : α

structure B (α : Type) extends A α where
  z : Nat

def A.map (f : α → β) (a : A α) : A β := ⟨a.x, f a.y⟩

-- elaborator that turns projections into raw projections (`Expr.proj` constructor)
open Lean Meta in
elab "unfold" e:term : term => do
  let e ← Elab.Term.elabTerm e none
  let e ← unfoldDefinition e
  return e

def test (i : B α) : unfold i.toA.x := sorry

set_option trace.Meta.isDefEq true
set_option trace.Meta.isDefEq.delta true
set_option trace.Meta.isDefEq.cache true

example (i : B α) (f : α → β) : (i.toA.map f).x := by
  apply @test -- error

The problem is that it initially assigns ?α := β, but it needs to backtrack from that to find the correct ?α := α, which it doesn't manage.

This failure only becomes visible when working with a raw projection. When we remove the unfold elaborator (to get the normal projection function), the example seems to succeed, but this is due to another bug: the place where it would previously assign ?α := β (and not revert it), it now doesn't because of a cache hit of false. But this cache was established in a metavariable context where ?α := β was already true. So applying this cache is illegal. And if we didn't apply this cache, it would still fail in the same way.

The first bug is easily fixed by inserting a checkpointDefEq in the right place. The second bug is directly related to the slowness from #lean4 > Exponential blowup in unification with metavariables.