# Type narrowing

Narrowing is how the analyzer uses what a condition says. In `if x > 5 then x else 0` the `x` that is returned is not the declared `number | Null`: the condition was true, so it is a number above 5. Every read of a name is analyzed under the facts available in its branch. Narrowing improves result bounds, supports warnings about fixed conditions, and lets the optimizer remove checks. It therefore has consequences for execution, even though the runtime does not apply the facts itself. The [assessment](type-system-analysis.md#2-contracts-and-evidence) states the contracts and the remaining audit work; the rules and tested examples below do not establish general soundness.

This page has the general rules. Each type has a page of its own with the conditions that narrow it and what they leave ([the index](#12-the-pages)), and [overloaded functions](narrowing/overloaded-functions.md) says how narrowed arguments meet functions with several signatures. [type-system.md](type-system.md) explains the types that are narrowed, and [architecture.md](architecture.md) where the code sits.

| Expression | Type | Warnings |
| --- | --- | --- |
| `if x > 5 then x else 0` | `number in 0, (5..max]` | — |
| `if x != null then x + 1 else 0` | `number` | — |
| `if v instance of number then v else 0` | `number` | — |
| `x > 5 and x < 3` | `boolean = false \| Null` | `decided_condition` |
| `if n > 10 then 1 else 2` | `number = 2` | `decided_condition` |

Contents: [1 Vocabulary](#1-vocabulary) · [2 The names in the examples](#2-the-names-in-the-examples) · [3 What gives a fact](#3-what-gives-a-fact) · [4 Then, else and null](#4-then-else-and-null) · [5 And and or](#5-and-and-or) · [6 Where facts apply](#6-where-facts-apply) · [7 What it changes](#7-what-it-changes) · [8 What gives no fact](#8-what-gives-no-fact) · [9 Limits](#9-limits) · [10 Correctness obligations and checks](#10-correctness-obligations-and-checks) · [11 The code](#11-the-code) · [12 The pages](#12-the-pages) · [13 Does it narrow as far as it can?](#13-does-it-narrow-as-far-as-it-can)

## 1. Vocabulary

- **Subject.** What a fact is about: a name (`x`), a path that starts at a name (`p.age`), a local, which is a parameter of a function, an iterator, or an entry of a context, identified by the depth of the context that binds it, so that a name bound again deeper takes no fact (D-193), and in the brackets of a filter the element (`item`) or one of its entries.
- **Fact.** A function from the type of a subject to the alternatives of it that are left. A fact only takes alternatives away or makes a set of values smaller. It must preserve every value the subject can have in that branch; shrinking alone does not establish this obligation. A fact that leaves nothing says that the branch cannot be taken: a read of the subject there keeps the type it had, since any type will do, and the `if` leaves the branch out of its type and says that it never runs (section 7, D-152, D-173).
- **Branch.** `then` is where the condition was `true`. `else` is where it was not: `false`, `null`, or a value that is no boolean, since `if` takes the else branch for anything but `true` (Table 50). That asymmetry is the source of most of what follows: the not-true branch is rarely as informative as the true one.

Facts compose by the logic around them, and they stack: a read inside a branch has the facts of every condition that encloses it, and the facts of the same subject are applied one after the other.

## 2. The names in the examples

The tables are checked against the analyzer using this scope (`Feel.Sweep.scope/0`). Expression rows compare the prepared root types (with default optimization) and warning codes; condition rows inspect the subject in the unoptimized branch IR. Constant folding can make a root type more precise. This is distinct from checking every possible runtime binding. A name has its declared type, with `null` added, as for every name that is bound from outside (`x` is `number | Null`); allowed values narrow the type of the name when the run enforces them (D-138), as in `n`. An allowed value is a unary test, which is a condition of `?`, and narrows by the rules of these pages (D-161): `? * 2 < 100` as an allowed value narrows as `x * 2 < 100` does in a condition.

| Name | Declared as |
| --- | --- |
| `x`, `y` | `number` |
| `k` | `number!`, a number that is never `null` (D-48) |
| `n` | `number` with the allowed values `[0..10]` |
| `age` | `number` with the allowed values `[0..150]` |
| `s`, `s2` | `string` |
| `b`, `b2` | `boolean` |
| `d`, `dr` | `date`; `dr` allows `[@"2020-01-01"..@"2022-12-31"]` |
| `dt`, `dtr` | `date and time`; `dtr` allows `[@"2024-01-01T00:00:00"..@"2024-01-31T23:59:59"]` |
| `tm`, `tmr` | `time`; `tmr` allows `[@"08:00:00"..@"18:00:00"]` |
| `ym`, `yms` | `years and months duration`; `yms` allows `[@"P0M"..@"P5Y"]` |
| `dd`, `dds` | `days and time duration`; `dds` allows `[@"PT0S"..@"P3D"]` |
| `xs`, `ys` | `list<number>`, `list<string>` |
| `ps` | `list<context<age: number, name: string>>` |
| `q` | `context<age: number, name: string>` with the allowed values `[0..150]` for `age` |
| `qs` | `list<context<age: number, name: string>>` with the allowed values `[0..150]` for the `age` of each |
| `ls` | `list<list<number>>` with the allowed values `> 0` for the numbers, and the type constraint `count(?) <= 2` for the inner lists |
| `ws` | `list<number>` with the type constraint `count(?) > 0` |
| `top` | `number` with the allowed values `[18..65]` |
| `capped` | `number` with the allowed values `<= top`, which mention another name (D-170) |
| `emp` | `context<age: number, limit: number>` with the allowed values `<= emp.limit` for the `age` and `[0..65]` for the `limit` |
| `r` | `range<number>` |
| `p` | `context<age: number, name: string>` |
| `f` | `function<number> -> number` |
| `v` | `Any` |
| `m` | `Person`, a model-defined type: `context<age: number, name: string>` |

A type is written as `Feel.Type.Union.format/1` writes it: `number in [0..150] | Null` is a number from 0 to 150, or `null`; `-max` and `max` are the ends of decimal128; `string except "a"` is every string but one. Where a table says **—** for a branch, the branch cannot be taken.

The tables use the defaults `analysis: :full` and `declarations: :enforce`. The core tier keeps kind information but does not apply these set-valued facts. It preserves the same runtime values and diagnostics for supported settings; observable function signatures are captured independently of the extra full-tier precision. Preparation warnings can still describe different inferred bounds. `:trust` and `:audit` require full analysis.

Declaration stance also changes the assumptions behind the tables. `:enforce_wide` checks values without narrowing by allowed values. `:trust` and `:audit` use allowed values without repairing invalid bindings; the host must satisfy those assumptions. `:report` and `:ignore` do not narrow by allowed values, but still assume declared kinds. Non-null input declarations lose their null alternative only in the enforcing stances. See [declarations](type-system.md#54-declarations-what-a-scope-says) and `Feel.Analysis.Declarations` for the full contract.

## 3. What gives a fact

A condition gives facts about the subjects it reads, in the shapes below, and nothing else does (section 8). Each is read for three outcomes of the condition, and not for two ([5](#5-and-and-or)).

| Condition | Says | Pages |
| --- | --- | --- |
| a subject that is the whole condition (`b`) | `true` in `then`, anything else in `else` | [boolean](narrowing/boolean.md) |
| `= != < <= > >=` of a subject with any expression, on either side (`5 < x` is `x > 5`) | the values for which the comparison can be true, or can be false | every kind |
| `between` | the two comparisons of `value >= low and value <= high` (D-69) | [number](narrowing/number.md), [date](narrowing/date.md) |
| `subject in tests` | the tests are conditions of the input `?`: joined in `then`, met in `else` (D-61, D-194) | [number](narrowing/number.md), [string](narrowing/string.md) |
| `subject instance of T` | in `then`, what is in both the type and `T`, and never `null` unless `T` is `Null`; in `else`, the type less `T`: what is not wholly within `T`, and `null`, and for a name of type `Any` the kinds that `T` does not take out (D-23, D-194, D-39) | [any](narrowing/any.md), [null](narrowing/null.md) |
| `and`, `or` | the facts of the two sides, met or joined ([5](#5-and-and-or)) | |
| `not(c)` | the facts of `c` for the outcome that `not` turns over: where `c` is `false` in `then`, where it is `true` or unknown in `else` ([5](#5-and-and-or)) | [boolean](narrowing/boolean.md) |
| a condition compared with `true` or `false` (`(x > 5) = true`, `c != false`) | the facts of the condition: `c = true` is `true` where `c` is, and `false` for everything else, `null` included | [boolean](narrowing/boolean.md) |
| an arithmetic operation or a negation in a comparison (`x + 1 > 5`) | in `then`, its operands are not `null`, and are the numbers that give such a result (D-194, D-122); in `else`, the numbers that give a result it is `false` for, and `null`, where the operation cannot be `null` for the operand | [number](narrowing/number.md), [durations](narrowing/days-and-time-duration.md) |
| a call of a number function in a comparison (`abs(x) < 100`, `floor(x) = 3`, `sqrt(x) < 10`) | in `then`, its arguments are not `null`, and are the numbers that give such a result (D-161); in `else`, as for an operation | [number functions](narrowing/number-functions.md) |
| a call of any other built-in in a comparison (`string length(s) > 0`, `day of week(d) = "Monday"`, `sum(xs) > 5`) | its arguments are not `null` (unless the call takes one), and are of the kinds for which it gives such a result; the length of a string says whether it is the empty one (D-170). A name of type `Any` is taken kind by kind, **a function and a term that is not a value of FEEL among them**: a list function makes a list of any value, so `append(v) != null` leaves `Any` (D-155) | [any](narrowing/any.md#a-call-in-a-comparison), [string](narrowing/string.md), [list](narrowing/list.md), [date](narrowing/date.md) |
| a path (`p.age > 5`) | a fact about the path narrows the entry, and the source that has it (D-65, D-194) | [context](narrowing/context.md) |
| a property of a date, a duration, a time or a date and time (`d.year = 2024`) | narrows the set of the value (D-194, D-109) | [date](narrowing/date.md), [time](narrowing/time.md), [date and time](narrowing/date-and-time.md) |
| the element of a filter, in its brackets (`xs[item > 2]`) | narrows the elements the filter keeps (D-71) | [list](narrowing/list.md) |

How a comparison narrows a kind is specific to that kind, and is described on its page. What they all have in common is the subject of the next section.

## 4. Then, else and null

`null` is what makes the two branches unequal. An ordering with a `null` operand is `null`, and `null` is not `true`; but `null = null` is `true`, and `null != 5` is `true` (Table 50, D-04). So:

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `x > 5` | `number in (5..max]` | `number in [-max..5] \| Null` |
| `x = 5` | `number = 5` | `number in [-max..5), (5..max] \| Null` |
| `x != 5` | `number in [-max..5), (5..max] \| Null` | `number = 5` |
| `x = null` | `Null` | `number` |
| `x != null` | `number` | `Null` |

- **When an ordering is true, the subject is not `null`,** and is in the set of values for which it can be true. When it is not true, the subject can still be `null`, so the type keeps `Null`.
- **`x != 5` is true for `null`,** so `Null` stays in `then` and drops out of `else`, where the comparison is certainly `false`.
- **`x = null` and `x != null` are the guards.** `x = null` is true only for `null`, and when it is not true the subject is not `null`: that is what turns `number | Null` into `number` in `if x = null then 0 else x + 1`.
- **`else` uses the values for which the comparison is *false* only when it cannot be `null`:** the other side is of one kind and never `null`. Otherwise every value remains. That is why `x > y` says less than `x > 5`:

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `x > y` | `number in (-max..max]` | `number \| Null` |
| `x = y` | `number \| Null` | `number \| Null` |
| `x > v` | `number` | `number \| Null` |
| `x = v` | `number \| Null` | `number \| Null` |

`y` can be `null`, so `x = y` can be true for a `null` `x`, and `x > y` is read from the *bounds* of `y`'s set: `x` is above its lowest value. `v` is `Any`, so the other side's kind is not known, and a number is all that `x > v` can say. The pages of the kinds go through the same questions for their sets. [null.md](narrowing/null.md) has the whole matrix.

A value compared with **itself** is one value, and not two of the type (D-170): `x = x` is `true` for every value of FEEL, `null` included, and an ordering of a kind that has one is `false` (`<`, `>`) or `true` (`<=`, `>=`) and `null` where the value is `null`, since an ordering with a `null` is `null`. A kind without an order (`b < b`) is a mismatch as always, and `Any` is not known to be a value of FEEL.

| Expression | Type | Warnings |
| --- | --- | --- |
| `x = x` | `boolean = true` | — |
| `p = p` | `boolean = true` | — |
| `x < x` | `boolean = false \| Null` | — |
| `x >= x` | `boolean = true \| Null` | — |
| `k < k` | `boolean = false` | — |
| `d <= d` | `boolean = true \| Null` | — |
| `b < b` | `Null` | `type_mismatch` |
| `v < v` | `boolean \| Null` | — |

An operand that has **no order** (a boolean, a list, a context, a range, a function) is `null` against anything for the four orderings, and so against a name of type `Any` (D-196): `true < v` and `true <= v` are `Null` with a `type_mismatch` warning, and `if true < v then 1 else 2` is `number = 2` with a `decided_condition`. [null.md](narrowing/null.md) has the rows.

The same goes for an operand for which an arithmetic operator has **no operation** (D-203): a boolean, a list, a context, a range and a function have none of `+ - * / **`, a string only `+`, a date, a time and a date and time `+` and `-`, a duration all but `**`, and a number all. `true + v`, `[1] - v`, `s - v` and `d * v` are `Null` with a `type_mismatch` warning for every `v`, and `if true + v > 1 then 1 else 2` is `number = 2` with a `decided_condition`; `s + v` is `string | Null`, `d + v` is `date | Null` and `x + v` is `number | Null`, the kinds that their pairs give (D-203), and `-v` is `number | years and months duration | days and time duration | Null`, the kinds that a negation has (D-207), as `v - v` is `0` of a number or a duration, or `null`. [null.md](narrowing/null.md) has the rows.

## 5. And and or

| | `then` | `else` |
| --- | --- | --- |
| `a and b` | the facts of both, one after the other | a subject is narrowed only if **both** sides narrow it, to what either leaves |
| `a or b` | a subject is narrowed only if **both** sides narrow it, to what either leaves | the facts of both, one after the other |

The right operand is read knowing what the left said: the right of `a and b` is analyzed in the `then` facts of `a`, and the right of `a or b` in its `else` facts (D-194). So `x != null and x > 5` is `boolean`, never `null`, and `x = null or x > 5` is too.

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `x > 5 and x < 10` | `number in (5..10)` | `number in [-max..5], [10..max] \| Null` |
| `x < 0 or x > 10` | `number in [-max..0), (10..max]` | `number in [0..10] \| Null` |
| `x > 5 and y > 3` | `number in (5..max]` | `number \| Null` |
| `x > 5 or y > 3` | `number \| Null` | `number in [-max..5] \| Null` |

| Condition | `y` when true | `y` when not true |
| --- | --- | --- |
| `x > 5 and y > 3` | `number in (3..max]` | `number \| Null` |

A subject that only one side of an "either" narrows is not narrowed: in `x > 5 or y > 3` the second may be the one that was true, so `x` is as it was.

**Three outcomes.** `else` is where a condition was not `true`, which is two cases that `not`, `and` and `or` tell apart: it was `false`, or it was *unknown* (`null`, or a value that is no boolean; `not(5)` is `null`, and so is `5 and true`). The facts of a condition are asked for each of them (`Narrowing.facts/2`: `:then`, `:false`, `:null`, and `:else` for the two together), and a set of facts holds at least every state that has the outcome, so a shape that is not read says nothing for it. `not(c)` is `true` where `c` is `false`, `false` where `c` is `true`, and unknown where `c` is; its `else` is the other two. `a and b` is `false` where `a` is, or `b` is; unknown where `a` is and `b` is not `false`, or where `a` is `true` and `b` unknown. The right operand was read knowing what the left said (above), so what it says of the names the left narrowed holds only where the left is `true`, and the unknown cases of the left are all kept for them.

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `not(x = null)` | `number` | `Null` |
| `not(x > 5)` | `number in [-max..5]` | `number in (5..max] \| Null` |
| `not(x = 5)` | `number in [-max..5), (5..max] \| Null` | `number = 5` |
| `not(not(x > 5))` | `number in (5..max]` | `number in [-max..5] \| Null` |
| `not(x = null or y = null)` | `number` | `number \| Null` |
| `not(x != null and y != null)` | `number \| Null` | `number` |
| `(x > 5) = true` | `number in (5..max]` | `number in [-max..5] \| Null` |
| `(x > 5) != true` | `number in [-max..5] \| Null` | `number in (5..max]` |
| `(x > 5) = false` | `number in [-max..5]` | `number in (5..max] \| Null` |


**An operand that is never a boolean** leaves one outcome out (D-170). The tables of the runtime distinguish `true`, `false` and "otherwise" (`null`, or a value of any other kind): a `false` decides a conjunction and a `true` a disjunction, and otherwise the result is `null`. So `b and null` is `false` or `null` and never `true`, and `b or null` is `true` or `null` and never `false`. A name of type `Any` may be a boolean, and the same holds for it.

| Expression | Type | Warnings |
| --- | --- | --- |
| `b and null` | `boolean = false \| Null` | — |
| `b or 1` | `boolean = true \| Null` | — |
| `true and null` | `Null` | — |
| `v and "a"` | `boolean = false \| Null` | — |
| `v and false` | `boolean = false` | — |
| `v and true` | `boolean \| Null` | — |
| `if b and null then 1 else 2` | `number = 2` | `decided_condition` |

## 6. Where facts apply

A fact applies to every read in the part of the expression that it holds for, and the part is:

- the **branches of an `if`**, and every condition inside them;
- the **right operand** of `and` and of `or`, and the upper bound of `between`, and the upper comparison of a range in an `in`, which are read knowing the first part (D-194);
- the **brackets of a filter**, for the elements it keeps (D-71);
- the **body of a function** that is called where it is written or through a key, which is analyzed again with the types of the arguments and the facts that hold at the call (D-193), once for the same ones (D-193);
- the **locals**: the body of a `for`, `some` or `every`, the entries of a context, the parameters of a function.
- the **outputs of a rule of a decision table**, for the entries of the rule: the rule matched, so each of its entries was satisfied by the input of its column, and an entry `>= 18` of the input `age` is `age >= 18` in its outputs (D-195). A `not(...)` entry is the outcome `false` of the tests (D-194), a `-` is the input values of its column if it has some, and the defaults and output values of the table are not under a rule. A table has no text, so there are no rows of it in the tables of these pages; `test/feel/analysis/table_narrowing_test.exs` and the sweep of `scripts/sweep/tables.exs` cover it.

| Expression | Type | Warnings |
| --- | --- | --- |
| `if x > 5 then (if x > 8 then x else 0) else 3` | `number in 0, 3, (8..max]` | — |
| `x = null or x > 5` | `boolean` | — |
| `x != null and x > 5` | `boolean` | — |
| `for i in xs return if i > 5 then i else 0` | `list<number in 0, (5..max]> \| Null` | — |
| `{a: x, b: if a > 5 then a else 0}` | `context<a: number \| Null, b: number in 0, (5..max]>` | — |
| `(function(a: number) if a > 5 then a else 0)(x)` | `number in 0, (5..max]` | — |
| `(function(a) if a > 5 then a else 0)(v)` | `number in 0, (5..max]` | — |
| `(function(a: number) if x > 5 then a + x else a)(1)` | `number in 1, [6..max]` | — |
| `xs[item > 2]` | `list<number in (2..max]> \| Null` | — |
| `[{a: 1}, {a: 2}][a >= 2]` | `non-empty list<context<a: number = 2>>` | — |
| `{ok: x > 5, r: if ok then x else 0}.r` | `number in 0, (5..max]` | — |
| `{ok: x > 5, r: if not(ok) then x else 0}.r` | `number in [-max..5]` | — |
| `(function(c) if c then x else 0)(x > 5)` | `number in 0, (5..max]` | — |

**A name that is bound to a condition remembers it** (D-194 in [decisions.md](decisions.md#d-194-conditions-have-true-false-and-unknown-outcomes)). `ok` above holds the value that `x > 5` had, so `if ok` says of `x` what `if x > 5` does, in each outcome: `x` is above 5 where `ok` is true, and `ok` is false or unknown where `x` is at most 5 or `null`. It holds for the entries of a context, for the entries that are names of one (`{o: ok}`), and for the parameter of a function written in the expression that is called at once, or through a key, with a condition (D-193). It is the facts of the condition as they were made where the name was bound, about the names of the scope and the paths from them; those about a local of the place of the call (`for i in xs return f(i > 5)`) are not about a local of the function, so they are left out. The nodes of the body of a function are those of its analysis for any argument, so the type of the *call* is narrower and a node in the body is not.

**A name that is bound again shadows the fact.** `x` in `if x > 5 then (for x in xs return x) else null` is the iterator, not the `x` the condition read, and a fact is about the one that was read. A fact about a variable is not about a local of the same name, and a local is distinguished from another of the same name by the depth of its context.

| Expression | Type | Warnings |
| --- | --- | --- |
| `if x > 5 then (for x in xs return x) else null` | `list<number \| Null> \| Null` | — |
| `if x > 5 then (function(x: number) x)(1) else null` | `number = 1 \| Null` | — |
| `if x > 5 then {x: 1, r: x} else null` | `context<r: number = 1, x: number = 1> \| Null` | — |

Rule-output narrowing and table proofs answer different questions. The former analyzes an output under the assumption that its row matched. `Feel.Rules` separately asks about coverage, overlap and FIRST reachability using possible-input upper bounds and certain-input lower bounds. DMN keeps named type definitions during proof preparation, but cells reading model/local values or filter fields stay unknown when their enclosing scope cannot be preserved. Wildcards use effective `inputValues`; explicit entries use their own tests. These queries produce diagnostics, not a license to eliminate a rule's outputs. See the [table-proof contract](type-system.md#56-what-the-types-are-used-for).

## 7. What it changes

**The type of every read** in the part the fact holds for. That is most of it, and the pages of the kinds have the details.

**The type of the `if`.** `Feel.Analysis.Inference.reachable/1` says, from the type of the condition, whether the `then` branch can be taken (some alternative can be `true`) and whether the `else` can (unless the condition is `boolean = true` for sure). The type of the `if` is the union of the types of the branches that can be taken, and the warnings of a branch that cannot are not reported.

**A branch whose facts leave a name nothing** is a branch that cannot be taken either (D-152, D-194). It is found in two ways, and both ask the same `Refinement.narrowed/2` of the facts of the conditions around the branch and of its own, for the type that a read gives the name:

- *By a read* (D-152). The facts are applied where a name is read, and a read that finds they leave the name no value tells the `if` whose branch it is in (`count(v) = 1 and v = []`, which nothing makes true, since a list of one element is not `[]`, and which the type of the condition does not say for a `v` of type `Any`; an ordering of what has no order, `v < true`, is `Null` by its type, D-196, and decided without any help from the facts). The branch is left out of the type of the `if` and its warnings are not reported, as for a condition that cannot be true, and the `if` says that the branch never runs (an `unreachable_branch` warning, below). It costs nothing: the read applies the fact already. Only a branch that reads such a name is found this way.
- *By a call* (D-194). A condition that compares a call of a rounding function, of `exp` or of `log` (`floor(x) = 2.5`) is the one place where the facts know what the type of the condition does not: the type of the call is a hull of its results, `floor(x) = 2.5` is undecided for it, and no number gives such a result. The facts are applied to the name that the call reads, whether or not anything in the branch reads it (`if floor(x) = 2.5 then 5 else 7` is `number = 7`). It is asked for a comparison on either side, through an operation or an `abs`, `sqrt` or `modulo` (`floor(x) + 1 = 3.5`), for the value of a `between` and the subject of an `in`, and for the operands of an `and` or an `or`; for the `then` branch, since the facts of a call are those of its `then`; and for a name, a local or the element of a filter whose type has no `Any` and no negation in it. What the fact leaves of the type is kept for the reads of the branch, so a branch that reads the name applies the fact once.

Nothing else is asked of a branch that reads none of the names its facts are about, and it is in the type, with no warning: applying the facts at every `if` costs 20 to 65 % of preparing a chain of `else if` on a number at least (a number given, no look-up of the name: one `x = 1` is 550 to 850 reductions, and a term of the chain is analyzed in 2,300 to 5,000), 25 to 185 % with the type of the name looked up, and 80 to 470 % applied to `Any`, which does not find the `floor` condition at all; a chain of `v instance of …` that returns constants is twice the cost of preparing it. The sets of the types decide a comparison of a name, of an operation on names or of an `abs`, `sqrt` or `modulo` as the facts do (an image of an interval is an interval), and of 6,702 conditions of those and of the calls against constants, the facts find 196 that the type of the condition does not, every one a rounding function, `exp` or `log` (D-194 has the measure). A conditional whose two branches are both found out is not taken in the branch of the one around it.

**A `decided_condition` warning**, when a condition that reads a name still has one outcome: always true (the `else` never runs), or never true (the `then` never runs). The same for an operand of `and` or `or` (it can be left out, or it decides the operation) and for a unary test that no input satisfies. A condition of constants is how a branch is switched off (`if true`) and is not reported, nor is a branch that cannot run itself.

**An `unreachable_branch` warning** (D-173), for a branch that the type of the condition leaves and in which a read found that the facts leave its name no value: the analogue of the redundant clause that Elixir reports. Its span is the branch, its message says which branch and the name that was read, and its `details` have `branch` (`:then` or `:else`) and `name`. It is a warning and not an info for the reason a `decided_condition` is one: a condition that no value of a name satisfies, or that every value satisfies, is most often a mistake, and an `:info` is for what was done on a value's behalf. It is found when the expression is prepared and changes no result. The facts that the branch has are those of its own condition and of the conditions around it, so the message does not blame the condition of the `if` it is reported for. It is not reported:

- for a branch that reads none of the names its facts are about, unless the condition compares a call of a rounding function, `exp` or `log` (above): `if count(v) = 1 and v = [] then 5 else 7` is `number in 5, 7`, and so is `if floor(v) = 2.5 then 5 else 7` for a `v` of type `Any`; nor for the facts of a path such as `p.age`: neither a read of the path nor the call finds that they leave it nothing (`if floor(p.age) = 2.5 then p.age else 7` is `number | Null`);
- for a constant condition (`if true then x else 7`), nor for a branch that the type of the condition rules out, which a `decided_condition` has already reported for the condition, so the branch is not reported twice;
- for a conditional both of whose branches are found out, nor for one in a branch that is not taken: the place that cannot be reached is the branch of the conditional around it, which says so once;
- for a conditional in the right operand of an `and` or an `or`, or in the upper bound of a `between`, that has facts of the left one: the operand is read under facts that hold only where it decides the operation, and is run all the same (D-53), so what the facts rule out is run as well. The branch is out of the type as before; it is not reported as unreachable. (A branch that is out because of the condition of its own `if` alone is not reported either, in these places.)
- for the body of a function that is analyzed again for a call: the facts of the call are not the function's, and the warnings are those of the function as it is written (D-193). `(function(n) if floor(n) = 2.5 then n else 7)(x)` is `number = 7` with no warning, and with `n: number` in the parameter the function reports it itself.

| Expression | Type | Warnings |
| --- | --- | --- |
| `if n > 10 then 1 else 2` | `number = 2` | `decided_condition` |
| `if n >= 0 then 1 else 2` | `number in 1, 2` | — |
| `if x > 5 then (if x > 3 then 1 else 2) else 3` | `number in 1, 3` | `decided_condition` |
| `if count(v) = 1 and v = [] then v else 7` | `number = 7` | `unreachable_branch` |
| `if count(v) = 1 and v = [] then (if y > 0 then 1 else v) else 7` | `number in 1, 7` | `unreachable_branch` |
| `if count(v) = 1 and v = [] then 5 else 7` | `number in 5, 7` | — |
| `if v < true then 5 else 7` | `number = 7` | `type_mismatch`, `decided_condition` |
| `if v <= true then 5 else 7` | `number = 7` | `type_mismatch`, `decided_condition` |
| `if floor(x) = 2.5 then x else 7` | `number = 7` | `unreachable_branch` |
| `if floor(x) = 2.5 then (if y > 0 then 1 else x) else 7` | `number = 7` | `unreachable_branch` |
| `if floor(x) = 2.5 then 5 else 7` | `number = 7` | `unreachable_branch` |
| `if floor(x) = 2.5 or floor(x) = 3.5 then 5 else 7` | `number = 7` | `unreachable_branch` |
| `if exp(x) = 3 then 5 else 7` | `number = 7` | `unreachable_branch` |
| `if floor(x) = 2.5 or y > 0 then 5 else 7` | `number in 5, 7` | — |
| `if floor(x) != 2.5 then 5 else 7` | `number = 5` | `unreachable_branch` |
| `if floor(v) = 2.5 then 5 else 7` | `number in 5, 7` | — |
| `if abs(x) = 2.5 then 5 else 7` | `number in 5, 7` | — |
| `if floor(p.age) = 2.5 then p.age else 7` | `number \| Null` | — |
| `if true then (if floor(x) = 2.5 then x else 7) else 0` | `number = 7` | `unreachable_branch` |
| `floor(x) = 2.5 and (if y > 0 then x else 1) > 0` | `boolean` | `decided_condition` |
| `x > 5 and x > 3` | `boolean \| Null` | `decided_condition` |
| `n >= 0 and n <= 10` | `boolean = true \| Null` | `decided_condition` |
| `x > 5 and x < 3` | `boolean = false \| Null` | `decided_condition` |
| `x < 0 or x >= 0` | `boolean = true \| Null` | — |
| `n in [0..10]` | `boolean = true \| Null` | — |
| `n between 0 and 10` | `boolean = true \| Null` | — |
| `n in [20..30]` | `boolean = false \| Null` | — |

`if n >= 0 then 1 else 2` is not decided because `n` can be `null`, and then the condition is `null`. That is the reason a warning is as exact as the types: `x < 0 or x >= 0` is `true` or `null`, not `true`.

**The optimizer.** It reads the types: a check that a type already settles (a conversion of the result, the allowed values of a result) is dropped, and a condition whose type is a constant is folded. A narrowing that was unsound would make it drop a check that was needed, which is why section 10 matters ([type-system.md](type-system.md), 5.6 and 6).

## 8. What gives no fact

The facts are read from a closed set of shapes (section 3). Anything else says nothing about its subjects, and a subject keeps the type it had:

- **Built-in functions as conditions on their own:** `includes(r, x)`, `contains`, `starts with`, `matches`, with no comparison. (`count(xs)` compared with a whole number is a fact about `xs`, D-194, and a call compared with a value says what it does of its arguments, D-170; the `else` of a call is read where the call cannot be `null` for the argument: an operation, a number function and `string length`, not another built-in.) `not(c)` is read ([5](#5-and-and-or)).
- **A boolean that was computed, where its facts are not kept.** A name that is bound to a condition remembers it (section 6), and a name that is bound to anything else (`ok: f(x) > 5` with a call that gives no fact, a value that came from a list) does not.
- **A comparison of two expressions** (`x + y > 5` narrows `x` to a non-null number, but no set: `y` is unknown).
- **A condition on an indexed element** (`xs[1] > 0`), a **range held as a value** (`x in r`), or a quantifier (`some i in xs satisfies i > 5`) does not generally propagate a fact back to `xs` or the range's endpoints. Selected comparisons of `count(xs)` with whole numbers do narrow empty versus non-empty lists; they do not encode arbitrary lengths ([list](narrowing/list.md)).
- **An unsupported or indeterminate exclusion from `Any`.** Scalar comparisons can keep the complement of their certainly-true set: `v > 5` leaves `Any except number in (5..max] | Null` when not true. If the other side is unknown, or no useful certainty bound can be constructed, the not-true branch may remain `Any | Null` ([any.md](narrowing/any.md)).
- **A function value**: `instance of function<...>` removes `null`, and takes the function types of a function out of the type or leaves them (an overload, D-171), and a call finds what the test says of the arguments it takes ([function.md](narrowing/function.md)).

## 9. Limits

The intended policy for possible-value facts is to widen when a representation budget is exhausted. The limits below describe that policy. Negation, function parameters and certain-input rule sets require different directions: nested exclusions are kept, function projection checks variance, and certain numeric/string sets use lower bounds rather than these ordinary upper-bound policies. `NumberSet` complement and inclusion are exact over their supplied sets. The [assessment](type-system-analysis.md#33-negation-and-variance-determine-the-direction-of-approximation) states the contracts and remaining proof obligations.

| What | Limit | What happens |
| --- | --- | --- |
| the pieces of a set of numbers, of a date or of a duration | 16 | the one interval that holds them all; the next fact cuts from that |
| the strings of a set | 64 | every string |
| a property walk (`d.month` and `d.day`; duration hours, minutes and seconds; `dt.hour` and the finer clock fields) | 1,200 months, 2,000 cycles, or 512 pieces | the walk returns `:error` and the set is left as it was |
| a years-and-months duration added to or subtracted from a date | 2,000 pieces, or 400 months of the date | one interval from the first date to the last |
| the months of a years-and-months duration times or divided by a number, and the dates that give a date in a set | 64 months | one interval from the first month to the last |
| the facts about the other paths from a name that one read applies | 16 (D-154) | the type says less of the name, which is true |
| the facts about one subject that cannot be answered from its type, per `and` / `or` chain | `max_narrowing_facts`, 256 (D-154) | an error of kind `:limit`, code `:too_many_facts`, when the expression is prepared |

A property walk that finishes still stores its amounts in a number set, so more than 16 intervals become the hull in the first row. `dds.minutes = 30` does that. The walk limits above are where the walk refuses and the subject stays as it was. Past the date-arithmetic and month limits, the result is one interval that holds every piece the walk would have built, and more.

The 16 pieces are why `x != 1 and x != 2 and …` narrows a number until the sixteenth hole: with `x != 15` as the last, the set is `[-max..1), (1..2), …, (15..max]`, sixteen intervals. One more, and the seventeen intervals become `number | Null`, and each fact after that cuts the hull again (`x != 17` gives `[-max..17), (17..max]`). For this positive numeric bound, taking the hull keeps possible values and loses precision. The same operation cannot be reused as a lower bound for certainty. Exact complement preserves the meaning of the supplied set, but cannot recover gaps already filled by an earlier hull.

For certain string inputs of decision rules, the 64-point/exclusion check follows bulk union or intersection of the entry list. String intervals do not count toward that cap. Keeping the bulk operations avoids repeatedly rebuilding a growing interval set in positive and negated lists.

`max_narrowing_facts` counts facts that **cannot be answered from the type** the subject is read at, and have to be applied to it at each read: the work for a subject grows with the square of their number. A thousand facts that the type answers (`x = "a" or x = "b" or …`) cost no more than one. The condition that went over is named:

```
p.age > 1 and 1 / p.age > 0 and p.age > 2 and 1 / p.age > 0 and …        (20 pairs, max_narrowing_facts: 5)
→ {:error, %Feel.Error{kind: :limit, code: :too_many_facts}}
  the conditions say too much about "p.age": 6 facts about it have to be applied to its type, and at most 5 are allowed
```

With the default of 256 the same 20 pairs are prepared. The example uses a *path*: the same chain about a plain name (`x > 1 and 1 / x > 0 and …`) is answered from the type of the name, and was prepared without reaching the limit with 200 pairs.

## 10. Correctness obligations and checks

The documentation tables themselves are executable checks. From the umbrella root:

```sh
mix test apps/feel/test/feel/sweep/docs_test.exs
MIX_ENV=test mix do --app feel cmd mix run scripts/sweep/check_docs.exs
```

Both compare the recognized tables in this page and `narrowing/*.md` with current analysis, including warning codes. They do not execute every prose example, compare warning wording, or prove that a bound contains all runtime results. The [sweep guide](../scripts/sweep/README.md) explains the separate generated runtime and tier checks.

A narrowed type must contain every value that its subject can have where it is read, under the stated assumptions. Unknown conditions should contribute no fact; bounded approximations must preserve the required inclusion direction. The optimizer may otherwise remove a check the run needs.

These are obligations, not properties established by the current implementation. The [contracts of the assessment](type-system-analysis.md#2-contracts-and-evidence) show why checking each rule in isolation or widening positive result bounds does not establish correctness of their composition.

What looks for a violation:

| Test | Checks |
| --- | --- |
| [`narrowing_soundness_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/narrowing_soundness_test.exs) | selected conditions read as names, context entries and function parameters: facts are checked against values reaching the branch on finite binding grids |
| [`condition_narrowing_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/condition_narrowing_test.exs) | the types of `in`, `instance of`, operations, paths and shapes, and the run |
| [`operand_narrowing_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/operand_narrowing_test.exs), [`temporal_operand_narrowing_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/temporal_operand_narrowing_test.exs) | the operands of an operation, for numbers and for dates and durations |
| [`narrowing_filters_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/narrowing_filters_test.exs), [`and_narrowing_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/and_narrowing_test.exs) | the elements of a filter; the right operand of `and` |
| [`narrowing_memo_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/narrowing_memo_test.exs) | the answers that a chain of conditions keeps equal what the facts would leave |
| [`unreachable_branch_test.exs`](https://github.com/FeeJai/BDM/blob/main/apps/feel/test/feel/analysis/unreachable_branch_test.exs) | selected unreachable branches, `Never` nodes and warning placement; inference also uses three-outcome facts and selected call preimages (D-173, D-194) |

Precision checks also require useful narrowing in selected cases. Neither precision checks nor a finite soundness grid prove the universal obligation; shared membership code can hide a semantic defect.

## 11. The code

| Module | Does |
| --- | --- |
| [`analysis/narrowing.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/narrowing.ex) | the facts of a condition, their meet and join, and `narrow/2`; the paths (`narrow_source/3`), the operations and the elements of a filter |
| [`analysis/test_sets.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/test_sets.ex) | what a comparison leaves of a kind, as sets, for narrowing and for allowed values |
| [`analysis/preimage.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/preimage.ex) | the numbers an operand can be when an operation is in a set |
| [`analysis/images/number/preimage.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/images/number/preimage.ex) | the numbers an argument of a number function can be when its result is in a set |
| [`analysis/moment_tests.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/moment_tests.ex) | a comparison of a time or a date and time, on the lines of their zones |
| [`analysis/date_properties.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/date_properties.ex), [`duration_properties.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/duration_properties.ex), [`moment_properties.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/moment_properties.ex) | the sets that a fact about a property leaves |
| [`analysis/filters.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/filters.ex) | the elements a predicate keeps |
| [`analysis/analyzer.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/analyzer.ex) | where the facts are applied: `if`, `and`, `or`, `between`, the context of a read |
| [`analysis/inference.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/inference.ex) | `reachable/1` and `conditional/3`: which branch can run |

The [current decision record](decisions.md) groups the relevant choices: D-194 for condition outcomes, D-122 for inverse arithmetic, D-193 for binding summaries, D-173 for unreachable code, and D-154 for budgets.

## 12. The pages

| Page | Covers |
| --- | --- |
| [number](narrowing/number.md) | intervals of decimals; comparisons, `between`, `in`, operations |
| [number functions](narrowing/number-functions.md) | a comparison of `abs`, `floor`, `round *`, `sqrt`, `exp`, `log`, `modulo`; an allowed value that is one |
| [string](narrowing/string.md) | strings and intervals of strings, in the order of the run |
| [boolean](narrowing/boolean.md) | `true` and `false`; a boolean as a condition |
| [date](narrowing/date.md) | days; comparisons and the properties of a date |
| [time](narrowing/time.md) | seconds of the day, on the lines of their zones |
| [date and time](narrowing/date-and-time.md) | seconds, zones, and their properties |
| [years and months duration](narrowing/years-and-months-duration.md) | months |
| [days and time duration](narrowing/days-and-time-duration.md) | seconds |
| [list](narrowing/list.md) | the type of the elements; equality; the elements a filter keeps |
| [range](narrowing/range.md) | what a range value allows |
| [context](narrowing/context.md) | paths, and the sources that they narrow; the context functions |
| [conversions](narrowing/conversions.md) | the type of `number`, `string`, `date`, `time`, `date and time`, `duration`, `years and months duration` and `range` |
| [structure](narrowing/structure.md) | the allowed values and the type constraint of a member of a value, and of a list as a whole |
| [function](narrowing/function.md) | what a function type allows |
| [null](narrowing/null.md) | the `Null` alternative: guards, and every operator against every other side |
| [Any](narrowing/any.md) | a name of any type, narrowed kind by kind |
| [named types](narrowing/named-types.md) | model-defined types |
| [overloaded functions](narrowing/overloaded-functions.md) | functions with several signatures, and function values |

## 13. Does it narrow as far as it can?

Section 10 is about one half of the question: a narrowed type has to hold every value that the subject can have. The other half is that it should hold nothing else, and nothing in the tests of section 10 asks about it. The **construct suite** (`test/feel/construct_suite`, `test/support/construct_suite`) does.

**What a case is.** A catalog (`Feel.ConstructSuite.Catalog.*`) is a list of expressions, each an example of a construct, with the IR that the analyzer makes of it as text, one node per line with its type (`Feel.ConstructSuite.IRText`):

```
if :: number in 0, (5..max]
  compare gt :: boolean | Null
    var x :: number | Null
    const :: number = 5
  var x :: number in (5..max]
  const :: number = 0
```

The catalogs cover every kind of node of the syntax tree and every operator (`expressions`), the nodes that the declarations of the scope put around an expression (`declarations`), lists of unary tests, a function of an extension, the conditions of section 3 for each kind of subject, in the `then` and in the `else` branch (`conditions`, a case is `if C then S else S`), and the places of section 6, what shadows a fact, what gives none, and the limits of section 9 (`positions`). `coverage_test.exs` reads the tables of `Feel.AST` and `Feel.IR` and fails for a kind of node that has no case, so that a new construct cannot be added without one. A test holds each case to its IR and its warnings, so a change of the analysis shows as the diff of the IR. From the umbrella root, `MIX_ENV=test mix do --app feel cmd mix run scripts/construct_suite.exs --check` reports changed snapshots; omitting `--check` rewrites them and requires reviewing the diff.

**How "as far as it can" is asked.** `Feel.ConstructSuite.Oracle` runs the expression on a grid: the product of the values of its names, each name with the constants of the expression and the edges of its allowed values, and the number below and above each (`Pools`), the way the sweeps do, and observes the values that reach each node (`Feel.Backend.Interpreter.run_monitored/4`, the monitor of `Feel.Paranoid`), each node by itself and not by its text: the two comparisons of the range in `n in [20..30]` are one span, and so are a node of the verification of a declared value and one of the expression. A node is **wider than the runs** when its type holds something that no run brings to it:

| Node | Wider than the runs when |
| --- | --- |
| a read of a name, or of an entry of one (`x`, `p.age`) | the type holds a value the name was bound to in some run, and that never reached this read: `x` after `x != null` that is `number \| Null` |
| a condition (`compare`, `logic`, `between`, `in`, `instance_of`, a quantifier) | its type has `true`, `false` or `null`, and no run gave it |
| any other node | no run reached it, and its type is not the type of no value (D-173); not said of the body of a function (it runs when it is called) or of the right operand of an `and` or an `or` (and the upper bound of a `between`, and the upper comparison of a range in an `in`) when the types of the left rule out the condition it is told under, as in `false and b`: such an operand is run (D-53), but the monitor is not told it (D-170) |

The grid is not all values, so a witness is a lead and not a proof: a value that the pools lack makes a type look wider than it is. Every gap in the catalogs has been examined, and a case can add values (`extra:`). The suite does not judge a node that is not a condition or a read, such as the result of an arithmetic operation; a case can say what such a node should be (`ideal:`) when it is known.

**Gaps.** A gap is a node that is wider than the runs, with the reason, in the case (`gaps:`). The test of the case fails for a gap that is not listed and for one that is closed, so the list is always the list that the runs find. Each case that has gaps has a second test, tagged `:gap` and left out of `mix test`, that says what the narrowing should do (no node wider than the runs, the nodes of `ideal:` as they should be):

```sh
mix test apps/feel/test/feel/construct_suite --include gap
```

The current `gaps:` and `ideal:` entries in the [construct catalogs](https://github.com/FeeJai/BDM/tree/main/apps/feel/test/support/construct_suite/catalog) are the maintained precision backlog. The tagged run above intentionally exposes cases whose ideal bounds are not yet inferred; it is separate from the ordinary passing regression suite. Old inventories included direct-call specialization and impossible floor comparisons that later repairs can handle, so they should not be read as a current list of missing features. A gap on a finite grid still needs semantic review before being treated as a valid optimization opportunity.

This catalog is not an inventory of every precision gap. Repeated-read rules cover selected operators (D-170, D-207), but duration self-addition still combines independent intervals and can admit sums of different possible values. See the [month-duration](narrowing/years-and-months-duration.md#limits) and [second-duration](narrowing/days-and-time-duration.md#limits) limits and the [backlog](todo.md).