Get ready to learn about dependent pairs and singletons!
I'm going to rewrite your system a little bit to simplify it.
First off, I'm going to shrink your universe of types from all of Haskell to a much simpler universe consisting of a single primitive type and arrows.
infixr 0 :->
data Type = Unit | Type :-> Type
Hopefully you should be able to see how to extend this with more primitive types.
I'm also going to remove most of the bits from Comb, since they can all be expressed in terms of one another.
data Comb a where
S :: Comb ((a :-> b :-> c) :-> (a :-> b) :-> a :-> c)
K :: Comb (a :-> b :-> a)
(:$) :: Comb (a :-> b) -> Comb a -> Comb b
i = S :$ K :$ i
b = (S :$ (K :$ S)) :$ K
c = S :$ (S :$ (K :$ (S :$ (K :$ S) :$ K)) :$ S) :$ (K :$ K)
w = S :$ S :$ (S :$ K)
Now to your question. As you correctly surmised, when you're reading user input you can't predict statically what the type of the resulting term will be, so you need to existentially quantify it.
data Ex f = forall a. Ex (f a)
The problem is: how do you recover the type information in order to be able to manipulate terms? We can pair up a Comb with another value which you can pattern-match on at runtime to learn the type of the Comb. Here's a combinator for pairing things up.
data (f :*: g) i = f i :*: g i
(I lifted both of these types from the Hasochism paper.) :*: pairs up two types ensuring that their indices are equal. We'll use it together with Ex to simulate a dependent pair or sigma type: a pair of values for whom the type of the second component depends on the value of the first. The idea is that f will be a GADT which tells you something about its index, so pattern matching on f gives you information about the type of g.
type Sg f g = Ex (f :*: g)
pattern Sg x y = Ex (x :*: y)
Now the clever part: coming up with a GADT which tells you about a combinator term's type.
data Typey t where
Unity :: Typey Unit
Arry :: Typey a -> Typey b -> Typey (a :-> b)
Typey is called a singleton. For a given t, there exists exactly one value of type Typey t. So if you have a Typey t value, you know everything there is to know about t.
Singleton values are ultimately a hack. Typey is not Type; it's a value-level stand-in for Type's duplicated type-level copy. In a real dependently-typed system you don't need singleton glue to affix value-level stuff to type-level stuff because the distinction isn't there in the first place.
Our existentially-quantified combinators now look like this. AComb packs up a Comb with a runtime representation of its type. This technique allows us to guarantee that the boxed Comb is well-typed; we just can't say statically what that type is.
type AComb = Sg Typey Comb
How do we write ($$), which attempts to apply an AComb to another AComb? We need to pattern-match on their associated Typeys in order to learn whether or not it's possible to apply one to the other. In particular, we're going to need a way to know whether two types are equal.
Here comes propositional equality, a GADT proof that two type-level things are equal. You can only give a value of Refl if you can explain to GHC that a and b are in fact the same. Conversely, if you pattern-match on Refl then GHC will add a ~ b to the typing context.
data a :~: b where
Refl :: a :~: a
withEq :: a :~: b -> (a ~ b => r) -> r
withEq Refl x = x
Here's a helper function to lift a pair of equalities through the :-> constructor.
arrEq :: (a :~: c) -> (b :~: d) -> (a :-> b) :~: (c :-> d)
arrEq Refl Refl = Refl
As promised, we can write down a function to check whether two Types are equal. We proceed by pattern-matching on their associated singleton Typeys, failing if we find the types to be incompatible. If the equality test succeeds, the spoils are a proof that the types are equal.
tyEq :: Typey t -> Typey u -> Maybe (t :~: u)
tyEq Unity Unity = Just Refl
tyEq (Arry a b) (Arry c d) = liftA2 arrEq (tyEq a c) (tyEq b d)
tyEq _ _ = Nothing
withTyEq :: Typey t -> Typey u -> (t ~ u => a) -> Maybe a
withTyEq t u x = fmap (\p -> withEq p x) (tyEq t u)
Finally, we can write $$. The typing rule goes like this:
f : a -> b y : a
------------------- App
f y : b
That is, if the left-hand term of $$ is a function type, and the type of the right-hand term matches the function's domain, we can type the application. So the implementation of this rule has to test (using withTyEq) whether the relevant types match in order to return the resulting term.
($$) :: AComb -> AComb -> Maybe AComb
Sg (Arry a b) x $$ Sg t y = withTyEq a t $ Sg b (x :$ y)
_ $$ _ = Nothing
Generating Typey terms corresponds to the act of type-checking. In other words, a function parse :: String -> AComb has to do both parsing and type-checking. In real compilers, these two phases are separated.
So I'd advise parsing the user input into an untyped syntax tree, which admits ill-formed terms, and then generating typing information separately.
data Expr = S | K | Expr :$ Expr
parse :: String -> Parser Expr
typeCheck :: Expr -> Maybe AComb
A fun exercise (in more-dependently-typed languages) is to modify typeCheck to return a more detailed explanation of why type-checking failed, like this bit of pseudo-Agda:
data Void : Set where
Not : Set -> Set
Not a = a -> Void
data TypeError : Expr -> Set where
notArr : Not (IsFunction f) -> TypeError (f :$ x)
mismatch : Not (domain f :~: type x) -> TypeError (f :$ x)
inFunc : TypeError f -> TypeError (f :$ x)
inArg : TypeError x -> TypeError (f :$ x)
typeCheck : (e : Expr) -> Either (TypeError e) AComb
You can also make typeCheck more precise by giving assurance that it doesn't change the term you give it (another exercise).
For further reading, see The View from the Left, which features a verified type-checker for the lambda calculus.
Typeyis monomorphic. I.e. you can't applyaid :: ACombto itself. For this to work you'd need to add explicit type variables and changetyEqtotyUnify. – Agathy