From 613cf195099ad62253a1513695c3c9e09711feae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Mar 2022 15:11:03 -0800
Subject: [PATCH] fix: discrimination trees and "stuck" terms

See comments and new test.
---
 src/Lean/Meta/DiscrTree.lean | 23 +++++++++++++++
 tests/lean/run/stuckTC.lean  | 54 ++++++++++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+)
 create mode 100644 tests/lean/run/stuckTC.lean

diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 7d7bdb28f5..7cc50c52be 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -7,6 +7,7 @@ import Lean.Meta.Basic
 import Lean.Meta.FunInfo
 import Lean.Meta.InferType
 import Lean.Meta.WHNF
+import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta.DiscrTree
 /-
@@ -369,6 +370,28 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
   match e.getAppFn with
   | Expr.lit v _       => return (Key.lit v, #[])
   | Expr.const c _ _   =>
+    if (← getConfig).isDefEqStuckEx && e.hasMVar then
+      if (← isReducible c) then
+        /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded.
+           This can happen if the metavariables in `e` are "blocking" smart unfolding.
+           If `isDefEqStuckEx` is enabled, then we must throw the `isDefEqStuck` exception to postpone TC resolution.
+           Here is an example. Suppose we have
+           ```
+            inductive Ty where
+              | bool | fn (a ty : Ty)
+
+
+            @[reducible] def Ty.interp : Ty → Type
+              | bool   => Bool
+              | fn a b => a.interp → b.interp
+           ```
+           and we are trying to synthesize `BEq (Ty.interp ?m)`
+        -/
+        Meta.throwIsDefEqStuck
+      if (← isMatcherApp e <||> isRec c) then
+        /- Similar to the previous case, but for `match` and recursor applications. It may be stuck (i.e., did not reduce)
+           because of metavariables. -/
+        Meta.throwIsDefEqStuck
     let nargs := e.getAppNumArgs
     return (Key.const c nargs, e.getAppRevArgs)
   | Expr.fvar fvarId _ =>
diff --git a/tests/lean/run/stuckTC.lean b/tests/lean/run/stuckTC.lean
new file mode 100644
index 0000000000..ec65d2c100
--- /dev/null
+++ b/tests/lean/run/stuckTC.lean
@@ -0,0 +1,54 @@
+namespace Ex1
+
+inductive Ty where
+  | int
+  | bool
+  | fn (a ty : Ty)
+
+@[reducible] def Ty.interp : Ty → Type
+  | int    => Int
+  | bool   => Bool
+  | fn a b => a.interp → b.interp
+
+def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
+  f x y
+
+def f (a b : Ty.bool.interp) : Ty.bool.interp :=
+  test (.==.) a b
+
+end Ex1
+
+namespace Ex2
+
+inductive Ty where
+  | int
+  | bool
+
+@[reducible] def Ty.interp : Ty → Type
+  | int    => Int
+  | bool   => Bool
+
+def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
+  f x y
+
+def f (a b : Ty.bool.interp) : Ty.bool.interp :=
+  test (.==.) a b
+
+end Ex2
+
+namespace Ex3
+
+inductive Ty where
+  | int
+  | bool
+
+@[reducible] def Ty.interp (ty : Ty) : Type :=
+  Ty.casesOn (motive := fun _ => Type) ty Int Bool
+
+def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
+  f x y
+
+def f (a b : Ty.bool.interp) : Ty.bool.interp :=
+  test (.==.) a b
+
+end Ex3