Fix information propagation

leanprover · Feb 25, 2025 · b14463f · b14463f
1 parent 0430515
commit b14463f
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/Lean/Elab/PreDefinition/Mutual.lean b/src/Lean/Elab/PreDefinition/Mutual.lean
@@ -85,8 +85,8 @@ partial def Info.setCallerParam (calleeIdx argIdx callerIdx paramIdx : Nat) (inf
         -- all good
         info
       else
-        -- Inconsistent information, mark both as not fixed
-        info.setNotFixed callerIdx paramIdx |>.setNotFixed calleeIdx argIdx
+        -- Inconsistent information
+        info.setNotFixed calleeIdx argIdx
     else
       -- Set the new entry
       let info := info.modify calleeIdx (·.modify argIdx (·.map (·.set! callerIdx (some paramIdx))))
@@ -102,7 +102,8 @@ partial def Info.setCallerParam (calleeIdx argIdx callerIdx paramIdx : Nat) (inf
           for otherArgIdx in [:info[otherFunIdx]!.size] do
             if let some otherArgsInfo := info[otherFunIdx]![otherArgIdx]! then
               if let some paramIdx' := otherArgsInfo[calleeIdx]! then
-                info := info.setCallerParam otherFunIdx otherArgIdx callerIdx paramIdx
+                if paramIdx' = argIdx then
+                  info := info.setCallerParam otherFunIdx otherArgIdx callerIdx paramIdx
 
         return info
     else