Holes in GHC

[Simon Peyton-Jones]

Thijs

You are describing the implementation of something, but you do not give a specification.  It's hard for me to help you with the design of something when I don't know what the goal is.

Can you give a series of concrete examples of what you want to happen?  Is this just in GHCi?  Or do you expect the batch compiler to behave specially?  

Don't worry about the implementation: just say what you would LIKE to achieve.

Simon

|  -----Original Message-----
|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Thijs Alkemade
|  Sent: 25 January 2012 15:21
|  To: glasgow-haskell-users at haskell.org
|  Subject: Holes in GHC
|  
|  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
|  
|  _______________________________________________
|  Glasgow-haskell-users mailing list
|  Glasgow-haskell-users at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users