Type inference for a scala combinator calculus data model

I'm trying out a very light-weight encoding of combinator calculus in scala. Initially, I'm simply implementing the S and K combinators, application and constant values. Later I hope to lift scala functions in and allow evaluation of an expression as a scala function. However, that's for later. Here is what I have so far.

/** Combinator expression */
sealed abstract class CE

/** Application: CE| (x y) <=> LC| (x:(A=>B) y:A) : B */
case class Ap[A <: CE, B <: CE, X](e1: A, e2: B) extends CE

/** A raw value with type */
case class Value[T](v: T) extends CE

/** Some combinator */
sealed abstract class Comb extends CE

/** The S combinator: CE| S x y z
 *                    LC| λx:(A=>B=>C).λy:(A=>B).λz:A.(x z (y z)) : C
 *  S : ∀A.∀B.∀C. (A => B => C) => (A => B) => A => C
 */
case object S extends Comb
/** The K combinator: CE| K x y
 *                    LC| λx:A.λy:B.x:A : A
 *  K : ∀A => ∀B => A
 */
case object K extends Comb

Now I would like to do some type inference over this. For simplicity of implementing small- and large-step reduction, the data model is untyped, so I'd like types to be external to this structure. Let's introduce something to hold the type information.

trait TypeOf { type typeOf }

The Value type is easy.

implicit def typeOfValue[T](vt: Value[T]) : TypeOf =
    new TypeOf { type typeOf = T }

Application is a little more tricky, but basically boils down to function application. Let's introduce a type ⊃ for combinator application, to avoid confusion with normal scala application.

/** Combinator application */
class ⊃[+S, -T]

implicit def typeOfAp[Ap[A, B], A <: CE, B <: CE], X, Y](Ap(A, B)
  (implicit aIsFXY: A#typeOf =:= (X⊃Y), bIsX: B#typeOf =:= X) : TypeOf =
      { type typeOf = Y }

This is where I get stuck. I need to represent the type of the S an