Created
February 15, 2014 13:51
-
-
Save Blaisorblade/9019567 to your computer and use it in GitHub Desktop.
Scalac semi-gets type refinement with type functions, but only "semi" — see comments inside the gist for the breakage, comments below the gist for explanation.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
package bugreport | |
object BugReport { | |
/* A simple universe of types */ | |
sealed trait Type { | |
type Eval | |
type DT <: Type | |
} | |
sealed trait BaseType[BaseT] extends Type { | |
type Eval = BaseT | |
} | |
sealed trait BaseInt extends BaseType[Int] { | |
type DT = BaseInt | |
} | |
trait Exp[TP <: Type] { | |
type T = TP | |
def derive: Exp[T#DT] | |
} | |
//Adding 'final' here does not help this time. | |
final case class Num(t: Int) extends Exp[BaseInt] { | |
def derive: Exp[T#DT] = Num(0) | |
} | |
def unsafeCoerce[T](a: T): Nothing = a.asInstanceOf[Nothing] | |
def derive[T <: Type](term: Exp[T]): Exp[T#DT] = | |
term match { | |
case Num(n) => | |
val a = Num(n): Exp[T#DT] | |
//.asInstanceOf[Exp[T#DT]] doesn't work. | |
//a.asInstanceOf[Exp[T#DT]] | |
//unsafeCoerce(a) //Works | |
a //fails | |
} | |
} |
I think the approach for GADT type checking is fundamentally broken. It mutates the method type parameter's symbol info and does not substitute properly into the tree. The real solution would be to use TypeVars, but then you have to do an expensive substitution on the whole method as you've discovered (to catch the result type). There's a similar issue with undoLog (in that it uses global mutable state rather than a true transaction log of constraints). It would be very interesting to see if we can get a little closer to dotty (albeit much more conservatively) by implementing proper constraint-based type inference. Obviously, quite the undertaking...
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I think the root problem is the broken assumption that we can sharpen the bounds, compute the type of the case body, then weaken the bounds of the result.
What we see instead is that the "weaken the bounds" part sometimes ends up as a no-op, because the result type no longer contained the type parameter. Why? The sharper bounds enabled us to dealias
DT
toBaseInt
.