File tree Expand file tree Collapse file tree 3 files changed +32
-0
lines changed Expand file tree Collapse file tree 3 files changed +32
-0
lines changed Original file line number Diff line number Diff line change 1+ // scalac: -Werror
2+ object GADT {
3+ import =:= ._
4+
5+ enum =:= [A , B ] {
6+ case Refl [C ]() extends (C =:= C )
7+ }
8+
9+ def unwrap [A ,B ](opt : Option [A ])(using ev : A =:= Option [B ]): Option [B ] = ev match {
10+ case Refl () => opt.flatMap(identity[Option [B ]])
11+ }
12+ }
Original file line number Diff line number Diff line change 1+ // scalac: -Werror
2+ object GADT {
3+ import =:= ._
4+
5+ enum =:= [A , B ] {
6+ case Refl [C ]() extends (C =:= C )
7+ }
8+
9+ def unwrap [A ,B ](opt : Option [A ])(using ev : A =:= Option [B ]): Option [B ] = ev match {
10+ case _ : Refl [? ] => opt.flatMap(identity[Option [B ]])
11+ }
12+ }
Original file line number Diff line number Diff line change 1+ // scalac: -Werror
2+ object Main extends App :
3+ enum Extends [A , B ]:
4+ case Ev [B , A <: B ]() extends (A Extends B )
5+
6+ def cast (a : A ): B = this match {
7+ case Extends .Ev () => a
8+ }
You can’t perform that action at this time.
0 commit comments