Strata.Laurel.isSubtype (ctx : Strata.Laurel.TypeLattice)
  (sub sup : Strata.Laurel.HighTypeMd) : Bool
Strata.Laurel.isSubtype
  (ctx : Strata.Laurel.TypeLattice)
  (sub sup : Strata.Laurel.HighTypeMd) :
  Bool

Pure subtyping <:. Walks the extending chain for CompositeType (via TypeLattice.ancestors), unfolds TypeAlias to its target, and unwraps ConstrainedType to its base (both via TypeLattice.unfold), then falls back to structural equality via highEq.

Used together with isConsistent to form isConsistentSubtype, which is what the bidirectional checker invokes at every check-mode boundary (rule [⇐] Sub).

Strata.Laurel.isConsistent (ctx : Strata.Laurel.TypeLattice)
  (a b : Strata.Laurel.HighTypeMd) : Bool
Strata.Laurel.isConsistent
  (ctx : Strata.Laurel.TypeLattice)
  (a b : Strata.Laurel.HighTypeMd) : Bool

Consistency ~ (Siek–Taha): the symmetric gradual relation. Unknown is the dynamic type and is consistent with everything; otherwise structural equality after unfolding aliases / constrained types.

MultiValuedExpr is checked element-wise so the same equivalence propagates through procedure-output tuples.

Used directly by [⇒] Op-Eq, where the operand types must be mutually consistent (no subtype direction is privileged), and as one half of isConsistentSubtype.

Strata.Laurel.isConsistentSubtype (ctx : Strata.Laurel.TypeLattice)
  (sub sup : Strata.Laurel.HighTypeMd) : Bool
Strata.Laurel.isConsistentSubtype
  (ctx : Strata.Laurel.TypeLattice)
  (sub sup : Strata.Laurel.HighTypeMd) :
  Bool

Consistent subtyping: ∃ R. sub ~ R ∧ R <: sup. DERIVED from the proof-relevant coerce so the yes/no answer and the inserted coercion can never disagree (ONE judgment). Used by rule [⇐] Sub and every bespoke check rule. That single choice is what makes the system gradual: an expression of type Unknown (a hole, an unresolved name, a Hole _ none) flows freely into any typed slot, and any expression flows freely into a slot of type Unknown.

Generic polymorphism flows through coerce's final fallback, which delegates to isConsistent/isSubtype (element-wise generic args, .TVar wildcard, substitutedAncestors) — so a concrete Box<int> satisfies a Box<T> slot and C<args> <: P<pargs> holds, all as a refl witness.