How I would like to implement https://github.com/scala/scala/blob/v2.10.2/src/reflect/scala/reflect/api/TreeCreator.scala

gistfile1.txt

// TreeCreator is conceptually a dependent function that:
// 1) Takes a universe-bound mirror
// 2) Produces a tree from the same universe

// So I would like to write it as follows (imaginary syntax)
// e.g. as per this proposal: http://blaisorbladeprog.blogspot.de/2013/01/flexible-implicits-from-agda-for-scala.html
abstract class TreeCreator {
  def apply[[u: Universe]](m: u.Mirror): u.Tree
}

// Or even like this, which would be even better
type TreeCreator[[u: Universe]] = u.Mirror => u.Tree

// And then I would like to use it as follows
trait Universe {
  object TypeTag { def apply[T](tpec: TypeCreator): TypeTag[T] = ... }
}
import scala.reflect.runtime.{universe => ru}
ru.TypeTag(m => m.staticClass("scala.Int").toType)

// I.e. if the compiler then would be able to:
// 1) Infer u, so that I don't have to specify it every time I invoke the method
// 2) Perform eta-expansion for DMT function literals, so that I don't have to subclass TreeCreator every time
// Then I would be happy!

This sounds pretty cool, though dependent function types are already hard by themselves.

I'm not sure about 2) in the end. Is that about m => m.staticClass("scala.Int").toType desugaring to [[u: Universe]] => (m : u.Mirror) => m.staticClass("scala.Int").toType? Agda does this kind of inference too, but I'd need to find the relevant literature to figure out how they do that.