Support for GADTs

shared/src/main/scala/mlscript/NewParser.scala

@@ -1147,7 +1147,7 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo
         }
         val lb = getTypeName("restricts")
         val ub = getTypeName("extends")
-
+        // TODO update `TypeParamInfo` to use lb and ub
         yeetSpaces match {
           case (COMMA, l0) :: _ =>
             consume

shared/src/main/scala/mlscript/NormalForms.scala

@@ -241,7 +241,14 @@ class NormalForms extends TyperDatatypes { self: Typer =>
       case (LhsTop, _) => false
       case (LhsRefined(b1, ts1, rt1, trs1), LhsRefined(b2, ts2, rt2, trs2)) =>
         b2.forall(b2 => b1.exists(_ <:< b2)) &&
-          ts2.forall(ts1) && rt1 <:< rt2 &&
+          ts2.forall {
+            case sk: SkolemTag => ts1(sk)
+            case tt: TraitTag => ts1(tt)
+            case Extruded(pol, sk) => !pol || ts1.exists { // find ? <: bot
+              case Extruded(true, _) => true
+              case _ => false
+            }
+          } && rt1 <:< rt2 &&
           trs2.valuesIterator.forall(tr2 => trs1.valuesIterator.exists(_ <:< tr2))
     }
     def isTop: Bool = isInstanceOf[LhsTop.type]

shared/src/main/scala/mlscript/NuTypeDefs.scala

@@ -1655,6 +1655,7 @@ class NuTypeDefs extends ConstraintSolver { self: Typer =>
                     println(s"baseClsImplemMembers ${baseClsImplemMembers}")
 
                     val newImplems = ttu.implementedMembers.map {
+                      // * transform type alias member to type member
                       case als: TypedNuAls => 
                         if (tparamFields.map(_._1.name).contains(als.name))
                           err(msg"Class type member '${als.name}' already exists", als.toLoc)

shared/src/test/diff/ecoop23/PolymorphicVariants.mls

@@ -143,7 +143,7 @@ mixin EvalExpr {
 }
 //│ mixin EvalExpr() {
 //│   super: {eval: ('a, Var) -> 'b}
-//│   this: {eval: ('a, ??A & 'A | ??A0 & 'A0) -> (Object | ~??A1 & ~??A2)}
+//│   this: {eval: ('a, ??A & 'A | ??A0 & 'A0) -> (Object | ~??A1)}
 //│   fun eval: ('a, 'b & (Add['A] | Mul['A0] | Numb | Var)) -> (Numb | 'b)
 //│ }
 
@@ -191,7 +191,7 @@ Test2.eval(Cons(["c", Abs("d", Var("d"))], Nil), Abs("a", Var("a")))
 //│   Error: non-exhaustive case expression
 
 Test2.eval(Cons(["a", Abs("d", Var("d"))], Nil), Add(Numb(1), Var("a")))
-//│ Abs[Var] & ??A | Add[Numb | Var] | Numb | Var
+//│ Abs[Var] & ??A | Add[Numb | Var] | Numb & ??A0 | Var
 //│ res
 //│     = Add {}
 
@@ -201,23 +201,23 @@ module Test3 extends EvalVar, EvalExpr, EvalLambda
 //│ }
 //│ where
 //│   'A :> 'b
-//│      <: Object | ~(??A0 & (??A1 | ??A2))
+//│      <: Object | ~(??A0 & ??A1)
 //│   'b :> App[nothing] | Abs[nothing] | Numb | Var | ??A0 & 'A | 'a
-//│   'a <: Add[Abs['A0] | App['A1] | 'a & (Object & ~#Abs & ~#App | ~#Abs & ~#App & ~??A3) | ~??A3] | Mul[Abs['A0] | App['A1] | 'a & (Object & ~#Abs & ~#App | ~#Abs & ~#App & ~??A4) | ~??A4] | Numb | Var
-//│   'A0 <: Abs['A0] | App['A1] | 'a & (Object & ~#Abs & ~#App | ~#Abs & ~#App & ~??A5) | ~??A5
-//│   'A1 <: Abs['A0 & (Abs['A0] | App['A1] | Object & 'a & ~#Abs & ~#App | ~??A6)] | Abs['A0] & ~#Abs | App['A1] | Object & 'a & ~#Abs & ~#App | ~??A7
+//│   'a <: Add[Abs['A0] | App['A1] | 'a & (Object & ~#Abs & ~#App | ~#Abs & ~#App & ~??A2) | ~??A2] | Mul[Abs['A0] | App['A1] | 'a & (Object & ~#Abs & ~#App | ~#Abs & ~#App & ~??A3) | ~??A3] | Numb | Var
+//│   'A0 <: Abs['A0] | App['A1] | 'a & (Object & ~#Abs & ~#App | ~#Abs & ~#App & ~??A4) | ~??A4
+//│   'A1 <: Abs['A0 & (Abs['A0] | App['A1] | Object & 'a & ~#Abs & ~#App | ~??A5)] | Abs['A0] & ~#Abs | App['A1] | Object & 'a & ~#Abs & ~#App | ~??A6
 
 Test3.eval(Cons(["c", Abs("d", Var("d"))], Nil), Abs("a", Var("a")))
 //│ 'a
 //│   where
-//│     'a :> App['a] | Abs['a] | Abs[Var] & ??A | Numb | Var
+//│     'a :> App['a] | Abs['a] | Abs[Var] & ??A | Numb | Var & ??A0
 //│ res
 //│     = Abs {}
 
 Test3.eval(Cons(["c", Abs("d", Var("d"))], Nil), App(Abs("a", Var("a")), Add(Numb(1), Var("c"))))
 //│ 'a
 //│   where
-//│     'a :> App['a] | Abs['a] | Abs[Var] & ??A | Add[Numb | Var] & ??A0 | Numb | Numb & ??A1 | Var
+//│     'a :> App['a] | Abs['a] | Abs[Var] & ??A | Add[Numb | Var] & ??A0 | Numb & ??A1 | Var & ??A2
 //│ res
 //│     = Add {}
 
@@ -228,7 +228,7 @@ module Test3 extends EvalVar, EvalLambda, EvalExpr
 //│ }
 //│ where
 //│   'A :> ??A0 & 'A0 | ??A1 & 'A1 | 'a
-//│      <: Object | ~(??A2 & (??A3 | ??A4))
+//│      <: Object | ~(??A2 & ??A3)
 //│   'a :> Abs[nothing] | App[nothing] | Numb | Var | ??A0 & 'A0 | ??A1 & 'A1 | ??A2 & 'A
 //│   'A0 <: Add['A0] | Mul['A1] | Numb | Var | ~??A0
 //│   'A1 <: Add['A0] | Mul['A1] | Numb | Var | ~??A1
@@ -249,9 +249,9 @@ Test3.eval(Cons(["c", Abs("d", Var("d"))], Nil), Abs("a", Var("a")))
 //│ ╟── from reference:
 //│ ║  l.137: 	    let vv = map_expr(eta, v)
 //│ ╙──       	                           ^
-//│ Abs[Var] | error | 'a
+//│ Abs[Var] | Numb | error | 'a
 //│   where
-//│     'a :> Abs[Var | 'a] | Abs[Var] & ??A | App['a] | Numb | Var
+//│     'a :> Abs[Var | 'a] | App['a] | Var | ??A & (Abs[Var] | Numb)
 //│ res
 //│ Runtime error:
 //│   Error: non-exhaustive case expression

shared/src/test/diff/ecoop23/SimpleRegionDSL_raw.mls

@@ -344,9 +344,9 @@ module TestElim extends Eliminate
 //│   'Region3 <: Intersect['Region] | Outside['Region0] | Scale['Region1] | Translate['Region2] | Union['Region3] | 'a & (Object & ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union | ~#Intersect & ~#Outside & ~#Scale & ~#Translate & ~#Union & ~??Region4) | ~??Region4
 
 TestElim.eliminate(Outside(Outside(Univ())))
-//│ Univ & ??Region | Univ & ??Region0 | 'a
+//│ Univ & ??Region | 'a
 //│   where
-//│     'a :> Univ & ??Region | Univ & ??Region0 | Scale[Univ & ??Region | Univ & ??Region0 | 'a] | Outside[Univ & ??Region | Univ & ??Region0 | 'a] | Union[Univ & ??Region | Univ & ??Region0 | 'a] | Intersect[Univ & ??Region | Univ & ??Region0 | 'a] | Translate[Univ & ??Region | Univ & ??Region0 | 'a]
+//│     'a :> Univ & ??Region | Scale[Univ & ??Region | 'a] | Outside[Univ & ??Region | 'a] | Union[Univ & ??Region | 'a] | Intersect[Univ & ??Region | 'a] | Translate[Univ & ??Region | 'a]
 //│ res
 //│     = Univ {}
 

shared/src/test/diff/fcp-lit/QML.mls

@@ -510,7 +510,7 @@ def step = fun xx -> xx (fun ((((xinit, xsub), xupdate), xfold),) ->
 
 let mkArray n = if n == 0 then base else step base in
   mkArray 1 (fun ((((xinit, xsub), xupdate), xfold),) -> xinit 2)
-//│ res: ??r | ??r0
+//│ res: ??r
 //│    = [ 2, 2 ]
 
 def mkArray : int -> ExSig

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

@@ -52,7 +52,7 @@ r1 id
 //│ ╟── Note: constraint arises from type variable:
 //│ ║  l.18: 	def foo: forall 'x. ('x -> 'x, 'x -> 'x)
 //│ ╙──      	                               ^^
-//│ res: error | 'a -> 'a | ??y
+//│ res: ??y
 
 :e
 r2 id
@@ -72,6 +72,6 @@ r2 id
 //│ ╟── Note: constraint arises from type variable:
 //│ ║  l.18: 	def foo: forall 'x. ('x -> 'x, 'x -> 'x)
 //│ ╙──      	                               ^^
-//│ res: error | 'a -> 'a | ??y
+//│ res: ??y
 
 

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

@@ -254,7 +254,7 @@ sb (fun arr1 -> sb (fun arr2 -> arr2.Update (arr1.Init true)))
 //│ ╟── Note: constraint arises from application:
 //│ ║  l.234: 	sb (fun arr1 -> sb (fun arr2 -> arr2.Update (arr1.Init true)))
 //│ ╙──       	                                             ^^^^^^^^^^^^^^
-//│ res: error | int -> anything -> (??Rep | ??Rep0)
+//│ res: error | int -> anything -> ??Rep
 //│    = [Function (anonymous)]
 
 sb (fun arr ->
@@ -270,20 +270,20 @@ sb (fun arr ->
 
 :e
 def simpleStep arr = arr (fun impl -> fun k -> k (simpleStepImpl impl))
-//│ ((forall 'Rep 'a 'A 'c 'A0 'd 'Rep0 'A1. ArraysRep[in 'A1 & 'A & 'A0 out 'A | 'A1, in 'Rep0 & 'Rep & 'c out 'Rep0 | 'Rep] -> ((forall 'Rep1. ArraysImpl['A0, 'Rep1] with {
-//│   fold: forall 'b. ('A -> 'b -> 'b) -> 'b -> (('Rep, anything,),) -> 'b,
-//│   init: 'A1 -> ('Rep0, "initialized",),
-//│   sub: (('Rep, anything,),) -> int -> 'A,
-//│   update: forall 'e. (('Rep & 'e, anything,),) -> int -> 'A1 -> ('Rep0 | 'e, "updated",)
-//│ }) -> 'a) -> 'a) -> 'f) -> 'f
+//│ ((forall 'Rep 'A 'Rep0 'a 'c 'A0 'A1 'd. ArraysRep[in 'A & 'A1 & 'A0 out 'A1 | 'A, in 'Rep & 'Rep0 & 'a out 'Rep | 'Rep0] -> ((forall 'Rep1. ArraysImpl['A0, 'Rep1] with {
+//│   fold: forall 'b. ('A1 -> 'b -> 'b) -> 'b -> (('Rep0, anything,),) -> 'b,
+//│   init: 'A -> ('Rep, "initialized",),
+//│   sub: (('Rep0, anything,),) -> int -> 'A1,
+//│   update: forall 'e. (('Rep0 & 'e, anything,),) -> int -> 'A -> ('Rep | 'e, "updated",)
+//│ }) -> 'c) -> 'c) -> 'f) -> 'f
 //│ where
-//│   'Rep1 :> ('Rep0 | 'd, "initialized" | "updated",)
-//│         <: ('Rep & 'c, anything,)
-//│   'c <: 'Rep & 'd
-//│   'd :> 'Rep0
-//│      <: 'Rep & 'c
-//│   'A0 :> 'A
-//│       <: 'A1
+//│   'Rep1 :> ('Rep | 'd, "initialized" | "updated",)
+//│         <: ('Rep0 & 'a, anything,)
+//│   'a <: 'Rep0 & 'd
+//│   'd :> 'Rep
+//│      <: 'Rep0 & 'a
+//│   'A0 :> 'A1
+//│       <: 'A
 //│   <:  simpleStep:
 //│ Arrays['a] -> Arrays['a]
 //│ ╔══[ERROR] Type error in def definition
@@ -383,10 +383,10 @@ def stepImpl arrImpl = ArraysImpl {
     fold = fun f -> fun b -> fun ((r0, r1)) -> arrImpl.Fold f (arrImpl.Fold f b r0) r1
   }
 //│ stepImpl: ArraysRep[in 'A & 'A0 & 'A1 out 'A0 | 'A, in 'Rep & 'Rep0 & 'a & 'c out 'Rep | 'Rep0] -> (ArraysImpl['A1, 'Rep1] with {
-//│   fold: forall 'b 'b0. ('A0 -> 'b0 -> 'b0 & 'A0 -> 'b -> ('b0 & 'b)) -> ('b0 & 'b) -> (('Rep0, 'Rep0,),) -> 'b0,
+//│   fold: forall 'b 'b0. ('A0 -> 'b -> 'b & 'A0 -> 'b0 -> ('b & 'b0)) -> ('b & 'b0) -> (('Rep0, 'Rep0,),) -> 'b,
 //│   init: 'A -> ('Rep, 'Rep,),
 //│   sub: (('Rep0, 'Rep0,),) -> int -> 'A0,
-//│   update: forall 'd 'e. (('Rep0 & 'd, 'Rep0 & 'e,),) -> int -> 'A -> ('Rep | 'd, 'Rep | 'e,)
+//│   update: forall 'd 'e. (('Rep0 & 'e, 'Rep0 & 'd,),) -> int -> 'A -> ('Rep | 'e, 'Rep | 'd,)
 //│ })
 //│ where
 //│   'Rep1 :> ('Rep | 'a | 'f, 'Rep | 'c | 'g,)
@@ -407,11 +407,11 @@ def step: Arrays['a] -> Arrays['a]
 //│     = <missing implementation>
 
 def step arr = arr (fun impl -> fun (k: ArraysRepConsumer['a, 'r]) -> k (stepImpl impl))
-//│ ((forall 'Rep 'a 'A 'A0 'A1. ArraysRep[in 'A & 'A0 & 'A1 out 'A | 'A0, 'Rep] -> ArraysRepConsumer['A, 'a] -> 'a) -> 'b) -> 'b
+//│ ((forall 'A 'A0 'Rep 'a 'A1. ArraysRep[in 'A1 & 'A & 'A0 out 'A1 | 'A, 'Rep] -> ArraysRepConsumer['A1, 'a] -> 'a) -> 'b) -> 'b
 //│   where
-//│     'A :> 'A0
-//│        <: 'A1
-//│     'A1 <: 'A
+//│     'A1 :> 'A
+//│         <: 'A0
+//│     'A0 <: 'A1
 //│   <:  step:
 //│ Arrays['a] -> Arrays['a]
 //│     = [Function: step]
@@ -462,7 +462,7 @@ snb = mkMonoArray 5
 //│    = [Function (anonymous)]
 
 snb (fun arr -> arr.Init true)
-//│ res: ??Rep | ??Rep0
+//│ res: ??Rep
 //│    = [
 //│        [ [ [Array], [Array] ], [ [Array], [Array] ] ],
 //│        [ [ [Array], [Array] ], [ [Array], [Array] ] ]
@@ -479,7 +479,7 @@ snb = mkMonoArray 5
 //│    = [Function (anonymous)]
 
 snb (fun arr -> arr.Init true)
-//│ res: ??Rep | ??Rep0
+//│ res: ??Rep
 //│    = [ [ [ [Array], 'initialized' ], 'initialized' ], 'initialized' ]
 
 

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

@@ -195,7 +195,7 @@ snb = mkMonoArray 3
 
 // * Here we are trying to leak the internally-quantified representation, resulting in `anything` being returned
 snb (fun arr -> arr.init true)
-//│ res: ??rep | ??rep0
+//│ res: ??rep
 //│    = [ [ [ true, 'hi' ], 'hi' ], 'hi' ]
 
 
@@ -266,7 +266,7 @@ snb = mkMonoArray 3
 
 // * Here we are trying to leak the internally-quantified representation, resulting in `anything` being returned
 snb (fun arr -> arr.init true)
-//│ res: ??rep | ??rep0
+//│ res: ??rep
 //│    = [ [ [ true, 'hi' ], 'hi' ], 'hi' ]
 
 
@@ -363,20 +363,20 @@ def step arr = arr (forall 'a. fun impl -> forall 'r. fun (k: ArraysImplConsumer
 
 // * ...unless we use `stepImpl_ty` instead of `stepImpl`
 def step arr = arr (fun impl -> forall 'r. fun (k: ArraysImplConsumer['a, 'r]) -> k (stepImpl_ty impl))
-//│ ((forall 'r 'a 'r0 'a0 'a1. ArraysImpl[in 'a0 & 'a1 out 'a0 | 'a1, 'r0] -> ArraysImplConsumer['a, 'r] -> 'r) -> 'b) -> 'b
+//│ ((forall 'a 'a0 'r 'r0 'a1. ArraysImpl[in 'a & 'a0 out 'a | 'a0, 'r] -> ArraysImplConsumer['a1, 'r0] -> 'r0) -> 'b) -> 'b
 //│   where
-//│     'a :> 'a0
-//│        <: 'a1
+//│     'a1 :> 'a
+//│         <: 'a0
 //│   <:  step:
 //│ Arrays['a] -> Arrays['a]
 //│     = [Function: step8]
 
 
 def step arr = arr (fun impl -> (fun k -> k (stepImpl impl)) : Arrays['a])
-//│ ((forall 'a 'a0 'r. ArraysImpl[in 'a out 'a | 'a0, 'r] -> Arrays['a]) -> 'b) -> 'b
+//│ ((forall 'a 'a0 'r. ArraysImpl[in 'a & 'a0 out 'a, 'r] -> Arrays['a0]) -> 'b) -> 'b
 //│   where
-//│     'a := 'a0
-//│     'a0 :> 'a
+//│     'a :> 'a0
+//│     'a0 := 'a
 //│   <:  step:
 //│ Arrays['a] -> Arrays['a]
 //│     = [Function: step9]

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

@@ -482,7 +482,7 @@ snb = mkMonoArray 3
 
 // * Here we are trying to leak the internally-quantified representation, resulting in extruded types being returned
 snb (fun arr -> arr.init true)
-//│ res: ??rep | ??rep0
+//│ res: ??rep
 //│    = [ [ [ true, 'hi' ], 'hi' ], 'hi' ]
 
 
@@ -583,19 +583,19 @@ def s arr (k: ArraysImplConsumer['a, 'rep]) = arr (fun impl -> k (stepImpl_ty im
 // * We can see it shouldn't be simplified to nothing:
 :ns
 s
-//│ res: forall 'b 'a 'a0 'rep 'c. 'c -> (forall 'd 'a1 'rep0. ArraysImplConsumer['a1, 'rep0] -> 'd)
+//│ res: forall 'a 'b 'c 'rep 'a0. 'b -> (forall 'd 'a1 'rep0. ArraysImplConsumer['a1, 'rep0] -> 'd)
 //│   where
-//│     'd :> 'b
+//│     'd :> 'c
 //│     'rep0 <: 'rep
-//│     'a1 :> 'a0
-//│         <: 'a
-//│     'c <: (forall 'e 'a2 'f 'r. 'e -> 'f) -> 'b
+//│     'a1 :> 'a
+//│         <: 'a0
+//│     'b <: (forall 'e 'a2 'f 'r. 'e -> 'f) -> 'c
 //│     'f :> 'rep
 //│     'e <: ArraysImpl['a2, 'r]
-//│     'a2 :> 'a
-//│         <: 'a0
-//│     'a <: 'a0
+//│     'a2 :> 'a0
+//│         <: 'a
 //│     'a0 <: 'a
+//│     'a <: 'a0
 //│    = [Function: s]
 
 // * BTW: this doesn't work (same reason as before: k needs an annotation)
@@ -650,7 +650,7 @@ snb = mkMonoArray 3
 
 // * Here we are trying to leak the internally-quantified representation, resulting in extruded types being returned
 snb (fun arr -> arr.init true)
-//│ res: ??rep | ??rep0
+//│ res: ??rep
 //│    = [ [ [ true, 'hi' ], 'hi' ], 'hi' ]
 
 

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

@@ -187,7 +187,7 @@ snb.use of impl =>
 // * Here we are trying to leak the internally-quantified representation, resulting in the `??rep` extrusion
 snb.use of impl => impl.init(true)
 // :d
-//│ true | ??rep
+//│ ??rep
 //│ res
 //│     = [
 //│         [ [ true, true ], [ true, true ] ],
@@ -329,7 +329,7 @@ snb.use of impl =>
 //│ ]
 
 snb.use of impl => impl.init(true)
-//│ true | ??rep
+//│ ??rep
 //│ res
 //│     = [
 //│         [ [ true, true ], [ true, true ] ],