A thought. Based on my limited understanding of your goals, suppose instead of (say) f (__, True) __ you transformed to \xy -> f (x,True) y That is, replace each hole with a variable. Now do type inference. You'll get a type like Int -> Bool -> ... and that tells you the type of the two holes. Or you might get a type like forall a. a -> [a] -> .... and that too tells you a lot about the types of the holes. Or you might get a type like forall a. Ord a => a -> [a] -> ... To me it looks like you get exactly the info that (I think) you want, and moreover you can do that without changing the type inference engine at all. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Simon Peyton-Jones | Sent: 26 January 2012 14:25 | To: Thijs Alkemade; glasgow-haskell-users@haskell.org | Subject: RE: Holes in GHC | | 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 | | | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users