Repository navigation
feat(semantics): resolve operation signatures and type-check calls, bindings, and returns #195
Description
Audited on master at 5630d74ec9cd912d4e2f325349f1943cbc15bcc6. This is a scoped implementation item under #147, based on the typed control/dataflow/effect audit. Proposed syntax below is illustrative unless explicitly marked as a current reproducer.
Problem and current evidence
Type annotations are currently mapped into target strings, often by heuristics in nlsc/schema.py:229–392. nlsc/resolver.py:37–124 checks declared DEPENDS, not the actual operations called or the types flowing through them.
Reproduced:
[missing](1) -> result, with no DEPENDS entry, passes both shared validation and CLIverify --json; execution raisesNameError.- Calling a declared
increment(x: number)as[increment]("hello")passes validation, then fails atx + 1. RETURNSmixes a declared result type and a return expression, encouraging backend guesses.
Implementation hints
- Add a semantic symbol table for module/local ANLUs, constructors, imported operations, and explicitly supported builtins/foreign functions. Each operation has parameter types, result type, and later effect/failure contracts.
- Derive actual call dependencies from call nodes; compare DEPENDS against them as a declared contract. An omitted declaration must never make an unknown call valid.
- Resolve type names to target-neutral TypeRefs; check arity, argument types, field access, binding use, and return compatibility before either backend runs.
- Split the semantic return declaration from its value expression (
ReturnSpecor equivalent), preserving unambiguous legacy cases with a documented migration. A type alone is not a default value. - Reject duplicate identifiers and target-name collisions such as
foo-barversusfoo_bar. - Keep
any/unknown explicit; do not use a fallback toAnyas evidence of type safety. Native/foreign calls require declared signatures in checked code. - Plug the pass into the shared pipeline and diagnostic catalog, including CLI verify/compile/run/watch and editor consumers. This is a validity check, distinct from
nlsc lint— Semantic Linter #94's intent-quality lint.
Acceptance criteria
- Unknown calls, wrong arity/types, undefined value uses, unknown fields/types, and incompatible returns fail before code generation.
- Valid local calls, documented builtins/imports, optional inputs, and supported self-recursion pass.
- Inferred call dependencies do not depend on whether a user remembered DEPENDS.
-
RETURNS: totaland an explicit declared return type have distinct, testable meanings. - The same invalid program yields the same source diagnostic for every target.
- Both parser paths feed the same checker; native annotations are no longer treated as a substitute for NLS type validation.
Related: #75/#143/#147. Initial scope is the documented core types; generic typestate/ownership rules are a subsequent feature.
Implementation ordering
Integration depends on #194. Add the regression fixtures before implementation. Concrete bug fixes can land incrementally while those foundations are developed.
Osprey-informed implementation refinements
The initial IR and lowering boundary landed in #194 / #203. Extend the existing IR and lowerer; the earlier reproductions above describe the original audit snapshot, not a fresh verification of this commit.
- Assign resolved symbol identities to operations, imports, locals, and builtins. Builtin typing and callback behavior must follow that identity, so a user binding named like a builtin does not inherit its signature or privileged treatment.
- Reuse the IR's TypeRef and separate return specification. Store resolved types/callees in checked nodes or node-ID-indexed semantic tables; emitters should not repeat name or type inference.
- Distinguish successful parsing/lowering from successful type checking. An IR with no Foreign nodes still needs call, field, return, and control validation before it is advertised as checked.
- Represent callable parameter/result types and latent operation requirements for the callable forms NLS supports. A callback returned through a record or wrapper cannot lose its contract. Unsupported dynamic shapes need an explicit diagnostic or conservative unknown summary.
- Start with NLS's documented core types. Osprey's Hindley–Milner implementation is a reference for constraint solving and generalization, not a requirement to adopt full HM inference, implicit Result wrapping, currying, or another language's syntax.
Additional acceptance cases:
- A shadowed builtin is resolved and checked as the actual user binding; aliases retain the resolved callee identity.
- Both parser paths produce the same resolved semantic result for equivalent source, independently of selected backend.
- A supported callable passed/returned through a wrapper retains argument/result types and latent requirements; an unsupported callable form is never silently treated as pure or well-typed.
- Lowering success alone cannot bypass this pass in compile/run/watch/test or editor validation.
References pinned to Osprey 8792de9f6d159922141f9d191e4bc5d256fbb971: type implementation, operation/callback analysis, and shared frontend contract.
Follow-on consumers are typed handlers #207, resumption #208, and backend conformance #202. They do not expand this issue into a handler runtime implementation.
Activity
fix(resolver.nl): declare errors input instead of undefined self