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.

ScalacIsCrazy.scala

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
    }
}

From a blackbox investigation, it seems that inside the case branch, Scalac correctly discovers that Exp[T#DT] = Exp[BaseInt#DT] = Exp[BaseInt] and rewrites Exp[T#DT] to Exp[BaseInt], but it does not do the same to the expected return type, and that's why a.asInstanceOf[Exp[T#DT]] does not typecheck with expected type Exp[T#DT].

Here's a reduced look at it:

package bugreport

object BugReport {
  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 unwanted GADT refinement

    type X = T#DT
    val res2 = term match { case _: Num => (??? : Exp[X]) }
    res2: Exp[T#DT] // works
  }
}

You probably want to focus your investigation on code paths that hit Context#savedTypeBounds.

[log typer] Saving type T info= <: bugreport.BugReport.Type
[log typer] updated bounds: type T from  <: bugreport.BugReport.Type to:  >: bugreport.BugReport.BaseInt <: bugreport.BugReport.BaseInt
[log typer] Discarding inferred TypeBounds(lo=bugreport.BugReport.BaseInt, hi=bugreport.BugReport.BaseInt) because type T does not appear in: bugreport.BugReport.Exp[bugreport.BugReport.BaseInt]
sandbox/test.scala:19: error: type mismatch;
 found   : bugreport.BugReport.Exp[bugreport.BugReport.BaseInt]
 required: bugreport.BugReport.Exp[T#DT]
    res1: Exp[T#DT] // fails, the prefix of the type projection in the case body underwent unwanted GADT refinement
    ^

...savedTypeBounds...

Thanks, I had figured that had to do with it, but it's reassuring to know.

[log typer] Discarding inferred TypeBounds(lo=bugreport.BugReport.BaseInt, hi=bugreport.BugReport.BaseInt) because type T does not appear in: bugreport.BugReport.Exp[bugreport.BugReport.BaseInt]

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!

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 call crazyType. This looks like Exp[T#DT]; the problem is that both T#DT and T are instances of AbstractNoArgsTypeRef, and the instance for T wraps the correct TypeSkolem, having as infos typer: >: 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...