These are chat archives for typelevel/scala

2nd
Jun 2017
Hamish Dickson
@hamishdickson
Jun 02 2017 12:12
heya, would you expect this exhaustiveness warning with -Yliteral-types enabled?
scala> val t: true = true
t: true = true

scala> t match {
     | case true => 1
     | }
<console>:13: warning: match may not be exhaustive.
It would fail on the following input: false
       t match {
       ^
res0: Int = 1
Alexander Konovalov
@alexknvl
Jun 02 2017 17:58
I would not, but Scala compiler is a mystery.
;)
Rob Norris
@tpolecat
Jun 02 2017 20:55
Would it make sense for a GADT match on a singleton type to be able to materialize the value on the RHS?
It can't now but it seems like it would be ok to do so.
Well I guess Nothing would mess it up.
Edmund Noble
@edmundnoble
Jun 02 2017 20:57
Yeah that's the subtle difference between case O => O and case o: O.type =>. Equals is used for one, eq for the other.
I don't think Nothing would mess it up nearly as much as an overriden .equals.
I think :confused: I'm not sure and not at my computer.
Rob Norris
@tpolecat
Jun 02 2017 21:10
I mean, if you had sealed trait Foo[A <: Int with Singleton] and case object Blah extends Foo[Nothing] then given a Foo[A] and case Blah => valueOf[A] it would have to hand you a Nothing. So it doesn't work.
jeremyrsmith
@jeremyrsmith
Jun 02 2017 21:12
valueOf needs a ValueOf in scope… as soon as the literal type is forgotten you can’t get that anymore
Rob Norris
@tpolecat
Jun 02 2017 21:13
well I guess it would just not compile for Nothing
jeremyrsmith
@jeremyrsmith
Jun 02 2017 21:13
so the only way you could use valueOf is if ValueOf was passed implicitly to the method you’re in (which already proves it’s not Nothing), or if you already have the value there on your screen
Rob Norris
@tpolecat
Jun 02 2017 21:13
You could know it if a GADT match knows the type.
case object Blah extends Foo[42] ... case Blah => // scala knows A =:= 42
jeremyrsmith
@jeremyrsmith
Jun 02 2017 21:14
Ah, you’re right!
Rob Norris
@tpolecat
Jun 02 2017 21:14
So yeah it could still materialize a value on the RHS if it's a legit singleton type.
It just wouldn't work with Nothing.
@milessabin is there a problem with this conceptually, or implementation-wise? (question was, why can't a GADT match proving a singleton type materialize the value?)