From 2ca67d88489f9ea025e7c79ca1ab13778a29a249 Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Tue, 6 Aug 2024 17:52:08 +0200
Subject: [PATCH] RulePattern: fix assignment of universe mvars in openRuleType

The new Lean version seems to have broken this, possibly via changes to
`checkedAssign`.
---
 Aesop/RulePattern.lean                |  6 ++--
 AesopTest/RulePatternUniverseBug.lean | 45 ++++++++++++++-------------
 2 files changed, 26 insertions(+), 25 deletions(-)

diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean
index 7716e99..627e618 100644
--- a/Aesop/RulePattern.lean
+++ b/Aesop/RulePattern.lean
@@ -145,9 +145,9 @@ def openRuleType (pat : RulePattern) (inst : RulePatternInstantiation)
   for h : i in [:mvars.size] do
     if let some inst ← pat.getInstantiation inst i then
       let mvarId := mvars[i]'h.2 |>.mvarId!
-      -- We use `checkedAssign`, rather than `assign`, to make sure that
-      -- universe metavariables occurring in `mvars` are assigned.
-      if ← mvarId.checkedAssign inst then
+      -- We use `isDefEq` to make sure that universe metavariables occurring in
+      -- the type of `mvarId` are assigned.
+      if ← isDefEq (.mvar mvarId) inst then
         assigned := assigned.insert mvarId
       else
         throwError "openRuleType: type-incorrect pattern instantiation: argument has type '{← mvarId.getType}' but pattern instantiation '{inst}' has type '{← inferType inst}'"
diff --git a/AesopTest/RulePatternUniverseBug.lean b/AesopTest/RulePatternUniverseBug.lean
index be1c253..c8e7db1 100644
--- a/AesopTest/RulePatternUniverseBug.lean
+++ b/AesopTest/RulePatternUniverseBug.lean
@@ -8,7 +8,10 @@ Authors: Son Ho, Jannis Limperg
 -- assigned during rule pattern matching. Thanks to Son Ho for reporting this
 -- issue.
 
-import Aesop
+import Aesop.Frontend.Attribute
+import Aesop.Frontend.Saturate
+
+set_option aesop.check.all true
 
 namespace List
 
@@ -28,24 +31,22 @@ def indexOpt (ls : List α) (i : Int) : Option α :=
   | [] => none
   | hd :: tl => if i = 0 then some hd else indexOpt tl (i - 1)
 
--- FIXME this is failing under v4.11.0-rc1
-
--- theorem indexOpt_bounds (ls : List α) (i : Int) :
---   ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i := by
---   match ls with
---   | [] => simp [indexOpt]; omega
---   | _ :: tl =>
---     have := indexOpt_bounds tl (i - 1)
---     if h : i = 0 then
---       simp [indexOpt, *]
---       saturate
---       omega
---     else
---       simp [indexOpt, len, *]
---       constructor <;> intro a <;> cases a
---       . left
---         saturate
---         omega
---       . right; omega
---       . left; omega
---       . right; omega
+theorem indexOpt_bounds (ls : List α) (i : Int) :
+    ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i := by
+  match ls with
+  | [] => simp [indexOpt]; omega
+  | _ :: tl =>
+    have := indexOpt_bounds tl (i - 1)
+    if h : i = 0 then
+      simp [indexOpt, *]
+      saturate
+      omega
+    else
+      simp [indexOpt, len, *]
+      constructor <;> intro a <;> cases a
+      . left
+        saturate
+        omega
+      . right; omega
+      . left; omega
+      . right; omega