Finding the type of a hole

Sean Leather leather at cs.uu.nl
Thu Jan 5 14:08:27 CET 2012


We're currently looking into so-called expression holes in GHC -- like the
type goals of Agda -- and we've run into a problem of understanding.

We have defined an expression, call it __ for now, for which we want to
find the type after a program is type-checked. In tcExpr (TcExpr.lhs), we
can see the type that arrives in the argument res_ty, but that does not
appear to give the correct (or final?) type after applying zonkTcType. For
example, if we have (__, __), then we find that both holes have some type
"t" (as printed). We also see this in a module with declarations such as f
= __ and g = __. When these are actually typed, they get unique type
variables as expected. So, apparently, we're missing something in trying to
find the proper type of a hole.

Any suggestions on what we should do or look at?

Note that we're currently working from 7.2.2, because we could not
previously build HEAD.

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120105/51f74185/attachment.htm>


More information about the Glasgow-haskell-users mailing list