fix: ihave and iapply do not synthesize all tc (#159)

* fix: ihave and iapply do not synthesize all tc

---------

Co-authored-by: Michael Sammler <noreply@sammler.me>

Author: lzy0505

src/Iris/BI/Lib/Fixpoint.lean

@@ -85,10 +85,8 @@ instance least_fixpoint_absorbing [BIMonoPred F]
     letI _ : NonExpansive fun x => iprop(True -∗ bi_least_fixpoint F x) :=
       ⟨fun _ _ _ H => wand_ne.ne .rfl (NonExpansive.ne H)⟩
     iapply least_fixpoint_iter
-    · infer_instance -- FIXME: Issue #156
     iintro !> %y HF HT
     iapply least_fixpoint_unfold
-    · infer_instance -- FIXME: Issue #156
     iapply mono_pred (Φ := (fun x : A => iprop(True -∗ bi_least_fixpoint F x))) $$ [], [HF, HT]
     · iintro !> %x HF
       iapply HF
@@ -106,10 +104,8 @@ instance least_fixpoint_persistent_affine [BIMonoPred F]
     letI _ : NonExpansive fun x => iprop(□ bi_least_fixpoint F x) :=
       ⟨fun _ _ _ H => intuitionistically_ne.ne (NonExpansive.ne H)⟩
     iapply least_fixpoint_iter
-    · infer_instance -- FIXME: Issue #156
     iintro !> %y #HY !>
     iapply least_fixpoint_unfold
-    · infer_instance -- FIXME: Issue #156
     iapply mono_pred (Φ := fun x => iprop(□ bi_least_fixpoint F x))
     · iintro !> %_ #Hx
       iexact Hx
@@ -124,10 +120,8 @@ instance least_fixpoint_persistent_absorbing [BIMonoPred F]
     letI _ : NonExpansive fun x => iprop(<pers> bi_least_fixpoint F x) :=
       ⟨fun _ _ _ H => persistently_ne.ne <| NonExpansive.ne H⟩
     iapply least_fixpoint_iter
-    · infer_instance -- FIXME: Issue #156
     iintro !> %y #HF !>
     iapply least_fixpoint_unfold
-    · infer_instance -- FIXME: Issue #156
     iapply mono_pred (Φ := fun x => iprop(<pers> bi_least_fixpoint F x)) $$ [], HF
     letI _ := @least_fixpoint_absorbing _ _ _ _ _ _ Habsorb
     iintro !> %x #H
@@ -137,10 +131,8 @@ theorem least_fixpoint_strong_mono (G : (A → PROP) → (A → PROP)) [BIMonoPr
     ⊢ □ (∀ Φ x, F Φ x -∗ G Φ x) -∗ ∀ x, bi_least_fixpoint F x -∗ bi_least_fixpoint G x := by
   iintro #Hmon
   iapply least_fixpoint_iter
-  · infer_instance -- FIXME: Issue #156
   iintro !> %y IH
   iapply least_fixpoint_unfold
-  · infer_instance -- FIXME: Issue #156
   iapply Hmon $$ IH
 
 section Strong
@@ -169,18 +161,15 @@ theorem least_fixpoint_ind_wf :
   · iintro H1 H2
     iapply H1
     iapply least_fixpoint_unfold
-    · infer_instance
     iexact H2
   iapply Hthis
   iintro HF
   iapply HM
   iapply mono_pred (Φ := (bi_least_fixpoint F)) $$ [], HF
   imodintro
   iapply least_fixpoint_iter
-  · infer_instance -- FIXME: Issue #156
   iintro !> %y Hy
   iapply least_fixpoint_unfold
-  · exact wf_pred_mono (F := F) (Φ := Φ)
   isplit
   · iapply HM $$ Hy
   · iexact Hy
@@ -190,8 +179,6 @@ theorem least_fixpoint_ind :
       ∀ x, bi_least_fixpoint F x -∗ Φ x := by
   iintro #HM
   iapply least_fixpoint_ind_wf
-  · infer_instance
-  · infer_instance
   iintro !> %y Hy
   iapply HM
   letI _ : NonExpansive fun x => iprop(Φ x ∧ bi_least_fixpoint F x) :=
@@ -202,7 +189,6 @@ theorem least_fixpoint_ind :
   · iclear HM
     exact (least_fixpoint_unfold_1 ..).trans and_elim_l
   · iapply least_fixpoint_strong_mono $$ [], Hx
-    · infer_instance
     iintro !> %_ %_ ⟨-, H⟩
     iexact H
 

src/Iris/ProofMode/ProofModeM.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Zongyuan Liu
 -/
 import Iris.ProofMode.Expr
 import Iris.ProofMode.Classes
@@ -90,7 +90,7 @@ def ProofModeM.runTactic (x : MVarId → IrisGoal → ProofModeM α) (s : ProofM
   let (res, {goals}) ← StateRefT'.run (x mvar g) s
 
   -- make sure to synthesize everything postponed
-  Term.synthesizeSyntheticMVarsNoPostponing
+  Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
 
   -- put the goals that depend on other goals last
   let dependees ← goals.foldlM (λ m g => do

src/Iris/ProofMode/Tactics/HaveCore.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Zongyuan Liu
 -/
 import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Tactics.Basic
@@ -55,6 +55,13 @@ private def iHaveCore {e} (hyps : @Hyps u prop bi e)
     let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
     let otherMVarIds ← getMVarsNoDelayed val
     let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
+
+    -- If the new mvars have type class assumption that could not be solved, register them such
+    -- that they are tried to be solved again at the end of `ProofModeM.runTactic` (using Term.synthesizeSyntheticMVarsNoPostponing)
+    for mvar in newMVars do
+      if (← isSyntheticMVar mvar) && !(← mvar.mvarId!.isAssignedOrDelayedAssigned) then
+        Term.registerSyntheticMVarWithCurrRef mvar.mvarId! (.typeClass .none)
+
     for mvar in newMVarIds ++ otherMVarIds do
       addMVarGoal mvar