Remove unsound simplification of negated record types in positive positions

Author: LPTK

shared/src/main/scala/mlscript/TyperHelpers.scala

@@ -646,9 +646,6 @@ abstract class TyperHelpers { Typer: Typer =>
       case ComposedType(false, l, r) => l.negNormPos(f, p) | r.negNormPos(f, p)
       case NegType(n) => f(n).withProv(p)
       case tr: TypeRef if !preserveTypeRefs && tr.canExpand => tr.expandOrCrash.negNormPos(f, p)
-      case _: RecordType | _: FunctionType => BotType // Only valid in positive positions!
-        // Because Top<:{x:S}|{y:T}, any record type negation neg{x:S}<:{y:T} for any y=/=x,
-        // meaning negated records are basically bottoms.
       case rw => NegType(f(rw))(p)
     }
     def withProvOf(ty: SimpleType): ST = withProv(ty.prov)

shared/src/test/diff/fcp/Overloads.mls

@@ -93,33 +93,43 @@ if true then IISS else BBNN
 //│ res: (0 | 1 | true) -> number
 
 
-// * Note that type normalization is currently very aggressive at approximating negative non-tag types, to simplify the result:
+// * Note that type normalization used to be very aggressive at approximating non-tag type negations,
+// * to simplify the result, but this was changed as it was unsound
 
 def test: ~(int -> int)
-//│ test: in ~(int -> int) out nothing
+//│ test: ~(int -> int)
 
-// * Note about this known unsoundness: see test file BooleanFail.mls
+// * See also test file BooleanFail.mls about this previous unsoundness
+:e
 test = 42
 not test
 //│ 42
 //│   <:  test:
 //│ ~(int -> int)
-//│ res: bool
+//│ ╔══[ERROR] Type mismatch in application:
+//│ ║  l.105: 	not test
+//│ ║         	^^^^^^^^
+//│ ╟── type `~(int -> int)` is not an instance of type `bool`
+//│ ║  l.99: 	def test: ~(int -> int)
+//│ ║        	          ^^^^^^^^^^^^^
+//│ ╟── but it flows into reference with expected type `bool`
+//│ ║  l.105: 	not test
+//│ ╙──       	    ^^^^
+//│ res: bool | error
 
-// :ds
 def test: ~(int -> int) & ~bool
-//│ test: in ~bool & ~(int -> int) out nothing
+//│ test: ~bool & ~(int -> int)
 
 def test: ~(int -> int) & bool
-//│ test: in bool out nothing
+//│ test: bool
 
 def test: ~(int -> int) & ~(bool -> bool)
-//│ test: in ~(nothing -> (bool | int)) out nothing
+//│ test: ~(nothing -> (bool | int))
 
 def test: ~(int -> int | bool -> bool)
-//│ test: in ~(nothing -> (bool | int)) out nothing
+//│ test: ~(nothing -> (bool | int))
 
 def test: ~(int -> int & string -> string) & ~(bool -> bool & number -> number)
-//│ test: in ~(nothing -> (number | string) & int -> number & nothing -> (bool | string) & nothing -> (bool | int)) out nothing
+//│ test: in ~(nothing -> (number | string) & int -> number & nothing -> (bool | string) & nothing -> (bool | int)) out ~(nothing -> (bool | int) & nothing -> (bool | string) & int -> number & nothing -> (number | string))
 
 

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

@@ -190,7 +190,7 @@ id (error: A) with { x = 1 } : A | { x: 'a }
 //│ res: A | {x: nothing}
 
 def negWeird: ~(~(~(A & { x: int })))
-//│ negWeird: in ~(A & {x: int}) out ~A
+//│ negWeird: ~(A & {x: int})
 
 def v = negWeird with { x = 1 }
 //│ v: ~A\x & {x: 1} | {x: 1} & ~{x: int}

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

@@ -3,28 +3,52 @@
 
 // * The MLscript subtyping system is currently ill-formed in some corner cases.
 // * Notably, it considers functions and classes to intersect to nothing
-// * and also considers positive negated function/record types equivalent to nothing.
+// * and also used to considers positive negated function/record types equivalent to nothing.
 
 // * (This isn't the case in MLstruct, which has a sound subtyping lattice.)
 
 
-// * Example 1
+
+// * Example 1 – now fixed
+
 oops = 42 : ~(int -> int)
-not oops
-//│ oops: nothing
+//│ oops: ~(int -> int)
 //│     = 42
-//│ res: bool
+
+:e
+not oops
+//│ ╔══[ERROR] Type mismatch in application:
+//│ ║  l.19: 	not oops
+//│ ║        	^^^^^^^^
+//│ ╟── type `~(int -> int)` is not an instance of type `bool`
+//│ ║  l.14: 	oops = 42 : ~(int -> int)
+//│ ║        	            ^^^^^^^^^^^^^
+//│ ╟── but it flows into reference with expected type `bool`
+//│ ║  l.19: 	not oops
+//│ ╙──      	    ^^^^
+//│ res: bool | error
 //│    = false
 
 
-// * OTOH, this doesn't lead to immediate unsoundness:
+// * This was accepted but didn't immediately lead to immediate unsoundness:
 def f: (~{x: int}) -> 'a
-f = id
-//│ f: in nothing -> nothing out ~{x: int} -> nothing
+//│ f: ~{x: int} -> nothing
 //│  = <missing implementation>
+
+:e
+f = id
 //│ 'a -> 'a
 //│   <:  f:
-//│ nothing -> nothing
+//│ ~{x: int} -> nothing
+//│ ╔══[ERROR] Type mismatch in def definition:
+//│ ║  l.39: 	f = id
+//│ ║        	^^^^^^
+//│ ╟── type `~{x: int}` does not match type `'a`
+//│ ║  l.34: 	def f: (~{x: int}) -> 'a
+//│ ║        	       ^^^^^^^^^^^
+//│ ╟── Note: constraint arises from type variable:
+//│ ║  l.34: 	def f: (~{x: int}) -> 'a
+//│ ╙──      	                      ^^
 //│  = [Function: id]
 
 :e
@@ -33,64 +57,75 @@ f id
 f {}
 f (forall 'a. fun (x: 'a) -> x)
 //│ ╔══[ERROR] Type mismatch in application:
-//│ ║  l.31: 	f 0
+//│ ║  l.55: 	f 0
 //│ ║        	^^^
 //│ ╟── integer literal of type `0` does not match type `~{x: int}`
-//│ ║  l.31: 	f 0
+//│ ║  l.55: 	f 0
 //│ ║        	  ^
 //│ ╟── Note: constraint arises from type negation:
-//│ ║  l.21: 	def f: (~{x: int}) -> 'a
+//│ ║  l.34: 	def f: (~{x: int}) -> 'a
 //│ ╙──      	       ^^^^^^^^^^^
 //│ res: error
 //│    = 0
 //│ ╔══[ERROR] Type mismatch in application:
-//│ ║  l.32: 	f id
+//│ ║  l.56: 	f id
 //│ ║        	^^^^
 //│ ╟── reference of type `?a -> ?a` does not match type `~{x: int}`
-//│ ║  l.32: 	f id
+//│ ║  l.56: 	f id
 //│ ║        	  ^^
 //│ ╟── Note: constraint arises from type negation:
-//│ ║  l.21: 	def f: (~{x: int}) -> 'a
+//│ ║  l.34: 	def f: (~{x: int}) -> 'a
 //│ ╙──      	       ^^^^^^^^^^^
 //│ res: error
 //│    = [Function: id]
 //│ ╔══[ERROR] Type mismatch in application:
-//│ ║  l.33: 	f {}
+//│ ║  l.57: 	f {}
 //│ ║        	^^^^
 //│ ╟── record literal of type `anything` does not match type `~{x: int}`
-//│ ║  l.33: 	f {}
+//│ ║  l.57: 	f {}
 //│ ║        	  ^^
 //│ ╟── Note: constraint arises from type negation:
-//│ ║  l.21: 	def f: (~{x: int}) -> 'a
+//│ ║  l.34: 	def f: (~{x: int}) -> 'a
 //│ ╙──      	       ^^^^^^^^^^^
 //│ res: error
 //│    = {}
 //│ ╔══[ERROR] Type mismatch in application:
-//│ ║  l.34: 	f (forall 'a. fun (x: 'a) -> x)
+//│ ║  l.58: 	f (forall 'a. fun (x: 'a) -> x)
 //│ ║        	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 //│ ╟── function of type `'a -> 'a` does not match type `~{x: int}`
-//│ ║  l.34: 	f (forall 'a. fun (x: 'a) -> x)
+//│ ║  l.58: 	f (forall 'a. fun (x: 'a) -> x)
 //│ ║        	              ^^^^^^^^^^^^^^^^
 //│ ╟── Note: constraint arises from type negation:
-//│ ║  l.21: 	def f: (~{x: int}) -> 'a
+//│ ║  l.34: 	def f: (~{x: int}) -> 'a
 //│ ╙──      	       ^^^^^^^^^^^
 //│ res: error
 //│    = [Function (anonymous)]
 
 
-// * Example 2
+// * Example 2 – now fixed
 
 def g(x: 'a | {f: nothing}) = x.f(0)
 //│ g: {f: 0 -> 'a} -> 'a
 //│  = [Function: g]
 
+:e
 foo = forall 'x. fun (x: 'x) -> g(x)
-//│ foo: anything -> nothing
+//│ ╔══[ERROR] Type mismatch in application:
+//│ ║  l.112: 	foo = forall 'x. fun (x: 'x) -> g(x)
+//│ ║         	                                ^^^^
+//│ ╟── expression of type `'x & ~{f: nothing}` does not have field 'f'
+//│ ╟── Note: constraint arises from field selection:
+//│ ║  l.107: 	def g(x: 'a | {f: nothing}) = x.f(0)
+//│ ║         	                              ^^^
+//│ ╟── from type variable:
+//│ ║  l.107: 	def g(x: 'a | {f: nothing}) = x.f(0)
+//│ ╙──       	         ^^
+//│ foo: anything -> error
 //│    = [Function: foo]
 
 :re
 foo 0
-//│ res: nothing
+//│ res: error
 //│ Runtime error:
 //│   TypeError: x.f is not a function
 
@@ -135,11 +170,11 @@ b = a
 //│   <:  b:
 //│ Foo & {x: int}
 //│ ╔══[ERROR] Type mismatch in def definition:
-//│ ║  l.133: 	b = a
+//│ ║  l.168: 	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
+//│ ║  l.144: 	def b: int -> int & Foo | {x: int} & Foo
 //│ ╙──       	                              ^^^