<:, lub, glb, and term-level coercion, plus the direction-aware metavariable-solving algorithm used in place of a literal Specialize rule.

Term-level coercions aren't always available: Set/Function/Tuple/Record can always be wrapped generally (a set-image, a domain remap via CHOOSE, or projecting components/fields out of the original expression). Seq and Operator cannot in general — Seq has no static arity to rebuild a literal over, and Operator would need a first-class operator value this grammar has no constructor for — so for these two the structural rule still computes the correct <: relation recursively, but only returns a coercion when the sub-coercion needed is .id. Channel supports subtyping only via plain reflexivity (τ = τ'); a receive's element-vs-reference coercion is computed directly, not through Channel(τ) <: Channel(τ').

inductive SubtypeResult : Type

The three outcomes of a subtyping check — not a plain success/failure, since an unresolved metavariable hit from the upper-bound side can't yield a concrete coercion yet, only a recorded pending bound. pending carries which metavariable the eventual coercion depends on, so a caller can wrap its expression in TypedTLAPlus.Expression.mvar tagged with that id, to be resolved once the metavariable is.

• success (coe : TypedTLAPlus.Coercion) : SubtypeResult

  τ <: τ' holds, and coe witnesses it.

• pending (n : TypedTLAPlus.MVarId) : SubtypeResult

  τ <: τ' holds if metavariable n resolves wide enough — not yet known to hold outright.

• failure : SubtypeResult

  τ <: τ' does not hold.

structure PendingBounds : Type

Per-unresolved-metavariable pending upper bounds — accumulated until ?n resolves from a lower bound (subtype itself, below) or defaults at the end of checking. A bound can itself be a metavariable (?m <: ?n, both unresolved) — recorded here unchanged rather than merged with ?n's own identity, since ?m's and ?n's eventual solutions may legitimately diverge, only staying <:-related.

• bounds : Std.HashMap TypedTLAPlus.MVarId (List TypedTLAPlus.Typ)

@[implicit_reducible]

instance instEmptyCollectionPendingBounds : EmptyCollection PendingBounds

Equations

• instEmptyCollectionPendingBounds = { emptyCollection := { bounds := ∅ } }

class MonadPendingBounds (m : Type → Type) : Type

The pending-upper-bounds effect subtype needs on top of MonadMetavarContext.

• pendingUpperBounds : TypedTLAPlus.MVarId → m (List TypedTLAPlus.Typ)

  The upper bounds recorded so far on a metavariable, [] if none (including if it's already resolved — callers only consult this while a metavariable is still unresolved).

• addPendingUpperBound : TypedTLAPlus.MVarId → TypedTLAPlus.Typ → m Unit

  Record one more upper bound on a metavariable.

@[implicit_reducible]

instance instMonadPendingBoundsOfMonadOfMonadStateOfPendingBounds {m : Type → Type} [Monad m] [MonadStateOf PendingBounds m] : MonadPendingBounds m

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def instInhabitedSubtypeResult {m : Type → Type} [Monad m] : Inhabited (m SubtypeResult)

Needed for subtype/tryAxioms's own partial defs below to type-check at all (an arbitrary m isn't otherwise known nonempty).

Equations

• instInhabitedSubtypeResult = { default := pure SubtypeResult.failure }

partial def subtype {m : Type → Type} [Monad m] [MonadMetavarContext TypedTLAPlus.Typ m] [MonadPendingBounds m] [MonadFresh m] (τ τ' : TypedTLAPlus.Typ) : m SubtypeResult

The type checker's subtyping judgment — see the module doc for Coercion's own scope/limitations, and tryAxioms/each structural case below for how Coercion data gets built (discharge itself lives in Core/TypedTLAPlus/Coercion.lean's Coercion.apply). Also implements the direction-aware metavariable-solving algorithm in the three mvar cases below.

partial: no structurally-decreasing measure across tryAxioms' recursive calls (its intermediate types can be larger than the input, e.g. Str to Seq(Int)).

def lub {m : Type → Type} [Monad m] [MonadMetavarContext TypedTLAPlus.Typ m] [MonadPendingBounds m] [MonadFresh m] (τ τ' : TypedTLAPlus.Typ) : m (Option TypedTLAPlus.Typ)

The least upper bound of two types under <:, where it exists — <: is a partial order with no ⊤, so lub is a partial function: comparable types have one (the wider of the two), incomparable ones don't.

Equations

• lub τ τ' = do let __do_lift ← isSubtype✝ τ τ' if __do_lift = true then pure (some τ') else do let __do_lift ← isSubtype✝ τ' τ if __do_lift = true then pure (some τ) else pure none

def glb {m : Type → Type} [Monad m] [MonadMetavarContext TypedTLAPlus.Typ m] [MonadPendingBounds m] [MonadFresh m] (τ τ' : TypedTLAPlus.Typ) : m (Option TypedTLAPlus.Typ)

The greatest lower bound, dual to lub.

Equations

• glb τ τ' = do let __do_lift ← isSubtype✝ τ τ' if __do_lift = true then pure (some τ) else do let __do_lift ← isSubtype✝ τ' τ if __do_lift = true then pure (some τ') else pure none