On 5 jan. 2012, at 14:08, Sean Leather wrote:
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
As an update to this: I realized that tidying wasn't applied correctly. Previously each hole was typed separately using an empty tidy environment, causing wrong substitutions to be made. Using tidyOpenType and passing the updated environment for each hole has fixed the resulting type. Regards, Thijs