ch:disjoint-intersections: ch:disjoint-intersections

The first pair has distinct ordinary heads, so it is algorithmically disjoint. For the products, the first coordinates have distinct ordinary heads, so the left product rule proves disjointness even though the second coordinates are both $\mathsf{Int}$. Two arrows with the same result are rejected because the arrow clause compares only results. If their domains are $D_1,D_2$ and their common result is $R$, the raw type is a common supertype. The domain intersection need not be well formed. There is no common supertype in either accepted case.

Without the disjointness premises of I-Merge and WF-, synthesis gives with target $(1,2)$. The two checking derivations end in I-Sub, using $$c_1=\lambda p.{\pi }_{1}p,c_2=\lambda p.{\pi }_{2}p.$$ Their targets are $c_1(1,2)⟼1$ and $c_2(1,2)⟼2$. Both are well typed; their different values are the coherence failure.

Let $X=\mathsf{Int}$, $Y=\mathsf{Int}\to \mathsf{Int}$, and . Let $Z=\mathsf{Int}\times \mathsf{Int}$; then $A\ast Z$. Write $c_X:X\to X$ and $c_Y:Y\to Y$ for the raw coercions generated by S-Int and S-Arr, and put $$d_X=\lambda q.c_X({\pi }_{1}q),d_Y=\lambda q.c_Y({\pi }_{2}q),c_A=\lambda q.(d_{X}q,d_{Y}q).$$ These are the rule-generated coercions for , , and . For , the forbidden direct left rule gives $$\lambda p.c_A({\pi }_{1}p).$$ Rule S-R, followed by the permitted ordinary projections to $X$ and $Y$, gives $$\lambda p.((\lambda q.d_X({\pi }_{1}q))p,(\lambda q.d_Y({\pi }_{1}q))p).$$ Both have target type $(|A|\times |Z|)\to |A|$, but they are not alpha equal. They do beta-normalize to the same projection pair; this does not rescue the chapter’s raw-syntax uniqueness claim. Thus coercion typing still holds; lemma 21.10 is the first metatheorem in the chapter to fail, and raw elaboration coherence subsequently fails with it.

From , the coercion to $B$ is $\lambda p.{\pi }_2({\pi }_{1}p)$. From , it is $\lambda p.{\pi }_1({\pi }_{2}p)$. Their domains are respectively $(|A|\times |B|)\times |C|$ and $|A|\times (|B|\times |C|)$. Coherence compares two derivations of one fixed source judgment; it does not identify distinct, merely isomorphic source types or insert a product associator.

The merge synthesizes and elaborates to $(1,\lambda x.x)$. Checking the annotated function position against $\mathsf{Int}\to \mathsf{Int}$ inserts $\lambda p.{\pi }_{2}p$. Application therefore elaborates to $$(\lambda p.{\pi }_{2}p)(1,\lambda x.x)2⟼(\lambda x.x)2⟼2.$$

If the result types are disjoint, inversion of any common arrow supertype would exhibit a common supertype of the results, a contradiction. Conversely, if $A_2$ and $B_2$ share $C$, then is a raw common supertype of $A_1\to A_2$ and $B_1\to B_2$. The witness grammar is unrestricted, so this remains valid when its domain intersection is not well formed.

Take They are incomparable: answering the function component of $A$, or the product component of $B$, is impossible from the other type. Both subtype $C=\mathsf{Int}$. Closed inhabitants $1,,(\lambda x.x)$ and $2,,(3,4)$, with the displayed component annotations, coerce to $1$ and $2$. Thus incomparability does not imply disjointness.

For an intersection target, both derivations must end in S-R; the ordinary-target premises exclude S-L${}_i$. For an intersection source and ordinary target, two different left projections are excluded by unique contribution, and two equal projections reduce to the induction hypothesis. For equal ordinary heads, inversion forces the same one of S-Int, S-Arr, and S-Prod; distinct heads have no derivation. These are all overlapping last-rule pairs.