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

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