Type System

The type-system story in the current tree is wide, not narrow. It is not just about primitive types or inference; it is where effects, units, epistemics, ownership, refinements, traits, and pattern reasoning all meet. The comprehensive view has to show that breadth while staying honest about what is fully proven by the current artifact.

Current source map

• self-hosted/check/types.sio and self-hosted/check/infer.sio are the core starting points for ordinary typing and inference.
• self-hosted/check/effects.sio, units.sio, epistemic.sio, ownership.sio, traits.sio, and refinement.sio show how the checker has been split by concern.
• self-hosted/check/env.sio, defs.sio, patterns.sio, pat_decision.sio, and exhaustiveness.sio matter when understanding context, declarations, and match reasoning.

What the public docs can safely claim

• The checked artifact advertises units, refinement types, epistemic types, and algebraic effects as part of the language feature set.
• The refusal fixtures and current examples prove that at least part of this richer type story is not merely aspirational.
• The exact enforcement level for every advanced subsystem still depends on the artifact and on the particular code path you are exercising.

Small typed surface example

fn safe_div(a: i32, b: i32) -> i32 with Panic {
    if b == 0 {
        panic("division by zero")
    }
    a / b
}

How to stay truthful

• Use compile-fail and run-pass fixtures for claims about enforced behavior.
• Use source-map descriptions for breadth claims about the checker architecture.
• Do not collapse the whole checker into a simple Hindley-Milner story; the current repo is already structurally richer than that.