diff --git a/MarchLean/CapCheck.lean b/MarchLean/CapCheck.lean index 22b54ba..077b912 100644 --- a/MarchLean/CapCheck.lean +++ b/MarchLean/CapCheck.lean @@ -1146,6 +1146,42 @@ partial def patCoveredCtors : Pattern → List String | .con name _ => [bareCtorName name] | .wild | .var _ _ | .tuple _ | .lit _ | .record _ | .unsupported => [] +/-- The scrutinee type names for which march's `find_missing_mc` takes its +INFINITE-DOMAIN branch — `| TCon (("Int" | "Float" | "String" | "Char" | +"Atom"), _) -> …` (`typecheck.ml:4375`), transcribed verbatim. That branch +runs only AFTER the `has_first_wild` test above it has already failed, and it +then reports the column as missing unconditionally: there is no finite +constructor set to enumerate, so nothing but a wildcard row can cover such a +scrutinee. -/ +def infiniteDomainTyNames : List String := + ["Int", "Float", "String", "Char", "Atom"] + +/-- The boolean literals `p` covers, peeling `as` and unioning an `or_`'s +alternatives exactly as `patCoveredCtors` does (and for the same reason: +`norm_pat_all` expands a `PatOr` into one row per alternative, so +`true | false` yields both `SPLit` rows). Only `Bool` needs this — it is the +one type whose `find_missing_mc` branch enumerates LITERALS rather than +constructors. -/ +partial def patCoveredBoolLits : Pattern → List Bool + | .as _ p => patCoveredBoolLits p + | .or_ alts => alts.flatMap patCoveredBoolLits + | .lit (.bool b) => [b] + | .wild | .var _ _ | .con _ _ | .tuple _ | .lit _ | .record _ | .unsupported => [] + +/-- Is `p` a shape the `Bool` coverage test below actually models — a boolean +literal, through any depth of `as`/`or_`? This is the `Bool` analogue of +`isModeledArmPattern`: anything else on a guardless arm means this checker +cannot account for what the arm covers, and per the safety-net rule its +presence must read as "cannot judge" (⇒ exhaustive), never as "does not +cover". At a `Bool` scrutinee no other shape is well-typed, so this should be +unreachable; it is here so that a decoder change which ever makes it +reachable fails CONSERVATIVE instead of manufacturing a reject. -/ +partial def isBoolLitPattern : Pattern → Bool + | .as _ p => isBoolLitPattern p + | .or_ alts => alts.all isBoolLitPattern + | .lit (.bool _) => true + | .wild | .var _ _ | .con _ _ | .tuple _ | .lit _ | .record _ | .unsupported => false + /-- Is a `match_`'s arm list exhaustive over `scrutTy`, per march's `check_exhaustiveness` restricted to the guardless-coverage fragment it falls back to whenever any arm carries a `when` guard (`typecheck.ml:4546-4581`: @@ -1211,25 +1247,34 @@ become reachable for `Option`/tuple-headed scrutinees the moment the Task 3` fixtures below) is ever closed and such matches stop being screened out upstream. -**Known false-accept class (Finding I2, documented not fixed):** a -`Pattern.lit` arm list over a non-ADT scrutinee (`Int`/`String`/`Float`) has -no built-in/user ctor set to test against at all — but that mismatch is never -even reached: `Pattern.lit` is not one of `isModeledArmPattern`'s recognized -forms, so the SAFETY NET above fires FIRST on the unmodelled `.lit` pattern -and short-circuits to "exhaustive" before `headTypeName`/`scrutTy` are -consulted at all — this checker EXITS 0 on it either way. march, by -contrast, DOES exhaustiveness-check literal patterns against a scrutinee's -structure (`check_exhaustiveness` -handles `PatLit` rows) and rejects `match n do 0 -> 1; 1 -> 2 end` (no -catch-all) as non-exhaustive. This is therefore a live false-accept class, -not merely a "skip" as an earlier draft of this docstring implied — `Int`/ -`String`/`Float` matches are otherwise fully in-fragment (they reach this -gate at all, rather than being screened out by `hasUnsupported` upstream), -so the unknown-type carve-out's conservatism here produces a genuine -divergence from march, not an out-of-fragment skip. Left unfixed -deliberately: narrowing the unknown-type rule to close this gap risks -reintroducing a false reject elsewhere (the exact failure mode C1/C2 already -demonstrated), which this differential oracle must never manufacture. +**Finding I2 — FIXED (see the two branches at the head of the body below).** +A `Pattern.lit` arm list over a non-ADT scrutinee used to reach nothing at +all: `Pattern.lit` is not one of `isModeledArmPattern`'s recognized forms, so +the SAFETY NET fired FIRST on the unmodelled `.lit` and short-circuited to +"exhaustive" before `headTypeName`/`scrutTy` were consulted, and `Bool` — not +registered in `builtinCtors` — fell through the `find?` to the unknown-type +carve-out and got the same answer. march rejects both +(`match n do 0 -> 1; 1 -> 2 end` on an `Int`, `match b do true -> 1 end` on a +`Bool`; verified directly), so this was a live false-accept class, not a +skip: such matches are fully in-fragment and reach this gate rather than +being screened out by `hasUnsupported` upstream. + +The reason it is now safe to close — and why doing so does NOT contradict the +general-conservatism rule below — is that these two scrutinee types are ones +march decides OUTRIGHT. `find_missing_mc` needs no `env`, no module-scoped +ctor resolution and no row budget for them: it tests `has_first_wild`, and +then either reports missing unconditionally (`Int`/`Float`/`String`/`Char`/ +`Atom` — an infinite domain) or checks for both boolean literals (`Bool`). +Neither the ctor universe nor the or-expansion policy — the two RECONSTRUCTED +inputs that rule is about — is an input to that decision. The one input that +is, the wildcard test, is the one this checker genuinely models +(`isCatchAllPattern` ↔ `norm_pat`'s `SPWild`, a correspondence worked through +in that function's docstring). + +Still open, and still deliberately not fixed, is Finding I1 above: coverage +is compared only at the TOP level, so a `(Bool, Bool)` tuple scrutinee +matched by `(true, true)` alone is judged exhaustive here and rejected by +march. That one really does need the full pattern matrix. --- @@ -1304,6 +1349,58 @@ def matchExhaustive (scrutTy : Ty) (userCtors : List (String × List String)) let isCatchAll : Pattern × Option Term × Term → Bool := fun (p, g, _) => g.isNone && isCatchAllPattern p if arms.any isCatchAll then true + -- FINDING I2, now FIXED. A non-ADT scrutinee is not an unresolvable type + -- this checker must decline on — it is a type whose coverage rule march + -- states OUTRIGHT, with no `env` lookup, no module-scoped ctor resolution + -- and no row budget to reconstruct. `find_missing_mc` tests + -- `has_first_wild` FIRST (a row starting `SPWild`, i.e. exactly what + -- `isCatchAllPattern` computes: `norm_pat`/`norm_pat_all` emit `SPWild` + -- for `PatWild`/`PatVar` and for nothing else, peeling `PatAs` and either + -- distributing or widening `PatOr` — see `isCatchAllPattern`'s docstring, + -- which already mirrors that correspondence for the ADT case). Only when + -- that fails does it dispatch on the scrutinee type, and for + -- `Int`/`Float`/`String`/`Char`/`Atom` it then reports the column missing + -- UNCONDITIONALLY (`typecheck.ml:4375-4381`). So past the catch-all test + -- above, march's answer for such a scrutinee is "non-exhaustive", full + -- stop — independent of the arm patterns' shapes, which is why the + -- `isModeledArmPattern` safety net is deliberately NOT consulted first + -- here: there is no shape whose meaning we could be getting wrong, only a + -- wildcard row that is either present or absent. + -- + -- This closes a live FALSE-ACCEPT class, verified directly against march + -- inside `cap no_panic`: `match n do 0 -> ..; 1 -> .. end` on an `Int`, + -- `match s do "a" -> ..; "b" -> .. end` on a `String`, and + -- `match x do 1.0 -> ..; 2.0 -> .. end` on a `Float` are all rejected + -- ("contains a non-exhaustive `match`"), and all three were accepted here + -- because `Pattern.lit` is not an `isModeledArmPattern` shape, so the + -- safety net short-circuited to "exhaustive" before the scrutinee type was + -- ever consulted. + -- + -- This does NOT violate the general-conservatism rule below. That rule + -- governs the two inputs this checker RECONSTRUCTS (the ctor universe and + -- the or-expansion policy); neither is an input here. The wildcard test is + -- the one input this checker genuinely models, and it is the only one this + -- branch depends on. + else if (headTypeName scrutTy).any infiniteDomainTyNames.contains then false + -- `Bool` is the other type `find_missing_mc` decides outright, and the only + -- one it decides by enumerating LITERALS: it has exactly two values, so + -- (past the catch-all test) the match is exhaustive iff both the `true` and + -- the `false` literal appear on a GUARDLESS arm (`typecheck.ml:4363-4374`). + -- `Bool` is deliberately absent from `builtinCtors` (see its docstring), so + -- before this branch a `Bool` scrutinee fell through the `find?` below to + -- the unknown-type carve-out and was always judged exhaustive — a false + -- accept for `match b do true -> 1 end`, verified against march. + -- + -- Unlike the infinite-domain branch, this one DOES read arm shapes (it + -- counts which literals are present), so it keeps a safety net: if any + -- guardless arm is not a boolean literal, this checker cannot say what it + -- covers and declines (exhaustive) rather than guess. + else if headTypeName scrutTy == some "Bool" then + if arms.any (fun (p, g, _) => g.isNone && !isBoolLitPattern p) then true + else + let lits := arms.flatMap (fun (p, g, _) => + if g.isSome then [] else patCoveredBoolLits p) + lits.contains true && lits.contains false else if arms.any (fun (p, g, _) => g.isNone && !isModeledArmPattern p) then true else let covered : List String := @@ -4122,9 +4219,7 @@ def letTrailingDivNonZero : Module := { example : (checkCaps letTrailingDivNonZero).isViolation = false := by native_decide /-- Sibling walk `matchesIn`: a non-exhaustive `match` in a trailing let's -RHS. (An `Int` scrutinee would NOT pin this — `matchExhaustive` is -deliberately conservative there and answers "exhaustive"; only a user ADT -whose constructors it can enumerate exercises the walk.) -/ +RHS, over a user ADT whose constructors `matchExhaustive` can enumerate. -/ def letTrailingNonExhaustiveMatch : Module := { decls := [ colorDType, @@ -4165,4 +4260,90 @@ def letDestructuringBinderClean : Module := opqPureMod #eval checkCaps letDestructuringBinderClean -- expect: ok example : (checkCaps letDestructuringBinderClean).isViolation = false := by native_decide +-- ── Non-ADT scrutinee exhaustiveness (FINDING I2, fixed) ──────────────────── +-- +-- Every fixture below was run against march directly (`--check`, exit 0 = +-- accept / 1 = reject) as the `mod P do cap no_panic … end` program its +-- comment quotes; the `expect:` line records march's own verdict, not this +-- checker's preference. Before the fix the four rejecting cases all ACCEPTED +-- here, because `Pattern.lit` is not an `isModeledArmPattern` shape and the +-- safety net short-circuited to "exhaustive" before the scrutinee type was +-- consulted. + +/-- Build a `cap no_panic` module wrapping a single `match` on `x : ty`. -/ +def npMatchMod (ty : Ty) (arms : List (Pattern × Option Term × Term)) : Module := { + decls := [Decl.dmod "NE" [ + Decl.dopts ["no_panic"], + Decl.dfn "f" [("x", Lin.unrestricted, none)] none + (Term.match_ (Term.var "x" opqSp ty) arms opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } + +def npArm (l : Lit) : Pattern × Option Term × Term := (Pattern.lit l, none, opqInert) + +/-- `match n do 0 -> ..; 1 -> .. end` on an `Int`. march REJECTS. -/ +def neIntLits : Module := npMatchMod opqIntTy [npArm (.int 0), npArm (.int 1)] +#eval checkCaps neIntLits -- expect: violation naming no_panic +example : (checkCaps neIntLits).isViolation = true := by native_decide + +/-- Teeth: the SAME shape with a `_` catch-all. march ACCEPTS. -/ +def neIntWild : Module := + npMatchMod opqIntTy [npArm (.int 0), (Pattern.wild, none, opqInert)] +#eval checkCaps neIntWild -- expect: ok +example : (checkCaps neIntWild).isViolation = false := by native_decide + +/-- A bare VAR arm is march's other `SPWild` row (`norm_pat`'s `PatVar -> +SPWild`), so it catches all just like `_`. march ACCEPTS. -/ +def neIntVar : Module := + npMatchMod opqIntTy [npArm (.int 0), (Pattern.var "k" Lin.unrestricted, none, opqInert)] +#eval checkCaps neIntVar -- expect: ok +example : (checkCaps neIntVar).isViolation = false := by native_decide + +/-- `match s do "a" -> ..; "b" -> .. end` on a `String`. march REJECTS. -/ +def neStringLits : Module := + npMatchMod (Ty.con "String" []) [npArm (.str "a"), npArm (.str "b")] +#eval checkCaps neStringLits -- expect: violation naming no_panic +example : (checkCaps neStringLits).isViolation = true := by native_decide + +/-- `match x do 1.0 -> ..; 2.0 -> .. end` on a `Float`. march REJECTS. -/ +def neFloatLits : Module := + npMatchMod (Ty.con "Float" []) [npArm (.float "1.0"), npArm (.float "2.0")] +#eval checkCaps neFloatLits -- expect: violation naming no_panic +example : (checkCaps neFloatLits).isViolation = true := by native_decide + +/-- `match b do true -> .. end` — one of `Bool`'s two values. march REJECTS. -/ +def neBoolOne : Module := npMatchMod (Ty.con "Bool" []) [npArm (.bool true)] +#eval checkCaps neBoolOne -- expect: violation naming no_panic +example : (checkCaps neBoolOne).isViolation = true := by native_decide + +/-- Teeth: both `Bool` literals present is EXHAUSTIVE — the branch must count +literals, not simply reject every `Bool` match. march ACCEPTS. -/ +def neBoolBoth : Module := + npMatchMod (Ty.con "Bool" []) [npArm (.bool true), npArm (.bool false)] +#eval checkCaps neBoolBoth -- expect: ok +example : (checkCaps neBoolBoth).isViolation = false := by native_decide + +/-- Both literals reached through one OR-pattern (`true | false`), which +`norm_pat_all` expands into two `SPLit` rows. march ACCEPTS. -/ +def neBoolOr : Module := + npMatchMod (Ty.con "Bool" []) + [(Pattern.or_ [Pattern.lit (.bool true), Pattern.lit (.bool false)], none, opqInert)] +#eval checkCaps neBoolOr -- expect: ok +example : (checkCaps neBoolOr).isViolation = false := by native_decide + +/-- A GUARDED arm contributes nothing to guaranteed coverage, so `true` behind +a guard plus a bare `false` still misses `true`. march REJECTS. -/ +def neBoolGuardedTrue : Module := + npMatchMod (Ty.con "Bool" []) + [(Pattern.lit (.bool true), some (Term.lit (Lit.bool true) (Ty.con "Bool" [])), opqInert), + npArm (.bool false)] +#eval checkCaps neBoolGuardedTrue -- expect: violation naming no_panic +example : (checkCaps neBoolGuardedTrue).isViolation = true := by native_decide + +/-- A scrutinee type this checker cannot name at all (a type VARIABLE) still +declines — the new branches key off a head type NAME and must not widen the +unknown-type carve-out. -/ +def neUnknownScrut : Module := npMatchMod (Ty.var 0) [npArm (.int 0)] +#eval checkCaps neUnknownScrut -- expect: ok +example : (checkCaps neUnknownScrut).isViolation = false := by native_decide + end MarchLean.CapCheck diff --git a/MarchLean/Infer.lean b/MarchLean/Infer.lean index 05ecf3c..cd1fbee 100644 --- a/MarchLean/Infer.lean +++ b/MarchLean/Infer.lean @@ -1028,10 +1028,7 @@ def inferModule' (s : Supply) (m : Module) : InferM (List (Span × MTy)) := do let t ← infer s { ctx with level := ctx.level + 1 } rhs let sch ← generalize s ctx.level t ctx := ctx.addScheme name sch - | .dfn name params _ body => do - -- `retAnnot` (the surface return type) is ignored: inference derives - -- the body's type and cross-checks `resolved_ty`, rather than trusting - -- the annotation. It exists only for `CapCheck`'s Check 1 return scan. + | .dfn name params retAnnot body => do let lvl := ctx.level + 1 let recTy ← freshMVar s lvl let paramMTys ← params.mapM (fun _ => freshMVar s lvl) @@ -1044,6 +1041,31 @@ def inferModule' (s : Supply) (m : Module) : InferM (List (Span × MTy)) := do let ctxIn := (params.zip paramMTys).foldl (fun c ((n, _, _), mt) => c.addMono n mt) (ctx.addMono name recTy) let bodyTy ← infer s { ctxIn with level := lvl } body + -- Honor the surface RETURN annotation, exactly as the param + -- annotations above are honored. march checks a clause's body against + -- its declared return type (the `expected `X` but got `Y`` error a + -- `fn f(n : Int) : String do n end` raises); leaving `retAnnot` + -- unconstrained here was a live FALSE-ACCEPT class covering every + -- return-position mismatch — verified directly against march for + -- `: String` over an `Int` body, `: ()` over a non-unit body, + -- `: Float` over an integer literal, `: Int` over a `Float` literal, + -- a record field of the wrong type, a nominal type alias + -- (`type Age = Int` is NOT transparent to march — it rejects + -- `fn f(x : Int) : Age do x end`), and a call to a correctly-typed + -- function at the wrong return type. + -- + -- This cannot manufacture a false reject from a mis-decoded + -- annotation: `Decl.dfn.retAnnot` is `some` only when the annotation + -- is fully IN fragment — `Elab.decodeDecl` forces the whole + -- declaration to `Decl.unsupported` (⇒ file skips) when the return + -- type contains a `Ty.unsupported`, and `decodeSurfaceTy` maps a + -- surface type VARIABLE not among the decl's own type params (a `fn` + -- has none) to exactly that `Ty.unsupported`. So the `tyToMTy` below + -- sees only ground, in-fragment types and cannot throw; the only + -- outcome it adds is a genuine body/annotation mismatch. + match retAnnot with + | some rt => unify s bodyTy (← tyToMTy s [] rt) + | none => pure () unify s recTy (paramMTys.foldr MTy.arrow bodyTy) let sch ← generalize s ctx.level recTy ctx := ctx.addScheme name sch @@ -1375,9 +1397,11 @@ with no unbound-variable throw for `cap_narrow`/`root_cap`. Modeled as a -- expected: cap-narrow-module-ok: true /- Same shape as above, but checking that `cap_narrow`'s polymorphic result -actually unifies with the `Cap(IO.Network)` return annotation (`inferModule'` -ignores `retAnnot`, so this unify is done explicitly here — see its doc -comment above `.dfn`'s case). `λ(root : Cap(IO)). cap_narrow(root)` infers to +actually unifies with the `Cap(IO.Network)` return annotation. This drives the +unify through a bare `Term.lam` rather than through `inferModule'` (whose +`.dfn` arm now performs exactly this unify itself), so it pins the underlying +`cap_narrow`-result/annotation interaction independently of the decl-level +plumbing. `λ(root : Cap(IO)). cap_narrow(root)` infers to `Cap(IO) → ?a`; unifying `?a` with `Cap(IO.Network)` and zonking must yield exactly `Cap(IO) → Cap(IO.Network)`. -/ #eval show IO Unit from do @@ -1399,6 +1423,45 @@ exactly `Cap(IO) → Cap(IO.Network)`. -/ | .error e => IO.println s!"cap-narrow-unify-ERROR: {e}" -- expected: cap-narrow-unify-ok: true +/- RETURN ANNOTATION — `inferModule'`'s `.dfn` arm must check the inferred body +type against the declared return type. `fn f(n : Int) : String do n end` is +rejected by march ("expected `String` but got `Int`"), verified directly; before +this check it ACCEPTED here, and did so for every return-position mismatch — +`: ()` over a non-unit body, `: Float` over an integer literal, `: Int` over a +`Float` literal, and a nominal alias (`type Age = Int`, which march does NOT +treat transparently). This `#eval` has teeth: deleting the `retAnnot` unify +makes it print `retannot-mismatch-FAIL: accepted`. -/ +#eval show IO Unit from do + let s ← Supply.new + let bad : Decl := .dfn "f" [("n", .unrestricted, some (Ty.con "Int" []))] + (some (Ty.con "String" [])) (Term.var "n" dSpan dTy) + match ← (inferModule' s { decls := [bad], schemes := [], insts := [] }).run with + | .ok _ => IO.println "retannot-mismatch-FAIL: accepted" + | .error _ => IO.println "retannot-mismatch-rejected: true" +-- expected: retannot-mismatch-rejected: true + +/- The near-miss the check above must NOT break: a return annotation that +AGREES with the body still infers cleanly. `fn f(n : Int) : Int do n end`. -/ +#eval show IO Unit from do + let s ← Supply.new + let ok : Decl := .dfn "f" [("n", .unrestricted, some (Ty.con "Int" []))] + (some (Ty.con "Int" [])) (Term.var "n" dSpan dTy) + match ← (inferModule' s { decls := [ok], schemes := [], insts := [] }).run with + | .ok _ => IO.println "retannot-match-accepted: true" + | .error e => IO.println s!"retannot-match-FAIL: {e}" +-- expected: retannot-match-accepted: true + +/- And the other near-miss: an UNANNOTATED `fn` imposes no constraint at all, +so a body of any type still infers. `fn f(n : Int) do n end`. -/ +#eval show IO Unit from do + let s ← Supply.new + let un : Decl := .dfn "f" [("n", .unrestricted, some (Ty.con "Int" []))] + none (Term.var "n" dSpan dTy) + match ← (inferModule' s { decls := [un], schemes := [], insts := [] }).run with + | .ok _ => IO.println "retannot-absent-accepted: true" + | .error e => IO.println s!"retannot-absent-FAIL: {e}" +-- expected: retannot-absent-accepted: true + /- VALUE RESTRICTION — the discriminating test for `demoteToLevel0`. `let net = cap_narrow(root) in (net, net)` must make `net` MONOMORPHIC: both diff --git a/MarchLean/Syntax.lean b/MarchLean/Syntax.lean index 422c330..3300ae3 100644 --- a/MarchLean/Syntax.lean +++ b/MarchLean/Syntax.lean @@ -243,8 +243,11 @@ inductive Decl where — is always in fragment when present, because the decoder forces the whole declaration to `Decl.unsupported` when the return annotation is out of fragment. `CapCheck.capsInReturnSignature` scans it so Check 1 covers - `param_tys @ ret_tys` exactly as march's `check_module_needs` does; `Infer` - ignores it (it infers the body's type, not the annotation). -/ + `param_tys @ ret_tys` exactly as march's `check_module_needs` does, and + `Infer.inferModule'`'s `dfn` arm unifies the inferred BODY type against it, + exactly as it already does for each param annotation — march checks a + clause's body against its declared return type, and leaving this + unconstrained was a live false-accept class (see that arm's comment). -/ | dfn (name : String) (params : List (String × Lin × Option Ty)) (retAnnot : Option Ty) (body : Term) | dlet (name : String) (rhs : Term) | dtype (name : String) (params : List String) (ctors : List CtorSig)