Skip to content

Commit c389389

Browse files
committed
Add neg test
1 parent 1f9812e commit c389389

File tree

1 file changed

+35
-0
lines changed

1 file changed

+35
-0
lines changed
Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/** A modified version of gadt-injectivity-alt.scala. */
2+
object test {
3+
4+
enum SUB[-F, +G] {
5+
case Refl[S]() extends SUB[S, S]
6+
}
7+
8+
enum KSUB[-F[_], +G[_]] {
9+
case Refl[S[_]]() extends KSUB[S, S]
10+
}
11+
12+
def foo[F[_], G[_], A](
13+
keq: (F KSUB Option, Option KSUB F),
14+
ksub: Option KSUB G,
15+
sub: F[Option[A]] SUB G[Option[Int]],
16+
a: A
17+
) =
18+
keq._1 match { case KSUB.Refl() =>
19+
keq._2 match { case KSUB.Refl() =>
20+
ksub match { case KSUB.Refl() =>
21+
sub match { case SUB.Refl() =>
22+
// F = Option
23+
// & G >: Option
24+
// & F[Option[A]] <: G[Option[Int]]
25+
// =X=>
26+
// A <: Int
27+
//
28+
// counterexample: G = [T] => Any
29+
val i: Int = a // error
30+
()
31+
}
32+
}
33+
}
34+
}
35+
}

0 commit comments

Comments
 (0)