undulating humming

Coherent unrestricted intersection?

A, B sorts ("Curry types", etc.)
A∧B intersection (no refinement restriction)
X, Y types ("Church types", etc.)
e1 // e2 alleged coherent merge (cf. Elaborating…)

Judgments:

   e : A   —e has sort A
   e :: X   —e has principal type X
   A ⊑ X   —A refines X


e1 : A1      A1 ⊑ X1      e1 :: X1
e2 : A2      A2 ⊑ X2      e2 :: X2      X1 ⋈ X2
————————————————————————————
            e1 // e2 : A1 ∧ A2
            e1 // e2 : A2 ∧ A1


⊢ X1 ⋈ X2 read "X1 separate from X2", such that:

• If X ≤ Y or Y ≤ X (where "≤" = at-least-as-polymorphic-as) then ⊬ X ⋈ Y
    (corollary: ⊬ X ⋈ X)
• If X and Y have distinct head constructors then X ⋈ Y
• (X1 * X2) ⋈ (Y1 * Y2) if either X1 ⋈ Y1 or X2 ⋈ Y2
• (X1 + X2) ⋈ (Y1 + Y2) if X1 ⋈ Y1 and X2 ⋈ Y2
• (X1 → X2) ⋈ (Y1 → Y2) if X1 ⋈ Y1 and X2 ⋈ Y2


α ⊑ β ⊢ A ⊑ X
—————————————
⊢ ∀α.A ⊑ ∀β.X