Useful but limited polymorphism

README.md

@@ -62,14 +62,19 @@ tricu eval --format decode program.tri
 tricu eval --output result.txt program.tri
 ```
 
-Unchecked eval parses annotation syntax, discards contract metadata, skips
+Annotated programs run normally under `eval`; annotations are metadata, not
-producer-side View Contract checks during workspace module auto-builds, and does
+runtime types. If you want evaluation to ignore View Contracts completely while
-not publish unchecked View refs. 
+loading workspace modules, use unchecked mode:
 
 ```sh
 tricu eval --unchecked program.tri
 ```
 
+Unchecked eval parses annotation syntax, discards contract metadata, skips
+producer-side View Contract checks during workspace module auto-builds, and does
+not publish unchecked View refs. Executable module exports may still be cached in
+the content store.
+
 Check View Contract annotations explicitly:
 
 ```sh

docs/view-contracts.md

@@ -94,35 +94,108 @@ view envelope is well-formed, and recursively validates the `baseView`, but it
 must treat the guard payload/reference as opaque executable data, not as another
 View.
 
-## 4. Soundness Boundary
+## 4. Polymorphic and Abstract Views
 
-Views are descriptive boundary metadata, not types and not proofs about opaque
+View Contracts support portable polymorphism over Views. The View language is
-Tree Calculus terms. In particular, the checker does not claim parametricity,
+interpreted by the same portable checker model implemented in `tricu` terms.
-representation independence, or existential abstraction.
 
-Raw Tree Calculus observation can distinguish values by their tree
+Source syntax may use underscore-prefixed names as View variables inside
-representation. A term advertised as `Fn [A] A` can inspect its argument and
+annotations:
-choose a representation-dependent result; a metadata-only checker cannot rule
-that out. The same issue applies transitively through higher-order arguments and
-dynamically constructed observers.
 
-The checker therefore accepts only monomorphic Views. Legacy `Var`, `Forall`,
+```tri
-and `Exists` tags remain reserved so old artifacts fail deterministically, but
+id x@_a =@_a x
-they are not well-formed checker inputs.
+const x@_a y@_b =@_a x
+compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
+```
 
-The guarantees retained here are narrower:
+In the portable artifact, these lower to scoped View binders rather than
+unscoped source-name conventions. This fits the existing View encoding style:
+Views are tagged records with numeric tags and tagged fields. Polymorphic forms
+are View records such as:
 
-- View and typed-program envelopes are structurally well formed.
+```text
-- Declared monomorphic Views flow consistently across explicit typed nodes.
+Var localId
-- Guarded Views execute their predicates at represented boundaries.
+Forall binders body
-- Artifact references bind metadata to particular stored objects.
+Exists binders body
+```
 
-These guarantees do not establish that an opaque payload has an unguarded
+The current durable encoding uses stable local binder IDs. For example,
-structural View such as `List` or `Fn`. Such Views are conventions/assertions
+`id x@_a =@_a x` exports a shape equivalent to:
-used to place and compose checks. Only an executed guard observes the value.
+
+```text
+Forall [0] (Fn [Var 0] (Var 0))
+```
+
+Source names like `_a` are for authoring; the artifact carries binder scope and
+local IDs rather than relying on source-name identity.
+
+`Forall` supports generic contracts:
+
+```tri
+map f@(Fn [_a] _b) xs@(List _a) =@(List _b) ...
+head xs@(NonEmptyList _a) =@_a ...
+```
+
+At each checked use, the checker instantiates quantified variables into
+use-local internal variables and solves View compatibility constraints. The
+portable checker uses structural use-local IDs rather than expensive numeric
+freshening, and treats unconstrained variable-variable matches as constraints
+that do not create substitution cycles. Concrete observations still bind these
+variables when enough information is available. This is what lets explicitly
+annotated higher-order boundaries accept polymorphic values, for example
+`compose id id "x"`, and lets quantified values satisfy concrete requirements
+such as `Fn [String] String`. It gives useful polymorphic contracts for
+explicitly declared/imported View facts.
+
+`Exists` supports checked abstraction boundaries. A module can expose a value as
+"some representation `_repr` plus capabilities over `_repr`":
+
+```text
+Exists _repr.
+  Pair
+    (Fn [String] _repr)   -- constructor
+    (Fn [_repr] String)   -- renderer / eliminator
+```
+
+This does not make raw Tree Calculus inspection impossible. Unchecked code can
+always inspect trees. It means checked clients cannot justify
+representation-specific operations through the View system unless the package
+exports an appropriate capability or eliminator.
+
+This leads to an important distinction for future checked subsets:
+
+```text
+controlled observation: Bool/List/Maybe/Result/etc. eliminators with Views
+raw observation: direct tree-shape inspection through triage-like power
+```
+
+Useful application code can live mostly in the controlled fragment and receive
+explicit View validation over lambdas, application, let, and typed eliminators.
+Low-level library code may still use raw intensionality, but should expose
+disciplined Views and capabilities above it. Scott-encoded constructors and
+eliminators are a natural tricu-native representation for these APIs.
+
+Tree Calculus terms do not carry intrinsic principal Views, and raw intensional
+code can invalidate parametric claims. View Contracts are an explicit evidence
+and contract layer over tricu programs; limited polymorphic Views are supported
+when they are declared or imported as facts with provenance.
+
+The first stdlib annotation island starts with parametric functions that do not
+inspect representation:
+
+```tri
+id x@_a =@_a x
+const x@_a y@_b =@_a x
+compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
+```
+
+Re-export-only modules preserve imported View metadata, so these contracts flow
+through `prelude` rather than only through direct `base` imports.
+
+Functions built on raw `t`/`triage` should enter the checked world through
+trusted, controlled eliminator contracts rather than by treating arbitrary raw
+inspection as parametric.
 
-See [the intensionality analysis](../notes/view-contract-trust-provenance.md) for
-the rationale and remaining limitations.
 
 ## 5. Guards
 
@@ -186,22 +259,81 @@ A node may contain opaque executable fields. Those fields are tree terms, but
 they are not recursively decoded as view-tree nodes or Views unless the node's
 semantics explicitly says so.
 
-View facts may carry per-fact provenance:
+View facts may also carry explicit per-fact trust provenance:
 
 ```text
-Checked
+Checked    -- derived by checked lowering / checker validation
-Trusted
+Trusted    -- asserted by a trusted boundary, e.g. a primitive eliminator API
-Unchecked
+Unchecked  -- raw or assumed; no parametricity/abstraction guarantee
 ```
 
-These labels are retained for artifact compatibility and auditing. They identify
+In the portable view-tree envelope this provenance is represented as an optional
-the source of an assertion; they do not prove semantic membership, parametricity,
+field on `typedValue` / `typedRequire` facts. In module manifests the same
-or abstraction. An absent label is interpreted conservatively as `Unchecked`.
+provenance is carried beside the exported View Contract object reference so that
+imports and re-exports preserve it without relying on module-level convention.
+Absent provenance is interpreted conservatively as `Unchecked` at use sites.
 
-The former value-level polymorphic `viewFacts` catalogs and frontend
+For parametric checked definitions, the frontend now performs a conservative
-raw-intensionality taint pass have been removed. Monomorphic imported facts may
+raw-intensionality dependency pass over local definitions. If a definition with
-still be attached to exports, but consumers must treat them as assertions unless
+scoped View variables depends directly or indirectly on raw `triage` / raw `t`
-an executable guard enforces the relevant property.
+construction, or on an imported `Unchecked` fact, lowering fails and asks the
+author to route observation through a trusted eliminator boundary. This is
+intentionally provenance/dependency based; it is not an attempt to decide
+whether arbitrary Tree Calculus reduction will ever reach rule 3.
+
+View facts can be authored as ordinary value-level Tree Calculus metadata under
+one conventional top-level name:
+
+```text
+viewFacts = [fact ...]
+fact      = pair exportName (pair provenance view)
+```
+
+where `exportName` is a string naming a value exported by the module,
+`provenance` is `0 = Checked`, `1 = Trusted`, or `2 = Unchecked`, and `view` is
+the same portable View record used by `view-tree` artifacts. The host evaluates
+this value and decodes the data schema; it does not infer trust from source
+syntax, AST shape, module name, or a Haskell-side catalog.
+
+The initial trusted eliminator facts are authored this way in clearly separated
+stdlib `viewFacts` sections:
+
+```text
+matchBool  : forall r. r -> r -> Bool -> r
+matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
+matchList  : forall a r. r -> (a -> List a -> r) -> List a -> r
+```
+
+The `base` module provides small `facts*` authoring helpers for this advanced
+metadata, e.g. `factsFact`, `factsChecked`, `factsTrusted`, `factsUnchecked`,
+`factsForall`, `factsFn`, `factsVar`, `factsBool`, `factsString`, `factsByte`,
+`factsUnit`, `factsMaybe`, and `factsList`. These helpers construct ordinary
+Tree data; authority comes from the exported `viewFacts` value and its explicit
+provenance tags. Loader validation rejects duplicate fact names and facts for
+names the module does not export.
+
+Initial derived stdlib annotations using this trusted kernel include:
+
+```text
+maybeMap  : forall a b. (a -> b) -> Maybe a -> Maybe b
+maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
+maybeOr   : forall a. a -> Maybe a -> a
+```
+
+Recursive list combinators are currently published as explicit `Trusted`
+value-level facts rather than `Checked` source annotations, because their bodies
+pass through raw fixed-point machinery that the conservative parametric taint
+pass intentionally does not prove safe. This is the stabilized boundary: raw
+stdlib kernels establish conventions with explicit authority; ordinary checked
+clients consume those facts rather than re-proving the internals.
+
+```text
+headMaybe / lastMaybe / nthMaybe
+append / map / filter / foldl / foldr
+length / reverse / snoc / count / all? / any? / intersect
+take / drop / splitAt / concatMap / find / partition / zipWith
+string/list-byte helpers such as strLength, startsWith?, lines, words
+```
 
 ## 7. Checker Semantics
 

lib/base.tri

@@ -1,8 +1,8 @@
 false = t
 _     = t
 true  = t t
-id a = a
+id a@_a =@_a a
-const a b = a
+const a@_a b@_b =@_a a
 pair  = t
 if cond then else = t (t else (t t then)) t cond
 
@@ -10,7 +10,7 @@ y = ((mut wait fun : wait mut (x : fun (wait mut x)))
      (x : x x)
      (a0 a1 a2 : t (t a0) (t t a2) a1))
 
-compose f g x = f (g x)
+compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
 
 triage leaf stem fork = t (t leaf stem) fork
 test   = triage "Leaf" (_ : "Stem") (_ _ : "Fork")
@@ -114,9 +114,9 @@ matchMaybe nothingCase justCase maybe =
     maybe
 
 maybe default f m = matchMaybe default f m
-maybeMap f m = matchMaybe nothing (x : just (f x)) m
+maybeMap f@(Fn [_a] _b) m@(Maybe _a) =@(Maybe _b) matchMaybe nothing (compose just f) m
-maybeBind m f = matchMaybe nothing f m
+maybeBind m@(Maybe _a) f@(Fn [_a] (Maybe _b)) =@(Maybe _b) matchMaybe nothing f m
-maybeOr default m = matchMaybe default id m
+maybeOr default@_a m@(Maybe _a) =@_a matchMaybe default id m
 maybe? = matchMaybe false (_ : true)
 
 -- ---------------------------------------------------------------------------
@@ -221,3 +221,165 @@ resultMapErr = (f result :
 -- ---------------------------------------------------------------------------
 -- View facts
 -- ---------------------------------------------------------------------------
+
+factsFact name provenance view = pair name (pair provenance view)
+factsChecked = 0
+factsTrusted = 1
+factsUnchecked = 2
+factsField tag value = pair tag value
+factsRecord tag fields = pair tag fields
+factsVar id = factsRecord 8 [(factsField 10 id)]
+factsForall binders body =
+  factsRecord 9 [(factsField 11 binders) (factsField 12 body)]
+factsFn args result =
+  factsRecord 1 [(factsField 0 args) (factsField 1 result)]
+factsAny = factsRecord 0 []
+factsRef symbol = factsRecord 2 [(factsField 2 symbol)]
+factsBool = factsRef 0
+factsString = factsRef 1
+factsByte = factsRef 2
+factsUnit = factsRef 3
+factsMaybe elem = factsRecord 4 [(factsField 3 elem)]
+factsList elem = factsRecord 3 [(factsField 3 elem)]
+factsPair left right = factsRecord 5 [(factsField 4 left) (factsField 5 right)]
+factsResult err ok = factsRecord 6 [(factsField 6 err) (factsField 7 ok)]
+
+viewFacts =
+  [ (factsFact "pair" factsTrusted
+      (factsForall [0]
+        (factsFn
+          [(factsVar 0) (factsList (factsVar 0))]
+          (factsList (factsVar 0)))))
+    (factsFact "nothing" factsTrusted
+      (factsForall [0]
+        (factsMaybe (factsVar 0))))
+    (factsFact "just" factsTrusted
+      (factsForall [0]
+        (factsFn [(factsVar 0)] (factsMaybe (factsVar 0)))))
+    (factsFact "false" factsTrusted factsBool)
+    (factsFact "true" factsTrusted factsBool)
+    (factsFact "if" factsTrusted
+      (factsForall [0]
+        (factsFn [factsBool (factsVar 0) (factsVar 0)] (factsVar 0))))
+    (factsFact "triage" factsTrusted
+      (factsForall [0]
+        (factsFn [factsAny factsAny factsAny factsAny] (factsVar 0))))
+    (factsFact "test" factsTrusted factsString)
+    (factsFact "matchBool" factsTrusted
+      (factsForall [0]
+        (factsFn
+          [(factsVar 0) (factsVar 0) factsBool]
+          (factsVar 0))))
+    (factsFact "lAnd" factsTrusted
+      (factsFn [factsBool factsBool] factsBool))
+    (factsFact "lOr" factsTrusted
+      (factsFn [factsBool factsBool] factsBool))
+    (factsFact "matchPair" factsTrusted
+      (factsForall [0 1 2]
+        (factsFn
+          [(factsFn [(factsVar 0) (factsVar 1)] (factsVar 2))
+           (factsPair (factsVar 0) (factsVar 1))]
+          (factsVar 2))))
+    (factsFact "fst" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsPair (factsVar 0) (factsVar 1))] (factsVar 0))))
+    (factsFact "snd" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsPair (factsVar 0) (factsVar 1))] (factsVar 1))))
+    (factsFact "not?" factsTrusted
+      (factsFn [factsBool] factsBool))
+    (factsFact "and?" factsTrusted
+      (factsFn [factsBool factsBool] factsBool))
+    (factsFact "or?" factsTrusted
+      (factsFn [factsBool factsBool] factsBool))
+    (factsFact "xor?" factsTrusted
+      (factsFn [factsBool factsBool] factsBool))
+    (factsFact "equal?" factsTrusted
+      (factsForall [0]
+        (factsFn [(factsVar 0) (factsVar 0)] factsBool)))
+    (factsFact "succ" factsTrusted
+      (factsFn [factsByte] factsByte))
+    (factsFact "pred" factsTrusted
+      (factsFn [factsByte] factsByte))
+    (factsFact "isZero?" factsTrusted
+      (factsFn [factsByte] factsBool))
+    (factsFact "add" factsTrusted
+      (factsFn [factsByte factsByte] factsByte))
+    (factsFact "sub" factsTrusted
+      (factsFn [factsByte factsByte] factsByte))
+    (factsFact "lte?" factsTrusted
+      (factsFn [factsByte factsByte] factsBool))
+    (factsFact "gte?" factsTrusted
+      (factsFn [factsByte factsByte] factsBool))
+    (factsFact "lt?" factsTrusted
+      (factsFn [factsByte factsByte] factsBool))
+    (factsFact "gt?" factsTrusted
+      (factsFn [factsByte factsByte] factsBool))
+    (factsFact "mul" factsTrusted
+      (factsFn [factsByte factsByte] factsByte))
+    (factsFact "matchMaybe" factsTrusted
+      (factsForall [0 1]
+        (factsFn
+          [(factsVar 1)
+           (factsFn [(factsVar 0)] (factsVar 1))
+           (factsMaybe (factsVar 0))]
+          (factsVar 1))))
+    (factsFact "maybe" factsTrusted
+      (factsForall [0 1]
+        (factsFn
+          [(factsVar 1)
+           (factsFn [(factsVar 0)] (factsVar 1))
+           (factsMaybe (factsVar 0))]
+          (factsVar 1))))
+    (factsFact "maybe?" factsTrusted
+      (factsForall [0]
+        (factsFn [(factsMaybe (factsVar 0))] factsBool)))
+    (factsFact "ifLazy" factsTrusted
+      (factsForall [0]
+        (factsFn
+          [factsBool
+           (factsFn [factsUnit] (factsVar 0))
+           (factsFn [factsUnit] (factsVar 0))]
+          (factsVar 0))))
+    (factsFact "andLazy?" factsTrusted
+      (factsFn [factsBool (factsFn [factsUnit] factsBool)] factsBool))
+    (factsFact "ok" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsVar 1) factsAny] (factsResult (factsVar 0) (factsVar 1)))))
+    (factsFact "err" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsVar 0) factsAny] (factsResult (factsVar 0) (factsVar 1)))))
+    (factsFact "matchResult" factsTrusted
+      (factsForall [0 1 2]
+        (factsFn
+          [(factsFn [(factsVar 0) factsAny] (factsVar 2))
+           (factsFn [(factsVar 1) factsAny] (factsVar 2))
+           (factsResult (factsVar 0) (factsVar 1))]
+          (factsVar 2))))
+    (factsFact "resultIsOk" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsResult (factsVar 0) (factsVar 1))] factsBool)))
+    (factsFact "resultIsErr" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsResult (factsVar 0) (factsVar 1))] factsBool)))
+    (factsFact "mapResult" factsTrusted
+      (factsForall [0 1 2]
+        (factsFn
+          [(factsFn [(factsVar 1)] (factsVar 2))
+           (factsResult (factsVar 0) (factsVar 1))]
+          (factsResult (factsVar 0) (factsVar 2)))))
+    (factsFact "bindResult" factsTrusted
+      (factsForall [0 1 2]
+        (factsFn
+          [(factsResult (factsVar 0) (factsVar 1))
+           (factsFn [(factsVar 1)] (factsResult (factsVar 0) (factsVar 2)))]
+          (factsResult (factsVar 0) (factsVar 2)))))
+    (factsFact "resultOr" factsTrusted
+      (factsForall [0 1]
+        (factsFn [(factsVar 1) (factsResult (factsVar 0) (factsVar 1))] (factsVar 1))))
+    (factsFact "resultMapErr" factsTrusted
+      (factsForall [0 1 2]
+        (factsFn
+          [(factsFn [(factsVar 0)] (factsVar 2))
+           (factsResult (factsVar 0) (factsVar 1))]
+          (factsResult (factsVar 2) (factsVar 1)))))]

lib/list.tri

@@ -291,3 +291,151 @@ zipWith_ self f xs ys =
         ys)
     xs
 zipWith = f xs ys : y zipWith_ f xs ys
+
+-- ---------------------------------------------------------------------------
+-- View facts
+--
+-- Value-level metadata consumed by View tooling. These facts are ordinary Tree
+-- Calculus data, not host-side assumptions and not part of the public stdlib
+-- API exported by module manifests.
+-- ---------------------------------------------------------------------------
+
+viewFacts =
+  [(factsFact "matchList" factsTrusted
+     (factsForall [0 1]
+       (factsFn
+         [(factsVar 1)
+          (factsFn
+            [(factsVar 0) (factsList (factsVar 0))]
+            (factsVar 1))
+          (factsList (factsVar 0))]
+         (factsVar 1))))
+   (factsFact "emptyList?" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0))] factsBool)))
+   (factsFact "tail" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0))] (factsList (factsVar 0)))))
+   (factsFact "append" factsTrusted
+     (factsForall [0]
+       (factsFn
+         [(factsList (factsVar 0))
+          (factsList (factsVar 0))]
+         (factsList (factsVar 0)))))
+   (factsFact "lExist?" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsVar 0) (factsList (factsVar 0))] factsBool)))
+   (factsFact "map" factsTrusted
+     (factsForall [0 1]
+       (factsFn
+         [(factsFn [(factsVar 0)] (factsVar 1))
+          (factsList (factsVar 0))]
+         (factsList (factsVar 1)))))
+   (factsFact "filter" factsTrusted
+     (factsForall [0]
+       (factsFn
+         [(factsFn [(factsVar 0)] factsBool)
+          (factsList (factsVar 0))]
+         (factsList (factsVar 0)))))
+   (factsFact "foldl" factsTrusted
+     (factsForall [0 1]
+       (factsFn
+         [(factsFn [(factsVar 1) (factsVar 0)] (factsVar 1))
+          (factsVar 1)
+          (factsList (factsVar 0))]
+         (factsVar 1))))
+   (factsFact "foldr" factsTrusted
+     (factsForall [0 1]
+       (factsFn
+         [(factsFn [(factsVar 1) (factsVar 0)] (factsVar 1))
+          (factsVar 1)
+          (factsList (factsVar 0))]
+         (factsVar 1))))
+   (factsFact "length" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0))] factsByte)))
+   (factsFact "reverse" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0))] (factsList (factsVar 0)))))
+   (factsFact "snoc" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsVar 0) (factsList (factsVar 0))] (factsList (factsVar 0)))))
+   (factsFact "count" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsVar 0) (factsList (factsVar 0))] factsByte)))
+   (factsFact "all?" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsFn [(factsVar 0)] factsBool) (factsList (factsVar 0))] factsBool)))
+   (factsFact "any?" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsFn [(factsVar 0)] factsBool) (factsList (factsVar 0))] factsBool)))
+   (factsFact "intersect" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0)) (factsList (factsVar 0))] (factsList (factsVar 0)))))
+   (factsFact "headMaybe" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
+   (factsFact "lastMaybe" factsTrusted
+     (factsForall [0]
+       (factsFn [(factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
+   (factsFact "nthMaybe" factsTrusted
+     (factsForall [0]
+       (factsFn [factsByte (factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
+   (factsFact "take" factsTrusted
+     (factsForall [0]
+       (factsFn [factsByte (factsList (factsVar 0))] (factsList (factsVar 0)))))
+   (factsFact "drop" factsTrusted
+     (factsForall [0]
+       (factsFn [factsByte (factsList (factsVar 0))] (factsList (factsVar 0)))))
+   (factsFact "splitAt" factsTrusted
+     (factsForall [0]
+       (factsFn
+         [factsByte (factsList (factsVar 0))]
+         (factsPair (factsList (factsVar 0)) (factsList (factsVar 0))))))
+   (factsFact "concatMap" factsTrusted
+     (factsForall [0 1]
+       (factsFn
+         [(factsFn [(factsVar 0)] (factsList (factsVar 1)))
+          (factsList (factsVar 0))]
+         (factsList (factsVar 1)))))
+   (factsFact "find" factsTrusted
+     (factsForall [0]
+       (factsFn
+         [(factsFn [(factsVar 0)] factsBool)
+          (factsList (factsVar 0))]
+         (factsMaybe (factsVar 0)))))
+   (factsFact "partition" factsTrusted
+     (factsForall [0]
+       (factsFn
+         [(factsFn [(factsVar 0)] factsBool)
+          (factsList (factsVar 0))]
+         (factsPair (factsList (factsVar 0)) (factsList (factsVar 0))))))
+   (factsFact "strLength" factsTrusted
+     (factsFn [factsString] factsByte))
+   (factsFact "strAppend" factsTrusted
+     (factsFn [factsString factsString] factsString))
+   (factsFact "strEq?" factsTrusted
+     (factsFn [factsString factsString] factsBool))
+   (factsFact "strEmpty?" factsTrusted
+     (factsFn [factsString] factsBool))
+   (factsFact "startsWith?" factsTrusted
+     (factsFn [factsString factsString] factsBool))
+   (factsFact "endsWith?" factsTrusted
+     (factsFn [factsString factsString] factsBool))
+   (factsFact "contains?" factsTrusted
+     (factsFn [factsString factsString] factsBool))
+   (factsFact "lines" factsTrusted
+     (factsFn [factsString] (factsList factsString)))
+   (factsFact "unlines" factsTrusted
+     (factsFn [(factsList factsString)] factsString))
+   (factsFact "words" factsTrusted
+     (factsFn [factsString] (factsList factsString)))
+   (factsFact "unwords" factsTrusted
+     (factsFn [(factsList factsString)] factsString))
+   (factsFact "zipWith" factsTrusted
+     (factsForall [0 1 2]
+       (factsFn
+         [(factsFn [(factsVar 0) (factsVar 1)] (factsVar 2))
+          (factsList (factsVar 0))
+          (factsList (factsVar 1))]
+         (factsList (factsVar 2)))))]

lib/view.tri

@@ -335,12 +335,11 @@ wellFormedResultView? = (view :
 wellFormedGuardedView? = (view :
   fields2? (viewPayload view) viewFieldBase viewFieldGuard)
 
--- Tags 8-10 remain reserved so old artifacts decode deterministically, but
+wellFormedVarView? = (view :
--- quantified/variable Views are no longer accepted by the checker. They
+  fields1? (viewPayload view) viewFieldVar)
--- implied abstraction and parametricity that raw Tree Calculus cannot enforce.
-wellFormedVarView? = (_ : false)
 
-wellFormedQuantifiedView? = (_ : false)
+wellFormedQuantifiedView? = (view :
+  fields2? (viewPayload view) viewFieldBinders viewFieldBody)
 
 wellFormedView_ self view =
   lazyBool
@@ -514,6 +513,28 @@ hasView? = (symbol view env :
     (viewSet : viewSetHas? view viewSet)
     (lookupViews symbol env))
 
+viewSetHasCompatible_ self namespace expected viewSet =
+  lazyList
+    (_ : false)
+    (fact rest :
+      lazyMaybe
+        (_ : self namespace expected rest)
+        (_ : true)
+        (matchView expected (instantiateView namespace (viewFactView fact)) t))
+    viewSet
+
+viewSetHasCompatible? = (namespace expected viewSet :
+  lazyBool
+    (_ : true)
+    (_ : y viewSetHasCompatible_ namespace expected viewSet)
+    (anyView? expected))
+
+hasCompatibleView? = (symbol view env :
+  lazyMaybe
+    (_ : anyView? view)
+    (viewSet : viewSetHasCompatible? symbol view viewSet)
+    (lookupViews symbol env))
+
 addViewToSet = (view evidence viewSet :
   lazyBool
     (_ : viewSet)
@@ -536,19 +557,44 @@ extendEnv_ self symbol view evidence env =
 extendEnv = (symbol view evidence env :
   y extendEnv_ symbol view evidence env)
 
-findFnView_ self viewSet =
+instantiateVarId = (namespace localId :
+  pair namespace localId)
+
+instantiateBinders_ self namespace binders subst =
+  lazyList
+    (_ : subst)
+    (binder rest :
+      self namespace rest (pair (pair binder (viewVar (instantiateVarId namespace binder))) subst))
+    binders
+
+instantiateBinders = (namespace binders subst :
+  y instantiateBinders_ namespace binders subst)
+
+instantiateView = (namespace view :
+  lazyBool
+    (_ : substituteView (instantiateBinders namespace (viewBinderNames view) t) (viewQuantifiedBody view))
+    (_ : view)
+    (forallView? view))
+
+viewAsFn = (namespace view :
+  let instantiated = instantiateView namespace view in
+  lazyBool
+    (_ : just instantiated)
+    (_ : nothing)
+    (fnView? instantiated))
+
+findFnView_ self namespace viewSet =
   lazyList
     (_ : nothing)
     (fact rest :
-      let view = viewFactView fact in
+      lazyMaybe
-      lazyBool
-        (_ : just view)
         (_ : self rest)
-        (fnView? view))
+        (fnView : just fnView)
+        (viewAsFn namespace (viewFactView fact)))
     viewSet
 
-findFnView = (viewSet :
+findFnView = (namespace viewSet :
-  y findFnView_ viewSet)
+  y findFnView_ namespace viewSet)
 
 firstKnownView = (viewSet :
   lazyList
@@ -561,6 +607,157 @@ actualViewFor = (symbol env :
     (_ : viewAny)
     (viewSet : firstKnownView viewSet)
     (lookupViews symbol env))
+
+substLookup_ self name subst =
+  lazyList
+    (_ : nothing)
+    (entry rest :
+      lazyBool
+        (_ : just (snd entry))
+        (_ : self name rest)
+        (equal? name (fst entry)))
+    subst
+
+substLookup = (name subst : y substLookup_ name subst)
+
+substBind = (name actual subst :
+  lazyBool
+    (_ : just subst)
+    (_ :
+      lazyBool
+        (_ : just subst)
+        (_ :
+          lazyMaybe
+            (_ : just (pair (pair name actual) subst))
+            (existing :
+              lazyBool
+                (_ : just subst)
+                (_ : nothing)
+                (equal? existing actual))
+            (substLookup name subst))
+        (varView? actual))
+    (equal? actual (viewVar name)))
+
+substituteView_ self subst view =
+  lazyBool
+    (_ :
+      lazyMaybe
+        (_ : view)
+        (bound : self subst bound)
+        (substLookup (viewVarName view) subst))
+    (_ :
+      lazyBool
+        (_ : viewFn (y substituteViews_ self subst (fnArgs view)) (self subst (fnResult view)))
+        (_ :
+          lazyBool
+            (_ : viewList (self subst (field0 (viewPayload view))))
+            (_ :
+              lazyBool
+                (_ : viewMaybe (self subst (field0 (viewPayload view))))
+                (_ :
+                  lazyBool
+                    (_ : viewPair (self subst (field0 (viewPayload view))) (self subst (field1 (viewPayload view))))
+                    (_ :
+                      lazyBool
+                        (_ : viewResult (self subst (field0 (viewPayload view))) (self subst (field1 (viewPayload view))))
+                        (_ :
+                          lazyBool
+                            (_ : viewGuarded (self subst (guardedViewBase view)) (guardedViewGuard view))
+                            (_ : view)
+                            (guardedView? view))
+                        (resultView? view))
+                    (pairView? view))
+                (maybeView? view))
+            (listView? view))
+        (fnView? view))
+    (varView? view)
+
+substituteViews_ self viewSelf subst views =
+  lazyList
+    (_ : t)
+    (view rest : pair (viewSelf subst view) (self viewSelf subst rest))
+    views
+
+substituteView = (subst view : y substituteView_ subst view)
+
+matchViewList_ self matchSelf expected actual subst =
+  lazyList
+    (_ :
+      lazyList
+        (_ : just subst)
+        (_ _ : nothing)
+        actual)
+    (expectedHead expectedRest :
+      lazyList
+        (_ : nothing)
+        (actualHead actualRest :
+          lazyMaybe
+            (_ : nothing)
+            (nextSubst : self matchSelf expectedRest actualRest nextSubst)
+            (matchSelf expectedHead actualHead subst))
+        actual)
+    expected
+
+matchView_ self expected actual subst =
+  lazyBool
+    (_ : just subst)
+    (_ :
+      lazyBool
+        (_ : substBind (viewVarName expected) actual subst)
+        (_ :
+          lazyBool
+            (_ : substBind (viewVarName actual) expected subst)
+            (_ :
+              lazyBool
+                (_ : just subst)
+                (_ :
+                  lazyBool
+                    (_ :
+                      lazyMaybe
+                        (_ : nothing)
+                        (argSubst : self (fnResult expected) (fnResult actual) argSubst)
+                        (y matchViewList_ self (fnArgs expected) (fnArgs actual) subst))
+                    (_ :
+                      lazyBool
+                        (_ : self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst)
+                    (_ :
+                      lazyBool
+                        (_ : self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst)
+                        (_ :
+                          lazyBool
+                            (_ :
+                              lazyMaybe
+                                (_ : nothing)
+                                (leftSubst : self (field1 (viewPayload expected)) (field1 (viewPayload actual)) leftSubst)
+                                (self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst))
+                            (_ :
+                              lazyBool
+                                (_ :
+                                  lazyMaybe
+                                    (_ : nothing)
+                                    (errSubst : self (field1 (viewPayload expected)) (field1 (viewPayload actual)) errSubst)
+                                    (self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst))
+                                (_ :
+                                  lazyBool
+                                    (_ : self (guardedViewBase expected) actual subst)
+                                    (_ :
+                                      lazyBool
+                                        (_ : self expected (guardedViewBase actual) subst)
+                                        (_ : nothing)
+                                        (guardedView? actual))
+                                    (guardedView? expected))
+                                (and? (resultView? expected) (resultView? actual)))
+                            (and? (pairView? expected) (pairView? actual)))
+                        (and? (maybeView? expected) (maybeView? actual)))
+                    (and? (listView? expected) (listView? actual)))
+                (and? (fnView? expected) (fnView? actual)))
+                (equal? expected actual))
+            (varView? actual))
+        (varView? expected))
+    (anyView? expected)
+
+matchView = (expected actual subst : y matchView_ expected actual subst)
+
 checkerErr = (tag fields env : err (diagnostic tag fields) env)
 checkerOk = (env : ok env t)
 
@@ -592,16 +789,28 @@ checkApplicationSymbols = (policy argSymbol outSymbol env fnView :
   lazyList
     (_ : checkerErr errorTagZeroArityFunction t env)
     (argView restArgs :
-      let resultView = fnResidual restArgs (fnResult fnView) in
+      let actualView = instantiateView argSymbol (actualViewFor argSymbol env) in
-      lazyBool
+      lazyMaybe
-        (_ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred env))
         (_ :
           lazyResult
             (diag envAtError : err diag envAtError)
-            (nextEnv _ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred nextEnv))
+            (nextEnv _ : checkerOk (extendEnv outSymbol (fnResidual restArgs (fnResult fnView)) evidenceTagInferred nextEnv))
             (missingArgumentOrGuardedBase policy argSymbol argView env))
-        (hasView? argSymbol argView env))
+        (subst :
+          let nextEnv =
+            lazyBool
+              (_ : extendEnv argSymbol argView evidenceTagRequired env)
+              (_ : env)
+              (guardedView? argView) in
+          checkerOk
+            (extendEnv
+              outSymbol
+              (substituteView subst (fnResidual restArgs (fnResult fnView)))
+              evidenceTagInferred
+              nextEnv))
+        (matchView argView actualView t))
     (fnArgs fnView))
+
 -- ---------------------------------------------------------------------------
 -- View-tree checker artifact
 -- ---------------------------------------------------------------------------
@@ -755,7 +964,7 @@ checkTypedRequireNode = (policy node env :
             (hasView? symbol (guardedViewBase view) env))
         (_ : missingRequiredView policy symbol view env)
         (guardedView? view))
-    (hasView? symbol view env))
+    (hasCompatibleView? symbol view env))
 
 missingArgumentOrGuardedBase = (policy symbol view env :
   lazyBool
@@ -774,7 +983,7 @@ checkTypedApplyNode = (policy node env :
       lazyMaybe
         (_ : checkerOk env)
         (fnView : checkApplicationSymbols policy (typedApplyArg node) (typedNodeSymbol node) env fnView)
-        (findFnView calleeViews))
+        (findFnView (typedApplyCallee node) calleeViews))
     (lookupViews (typedApplyCallee node) env))
 
 checkTypedNode = (policy node env :
@@ -1553,8 +1762,8 @@ viewContractSelfTests = [
   (viewContractProbe (wellFormedView? (viewPair viewBool viewString)))
   (viewContractProbe (wellFormedView? (viewResult viewString viewBool)))
   (viewContractProbe (wellFormedView? (viewGuarded viewString (x : x))))
-  (viewContractProbe (not? (wellFormedView? (viewVar 0))))
+  (viewContractProbe (wellFormedView? (viewVar 0)))
-  (viewContractProbe (not? (wellFormedView? (viewForall [(0)] (viewFn [(viewVar 0)] (viewVar 0))))))
+  (viewContractProbe (wellFormedView? (viewForall [(0)] (viewFn [(viewVar 0)] (viewVar 0)))))
   (viewContractProbe (equal? (renderView viewBool) "Bool"))
   (viewContractProbe (equal? (renderView (viewList viewBool)) "List Bool"))
   (viewContractProbe (equal? (renderView (viewMaybe viewString)) "Maybe String"))

notes/view-contract-trust-provenance.md

@@ -1,95 +1,122 @@
-# View Contracts at the intensionality boundary
+# View Contract trust provenance and controlled intensionality
 
-## Conclusion
+## Problem
 
-Tree Calculus does not support the abstraction theorem that the former
+Tree Calculus / tricu code can perform raw intensional observation through `t` /
-parametric View design assumed. Views can remain useful as boundary metadata and
+`triage`-like power. Exact detection of whether an arbitrary term ever reaches
-as instructions for runtime guard placement, but they must not be presented as
+rule 3 is undecidable: the SK fragment is already Turing-complete, and a program
-types, proofs of parametricity, or representation-hiding abstraction.
+can construct/apply an intensional observer iff an encoded machine halts.
 
-## Fundamental conflicts
+Therefore View Contracts must not rely on an exact semantic test for "will this
+term inspect representation?".
 
-### Raw observation defeats representation independence
+## Key correction
 
-A parametric contract such as:
+A purely syntactic invariant such as "the initial tree contains no
+`Fork(Fork(_, _), _)`" is not reduction-closed. For example:
 
 ```text
-forall a. a -> a
+Fork (Stem (Fork a b)) c  ==>  Fork (Fork a b) c
 ```
 
-normally relies on code being unable to learn anything about `a`. A Tree
+So absence of a current rule-3 redex is not enough.
-Calculus term can inspect the tree supplied at `a`, distinguish
-representations, and return a representation-dependent value. The View variable
-does not hide or seal that tree.
 
-The same breaks existential abstraction. Advertising a payload as
+## Direction
-`exists repr. ...` changes no operational capability: a client can still
-inspect the representation directly.
 
-### Opaque payloads are asserted, not checked
+Use explicit provenance/capability discipline, not exact intensionality
+decision.
 
-A typed-value node carries an executable tree beside a View. Metadata validation
+View Contract checking and parametric checked-subset validation are distinct:
-deliberately treats that executable field as opaque. Consequently, accepting a
-node proves that the envelope and View are well formed; it does not prove that
-the tree denotes the advertised `Fn`, `List`, `Maybe`, or other structural
-View.
 
-Provenance labels do not change this. `Checked` and `Trusted` record where an
+- View Contract checking: verifies executable tree artifacts against declared
-assertion came from, but neither is a derivation that another implementation can
+  boundary Views.
-replay to establish the assertion.
+- Parametric checked-subset validation: verifies that abstraction/parametricity
+  claims do not depend on raw untrusted intensional observation.
 
-### Syntactic taint is not a semantic parametricity proof
+Unchecked/raw Tree Calculus can always inspect trees. Existential/abstract Views
+are checker-level opacity: checked clients cannot justify representation-specific
+operations unless an exported trusted capability/eliminator provides them.
 
-Rejecting direct uses of `t` or `triage` is neither complete nor a stable
+## Provenance model
-soundness boundary:
 
-- an observer can be assembled after reduction;
+Contract facts/artifacts should carry explicit provenance. Do not rely on module
-- observation can arrive through higher-order or dynamically selected code;
+or catalog convention.
-- unknown external code can hide observation;
-- absence of a rule-3 redex is not reduction-closed;
-- exact detection would subsume non-trivial termination/reachability questions.
 
-A conservative taint pass can define a programming convention, but it cannot
+Recommended durable provenance classes:
-justify the parametric or abstraction guarantees previously attached to Views.
 
-### Flow checking only checks represented flow
+```text
+Checked  -- derived by checked lowering / checker validation
+Trusted  -- asserted by a trusted boundary, e.g. a primitive eliminator API
+Unchecked -- no abstraction/parametricity guarantee; raw/assumed fact if exposed
+```
 
-The checker sees frontend-emitted value, application, and requirement nodes. It
+The correct granularity is per exported View fact, not per module. A single
-can check consistency among those nodes, but it cannot establish that the graph
+module may contain checked definitions, trusted eliminators, and unchecked raw
-faithfully represents every use performed by the opaque executable payload.
+helpers.
-This is useful artifact validation, not whole-program typing.
 
-## Retained contract
+## Controlled intensionality
 
-The reduced checker may soundly claim only:
+Raw intensionality should be tracked by dependency/provenance, not syntax-only.
 
-1. View, node, and program envelopes satisfy their declared data schemas.
+- Direct `triage` / arbitrary `t` eliminator use is raw intensional capability.
-2. Explicit monomorphic View facts are propagated consistently through the
+- Trusted eliminators expose controlled observation and do not taint clients.
-   represented application graph.
+- Calling unchecked/untrusted code taints the caller for parametricity purposes.
-3. A `Guarded` View causes its executable predicate to run at represented
+- Constructors/literals are not automatically tainting unless they expose raw
-   boundaries, and guard failure prevents checked execution.
+  inspection power.
-4. Content-addressed references prevent an attached View artifact from silently
-   drifting to a different stored object.
 
-Items 1, 2, and 4 establish metadata integrity, not semantic membership in an
+Parametric checked mode rejects annotated definitions whose derivation depends
-unguarded View. Item 3 is the only retained mechanism that observes an ordinary
+on raw/untrusted intensionality, while trusted facts may describe raw internals
-runtime value.
+behind explicit contracts.
 
-## Code direction
+## Trusted eliminator kernel
 
-The initial rollback therefore:
+First trusted observation capabilities should be the smallest useful kernels:
 
-- removes View-variable instantiation, substitution, and unification from the
+```text
-  portable checker;
+matchBool  : forall r. r -> r -> Bool -> r
-- rejects `Var`, `Forall`, and `Exists` as checker inputs while reserving
+matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
-  their legacy tags for deterministic decoding;
+matchList  : forall a r. r -> (a -> List a -> r) -> List a -> r
-- removes the frontend raw-intensionality taint pass;
+```
-- removes polymorphic stdlib annotations and value-level View facts;
-- retains monomorphic View flow, artifact plumbing, diagnostics, and executable
-  guards.
 
-Further simplification should treat unguarded structural Views as descriptive
+Derived functions should be checked against these trusted capabilities where
-labels. If stronger guarantees are desired later, they require an operational
+possible. Raw recursive kernels and other code
-mechanism such as runtime recognizers/seals or a genuinely restricted language
+that passes through fixed-point/intensional machinery should publish explicit
-whose evaluator enforces the restriction. Metadata provenance alone is
+`Trusted` facts rather than being treated as checked.
-insufficient.
+
+Current stdlib shape:
+
+```text
+Checked annotations where the body checks through trusted capabilities:
+  maybeMap  : forall a b. (a -> b) -> Maybe a -> Maybe b
+  maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
+  maybeOr   : forall a. a -> Maybe a -> a
+
+Trusted value-level facts for raw/recursive stdlib boundaries:
+  headMaybe / lastMaybe / nthMaybe
+  append / map / filter / foldl / foldr
+  length / reverse / snoc / count / all? / any? / intersect
+  take / drop / splitAt / concatMap / find / partition / zipWith
+  string/list-byte helpers such as strLength, startsWith?, lines, words
+```
+
+Do not assign total contracts to partial APIs such as:
+
+```text
+head : List a -> a
+```
+
+Prefer `headMaybe : List a -> Maybe a`, or later introduce `NonEmptyList a`.
+
+## Implementation order
+
+Most-correct tractable path:
+
+1. Add contract provenance to the Haskell View model and portable artifacts. ✅
+2. Preserve provenance through module exports/imports/re-exports. ✅
+3. Teach checker environments to distinguish checked vs trusted facts. ✅
+4. Add trusted stdlib eliminator facts. ◐ initial value-level `viewFacts` landed for `matchBool`, `matchMaybe`, `matchList`; Haskell trusted catalog removed
+5. Add parametric-mode dependency/effect checking. ◐ local raw-dependency and unchecked-import rejection landed
+6. Annotate/publish derived stdlib Views at the right provenance. ◐ checked `maybeMap`/`maybeBind`/`maybeOr`; trusted value-level facts for recursive list combinators
+
+Avoid introducing implicit trusted catalogs before provenance exists; that would
+create semantics that later need to be unwound.

src/Check.hs

@@ -10,7 +10,7 @@ import Check.Core
 import Check.IO
 import ContentStore (ObjectRef, StorePath, getViewType)
 import Eval (evalTricu)
-import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore)
+import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore, valueViewFactsFromEnv)
 import Research (Env, ViewType)
 
 import qualified Data.Map as Map
@@ -29,7 +29,8 @@ checkFileWithStore store path = do
   let baseEnv = Map.union viewEnv (loadedImports loaded)
       checkerEnv = evalTricu baseEnv (loadedAst loaded)
   imports <- importedViewsFromResolvedModulesEither (loadImportedView store) (loadedModules loaded)
-  checkProgramWithEnvAndImportedViews checkerEnv imports (loadedAst loaded)
+  valueFacts <- either (errorWithoutStackTrace . ("invalid value-level viewFacts: " ++)) pure (valueViewFactsFromEnv checkerEnv)
+  checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) (loadedAst loaded)
 
 viewCheckerEnv :: Env
 viewCheckerEnv = unsafePerformIO (evaluateFile "./lib/view.tri")

src/Check/Core.hs

@@ -12,6 +12,7 @@ module Check.Core
   , lowerViewExpr
   ) where
 
+import Control.Applicative ((<|>))
 import Control.Monad.State.Strict
 import Data.Char (isDigit)
 import Data.Maybe (mapMaybe)
@@ -73,11 +74,6 @@ checkSourceWithEnvAndImportedViews checkerEnv imports source =
   checkProgramWithEnvAndImportedViews checkerEnv imports (parseTricu source)
 
 checkProgramWithEnvAndImportedViews :: Env -> [ImportedView] -> [TricuAST] -> IO String
-checkProgramWithEnvAndImportedViews _ _ asts
-  | not (any isAnnotatedDefinition asts) = pure "ok"
-  where
-    isAnnotatedDefinition SDefAnn {} = True
-    isAnnotatedDefinition _ = False
 checkProgramWithEnvAndImportedViews checkerEnv imports asts = do
   case lowerProgramWithImportedViewsDebugInEnv checkerEnv imports asts of
     Left err -> pure err
@@ -104,6 +100,79 @@ annotateDiagnostic debugNames message =
           "symbol " ++ symText ++ " (" ++ label ++ ") " ++ unwords rest
     _ -> message
 
+viewExprHasParametricBinder :: ViewExpr -> Bool
+viewExprHasParametricBinder expr = case expr of
+  VEVar _ -> True
+  VEVarId _ -> True
+  VEList items -> any viewExprHasParametricBinder items
+  VEApp fn arg -> viewExprHasParametricBinder fn || viewExprHasParametricBinder arg
+  VEForall binders body -> not (null binders) || viewExprHasParametricBinder body
+  VEExists binders body -> not (null binders) || viewExprHasParametricBinder body
+  VEName _ -> False
+  VEInt _ -> False
+  VEString _ -> False
+  VERaw _ -> False
+
+rawTaintedDefinitions :: Set.Set String -> [TricuAST] -> Map.Map String String
+rawTaintedDefinitions allowedExternalFacts asts = fixedPoint initiallyRaw
+  where
+    allowedFacts = allowedExternalFacts
+    definitions = Map.fromList
+      [ (name, (args, body))
+      | ast <- asts
+      , Just (name, args, body) <- [definitionBody ast]
+      ]
+    localNames = Map.keysSet definitions
+    initiallyRaw = Map.mapMaybeWithKey
+      (\name (args, body) ->
+        if name `Set.member` allowedFacts
+          then Nothing
+          else definitionUnsafeBaseReason localNames allowedFacts (Set.fromList args) body)
+      definitions
+
+    fixedPoint tainted =
+      let tainted' = Map.mapMaybeWithKey (transitiveReason tainted) definitions
+          combined = Map.union tainted tainted'
+      in if combined == tainted then tainted else fixedPoint combined
+
+    transitiveReason tainted name (args, body)
+      | name `Map.member` tainted = Nothing
+      | name `Set.member` allowedFacts = Nothing
+      | otherwise = case filter (`Map.member` tainted) (astFreeRefs (foldr Set.delete localNames args) body) of
+          helper : _ -> Just $ "depends on raw-tainted local helper " ++ show helper ++ " (" ++ tainted Map.! helper ++ ")"
+          [] -> Nothing
+
+    definitionBody ast = case ast of
+      SDef name args body -> Just (name, args, body)
+      SDefAnn name args _ body -> Just (name, defArgNames args, body)
+      _ -> Nothing
+
+definitionUnsafeBaseReason :: Set.Set String -> Set.Set String -> Set.Set String -> TricuAST -> Maybe String
+definitionUnsafeBaseReason localNames allowedExternalFacts bound ast = case ast of
+  SVar name _
+    | name `Set.member` bound -> Nothing
+    | name `Set.member` localNames -> Nothing
+    | name `Set.member` allowedExternalFacts -> Nothing
+    | name == "triage" -> Just "uses raw triage directly"
+    | otherwise -> Just $ "depends on unchecked or unknown external name " ++ show name
+  SInt _ -> Nothing
+  SStr _ -> Nothing
+  SList items -> firstJust (map (definitionUnsafeBaseReason localNames allowedExternalFacts bound) items)
+  SDef _ args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
+  SDefAnn _ args _ body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound (defArgNames args)) body
+  SApp fn arg -> definitionUnsafeBaseReason localNames allowedExternalFacts bound fn <|> definitionUnsafeBaseReason localNames allowedExternalFacts bound arg
+  TLeaf -> Just "uses raw t directly"
+  TStem _ -> Just "uses raw t directly"
+  TFork _ _ -> Just "uses raw t directly"
+  SLambda args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
+  SEmpty -> Nothing
+  SImport _ _ -> Nothing
+
+firstJust :: [Maybe a] -> Maybe a
+firstJust [] = Nothing
+firstJust (Just x : _) = Just x
+firstJust (Nothing : xs) = firstJust xs
+
 astFreeRefs :: Set.Set String -> TricuAST -> [String]
 astFreeRefs candidates ast = case ast of
   SVar name _ | name `Set.member` candidates -> [name]
@@ -118,7 +187,6 @@ astFreeRefs candidates ast = case ast of
   TStem inner -> astFreeRefs candidates inner
   TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right
   SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body
-  SLet name val body -> astFreeRefs candidates val ++ astFreeRefs (Set.delete name candidates) body
   SEmpty -> []
   SImport _ _ -> []
 
@@ -159,6 +227,7 @@ data LowerState = LowerState
   , knownNodeViews :: Map.Map Integer ViewExpr
   , nodePayloads :: Map.Map Integer T
   , debugNames :: Map.Map Integer String
+  , rawTaintedDefs :: Map.Map String String
   }
 
 type LowerM a = StateT LowerState (Either String) a
@@ -216,6 +285,12 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
         , Just term <- [Map.lookup name checkerEnvForLowering]
         ]
       annotated = [ def | def@SDefAnn {} <- asts ]
+      allowedExternalFacts = Set.fromList
+        [ importedViewName imported
+        | imported <- imports
+        , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted]
+        ]
+      taintedDefs = rawTaintedDefinitions allowedExternalFacts asts
       initialState = LowerState
         { nextSym = fromIntegral (Map.size tops + Map.size importedSyms)
         , topSyms = tops
@@ -224,6 +299,7 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
         , knownNodeViews = Map.union trustedLocalKnown importKnown
         , nodePayloads = payloads
         , debugNames = Map.union topDebug importDebug
+        , rawTaintedDefs = taintedDefs
         }
   (localNodes, finalState) <- runStateT (lowerAnnotatedProgram annotated) initialState
   trustedLocalNodes <- mapM (lowerImportedView (nodePayloads finalState)) trustedLocalFacts
@@ -252,6 +328,10 @@ lowerAnnotatedProgram defs = do
 lowerDefinitionDeclaration :: TricuAST -> LowerM [String]
 lowerDefinitionDeclaration (SDefAnn name args ret _) = do
   let (_, _, declaredView) = canonicalDefinitionViews args ret
+  tainted <- gets rawTaintedDefs
+  if viewExprHasParametricBinder declaredView && name `Map.member` tainted
+    then liftEither (Left $ "parametric View definition " ++ show name ++ " depends on raw intensional Tree Calculus machinery (" ++ tainted Map.! name ++ "); use a trusted eliminator boundary instead")
+    else do
       sym <- symbolForTop name
       recordKnown sym declaredView
       node <- typedValueNode sym declaredView
@@ -272,7 +352,17 @@ viewAnyType :: ViewExpr
 viewAnyType = VEName "Any"
 
 canonicalDefinitionViews :: [DefArg] -> Maybe ViewExpr -> ([DefArg], Maybe ViewExpr, ViewExpr)
-canonicalDefinitionViews args ret = (args, ret, declaredDefinitionView args ret)
+canonicalDefinitionViews args ret =
+  let rawView = declaredDefinitionView args ret
+      vars = Set.toList (freeViewVars rawView)
+      binderIds = zip vars [0..]
+      binderMap = Map.fromList binderIds
+      mappedArgs = map (mapDefArgView (rewriteViewVars binderMap)) args
+      mappedRet = fmap (rewriteViewVars binderMap) ret
+      mappedView = declaredDefinitionView mappedArgs mappedRet
+      binders = map snd binderIds
+      declaredView = if null vars then mappedView else VEForall binders mappedView
+  in (mappedArgs, mappedRet, declaredView)
 
 declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
 declaredDefinitionView args ret =
@@ -282,6 +372,10 @@ declaredDefinitionView args ret =
   where
     resultType = maybe viewAnyType id ret
 
+mapDefArgView :: (ViewExpr -> ViewExpr) -> DefArg -> DefArg
+mapDefArgView f (DefBinder name mTy) = DefBinder name (fmap f mTy)
+mapDefArgView f (DefPhantom ty) = DefPhantom (f ty)
+
 argType :: DefArg -> ViewExpr
 argType (DefBinder _ Nothing) = viewAnyType
 argType (DefBinder _ (Just ty)) = ty
@@ -490,14 +584,6 @@ lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of
   (SApp (SApp (SVar "err" _) value) rest, Just (VTResult errView _)) ->
     lowerUnshadowedConstructor "err" expr expected $
       lowerResultConstructor expected (viewTypeToExpr errView) value rest
-  (SLet name value body, _) -> do
-    (valueSym, valueNodes, _) <- lowerExprKnown value
-    recordDebugName valueSym name
-    bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
-    let (bodySym, bodyNodes, bodyKnown) = bodyResult
-    pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
-  -- Hand-written immediately-applied lambda (not compiler output; let/where
-  -- now emit SLet). Kept for source that relies on alias semantics.
   (SApp (SLambda [name] body) value, _) -> do
     (valueSym, valueNodes, _) <- lowerExprKnown value
     bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
@@ -572,14 +658,6 @@ lowerExprKnown TLeaf = do
 lowerExprKnown (SList items) = do
   (sym, nodes, view, _) <- lowerListLiteral items
   pure (sym, nodes, Just view)
-lowerExprKnown (SLet name value body) = do
-  (valueSym, valueNodes, _) <- lowerExprKnown value
-  recordDebugName valueSym name
-  bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
-  let (bodySym, bodyNodes, bodyKnown) = bodyResult
-  pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
--- Hand-written immediately-applied lambda (not compiler output; let/where
--- now emit SLet). Kept for source that relies on alias semantics.
 lowerExprKnown (SApp (SLambda [name] body) value) = do
   (valueSym, valueNodes, known) <- lowerExprKnown value
   bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
@@ -802,8 +880,8 @@ lowerViewExpr ty = case ty of
   VEName "Byte" -> Right "viewByte"
   VEName "Unit" -> Right "viewUnit"
   VEName name -> Right name
-  VEVar name -> Left $ "polymorphic View variables are unsupported: " ++ show name
+  VEVar name -> Right $ "viewVar " ++ show name
-  VEVarId varId -> Left $ "polymorphic View variables are unsupported: " ++ show varId
+  VEVarId varId -> Right $ "viewVar " ++ show varId
   VEInt n -> Right (show n)
   VEString s -> Right (show s)
   VEList items -> do
@@ -833,10 +911,45 @@ lowerViewExpr ty = case ty of
     f <- lowerViewExpr func
     a <- lowerViewExpr arg
     Right $ parens f ++ " " ++ parens a
-  VEForall _ _ -> Left "quantified View contracts are unsupported"
+  VEForall binders body -> do
-  VEExists _ _ -> Left "existential View contracts are unsupported"
+    bodyExpr <- lowerViewExpr body
+    Right $ "viewForall " ++ lowerStringList binders ++ " " ++ parens bodyExpr
+  VEExists binders body -> do
+    bodyExpr <- lowerViewExpr body
+    Right $ "viewExists " ++ lowerStringList binders ++ " " ++ parens bodyExpr
   VERaw raw -> Right raw
 
+lowerStringList :: [Integer] -> String
+lowerStringList items = "[" ++ unwords (map (parens . show) items) ++ "]"
+
+quantifyFreeViewVars :: ViewExpr -> ViewExpr
+quantifyFreeViewVars view =
+  let vars = Set.toList (freeViewVars view)
+      binderIds = zip vars [0..]
+      binderMap = Map.fromList binderIds
+      body = rewriteViewVars binderMap view
+      binders = map snd binderIds
+  in if null vars then view else VEForall binders body
+
+rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
+rewriteViewVars binderMap view = case view of
+  VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
+  VEList items -> VEList (map (rewriteViewVars binderMap) items)
+  VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
+  VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
+  VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
+  _ -> view
+
+freeViewVars :: ViewExpr -> Set.Set String
+freeViewVars view = case view of
+  VEVar name -> Set.singleton name
+  VEVarId _ -> Set.empty
+  VEList items -> Set.unions (map freeViewVars items)
+  VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
+  VEForall _ body -> freeViewVars body
+  VEExists _ body -> freeViewVars body
+  _ -> Set.empty
+
 treeSource :: T -> String
 treeSource Leaf = "t"
 treeSource (Stem x) = "(t " ++ treeSource x ++ ")"

src/Check/IO.hs

@@ -105,7 +105,6 @@ instrumentIOContinuations asts = mapM transformTop asts
       SApp (SVar "io" h) action -> SApp (SVar "io" h) <$> transformIOAction action
       SApp f a -> SApp <$> transformExpr f <*> transformExpr a
       SLambda params body -> SLambda params <$> transformExpr body
-      SLet name val body -> SLet name <$> transformExpr val <*> transformExpr body
       TStem x -> TStem <$> transformExpr x
       TFork x y -> TFork <$> transformExpr x <*> transformExpr y
       _ -> pure expr
@@ -119,7 +118,6 @@ instrumentIOContinuations asts = mapM transformTop asts
         SApp <$> (SApp (SVar "bind" h) <$> transformIOAction left) <*> (SLambda params <$> transformIOAction body)
       SApp f a -> SApp <$> transformIOAction f <*> transformIOAction a
       SLambda params body -> SLambda params <$> transformIOAction body
-      SLet name val body -> SLet name <$> transformIOAction val <*> transformIOAction body
       _ -> transformExpr action
 
     checkedPureActionFor value =
@@ -185,7 +183,6 @@ mentionsContractedName contracts expr = case expr of
   SVar name _ -> Map.member name contracts
   SApp f a -> mentionsContractedName contracts f || mentionsContractedName contracts a
   SLambda _ body -> mentionsContractedName contracts body
-  SLet _ val body -> mentionsContractedName contracts val || mentionsContractedName contracts body
   SList items -> any (mentionsContractedName contracts) items
   TStem x -> mentionsContractedName contracts x
   TFork x y -> mentionsContractedName contracts x || mentionsContractedName contracts y
@@ -375,7 +372,6 @@ substAst subst expr = case expr of
   SVar name Nothing -> Map.findWithDefault expr name subst
   SApp f a -> SApp (substAst subst f) (substAst subst a)
   SLambda params body -> SLambda params (substAst (foldr Map.delete subst params) body)
-  SLet name val body -> SLet name (substAst subst val) (substAst (Map.delete name subst) body)
   SList items -> SList (map (substAst subst) items)
   TStem x -> TStem (substAst subst x)
   TFork x y -> TFork (substAst subst x) (substAst subst y)
@@ -401,7 +397,6 @@ astSource expr = case expr of
   SList items -> "[" ++ unwords (map (parens . astSource) items) ++ "]"
   SApp f a -> parens (astSource f) ++ " " ++ parens (astSource a)
   SLambda params body -> parens (unwords params ++ " : " ++ astSource body)
-  SLet name val body -> parens ("let " ++ name ++ " = " ++ astSource val ++ " in " ++ astSource body)
   TLeaf -> "t"
   TStem x -> "(t " ++ astSource x ++ ")"
   TFork x y -> "(t " ++ astSource x ++ " " ++ astSource y ++ ")"

src/Eval.hs

@@ -75,7 +75,6 @@ evalTricu env x = go env (reorderDefs env (map recoverParams x))
 evalASTSync :: Env -> TricuAST -> T
 evalASTSync env term = case term of
   SLambda _ _ -> evalASTSync env (elimLambda term)
-  SLet name val body -> evalASTSync env (SApp (SLambda [name] body) val)
   SVar name Nothing -> case Map.lookup name env of
     Just v -> v
     Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined"
@@ -109,7 +108,6 @@ annotatedBinders (DefPhantom _ : rest) = annotatedBinders rest
 elimLambda :: TricuAST -> TricuAST
 elimLambda = go
   where
-    go (SLet name val body) = go (SApp (SLambda [name] body) val)
     go term
       | etaReduction term   = go (etaReduceResult term)
       | triagePattern term  = _TRI
@@ -192,8 +190,6 @@ freeVars (SVar v Nothing) = Set.singleton v
 freeVars (SVar v (Just _)) = Set.singleton v
 freeVars (SApp t u) = Set.union (freeVars t) (freeVars u)
 freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs)
-freeVars (SLet name val body) =
-  Set.union (freeVars val) (Set.delete name (freeVars body))
 freeVars (SDef _ params body) = Set.difference (freeVars body) (Set.fromList params)
 freeVars (SDefAnn _ args _ body) = Set.difference (freeVars body) (Set.fromList (annotatedBinders args))
 freeVars (TStem t) = freeVars t
@@ -301,7 +297,6 @@ findVarNames ast = case ast of
   SVar name _ -> [name]
   SApp a b -> findVarNames a ++ findVarNames b
   SLambda args body -> findVarNames body \\ args
-  SLet name val body -> findVarNames val ++ (findVarNames body \\ [name])
   SDef name args body -> name : (findVarNames body \\ args)
   SDefAnn name args _ body -> name : (findVarNames body \\ annotatedBinders args)
   _ -> []
@@ -322,7 +317,6 @@ toDB env = \case
   SInt n       -> BInt n
   SList xs     -> BList (map (toDB env) xs)
   SEmpty       -> BEmpty
-  SLet name val body -> toDB env (SApp (SLambda [name] body) val)
   SDef{}       -> error "toDB: unexpected SDef at this stage"
   SDefAnn{}    -> error "toDB: unexpected SDefAnn at this stage"
   SImport _ _  -> BEmpty

src/FileEval.hs

@@ -14,6 +14,7 @@ module FileEval
   , compileFileWithStore
   , loadFileWithStore
   , loadFileWithStoreMode
+  , valueViewFactsFromEnv
   , defaultStorePath
   ) where
 
@@ -35,6 +36,8 @@ import Wire (buildBundle, encodeBundle, decodeBundle, verifyBundle, Bundle(..))
 
 import Data.List       (partition, isPrefixOf)
 import Data.Maybe      (mapMaybe)
+import Control.Monad   (forM)
+import qualified Data.Set as Set
 import System.Directory (getHomeDirectory, getTemporaryDirectory)
 import System.FilePath ((</>))
 import System.Exit (die)
@@ -201,9 +204,12 @@ buildWorkspaceModule ctx store moduleName sourcePath = do
   localViewsResult <- localViews
   resolvedLocalViews <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid exported View Contract annotation: ") ++)) pure localViewsResult
   importedViews <- importedViewsFromResolvedModulesEither (getViewType store) (loadedModules loaded)
+  valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv env)
+  validateValueViewFactExports moduleName names valueFacts
   let localViewFacts = Map.map (\view -> (view, ViewChecked)) resolvedLocalViews
       importedViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- importedViews]
-      exportViewFacts = Map.union localViewFacts importedViewFacts
+      valueViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- valueFacts]
+      exportViewFacts = Map.unions [localViewFacts, valueViewFacts, importedViewFacts]
   exports <- mapM (buildExport env exportViewFacts) names
   manifestHash <- putManifest store (ModuleManifest [] exports)
   writeAlias store ModuleAlias (T.pack moduleName) (ObjectRef (unDomain manifestDomain) manifestHash)
@@ -231,12 +237,62 @@ enforceWorkspaceModuleContracts store moduleName importEnv modules asts
       viewEnv <- evaluateFileWithContextWithStoreAndMode IgnoreContracts (Just store) Map.empty "./lib/view.tri"
       let checkerEnv = evalTricu (Map.union viewEnv importEnv) asts
       imports <- importedViewsFromResolvedModulesEither (getViewType store) modules
-      resultText <- checkProgramWithEnvAndImportedViews checkerEnv imports asts
+      valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv checkerEnv)
+      resultText <- checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) asts
       case resultText of
         "ok" -> pure ()
         diagnostic -> errorWithoutStackTrace $
           "Workspace module " ++ show moduleName ++ " failed View Contract check: " ++ diagnostic
 
+valueViewFactsFromEnv :: Env -> Either String [ImportedView]
+valueViewFactsFromEnv env = case Map.lookup "viewFacts" env of
+  Nothing -> Right []
+  Just factsTree -> do
+    facts <- context "viewFacts is not a list" (toList factsTree)
+    decoded <- forM (zip [0 :: Int ..] facts) (uncurry decodeFactAt)
+    rejectDuplicateFacts decoded
+    pure decoded
+  where
+    decodeFactAt index factTree = do
+      (nameTree, rest) <- context prefix (pairParts factTree)
+      name <- context (prefix ++ ": export name is not a string") (toString nameTree)
+      (provenanceTree, viewTree) <- context (prefixFor name ++ ": payload is not a pair") (pairParts rest)
+      provenance <- context (prefixFor name ++ ": invalid provenance") (decodeProvenance provenanceTree)
+      view <- context (prefixFor name ++ ": malformed View") (treeToViewType viewTree)
+      pure (ImportedView name view provenance)
+      where
+        prefix = "viewFacts[" ++ show index ++ "]"
+        prefixFor name = prefix ++ " for " ++ show name
+
+    pairParts (Fork left right) = Right (left, right)
+    pairParts _ = Left "expected pair"
+
+    decodeProvenance tree = do
+      n <- toNumber tree
+      case n of
+        0 -> Right ViewChecked
+        1 -> Right ViewTrusted
+        2 -> Right ViewUnchecked
+        _ -> Left $ "unknown provenance tag " ++ show n
+
+    rejectDuplicateFacts facts = go Set.empty facts
+      where
+        go _ [] = Right ()
+        go seen (fact : rest)
+          | importedViewName fact `Set.member` seen = Left $ "duplicate viewFacts entry for " ++ show (importedViewName fact)
+          | otherwise = go (Set.insert (importedViewName fact) seen) rest
+
+    context label = either (Left . ((label ++ ": ") ++)) Right
+
+validateValueViewFactExports :: String -> [String] -> [ImportedView] -> IO ()
+validateValueViewFactExports moduleName exportedNames facts = do
+  let exported = Set.fromList exportedNames
+      missing = [importedViewName fact | fact <- facts, importedViewName fact `Set.notMember` exported]
+  case missing of
+    [] -> pure ()
+    name : _ -> errorWithoutStackTrace $
+      "Workspace module " ++ show moduleName ++ " has value-level viewFacts for non-exported name " ++ show name
+
 isAnnotatedDefinition :: TricuAST -> Bool
 isAnnotatedDefinition SDefAnn {} = True
 isAnnotatedDefinition _ = False
@@ -244,10 +300,13 @@ isAnnotatedDefinition _ = False
 topLevelDefinitions :: [TricuAST] -> [String]
 topLevelDefinitions = mapMaybe go
   where
-    go (SDef name _ _) = Just name
+    go (SDef name _ _) | not (isViewFactMetadataName name) = Just name
-    go (SDefAnn name _ _ _) = Just name
+    go (SDefAnn name _ _ _) | not (isViewFactMetadataName name) = Just name
     go _ = Nothing
 
+isViewFactMetadataName :: String -> Bool
+isViewFactMetadataName name = name == "viewFacts"
+
 topLevelDefinitionViews :: [TricuAST] -> Map.Map String ViewExpr
 topLevelDefinitionViews asts = Map.fromList (mapMaybe go asts)
   where
@@ -269,7 +328,7 @@ resolveViewExpression checkerEnv view = do
     Left err -> Left $ "could not validate view expression " ++ show expr ++ ": " ++ err
 
 definitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
-definitionView args resultView =
+definitionView args resultView = quantifyFreeViewVars $
   case argViews of
     [] -> finalView
     _  -> VEApp (VEApp (VEName "Fn") (VEList argViews)) finalView
@@ -277,6 +336,34 @@ definitionView args resultView =
     argViews = map defArgView args
     finalView = maybe exportedViewAny id resultView
 
+quantifyFreeViewVars :: ViewExpr -> ViewExpr
+quantifyFreeViewVars view =
+  let vars = Set.toList (freeViewVars view)
+      binderIds = zip vars [0..]
+      binderMap = Map.fromList binderIds
+      body = rewriteViewVars binderMap view
+      binders = map snd binderIds
+  in if null vars then view else VEForall binders body
+
+rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
+rewriteViewVars binderMap view = case view of
+  VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
+  VEList items -> VEList (map (rewriteViewVars binderMap) items)
+  VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
+  VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
+  VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
+  _ -> view
+
+freeViewVars :: ViewExpr -> Set.Set String
+freeViewVars view = case view of
+  VEVar name -> Set.singleton name
+  VEVarId _ -> Set.empty
+  VEList items -> Set.unions (map freeViewVars items)
+  VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
+  VEForall _ body -> freeViewVars body
+  VEExists _ body -> freeViewVars body
+  _ -> Set.empty
+
 defArgView :: DefArg -> ViewExpr
 defArgView (DefBinder _ Nothing) = exportedViewAny
 defArgView (DefBinder _ (Just ty)) = ty

src/Main.hs

@@ -17,13 +17,11 @@ import FileEval
   )
 import IODriver (IOPermissions(..), runIO)
 import Parser (parseTricu)
-import REPL (repl, replWithStore)
+import REPL (repl)
 import Research (T, EvaluatedForm(..), Env, formatT, exportDag)
 import Wire (encodeBundle, defaultExportNames, Bundle(..))
 
-import Control.Monad (foldM, forM, unless, when)
+import Control.Monad (foldM, unless, when)
-import Data.Char (isAlphaNum)
-import Data.List (sortOn)
 import qualified Data.Text as T
 import Data.Version (showVersion)
 import Paths_tricu (version)
@@ -33,18 +31,13 @@ import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as BL
 import qualified Data.Sequence as Seq
 import qualified Data.Map as Map
-import System.Directory (createDirectoryIfMissing, getHomeDirectory)
+import System.Directory (getHomeDirectory)
 import System.FilePath (takeBaseName, (</>))
 
 -- ---------------------------------------------------------------------------
 -- CLI argument types
 -- ---------------------------------------------------------------------------
 
-data AppArgs = AppArgs
-  { globalStore :: Maybe FilePath
-  , appCommand   :: TricuArgs
-  } deriving (Show)
-
 data TricuArgs
   = Repl
   | Check
@@ -81,8 +74,6 @@ data TricuArgs
       , exportOutput  :: FilePath
       , exportNames   :: [String]
       , exportStore   :: Maybe FilePath
-      , exportAll     :: Bool
-      , exportSplit   :: Bool
       , dag           :: Bool
       }
   | StoreAliasList
@@ -260,14 +251,6 @@ exportParser = ArboricxExport
      <> metavar "PATH"
      <> help "Content-addressed store path"
       ))
-  <*> switch
-      ( long "all"
-     <> help "Export all name aliases that point at tree-term objects"
-      )
-  <*> switch
-      ( long "split"
-     <> help "Write one single-export bundle per export; --output is treated as a directory"
-      )
   <*> switch
       ( long "dag"
      <> help "Export as a topologically-sorted DAG node table instead of a bundle"
@@ -314,15 +297,9 @@ storeAliasGetParser = StoreAliasGet
 versionStr :: String
 versionStr = "tricu " ++ showVersion version
 
-tricuParser :: Parser AppArgs
+tricuParser :: Parser TricuArgs
-tricuParser = AppArgs
+tricuParser = (subparser topCommands <|> pure Repl)
-  <$> optional (option str
+  <**> infoOption versionStr (long "version" <> help "Show version")
-      ( long "store"
-     <> metavar "PATH"
-     <> help "Global content-addressed store path used by commands and the REPL unless a subcommand overrides it"
-      ))
-  <*> ((subparser topCommands <|> pure Repl)
-      <**> infoOption versionStr (long "version" <> help "Show version"))
   where
     topCommands = mconcat
       [ command "check" (info (checkParser <**> helper)
@@ -365,15 +342,13 @@ storeAliasParser = subparser $ mconcat
 
 main :: IO ()
 main = do
-  appArgs <- execParser $ info (tricuParser <**> helper)
+  args <- execParser $ info (tricuParser <**> helper)
     ( fullDesc
    <> progDesc "Exploring Tree Calculus"
    <> header versionStr
     )
-  let mGlobalStore = globalStore appArgs
-      args = applyGlobalStore mGlobalStore (appCommand appArgs)
   case args of
-    Repl               -> runReplWithStore mGlobalStore
+    Repl               -> runRepl
     Check {}           -> runCheck args
     Eval {}            -> runEval args
     ArboricxCompile {} -> runCompile args
@@ -387,31 +362,11 @@ main = do
 -- Command runners
 -- ---------------------------------------------------------------------------
 
-applyGlobalStore :: Maybe FilePath -> TricuArgs -> TricuArgs
-applyGlobalStore mGlobal args = case args of
-  Repl -> Repl
-  Check {} -> args { checkStore = preferLocal (checkStore args) }
-  Eval {} -> args { evalStore = preferLocal (evalStore args) }
-  ArboricxCompile {} -> args { compileStore = preferLocal (compileStore args) }
-  ArboricxImport {} -> args { importStore = preferLocal (importStore args) }
-  ArboricxExport {} -> args { exportStore = preferLocal (exportStore args) }
-  StoreAliasList {} -> args { storePathOpt = preferLocal (storePathOpt args) }
-  StoreAliasGet {} -> args { storePathOpt = preferLocal (storePathOpt args) }
-  where
-    preferLocal local = case local of
-      Just _  -> local
-      Nothing -> mGlobal
-
 runRepl :: IO ()
-runRepl = runReplWithStore Nothing
+runRepl = do
-
-runReplWithStore :: Maybe FilePath -> IO ()
-runReplWithStore mStore = do
   putStrLn "Welcome to the tricu REPL"
   putStrLn "You may exit with `CTRL+D` or the `!exit` command."
-  case mStore of
+  repl
-    Nothing -> repl
-    Just store -> replWithStore (StorePath store)
 
 runCheck :: TricuArgs -> IO ()
 runCheck opts = do
@@ -511,27 +466,17 @@ runExportBundle opts = do
       modules = exportModules opts
       out     = exportOutput opts
       names   = exportNames opts
-      allFlag = exportAll opts
-      splitFlag = exportSplit opts
   when (null out) $ die "tricu arboricx export: --output is required"
-  when (null targets && null modules && not allFlag) $
+  when (null targets && null modules) $
-    die "tricu arboricx export: at least one --target, --module, or --all is required"
+    die "tricu arboricx export: at least one --target or --module is required"
-  when (splitFlag && not (null names)) $
-    die "tricu arboricx export --split: --name is not supported; split bundles use their export names"
   store <- resolveStorePath (exportStore opts)
-  allEntries <- if allFlag then resolveAllNameExports store else pure []
   targetRoots <- mapM (resolveStoreTarget store) targets
   moduleRoots <- concat <$> mapM (resolveModuleExports store) modules
   let targetEntries = zip (defaultExportNames (length targetRoots)) targetRoots
-      entries = allEntries ++ targetEntries ++ moduleRoots
+      entries = targetEntries ++ moduleRoots
       expNames = if null names then map fst entries else map T.pack names
-  when (null entries) $
-    die "tricu arboricx export: no tree-term exports found"
   when (length expNames /= length entries) $
     die "tricu arboricx export: number of --name values must match number of exported roots"
-  if splitFlag
-    then runExportBundleSplit store out (zip expNames (map snd entries))
-    else do
   bundle <- packBundleFromStore store (zip expNames (map snd entries))
   let bundleData = encodeBundle bundle
   BL.writeFile out (BL.fromStrict bundleData)
@@ -539,19 +484,6 @@ runExportBundle opts = do
   putStrLn $ "  nodes: " ++ show (Seq.length (bundleNodes bundle))
   putStrLn $ "  size: " ++ show (BS.length bundleData) ++ " bytes"
 
-runExportBundleSplit :: StorePath -> FilePath -> [(T.Text, ObjectHash)] -> IO ()
-runExportBundleSplit store outDir entries = do
-  createDirectoryIfMissing True outDir
-  written <- forM (zip [0 :: Int ..] entries) $ \(i, (name, root)) -> do
-    bundle <- packBundleFromStore store [(name, root)]
-    let bundleData = encodeBundle bundle
-        path = outDir </> splitBundleFileName i name
-    BL.writeFile path (BL.fromStrict bundleData)
-    pure (path, Seq.length (bundleNodes bundle), BS.length bundleData)
-  putStrLn $ "Exported " ++ show (length written) ++ " split bundle(s) to " ++ outDir
-  mapM_ (\(path, nodeCount, byteCount) ->
-    putStrLn $ "  " ++ path ++ " (nodes: " ++ show nodeCount ++ ", size: " ++ show byteCount ++ " bytes)") written
-
 runStoreAliasList :: TricuArgs -> IO ()
 runStoreAliasList opts = do
   store <- resolveStorePath (storePathOpt opts)
@@ -611,19 +543,6 @@ resolveStoreTarget store target = do
     Just _ -> return root
     Nothing -> die $ "Term not found in store: " ++ target
 
-resolveAllNameExports :: StorePath -> IO [(T.Text, ObjectHash)]
-resolveAllNameExports store = do
-  aliases <- sortOn fst <$> listAliases store NameAlias
-  fmap concat $ mapM exportAlias aliases
-  where
-    exportAlias (name, ref)
-      | objectRefKind ref /= unDomain treeTermDomain = pure []
-      | otherwise = do
-          mTree <- getTreeTerm store (objectRefHash ref)
-          case mTree of
-            Nothing -> die $ "Name alias tree term not found: " ++ T.unpack name
-            Just _  -> pure [(name, objectRefHash ref)]
-
 resolveModuleExports :: StorePath -> String -> IO [(T.Text, ObjectHash)]
 resolveModuleExports store moduleTarget = do
   manifestHash <- resolveModuleManifestHash store moduleTarget
@@ -655,17 +574,6 @@ resolveModuleManifestHash store moduleTarget = do
 formatObjectRef :: ObjectRef -> String
 formatObjectRef ref = T.unpack (objectRefKind ref) ++ " " ++ T.unpack (objectRefHash ref)
 
-splitBundleFileName :: Int -> T.Text -> FilePath
-splitBundleFileName i name = show i ++ "-" ++ sanitize (T.unpack name) ++ ".arboricx"
-  where
-    sanitize [] = "export"
-    sanitize xs = case map safeChar xs of
-      [] -> "export"
-      ys -> ys
-    safeChar c
-      | isAlphaNum c || c == '-' || c == '_' || c == '.' = c
-      | otherwise = '_'
-
 writeOutput :: FilePath -> String -> IO ()
 writeOutput path content
   | null path = putStr content

src/Parser.hs

@@ -496,7 +496,7 @@ whereChainP parseBody = do
     Nothing -> pure body
     Just (name, args, value) ->
       let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-      in pure (SLet name boundValue body)
+      in pure (SApp (SLambda [name] body) boundValue)
 
 whereBindingP :: TokParser (String, [String], TricuAST)
 whereBindingP = do
@@ -524,7 +524,7 @@ letP = do
   bodyIndent <- skipNestedNewlinesGetIndent
   body <- exprAtIndentP bodyIndent
   let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-  pure (SLet name boundValue body)
+  pure (SApp (SLambda [name] body) boundValue)
 
 data DoStmt
   = DoBind String TricuAST

src/REPL.hs

@@ -10,17 +10,7 @@ import FileEval
   )
 import Parser (parseTricu)
 import Research (EvaluatedForm(..), Env, formatT)
-import ContentStore
+import ContentStore (StorePath(..))
-  ( AliasKind(..)
-  , ObjectRef(..)
-  , StorePath(..)
-  , cachedFilesystemResolver
-  , getTreeTerm
-  , readAlias
-  , treeTermDomain
-  , unDomain
-  )
-import Module.Resolver (resolveModuleImport, resolvedModulesEnv)
 
 import Control.Exception (SomeException, catch, displayException)
 import Control.Monad.IO.Class (liftIO)
@@ -32,7 +22,6 @@ import System.Console.Haskeline
 import System.Directory (doesFileExist)
 
 import qualified Data.Map as Map
-import qualified Data.Text as T
 
 -- | Source-local REPL with the same filesystem CAS/module loader used by the
 -- CLI. View Contract checking is explicit (`!check`); evaluation can run in
@@ -46,10 +35,8 @@ data REPLState = REPLState
   }
 
 repl :: IO ()
-repl = defaultStorePath >>= replWithStore
+repl = do
-
+  store <- defaultStorePath
-replWithStore :: StorePath -> IO ()
-replWithStore store = do
   envRef <- newIORef Map.empty
   let settings = Settings
         { complete = completeRepl envRef
@@ -79,8 +66,6 @@ replWithStore store = do
             "!env" -> handleEnv state >> loop state
             _ | "!load" `isPrefixOf` s -> handleLoad state (strip $ drop 5 s)
               | "!check" `isPrefixOf` s -> handleCheck state (strip $ drop 6 s)
-              | "!use" `isPrefixOf` s -> handleUse state (strip $ drop 4 s)
-              | "!name" `isPrefixOf` s -> handleName state (strip $ drop 5 s)
               | "!store" `isPrefixOf` s -> handleStore state (strip $ drop 6 s)
               | "!format" `isPrefixOf` s -> handleFormat state (strip $ drop 7 s)
               | "!unchecked" `isPrefixOf` s -> handleUnchecked state (strip $ drop 10 s)
@@ -100,8 +85,6 @@ replWithStore store = do
       outputStrLn "  !output                - Change output format interactively"
       outputStrLn "  !format FORM           - Set output format: tree, fsl, ast, ternary, ascii, decode, number, string"
       outputStrLn "  !load FILE             - Load and evaluate a .tri file into the environment"
-      outputStrLn "  !use MODULE [NS]       - Load a module alias/manifest from the store (NS defaults to !Local)"
-      outputStrLn "  !name NAME [LOCAL]     - Load a name alias/tree-term hash from the store"
       outputStrLn "  !check FILE            - Check View Contract annotations in a .tri file"
       outputStrLn "  !store [PATH]          - Show or set the content-addressed store path"
       outputStrLn "  !unchecked [on|off]    - Show or set unchecked eval mode"
@@ -153,49 +136,6 @@ replWithStore store = do
               outputStrLn output
               loop state
 
-    handleUse :: REPLState -> String -> InputT IO ()
-    handleUse state arg = case words arg of
-      [] -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
-      [moduleTarget] -> loadModule moduleTarget "!Local"
-      [moduleTarget, namespace] -> loadModule moduleTarget namespace
-      _ -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
-      where
-        loadModule moduleTarget namespace = do
-          resolver <- liftIO $ cachedFilesystemResolver (replStore state)
-          resolved <- liftIO $ resolveModuleImport resolver moduleTarget namespace
-          let importedEnv = resolvedModulesEnv [resolved]
-              env' = Map.union importedEnv (replEnv state)
-          liftIO $ writeIORef (replEnvRef state) env'
-          outputStrLn $ "Loaded " ++ show (Map.size importedEnv) ++ " export(s) from store module " ++ moduleTarget
-          loop state { replEnv = env' }
-
-    handleName :: REPLState -> String -> InputT IO ()
-    handleName state arg = case words arg of
-      [] -> outputStrLn "Usage: !name NAME [LOCAL]" >> loop state
-      [name] -> loadName name name
-      [name, localName] -> loadName name localName
-      _ -> outputStrLn "Usage: !name NAME [LOCAL]" >> loop state
-      where
-        loadName name localName = do
-          let store = replStore state
-              nameText = T.pack name
-          mAlias <- liftIO $ readAlias store NameAlias nameText
-          let root = maybe nameText objectRefHash mAlias
-              badKind = case mAlias of
-                Just ref -> objectRefKind ref /= unDomain treeTermDomain
-                Nothing -> False
-          if badKind
-            then outputStrLn ("Name alias does not point at a tree term: " ++ name) >> loop state
-            else do
-              mTerm <- liftIO $ getTreeTerm store root
-              case mTerm of
-                Nothing -> outputStrLn ("Tree term not found in store: " ++ name) >> loop state
-                Just term -> do
-                  let env' = Map.insert localName term (replEnv state)
-                  liftIO $ writeIORef (replEnvRef state) env'
-                  outputStrLn $ "Loaded " ++ name ++ " as " ++ localName
-                  loop state { replEnv = env' }
-
     handleStore :: REPLState -> String -> InputT IO ()
     handleStore state path
       | null path = do
@@ -261,8 +201,6 @@ completeRepl envRef input@(left, _right)
       , "!reset"
       , "!help"
       , "!load"
-      , "!use"
-      , "!name"
       , "!check"
       , "!store"
       , "!unchecked"

src/Research.hs

@@ -84,11 +84,6 @@ data TricuAST
   | TStem TricuAST
   | TFork TricuAST TricuAST
   | SLambda [String] TricuAST
-  -- Non-recursive local binding: `name = boundValue` scoped over `body`.
-  -- Produced by let/where desugaring. `boundValue` already folds any binding
-  -- arguments into nested SLambda. Semantically equal to
-  --   SApp (SLambda [name] body) boundValue
-  | SLet String TricuAST TricuAST
   | SEmpty
   | SImport String String
   deriving (Show, Eq, Ord)

test/Spec.hs

@@ -77,13 +77,13 @@ allTestLibsEnv = unsafePerformIO $ do
 tests :: TestTree
 tests = testGroup "Tricu Tests"
   [ lexer
-  , parser
+  --, parser
-  , simpleEvaluation
+  --, simpleEvaluation
-  , lambdas
+  --, lambdas
-  , providedLibraries
+  --, providedLibraries
-  , maybeTests
+  --, maybeTests
-  , fileEval
+  --, fileEval
-  , demos
+  --, demos
   --, decoding
   --, elimLambdaSingle
   --, stressElimLambda
@@ -94,7 +94,7 @@ tests = testGroup "Tricu Tests"
   --, binaryParserTests
   --, httpParsingTests
   --, contentStoreTests
-  --, viewContractTests
+  , viewContractTests
   --, ioDriverTests
   ]
 
@@ -336,7 +336,7 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let expression" $ do
       let input  = "let x = t t in x"
-          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
+          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
       parseSingle input @?= expect
 
   , testCase "Evaluate let expression" $ do
@@ -344,36 +344,18 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let function binding" $ do
       let input  = "let f x = x in f t"
-          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
+          expect = SApp (SLambda ["f"] (SApp (SVar "f" Nothing) TLeaf))
-                        (SApp (SVar "f" Nothing) TLeaf)
+                        (SLambda ["x"] (SVar "x" Nothing))
       parseSingle input @?= expect
 
   , testCase "Parse where expression" $ do
       let input  = "x where x = t t"
-          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
+          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
       parseSingle input @?= expect
 
   , testCase "Evaluate where expression" $ do
       tricuTestString "x where x = 1" @?= "Fork (Stem Leaf) Leaf"
 
-  , testCase "Parse where binding with arguments (SLet)" $ do
-      let input  = "f 3 where f x = x"
-          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
-                        (SApp (SVar "f" Nothing) (SInt 3))
-      parseSingle input @?= expect
-
-  , testCase "Evaluate where binding with arguments matches applied lambda" $ do
-      tricuTestString "f (t t) where f x = t x x"
-        @?= tricuTestString "(f : f (t t)) (x : t x x)"
-
-  , testCase "Evaluate nested let bindings" $ do
-      tricuTestString "let a = t t in let b = t in t a b"
-        @?= tricuTestString "t (t t) t"
-
-  , testCase "Inner let binding shadows outer binding" $ do
-      tricuTestString "let x = t in let x = t t in x"
-        @?= tricuTestString "t t"
-
   , testCase "Parse indented multiline definition body" $ do
       let input  = "x =\n  t\n    t"
           expect = SDef "x" [] (SApp TLeaf TLeaf)
@@ -3234,6 +3216,30 @@ viewContractTests = testGroup "View Contract Tests"
                     view <- getViewType store viewRef
                     view @?= Right (VTFn [VTRef 10] (VTRef 10))
 
+  , testCase "Workspace modules publish explicitly quantified polymorphic views" $
+      withSystemTempDirectory "tricu-workspace-polymorphic-view" $ \dir -> do
+        let store = StorePath (dir </> "store")
+            utilPath = dir </> "util.tri"
+            mainPath = dir </> "main.tri"
+        writeFile (dir </> "tricu.workspace") "module util = util.tri\n"
+        writeFile utilPath "idP x@_a =@_a x\n"
+        writeFile mainPath "!import \"util\" Util\n\nmain =@String Util.idP \"hi\"\n"
+        _ <- evaluateFileWithStore (Just store) mainPath
+        mAlias <- readAlias store ModuleAlias "util"
+        case mAlias of
+          Nothing -> assertFailure "expected util module alias"
+          Just ref -> do
+            mManifest <- getManifest store (objectRefHash ref)
+            case mManifest of
+              Nothing -> assertFailure "expected util module manifest"
+              Just manifest -> case find ((== "idP") . unpack . moduleExportName) (moduleManifestExports manifest) of
+                Nothing -> assertFailure "expected idP export"
+                Just ex -> case moduleExportView ex of
+                  Nothing -> assertFailure "expected idP view ref"
+                  Just viewRef -> do
+                    view <- getViewType store viewRef
+                    view @?= Right (VTForall [0] (VTFn [VTVar 0] (VTVar 0)))
+
   , testCase "Workspace modules publish string custom view aliases" $
       withSystemTempDirectory "tricu-workspace-string-view-alias" $ \dir -> do
         let store = StorePath (dir </> "store")
@@ -3315,10 +3321,232 @@ viewContractTests = testGroup "View Contract Tests"
             ]
         readAlias store ModuleAlias "util" >>= (@?= Nothing)
 
-  , testCase "tricu check rejects polymorphic View variables" $ do
+  , testCase "tricu check lowers free View variables under explicit Forall" $ do
       case lowerSource "idP x@_a =@_a x\n" of
-        Left err -> assertBool "expected unsupported polymorphism diagnostic" $ "polymorphic View variables are unsupported" `isInfixOf` err
+        Left err -> assertFailure err
-        Right _ -> assertFailure "expected polymorphic View rejection"
+        Right lowered -> do
+          assertBool "expected polymorphic declaration to be explicitly quantified" $ "viewForall [(0)]" `isInfixOf` lowered
+          assertBool "expected quantified identity function body" $ "viewFn [(viewVar 0)] (viewVar 0)" `isInfixOf` lowered
+
+  , testCase "tricu check supports first-order polymorphic identity View variables" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nmain =@String idP \"hi\"\n"
+      output @?= "ok"
+
+  , testCase "tricu check propagates first-order polymorphic result relationships" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "constP x@_a y@_b =@_a x\nmain =@String constP \"hi\" 1\n"
+      output @?= "ok"
+
+  , testCase "tricu check instantiates quantified Views at higher-order boundaries" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\ncomposeP f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\nmain =@String composeP idP idP \"hi\"\n"
+      output @?= "ok"
+
+  , testCase "tricu check matches quantified values against concrete Fn requirements" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nacceptSS f@(Fn [String] String) =@String f \"hi\"\nmain =@String acceptSS idP\n"
+      output @?= "ok"
+
+  , testCase "tricu check propagates nested polymorphic List relationships" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "idList xs@(List _a) =@(List _a) xs\nmain =@(List String) idList [(\"hi\")]\n"
+      output @?= "ok"
+
+  , testCase "tricu check keeps polymorphic instantiation acyclic for reciprocal higher-order constraints" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nrel f@(Fn [_a] _b) g@(Fn [_b] _a) =@String \"ok\"\nmain =@String rel idP idP\n"
+      output @?= "ok"
+
+  , testCase "tricu check supports first-principles parametric stdlib island shapes" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "idV x@_a =@_a x\nconstV x@_a y@_b =@_a x\ncomposeV f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\nmain =@String composeV idV (constV \"hi\") 1\n"
+      output @?= "ok"
+
+  , testCase "tricu check rejects raw triage in parametric annotated definitions" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "bad x@_a =@String triage \"leaf\" (_ : \"stem\") (_ _ : \"fork\") x\n"
+      output `containsAll` ["parametric View definition \"bad\"", "uses raw triage directly", "trusted eliminator boundary"]
+
+  , testCase "tricu check rejects raw t in parametric annotated definitions" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "bad x@_a =@_a t\n"
+      output `containsAll` ["parametric View definition \"bad\"", "uses raw t directly", "trusted eliminator boundary"]
+
+  , testCase "tricu check rejects parametric definitions depending on local raw helpers" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "raw x = triage \"leaf\" (_ : \"stem\") (_ _ : \"fork\") x\nbad x@_a =@String raw x\n"
+      output `containsAll` ["parametric View definition \"bad\"", "raw-tainted local helper \"raw\"", "uses raw triage directly"]
+
+  , testCase "tricu check rejects parametric definitions depending on unchecked imported facts" $ do
+      let imported = [ImportedView "Ext.raw" (VTFn [VTVar 0] (VTName "String")) ViewUnchecked]
+      output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "bad x@_a =@String Ext.raw x\n"
+      output `containsAll` ["parametric View definition \"bad\"", "unchecked or unknown external name \"Ext.raw\""]
+
+  , testCase "tricu check accepts parametric code through value-level trusted stdlib facts" $ do
+      facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
+      let source = "idP x@_a =@_a x\nmaybeOrV default@_a m@(Maybe _a) =@_a matchMaybe default idP m\n"
+      output <- checkSourceWithEnvAndImportedViews allTestLibsEnv facts source
+      output @?= "ok"
+
+  , testCase "unused value-level trusted facts do not perturb root selection" $ do
+      facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
+      output <- checkSourceWithEnvAndImportedViews allTestLibsEnv facts "idP x@_a =@_a x\n"
+      output @?= "ok"
+
+  , testCase "value-level trusted stdlib facts lower with Trusted provenance" $ do
+      facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
+      case lowerSourceWithImportedViews facts "notV x@Bool =@Bool matchBool false true x\n" of
+        Left err -> assertFailure err
+        Right lowered -> assertBool "expected trusted provenance in lowered view tree" $ "typedValueWithProvenance" `isInfixOf` lowered && "viewProvenanceTrusted" `isInfixOf` lowered
+
+  , testCase "tricu check uses annotated id const compose through re-export modules" $
+      withSystemTempDirectory "tricu-stdlib-prelude-views" $ \dir -> do
+        let store = StorePath (dir </> "store")
+            basePath = dir </> "mybase.tri"
+            preludePath = dir </> "myprelude.tri"
+            mainPath = dir </> "main.tri"
+        writeFile (dir </> "tricu.workspace") "module mybase = mybase.tri\nmodule myprelude = myprelude.tri\n"
+        writeFile basePath "id a@_a =@_a a\nconst a@_a b@_b =@_a a\ncompose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\n"
+        writeFile preludePath "!import \"mybase\" !Local\n"
+        writeFile mainPath "!import \"myprelude\" !Local\nmain =@String compose id (const \"hi\") 1\n"
+        output <- checkFileWithStore store mainPath
+        output @?= "ok"
+
+  , testCase "Workspace value-level viewFacts export and re-export Trusted provenance" $
+      withSystemTempDirectory "tricu-workspace-value-view-facts" $ \dir -> do
+        let store = StorePath (dir </> "store")
+            depPath = dir </> "dep.tri"
+            shimPath = dir </> "shim.tri"
+            mainPath = dir </> "main.tri"
+            factBlock = unlines
+              [ "factsPair = t"
+              , "factsFact name provenance view = factsPair name (factsPair provenance view)"
+              , "factsTrusted = 1"
+              , "factsField tag value = factsPair tag value"
+              , "factsRecord tag fields = factsPair tag fields"
+              , "factsVar id = factsRecord 8 [(factsField 10 id)]"
+              , "factsForall binders body = factsRecord 9 [(factsField 11 binders) (factsField 12 body)]"
+              , "factsFn args result = factsRecord 1 [(factsField 0 args) (factsField 1 result)]"
+              , "viewFacts = [(factsFact \"rawId\" factsTrusted (factsForall [0] (factsFn [(factsVar 0)] (factsVar 0))))]"
+              ]
+            expected = VTForall [0] (VTFn [VTVar 0] (VTVar 0))
+        writeFile (dir </> "tricu.workspace") "module dep = dep.tri\nmodule shim = shim.tri\n"
+        writeFile depPath ("rawId x = x\n" ++ factBlock)
+        writeFile shimPath "!import \"dep\" !Local\n"
+        writeFile mainPath "!import \"shim\" Shim\nmain x@_a =@_a Shim.rawId x\n"
+        output <- checkFileWithStore store mainPath
+        output @?= "ok"
+        forM_ [("dep", "rawId"), ("shim", "rawId")] $ \(moduleName, exportName) -> do
+          mAlias <- readAlias store ModuleAlias (pack moduleName)
+          case mAlias of
+            Nothing -> assertFailure ("expected " ++ moduleName ++ " module alias")
+            Just ref -> do
+              mManifest <- getManifest store (objectRefHash ref)
+              case mManifest of
+                Nothing -> assertFailure ("expected " ++ moduleName ++ " module manifest")
+                Just manifest -> do
+                  assertBool ("viewFacts should not be exported from " ++ moduleName) $
+                    all ((/= "viewFacts") . unpack . moduleExportName) (moduleManifestExports manifest)
+                  case find ((== exportName) . unpack . moduleExportName) (moduleManifestExports manifest) of
+                    Nothing -> assertFailure ("expected " ++ exportName ++ " export from " ++ moduleName)
+                    Just ex -> do
+                      moduleExportViewProvenance ex @?= Just ViewTrusted
+                      case moduleExportView ex of
+                        Nothing -> assertFailure "expected trusted value-level view ref"
+                        Just viewRef -> do
+                          view <- getViewType store viewRef
+                          view @?= Right expected
+
+  , testCase "value-level viewFacts decoder reports malformed fact context" $ do
+      let env = evalTricu Map.empty (parseTricu "viewFacts = [(t \"bad\" (t 9 t))]\n")
+      case valueViewFactsFromEnv env of
+        Right _ -> assertFailure "expected malformed provenance error"
+        Left err -> err `containsAll` ["viewFacts[0]", "bad", "invalid provenance", "unknown provenance tag 9"]
+
+  , testCase "value-level viewFacts decoder reports malformed View context" $ do
+      let env = evalTricu Map.empty (parseTricu "viewFacts = [(t \"bad\" (t 1 (t 9 [])))]\n")
+      case valueViewFactsFromEnv env of
+        Right _ -> assertFailure "expected malformed View error"
+        Left err -> err `containsAll` ["viewFacts[0]", "bad", "malformed View"]
+
+  , testCase "value-level viewFacts decoder rejects duplicate fact names" $ do
+      let env = evalTricu Map.empty (parseTricu "v = t 9 [(t 11 []) (t 12 (t 0 []))]\nviewFacts = [(t \"dup\" (t 1 v)) (t \"dup\" (t 1 v))]\n")
+      case valueViewFactsFromEnv env of
+        Right _ -> assertFailure "expected duplicate viewFacts error"
+        Left err -> err `containsAll` ["duplicate viewFacts entry", "dup"]
+
+  , testCase "Workspace modules reject viewFacts for non-exported names" $
+      withSystemTempDirectory "tricu-workspace-view-facts-nonexport" $ \dir -> do
+        let store = StorePath (dir </> "store")
+            depPath = dir </> "dep.tri"
+            mainPath = dir </> "main.tri"
+        writeFile (dir </> "tricu.workspace") "module dep = dep.tri\n"
+        writeFile depPath "rawId x = x\nv = t 9 [(t 11 []) (t 12 (t 0 []))]\nviewFacts = [(t \"missing\" (t 1 v))]\n"
+        writeFile mainPath "!import \"dep\" Dep\nmain = Dep.rawId t\n"
+        outcome <- try (evaluateFileWithStore (Just store) mainPath) :: IO (Either SomeException Env)
+        case outcome of
+          Right _ -> assertFailure "expected non-exported viewFacts rejection"
+          Left err -> show err `containsAll` ["viewFacts for non-exported name", "missing"]
+
+  , testCase "stdlib list value-level facts publish Trusted contracts" $
+      withSystemTempDirectory "tricu-stdlib-list-view-facts" $ \dir -> do
+        let store = StorePath (dir </> "store")
+            basePath = dir </> "base.tri"
+            listPath = dir </> "list.tri"
+            mainPath = dir </> "main.tri"
+        baseSource <- readFile "./lib/base.tri"
+        listSource <- readFile "./lib/list.tri"
+        writeFile (dir </> "tricu.workspace") "module base = base.tri\nmodule list = list.tri\n"
+        writeFile basePath baseSource
+        writeFile listPath listSource
+        writeFile mainPath "!import \"list\" L\ninc x@Byte =@Byte x\nmain xs@(List Byte) =@(List Byte) L.map inc xs\n"
+        output <- checkFileWithStore store mainPath
+        output @?= "ok"
+        mAlias <- readAlias store ModuleAlias (pack "list")
+        case mAlias of
+          Nothing -> assertFailure "expected list module alias"
+          Just ref -> do
+            mManifest <- getManifest store (objectRefHash ref)
+            case mManifest of
+              Nothing -> assertFailure "expected list module manifest"
+              Just manifest -> do
+                let trustedNames =
+                      [ "emptyList?", "tail", "append", "lExist?", "map", "filter"
+                      , "foldl", "foldr", "length", "reverse", "snoc", "count"
+                      , "all?", "any?", "intersect", "headMaybe", "lastMaybe"
+                      , "nthMaybe", "take", "drop", "splitAt", "concatMap", "find"
+                      , "partition", "strLength", "strAppend", "strEq?", "strEmpty?"
+                      , "startsWith?", "endsWith?", "contains?", "lines", "unlines"
+                      , "words", "unwords", "zipWith"
+                      ]
+                forM_ trustedNames $ \exportName ->
+                  case find ((== exportName) . unpack . moduleExportName) (moduleManifestExports manifest) of
+                    Nothing -> assertFailure ("expected " ++ exportName ++ " export")
+                    Just ex -> moduleExportViewProvenance ex @?= Just ViewTrusted
+
+  , testCase "Workspace re-export-only modules preserve imported View Contracts" $
+      withSystemTempDirectory "tricu-workspace-reexport-views" $ \dir -> do
+        let store = StorePath (dir </> "store")
+            depPath = dir </> "dep.tri"
+            shimPath = dir </> "shim.tri"
+            mainPath = dir </> "main.tri"
+        writeFile (dir </> "tricu.workspace") "module dep = dep.tri\nmodule shim = shim.tri\n"
+        writeFile depPath "idP x@_a =@_a x\n"
+        writeFile shimPath "!import \"dep\" !Local\n"
+        writeFile mainPath "!import \"shim\" Shim\nmain =@String Shim.idP \"hi\"\n"
+        output <- checkFileWithStore store mainPath
+        output @?= "ok"
+        mAlias <- readAlias store ModuleAlias "shim"
+        case mAlias of
+          Nothing -> assertFailure "expected shim module alias"
+          Just ref -> do
+            mManifest <- getManifest store (objectRefHash ref)
+            case mManifest of
+              Nothing -> assertFailure "expected shim module manifest"
+              Just manifest -> case find ((== "idP") . unpack . moduleExportName) (moduleManifestExports manifest) of
+                Nothing -> assertFailure "expected idP re-export"
+                Just ex -> do
+                  moduleExportViewProvenance ex @?= Just ViewChecked
+                  case moduleExportView ex of
+                    Nothing -> assertFailure "expected idP re-export view ref"
+                    Just viewRef -> do
+                      view <- getViewType store viewRef
+                      view @?= Right (VTForall [0] (VTFn [VTVar 0] (VTVar 0)))
+
+  , testCase "tricu check rejects inconsistent first-order polymorphic View bindings" $ do
+      output <- checkSourceWithEnv allTestLibsEnv "same x@_a y@_a =@_a x\nmain =@String same \"hi\" 1\n"
+      output @?= "symbol 6 (byte literal) expected String but got Byte"
 
   , testCase "tricu check catches undersaturated annotated function calls via residual Fn view" $ do
       output <- checkSourceWithEnv allTestLibsEnv "f x@String y@String =@String x\nmain =@String f \"a\"\n"