Hello! As mentioned in our previous mail [1], we've been working on introducing Agda's holes into GHC [2]. Our general approach is as follows: we've added a hole to the syntax, denoted here by two underscores: "__". We've introduced a new HsExpr for this, which stores the hole's source span (as this is the only thing that a user needs to identify the hole). Then, we extended the local environment of the typechecker to include a mutable Map, mapping a SrcSpan to a Type and a WantedConstraints (we need these later to produce the correct class constraints on the type). In TcExpr.lhs, whenever the tcExpr function encounters a hole, it adds the source position with the res_ty and the current tcl_lie to the map. After type checking has finished, these types can be taken out of the map and shown to the user, however, we are not sure yet where to do this. Currently the map is read in tcRnModule and tcRnExpr, so loading modules and evaluating expressions with ":t" will show the types of the holes in that module or expression. There, we call mkPiTypes, mkForAllTys (with the quantified type variables we obtained from the WantedConstraints), we zonk and tidy them all (most of this imitates how tcRnExpr modifies a type before returning it, except the tidying, which needs to pass the updated TidyEnv to the tidying of the next hole). Examples: *Main> :t [__, ()] tcRnExpr2: [(<interactive>:1:2-3, ())] [__, ()] :: [()] *Main> :t map __ __ tcRnExpr2: [(<interactive>:1:5-6, a0 -> b), (<interactive>:1:8-9, [a0])] map __ __ :: [b] Any feedback on this design would be appreciated. We would like to know if this is something that could be considered to be added to GHC, and what your requirements for that are. Also, we have a confusing problem when type checking a module. Above, we showed the result of ":t map __ __" in ghci. However, if we put "f = map __ __" in a module, we get: tcRnModule: [(f.hs:1:9-10, GHC.Prim.Any * -> b), (f.hs:1:12-13, [GHC.Prim.Any *])] If I read GHC.Prim.Any * as forall a. a, then this is not correct: the GHC.Prim.Any * in both holes should have the same type. We assume it shows up because the type that should be there does not occur in the type signature of f (as it's just [b]), but so far we've been unable to figure out why this behavior is different in interactive mode. Does someone have an idea about what to do to avoid the introduction of these GHC.Prim.Any * types? Best regards, Thijs Alkemade [1] http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021453.h... [2] https://github.com/xnyhps/ghc/commits/master