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

[Thijs Alkemade]

On 19 jul. 2012, at 19:28, Philip Holzenspies wrote:

> 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

Hi Philip,

As Simon has said, I have been working on implementing Agda-like holes in GHC. This is somewhat similar to what you've been working on, but so far I've only been concerned into reporting these holes to the user, and not trying to figure out what could fit into it. Also, I was adding it to GHC directly, not using the GHC API, so our approaches are quite different. But I'm hoping my experience might help you a little.

Could you show how simplifyTop fails, or show a bit more of you code? I wasn't able to get just this piece running as you described. If it is an ambiguity error as you say, it could just be the monomorphism restriction incorrectly assuming your types belong to top level declarations and rejecting them.

Regards,
Thijs Alkemade
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 841 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120723/c2f13419/attachment.pgp>