<div>We&#39;re currently looking into so-called expression holes in GHC -- like the type goals of Agda -- and we&#39;ve run into a problem of understanding.</div><div><br></div><div>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 &quot;t&quot; (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&#39;re missing something in trying to find the proper type of a hole.</div>

<div><br></div><div>Any suggestions on what we should do or look at?</div><div><br></div><div>Note that we&#39;re currently working from 7.2.2, because we could not previously build HEAD.</div><div><br></div><div>Thanks,</div>

<div>Sean</div>