Thomasgorissen/assume parameters

.claude/skills/writing-l4-rules/SKILL.md

@@ -233,6 +233,20 @@ The description is the single highest-value sentence in the whole file: it is wh
 @export Calculate the annual income tax owed by an individual resident taxpayer
 ```
 
+### ASSUMEs as export parameters
+
+Module-level `ASSUME`s that an `@export` function references are promoted to
+parameters of that function and must be supplied by the caller — they behave
+just like `GIVEN` parameters at the API boundary. ASSUMEs not referenced by
+any exported function remain internal assumptions.
+
+**Function-typed inputs are not allowed for `@export`.** Neither a `GIVEN`
+parameter nor a referenced `ASSUME` may have a `FUNCTION FROM … TO …` type
+on an exported function: GIVENs can't be passed over JSON, and function-typed
+ASSUMEs stay uninterpreted at runtime (any call fails with a stuck
+"assumed term" error). The typechecker and `jl4-service` deploy both reject
+such bundles with `Function type inputs are not supported for @export`.
+
 ### `@desc` — document parameters
 
 Put an inline `@desc` on **every** `GIVEN` parameter an API caller has to supply. These descriptions flow into the OpenAPI parameter docs and the MCP tool's `inputSchema`, and they are what LLMs read when deciding **how to construct a valid call**.

doc/reference/types/ASSUME.md

@@ -60,6 +60,40 @@ DECIDE isEligible IS
 - When evaluated directly, assumed values remain symbolic
 - Assumed values are typically bound via `#CHECK ... WITH` or `#TRACE ... WITH`
 
+## ASSUME and `@export`
+
+When a module-level ASSUME is referenced by an `@export`-decorated DECIDE, it
+is promoted to a parameter of the exported function and must be supplied by
+the caller at request time (alongside the function's `GIVEN` parameters).
+ASSUMEs not referenced by any exported function remain module-level
+assumptions and are unaffected.
+
+```l4
+ASSUME age IS A NUMBER         -- promoted to a parameter of `isAdult`
+ASSUME unused IS A BOOLEAN     -- stays assumed (no @export uses it)
+
+@export Check if the subject is an adult
+DECIDE isAdult IS age >= 18
+```
+
+### Function-typed inputs are not supported for `@export`
+
+An `@export` function cannot accept a function-typed input, whether declared
+as a `GIVEN` parameter or as a referenced ASSUME:
+
+```l4
+-- ✘ Rejected at typecheck / deploy time
+ASSUME predicate IS A FUNCTION FROM NUMBER TO BOOLEAN
+@export Apply the predicate
+DECIDE `applies` IF predicate OF 42
+```
+
+Functions can't be passed over JSON (REST/MCP), and function-typed ASSUMEs
+stay uninterpreted at runtime — so any call would fail with an "assumed
+term" error rather than return a value. The typechecker emits
+`Function type inputs are not supported for @export` and the service
+refuses to deploy such bundles.
+
 ## Binding Assumed Values
 
 ```l4

jl4-core/jl4-core.cabal

@@ -161,6 +161,7 @@ test-suite jl4-core-test
     TemporalContextSpec
     MixfixParserSpec
     UUID5Spec
+    ExportValidationSpec
   build-tool-depends:
     hspec-discover:hspec-discover
   build-depends:

jl4-core/src/L4/Export.hs

@@ -12,8 +12,11 @@ module L4.Export (
   buildTypeDescMap,
   assumesFromModule,
   extractAssumeParamTypes,
+  extractAssumeParamResolveds,
   extractImplicitAssumeParams,
   hasTypeInferenceVars,
+  validateExportInputs,
+  isExportedDecide,
 ) where
 
 import Base
@@ -30,7 +33,7 @@ import qualified Data.Set as Set
 import L4.Annotation (getAnno)
 import L4.Syntax
 import L4.TypeCheck.Environment (maybeUnique)
-import L4.TypeCheck.Types (CheckErrorWithContext(..), CheckError(..), CheckEntity(..), EntityInfo)
+import L4.TypeCheck.Types (CheckErrorWithContext(..), CheckError(..), CheckEntity(..), CheckErrorContext(..), EntityInfo)
 import Optics
 
 type TypeDescMap = Map.Map Unique Text
@@ -259,30 +262,39 @@ collectTypeSynonyms (MkModule _ _ section) =
     Section _ sub -> goSection sub
     _ -> []
 
--- | Check if a type is a function type, expanding type synonyms.
--- This handles types like `DECLARE Pred IS A FUNCTION FROM NUMBER TO BOOLEAN`
--- followed by `ASSUME p IS A Pred`.
+-- | Check if a type /contains/ a function type anywhere — expanding type
+-- synonyms and recursing into parameterised type constructors
+-- (@MAYBE OF (FUNCTION FROM A TO B)@, @LIST OF FUNCTION …@, etc.).
+-- @\@export@ cannot accept any such parameter because functions can't be
+-- passed over JSON regardless of their wrapper.
 isFunctionTypeExpanded :: Map.Map Unique (Type' Resolved) -> Type' Resolved -> Bool
 isFunctionTypeExpanded synonyms = go Set.empty
  where
   go visited ty = case ty of
     Fun {} -> True
     Forall _ _ inner -> go visited inner
-    TyApp _ name [] ->
+    TyApp _ name args ->
       let u = getUnique name
-      in if Set.member u visited
-            then False  -- Prevent infinite recursion on cyclic synonyms
-            else case Map.lookup u synonyms of
-              Just expanded -> go (Set.insert u visited) expanded
-              Nothing -> False
+          expansion = case Map.lookup u synonyms of
+            Just expanded | not (Set.member u visited) ->
+              go (Set.insert u visited) expanded
+            _ -> False
+      in expansion || any (go visited) args
     _ -> False
 
--- | Collect all free variable references (by Unique) from an expression.
--- Uses cosmosOf gplate for recursive traversal of the expression AST.
-collectFreeRefs :: Expr Resolved -> Set.Set Unique
-collectFreeRefs =
+-- | Collect the 'Unique' of every identifier the expression references —
+-- whether it appears as a plain variable (@App _ ref []@) or as a function
+-- applied to arguments (@App _ ref [arg, ...]@). This is the single canonical
+-- dependency collector for an expression body.
+--
+-- Upstream callers (e.g. 'extractAssumedDependencies') intersect this set
+-- with a pre-filtered map (e.g. 'assumesFromModule' drops function-typed
+-- ASSUMEs), so semantic specialization happens at the filter step rather
+-- than in the collector itself.
+collectReferencedUniques :: Expr Resolved -> Set.Set Unique
+collectReferencedUniques =
   foldMapOf (cosmosOf (gplate @(Expr Resolved))) $ \case
-    App _ (Ref _ uniq _) [] -> Set.singleton uniq
+    App _ (Ref _ uniq _) _ -> Set.singleton uniq
     _ -> Set.empty
 
 -- | Extract ASSUME declarations that are referenced by a DECIDE body.
@@ -294,7 +306,7 @@ extractAssumedDependencies
   -> [ExportedParam]
 extractAssumedDependencies typeDescMap assumes (MkDecide _ _ _ body) =
   let
-    referencedUniques = collectFreeRefs body
+    referencedUniques = collectReferencedUniques body
     matchingAssumes =
       [ assume
       | (uniq, assume) <- Map.toList assumes
@@ -328,22 +340,33 @@ extractAssumeParamTypes
   :: Module Resolved
   -> Decide Resolved
   -> [(Text, Type' Resolved)]
-extractAssumeParamTypes mod' (MkDecide _ _ _ body) =
+extractAssumeParamTypes mod' decide =
+  [ (resolvedToText r, ty) | (r, ty) <- extractAssumeParamResolveds mod' decide ]
+
+-- | Like 'extractAssumeParamTypes' but returns the 'Resolved' name instead of
+-- its textual form. Consumers that need to bind the ASSUME in a local scope
+-- (e.g. MLIR lowering) need the Resolved so subsequent in-scope references
+-- resolve to the local binding.
+extractAssumeParamResolveds
+  :: Module Resolved
+  -> Decide Resolved
+  -> [(Resolved, Type' Resolved)]
+extractAssumeParamResolveds mod' (MkDecide _ _ _ body) =
   let
     assumes = assumesFromModule mod'
-    referencedUniques = collectFreeRefs body
+    referencedUniques = collectReferencedUniques body
     matchingAssumes =
       [ assume
       | (uniq, assume) <- Map.toList assumes
       , Set.member uniq referencedUniques
       ]
   in
-    mapMaybe assumeToTypeInfo matchingAssumes
+    mapMaybe assumeToResolvedInfo matchingAssumes
  where
-  assumeToTypeInfo :: Assume Resolved -> Maybe (Text, Type' Resolved)
-  assumeToTypeInfo (MkAssume _ _ (MkAppForm _ name _ _) (Just ty)) =
-    Just (resolvedToText name, ty)
-  assumeToTypeInfo _ = Nothing
+  assumeToResolvedInfo :: Assume Resolved -> Maybe (Resolved, Type' Resolved)
+  assumeToResolvedInfo (MkAssume _ _ (MkAppForm _ name _ _) (Just ty)) =
+    Just (name, ty)
+  assumeToResolvedInfo _ = Nothing
 
 -- | Check if a type contains any unresolved inference variables.
 -- Types with inference variables cannot be used for implicit ASSUMEs
@@ -378,3 +401,84 @@ extractImplicitAssumeParams errors =
   | MkCheckErrorWithContext{kind = OutOfScopeError name ty} <- errors
   , not (hasTypeInferenceVars ty)
   ]
+
+-- | Validate that no @export-decorated DECIDE has a function-typed input —
+-- either a GIVEN parameter, or a module-level ASSUME the body calls.
+-- Function-typed inputs can't be evaluated end-to-end: GIVENs can't be
+-- passed over JSON, and function-typed ASSUMEs stay 'ValAssumed' at
+-- runtime, causing a stuck "assumed term" error when the body invokes them.
+validateExportInputs :: Module Resolved -> [CheckErrorWithContext]
+validateExportInputs mod' =
+  let synonyms = collectTypeSynonyms mod'
+      assumes  = allAssumesFromModule mod'
+  in concatMap (checkOneExport synonyms assumes) (collectExportedDecides mod')
+
+-- | Collect every DECIDE whose description carries the @export flag.
+collectExportedDecides :: Module Resolved -> [Decide Resolved]
+collectExportedDecides (MkModule _ _ section) = goSection section
+ where
+  goSection (MkSection _ _ _ decls) = decls >>= goDecl
+  goDecl = \case
+    Decide _ d | isExportedDecide d -> [d]
+    Section _ sub -> goSection sub
+    _ -> []
+
+isExportedDecide :: Decide Resolved -> Bool
+isExportedDecide decide =
+  case getAnno decide ^. annDesc of
+    Just desc -> (parseDescText (getDesc desc)).flags.isExport
+    Nothing   -> False
+
+-- | Like 'assumesFromModule' but WITHOUT the function-type filter —
+-- so the validator sees every ASSUME and can flag function-typed ones.
+allAssumesFromModule :: Module Resolved -> Map.Map Unique (Assume Resolved)
+allAssumesFromModule (MkModule _ _ section) =
+  Map.fromList (collectSection section)
+ where
+  collectSection (MkSection _ _ _ decls) = decls >>= collectDecl
+  collectDecl = \case
+    Assume _ assume@(MkAssume _ _ (MkAppForm _ name _ _) _) ->
+      [(getUnique name, assume)]
+    Section _ sub -> collectSection sub
+    _ -> []
+
+checkOneExport
+  :: Map.Map Unique (Type' Resolved)
+  -> Map.Map Unique (Assume Resolved)
+  -> Decide Resolved
+  -> [CheckErrorWithContext]
+checkOneExport synonyms assumes decide@(MkDecide _ tySig (MkAppForm _ fnName _ _) _) =
+  checkGivenFunctionInputs synonyms fnName tySig
+  ++ checkAssumeFunctionInputs synonyms assumes fnName decide
+
+checkGivenFunctionInputs
+  :: Map.Map Unique (Type' Resolved)
+  -> Resolved
+  -> TypeSig Resolved
+  -> [CheckErrorWithContext]
+checkGivenFunctionInputs synonyms fnName (MkTypeSig _ (MkGivenSig _ names) _) =
+  [ mkExportFunErr fnName paramName
+  | MkOptionallyTypedName _ paramName (Just ty) <- names
+  , isFunctionTypeExpanded synonyms ty
+  ]
+
+checkAssumeFunctionInputs
+  :: Map.Map Unique (Type' Resolved)
+  -> Map.Map Unique (Assume Resolved)
+  -> Resolved
+  -> Decide Resolved
+  -> [CheckErrorWithContext]
+checkAssumeFunctionInputs synonyms assumes fnName (MkDecide _ _ _ body) =
+  let referencedUniques = collectReferencedUniques body
+  in [ mkExportFunErr fnName paramName
+     | (uniq, MkAssume _ _ (MkAppForm _ paramName _ _) (Just ty)) <- Map.toList assumes
+     , Set.member uniq referencedUniques
+     , isFunctionTypeExpanded synonyms ty
+     ]
+
+mkExportFunErr :: Resolved -> Resolved -> CheckErrorWithContext
+mkExportFunErr fnName paramName =
+  MkCheckErrorWithContext
+    { kind    = ExportFunctionTypeInput fnName paramName
+    , context = WhileCheckingDecide (getActual fnName) None
+    }

jl4-core/src/L4/TypeCheck.hs

@@ -93,6 +93,7 @@ import L4.TypeCheck.Unify
 import L4.TypeCheck.With as X
 import qualified L4.Utils.IntervalMap as IV
 import L4.Mixfix (MixfixInfo(..), MixfixPatternToken(..), extractMixfixInfo, canonicalMixfixName, firstKeyword)
+import qualified L4.Export as Export
 
 import Control.Applicative
 import Data.Monoid
@@ -175,9 +176,10 @@ doCheckProgramWithDependencies checkState checkEnv program =
                 -- Combine mixfix registry from imports with this module's local definitions
                 -- so importing modules can use mixfix functions defined here
                 combinedMixfixRegistry = unionMixfixRegistry localMixfixRegistry env.mixfixRegistry
+                exportErrs = Export.validateExportInputs rprog
             in MkCheckResult
               { program = rprog
-              , errors = substErrs ++ moreErrs
+              , errors = substErrs ++ moreErrs ++ exportErrs
               , substitution = s'.substitution
               , environment = env.environment
               , entityInfo = env.entityInfo
@@ -3223,6 +3225,12 @@ prettyCheckError (SuppliedComputedField fieldName) =
   , "Computed fields are automatically derived from their MEANS expression."
   , "Remove this field from the constructor."
   ]
+prettyCheckError (ExportFunctionTypeInput _fnName paramName) =
+  [ "Function type inputs are not supported for @export."
+  , "The parameter "
+      <> quotedName (getActual paramName)
+      <> " has a function type."
+  ]
 
 -- | Pretty print mixfix match errors with helpful suggestions.
 prettyMixfixMatchError :: Name -> MixfixMatchError -> [Text]

jl4-core/src/L4/TypeCheck/Types.hs

@@ -93,6 +93,10 @@ data CheckError =
     -- ^ Circular dependency between computed fields (record name, cycle of field names)
   | SuppliedComputedField Name
     -- ^ Tried to supply a computed field in a record constructor (field name)
+  | ExportFunctionTypeInput Resolved Resolved
+    -- ^ An @export-decorated DECIDE has a function-typed input (GIVEN or
+    -- referenced ASSUME). Arguments: exported-function name, offending
+    -- parameter/assume name.
   deriving stock (Eq, Generic, Show)
   deriving anyclass NFData