Changes from meeting

Author: LPTK

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

@@ -849,15 +849,15 @@ class ConstraintSolver extends NormalForms { self: Typer =>
             }
             val u = lhs.tsc.filter(_._1.constraints.sizeCompare(1) === 0)
             u.foreachEntry { case (k, _) =>
-              k.tvs.foreach {
+              k.tvs.mapValues(_.unwrapProxies).foreach { // TODO less inefficient; remove useless case
                 case (_,tv: TV) => tv.tsc.remove(k)
                 case (_,ProvType(tv: TV)) => tv.tsc.remove(k)
                 case _ => ()
               }
             }
             u.foreachEntry { case (k, _) =>
               k.constraints.head.zip(k.tvs).foreach {
-                case (c, (pol, t)) => if (pol) rec(t, c, true) else rec(c, t, true)
+                case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false)
               }
             }
             lhs.lowerBounds.foreach(rec(_, rhs, true)) // propagate from the bound
@@ -877,15 +877,15 @@ class ConstraintSolver extends NormalForms { self: Typer =>
             }
             val u = rhs.tsc.filter(_._1.constraints.sizeCompare(1) === 0)
             u.foreachEntry { case (k, _) =>
-              k.tvs.foreach {
+              k.tvs.mapValues(_.unwrapProxies).foreach { // TODO less inefficient; remove useless case
                 case (_,tv: TV) => tv.tsc.remove(k)
                 case (_,ProvType(tv: TV)) => tv.tsc.remove(k)
                 case _ => ()
               }
             }
             u.foreachEntry { case (k, _) =>
               k.constraints.head.zip(k.tvs).foreach {
-                case (c, (pol, t)) => if (pol) rec(t, c, true) else rec(c, t, true)
+                case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false)
               }
             }
             rhs.upperBounds.foreach(rec(lhs, _, true)) // propagate from the bound

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

@@ -109,9 +109,9 @@ f(0) + 1
 //│ ╟── type `number` is not an instance of type `int`
 //│ ║  l.13: 	def BBNN: bool -> bool & number -> number
 //│ ║        	                                   ^^^^^^
-//│ ╟── but it flows into integer literal with expected type `int`
+//│ ╟── but it flows into application with expected type `int`
 //│ ║  l.105: 	f(0) + 1
-//│ ╙──       	  ^
+//│ ╙──       	^^^^
 //│ res: error | int
 
 f : int -> number

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

@@ -488,9 +488,7 @@ g(0)
 //│ ╔══[ERROR] Type mismatch in application:
 //│ ║  l.487: 	g(0)
 //│ ║         	^^^^
-//│ ╟── integer literal of type `Int` does not match type `?a`
-//│ ║  l.487: 	g(0)
-//│ ║         	  ^
+//│ ╟── expression of type `Int` does not match type `?a`
 //│ ╟── Note: constraint arises from application:
 //│ ║  l.477: 	let g = x => s(r(x))
 //│ ╙──       	               ^^^^
@@ -523,15 +521,14 @@ fun snd: A -> Int -> Int & Str -> Str -> Str
 :e
 x => app2(snd)(x):Int
 //│ ╔══[ERROR] Type mismatch in type ascription:
-//│ ║  l.524: 	x => app2(snd)(x):Int
+//│ ║  l.522: 	x => app2(snd)(x):Int
 //│ ║         	     ^^^^^^^^^^^^
-//│ ╟── application of type `Int` is not an instance of type `A`
+//│ ╟── type `Int` is not an instance of type `A`
+//│ ║  l.515: 	fun app2: ('a -> 'a -> 'a) -> 'a -> 'a
+//│ ║         	                       ^^
 //│ ╟── Note: constraint arises from type reference:
-//│ ║  l.520: 	fun snd: A -> Int -> Int & Str -> Str -> Str
-//│ ║         	         ^
-//│ ╟── from type reference:
-//│ ║  l.524: 	x => app2(snd)(x):Int
-//│ ╙──       	                  ^^^
+//│ ║  l.518: 	fun snd: A -> Int -> Int & Str -> Str -> Str
+//│ ╙──       	         ^
 //│ nothing -> Int
 //│ res
 //│     = <no result>