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

[Simon Peyton-Jones]

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