ch:dependent-object-types: variable-path DOT

Binding the implementation gives $n : μ (c : {A : N . . N} \land {v a l u e : c . A}) .$ Rule DOT-Rec-E exposes $n : {A : N . . N} \land {v a l u e : n . A}$ . Intersection elimination gives $n : {v a l u e : n . A}$ , and DOT-Fld-E gives $n . v a l u e : n . A$ . The other intersection projection gives $n : {A : N . . N}$ , so DOT-Sel-U derives $n . A <: N$ (and DOT-Sel-L derives the reverse bound). Replacing the member declaration by ${A : ⊥ . . ⊤}$ changes the DOT-Sel-U conclusion to $n . A <: ⊤$ . The step that formerly supplied $n . A <: N$ is therefore absent.

Interpret types in the lattice $0 < 1$ , with $⊥ = 0$ and $⊤ = 1$ . After deleting DOT-Sel-L, interpret $x . A = 0$ . The remaining upper premise $x . A <: ⊥$ is $0 \leq 0$ , while $⊤ <: ⊥$ is the false statement $1 \leq 0$ . After restoring DOT-Sel-L and deleting DOT-Sel-U, interpret $x . A = 1$ . The lower premise $⊤ <: x . A$ is $1 \leq 1$ , while the collapsed conclusion remains false. Each selection rule supplies a different half of the path from top to bottom; neither half alone collapses the lattice.

Let the inert context extracted from $E$ bind $x = λ (z : S^{'}) t$ . Clause 1 of theorem 107.9 locates the dependent-function declaration bound to $x$ and supplies its domain comparison; clause 2 identifies the value as that lambda and supplies the comparison needed to obtain $Γ ⊢ y : S^{'}$ . Inversion of lambda typing supplies $Γ, z : S^{'} ⊢ t : T^{'} .$ The required source substitution lemma is exactly $\frac{Γ, z : S^{'} ⊢ t : T^{'} Γ ⊢ y : S^{'}}{Γ ⊢ t [y / z] : T^{'} [y / z]} .$ The canonical-form codomain comparison and subsumption then recover the original application result $T [y / z]$ , and the typing reconstruction for $E$ places the reduct at the original whole-term type. Without inertness, general typing cannot be converted to tight and precise typing: a bad-bound selection may fabricate the function type of $x$ , so canonical forms cannot recover a lambda and the proof stops before the displayed substitution premise.

The type $\forall (x : S) T$ is inert by the function clause. The type $μ (x : {A : S . . S} \land {a : x . A})$ is inert by the recursive-record clause: its type member has equal bounds, its field has a well-formed type, and its labels are distinct. The type $μ (x : {A : S . . U})$ with $S \neq U$ is not inert because its sole member violates the equal-bounds condition.

Rule DOT-Rec-E gives $x : {A : T . . T} \land {a : x . A} .$ The field intersection projection followed by DOT-Fld-E yields $x . a : x . A$ . The member projection is the precise judgment $Γ ⊢_{!} x : {A : T . . T}$ ; therefore DOT-T-Sel-L and DOT-T-Sel-U give $Γ ⊢_{#} T <: x . A, Γ ⊢_{#} x . A <: T .$ The field result is retained between these equal tight bounds.

Choose distinct closed record types $S = {a : ⊤}$ and $U = {b : ⊤}$ . In $x : {A : ⊤ . . ⊥}$ , selection and transitivity give $S <: ⊤ <: x . A <: ⊥ <: U$ , hence $S <: U$ ; the symmetric outer top/bottom chain also gives $U <: S$ . However, DOT-Def-Type types a concrete definition ${A = T}$ only as ${A : T . . T}$ . Definition intersection preserves that equality and DOT-Obj-I installs precisely those member declarations. Consequently an object value placed in the runtime context can contribute only equal bounds; it cannot contribute ${A : ⊤ . . ⊥}$ , since $⊤ \neq ⊥$ .

Suppose $E$ binds $x = ν (z : T^{'}) d$ and the redex is $E [x . a]$ . Canonical forms recover the precise recursive type $μ (z : T^{'})$ ; DOT-Rec-E exposes $T^{'} [x / z]$ . Precise intersection decomposition locates the declaration ${a : S}$ . Pairwise label disjointness makes this occurrence unique, so inversion of definition typing locates the corresponding definition ${a = t}$ and gives $t : S$ after receiver substitution. The projection root therefore replaces $x . a$ by a term of the same field type. Rebuild the surrounding let bindings of $E$ from the innermost one outward; each unchanged value retains its inert declaration and each let rule retains the original result type. Thus the whole reduct has the type of the original projection context.