From f85ac7b5dc0967022add0c9d0a41d37c3402661a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Dec 2019 18:42:33 -0800
Subject: [PATCH] feat: add `isLevelDefEqStuck` exception

---
 src/Init/Lean/Meta/Exception.lean  | 9 ++++++---
 src/Init/Lean/Meta/ExprDefEq.lean  | 2 +-
 src/Init/Lean/Meta/LevelDefEq.lean | 8 ++++++--
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean
index 6d3614dfd8..9ea0d94a5b 100644
--- a/src/Init/Lean/Meta/Exception.lean
+++ b/src/Init/Lean/Meta/Exception.lean
@@ -29,7 +29,8 @@ inductive Exception
 | invalidProjection    (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext)
 | revertFailure        (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext)
 | readOnlyMVar         (mvarId : MVarId) (ctx : ExceptionContext)
-| isDefEqStuck         (t s : Expr) (ctx : ExceptionContext)
+| isLevelDefEqStuck    (u v : Level) (ctx : ExceptionContext)
+| isExprDefEqStuck     (t s : Expr) (ctx : ExceptionContext)
 | letTypeMismatch      (fvarId : FVarId) (ctx : ExceptionContext)
 | appTypeMismatch      (f a : Expr) (ctx : ExceptionContext)
 | bug                  (b : Bug) (ctx : ExceptionContext)
@@ -51,7 +52,8 @@ def toStr : Exception → String
 | invalidProjection _ _ _ _     => "invalid projection"
 | revertFailure _ _ _           => "revert failure"
 | readOnlyMVar _ _              => "try to assign read only metavariable"
-| isDefEqStuck _ _ _            => "isDefEq is stuck"
+| isLevelDefEqStuck _ _ _       => "isDefEq is stuck"
+| isExprDefEqStuck _ _ _        => "isDefEq is stuck"
 | letTypeMismatch _ _           => "type mismatch at let-expression"
 | appTypeMismatch _ _ _         => "application type mismatch"
 | bug _ _                       => "bug"
@@ -74,7 +76,8 @@ def toMessageData : Exception → MessageData
 | invalidProjection s i e ctx     => mkCtx ctx $ `invalidProjection ++ " " ++ mkProj s i e
 | revertFailure xs decl ctx       => mkCtx ctx $ `revertFailure -- TODO improve
 | readOnlyMVar mvarId ctx         => mkCtx ctx $ `readOnlyMVar ++ " " ++ mkMVar mvarId
-| isDefEqStuck t s ctx            => mkCtx ctx $ `isDefEqStuck ++ " " ++ t ++ " =?= " ++ s
+| isLevelDefEqStuck u v ctx       => mkCtx ctx $ `isLevelDefEqStuck ++ " " ++ u ++ " =?= " ++ v
+| isExprDefEqStuck t s ctx        => mkCtx ctx $ `isExprDefEqStuck ++ " " ++ t ++ " =?= " ++ s
 | letTypeMismatch fvarId ctx      => mkCtx ctx $ `letTypeMismatch ++ " " ++ mkFVar fvarId
 | appTypeMismatch f a ctx         => mkCtx ctx $ `appTypeMismatch ++ " " ++ mkApp f a
 | bug _ _                         => "internal bug" -- TODO improve
diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 950c51851e..9c91b16a5c 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -918,7 +918,7 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
   cond (!tAssign? && !sAssign?)
     (if tFn.isMVar || sFn.isMVar then do
        ctx ← read;
-       if ctx.config.isDefEqStuckEx then throwEx $ Exception.isDefEqStuck t s
+       if ctx.config.isDefEqStuckEx then throwEx $ Exception.isExprDefEqStuck t s
        else pure LBool.false
      else pure LBool.undef) $ do
   -- Both `t` and `s` are terms of the form `?m ...`
diff --git a/src/Init/Lean/Meta/LevelDefEq.lean b/src/Init/Lean/Meta/LevelDefEq.lean
index 9d5e5a06bf..2a864dded3 100644
--- a/src/Init/Lean/Meta/LevelDefEq.lean
+++ b/src/Init/Lean/Meta/LevelDefEq.lean
@@ -67,8 +67,12 @@ partial def isLevelDefEqAux : Level → Level → MetaM Bool
       isLevelDefEqAux lhs' rhs'
     else do
       mctx ← getMCtx;
-      if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then
-        pure false
+      if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then do
+        ctx ← read;
+        if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then
+          throwEx $ Exception.isLevelDefEqStuck lhs rhs
+        else
+          pure false
       else do
         k ← getLevelConstraintKind lhs rhs;
         match k with