Hi again, For my previous example: main = putStr $ show (fred 1 3) where fred a b = let myid x = x in myid (plus a b) plus x y = x + y I can now get the following output: ==================== Bernie: All Binder TypeSigs ==================== main :: IO () plus :: forall a. (Num a) => a -> a -> a fred :: forall a. (Num a) => a -> a -> a myid :: forall t_aMv. t_aMv -> t_aMv Which is exactly what I want. Turned out to be quite simple in the end. Thanks a lot for all your help Simon. Just out of curiosity, do you think that this sort of output would be useful for other people? I don't know what your plans are for GHCi, but you may be considering a mode that prints types out, something like :t in hugs. I always found it frustrating in hugs that I couldn't get the types of locally defined values. My students also find this frustrating, and it sometimes causes them to avoid local definitions. Obviously there are issues with type variables which are quantified outside the local definition, but careful naming of things should be able to fix this. Regards, Bernie. Simon Peyton-Jones writes:

Bernie

All (I think) the top level bindings come out of the type check as an AbsBinds. This is where we generalise from a monomorphic thing to a polymorphic thing.

An AbsBinds has four components, the third of which is a list of triples (TyVar, Id, Id). You want to grab the first of these Ids (only). You can then ignore the MonoBinds inside the fourth component of the AbsBinds. So your code will get quite a bit simpler.

The two Ids in the triple are the polymorphic top-level binder and the monomorphic (perhaps recursive) thing that it generalises. It's a bit hard to explain in a short space. Look at the output of the desugarer for a simple defn, to see what an AbsBinds translates to.

Anyway these polymorphic Ids will have exactly the for-alls and constraints that you want

hope this gets you moving