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