Skip to content

Commit 3084bf9

Browse files
author
Aleksander Boruch-Gruszecki
committed
Add test showing injectivity issue
1 parent f008bbc commit 3084bf9

File tree

1 file changed

+24
-0
lines changed

1 file changed

+24
-0
lines changed

tests/gadt-neg/uninjectivity.scala

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
object uninjectivity {
2+
sealed trait EQ[A, B]
3+
final case class Refl[T]() extends EQ[T, T]
4+
5+
def absurd1[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match {
6+
case Refl() =>
7+
x // should be an error
8+
}
9+
10+
def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fi: F[Int], fs: F[String]): G[Int] = eq match {
11+
case Refl() =>
12+
val gs: G[String] = fs // error
13+
// fi
14+
???
15+
}
16+
17+
def absurd3[F[_], G[_], X, Y](eq: EQ[F[X], G[Y]], fx: F[X]): G[Y] = eq match {
18+
case Refl() =>
19+
val gx: G[X] = fx // error
20+
val fy: F[Y] = fx // error
21+
// fx
22+
???
23+
}
24+
}

0 commit comments

Comments
 (0)