API function to check whether one type fits "in" another
Simon PeytonJones
simonpj at microsoft.com
Thu Jun 28 09:07:01 CEST 2012
Philip
 What I'm looking for is a function

 fitsInto :: TermType > HoleType > Maybe [(TyVar,Type)]
Happily there is such a function, but you will need to become quite familiar with GHC's type inference engine.
We need to tighten up the specification first. I believe that you have function and argument, whose *most general types* are
fun :: forall a b c. fun_ty
arg :: forall p q. arg_ty
You want to ask whether 'arg' could possibly be 'fun's second (say) argument.
To answer this you must first instantiate 'fun' correctly. For example, suppose
fun :: forall a. [a] > Int
arg :: [Bool]
Then we can indeed pass 'arg' to 'fun' but only if we instantiate 'fun' at Bool, thus:
fun Bool :: [Bool] > Int
Now indeed the first argument of (fun Bool) has precisely type [Bool] and we are done.
This business of instantiating a polymorphic function with a type, using a type application (f Bool) is a fundamental part of how GHC works (and indeed type inference in general). If you aren't familiar with it, maybe try reading a couple of papers about GHC's intermediate language, System F or FC.
To play this game we have to correctly "guess" the type at which to instantiate 'fun'. This is what type inference does: we instantiate 'fun' with a unification variable 'alpha' meaning "I'm not sure" and then accumulate equality constraints that tell us what type 'alpha' stands for.
The other complication is that 'arg' might also need instantiation to fit, but I'll ignore that for now. It'll only show up in more complicated programs.
So you want a function something like this:
fits :: Type  The type of the function
> Int  Which argument position we are testing
> Type  The argument
> TcM Bool  Whether it fits
fits fun_ty arg_no arg_ty
= do { inst_fun_ty < deeplyInstantiate fun_ty
; llet (fun_arg_tys, fun_res_ty) = splitFunTys inst_fun_ty
the_arg_ty = fun_arg_tys !! arg_no
; unifyType the_arg_ty arg_ty }
The first step instantiates the function type (deeplyInstantiate is in Inst.lhs) with fresh unification variables. The second extracts the appropriate argument. Then we unify the argument type the function expects with that of the supplied argument.
Even then you aren't done. Unification collects constraints, and we need to check they are solutle. So we'll really need something like
do { constraints < captureConstriaints (fits fun_ty arg_no arg_ty)
; tcSimplifyTop constraints }
And the final thing you need to do is intiate the type checker monad with initTc, and check whether any errors occurred.
It occurs to me that a simpler way to do this might be to piggy back on the work of Thijs Alkemade [thijsalkemade at gmail.com] at Chalmers on "holes". He's going to make it possible to make an expression
fun _ arg
where the underscore means "hole". Then you can give this entire expression to the type checker and have it figure out whether it is typeable, and if so what the type the "_" is. This would mean you didn't need to do any of the above stuff (and I have simplified considerably in writing the above). Maybe look at the ticket http://hackage.haskell.org/trac/ghc/ticket/5910 and wiki page http://hackage.haskell.org/trac/ghc/wiki/Holes
Simon
More information about the Glasgowhaskellusers
mailing list