Repository navigation
v0.19.0
[0.19.0] - 2026-10-06
Changed
-
BREAKING: Keep Surf pipes as syntax sugar;
fmtpreserves authored pipes, whiledeepandsurfemit normalized calls. Ungrouped mixes with other operators, postfix access, ascriptions, updates, or open-ended forms now require parentheses. Previous Deep/cache/package payloads must be regenerated.Silent numeric value change:
0.1 |> cast(f64)now adopts the f64 cast target before rounding, exactly likecast(0.1, f64). Its bits change from3fb99999a0000000to3fb999999999999a. To retain the former value, write0.1f32 |> cast(f64). Before upgrading a shell or downstream repository, runchelis migrate pipes --baseline-compiler OLD --inplace PATH...; it proves the complete expanded Deep unchanged before replacing the batch.--checkaudits without writing; explicit--keep-goingchecks or migrates independently proven files and reports every failure with a nonzero exit. -
BREAKING: A numeric literal's dtype is written at its site: it comes from the literal's suffix, or from a dtype-stating construct that directly contains it when the literal's kind admits the stated dtype, or else from the
i32/f32default, and never from a callee's signature or anything further away. The closed set of constructs is a declaration (the declared type of the binding ordefresult that the literal, or its negation, initializes, and a declared tensor type's element dtype for every literal element of a bare bracket initializer), acastwhose operand is the literal, and a new optional dtype argument ofto_tensor. Expression ascriptions such as(1.0 : f64)and declaredListtypes still only check.- Scalar declarations now bind their literal:
x: f64 = 1.1is exactly1.1f64,def f() -> i8 = -128binds thei8minimum, andx: i64 = 3000000000is accepted. Previously each was rejected as a dtype mismatch. A declaration states the dtype only of a literal that is its whole initializer:x: f64 = neg(1.1)andx: f64 = if c then 1.1 else 2.2stay rejected, and so do type aliases such asx: P = 1.1. to_tensor(xs, p)takes an optional dtypep, a primitive in an argument position that always names a dtype, never a value. It statespfor every unsuffixed literal element of a bracket-literalxs, soto_tensor([1.1, 2.2], f64)builds the exactf64values. It never converts: a leaf dtype other thanp, such asto_tensor([1.0f64], f32), is a type error. A dtype-bounded binderpis accepted as the dtype argument over leaves that already have dtypep, such asto_tensor([cast(1.1, p)], p). An unsuffixed literal that a binder dtype argument or a declared binder type would bind, as into_tensor([1.1], p)ordef f[p: Float](x: p) -> p = 1.1, is rejected with a diagnostic that namescast(1.1, p); see #3148.- An unsuffixed literal element of a
to_tensorcall without a dtype argument is a type error. Writeto_tensor([1.1, 2.2], f32)(ori32for integers) to keep the previous value, or state the dtype you mean. In particularcast(to_tensor([1.1, 2.2]), f64), which rounded both elements throughf32, is rejected and its diagnostic names bothto_tensor([1.1, 2.2], f64)andcast(to_tensor([1.1, 2.2], f32), f64)(#3080).xs: tensor[2, f32] = to_tensor([1.1, 2.2])is the same error; the bare bracketxs: tensor[2, f32] = [1.1, 2.2]keeps taking the declared dtype. AListbound first keeps its defaults:xs = [1.1]; to_tensor(xs)is accepted. In Deep, an untyped numeric literal element of ato_tensorargument is rejected. - A cast whose unsuffixed literal operand its primitive target binds desugars to that literal alone, with no
castnode:cast(1.1, f64)has exactly the Deep of1.1f64, andcast(3000000000, i64)that of3000000000i64(#3135). A negated operand folds into one signed literal at the target, socast(-128, i8)is thei8minimum, which has no suffixed spelling. Values are unchanged. Every other literal cast keeps its node and converts:cast(1.1f32, f64)still widens thef32value,cast(2.0, i32)converts thef32default,cast(1, bool)istrue, and a cast to a dtype binder converts at the binder's members the literal's kind does not admit. to_tensoris a reserved name. Binding it as a top-level or packagedef,sig, ormacro, a function, lambda, or macro parameter, a block or pattern binder, or an imported name is rejected asReservedNamein Surf and in Deep, inside a reef package too. This replaces the refusal of a declared tensor literal under a localto_tensorbinding, and it rejects the previously accepted programs of #3152 and #3167.chelis surfprints a literal without its suffix only where re-reading the output binds it at the same dtype, and always suffixes a cast's literal operand, so a Deep-to-Surf round trip keeps every literal's dtype and everycastnode (#3165).
- Scalar declarations now bind their literal:
-
BREAKING: A macro definition must reference every one of its parameters in its body.
chelis check,eval, andbuildnow reject amacrowhose body never uses a parameter, naming the macro and the parameter, whether or not the program calls the macro; a reference inside the scope of a body binder of the same name, such as afnparameter, does not count. Previously the argument for such a parameter was dropped during expansion, before name resolution, type checking, effect inference, and linearity checking, somacro first(a, b) = awithfirst(1i32, never_declared),first(1i32, print("boom")), or a reusedkeychecked clean and ran without the argument's effect, and a wrong-arity macro call inside the argument was never rejected. Rewrite such a macro without the unused parameter.In a single file or an entry module, a macro parameter now shadows an imported name of the same spelling inside the macro body, as it already did in library modules. Previously
import Std.Scalar (abs)withmacro apply(abs, x) = abs(x)bound the body'sabsto the import, soapply(neg1, 5i32)calledStd.Scalar.absand droppedneg1. See #3266. -
The canonical project reference describes Chelis's architecture and package
boundaries in present tense. See PR #3274.
Fixed
-
Rank-polymorphic
chelis evalcalls now enforce checked local tensor extent claims in execution order, including claims after the returned value is produced. Local claim axes account for expanded rank spreads in both eval and compiled C. See #3092. -
The checker rejects constructor and tuple patterns that cannot match the
scrutinee type, including wrong nominal constructors, non-tuple scrutinees,
and tuple arity mismatches. See #3228. -
Compiled C programs now respect the scope of match-arm pattern binders when a call is inlined. A pattern that re-binds a parameter's name, in any constructor, record, tuple,
@or nested pattern, keeps that name for its guard and body, and a pattern binder no longer captures a name read by a function passed in or defined around the match. Previously such programs could print a different result fromchelis eval. See #3229. -
A positional pattern over a record now binds the record's declared fields in the tensor graph that
gradandvmaplower to, whatever order the record literal wrote its fields in. Previouslymatch P { b: ..., w: ... } with { | P(w, b) => ... }boundwandbto each other's values there. As a result,gradreturned the gradient of a different function,vmapreturned wrong forward values in bothchelis evaland compiled C, and compiled C returned a wrong gradient with respect to a record-typed parameter built from such a literal. Field expressions still evaluate in written order. A lowering that cannot determine a record's declared field order now rejects such a pattern instead of guessing. See #3230. -
The checker rejects calls that use one type binder as both a tensor precision and an incompatible ordinary type. Cyclic precision constraints also report a type error. See #3233.
-
chelis proveno longer certifies a false property whose binder or module name is spelled like a solver symbol the prover generates, such as__erf_abs_0,__contract_std_normal_cdf_0, or__contract_std_quantile_0. Generated symbols are now chosen fresh against every name in the goal, so such a name stays an independent variable and the property is refuted or left unsupported; a counterexample may show the generated symbol with a numeric suffix. A solver goal that declares one variable twice is rejected instead of merging the two variables into one. See #3236. -
A macro call must supply exactly one positional argument per macro parameter and no named argument, and a macro definition may not repeat a parameter name.
chelis check,eval, andbuildnow reject a call with too few or too many arguments, naming the macro and both counts; a call that passesaccumulator=, naming the macro and the argument; and a repeated parameter, naming the macro and the parameter. Previously a missing argument let its parameter resolve to a same-named binding at the call site, a surplus argument was dropped before name, type, effect, and linearity checking, a call'saccumulator=was dropped so the expansion accumulated at the default precision, and a repeated parameter silently took the last argument. This applies to user-defined and standard prelude macros; anaccumulator=written inside a macro body is unaffected. See #3239. -
Constructor patterns with too few or too many fields now fail type checking with the constructor name and both field counts. This prevents evaluation and compiled C from selecting different match arms. See #3252.
-
Pipe grouping errors suggest parentheses for the rejected field access or
open-ended expression, and the migration guide pairs pipe migration with the
compiler pin bump. See #3254. -
Compiled C now evaluates the fields of a by-name record literal in written order, as
chelis evaldoes, when that order differs from the type's declared field order. Previously the C lane evaluated them in declared order, so a program such asS { hi: index(xs, 5), lo: index(xs, 7) }trapped on the field declared first rather than the field written first, and field effects such asdebugprinted in a different order than ineval. Field values are still stored in declared order. See #3265. -
chelis proveno longer loses a verdict when the module defines a name the prover uses for its own evaluation roots, such as__chelis_property_probe,__chelis_property_pre,__chelis_value_probe,__chelis_gen_probe, or__chelis_const_probe. Such a module used to end with aduplicate definitionerror or a spurious generator-starvationunsupportedresult; every injected root is now named fresh against the program, so the module gets the same result as with the definition renamed. When an opaque binder's constructor probe program is rejected before it runs, the record is now anerrorcarrying that diagnostic instead of a generator-starvation result. See #3267. -
chelis buildfor C, HIP and Metal now rejects a call through a function value that amatchpattern projected out of a constructor payload, a record field, anOption, or a tuple whose function component is not a callback parameter. The rejection is the typedunsupported:diagnostic that names the C target and cites #879. Previously the build failed inside ownership lowering with a message naming a compiler-generated binder such as__chelis_pattern_h__inl1.chelis evalstill runs these programs. Two related forms are not fixed here. Matching on a function-valued scrutinee directly (match f with { | g => g(x) }) still fails with an internal host site-map error. This failure predates this change, and no issue tracks it yet. Projecting a callback parameter out of a tuple (match (f, x) with { | (g, k) => g(k) }) still fails with the unbranded ownership-level #879 error. See #3268. -
Diagnostics from
chelis check,chelis evalandchelis buildin a reef package now name declarations and types as the author wrote them instead of by the package linker's privatepkg__<package>__<Module>__<name>spelling. A declaration of the checked module is named bare (def 'out'), so a package module and a standalone file report the same text; a declaration of any other module is qualified by its module path (Demo.Util.helper,Std.Datetime.Date), and also by package when two packages share that path, so no two declarations are named alike. Authored names containing__are shown whole. See #3269. -
A
deforsignamed like a standard prelude macro (residual,linear_layer,cross_entropy) in any module of a reef package graph is now rejected bychelis check,chelis build, andchelis evalalike. This covers the checked module, the modules it imports, the package's other modules, and the modules of its dependency packages. The spec/02 §P5b diagnostic names the declaration as written, prefixed with the file of the module that declares it. Previously, inside a package,checkreported the program clean andbuildproduced a binary that called thedefinstead of the macro.evalrejected the program only when the declaration was in the evaluated file. See #3270. -
Surf property fuzzing reuses the checked and lowered library across samples,
guards, and shrinking trials, reducing the cost of properties over standard
library modules. Sample probes still pass the shared compiler checks.