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

[Philip Holzenspies]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120719/cf6f5e74/attachment.htm>