Skip to content

Commit

Permalink
fix not a function error
Browse files Browse the repository at this point in the history
  • Loading branch information
@auht
auht committed Sep 15, 2024
1 parent 50afcc4 commit a540d00
Show file tree
Hide file tree
Showing 4 changed files with 108 additions and 59 deletions.
30 changes: 26 additions & 4 deletions shared/src/main/scala/mlscript/ConstraintSolver.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -629,8 +629,32 @@ class ConstraintSolver extends NormalForms { self: Typer =>
case (LhsRefined(S(b: ArrayBase), ts, r, _), _) => reportError()
case (LhsRefined(S(ov: Overload), ts, r, trs), RhsBases(_, S(L(f: FunctionType)), _)) if noApproximateOverload =>
TupleSetConstraints.mk(ov, f) match {
case S(tsc) => if (!tsc.tvs.isEmpty && tsc.constraints.isEmpty) reportError()
case N => reportError()
case S(tsc) =>
if (tsc.tvs.nonEmpty) {
tsc.tvs.mapValuesIter(_.unwrapProxies).zipWithIndex.flatMap {
case ((true, tv: TV), i) => tv.lowerBounds.iterator.map((_,tv,i,true))
case ((false, tv: TV), i) => tv.upperBounds.iterator.map((_,tv,i,false))
case _ => Nil
}.find {
case (b,_,i,_) =>
tsc.updateImpl(i,b)
tsc.constraints.isEmpty
}.foreach {
case (b,tv,_,p) => if (p) rec(b,tv,false) else rec(tv,b,false)
}
if (tsc.constraints.sizeCompare(1) === 0) {
tsc.tvs.values.map(_.unwrapProxies).foreach {
case tv: TV => tv.tsc.remove(tsc)
case _ => ()
}
tsc.constraints.head.iterator.zip(tsc.tvs).foreach {
case (c, (pol, t)) =>
if (!pol) rec(c, t, false)
if (pol) rec(t, c, false)
}
}
}
case N => reportError(S(msg"is not an instance of `${f.expNeg}`"))
}
case (LhsRefined(S(ov: Overload), ts, r, trs), _) =>
annoying(Nil, LhsRefined(S(ov.approximatePos), ts, r, trs), Nil, done_rs) // TODO remove approx. with ambiguous constraints
Expand Down Expand Up @@ -853,12 +877,10 @@ class ConstraintSolver extends NormalForms { self: Typer =>
}
}
u._2.foreach { k =>
println(s"tag5: ${k.tvs}")
k.constraints.head.iterator.zip(k.tvs).foreach {
case (c, (pol, t)) => if (pol) rec(t, c, false) else rec(c, t, false)
}
}
println(s"tag2: $u")
lhs.lowerBounds.foreach(rec(_, rhs, true)) // propagate from the bound

case (lhs, rhs: TypeVariable) if lhs.level <= rhs.level =>
Expand Down
22 changes: 5 additions & 17 deletions shared/src/main/scala/mlscript/TyperDatatypes.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -683,11 +683,11 @@ abstract class TyperDatatypes extends TyperHelpers { Typer: Typer =>
(u,l.reduce((x,y) => ComposedType(!p,x,y)(noProv)))
}
}
tvs.values.map(_.unwrapProxies).foreach {
case tv: TV => tv.tsc += this -> Set.empty
case _ => ()
}
if (!u.isEmpty) {
tvs.values.map(_.unwrapProxies).foreach {
case tv: TV => tv.tsc += this -> Set.empty
case _ => ()
}
tvs = u.flatMap(_.keys).distinct
constraints = tvs.map(x => u.map(_.getOrElse(x,if (x._1) TopType else BotType))).transpose
tvs.values.map(_.unwrapProxies).zipWithIndex.foreach {
Expand Down Expand Up @@ -721,6 +721,7 @@ abstract class TyperDatatypes extends TyperHelpers { Typer: Typer =>
}
def lcg(pol: Bool, first: ST, rest: ST)(implicit ctx: Ctx)
: Opt[Ls[(Bool, ST) -> ST]] = (first.unwrapProxies, rest.unwrapProxies) match {
case (a, ExtrType(p)) if p =/= pol => S(Nil)
case (a, ComposedType(p,l,r)) if p =/= pol =>
for {
lm <- lcg(pol,a,l)
Expand Down Expand Up @@ -781,24 +782,11 @@ abstract class TyperDatatypes extends TyperHelpers { Typer: Typer =>
tvs.mapValuesIter(_.unwrapProxies).zipWithIndex.foreach {
case ((true, tv: TV), i) =>
tv.tsc.updateWith(tsc)(_.map(_ + i).orElse(S(Set(i))))
tv.lowerBounds.foreach(tsc.updateImpl(i, _))
case ((false, tv: TV), i) =>
tv.tsc.updateWith(tsc)(_.map(_ + i).orElse(S(Set(i))))
tv.upperBounds.foreach(tsc.updateImpl(i, _))
case _ => ()
}
println(s"TSC mk: ${tsc.tvs} in ${tsc.constraints}")
if (tsc.constraints.sizeCompare(1) === 0) {
tvs.values.map(_.unwrapProxies).foreach {
case tv: TV => tv.tsc.remove(tsc)
case _ => ()
}
tsc.constraints.head.iterator.zip(tvs).foreach {
case (c, (pol, t)) =>
if (!pol) constrain(c, t)(raise, ov.prov, ctx)
if (pol) constrain(t, c)(raise, ov.prov, ctx)
}
}
S(tsc)
}
}
Expand Down
6 changes: 3 additions & 3 deletions shared/src/test/diff/fcp/Overloads.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ IISS : ZZII
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.30: IISS : ZZII
//│ ║ ^^^^
//│ ╟── type `int -> int & string -> string` is not a function
//│ ╟── type `int -> int & string -> string` is not an instance of `0 -> 0`
//│ ║ l.12: def IISS: int -> int & string -> string
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `0 -> 0`
Expand All @@ -50,7 +50,7 @@ IISS : BBNN
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.49: IISS : BBNN
//│ ║ ^^^^
//│ ╟── type `int -> int & string -> string` is not a function
//│ ╟── type `int -> int & string -> string` is not an instance of `bool -> bool`
//│ ║ l.12: def IISS: int -> int & string -> string
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `bool -> bool`
Expand Down Expand Up @@ -141,7 +141,7 @@ if true then IISS else BBNN
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.140: (if true then IISS else BBNN) : (0 | 1 | true) -> number
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── type `int -> int & string -> string` is not a function
//│ ╟── type `int -> int & string -> string` is not an instance of `(0 | 1 | true) -> number`
//│ ║ l.12: def IISS: int -> int & string -> string
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `(0 | 1 | true) -> number`
Expand Down
109 changes: 74 additions & 35 deletions shared/src/test/diff/nu/HeungTung.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ fun g = f
//│ ╔══[ERROR] Type mismatch in definition:
//│ ║ l.72: fun g = f
//│ ║ ^^^^^
//│ ╟── type `Int -> Int & Bool -> Bool` is not a function
//│ ╟── type `Int -> Int & Bool -> Bool` is not an instance of `(Int | false | true) -> (Int | false | true)`
//│ ║ l.51: fun f: (Int -> Int) & (Bool -> Bool)
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `(Int | false | true) -> (Int | false | true)`
Expand Down Expand Up @@ -104,7 +104,7 @@ fun j = f
//│ ╔══[ERROR] Type mismatch in definition:
//│ ║ l.103: fun j = f
//│ ║ ^^^^^
//│ ╟── type `Int -> Int & Bool -> Bool` is not a function
//│ ╟── type `Int -> Int & Bool -> Bool` is not an instance of `nothing -> nothing`
//│ ║ l.51: fun f: (Int -> Int) & (Bool -> Bool)
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `nothing -> nothing`
Expand Down Expand Up @@ -149,7 +149,7 @@ f(if true then 0 else false)
//│ ╔══[ERROR] Type mismatch in application:
//│ ║ l.148: f(if true then 0 else false)
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── type `Int -> Int & Bool -> Bool` is not a function
//│ ╟── type `Int -> Int & Bool -> Bool` is not an instance of `(0 | false) -> ?a`
//│ ║ l.51: fun f: (Int -> Int) & (Bool -> Bool)
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `(0 | false) -> ?a`
Expand All @@ -176,12 +176,9 @@ f(refined if true then 0 else false) // this one can be precise again!
//│ ╔══[ERROR] Type mismatch in application:
//│ ║ l.166: f(refined if true then 0 else false) // this one can be precise again!
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── type `Int -> Int & Bool -> Bool` is not a function
//│ ║ l.51: fun f: (Int -> Int) & (Bool -> Bool)
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `?a -> ?b`
//│ ╟── application of type `error` does not match type `?a`
//│ ║ l.166: f(refined if true then 0 else false) // this one can be precise again!
//│ ╙── ^
//│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ 'a
//│ where
//│ 'b :> error
Expand Down Expand Up @@ -242,7 +239,7 @@ type T = List[Int]
:e // TODO application types
type Res = M(T)
//│ ╔══[ERROR] Wrong number of type arguments – expected 0, found 1
//│ ║ l.243: type Res = M(T)
//│ ║ l.240: type Res = M(T)
//│ ╙── ^^^^
//│ type Res = M

Expand All @@ -265,21 +262,21 @@ fun f: Int -> Int
fun f: Bool -> Bool
fun f = id
//│ ╔══[ERROR] A type signature for 'f' was already given
//│ ║ l.265: fun f: Bool -> Bool
//│ ║ l.262: fun f: Bool -> Bool
//│ ╙── ^^^^^^^^^^^^^^^^^^^
//│ fun f: forall 'a. 'a -> 'a
//│ fun f: Int -> Int

:e // TODO support
f: (Int -> Int) & (Bool -> Bool)
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.274: f: (Int -> Int) & (Bool -> Bool)
//│ ║ l.271: f: (Int -> Int) & (Bool -> Bool)
//│ ║ ^
//│ ╟── type `Bool` is not an instance of type `Int`
//│ ║ l.274: f: (Int -> Int) & (Bool -> Bool)
//│ ║ l.271: f: (Int -> Int) & (Bool -> Bool)
//│ ║ ^^^^
//│ ╟── Note: constraint arises from type reference:
//│ ║ l.264: fun f: Int -> Int
//│ ║ l.261: fun f: Int -> Int
//│ ╙── ^^^
//│ Int -> Int & Bool -> Bool
//│ res
Expand Down Expand Up @@ -346,17 +343,17 @@ fun test(x) = refined if x is
A then 0
B then 1
//│ ╔══[WARNING] Paren-less applications should use the 'of' keyword
//│ ║ l.345: fun test(x) = refined if x is
//│ ║ l.342: fun test(x) = refined if x is
//│ ║ ^^^^^^^^^^^^^^^
//│ ║ l.346: A then 0
//│ ║ l.343: A then 0
//│ ║ ^^^^^^^^^^
//│ ║ l.347: B then 1
//│ ║ l.344: B then 1
//│ ╙── ^^^^^^^^^^
//│ ╔══[ERROR] Illegal use of reserved operator: refined
//│ ║ l.345: fun test(x) = refined if x is
//│ ║ l.342: fun test(x) = refined if x is
//│ ╙── ^^^^^^^
//│ ╔══[ERROR] identifier not found: refined
//│ ║ l.345: fun test(x) = refined if x is
//│ ║ l.342: fun test(x) = refined if x is
//│ ╙── ^^^^^^^
//│ fun test: (A | B) -> error
//│ Code generation encountered an error:
Expand Down Expand Up @@ -412,11 +409,11 @@ x => q(x)
:e
(x => q(x))(1):Int
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.413: (x => q(x))(1):Int
//│ ║ l.410: (x => q(x))(1):Int
//│ ║ ^^^^^^^^^^^^^^
//│ ╟── application of type `?a` does not match type `Int`
//│ ╟── Note: constraint arises from type reference:
//│ ║ l.413: (x => q(x))(1):Int
//│ ║ l.410: (x => q(x))(1):Int
//│ ╙── ^^^
//│ Int
//│ res
Expand All @@ -426,11 +423,11 @@ x => q(x)
:e
q(1):int
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.427: q(1):int
//│ ║ l.424: q(1):int
//│ ║ ^^^^
//│ ╟── application of type `?a` does not match type `int`
//│ ╟── Note: constraint arises from type reference:
//│ ║ l.427: q(1):int
//│ ║ l.424: q(1):int
//│ ╙── ^^^
//│ int
//│ res
Expand Down Expand Up @@ -460,7 +457,7 @@ fun r: Int -> Int & Bool -> Bool
x => r(r(x))
//│ ╔══[ERROR] ambiguous
//│ ╟── cannot determine satisfiability of type ?a
//│ ║ l.460: x => r(r(x))
//│ ║ l.457: x => r(r(x))
//│ ╙── ^^^^
//│ forall 'a 'b 'c. 'a -> 'c
//│ where
Expand All @@ -487,9 +484,9 @@ fun u: {x:0, y:Int} -> Int & {x:1, z: Str} -> Str
//│ fun u: {x: 0, y: Int} -> Int & {x: 1, z: Str} -> Str

(a, b, c) => u({x: a, y: b, z: c})
//│ forall 'a 'b 'c 'd. ('a, 'd, 'b) -> 'c
//│ forall 'a 'b 'c 'd. ('a, 'c, 'd) -> 'b
//│ where
//│ [+'b, -'c, +'a, +'d] in {[anything, Int, 0, Int], [Str, Str, 1, anything]}
//│ [-'b, +'a, +'c, +'d] in {[Int, 0, Int, anything], [Str, 1, anything, Str]}
//│ res
//│ = <no result>
//│ u is not implemented
Expand All @@ -516,11 +513,11 @@ let g = x => s(r(x))
:e
g(0)
//│ ╔══[ERROR] Type mismatch in application:
//│ ║ l.517: g(0)
//│ ║ l.514: g(0)
//│ ║ ^^^^
//│ ╟── expression of type `Int` does not match type `?a`
//│ ╟── Note: constraint arises from application:
//│ ║ l.507: let g = x => s(r(x))
//│ ║ l.504: let g = x => s(r(x))
//│ ╙── ^^^^
//│ error
//│ res
Expand Down Expand Up @@ -551,13 +548,13 @@ fun snd: A -> Int -> Int & Str -> Str -> Str
:e
x => app2(snd)(x):Int
//│ ╔══[ERROR] Type mismatch in type ascription:
//│ ║ l.552: x => app2(snd)(x):Int
//│ ║ l.549: x => app2(snd)(x):Int
//│ ║ ^^^^^^^^^^^^
//│ ╟── type `Int` is not an instance of type `A`
//│ ║ l.545: fun app2: ('a -> 'a -> 'a) -> 'a -> 'a
//│ ║ l.542: fun app2: ('a -> 'a -> 'a) -> 'a -> 'a
//│ ║ ^^
//│ ╟── Note: constraint arises from type reference:
//│ ║ l.548: fun snd: A -> Int -> Int & Str -> Str -> Str
//│ ║ l.545: fun snd: A -> Int -> Int & Str -> Str -> Str
//│ ╙── ^
//│ nothing -> Int
//│ res
Expand All @@ -571,7 +568,7 @@ app2_(snd)
//│ 'a -> 'b
//│ where
//│ 'a <: 'b
//│ [-'a, +'a, -'b] in {[Int, A & Int, Int], [Str, Str, Str]}
//│ [+'a, -'a, -'b] in {[A & Int, Int, Int], [Str, Str, Str]}
//│ res
//│ = <no result>
//│ snd is not implemented
Expand All @@ -594,13 +591,13 @@ fun f: (Str => Str) & ((Str, Int) => Int)
:e
f("abc", "abc")
//│ ╔══[ERROR] Type mismatch in application:
//│ ║ l.595: f("abc", "abc")
//│ ║ l.592: f("abc", "abc")
//│ ║ ^^^^^^^^^^^^^^^
//│ ╟── type `Str -> Str & (Str, Int) -> Int` is not a function
//│ ║ l.590: fun f: (Str => Str) & ((Str, Int) => Int)
//│ ╟── type `Str -> Str & (Str, Int) -> Int` is not an instance of `("abc", "abc") -> ?a`
//│ ║ l.587: fun f: (Str => Str) & ((Str, Int) => Int)
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `("abc", "abc") -> ?a`
//│ ║ l.595: f("abc", "abc")
//│ ║ l.592: f("abc", "abc")
//│ ╙── ^
//│ error
//│ res
Expand All @@ -612,3 +609,45 @@ f("abcabc")
//│ res
//│ = <no result>
//│ f is not implemented

:e
x => rt([not(x)])
//│ ╔══[ERROR] Type mismatch in application:
//│ ║ l.614: x => rt([not(x)])
//│ ║ ^^^^^^^^^^^^
//│ ╟── application of type `Bool` does not match type `?a`
//│ ║ l.614: x => rt([not(x)])
//│ ╙── ^^^^^^
//│ forall 'a 'b. Bool -> 'a
//│ where
//│ 'b :> Bool
//│ 'a :> error
//│ [-'a, +'b] in {}
//│ res
//│ = <no result>
//│ rt is not implemented

:e
rt(0)
//│ ╔══[ERROR] Type mismatch in application:
//│ ║ l.631: rt(0)
//│ ║ ^^^^^
//│ ╟── type `{0: Int} -> Int & {0: Str} -> Str` is not an instance of `0 -> ?a`
//│ ║ l.527: fun rt: {0: Int} -> Int & {0: Str} -> Str
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── but it flows into reference with expected type `0 -> ?a`
//│ ║ l.631: rt(0)
//│ ╙── ^^
//│ error
//│ res
//│ = <no result>
//│ rt is not implemented

fun z: {0:Int} -> nothing & Str -> Str
//│ fun z: {0: Int} -> nothing & Str -> Str

z([1])
//│ nothing
//│ res
//│ = <no result>
//│ z is not implemented

0 comments on commit a540d00

Please sign in to comment.