API function to check whether one type fits "in" another

["Philip K. F. Hölzenspies"]

L.S.,

I sent this to the cvs-ghc list, but was - correctly - redirected here.

We're trying to write an alternative interactive front-end (alternative to ghci). This front-end is very type-driven; terms are composed not as characters on a prompt, but as applications of terms to terms. At every application of a term to another, we want to check whether the application is well typed and what type variables would have to change.

Suppose I want to build the term

flip fmap (+) :: Num n => ((n -> n) -> b) -> n -> b

In our front-end, however, we do not need the flip; we leave unfilled holes with their type annotated, so the above would really look like this (where [[ and ]] denote a hole):

fmap [[ (n -> n) -> b ]] (+) :: Num n => n -> b

We start this off by asking for the types of these separate things, using GHC.exprType, giving:

fmap:
ForAllTy f (ForAllTy a (ForAllTy b (FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (FunTy (FunTy (TyVarTy a) (TyVarTy b)) (FunTy (AppTy (TyVarTy f) (TyVarTy a)) (AppTy (TyVarTy f) (TyVarTy b)))))))

(+):
ForAllTy a (FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a))))

(Note that 'Var' things are pretty printed to just show their name, whereas all the constructors of Type are displayed using show.)

The thing that we really want to ask the GHC-API is whether (+) 'fits into' the second argument-hole of fmap, i.e. we want to know whether (type of +)

ForAllTy a (FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a))))

fits into (type of second argument of fmap)

ForAllTy f (ForAllTy a (FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (AppTy (TyVarTy f) (TyVarTy a))))

What I'm looking for is a function

fitsInto :: TermType -> HoleType -> Maybe [(TyVar,Type)]

I have found many functions in TcUnify / Unify / TcMatches that look somewhat like this, but in all cases they required extra arguments. When these extra arguments are filled with arbitrary values, the result is always Nothing or some sort of panic.

Any pointers would be truly welcome.

Regards,
Philip