The type systems of feel

feel has two type languages that look alike and do different jobs. One is the type system of the DMN specification, a small lattice that says which values an operation is defined for. The other is an internal type that the analyzer infers with, and it is much richer: it makes null an explicit alternative, and it carries sets of values (intervals of numbers, sets of strings, the dates a date can be). The internal type is what lets x > 5 and x < 3 be shown never to be true, what lets the optimizer drop checks, and what supports explanations for selected possible null results. This is a value analysis with bounded approximations, rather than only a check of declared kinds.

This document is the implementation guide: it explains both type languages, their representations, and how the analyzer uses them. The type-system assessment contains the correctness contracts, scientific foundations, language comparisons, recommended design, and open obligations. The original examples were recorded on 2026-10-16 with Elixir 1.20.4 on OTP 29 after D-173; later updates cover callable summaries, three-outcome facts, D-207's unknown negation and repeated-value arithmetic, the initial correctness repairs of 18 October 2026, and the signature, range and DMN proof contracts described in the assessment. They are recorded examples rather than a fresh run of the whole guide, and may drift as the analysis improves. architecture.md says where the type modules sit in the pipeline; decisions.md says why (D-39, D-109 and the rest, cited below).

Correctness status. The reproduced function-result check bypasses, nested-negation errors, false rule proofs, numeric complement/inclusion failures and order-dependent equivalence answers are repaired. Function signatures and call refinements now have separate roles, and certainty bounds use a different approximation direction from possible results. join/2 promises a conservative common supertype, not a least one. The assessment states each contract and the remaining audit work; these regressions do not establish a general soundness or completeness guarantee.

Contents: 1 The two languages · 2 The lattice · 3 The internal type · 4 Internal type against lattice · 5 Using the types (inference, why a result is null, narrowing, declarations, calls, uses, limits) · 6 Soundness · 7 Reading list

1. The two type languages

They are connected by two functions that are not inverses. Union.from_spec/1 reads a type of the specification and adds :null at every level. Union.to_spec/1 goes back, drops :null, and joins what is left with the lattice's join, so it loses information:

type expression  --Feel.Type.parse-->  Feel.Type  --from_spec-->  Union
(list<number>)                         (declared)                    |
                                                                     |  Analyzer: infers a Union for every node,
                                                                     |  narrows it by conditions, checks calls
                                                                     v
Feel.type/1  <------ to_spec -------------------------------   meta.type of the IR
(spec type)                                                          |
                                                                     |  Optimizer drops checks the type settles;
                                                                     v  diagnostics warn of certain mismatches

Feel.type/1, the type a caller sees, uses the declaration type language. The union stays internal. For guarded recursion, from_spec/1 produces a bounded upper approximation rather than an exact translation. Runtime membership keeps the original declaration graph; see guarded types.

2. The specification's lattice (Feel.Type)

The specification (section 10.3.2.9, Figure 10-26) gives FEEL a lattice with Any on top and Null at the bottom. Apart from the parameterised families the lattice is flat: the primitive types are siblings.

Any                     the top: every value, null included
 |-- number, string, boolean
 |-- date, time, date and time
 |-- years and months duration, days and time duration      (no common supertype)
 |-- list<T>, range<T>, context<k: T, ...>, function<T, ...> -> R
Null                    the bottom: the value null, which is under every type

All the children of Any are siblings, with no edge between them. Only the parameterised families, on the last child line, are ordered inside themselves, by the rules below.

The rules, as Feel.Type.Conformance implements them (T <: S means "T can be used where S is expected"):

The specification lattice has no union constructor. Feel.Type.join/2 computes a common supertype, which is why a list literal of mixed things is list<Any>. The API promises a conservative common supertype; it need not be the least expressible one for functions or composite declarations. Equivalence accepts equal terms or conformance in both directions, so reordered union declarations can compare equivalent. For bounded relations, failure to prove equivalence does not prove semantic inequality. See section 2.6.

Feel.Type.join(:number, :string)                       #=> :any
Feel.Type.join({:list, :number}, {:list, :string})     #=> {:list, :any}
Feel.Type.join(:number, :null)                         #=> :number          (null is absorbed)
Feel.Type.conforms?(:date, :date_and_time)             #=> false
small = {:context, %{"id" => :number, "name" => :string}}
large = {:context, %{"id" => :number, "name" => :string, "age" => :number}}
Feel.Type.conforms?(large, small)                      #=> true (more entries conform to fewer)
Feel.Type.conforms?(small, large)                      #=> false
Feel.Type.of([1, "a", true])                           #=> {:list, :any}

Three more pieces belong to the lattice and not to the union:

• instance of (Table 62): null is an instance of Null only, so Feel.Type.instance?(nil, :number) is false, while Feel.Type.value_conforms?(nil, :number) is true. The two questions differ, and both are needed.
• Implicit conversions (section 10.3.2.9.4, D-24): where a value is bound to a parameter of a declared type it may be converted. The three are from a singleton list (["foobar"] to "foobar"), to a singleton list (3 to [3]), and from a date to a date and time at midnight UTC. They are tried only when the value does not already fit, in that order, and at most one applies. One more is not in the specification, but the TCK needs it (D-197): a built-in function with several signatures that differ only in their types (abs), where a function type is declared that the function is not an instance of but one of its signatures is (function<number> -> number), becomes the function of that signature, which takes what the type says and returns null for the rest.
• T!, an extension (D-48): a declaration that the name is never null. It is the only way to say "not null", and it exists because the lattice has none. A type in an expression may have it too (D-48).

Two more extensions go past the lattice, for what a host declares (D-178), as T! does: the lattice has no union and no negation, and the internal type has both, so a declaration may say that a name is anything but a number, or a number or a string.

Runtime membership evaluates a composite's union or negation directly against the exact component declarations (Feel.Type.Composite). This also covers recursion in a value's function signature when the target itself has none. The analysis projection can be wider, especially for recursive negation, and cannot replace that runtime check. Non-recursive composite conformance asks Union.subtype?/2; composite conformance with recursive descriptors accepts identical terms conservatively. null is in them as it is in every declared type, since the run exempts null (D-138), and only a mark on the whole takes it out. They nest in a list, a range, a context and a function type. Any except takes the rest of the union (Any except number | string is neither), a type may be put in parentheses, and a ! on a member is refused ((Any except number)! is how to mark the whole). The conversions are the lattice's, asked of the union: a singleton list is unwrapped when its element is in the type and the list is not, and nothing is wrapped in a list and no date is converted to a date and time in order to reach a member. Feel.type/1 is a type of the specification, so for such a name it is wider (Any, list<Any>).

Feel.Type.parse("Any except number | string")      #=> {:ok, {:not, {:union, [:number, :string]}}}
Feel.Type.parse("list<number | string>")           #=> {:ok, {:list, {:union, [:number, :string]}}}
Feel.Type.parse("Any except number!")              #=> {:error, …}   a ! on a member is not read; mark the whole: (Any except number)!
Feel.Type.format({:union, [:number, {:not, :string}]})   #=> "number | (Any except string)"

These are for the declarations of a scope, the result type and the input of unary tests, and for a type of the scope that an expression names (v instance of tId, function(a: tId) a, where tId is number | string). The types written in an expression are those of the specification and T!: x instance of Any except number is Any followed by a word that is not part of the type.

Because null is under every type, the lattice cannot say that 1 < 2 is never null or that 1 < null is always null. Both are just boolean. That is what the second type language is for.

2.1 Model-defined and guarded recursive types

Feel.ItemDefinitions resolves acyclic model definitions into ordinary structural types. Recursion is a caller-selected extension with three modes:

In guarded mode, every cycle must cross a context member or list element. Alias-only cycles and cycles through function signatures remain errors. A finite function item may accept or return recursive data. Build graphs through Feel.ItemDefinitions; a plain cyclic map of unresolved {:named, name} types still fails Feel.Type.resolve/2.

definitions = Feel.ItemDefinitions.new([
  %{name: "Node", components: [%{name: "next", type_ref: "Node"}]}
], recursive: :guarded)
type = Feel.ItemDefinitions.types(definitions)["Node"]
Feel.Type.value_conforms?(%{"next" => %{"next" => nil}}, type) #=> true
Feel.Type.value_conforms?(%{"next" => %{}}, type)              #=> false: missing next

Runtime membership checks the full finite value. A present null member keeps the normal null exemption; a missing member does not conform. Allowed values and type constraints are separate: instance of and Feel.Type.value_conforms?/2 check structure only. Declarations carrying those constraints enforce them at every recursive occurrence through graph paths. Constraint traversal is incremental: a rejected occurrence stops the walk immediately. Successful checks share reversed paths; only a failing diagnostic constructs its complete forward path, avoiding quadratic path materialization on deep chains. During contained FEEL execution, shared worker deadlines and heap policies bound structural membership and recursive selector traversal, including shared-subtree expansion. Constraint tests retain their call and iteration counters even when diagnostics are isolated. Direct host membership queries have no worker, so containing them is the caller's responsibility. Ordinary conversions apply at binding, parameter and result boundaries, including singleton wrapping for a recursive collection or alias, and unwrapping for a recursive context. They do not convert fields inside a context. A collection's allowed values apply to its elements; its type constraint applies to the whole list.

To enforce constraints, build the variable's scope from the definitions. Supplying only types(definitions)["Node"] to a plain scope, or calling value_conforms?/2, does not carry them:

definitions = Feel.ItemDefinitions.new([
  %{name: "Node", components: [
    %{name: "value", type_ref: "number", allowed_values: "[0..9]"},
    %{name: "next", type_ref: "Node"}
  ]}
], recursive: :guarded)
{scope, unread} = Feel.ItemDefinitions.scope(definitions, %{"node" => "Node"})
# unread == %{}; inspect ItemDefinitions.problems/1 and unread before using model declarations
{:ok, expression} = Feel.prepare("node", scope: scope)
bad = %{"value" => Decimal.new(1), "next" => %{"value" => Decimal.new(20), "next" => nil}}
{:ok, nil, [diagnostic]} = Feel.run(expression, %{"node" => bad})
{diagnostic.code, diagnostic.details.path} #=> {:value_not_allowed, ["next", "value"]}

This uses the default declarations: :enforce: a failing descendant makes the whole variable null, and strict execution ends with an error. Declaration stances such as :report, :trust and :ignore keep their existing behavior; selecting guarded mode does not override them. Diagnostic paths use member names and one-based list indexes. For a result boundary, obtain {:ok, type, constraints} from Feel.ItemDefinitions.variable(definitions, "Node"), then pass result_type: type, result_allowed_values: constraints to Feel.prepare/2.

Analysis unfolds repeated names conservatively and shares a 256-node projection budget. Exhaustion widens the analysis, with no corresponding cutoff in runtime membership. Inclusion in the projection proves neither recursive membership nor that conversion preserves the operand: parameter and result bounds describe the converted value, and specialization discards pre-conversion shapes, callees and origins. Recursive result checks and reachable negative branches remain.

Recursive conformance accepts identical reachable graphs under consistent one-to-one renaming, including import prefixes, while ignoring unrelated graph entries. Constructors, constraints and reference sharing must agree. It also accepts graphs related by ordinary lattice rules but does not provide general recursive subtyping or equivalence. Even a structural upper projection need not be accepted as a recursive function's result signature. Runtime closures keep an enforced recursive result declaration through result and binding checks (Feel.IR.result_spec/1). The analyzer selects the runtime result signature before optimization and stores it in the function's meta.returns; both backends keep it when a conditional body folds to a declaration. Observable analysis arrows use Any | Null for that result and keep structural bounds only as call refinements. Recursive parameter domains use an empty lower bound in upper arrows. Graph projection and overlapping runtime signatures can lose call precision too. These are analysis limits, not weaker finite-data validation (D-189).

3. The internal type: Feel.Type.Union

3.1 The shape

A union is a list of the alternatives a value may have, and :null is one of them when the value may be null:

:any inside a union means any value that is not null, and it is the union of the kinds of value (D-39): the eight primitive kinds, a list, a range, a context and a function of any shape, and foreign, a term that is not a value of FEEL (the host binds what it likes, and the run treats it as a value of an unknown kind). A union that has all of them is Any, and one that lacks some is written by what it lacks: Any except number. The parts of a list, a range, a context or a function are unions in turn, so list<number> and list<number | null> are different members.

The members a union can have (Feel.Type.Union, the type member), and how Union.format/2 writes them:

A union has a normal form, built by Union.new/1, so that two unions of the same alternatives are equal: no repeats, a fixed order with :null last, :any absorbs everything else, and at most one alternative per kind of number, string, boolean, date and duration (the sets of several are joined).

Union.new([:null, :number, :number])    #=> [:number, :null]
Union.new([:number, :any])              #=> [:any]
Union.new([:any, :null, :boolean])      #=> [:any, :null]

A union that is built has at least one alternative: Union.new/1 raises for none. The least type of an expression that runs is [:null], because a failure is a null and not the lack of a value, so a type with no alternative is not the type of anything that has a value. But there is one, the empty union, Union.never(), [], written Never (D-173). It is the never of TypeScript and the none() of Elixir:

• It is the type of code that cannot run, and it is not [:null]. [:null] is code that runs and gives null; Never is code that gives nothing because it is not run. The analyzer gives it to every node of a branch of an if that cannot be taken (5.3).
• It is the bottom of the order: subtype?([], u) is true for every u, nothing but itself is within it, contains?([], v) is false for every value, and Union.new/1 leaves it out of what it joins. Where the lattice has Null at the bottom because null is under every type, the union has Never, because [:null] is not under [:number].
• Union.intersect/2 and Union.difference/2 return it when two unions share nothing, or when nothing is left (the two cannot be the same value), and it is the element type of the empty list ({:list, []}, below).

A node of this type that a run reaches means that the type was wrong, and Feel.Paranoid says so (section 6).

3.2 null made explicit

This is the first of the two things that the union adds to the lattice (D-39). The analyzer can now say that a result is, or is not, null:

A number that is bound from outside may be null, so age is number | Null. A constant never is. Note the two rows of structure: the type of a list is the union of its elements (the specification's list<Any> forgets that the elements are a boolean, a number and a string), and a context literal has a closed type, the entries it has and no others, where a declared context type is open (D-65). A closed context is a subtype of the open one with the same entries, so it knows more, for instance that an entry it does not list is not there.

3.3 Value sets

Numeric set endpoints and runtime numbers are related but not interchangeable. NumberSet can hold decimal bounds that do not themselves fit the runtime's 34-digit format; month-duration images can also contain integers of arbitrary size. Rounding images cut their endpoints outward to representable FEEL numbers (D-220), preserving upper bounds instead of using a huge exact integer step as a runtime operand. Power inference remains conservative for unsupported corners; root, logarithm and exponential images can fall back to signature bounds. See the numeric endpoint rules.

This is the second addition (D-39, D-109). An alternative can say which values it has. The bare kind (:number) is every value of the kind and contains any set of it.

The image trick is worth a sentence. A date, a duration, a time and a date and time are ordered, and for the durations also added and scaled. If each value is mapped to a number, one-to-one and order-preserving, then the interval algebra written for numbers works for them too: the seconds of PT1H + PT2H are 3600 + 7200. A time and a date and time cannot use one number, because the order of two of them depends on their zones, so Moment keeps three lines of numbers far apart on the number line and a value is in a set when its numbers are on the right lines.

Numeric construction, union and intersection take an approximation policy: :outer (the default) replaces more than 16 merged intervals by their hull; :inner keeps at most 16 intervals as a subset; :exact keeps all intervals. Possible-result analysis uses upper bounds, while TestSets.certain/2 uses inner numeric bounds. NumberSet.complement/1 and subset?/2 are exact over their supplied sets, including when the complement of 16 intervals needs 17. Exact complement cannot recover values lost by an earlier approximation; callers must still choose the correct bound direction. In particular, numeric and numeric-image exclusions are combined exactly before complementing in Union.difference/2. Range-subtyping proofs can combine several individually small endpoint sets past the cap; using an outer hull there would erase genuine gaps and could prove false range coverage. The remaining positive result can still be widened safely. This does not turn every union operation into exact algebra.

Ordinary union normalization also widens string sets with more than 64 points or exclusions to the whole string kind. Certain string sets instead discard information before that widening can establish a false proof. The boundary cases are in sections 2.3 and 2.5. The ordinary upper-bound simplifications include:

[0..5) and [5..9]      become   [0..9]              touching intervals merge
[0..5) and (5..9]      stay     [0..5), (5..9]      5 is in neither, so there is a gap
[0..1], [10..11], ... [190..191]   (20 intervals)
                       become   [0..191]            over 16 intervals: the one that holds them all
a string set with more than 64 points or exclusions becomes every string in Union normalization

A set is not a type in the sense of a name for a class of values. It is a value domain with a union, an intersection, a complement, a subset test and a membership test. NumberSet.complement([0..150]) is [-max..0), (150..max], and StringSet.complement(["a"]) is (..) except "a". That is the complement of a set of values. The negation of a type with parts, which has no set to cut, is a member of its own (3.5).

3.4 The operations

Existing tests compare subtype?/2 with Feel.Type.conforms?/2 on selected specification types. An alternative that no alternative of the other union holds by itself may be held by several together (D-152): subtype?/2 then asks whether anything of it is left when the others are taken out (difference/2). So a case that a comparison alternative by alternative cannot see is detected, as in the set interpretation, for lists, ranges and contexts:

# the unions are written in shorthand here (Union.format/1 prints a closed context as `context<…>`); `|` is the union
a = closed context<k: "a" | 1>
b = closed context<k: "a"> | closed context<k: 1>
Union.subtype?(a, b)            #=> true      (every value of `a` is in `b`; it was `false` before D-152)
Union.subtype?(b, a)            #=> true

The procedures use resource bounds: a range search stops above 6 negations, and a context search above 4,096 parts or 256 for one entry (D-158). Functions use the signature model in section 3.5. A built-in with several signatures is an overload. A negative Boolean answer may mean only "not proved". A positive answer still needs a valid underlying inclusion argument; the current boundaries and projections prevent a blanket soundness claim.

Normalization keeps exclusions inside lists, ranges, contexts, functions and excluded types. Readers request a positive approximation explicitly at the level they inspect. Widening an excluded part or a function parameter during normalization would change the meaning in the wrong direction. For paths, that includes list elements and nested entries traversed by descendant selection, as well as the source union. Paths approximates those inspected unions locally; a selected context entry keeps its original exclusion-bearing type. The path-result check regression is described in section 2.4.

This obligation also applies to filter name discovery, recursive equality of context fields, context construction/merge, callback classification and generic signature-derived flattening. An excluded context can supply filter entries and unknown descendants; it cannot be treated as absent when deciding bindings or domain emptiness. Open context types do not establish that an unlisted key or value is missing. A callback's runtime acceptance follows its observable arrows, not a specialized Boolean call result. Recorded arrows are guarantees, not an exhaustive signature list: a three-argument function can also support a two-argument Boolean callback. Without a qualifying guaranteed arrow, list images keep both success and rejection, including after narrowing or exclusion. Section 2.4 states the reader rules, the result-check regressions and the bounded independent oracle.

A list has two more types that the union of the kinds does not give (D-152): the empty list, [], a list with no element it could have, and a list that has an element, a list type less it (non-empty list<number>). list<T> is the two, and the meet of two lists with no element in common is the empty list. These examples illustrate the supported list operations:

Union.intersect([list<number = 7>], [list<string>])        #=> [empty list]
Union.difference([list<number | Null>], [empty list])      #=> [non-empty list<number | Null>]
Union.new(non_empty ++ [empty list])                       #=> [list<number | Null>]

3.5 A kind less some of it, overloads, and functions

A list, a range, a context and a function have no set of values to cut, so what is left of Any when some of one is taken out is a member of its own, {:except, base, negations} (Feel.Type.Except, D-152): the values of base that are in none of the negations. It is how v instance of list<number> leaves its else branch:

if v instance of list<number> then 1 else v     #=> Any except list<number | Null> | Null      (v is Any)

Whether such a member has any value is queried kind by kind, subject to the representation and search limits. A list less lists of N1, N2, … is treated as empty when its base is within one of them (a list avoids each with an element of its own); a range has two ends that each avoid some of the negations (a range with more than 6 negations is taken to have values); a context is a box of the types of its entries and the question is whether the boxes of the negations cover it (at most 4,096 parts are visited, and 256 for one entry), and an entry that an open context does not list is there or not. Past a bound, or where the answer is not shown, the member is kept: the type holds more than it has to. Two members are also in normal form when no negation is within another and each shares values with the base.

A function has no values to list either. The only thing the run says of one is the function types it was declared with, so a function is a finite set of arrows, and it is an instance of a function type when one of its arrows is within it (Feel.Type.Arrows, D-171). That is what instance of answers, so it is the meaning of the type: the else of a test is taken out when the run takes it. An arrow A is within B when B's parameters are within A's and A's result is within B's (the rule of the specification), and a type of arrows less arrows has a function unless some arrow of the first is within some arrow taken out. It is one comparison and not a search.

A built-in function with several signatures is all of them. before is four function types, a point or a range for each of its two parameters; abs is declared with one parameter for the three kinds it takes. Its type is {:overload, arrows, refinements}: the arrows are what the algebra sees, and the refinements are what a call does for arguments within the parameters of a signature (abs of a duration is a duration), which types a call and nothing else:

before instance of function<number, number> -> boolean       #=> boolean = true
abs instance of function<number> -> number                   #=> boolean      (not true: abs takes the three kinds in one parameter)

The algebra stops short of the semantic subtyping of Frisch and Castagna, where (A → B) ∧ (C → D) is within (A ∪ C) → (B ∪ D). The run does not say that, and a type that said more than the run would put a value in an else branch that the type excluded. A union holds at most four overloads; past that each is its arrows.

A function literal also uses an overload when its body gives a more precise call result than its observable signature. For function(x: number) 1, the arrow returns nullable number, matching runtime metadata; the call refinement returns exactly 1. Only the arrow participates in instance of. Calling the function can use the refinement without claiming that the value has a non-null result signature. Literal closures keep this distinction when stored in a list or context. The observable signature comes from kind-only analysis in the written environment and stays fixed across analysis tiers, call specialization and optimization (D-219). Full analysis makes this additional bounded pass only when the expression contains function literals. Each pass retains the callable reanalysis budgets described in section 5.5. Private AST occurrence keys distinguish functions independently of their spans, so embedded trees with coincident spans do not share signatures.

For v: Any bound to 5, (if v instance of number then (function() v) else (function() 1)) instance of function<> -> number is false in both tiers: the selected closure's written result signature is Any. Calling that closure still returns 5; full analysis can keep its numeric call result. Runtime signature inspection, callback acceptance and result-check removal must not substitute that call fact for the observable arrow.

The guarded-recursion contract also applies to scope-declared functions and function values. Structural recursive call bounds are not observable signature proofs. When runtime signatures overlap, their possible results remain alternatives; projection does not turn each signature's result into a simultaneous call guarantee.

Public projection preserves a parameter's outer non-null mark and checks that the projected domain is within the original domain. If that check cannot be established, the whole function projects to Any. Union.erase_sets/1 follows the same variance rule: a parameter that would become broader makes the arrow fall back to the internal :function kind; result refinements can be widened normally.

4. The internal type against the lattice

The conversion loses information in both directions, which is why the union is for inference and the specification's type for everything else. Going out, to_spec([:number, :string]) is :any, and to_spec([:number]) is :number, which in the lattice also includes null. Going in, from_spec(:number) is [:number, :null], a null that may not be there.

A declaration has a specified meaning independent of the code translating it. Analysis facts may approximate that meaning, but their direction depends on the consumer. Neither the declaration implementation nor the inferred union is correct merely because its own membership and normalization procedures agree.

5. What the analyzer does with the types

5.1 Inference

Feel.Analysis.Inference types each operation by typing every pair of alternatives, one from each operand, and joining the results. [:number, :null] + [:number] is the pair number + number (number, or null on overflow) and the pair null + number (null). For numbers the operation runs on the sets: Feel.Analysis.Intervals gives the interval of what + - * / can produce, and says whether null is possible for lack of range (overflow past decimal128, a zero divisor, a result too small to write). The ends of a result are computed by the runtime's own arithmetic, so the rounding to 34 digits is the run's, and the ends are always included, which can only make a set larger.

The same expressions for names that are plain numbers, and for names whose scope declares allowed values (age in [0..150], d in [1..10]):

The last row shows the hole at zero that the divisor's set leaves (the bounds are abbreviated here: they are -max, 1.000…E-6143 with 34 digits, and max), and that a divisor whose set does not contain zero adds no Null of its own. The \| Null that remains is the name's: a bound d may be null.

An operand that has no order (a boolean, a list, a range, a context, a function, or a term that is no value of FEEL) is null for the four orderings whatever the other operand is, and so against Any, Any | Null and a named type (D-196): the run takes a pair of one such kind as an error, a pair of kinds that differ as a mismatch, and a null as null, so true < v and true <= v are Null (a mismatch, with a warning) for every v. The pairs are typed one by one, as ever, so a union is Null only if every pair of its alternatives is (number | boolean against Any is boolean | Null: the number can be above or below). OrderingKindsTest checks this against the runtime's table for every pair of kinds. The supported interpretation follows the domain table rather than using the alternative formula a <= b as a < b or a = b outside the ordered kinds. That formula would make true <= true true; both runtime and inference instead give null (D-196).

An operand of a kind that an arithmetic operator has no operation for is null whatever the other operand is, Any, Any | Null and a named type included (D-203), for the same reason: the run takes a pair with it as a type mismatch (and a null as null), so true + v, {a: 1} * v and [1] - v are Null (a mismatch, with a warning) for every v. A boolean, a list, a range, a context, a function and a term that is no value of FEEL have no operation at all; a string has + and no other ("a" - v is Null, "a" + v is string | Null: the v that is a string); a date, a time and a date and time have + and - (d * v is Null); a duration has all but **; only a number has **. The kinds are what the runtime's table says, and ArithmeticKindsTest checks the types against it for every pair of kinds. A union is Null only if every pair of its alternatives is.

A kind that has an operation against one that is not known (D-203) is a value of the kinds that its pairs give with a kind of the unknown one, and null: the unknown one is a value of every kind, and the run gives a value for the pairs of kinds that the tables name only. So x + v is number | Null (a number is added to a number only), s + v is string | Null, d + v is date | Null, ym + v is date | date and time | years and months duration | Null (a years and months duration is added to a date, a date and time and a years and months duration), dd / v is number | days and time duration | Null, x * v is number | years and months duration | days and time duration | Null, and v + w is the seven kinds that have a +, and Null (v - w has six of them, v * w and v / w three, v ** w one). The type is the union over the kinds of the unknown one of what the pair of the two kinds gives, so it is never narrower than the run, and no wider than the kinds say; the set of values of the known operand does not cut it (x in [0..10] makes x + v the same number | Null).

A negation has one operand, so no other to say what v is, and the run negates a number and the two durations only (D-207): -v is number | years and months duration | days and time duration | Null, the kinds of a negation (a string, a date, a time and a date and time have none: -s is Null, as ever). One v read twice (below) is one value of one kind, and the run gives for a value against itself v + v a number, a string, a years and months duration or a days and time duration (two dates are not added), v - v a 0 of a number, of a years and months duration or of a days and time duration (a date, a time and a date and time minus themselves are a days and time duration), v * v a number (a duration times itself is not defined), v / v a number (a duration over itself is one), and v ** v a number, and null: it is the union over the kinds of the pair of that kind with itself, and not of the pairs of two kinds (v - w has the six kinds, for a date and a duration are a pair).

In full analysis, the pairs are of two values unless the operands are one value (D-170): a name read twice, a member of one, a local. age - age is 0, not the difference of two numbers of [0..150], d / d is 1 (and null for a d that is 0), age * age is not below 0, and age + age is 2 * age (a set with a gap in it does not add its intervals to each other):

For ym / ym, a non-null duration gives one only when its month count is nonzero and has magnitude less than 10^34. Larger magnitudes fail the runtime's numeric conversion, even though the formal quotient would be one. Inference keeps null for that failure and for zero; if every possible month count fails, the result type is Null. A non-null declaration alone does not eliminate those failures.

A duration with a set of values added to itself is twice a value of the set, as x + x is for a number: a duration that can be either one or six months gives two or twelve months for ym + ym, not also seven, and the seconds are the same (D-207). The core analysis tier keeps independent-operand types for repeated reads.

Unary-test lowering uses inferred kinds only when that preserves dynamic matching's meaning. A nullable scalar expression that reads ? keeps a null result as an unknown answer, so -? and if b then -? else [], with b true, both remain unsatisfied on null input with the original arithmetic diagnostic. A null literal and explicit ? = null keep ordinary equality (D-40, D-209). Inferred precision must not change which null rule applies.

The same holds for the orderings and for a declared context (D-170): a number, a string, a date, a time, a date and time or a duration is neither less than itself nor greater, and is less or equal and greater or equal, and an ordering with a null is null, so age < age is false or null, and k < k for a number! is false. A context is equal to itself whatever its entries are, an open one (a declared type) included, since the run answers true for a context that is the same term before it looks at an entry (D-168). A boolean, a list or a range has no order (b < b is a mismatch, as ever), and Any is not known to be a value of FEEL (v < v is boolean | Null).

A relation between two names is held by the bounds only: age that allows <= max age is cut by the highest max age there is, where the test reads max age as it is verified, so that the type of max age is true of what the test sees (D-170).

5.2 Why a result can be null

The analysis tries to explain a possible Null by finding operands that cause it (D-161). This search is bounded and incomplete; a remaining Null need not have a discovered witness. Take three names declared number!: a price p of at most two decimals in [0..1000] (? >= 0 and ? <= 1000 and round half up(?, 2) = ?), a whole quantity q in [1..99] (floor(?) = ?), and an r in [0..1000] with any number of decimals. p * q is number in [0..99000], with no Null, and p * r is not:

p * q    number in [0..99000]
p * r    number in [0..1000000] | Null
  info operand_near_zero: the result can be null: a result too small to write when p = 0.5 and r = 1E-6176
  hint: allowed values that keep p and r away from zero rule that out, for example a lower bound of 0.001

The info is given for an operation whose operands cannot be null themselves (a name that may be null has the Null of its own, and says nothing more), and its code says what would rule the null out (D-161): :operand_near_zero, :operand_too_large, :operand_unbounded, or :null_possible for the rest. The reasons are found by running the operation. Feel.Analysis.NullReasons takes the values at which an operation fails (Feel.Type.Witness.edges/2: zero, the smallest numbers there are, the ends of the sets, the largest number, the first and last day of the calendar), runs it on every pair, and keeps the first pair the run turns down for each cause:

So a reason is a fact and not a guess: the pair is in the types of the operands and the run says null for it. A call of a built-in is searched in the same way (NullReasons.find_call/3, the code :null_possible, the function in details.function): the function is run on up to 256 combinations of edge values for a call, and 20,000 in an analysis. The search is sound and not complete (a cause whose values are not at an edge is missed); it also tests the sets from the other side, since a set that says null where no pair of edges does it is not exact there.

What takes the Null of a product away in the example is the grain of a number (D-161, step D): every number of a node is a multiple of 10^-d. A literal has its decimals, a name has the grain its allowed values say (round half up(?, 2) = ? is 2, floor(?) = ? is 0, modulo(?, 5) = 0, even(?)), a sum has the larger of its operands' grains, a product their sum, and floor, ceiling, round *, decimal, count and string length give theirs. A number of a grain is zero or at a distance of 10^-d from it at least, so a product of two with grains that add up to 6176 or less is never too small to write. The grain is a fact of the node and not a part of the type, as the length of a list is (D-193): a set of the multiples of a step is not an interval.

5.3 Narrowing

To inspect a bound, read the typed IR, rather than projecting it through the public FEEL type:

scope = Feel.Scope.new(%{"x" => :number})
{:ok, expression} = Feel.prepare("if x > 5 then x else 0", scope: scope)
Feel.type(expression) #=> :number
expression |> Feel.Expression.unoptimized_ir() |> Feel.IR.type() |> Feel.Type.Union.format()
#=> "number in 0, (5..max]"

The tables in the narrowing catalog use full analysis and enforcing declarations. Core analysis keeps broader bounds; runtime outcomes still follow the same contract. Preparation warnings describe inferred types and need not be identical between tiers. Runtime diagnostics and observable function signatures are covered by the separate tier-stability contract (D-219).

Feel.Analysis.Narrowing reads what a condition says about the names in it (D-194); narrowing.md has the rules, and a page for each kind of value. A fact is a function from the type of a name to the alternatives that are left, and it only ever takes alternatives away or makes a set smaller. After x > 5 is true, x is a number above 5 and not null; after y != 0, y is not 0. Facts come from comparisons, between, in, instance of, a name that is a whole condition, and and / or, which meet and join the facts as the logic does. They hold in the branches of an if, in the right operand of an and or an or, and for a path (p.age) and for a local (D-65, D-193).

x > 5 and x < 3                            boolean = false | Null          x < 3 is read with x above 5
if x > 5 then x else 0                     number in 0, (5..max]           the then-branch above 5, the else a point
if x != 0 then x else null                 number in [-max..0), (0..max] | Null
if s != "a" then s else null               string except "a" | Null
if n != 5 then n else null                 number in [0..5), (5..10] | Null          n allowed in [0..10]
if v instance of number then v else 0      number                          v is Any; a null is not a number
if x != null then x + 1 else 0             number                          never null: x + 1 cannot overflow
if x between 1 and 10 then x else null     number in [1..10] | Null
if p.age > 18 then p else null             context<age: number in (18..max], name: string | Null> | Null

The last line is the narrowing of a path: the fact is about p.age, and it shows up in the type of the context p. A comparison of an operation is read backwards by Feel.Analysis.Preimage (D-122): x + 1 > 5 leaves x above 4, and n + m > 150 for m in [0..100] leaves n above 50.

A comparison of a call of a built-in leaves, for an argument of type Any, the kinds for which the rule of the call gives a value of the kind the other side has, taken kind by kind with a function and a term that is not a value of FEEL among them (D-155): a list function makes a list of any value, so append(v) != null leaves Any, a function too, and a type that left it out was a check the optimizer then took away.

A condition that is decided removes a branch. A branch in which a read finds that the facts leave its name no value is out of the type of the if (D-152), and gets an unreachable_branch warning with the span of the branch (D-173; if floor(x) = 2.5 then x else 7 is number = 7); a condition whose own type is decided gets a decided_condition warning, which says it for the condition, so the two never say the same branch. Neither is said for a constant condition (if true), which is how a branch is switched off. A branch that is taken out cannot run, so every node in it is Never (D-173), and not the type it was given under facts that no run has. The body of a for, some or every over a list that is known to have no element never runs either, and its nodes are Never (D-170, every i in [] satisfies i > 2), and so are the domains after a domain that has none, which a loop does not read (D-170, for i in [], j in null return j is the empty list):

if x < 4 then (if x > 5 then x + 1 else 0) else 1        number in 0, 1
  if x > 5 then x + 1 else 0                              number = 0
    x > 5                                                 boolean = false      x is number in [-max..4) here
    x + 1                                                 Never                and so are x and 1 in it
    0                                                     number = 0

The branches:

if n > 10 then 1 else 2            number = 2        warning: the condition is never true; the then branch never runs     (n in [0..10])
if v instance of list<number> then 1 else v     Any except list<number | Null> | Null          (v is Any; the else is a kind less some of it, 3.5)

A branch that reads none of the names its facts are about stays in the type, unless its condition compares a call of a rounding function, exp or log (if floor(x) = 2.5 then 5 else 7 is number = 7, D-194): applying the facts at every if costs 20 to 65 per cent at the least, and the comparisons that the facts say more of than the types are those of such a call.

The shape of the algorithm is the shape of abstract interpretation: sets of numbers are an interval domain, the arithmetic of Intervals is its transfer function, the cap of 16 intervals is a widening, and Preimage is the backward transfer function used to refine a condition. One place does it by the book. In for i in 0..4 return if i = 0 then 1 else i * partial[-1], the type of partial (the results so far) depends on the type of the body, which depends on partial, so the analyzer iterates to a fixpoint: it starts from a list of nothing, types the body, takes what the body can be into partial, and types again until the body is within it. From the second round on the sets of values are given up, because i * partial[-1] never stops growing, and after the third round the results are Any (partial_fixpoint and widen in analyzer.ex).

5.4 Declarations: what a scope says

A Feel.Scope gives the names their types and says what a bound value has to satisfy. An allowed value is the source of a list of unary tests, as in the allowedValues of a DMN item definition, and a type constraint the same for the value as a whole (for a list, count(?) > 0 is for the list, where allowed values are for each element, D-51). A unary test is a condition of ?, so a constraint narrows by the rules of the narrowing pages (D-161, step A): ? * 2 < 100 as an allowed value narrows as x * 2 < 100 does in a condition. Both can be given for a member of a value by a subject {name, steps}, where a step is a key of a context or :each for the elements of a list (D-161, step E), and a source may be a list of texts that all hold:

scope = Feel.Scope.new(
  %{"person" => {:context, %{"age" => :number, "name" => :string}},
    "orders" => {:list, {:context, %{"total" => :number}}},
    "grid" => {:list, {:list, :number}}, "xs" => {:list, :number}},
  allowed_values: %{
    {"person", ["age"]} => "[0..150]",
    {"orders", [:each, "total"]} => "[0..1000]",
    {"grid", [:each]} => "> 0"},
  type_constraints: %{"xs" => "count(?) > 0"})

The run makes the types true (D-138): when it starts it checks the bound value of each name the expression reads, and a value that a test does not accept is null with a :value_not_allowed error, null itself being exempt. For a member the first one that is not allowed makes the whole value null, and the error says which: the value of "orders[3].total" is not one of its allowed values. A name declared ! ends the run instead. What a run does with a value that does not fit, and whether the constraints narrow the types, is the stance (:declarations, D-138; section 6). Feel.ItemDefinitions.scope/2 makes a scope from the item definitions of a model, with the constraints of each definition, of its components and of a collection's elements.

The declared type of a name may be a negation or a union (section 2, D-178). The stances treat it as any other: :enforce and :enforce_wide convert the bound value or make it null with a :type_mismatch, :audit and :report leave it and report it, :trust and :ignore rely on the host. With x declared Any except number, x + 1 is Null with a type_mismatch warning, where Any gave Any | Null, and if x instance of string then x else null is string | Null; with u declared number | string, u + 1 is number | Null and if u instance of number then u + 1 else 0 is number. The allowed values of such a name are enforced and do not narrow it (5.7).

5.5 Calls: built-in functions and functions of FEEL

A call of a built-in function starts with the type its signatures give (result kinds and Null), refined by a result rule (D-161, step C): Feel.Analysis.Images has a module for each family (booleans, contexts, conversions, lists, numbers, ranges, strings, temporal values), each registered built-in has a rule, and each rule is held to the run on the values at the edges of the types of its arguments (Feel.ImageCheck). These tests check containment and selected null witnesses on the exercised inputs; they do not establish exact result sets for every argument combination.

string length(s)                       number in 3, 4, 5 | Null          s allows "red", "green", "blue"
upper case(s)                          string in {"BLUE", "GREEN", "RED"} | Null
not(b)                                 boolean                            b is boolean!
abs(k)                                 number in [0..5]                   k is number! in [-5..3]
date("2024-05-01") + duration("P1D")   date = 2024-05-02

A comparison of a call narrows its arguments by their kinds, for every built-in with a rule: string length(s) > 0 leaves the strings but "" (if string length(s) > 0 then s else null is string except "" | Null for a s that has no allowed values, and for a v of Any the same with the lists: string except "" | list<Any | Null> | Null).

A function of FEEL has a type: function(a: number, b: number) a + b is function<number | Null, number | Null> -> number | Null. A call of one written in the expression, called at once or through the key of a context, is typed by analyzing its body again with the types of the arguments (D-193), so (function(a: number, b: number) a + b)(n, 1) for n in [0..10] is number in [1..11] | Null. That goes no deeper than three calls, and a call that repeats an earlier one has its type. A name declared with a function type is typed by its arrow, which knows nothing of the sets (f(n) for f: function<number> -> number is number | Null). A call with another number of arguments is Null with an arity_mismatch warning when the actual function values are known from syntax or the built-in registry; through a function or overload type alone it starts at Any | Null, since recorded arrows may omit signatures (ceiling takes a scale, D-171). The same applies when recorded arrows have the right arity but do not cover every argument's domain: another same-arity signature can succeed. Applicable call refinements can still narrow the result. Linked recursion carries separate single-signature callee evidence. Members are prepared again with their original settings before link signatures are probed; only the peer bindings constructed by Feel.Recursion receive this evidence, and local shadowing does not inherit it. Thus a self-call with an Any argument can keep its declared numeric result without treating a host extension's partial signature list as complete. Completeness is a fallback beside closure identities: discovery through contexts, list indexes, conditionals and iterator domains still specializes known literal bodies for their arguments. Forwarded containers prefer their retained shapes over compact completeness. Named calls of complete peers keep the written result or Null when they supply at most the parameter count; more names give Null. Omitted parameters can be null, while unknown or duplicate names still fail runtime binding. Names are not inferred from the arrow type. Context-entry containers retain completeness before aliases are bound, even when their detailed shapes exceed the 32-entry limit. If a known literal cannot be specialized because the three-call depth or source budget is exhausted, its marked complete signature still bounds the call. This uses its written result and possible null, without further specialization or treating an ordinary host declaration as complete. Descendant selection preserves this evidence when every function contained in the source is known complete: ({g: f}...g)[1](n - 1, v) retains a linked peer's result bound just as an ordinary path does. Partial host functions and unknown containers do not acquire completeness from their declared arrow types. A function that a call gives and that its body writes is the overload of the arrow as it was written, with the arrow typed for the arguments of the call as a refinement (D-171). Literal functions use this signature/refinement separation from their first analysis; the check-bypass example is kept as a regression. A built-in function with several observable signatures, used as a value, is an overload (3.5; not, count and upper case are plain function types). abs does not itself satisfy function<number> -> number, but declaration conversion can select its numeric signature and produce a function enforcing that contract (D-197). For a call without that conversion: (function(h: function<Any> -> Any, ys: list<number>) for x in ys return h(x))(abs, xs) is list<number in [0..max] | Null> | Null, since abs has a refinement for numbers (the other overloads, such as floor, give list<Any | Null> | Null there). Returned containers can still lose built-in call summaries, so {fs: (function() [abs, floor])(), r: fs[1](n)}.r is Any | Null. This is separate from keeping literal FEEL closures' signature/call distinction inside their types. A written list or context bound to a name also keeps known functions beside its type (D-193). There are no type variables, and a function written in FEEL has no declared result type.

A returned list or context still does not preserve every nested callable shape. For a newly created function inside such a container, call analysis restores the written parameters and an Any | Null result. Matching an arrow in an argument or unrelated entry is not proof of identity. It must not export a specialized body arrow as observable metadata (D-203). Nested overload arrows participate in this fallback too. Callable precision beyond the retained shapes remains open work.

Named calls through function types are Any | Null, since parameter names and the complete signature list are absent. Known function values still use their own binding rules. Callee identities passed to a parameter are retained only when conversion cannot replace the function: restricting abs to its numeric signature changes which calls it accepts. Specialized closure arrows are call facts; equality with an argument's arrow does not prove that the same function was returned. Alternative returned function signatures remain a union; combining them into an overload would incorrectly require every signature. Ambiguous alternatives keep their broader written types. Section 2.7 states the reader rules and the conservative precision tradeoffs.

A callee that says which function it is is not typed by its type but by the functions (D-193). The node of the callee is a key of a context literal, an item of a list literal or a branch of an if, and it is read (Feel.Analysis.Callees): each function literal in it is analyzed again for the arguments as one written at the call is (D-193), each built-in function is typed as its call by name would be (the rule of its family, above), and the call is any of them, null too where the callee or an argument may not fit. So {g: function(a) a * 2}.g(x) and [abs, floor][1](x) are number | Null (they were Any | Null), (if b then abs else ceiling)(age) is number in [0..150] | Null for an age in [0..150] (it was number | Null), and (if b then function(a) a * 2 else function(a) a + 1)(3) is number in 4, 6. At most 4 alternatives are read, and 64 KiB of function source are analyzed again for them in one analysis; past either the call is typed by the type of its callee.

A name keeps the functions too (D-193). The analysis keeps what it knows of a list or a context that a name is bound to beside its type, in the shapes of its structure (D-193: the shape of each item and of each entry), and the shape has the functions that the node of the item or entry says (callees). So {fs: [abs, floor], r: fs[1](x)}.r, {c: {g: function(a) a * 2}, r: c.g(x)}.r and fs[1].g(3) for a list of contexts are read from the name as they are at the call, four deep; the iterator of a for, some or every over a list of functions is any of them (for f in [abs, floor] return f(x) is list<number | Null>), and a parameter that a call gives an if, an item or a key of functions is any of them ((function(f: function<Any> -> Any, y) f(y))(if b then abs else ceiling, x) is number | Null; it was Any | Null). The shape is not part of a type, so the functions are not lost to D-152.

A call that gives a function says which (D-193): the body of a function that is analyzed again for a call says what it gives when it is a function written in it, an if of them, a name that has them or a call that gives them, and the node of the call keeps it beside its type (callees). So {g: function(a) function(c) a + c}.g(1)(2) is number = 3 through a key, a list item, an if, a name or a parameter, as (function(a) function(c) a + c)(1)(2) was, and a call that gives a value that may not be a function is typed by its type. A list or a context literal that is selected from more than once ({fs: [abs, floor]}.fs[1](x)) and a parameter that is given a list or a context of functions ((function(fs) fs[1](x))([abs, floor])) are read as a name that holds the value is.

5.6 What the types are used for

Diagnostics, for what is certain. An operation is a :type_mismatch warning at prepare/2 only when every pair of alternatives without a null operand is a mismatch. A null operand excuses a pair, and a mismatch that only some pairs have is not reported.

Preparation warnings and runtime diagnostics serve different purposes. A statically impossible built-in call is typed as Null and may warn using the inferred argument types. It keeps ordinary runtime validation, whose error message and details describe the actual values. They agree across analysis tiers, including in strict mode. Structural call errors such as invalid arity instead carry a fixed diagnostic in the IR. Preparation warnings themselves are allowed to differ across tiers.

The optimizer (D-45) removes a runtime check when the type has already settled it. The scope's declarations become wrapper nodes around the expression (allowed, conform, ...); after optimizing, the ones that the types prove are gone:

Folding. A pure operation on constants is evaluated, and full analysis can keep its exact value (number = 3), so most constant sub-expressions fold away before a backend sees them.

Decision tables. Feel.Rules asks of a table whose entries are unary tests whether the rules cover the inputs, overlap, or are dead, and the interface distinguishes proved, refuted with an input, and unknown (Feel.Type.Verdict, D-158). A rule is bounded from outside by the inputs it may match and from inside by the inputs it certainly matches, both as types, and a column has the type of its input (one narrowed by its allowed values, for instance). Numeric certainty keeps bounded subsets instead of filling gaps; string certainty drops information at its point budget. The former 17-point false coverage, overlap and deadness claims are now regression tests. Unsupported proofs may remain unknown; witnesses are not yet universally checked against the original unary tests. DMN adapts prepared wildcard entries to their effective inputValues, and keeps cells depending on model/local bindings, filter fields, aliases, dynamic lookup, extensions or indirect calls unknown. The original unit's named types are preserved through the queries' optional types: map, including resolved or folded instance of tests. Standalone Feel.Rules callers must supply those type definitions and effective tests or explicit :unknown cells; that API cannot reconstruct a DMN or lexical scope from text. See DMN's table-checking contract.

For a standalone proof using a named type, supply its definitions explicitly:

columns = [{"x", Feel.Type.Union.of_value(Decimal.new(1))}]
rules = [["if 1 instance of N then 1 else 2"]]
Feel.Rules.coverage(columns, rules, types: %{"N" => :number}) #=> :covered

These diagnostics concern the supplied abstract column domains, not reachability through upstream model decisions. Silence is not a coverage or disjointness proof: a query can be unknown, skipped for table size, or contained by its time/memory guard. Rule-output narrowing is a separate consumer that analyzes an output assuming its entry matched; unknown table proofs do not justify eliminating that output or its runtime checks.

String alternatives are combined with bulk union, and negated lists with bulk intersection, before applying the lower-bound point/exclusion budget. Intervals do not count toward that budget; a fold over a growing interval set would repeat sorting and intersection work without reaching the cap. Scaling regressions measure process reductions on positive and negated lists of disjoint intervals.

The audit. Feel.Paranoid.run/3 (D-159) runs the IR as the analyzer made it, with nothing taken out, and checks for every node that its value is in its type with Union.contains?/2; it also compares optimized execution. Result and error comparisons include every diagnostic field, in order, using recursive value equality for embedded decimals, contexts and functions. FEEL functions compare by signature metadata with their implementation closures ignored; equal metadata does not establish equal behavior. A shared membership bug can still escape the monitor.

The types therefore change what runs. An unsound type in this library is not a missed warning: it is a check that was removed and should not have been. This is why the correctness assessment distinguishes precision losses from invalid proofs and execution changes.

5.7 Current limits

The assessment distinguishes the contracts that are kept from remaining precision and verification work. Nested normalization, observable signatures, parameter projection and certainty construction now preserve the contracts described above. This does not complete the audit of every proof consumer, aggregation path, declaration assumption or observable effect.

The analysis also deliberately loses information: it has no general polymorphic type schemes or relational solver; cardinality, grain, temporal inverse rules and callable summaries are partial and bounded. Host declarations can express unions and negations that expression syntax cannot write. Non-null result constraints are rejected. Recursive item definitions default to rejection. The explicit recursive: :guarded mode keeps a finite graph and validates every finite descendant and component constraint. Cycles must consume a context member or list element and cannot cross a function signature. Analysis uses a structural upper approximation with a shared 256-node projection budget, which cannot justify recursive check removal or subtraction from a negative branch. Complete recursive subtyping and inference remain unsupported. The legacy recursive: :any mode is still explicitly approximate and does not validate the full recursive structure.

Use the narrowing catalog for concrete precision cases and the maintained backlog for open work. The decision record explains current choices; Git keeps earlier limits and implementation stages.

6. Keeping it sound

Under valid assumptions, an inferred possible-result type must contain every returned value. Making such a positive bound larger sacrifices precision. The same direction does not apply unchanged to certain rule inputs, negative positions or observable effects. The assessment states the obligations and lists the remaining audit work.

Representation budgets bound selected work: numeric/temporal intervals, finite strings, structural exclusions, overloads and callable reanalysis all have caps. Replacing a positive bound by its hull can be safe locally while complementing that hull is unsafe. Shrinking a fact alone does not prove it valid, and failure of subtype? can mean the algorithm could not establish inclusion.

The test evidence comes from complementary checks:

The sweeps share membership code with the analyzer; that limits their independence. Mutation checks probe selected blind spots, but neither passing tests nor unchanged precision establishes a theorem. The open obligations gives stronger acceptance criteria, including independent oracles and cap/variance boundary tests.

Declaration assumptions also matter. With :enforce, the runtime checks declarations and converts or rejects invalid bindings through the declared conformance/conversion boundary. :trust and :audit narrow without enforcing, so the host must supply valid values for those inferences to hold. :enforce_wide checks without allowed-value narrowing; :report and :ignore do not narrow by allowed values, but still assume declared kinds. An optimization justified by an unchecked assumption inherits that assumption.

7. Where to read more