Finding the type of a hole
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Glasgow-haskell-users