Explicitly derive example of known unsoundness in normal forms

Author: LPTK

shared/src/test/diff/mlscript/BooleanFail.mls

@@ -78,3 +78,92 @@ f (forall 'a. fun (x: 'a) -> x)
 //│    = [Function (anonymous)]
 
 
+// * Example 2
+
+def g(x: 'a | {f: nothing}) = x.f(0)
+//│ g: {f: 0 -> 'a} -> 'a
+//│  = [Function: g]
+
+foo = forall 'x. fun (x: 'x) -> g(x)
+//│ foo: anything -> nothing
+//│    = [Function: foo]
+
+:re
+foo 0
+//│ res: nothing
+//│ Runtime error:
+//│   TypeError: x.f is not a function
+
+
+
+// * Now let's consider why functions and classes can't intersect to nothing due to distributivity
+
+
+class Foo: { x: anything }
+//│ Defined class Foo
+
+
+// * These two types should be equivalent, but they visibly aren't:
+
+def a: (int -> int | {x: int}) & Foo
+def b: int -> int & Foo | {x: int} & Foo
+//│ a: Foo
+//│  = <missing implementation>
+//│ b: Foo & {x: int}
+//│  = <missing implementation>
+
+:ne
+ax = a.x
+bx = b.x
+//│ ax: anything
+//│ bx: int
+
+
+// * Yet, this does not immediately lead to unsoundness due to the aggressive normalization
+// * performed during constraint solving:
+
+:ne
+a = b
+//│ Foo & {x: int}
+//│   <:  a:
+//│ Foo
+
+:e
+:ne
+b = a
+//│ Foo
+//│   <:  b:
+//│ Foo & {x: int}
+//│ ╔══[ERROR] Type mismatch in def definition:
+//│ ║  l.133: 	b = a
+//│ ║         	^^^^^
+//│ ╟── expression of type `anything` is not an instance of type `int`
+//│ ╟── Note: constraint arises from type reference:
+//│ ║  l.109: 	def b: int -> int & Foo | {x: int} & Foo
+//│ ╙──       	                              ^^^
+
+
+// * To expose the unsoundness, we need some indirection with abstract types
+// * that prevent eagerly distributing the intersection type:
+
+class Test1[A, B]: { f: A & Foo }
+  method M: B & Foo | {x: int} & Foo
+//│ Defined class Test1[+A, +B]
+//│ Declared Test1.M: Test1[?, 'B] -> (Foo & 'B | Foo & {x: int})
+
+class Test2[B]: Test1[B | {x: int}, B]
+  method M = this.f : B & Foo | {x: int} & Foo
+//│ Defined class Test2[+B]
+//│ Defined Test2.M: Test2['B] -> (Foo & 'B | Foo & {x: int})
+
+oops = (Test2{f = Foo{x = "oops"}} : Test1[anything, int -> int]).M 
+//│ oops: Foo & {x: int}
+//│     = Foo { x: 'oops' }
+
+// * Notice the type confusion:
+oops.x + 1
+//│ res: int
+//│    = 'oops1'
+
+
+