Holes in GHC

[Thijs Alkemade]

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.html
[2] https://github.com/xnyhps/ghc/commits/master