The one effect the well-formedness pass needs beyond ordinary monadic error-reporting: fetching a module's checked declarations by name, to resolve what a .var's Origin.module tag points at (used by WellFormedness/Restrictions.lean's global-variable and transitive-call checks).

class MonadForeignLookup (m : Type → Type) : Type

Fetches a module's checked representation by name — the one seam between WellFormedness/ and Driver/'s module cache. Kept as its own class (rather than WellFormedness/ importing Driver/Modules.lean directly) to avoid a cycle: Driver/Modules.lean calls into WellFormedness/ to run the check after type-checking succeeds. No provenance payload needed — origin travels on the AST itself, so this only answers "what did module name declare," not "who declared this name."

• lookupForeign : String → m (Option TypedModule)

  The named module's checked declarations, if it exists — none should be unreachable in practice (a name with Origin.module name only exists because that module already type-checked).

@[implicit_reducible]

instance instMonadForeignLookupStateTOfMonad {m : Type → Type} {σ : Type} [Monad m] [MonadForeignLookup m] : MonadForeignLookup (StateT σ m)

Generic lift through StateT — lets WellFormedness/Restrictions.lean's transitive walk add a StateT (Std.HashSet (String × String)) layer (memoizing already-visited operator/ function bodies) on top of whatever concrete monad Driver/Modules.lean supplies MonadForeignLookup at, without that monad needing to know about the state layer.

Equations

• instMonadForeignLookupStateTOfMonad = { lookupForeign := fun (name : String) => liftM (lookupForeign name) }

@[implicit_reducible]

instance instMonadForeignLookupExceptTOfMonad {m : Type → Type} {ε : Type} [Monad m] [MonadForeignLookup m] : MonadForeignLookup (ExceptT ε m)

Generic lift through ExceptT — lets a caller whose own ambient monad already has MonadForeignLookup (e.g. Driver/Modules.lean's M, tagged with a different error type) run TypedTLAPlus.Module.checkWellFormed at ExceptT WellFormednessError m, catching its WellFormednessErrors locally without m itself needing to know about that error type.

Equations

• instMonadForeignLookupExceptTOfMonad = { lookupForeign := fun (name : String) => liftM (lookupForeign name) }

@[implicit_reducible]

instance instMonadForeignLookupDiagTOfMonad {m : Type → Type} {α β : Type} [Monad m] [MonadForeignLookup m] : MonadForeignLookup (DiagT α β m)

Generic lift through DiagT — same rationale as the ExceptT lift above, for a caller running TypedTLAPlus.Module.checkWellFormed/TypedTLAPlus.Expression.checkNode's own MonadDiagnostic-shaped stack (Fugue.lean's runPassDiag) rather than a bare ExceptT.

Equations

• instMonadForeignLookupDiagTOfMonad = { lookupForeign := fun (name : String) => liftM (lookupForeign name) }