Skip to content
Typhon

The Unsafe Boundary

unsafe: is Typhon’s escape hatch for talking to code the type system can’t reason about — typically untyped third-party libraries or genuinely dynamic Python. It is a lexical region, not a per-value cast, with a hidden marker that prevents Any from leaking into typed code.

The shape

import some_untyped_lib


def f() -> int:
    unsafe:
        let raw = some_untyped_lib.fetch()       # would be implicit_any outside
        let first = raw[0]
        let value = first.get("count")
    # `value` carries an `Unsafe[T]` marker — must re-assert before crossing out


    let count: int = int(value)                  # re-assertion
    return count

What happens:

  1. Inside unsafe:, expressions that would normally infer Any bind freely. The checker suppresses tyc::type_mismatch, tyc::nullable_use, tyc::interface_isinstance, tyc::arg_count, tyc::not_callable, and tyc::non_exhaustive_match inside the block depth.
  2. Values acquire a hidden Unsafe[T] marker. Visible in diagnostics, not in source.
  3. Crossing out of the block into a non-unsafe context requires re-assertion: an annotation, a narrowing check, or an explicit cast.

The block lowers to if True: so scope rules are preserved:

Why a lexical region, not a per-value cast?

A per-expression unsafe expr form (TypeScript’s as Any) would let users sprinkle dynamism everywhere. A lexical region forces it into one visible scope where readers can spot it and reviewers can interrogate it. The Unsafe[T] marker means the boundary is enforced even when the region tolerates dynamism internally.

If real codebases show a pattern of unsafe { single_call() }, we may revisit. For v1, blocks have been good enough.

What is suppressed

Inside unsafe:, the checker tracks an unsafe_depth counter. While the counter is non-zero, these diagnostics are silenced:

  • tyc::type_mismatch — assignments / calls with incompatible types are allowed.
  • tyc::nullable_use — T? values can be used as if T.
  • tyc::interface_isinstance — runtime isinstance against an interface is permitted (caveat: still PEP 544 semantics — attribute-presence only).
  • tyc::arg_count — call-site arity mismatches are tolerated.
  • tyc::not_callable — invoking a non-callable is tolerated.
  • tyc::non_exhaustive_match — match on a sealed union without all variants is allowed.

Diagnostics on lines outside the block are unaffected. The boundary is enforced at the block exit.

What is not suppressed

unsafe: doesn’t disable parse errors, name-resolution errors, syntax checks, formatting rules, the ? operator’s enclosing-function check, or any structural rule that doesn’t depend on inferred types.

unsafe:
    let x = 1
    let x: int = 2     # ❌ shadowing — still a resolver error
unsafe:
    let y: int = bad?  # ❌ ? outside a Result-returning function — still an error

Re-assertion forms

To use an Unsafe[T] value outside the block, re-assert the type with one of:

Annotated let / mut

unsafe:
    let raw = some_lib.fetch()
let parsed: dict[str, int] = raw      # ✅ annotation makes the type concrete

Narrowing

unsafe:
    let raw = some_lib.fetch()
if isinstance(raw, dict):
    use_dict(raw)                     # ✅ narrowed

Explicit cast

unsafe:
    let raw = some_lib.fetch()
let s: str = str(raw)                 # ✅ str() is the cast

as! — the sound, one-line boundary cast

The re-assertion forms above all share a weakness: an annotation like let parsed: dict[str, int] = raw trusts the boundary blindly. Nothing checks at runtime that raw actually is a dict[str, int]. EXPR as! TYPE is the sound replacement: it collapses the unsafe: block and the re-assertion into one line, and it verifies the shape at runtime.

def load(resp: Response) -> dict[str, int]:
    let data = resp.json() as! dict[str, int]   # was: unsafe: ... then re-assert
    return data


def first_id(row: Row) -> int:
    let uid = row[0] as! int
    return uid

What happens:

  1. The checker types the whole expression as TYPE. The boundary value (which may be Any) flows in freely — no unsafe: block, no Unsafe[T] marker, no unsafe_value_leak footgun. as! reuses the same machinery as type[T] generic inference, not a bespoke special case.
  2. The lowering (in tyc-syntax) rewrites EXPR as! TYPE to __typhon_checked_cast__(EXPR, TYPE), resolved via an injected from typhon_runtime.cast import checked_cast as __typhon_checked_cast__.
  3. At runtime, checked_cast checks the value against TYPE — scalars and classes, numeric widening, unions and T?, Literal[...], containers and mappings recursively, tuples, aliases, newtypes and interfaces — and raises TypeError on a mismatch. The full table of supported targets is on the unsafe reference page.

Sound, unlike TypeScript’s as

A static-only re-assertion trusts the boundary blindly; TypeScript’s as is an unchecked compile-time coercion. as! is neither — it can only let through values it cannot prove wrong. The structural check is the whole point.

Accepting and refusing targets

Any / object targets accept every value, and int → float (and bool → int) widening is honoured, so a JSON int cast as! float does not spuriously fail. A target the runtime cannot check — a bare type parameter, Callable, an iterator or awaitable contract, a parameterised user class such as Box[int] — is refused at check time (tyc::generic) rather than accepted silently.

VM behaviour

The in-process VM intercepts __typhon_checked_cast__ before argument evaluation and runs a structural check of its own, so a wrong-shaped scalar, container, tuple, union or plain alias raises TypeError under tyc run as it does after tyc build. It does not yet enforce Literal, newtype, generic-alias or interface targets: those casts pass under tyc run and raise TypeError on CPython. tyc fmt preserves the surface as! syntax.

The generated runtime file is typhon_runtime/cast.py, exposing checked_cast(value, tp).

Composition scope

In v0.14.0, as! was restricted to a single physical line in value position only. As of v0.15.0 the lowering is structural — a bracket-, string-, and comment-aware fixpoint rewrite — so as! composes wherever an expression can appear:

  • value positions (= / op= / return / yield / bare expression);
  • nested inside call arguments — save(row[0] as! int, label);
  • inside comprehensions / collection literals — [x as! int for x in xs];
  • in statement conditions — if raw as! bool:;
  • across a value expression spanning multiple physical lines, as long as the left operand stays bracket-balanced.

The left operand is the whole current syntactic slot — back to the enclosing bracket, a top-level , / ; / : separator, an assignment / augmented / walrus =, a return / yield / if / while / assert keyword, or the line start (so a + b as! int casts a + b). The right operand is parsed as a type expression (dotted name, optional [...] subscript, |-union), so trailing code after the type (x as! int + 1, the for of a comprehension) stays outside the cast. An as! whose right side isn’t a type expression is left for the parser to reject cleanly.

Which boundary tool to reach for

  • model X: — a boundary you validate repeatedly.
  • A .dty stub — a long-lived dependency.
  • as! — an ad-hoc one-off shape assertion, the sound runtime-checked upgrade over a bare unsafe: re-assertion.

See unsafe → as! for the reference-page summary.

When to use unsafe:

  • Exploring a new dependency. First day with a third-party library — wrap in unsafe: while you figure out the API.
  • Genuinely dynamic code. eval, RPC stubs, getattr chains, dynamic class construction.
  • Quick scripts. One-off CLI glue where writing stubs isn’t worth it.

For anything long-lived, write a .dty stub. The block stops being a code smell when the surface area is genuinely untypeable.

When not to use unsafe:

  • To silence a checker error you disagree with. Read the diagnostic first; it’s almost always pointing at a real bug.
  • As a per-call cast. The block scope is the unit; don’t wrap a single line just to short-circuit a diagnostic.
  • Long-term production code. If you find yourself with unsafe: blocks scattered through src/, the libraries deserve stubs. Run tyc check --stubs after writing them.

unsafe: inside async def

Works as expected. The block doesn’t make the function async or sync; it just opens the dynamism gate.

async def fetch() -> dict[str, int]:
    unsafe:
        let raw = await some_lib.fetch_async()
        let data = raw["payload"]
    let parsed: dict[str, int] = data
    return parsed

Common mistakes

Smuggling Unsafe[T] out

def parse() -> int:
    unsafe:
        let v = messy_lib.get_int()
    return v       # ❌ Unsafe[Any] cannot flow into a concrete `int` context

Fix: re-assert inside or at the boundary:

def parse() -> int:
    unsafe:
        let v = messy_lib.get_int()
        let checked: int = int(v)
    return checked

Wrapping too much

unsafe:
    let raw = some_lib.fetch()
    process_safely(raw)            # ⚠️ also runs inside unsafe — diagnostics suppressed

Keep unsafe: blocks small. If process_safely is part of your typed code, lift it out:

unsafe:
    let raw = some_lib.fetch()
let payload: dict[str, int] = raw
process_safely(payload)

Implementation note

unsafe: is implemented in two parts:

  • The parser treats unsafe: as a soft keyword with a colon-introduced suite (same shape as if).
  • The checker wraps the suite in a depth-tracked enter_unsafe() / exit_unsafe() pair. Values originating inside the block carry an Unsafe<T> wrapper in the type lattice; assignments at the boundary require coercion to the concrete T.
  • The desugarer rewrites the block as if True: so the scope rules apply unchanged in the emitted Python.

Where next