Ralph24 - #133
Merged
Merged
Ralph24#133
Conversation
Later match arms were not inferred. The checker now infers each arm and requires every arm body type to equal the first arm body type. A mismatch reports the arm body span. Errors inside later arms, such as unbound variables, now surface. The stricter pass exposed a latent rejection: unary minus only accepted Int. Codegen already emitted fneg for Float. The checker now accepts Int and Float operands for unary minus. Bit-not keeps the Int-only rule. The tyck oracle covers multi-arm match inference, arm type mismatch, later-arm unbound variables, and unary minus on Int, Float, and Bool. LLVM IR fixed-point converges. The kernel suite passes with the new compiler.
Tuple patterns never compared literal components. (1, s) matched any first component and silently took the first arm. The tuple try phase now tests Int, Bool, and String literal components against the peeled values. A mismatch branches to the next arm. Nested tuple patterns recurse with their component patterns. The checker no longer binds literal components as variables. Kernel oracles prove flat, three-component, and nested tuple literal matches, including fall-through to later arms. The concrete oracle failed before this change and passes after it. LLVM IR fixed-point converges. The kernel suite passes with the new compiler.
Map.empty, Set.empty, and List.empty produced a bare handle. The payload never pinned, so mixed keys and values passed check. A parameterized handle now pins key, value, and element wants for Map.set, Map.get, Map.contains, Map.remove, Map.getOrElse, Set.add, Set.contains, Set.remove, Set.union, and Set.intersect. Map.set and Set.add on a bare handle return the payload from the argument types, so Map.set(Map.empty(), "a", 1) is Map[String, Int]. List.cons pins the list argument from the element type. List.concat pins the second list from the first. The tyck oracle covers pinned construction, key, value, and element mismatches, and List.cons. LLVM IR fixed-point converges. The kernel suite passes with the new compiler.
Audit against the pre-change compiler showed the pinning behaviors were already live. Map.*, Set.*, List.cons, and List.concat route through genericArgs, which binds payload types structurally. The zipCheck helpers added in the previous pass were unreachable, as were the pre-existing Map.get, List.at, List.cons, and List.concat branches of kitRetFromTy. Delete all of them. The tyck oracle cases stay. They pass before and after this change. They now lock in the generic-path pinning semantics they were written to prove. LLVM IR fixed-point converges. The kernel suite passes.
sz_panic_push_src runs at every emitted function entry. It called coverage_hit even when SCUZZ_COVERAGE_DUMP was unset. coverage_hit is too large to inline, so the no-op path paid a call per source span. A gprof profile of scuzz check examples/compiler put coverage_hit at about 15 percent of self time. coverage_probe now sets a coverage_off flag when the dump path is unset. sz_coverage_hit and sz_panic_push_src skip the coverage_hit call when the flag is set. sz_coverage_env_refresh clears the flag. scuzz check examples/compiler drops from 21.6 s to 20.6 s wall. coverage_hit no longer appears in the flat profile. Runtime tests, LLVM IR fixed-point, tyck oracle, and the kernel suite pass.
refineEnv only inspected the top level of each for-bind value. An offer inside IO.both, a lambda, or a match arm never pinned the handle payload, so a take afterwards kept the loose type. refineEnv is now a full expression fold. Any Queue.offer or Deferred.complete in the bind value pins the payload in source order. An offer statically constrains the payload wherever it appears. A payload seen only through a lambda parameter still does not pin. The tyck oracle covers nested offers in IO.both, IO.foreach lambdas, and if expressions, plus Deferred.complete, with consistent and mismatched takes. LLVM IR fixed-point converges. The kernel suite passes with the new compiler.
Nested patterns in constructor fields and tuple components were broken in three ways. Constructor and tuple patterns in fields crashed the LLVM link. As-patterns, bare enum cases, or-patterns, float literals, and list literals in fields silently matched the wrong arm: Opt.Some(n @ 0) matched Some(5), W.V(Opt.None, _) matched V(Some(9), 2), and Opt.Some(0 | 1) matched Some(2). The checker now validates arm patterns and rejects nested composite patterns with a clear error. Literal, variable, wildcard, and cons patterns with simple parts stay valid in constructor fields. Literal, variable, wildcard, and nested tuple patterns stay valid in tuple components. Arm-level as-patterns and or-patterns are unchanged. The kernel example used two rejected forms. Opt.Some(n @ 0) is now Opt.Some(0), and Opt.Some(0 | 1) splits into two arms. Both were silently miscompiled before; runtime output is now correct for Some(5) and Some(2). The tyck oracle covers every rejected form and the supported forms. LLVM IR fixed-point converges. The kernel suite passes with the new compiler.
An unannotated lambda bound its parameter to the letter A, which
unifies with any type. f = (n => n + 1) then f("s") passed check and
crashed at runtime.
inferFunApply1 now rejects applying an env-bound function whose
parameter type is an unresolved param letter to a concrete argument.
The message asks for an annotation. Loose arguments still pass, so
generic def bodies are unchanged.
An inline lambda in apply position now infers with the argument type
as its expected type: (n => n + 1)(1) is Int, and (n => n + 1)("s")
fails with the arithmetic error. This also keeps the verify rewriter
sound: its generated pred.apply(reqv) applications now check the pred
against the payload type with no annotation needed.
The tyck oracle covers the crash case, annotated lambdas, the
monomorphic identity rejection, and inline apply. LLVM IR fixed-point
converges. The kernel suite and the io fuzz replay pass.
refineEnv pinned a bare handle only when an offer or complete named an env var directly. A payload seen only through a lambda parameter did not pin: IO.foreach([q], x => Queue.offer(x, 1)) left q bare, so a later take kept the loose type and unified with anything. refineEnv now detects iteration calls that bind a lambda parameter from a collection element: IO.foreach and IO.foreachDiscard in call form, and foreach, map, flatMap, and filter in method form. When the element type is a bare handle, the lambda parameter binds in the refinement env. If the body pins the parameter, the pinned payload propagates back to the collection source. A list literal pins each bare-handle element var. A list var pins its element type. The tyck oracle covers consistent and mismatched takes after a lambda-param offer, for Queue and Deferred, in both call and method forms. LLVM IR fixed-point converges. The kernel suite and the kits slice pass with the new compiler.
A lambda argument checked against a concrete function type inferred without the expected type. The unannotated lambda kept the loose A => A, which unified with any function type: apply(n => n) passed against f: Int => String, and f(1) returned Int where String was declared. The same escape held in def-body position. zipCheckGo now infers each argument with inferExpected, matching the generic call path. checkDefWhere infers the body with inferExpected against the declared return type. An unannotated lambda binds its parameter from the expected argument type, so apply(n => n) fails with expected Int => String, got Int => Int, and def wrong(): Int => String = n => n fails against the declared type. Three oracles moved to the more precise lambda annotation message: the mismatched annotation now fails at the parameter instead of the whole body. New expectedLamTypes oracle covers call-form and def-body positions, annotated and unannotated, first and last arguments. LLVM IR fixed-point converges. The kernel suite and the kits slice pass with the new compiler.
Every evaluation of a string literal allocated a fresh SzString through sz_string_from_cstr: malloc, copy, UTF-8 measure, and the release chain when the value died. Match arms comparing against a literal paid the same cost per comparison. A gprof profile of scuzz check examples/compiler put sz_string_from_cstr and string_alloc at about 8 percent of self time, plus their share of the 38 percent RC churn. Emitted literal sites now call sz_string_lit. The first call builds the string and pins its rc at SZ_RC_PINNED; later evaluations share one allocation from a hash table keyed by content. sz_retain and sz_release skip pinned blocks, and sz_alloc_rc_sum excludes them so TestRuntime leak oracles stay paired. Runtime data still flows through sz_string_from_cstr; only compile-time literals intern. The match-memory probe warms up before it measures: first-touch interning is a one-time, program-size-bounded allocation, and the steady-state delta is still zero. IR goldens in examples/cli and examples/codegen name sz_string_lit. scuzz check examples/compiler drops from 20.2 s to 16.9 s wall. A cold scuzz build examples/tyck drops from 70 s to 34 s. Runtime tests, ASan, LLVM IR fixed-point, tyck oracle, codegen oracle, kernel suite, and the UI slice pass.
Check accepts nested ctor, tuple, cons, as, and [] patterns. Emit tests the inner structure and fails through to the next arm.
A parameter letter must not match a concrete return type, so `id[A](x: A): Int = x` fails while call-site instantiation still works.
IO.println and kit calls treated A as String; pin the def's own parameters so those mismatches fail while IO.pure(x) still instantiates.
Pinned A was still treated as Int in + , compare, and unary minus, so x + 1 typechecked.
Pinned A was still treated as IO or as a function, so x.flatMap and x.apply typechecked.
Pinned A still unified with View and String through Type.eq, so a View.each body of type A typechecked.
…type. handleErrorWith, fail-channel unify, and lambda annotations now pin against the enclosing def so A does not match Int.
… Int or the element type. Port, HTTP response, handler, and View.each function-argument checks now pin against the enclosing def.
…ion. Pin only the caller type so List.filter cannot take `_ => x` for `A`, while unbound kit parameters still instantiate.
Str.capture returns the first match plus groups. Str.replaceMatch substitutes a literal string for that match. Str.matches stays a full-string test.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.