hkust-taco / mlscript

The MLscript programming language. Functional and object-oriented; structurally typed and sound; with powerful type inference. Soon to have full interop with TypeScript!
https://hkust-taco.github.io/mlscript
MIT License
175 stars 27 forks source link

Infinite loop in expanding abstract class with self type #209

Open Meowcolm024 opened 10 months ago

Meowcolm024 commented 10 months ago

The following code causes an infinite loop in type checking

abstract class Foo[T]: Bar { fun x: T }
abstract class Bar(val x: Int) extends Foo[Int] { fun f(y) = this.x + y }

fun test(f: Foo['a]) = if f is Foo then f.x
LPTK commented 10 months ago

Minimized:

abstract class Foo[T]: Foo[Int]
(f: Foo['a]) => f : Str

Minimized further (but the trace looks different):

abstract class Foo: Foo
(f: Foo) => f : Str
LPTK commented 10 months ago

Another one:

type Foo = Foo & Int
(f: Foo) => f : Str

We have to be more careful when we expand types during normalization...

LPTK commented 10 months ago

Note that this only happens on the "new parser/typer frontend" (https://github.com/hkust-taco/mlscript/pull/187). In the legacy frontend, we were careful to check for cycles in definitions and yielded "Error in class definitions: illegal cycle involving type Foo" for the latter example. We have to adapt these sorts of checks to the new frontend.

LPTK commented 9 months ago

Of course, we can also get unsoundness from such ill-formed types:

type A = A
//│ type A = A

(1 : A)()
//│ nothing
//│ res
//│ Runtime error:
//│   TypeError: 1 is not a function