Documentation

IsIntersection x y z witnesses the fact:

• All x, y, z share the same runtime representation

• z is an intersection type of x and y. In other words, the following three holds:

  • Sub z x

  • Sub z y

  • For any type s satisfying both of (Sub s x, Sub s y), Sub s z.

For a pair of Related types x and y, make some (existentially quantified) type xy where xy is an intersection type of x, y.

Two intersection types z,z' of the same pair of types x,y may be different, but they are equivalent in terms of coercibility.

When Sub x y, x itself is an intersection type of x, y.

Intersection is idempotent.

Note: combining idemp and unique, IsIntersection x x z -> Coercion x z holds.

Intersection is commutative.

Note: combining commutative and unique, IsIntersection x y xy -> IsIntersection y x yx -> Coercion xy yx holds.

Intersection is associative.

Note: combining associative and unique, the following holds.

   IsIntersection x y xy -> IsIntersection xy z xy'z
-> IsIntersection y z yz -> IsIntersection x yz x'yz
-> Coercion xy'z x'yz