Support for GADTs

shared/src/main/scala/mlscript/ConstraintSolver.scala

@@ -1426,8 +1426,11 @@ class ConstraintSolver extends NormalForms { self: Typer =>
             WildcardArg(extrude(lb, lowerLvl, false, upperLvl), extrude(ub, lowerLvl, true, upperLvl))(tr.prov)
           case (N, targ: ST) =>
             // * Note: the semantics of TypeBounds is inappropriuate for this use (known problem; FIXME later)
-            // TypeBounds.mk(extrude(targ, lowerLvl, false, upperLvl), extrude(targ, lowerLvl, true, upperLvl)) // Q: ? subtypes?
-            WildcardArg(extrude(targ, lowerLvl, false, upperLvl), extrude(targ, lowerLvl, true, upperLvl))(tr.prov)
+            // * use TypeBounds for type alias
+            if (ctx.tyDefs2.get(d.name).map(_.decl.kind === Als).getOrElse(false))
+              TypeBounds.mk(extrude(targ, lowerLvl, false, upperLvl), extrude(targ, lowerLvl, true, upperLvl)) // Q: ? subtypes?
+            else 
+              WildcardArg(extrude(targ, lowerLvl, false, upperLvl), extrude(targ, lowerLvl, true, upperLvl))(tr.prov)
             // * A sanity-checking version, making sure the type range is correct (LB subtype of UB):
             /* 
             val a = extrude(targ, lowerLvl, false, upperLvl)

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

@@ -1110,9 +1110,8 @@ abstract class TyperHelpers { Typer: Typer =>
             assert(td.tparams.size === targs.size)
             subst(td.body, td.tparams.lazyZip(targs).map {
               case (tp, w: WildcardArg) => 
-                // * FIXME we should NOT use TypeBounds here (somehow causes infinite subtyping loop)
-                // *       but raising an error will break a lot of  code related to alias (maybe changling `subst`)
-                SkolemTag(tp._2)(noProv) -> TypeBounds(w.lb, w.ub)(w.prov)
+                // SkolemTag(tp._2)(noProv) -> TypeBounds(w.lb, w.ub)(w.prov)
+                ??? // TODO raise proper error
               case (tp, st: ST) => SkolemTag(tp._2)(noProv) -> st
             }.toMap)
           case S(td: TypedNuTrt) =>

shared/src/test/diff/nu/Jonathan.mls

@@ -39,7 +39,7 @@ fun f(x) = x : NonBlocking
 fun onMousePressed(listener) =
   let l(e) = listener(e) : NonBlocking
   l(0).flatMap of a => l(1).flatMap of b => pure of ()
-//│ fun onMousePressed: ((0 | 1) -> NonBlocking[?, ?]) -> Effectful[(), nothing]
+//│ fun onMousePressed: forall 'a. ((0 | 1) -> NonBlocking[anything, 'a]) -> Effectful[(), 'a & ~Block]
 
 
 // * OK: `println` does not block

shared/src/test/diff/nu/i180.mls

@@ -54,7 +54,7 @@ fun (:-) listExclude(xs, x) =
     Cons(x', xs') and
       x === x' then xs' :- x
       else x' :: (xs' :- x)
-//│ fun (:-) listExclude: forall 'A 'A0. (Cons['A] | Nil, Eql[?]) -> (Nil | List[in 'A0 out 'A0 | ??A & 'A])
+//│ fun (:-) listExclude: forall 'A. (Cons['A] | Nil, Eql[?]) -> (Nil | List[??A & 'A])
 
 (Nil :- 0).join(", ")
 ((0 :: Nil) :- 0).join(", ")

shared/src/test/diff/tapl/NuSimplyTyped.mls

@@ -150,30 +150,6 @@ fun typeTerm(t: Term, ctx: TreeMap[Type]): Result[Type, Str] =
         Err(message) then Err(message)
       Ok(PrimitiveType(name)) then Err("cannot apply primitive type `" ++ name ++ "`")
       Err(message) then Err(message)
-//│ ╔══[ERROR] Subtyping constraint of the form `?typeTerm <: (?a, ?b) -> ?c` exceeded recursion depth limit (250)
-//│ ║  l.142: 	    Abs(Var(name), ty, body) and typeTerm(body, insert(ctx, name, ty)) is
-//│ ║         	                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ╙── Note: use flag `:ex` to see internal error info.
-//│ TEST CASE FAILURE: There was an unexpected type error
-//│ ╔══[ERROR] Subtyping constraint of the form `([?a, ?b, ?c]) -> ?d <: ?e -> ?f` exceeded recursion depth limit (250)
-//│ ║  l.137: 	  if t is
-//│ ║         	     ^^^^
-//│ ║  l.138: 	    Lit(_, ty) then Ok(ty)
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.139: 	    Var(name) and find(ctx, name) is
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.140: 	      Some(ty) then Ok(ty)
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.141: 	      None then Err("unbound variable `" ++ name ++ "`")
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.142: 	    Abs(Var(name), ty, body) and typeTerm(body, insert(ctx, name, ty)) is
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.143: 	      Ok(resTy) then Ok(FunctionType(ty, resTy))
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.144: 	      Err(message) then Err(message)
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ╙── Note: use flag `:ex` to see internal error info.
-//│ TEST CASE FAILURE: There was an unexpected type error
 //│ fun typeTerm: (t: Term, ctx: TreeMap[Type]) -> Result[Type, Str]
 
 fun showTypeTerm(t, ctx) =

shared/src/test/diff/tapl/NuUntyped.mls

@@ -82,9 +82,15 @@ fun listConcat(xs, ys) =
   if xs is
     Nil then ys
     Cons(x, xs') then Cons(x, listConcat(xs', ys))
-//│ fun listConcat: forall 'A 'A0 'a. (Cons[out 'A & ('A0 | ~??A)] | Nil, List['A0] & 'a) -> (Cons['A0] | 'a)
+//│ fun listConcat: forall 'A 'A0 'A1 'A2 'a 'A3. (Cons[out 'A1 & ('A | ~??A)] | Nil, List[in 'A0 out 'A2] & 'a) -> (Cons[in 'A out 'A3] | 'a)
 //│   where
-//│     'A0 :> ??A & 'A
+//│     'A :> 'A3 | ??A & 'A1
+//│        <: 'A2
+//│     'A2 :> 'A3 | 'A0 | ??A & 'A1
+//│         <: 'A
+//│     'A3 :> 'A | 'A0 | ??A & 'A1
+//│     'A0 :> 'A3
+//│         <: 'A
 
 fun listContains(xs, x) =
   if xs is
@@ -248,27 +254,17 @@ fun fv(t) =
     Var(name) then list1(name)
     Abs(Var(name), body) then listWithout(fv(body), name)
     App(lhs, rhs) then listConcat(fv(lhs), fv(rhs))
-//│ ╔══[ERROR] Subtyping constraint of the form `?a -> (?b | ?c | ?d) <: ?fv` exceeded recursion depth limit (250)
-//│ ║  l.246: 	fun fv(t) =
-//│ ║         	    ^^^^^^^
-//│ ║  l.247: 	  if t is
-//│ ║         	^^^^^^^^^
-//│ ║  l.248: 	    Var(name) then list1(name)
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.249: 	    Abs(Var(name), body) then listWithout(fv(body), name)
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.250: 	    App(lhs, rhs) then listConcat(fv(lhs), fv(rhs))
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ╙── Note: use flag `:ex` to see internal error info.
-//│ TEST CASE FAILURE: There was an unexpected type error
-//│ fun fv: forall 'A 'A0 'A1 'A2. (Abs | App | Var) -> (Cons[in 'A out 'A0] | Cons['A1] | Nil)
+//│ fun fv: forall 'A 'A0 'A1 'A2 'A3 'A4 'A5. (Abs | App | Var) -> (Cons[in 'A5 out 'A2] | Cons[in 'A4 out 'A2] | Nil)
 //│   where
-//│     'A :> 'A0 | 'A1
-//│        <: 'A2
-//│     'A0 :> 'A | 'A1 | 'A2
-//│     'A2 :> 'A0 | 'A | 'A1
-//│         <: 'A
-//│     'A1 <: 'A
+//│     'A5 :> 'A2 | ??A & 'A2 | ??A0 & 'A2
+//│         <: 'A4 & ('A & 'A0 & ('A3 | ~??A) | ~??A0 & ('A3 | ~??A))
+//│     'A2 :> 'A5 | 'A1
+//│     'A1 :> Str & ??A & ??A0 | 'A2 | 'A5 | ??A & 'A2 | ??A0 & 'A2
+//│         <: 'A5 & 'A4 & ('A & 'A0 & ('A3 | ~??A) | ~??A0 & ('A3 | ~??A))
+//│     'A4 <: 'A5 & 'A1 & ('A & 'A0 & ('A3 | ~??A) | ~??A0 & ('A3 | ~??A))
+//│     'A <: 'A5 & 'A1 & 'A4 & ('A0 & ('A3 | ~??A) | ~??A0 & ('A3 | ~??A))
+//│     'A0 <: 'A5 & 'A1 & 'A4 & ('A & ('A3 | ~??A) | ~??A0 & ('A3 | ~??A))
+//│     'A3 <: 'A5 & 'A4 & ('A & 'A0 | ~??A0)
 :ResetFuel
 
 fun showFv(t) =

shared/src/test/diff/ucs/JSON.mls

@@ -104,10 +104,16 @@ fun listJoin(xs, sep) =
 //│ type List[A] = Cons[A] | Nil
 //│ module Nil
 //│ class Cons[A](head: A, tail: List[A])
-//│ fun listConcat: forall 'A 'A0 'a. (Cons[out 'A & ('A0 | ~??A)] | Nil, List['A0] & 'a) -> (Cons['A0] | 'a)
+//│ fun listConcat: forall 'A 'a 'A0 'A1 'A2 'A3. (Cons[out 'A2 & ('A0 | ~??A)] | Nil, List[in 'A3 out 'A1] & 'a) -> (Cons[in 'A0 out 'A] | 'a)
 //│ fun listJoin: (Cons[?] | Nil, Str) -> Str
 //│ where
-//│   'A0 :> ??A & 'A
+//│   'A0 :> 'A | ??A & 'A2
+//│       <: 'A1
+//│   'A1 :> 'A | 'A3 | ??A & 'A2
+//│       <: 'A0
+//│   'A :> 'A0 | 'A3 | ??A & 'A2
+//│   'A3 :> 'A
+//│       <: 'A0
 
 type TreeMap[out A] = Node[A] | Empty
 module Empty
@@ -131,28 +137,22 @@ fun traverse(t, f) =
     Empty then Nil
     Node(key, value, left, right) then
       listConcat(traverse(left, f), Cons(f(key, value), traverse(right, f)))
-//│ ╔══[ERROR] Subtyping constraint of the form `(?a, ?b) -> (?c | ?d) <: ?traverse` exceeded recursion depth limit (250)
-//│ ║  l.129: 	fun traverse(t, f) =
-//│ ║         	    ^^^^^^^^^^^^^^^^
-//│ ║  l.130: 	  if t is
-//│ ║         	^^^^^^^^^
-//│ ║  l.131: 	    Empty then Nil
-//│ ║         	^^^^^^^^^^^^^^^^^^
-//│ ║  l.132: 	    Node(key, value, left, right) then
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.133: 	      listConcat(traverse(left, f), Cons(f(key, value), traverse(right, f)))
-//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ╙── Note: use flag `:ex` to see internal error info.
-//│ TEST CASE FAILURE: There was an unexpected type error
 //│ type TreeMap[A] = Empty | Node[A]
 //│ module Empty
 //│ class Node[A](key: Str, value: A, left: TreeMap[A], right: TreeMap[A])
 //│ fun insert: forall 'A 'a 'A0. (Empty | Node['A], Str, 'a & 'A0) -> Node['a]
 //│ fun find: forall 'A1 'A2. (Empty | Node['A1], Str) -> (None | Some['A2 | ??A & 'A1])
-//│ fun traverse: forall 'A3 'A4 'A5. (Empty | Node['A3], (Str, ??A0 & 'A3) -> 'A4) -> (Cons['A5] | Nil)
+//│ fun traverse: forall 'A3 'A4 'A5 'A6 'A7 'A8 'A9 'A10. (Empty | Node['A5], (Str, ??A0 & 'A5) -> ('A7 & 'A9 & ('A6 & 'A4 | ~??A1))) -> (Cons[in 'A7 out 'A3] | Nil)
 //│ where
-//│   'A4 <: 'A5
-//│   'A5 <: 'A4
+//│   'A7 <: 'A10 & ('A6 & 'A4 | ~??A1) & 'A9
+//│   'A10 :> 'A3 | ??A1 & 'A3
+//│        <: 'A7 & ('A6 & 'A4 | ~??A1)
+//│   'A3 :> 'A10 | 'A8 | 'A9 & 'A7 & ('A6 & 'A4 | ~??A1) | 'A9
+//│   'A8 <: 'A7 & ('A6 & 'A4 | ~??A1) & 'A4 & ('A6 | ~??A1) & 'A9
+//│   'A6 <: 'A7 & ('A4 | ~??A1) & 'A9
+//│   'A9 :> 'A3 | 'A10 | 'A8 | ??A1 & 'A3
+//│       <: 'A7 & ('A6 & 'A4 | ~??A1)
+//│   'A4 <: 'A7 & 'A8 & ('A6 | ~??A1)
 
 type JsonValue = JsonNull | JsonNumber | JsonString | JsonBoolean | JsonObject | JsonArray
 module JsonNull {
@@ -175,11 +175,6 @@ class JsonObject(entries: TreeMap[JsonValue]) {
 class JsonArray(elements: List[JsonValue]) {
   fun toString() = concat3("[", listJoin(elements, ", "), "]")
 }
-//│ ╔══[ERROR] Subtyping constraint of the form `forall ?a ?b ?c ?d. (?b, ?c) -> (?d | ?a) <: (?e, forall ?f ?g ?h. (?h, ?g) -> ?f) -> ?i` exceeded recursion depth limit (250)
-//│ ║  l.173: 	      else concat3("{ ", listJoin(traverse(entries, (k, v) => concat3(k, ": ", getStringOf(v))), ", "), " }")
-//│ ║         	                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ╙── Note: use flag `:ex` to see internal error info.
-//│ TEST CASE FAILURE: There was an unexpected type error
 //│ type JsonValue = JsonArray | JsonBoolean | JsonNull | JsonNumber | JsonObject | JsonString
 //│ module JsonNull {
 //│   fun toString: () -> "null"
@@ -281,7 +276,7 @@ fun expectWord(scanner, word, result) =
         ParseFailure(concat3("there should not be other alphabets after\"", word, "\""), scanner)
       else
         ParseSuccess(result, scanner)
-//│ fun expectWord: forall 'T 'a 'T0 'T1 'T2. (Scanner & {peek: Object & ~#Some | Some[anything], advance: Scanner}, Str, 'a & 'T1 & 'T2) -> (ParseFailure | ParseSuccess['T1 & 'T2 & ('T & 'T0 | 'a)])
+//│ fun expectWord: forall 'T 'T0 'a 'T1 'T2. (Scanner & {peek: Object & ~#Some | Some[anything], advance: Scanner}, Str, 'a & 'T0 & 'T) -> (ParseFailure | ParseSuccess['T0 & 'T & ('T2 & 'T1 | 'a)])
 
 // If we put this function together with the next block, there will be type
 // mismatch errors.
@@ -291,7 +286,7 @@ fun parseMatched(scanner, closingSymbol, parse, fn) =
       ParseSuccess(_, scanner) then ParseSuccess(fn(outcome), scanner)
       ParseFailure(message, scanner) then ParseFailure(message, scanner)
     ParseFailure(message, scanner) then ParseFailure(message, scanner)
-//│ fun parseMatched: forall 'T 'T0 'advance. ({advance: 'advance}, Str, 'advance -> (ParseFailure | ParseSuccess['T]), (??T & 'T) -> 'T0) -> (ParseFailure | ParseSuccess['T0])
+//│ fun parseMatched: forall 'advance 'T 'T0. ({advance: 'advance}, Str, 'advance -> (ParseFailure | ParseSuccess['T]), (??T & 'T) -> 'T0) -> (ParseFailure | ParseSuccess['T0])
 
 :ng
 fun parseEntries(scanner): ParseResult[TreeMap[JsonValue]] = error
@@ -328,7 +323,7 @@ fun parse(scanner) =
 //│ fun parseElements: Scanner -> ParseResult[List[JsonValue]]
 //│ fun parseStringContent: anything -> ParseResult[Str]
 //│ fun parseNumber: anything -> ParseResult[JsonNumber]
-//│ fun parse: forall 'T 'T0 'T1 'T2 'T3 'T4. Scanner -> (forall 'T5 'T6 'T7 'T8 'T9 'T10 'T11 'T12 'T13. ParseFailure | ParseSuccess[JsonObject & 'T7 & 'T11 & 'T5 & 'T4 & 'T10 & 'T0 & 'T8 & 'T & 'T13 & 'T1 & 'T6 & 'T2 & 'T9 & 'T3 | 'T12 & (JsonArray & 'T11 & 'T5 & 'T4 & 'T10 & 'T0 & 'T8 & 'T & 'T13 & 'T1 & 'T6 & 'T2 & 'T9 & 'T3 | 'T7 & (JsonString & 'T5 & 'T4 & 'T10 & 'T0 & 'T8 & 'T & 'T13 & 'T1 & 'T6 & 'T2 & 'T9 & 'T3 | 'T11 & (JsonBoolean & 'T6 & 'T2 & 'T9 & 'T3 | 'T5 & 'T4 & 'T10 & 'T0 & 'T8 & 'T & 'T13 & 'T1 & (JsonNull | 'T6 & 'T2 & 'T9 & 'T3))))] | ParseResult[JsonNumber])
+//│ fun parse: forall 'T 'T0 'T1 'T2 'T3 'T4. Scanner -> (forall 'T5 'T6 'T7 'T8 'T9 'T10 'T11 'T12 'T13. ParseFailure | ParseSuccess[JsonObject & 'T12 & 'T9 & 'T8 & 'T4 & 'T11 & 'T1 & 'T5 & 'T2 & 'T10 & 'T3 & 'T6 & 'T0 & 'T13 & 'T | 'T7 & (JsonArray & 'T9 & 'T8 & 'T4 & 'T11 & 'T1 & 'T5 & 'T2 & 'T10 & 'T3 & 'T6 & 'T0 & 'T13 & 'T | 'T12 & (JsonString & 'T8 & 'T4 & 'T11 & 'T1 & 'T5 & 'T2 & 'T10 & 'T3 & 'T6 & 'T0 & 'T13 & 'T | 'T9 & (JsonBoolean & 'T6 & 'T0 & 'T13 & 'T | 'T8 & 'T4 & 'T11 & 'T1 & 'T5 & 'T2 & 'T10 & 'T3 & (JsonNull | 'T6 & 'T0 & 'T13 & 'T))))] | ParseResult[JsonNumber])
 
 :ng
 toString of parse of scan of "    true"