33
44// * The MLscript subtyping system is currently ill-formed in some corner cases.
55// * Notably, it considers functions and classes to intersect to nothing
6- // * and also considers positive negated function/record types equivalent to nothing.
6+ // * and also used to considers positive negated function/record types equivalent to nothing.
77
88// * (This isn't the case in MLstruct, which has a sound subtyping lattice.)
99
1010
11- // * Example 1
11+
12+ // * Example 1 – now fixed
13+
1214oops = 42 : ~(int -> int)
13- not oops
14- //│ oops: nothing
15+ //│ oops: ~(int -> int)
1516//│ = 42
16- //│ res: bool
17+
18+ :e
19+ not oops
20+ //│ ╔══[ERROR] Type mismatch in application:
21+ //│ ║ l.19: not oops
22+ //│ ║ ^^^^^^^^
23+ //│ ╟── type `~(int -> int)` is not an instance of type `bool`
24+ //│ ║ l.14: oops = 42 : ~(int -> int)
25+ //│ ║ ^^^^^^^^^^^^^
26+ //│ ╟── but it flows into reference with expected type `bool`
27+ //│ ║ l.19: not oops
28+ //│ ╙── ^^^^
29+ //│ res: bool | error
1730//│ = false
1831
1932
20- // * OTOH, this doesn't lead to immediate unsoundness:
33+ // * This was accepted but didn't immediately lead to immediate unsoundness:
2134def f: (~{x: int}) -> 'a
22- f = id
23- //│ f: in nothing -> nothing out ~{x: int} -> nothing
35+ //│ f: ~{x: int} -> nothing
2436//│ = <missing implementation>
37+
38+ :e
39+ f = id
2540//│ 'a -> 'a
2641//│ <: f:
27- //│ nothing -> nothing
42+ //│ ~{x: int} -> nothing
43+ //│ ╔══[ERROR] Type mismatch in def definition:
44+ //│ ║ l.39: f = id
45+ //│ ║ ^^^^^^
46+ //│ ╟── type `~{x: int}` does not match type `'a`
47+ //│ ║ l.34: def f: (~{x: int}) -> 'a
48+ //│ ║ ^^^^^^^^^^^
49+ //│ ╟── Note: constraint arises from type variable:
50+ //│ ║ l.34: def f: (~{x: int}) -> 'a
51+ //│ ╙── ^^
2852//│ = [Function: id]
2953
3054:e
@@ -33,48 +57,148 @@ f id
3357f {}
3458f (forall 'a. fun (x: 'a) -> x)
3559//│ ╔══[ERROR] Type mismatch in application:
36- //│ ║ l.31 : f 0
60+ //│ ║ l.55 : f 0
3761//│ ║ ^^^
3862//│ ╟── integer literal of type `0` does not match type `~{x: int}`
39- //│ ║ l.31 : f 0
63+ //│ ║ l.55 : f 0
4064//│ ║ ^
4165//│ ╟── Note: constraint arises from type negation:
42- //│ ║ l.21 : def f: (~{x: int}) -> 'a
66+ //│ ║ l.34 : def f: (~{x: int}) -> 'a
4367//│ ╙── ^^^^^^^^^^^
4468//│ res: error
4569//│ = 0
4670//│ ╔══[ERROR] Type mismatch in application:
47- //│ ║ l.32 : f id
71+ //│ ║ l.56 : f id
4872//│ ║ ^^^^
4973//│ ╟── reference of type `?a -> ?a` does not match type `~{x: int}`
50- //│ ║ l.32 : f id
74+ //│ ║ l.56 : f id
5175//│ ║ ^^
5276//│ ╟── Note: constraint arises from type negation:
53- //│ ║ l.21 : def f: (~{x: int}) -> 'a
77+ //│ ║ l.34 : def f: (~{x: int}) -> 'a
5478//│ ╙── ^^^^^^^^^^^
5579//│ res: error
5680//│ = [Function: id]
5781//│ ╔══[ERROR] Type mismatch in application:
58- //│ ║ l.33 : f {}
82+ //│ ║ l.57 : f {}
5983//│ ║ ^^^^
6084//│ ╟── record literal of type `anything` does not match type `~{x: int}`
61- //│ ║ l.33 : f {}
85+ //│ ║ l.57 : f {}
6286//│ ║ ^^
6387//│ ╟── Note: constraint arises from type negation:
64- //│ ║ l.21 : def f: (~{x: int}) -> 'a
88+ //│ ║ l.34 : def f: (~{x: int}) -> 'a
6589//│ ╙── ^^^^^^^^^^^
6690//│ res: error
6791//│ = {}
6892//│ ╔══[ERROR] Type mismatch in application:
69- //│ ║ l.34 : f (forall 'a. fun (x: 'a) -> x)
93+ //│ ║ l.58 : f (forall 'a. fun (x: 'a) -> x)
7094//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
7195//│ ╟── function of type `'a -> 'a` does not match type `~{x: int}`
72- //│ ║ l.34 : f (forall 'a. fun (x: 'a) -> x)
96+ //│ ║ l.58 : f (forall 'a. fun (x: 'a) -> x)
7397//│ ║ ^^^^^^^^^^^^^^^^
7498//│ ╟── Note: constraint arises from type negation:
75- //│ ║ l.21 : def f: (~{x: int}) -> 'a
99+ //│ ║ l.34 : def f: (~{x: int}) -> 'a
76100//│ ╙── ^^^^^^^^^^^
77101//│ res: error
78102//│ = [Function (anonymous)]
79103
80104
105+ // * Example 2 – now fixed
106+
107+ def g(x: 'a | {f: nothing}) = x.f(0)
108+ //│ g: {f: 0 -> 'a} -> 'a
109+ //│ = [Function: g]
110+
111+ :e
112+ foo = forall 'x. fun (x: 'x) -> g(x)
113+ //│ ╔══[ERROR] Type mismatch in application:
114+ //│ ║ l.112: foo = forall 'x. fun (x: 'x) -> g(x)
115+ //│ ║ ^^^^
116+ //│ ╟── expression of type `'x & ~{f: nothing}` does not have field 'f'
117+ //│ ╟── Note: constraint arises from field selection:
118+ //│ ║ l.107: def g(x: 'a | {f: nothing}) = x.f(0)
119+ //│ ║ ^^^
120+ //│ ╟── from type variable:
121+ //│ ║ l.107: def g(x: 'a | {f: nothing}) = x.f(0)
122+ //│ ╙── ^^
123+ //│ foo: anything -> error
124+ //│ = [Function: foo]
125+
126+ :re
127+ foo 0
128+ //│ res: error
129+ //│ Runtime error:
130+ //│ TypeError: x.f is not a function
131+
132+
133+
134+ // * Now let's consider why functions and classes can't intersect to nothing due to distributivity
135+
136+
137+ class Foo: { x: anything }
138+ //│ Defined class Foo
139+
140+
141+ // * These two types should be equivalent, but they visibly aren't:
142+
143+ def a: (int -> int | {x: int}) & Foo
144+ def b: int -> int & Foo | {x: int} & Foo
145+ //│ a: Foo
146+ //│ = <missing implementation>
147+ //│ b: Foo & {x: int}
148+ //│ = <missing implementation>
149+
150+ :ne
151+ ax = a.x
152+ bx = b.x
153+ //│ ax: anything
154+ //│ bx: int
155+
156+
157+ // * Yet, this does not immediately lead to unsoundness due to the aggressive normalization
158+ // * performed during constraint solving:
159+
160+ :ne
161+ a = b
162+ //│ Foo & {x: int}
163+ //│ <: a:
164+ //│ Foo
165+
166+ :e
167+ :ne
168+ b = a
169+ //│ Foo
170+ //│ <: b:
171+ //│ Foo & {x: int}
172+ //│ ╔══[ERROR] Type mismatch in def definition:
173+ //│ ║ l.168: b = a
174+ //│ ║ ^^^^^
175+ //│ ╟── expression of type `anything` is not an instance of type `int`
176+ //│ ╟── Note: constraint arises from type reference:
177+ //│ ║ l.144: def b: int -> int & Foo | {x: int} & Foo
178+ //│ ╙── ^^^
179+
180+
181+ // * To expose the unsoundness, we need some indirection with abstract types
182+ // * that prevent eagerly distributing the intersection type:
183+
184+ class Test1[A, B]: { f: A & Foo }
185+ method M: B & Foo | {x: int} & Foo
186+ //│ Defined class Test1[+A, +B]
187+ //│ Declared Test1.M: Test1[?, 'B] -> (Foo & 'B | Foo & {x: int})
188+
189+ class Test2[B]: Test1[B | {x: int}, B]
190+ method M = this.f : B & Foo | {x: int} & Foo
191+ //│ Defined class Test2[+B]
192+ //│ Defined Test2.M: Test2['B] -> (Foo & 'B | Foo & {x: int})
193+
194+ oops = (Test2{f = Foo{x = "oops"}} : Test1[anything, int -> int]).M
195+ //│ oops: Foo & {x: int}
196+ //│ = Foo { x: 'oops' }
197+
198+ // * Notice the type confusion:
199+ oops.x + 1
200+ //│ res: int
201+ //│ = 'oops1'
202+
203+
204+
0 commit comments