Pantograph/Frontend/Elab.lean

@@ -149,9 +149,14 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
     match i.info with
     | .ofTermInfo termInfo  => do
       let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+      if (← mvarId.getType).hasSorry then
+        throwError s!"Coupling is not allowed in drafting"
       return [(mvarId, stxByteRange termInfo.stx)]
     | .ofTacticInfo tacticInfo => do
       let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      for mvarId in mvarIds do
+        if (← mvarId.getType).hasSorry then
+          throwError s!"Coupling is not allowed in drafting"
       let range := stxByteRange tacticInfo.stx
       return mvarIds.map (·, range)
     | _ => panic! "Invalid info"

Pantograph/Tactic/Assign.lean

@@ -30,7 +30,9 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
 def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
   Meta.transform src λ
     | .app (.app (.const ``sorryAx ..) type) .. => do
-      -- FIXME: Handle cases of coupled goals
+      let type ← instantiateMVars type
+      if type.hasSorry then
+        throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
       let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
       modify (mvar.mvarId! :: .)
       pure $ .done mvar