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@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Thijs Alkemade | Sent: 25 January 2012 15:21 | To: glasgow-haskell-users@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users