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 [thijsalkem...@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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
