isDefEq configuration for the elaborator.
Note that we enable all approximations but
In Lean3 and Lean 4, we used to use the quasi-pattern approximation during elaboration. The example:
demonstrates why it produces counterintuitive behavior.
We have the
It produces the following unification problem when we process the expected type:
?n ?α =?= StateT δ (StateT σ id) σ ==> (approximate using first-order unification) ?n := StateT δ (StateT σ id) ?α := σ
Then, we need to solve:
?m ?α =?= StateT σ id σ ==> instantiate metavars ?m σ =?= StateT σ id σ ==> (approximate since it is a quasi-pattern unification constraint) ?m := fun σ => StateT σ id σ
Note that the constraint is not a Milner pattern because σ is in
the local context of
?m. We are ignoring the other possible solutions:
We need the quasi-pattern approximation for elaborating recursor-like expressions (e.g., dependent
match with expressions).
Haskell would work on this example since it always uses first-order unification.
- One or more equations did not get rendered due to their size.