Re: API function to check whether one type fits "in" another
Thijs Alkemade <thijsalkemade <at> gmail.com>
2012-07-23 15:15:44 GMT
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.
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.
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org