Dear Simon, et al,
I finally got back around to working on this idea. I'm not yet quite sure
whether I've now understood it all. I have reread the latest edition of "System
F with Type Equality Coercions" (Jan 2011 version), so I understand that
inference is now just percolating coercions upwards, as it were, and then
solving the set of wanted constraints. If the set is consistent, the program
type-checks. This is at the core of what I have now:
typeCheck :: GhcMonad m => Type -> Type -> m (Messages, Maybe (TcCoercion, Bag
EvBind))
typeCheck expectedTy actualTy = do
let mod = mkModule mainPackageId $ mkModuleName "<NoModule>"
env <- getSession
liftIO $ initTc env HsSrcFile False mod $ do
(coerce,wanted) <- captureConstraints $ do
(expectedWrap, expectedRho) <- deeplyInstantiate DefaultOrigin expectedTy
(actualWrap, actualRho ) <- deeplyInstantiate DefaultOrigin actualTy
unifyType actualRho expectedRho
binds <- simplifyTop wanted
return (coerce,binds)
It appears both the "hole" (expectedTy) and the thing to go into the hole
(actualTy) need to be deeply instantiated, otherwise, this function rejects
putting (exprType "1") into the first argument position of (exprType "(+)"),
because it either can't match 'a' to 'Num b => b', or (if we take the
rho-type), it misses 'Num b'. Anyway, deeply instantiating both seems to solve
such problems and, in the cases I've tried, type checks the things I would
expect and rejects the things I would expect.
There are two missing bits, still:
Firstly, when leaving variables ambiguous (i.e. filling a "Monad m => a -> m a"
shaped hole with "return", leaving 'm' ambiguous), simplifyTop fails. Is it
possible to allow for ambiguous variables, in roughly the same way that
(exprType "mapM return") works just fine? I've looked at some other
simplification functions (TcSimplify.*), but the lack of documentation makes my
guesswork somewhat random.
Secondly, is there a way in the API to find all the appropriate substitutions
for the variables in the *original* types (i.e. loosing the fresh variables
introduced by deeplyInstantiate)? Ultimately, I would really like to end up
with a TvSubst, or any other mapping from TyVar to Type.
Ideas?
Regards,
Philip
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
