-
-
Save Blaisorblade/9019567 to your computer and use it in GitHub Desktop.
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 | |
} | |
} |
A more accurate reduction — fixing your reduced version wouldn't be enough, because we need some GADT refinement:
object BugReportReduced {
trait Type {
type DT <: Type
}
trait BaseInt extends Type {
type DT = BaseInt
}
trait Exp[TP <: Type]
class Num extends Exp[BaseInt]
def derive[T <: Type](term: Exp[T]): Any = {
val res1 = term match { case _: Num => (??? : Exp[T#DT]) }
res1: Exp[T#DT] // fails, the prefix of the type projection in the case body underwent wanted GADT refinement, but this is not reflected here.
val res1b = term match { case _ : Num => (new Num : Exp[T#DT]) } //works
res1b: Exp[T#DT] //fails
type X = T#DT
val res2 = term match { case _: Num => (??? : Exp[X]) }
res2: Exp[T#DT] // works
val res2b = term match { case _: Num => (new Num : Exp[X]) } //fails
res2b: Exp[T#DT] // this part works
}
}
I fear I'll have to defer this to next weekend.
Tonight I've found at least two distinct bugs:
-
This doesn't work unless you inline res; its body is typechecked without an expected type.
def derive2Harder[T <: Type](term: Exp[T]): Exp[T] = { val res = term match { //case _ : Num => (??? : Exp[BaseInt]) case _ : Num => (??? : Exp[T]) //also broken! } res }
-
This variant of the testcase shows the problem at its worst, I fear. savedTypeBounds seems to not matter.
val res1: Exp[T#DT] = term match { case _: Num => (??? : Exp[T#DT]) }
The case body gets turned into
(???: Exp[BaseInt])
, and is typechecked against a crazy type, which I'll callcrazyType
. This looks likeExp[T#DT]
; the problem is that both T#DT and T are instances ofAbstractNoArgsTypeRef
, and the instance forT
wraps the correct TypeSkolem, having as infostyper: >: bugreport.BugReportReduced.BaseInt <: bugreport.BugReportReduced.BaseInt
. So, maybe, this relates to
https://issues.scala-lang.org/browse/SI-7051, as the documentation of dealiasWiden helpfully suggests.
I have not figured out how exactly that type fails to normalize/dealias/widen, but I trust an AbstractType (ehm, AbstractNoArgsTypeRef) is not expecting a fully instantiated skolem inside.
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
to BaseInt
.
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...
Thanks, I had figured that had to do with it, but it's reassuring to know.
OK, that's wrong. Going to grep for the message, and figure out why it does not happen with X. Anyway, I suppose that the check should really look also at the expected type.
Thanks!