strata-org · keyboardDrummer · Jun 29, 2026 · Jul 7, 2026 · Jul 7, 2026 · Jul 7, 2026
@@ -39,7 +39,6 @@ def collectTypeRefs : HighTypeMd → List String
   | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
   | ⟨.Applied base args, _⟩ =>
       collectTypeRefs base ++ args.flatMap collectTypeRefs
-  | ⟨.Pure base, _⟩ => collectTypeRefs base
   | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs
   | ⟨.TCore name, _⟩ => [name]
   | _ => []

@@ -76,7 +76,6 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   | .TMap kt vt => collectHighTypeNames kt; collectHighTypeNames vt
   | .Applied base args =>
     collectHighTypeNames base; args.forM collectHighTypeNames
-  | .Pure base => collectHighTypeNames base
   | .Intersection types => types.forM collectHighTypeNames
   | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString
   | .TBv _ | .Unknown | .MultiValuedExpr _ => pure ()

@@ -55,7 +55,6 @@ partial def highTypeValToArg : HighType → Arg
     -- Applied types are not directly representable in the grammar;
     -- emit the base type as a best-effort approximation
     highTypeToArg base
-  | .Pure base => highTypeToArg base
   | .Intersection types =>
     match types with
     | [] => laurelOp "compositeType" #[ident "Unknown"]

@@ -13,7 +13,9 @@ public import Strata.Util.FileRange
 open StrataDDM
 
 /-
-Documentation for Laurel can be found in docs/verso/LaurelDoc.lean
+Documentation for Laurel can be found in docs/verso/LaurelDesignGuide.lean
+(language definition) and docs/verso/LaurelImplementationGuide.lean
+(translation to Core).
 
 This module contains the Laurel AST. The high-level Laurel API is in
 `Strata.Languages.Laurel`.
@@ -160,8 +162,6 @@ inductive HighType : Type where
   | UserDefined (name : Identifier)
   /-- A generic type application, e.g. `List<Int>`. -/
   | Applied (base : AstNode HighType) (typeArguments : List (AstNode HighType))
-  /-- A pure (value) variant of a composite type that uses structural equality instead of reference equality. -/
-  | Pure (base : AstNode HighType)
   /-- An intersection of types. Used for implicit intersection types, e.g. `Scientist & Scandinavian`. -/
   | Intersection (types : List (AstNode HighType))
   /-- Bitvector type of a given width. -/
@@ -544,7 +544,6 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va
   | HighType.TCore s1, HighType.TCore s2 => s1 == s2
   | HighType.Applied b1 args1, HighType.Applied b2 args2 =>
       highEq b1 b2 && args1.length == args2.length && (args1.attach.zip args2 |>.all (fun (a1, a2) => highEq a1.1 a2))
-  | HighType.Pure b1, HighType.Pure b2 => highEq b1 b2
   | HighType.Intersection ts1, HighType.Intersection ts2 =>
       ts1.length == ts2.length && (ts1.attach.zip ts2 |>.all (fun (t1, t2) => highEq t1.1 t2))
   | HighType.Unknown, HighType.Unknown => true
@@ -638,7 +637,7 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool :=
 /- ### Variance policy (covers `isSubtype` and `isConsistent`)
    All child-carrying constructors are INVARIANT by design: `isConsistent`
    bottoms out in `highEq` (structural equality) for `TSet`, `TMap`,
-   `Applied`, `Pure`, and `Intersection`. So `TSet Unknown ~
+   `Applied`, and `Intersection`. So `TSet Unknown ~
    TSet TInt` is FALSE — `Unknown` is a wildcard only at the TOP of a type,
    never under a constructor. This is intentional: `TSet` / `TMap` are MUTABLE
    collections, where covariance would be unsound; if you don't know the
@@ -650,11 +649,6 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool :=
    targets, so per-element consistency (letting an `Unknown` output flow into
    one slot) is correct rather than unsound.
 
-   `Pure b` is invariant today, but it is the one constructor where covariance
-   would be SOUND and desirable — it is the immutable value-view of a composite,
-   and immutability is exactly the condition that makes covariance safe.
-   TODO: Pure could be covariant once it matters (immutable value-view ⇒ covariance is sound)
-
    `Applied` (generics) is invariant as the safe default for not-yet-designed
    parametric types; real variance is per-constructor and deliberately deferred.
 

@@ -360,9 +360,6 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do
     let base' ← resolveHighType base
     let args' ← args.mapM resolveHighType
     pure (.Applied base' args')
-  | .Pure base =>
-    let base' ← resolveHighType base
-    pure (.Pure base')
   | .Intersection tys =>
     let tys' ← tys.mapM resolveHighType
     pure (.Intersection tys')
@@ -607,7 +604,7 @@ statements are in effect position (synthesized and discarded via
 
 Each typing rule is implemented as its own helper inside the mutual
 block below. Helpers are grouped by section to mirror the *Typing
-rules* index in `LaurelDoc.lean`:
+rules* index in `LaurelDesignGuide.lean`:
 
 - Literals — `Synth.litInt`, `Synth.litBool`, `Synth.litString`, `Synth.litDecimal`
 - Variables — `Synth.varLocal`, `Synth.varField`, `Check.varDeclare`
@@ -2794,7 +2791,6 @@ private def collectHighType (map : Std.HashMap Nat ResolvedNode) (ty : HighTypeM
   | .Applied base args =>
     let map := collectHighType map base
     args.foldl collectHighType map
-  | .Pure base => collectHighType map base
   | .Intersection tys => tys.foldl collectHighType map
   | .MultiValuedExpr tys => tys.foldl collectHighType map
   | _ => map

@@ -46,7 +46,6 @@ partial def resolveAliasType (amap : AliasMap) (ty : HighTypeMd)
     let base' := resolveAliasType amap base visited
     let args' := args.map (resolveAliasType amap · visited)
     { val := .Applied base' args', source := ty.source }
-  | .Pure base => { val := .Pure (resolveAliasType amap base visited), source := ty.source }
   | .Intersection tys =>
     { val := .Intersection (tys.map (resolveAliasType amap · visited)), source := ty.source }
   | _ => ty

@@ -140,7 +140,6 @@ partial def compositeRefToComposite (composites : Std.HashSet String) (ty : High
     { ty with val := .TMap (compositeRefToComposite composites kt) (compositeRefToComposite composites vt) }
   | .Applied base args =>
     { ty with val := .Applied (compositeRefToComposite composites base) (args.map (compositeRefToComposite composites ·)) }
-  | .Pure base => { ty with val := .Pure (compositeRefToComposite composites base) }
   | .Intersection tys => { ty with val := .Intersection (tys.map (compositeRefToComposite composites ·)) }
   | _ => ty
 

@@ -122,9 +122,9 @@ lifting, constrained-type elimination, …) before translating to Core and
 verifying. Several of those passes re-run `resolve` on their output. So a
 diagnostic that only `testLaurel` surfaces may originate from a later pass,
 not the verifier. The major passes are described in the **Translation
-Pipeline** section of the Laurel language manual — published at
-[strata-org.github.io/Strata](https://strata-org.github.io/Strata/laurel/html-single/),
-source in [`docs/verso/LaurelDoc.lean`](verso/LaurelDoc.lean) — and the full
+Pipeline** section of the Laurel implementation guide — published at
+[strata-org.github.io/Strata](https://strata-org.github.io/Strata/laurelimpl/html-single/),
+source in [`docs/verso/LaurelImplementationGuide.lean`](verso/LaurelImplementationGuide.lean) — and the full
 pass list and exact ordering live in
 [`Strata/Languages/Laurel/LaurelCompilationPipeline.lean`](../Strata/Languages/Laurel/LaurelCompilationPipeline.lean)
 (`laurelPipeline`).