Skip to content

Commit

Permalink
Add a couple of useful tests
Browse files Browse the repository at this point in the history
  • Loading branch information
LPTK committed Apr 2, 2024
1 parent 69392b3 commit f6be56b
Show file tree
Hide file tree
Showing 2 changed files with 187 additions and 0 deletions.
152 changes: 152 additions & 0 deletions shared/src/test/diff/nu/FunnyPoly.mls
Original file line number Diff line number Diff line change
@@ -0,0 +1,152 @@
:NewDefs
:NoJS

// * A bunch of semi-random polymorphism and extrusion tests.
// * Some of them yield very ugly types. (They might improve once we use proper wildcard args.)
// * I've been trying to reproduce/trigger the incompleteness of constraint solving
// * for constraints like `MyClass[S] & ?b <: MyClass[T]` where ?b is a lower-level type variable.



fun test(x: (forall 'a: 'a -> 'a) & 'b) =
let foo(y) =
x(y)
foo
//│ fun test: forall 'a 'b 'c. (x: forall 'a0. 'a0 -> 'a0 & ~('a -> 'a) | 'a0 -> 'a0 & 'b -> 'c) -> 'b -> 'c


type Id = forall 'a: 'a -> 'a
//│ type Id = forall 'a. 'a -> 'a

fun test(x: Id & 'b) =
let foo(y) = x(y)
foo
//│ fun test: forall 'b 'c 'a. (x: Id & 'b -> 'c | Id & ~('a -> 'a)) -> 'b -> 'c

fun test(x: Int | 'b) =
let foo(y) = (if true then x else y) : (Int | 'c)
foo
//│ fun test: forall 'c. (x: Int | 'c) -> (forall 'c0. (Int | 'c0) -> (Int | 'c | 'c0))



class Ref[T](x: T -> T)
//│ class Ref[T](x: T -> T)

class MyClass[A](x: A -> A)
//│ class MyClass[A](x: A -> A)

// Note: precedence of & is lower than that of ->
fun mk: forall 'b: (Ref['b]) -> MyClass[Int] & 'b
// fun mk(x) = error
//│ fun mk: forall 'b. Ref['b] -> MyClass[Int] & 'b

(x, y) => mk(x, y)
//│ (anything, anything) -> nothing

fun mk: forall 'a, 'b: (Ref['a], Ref['b]) -> (MyClass['a] & 'b)
//│ fun mk: forall 'a 'b. (Ref['a], Ref['b]) -> (MyClass['a] & 'b)

fun test(x, y) = mk(x, y)
//│ fun test: forall 'a 'b. (Ref['a], Ref['b]) -> (MyClass['a] & 'b)

:ns
test
//│ forall 'c 'd 'e 'a 'b. ('c, 'd) -> 'e
//│ where
//│ 'e :> MyClass['a] & 'b
//│ 'd <: Ref['b]
//│ 'c <: Ref['a]



fun test(x, y) =
let tmp = mk(x, y)
tmp
//│ fun test: forall 'a 'b. (Ref['a], Ref['b]) -> (MyClass['a] & 'b)

fun test(x, y) =
let tmp = mk(x, y)
let foo(z) = mk(z, tmp)
foo
//│ fun test: forall 'a 'b 'b0. (Ref['a], Ref['b]) -> (forall 'a0. Ref['a0] -> (MyClass['a0] & 'b0))
//│ where
//│ 'b <: Ref[?] | Ref[?] & ~{MyClass#A = 'a} | Ref['b0] | ~MyClass['a]

fun test(x, y) =
let tmp = mk(x, y)
let foo(z) = mk(z, tmp) : MyClass['x]
foo
//│ fun test: forall 'a 'b 'b0 'a0 'a1 'a2 'x. (Ref['a], Ref['b]) -> (forall 'a3 'x0. Ref['a3] -> MyClass['x0])
//│ where
//│ 'x0 <: 'x
//│ 'a3 :> 'a2 | 'a1
//│ <: 'a0
//│ 'b <: Ref[?] | Ref[?] & ~{MyClass#A = 'a} | Ref[in 'b0 out 'b0 & (MyClass[?] & ~{MyClass#A :> 'a0 & 'a1} | MyClass[in 'x out nothing] | {MyClass#A :> 'x <: nothing} & ~{MyClass#A :> 'a2 <: 'a2 | 'a0} | ~#MyClass | ~{MyClass#A :> 'a2 & 'a0 & 'a1})] & {
//│ Ref#T :> 'b0 <: 'b0 & (MyClass[?] & ~{MyClass#A :> 'a0 & 'a1 <: 'a2 | 'a1} | MyClass[in 'x out nothing] | {MyClass#A = 'x} & ~{MyClass#A :> 'a2 <: 'a2 | 'a0} | ~#MyClass | ~{MyClass#A :> 'a2 & 'a0 & 'a1 <: 'a2 | 'a0 | 'a1})
//│ } | ~MyClass['a]

fun test(x, y) =
let tmp = mk(x, y)
let foo(z) = mk(z, tmp) : MyClass['x]
[tmp, foo]
//│ fun test: forall 'a 'b 'b0 'a0 'a1 'a2 'x. (Ref['a], Ref['b]) -> [MyClass['a] & 'b, forall 'a3 'x0. Ref['a3] -> MyClass['x0]]
//│ where
//│ 'x0 <: 'x
//│ 'a3 :> 'a2 | 'a1
//│ <: 'a0
//│ 'b <: Ref[?] | Ref[?] & ~{MyClass#A = 'a} | Ref[in 'b0 out 'b0 & (MyClass[?] & ~{MyClass#A :> 'a0 & 'a1} | MyClass[in 'x out nothing] | {MyClass#A :> 'x <: nothing} & ~{MyClass#A :> 'a2 <: 'a2 | 'a0} | ~#MyClass | ~{MyClass#A :> 'a2 & 'a0 & 'a1})] & {
//│ Ref#T :> 'b0 <: 'b0 & (MyClass[?] & ~{MyClass#A :> 'a0 & 'a1 <: 'a2 | 'a1} | MyClass[in 'x out nothing] | {MyClass#A = 'x} & ~{MyClass#A :> 'a2 <: 'a2 | 'a0} | ~#MyClass | ~{MyClass#A :> 'a2 & 'a0 & 'a1 <: 'a2 | 'a0 | 'a1})
//│ } | ~MyClass['a]



fun ref: 'a -> Ref['a]
//│ fun ref: forall 'a. 'a -> Ref['a]

fun test(x, y) =
let tmp = ref(mk(x, y))
let foo(z) = mk(z, tmp)
foo
//│ fun test: forall 'a 'b. (Ref['a], Ref['b]) -> (forall 'a0. Ref['a0] -> (MyClass[in 'a0 | 'a out 'a & 'a0] & 'b))

fun test(x, y) =
let tmp = ref(mk(x, y))
let foo(z) = mk(z, tmp) : MyClass['x]
foo
//│ fun test: forall 'a 'b 'a0 'a1 'a2 'a3 'x 'x0. (Ref['a], Ref['b]) -> (forall 'a4 'x1. Ref['a4] -> MyClass['x1])
//│ where
//│ 'x1 :> 'x0
//│ <: 'x
//│ 'a4 :> 'a2 | 'a1
//│ <: 'a0 & 'a3
//│ 'b <: MyClass[?] & ~{MyClass#A :> 'a0 & 'a1 | 'a <: 'a & ('a2 | 'a1 | 'a3)} | MyClass[in 'x out 'x & 'x0] | {MyClass#A :> 'x <: 'x & 'x0} & ~{MyClass#A :> 'a2 | 'a <: 'a & ('a2 | 'a0)} | ~MyClass[in 'a | 'a2 & ('a0 & 'a1 | 'a) out 'a & ('a2 | 'a0 | 'a1 | 'a3)]



fun refined: forall 'A, 'B: (r: 'A) -> ('A & Ref['B])
//│ fun refined: forall 'A 'B. (r: 'A) -> (Ref['B] & 'A)

fun test(x: 'x) =
let foo() = refined(x)
foo
//│ fun test: forall 'x. (x: 'x) -> (forall 'B. () -> (Ref['B] & 'x))

// fun refined: forall 'A, 'B, 'C: (r: 'A, s: 'B) -> ('A & 'B & Ref['C])
fun refined: forall 'A, 'B, 'C: (r: 'A, s: 'B) -> ('A & 'B)
//│ fun refined: forall 'A 'B. (r: 'A, s: 'B) -> ('A & 'B)

fun test(x: 'x) =
let foo(y: Ref['r] & 'y) = y
foo(x)
//│ fun test: forall 'r 'y. (x: Ref['r] & 'y) -> (Ref['r] & 'y)

fun test(x: 'x) =
let foo(y) = refined(x, y) : Ref['r]
foo
//│ fun test: forall 'B 'r. (x: Ref[?] & ~'B | Ref[in 'r out nothing] | ~'B) -> (forall 'r0. 'B -> Ref['r0])
//│ where
//│ 'r0 <: 'r



35 changes: 35 additions & 0 deletions shared/src/test/diff/nu/TupleParamBlunder.mls
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
:NewDefs


// * TODO fix the parsing of this tuple-taking function signature!
fun f: [Int, Int] -> Int
fun f(a, b) = a + b // should not be a valid implementation
//│ fun f: (Int, Int) -> Int
//│ fun f: (Int, Int) -> Int

fun f: (Int, Int) -> Int
fun f(a, b) = a + b
//│ fun f: (Int, Int) -> Int
//│ fun f: (Int, Int) -> Int

:e
fun f: [Int, Int] => Int
fun f(a, b) = a + b
//│ ╔══[ERROR] Type mismatch in definition:
//│ ║ l.17: fun f(a, b) = a + b
//│ ║ ^^^^^^^^^^^^^^^
//│ ╟── type `[[Int, Int]]` does not match type `[?a, ?b]`
//│ ║ l.16: fun f: [Int, Int] => Int
//│ ║ ^^^^^^^^^^
//│ ╟── Note: constraint arises from tuple literal:
//│ ║ l.17: fun f(a, b) = a + b
//│ ╙── ^^^^^^
//│ fun f: (Int, Int) -> Int
//│ fun f: ([Int, Int]) -> Int

fun f: (Int, Int) => Int
fun f(a, b) = a + b
//│ fun f: (Int, Int) -> Int
//│ fun f: (Int, Int) -> Int


0 comments on commit f6be56b

Please sign in to comment.