Hi Simon, I'm a bit confused by the new handling of Typeable. * You say (in Note [Grand plan for Typeable]) that there is trouble making the TyCon/Module information for the types in GHC.Types. But what precisely goes wrong? I agree that it seems a bit fishy, but I don't actually see the spot where trouble lurks. Did you try this? * Even more bizarre would be putting TyCon/Module info for GHC.Prim stuff (I'm thinking about the super-magical TYPE) right in GHC.Prim. But still I can't quite articulate what goes wrong. There is no Prim.hi file that would be wonky. And, provided that GHC.Types itself doesn't try to solve a Typeable constraint, no one would ever notice the weird dependency. I recognize that this means we'd have to build the info somewhere manually in GHC, but I don't think that would be too hard -- and I think easier than the current story around name-mangling just so that you can write the typereps by hand in Data.Typeable.Internal. There's also not very many lifted tycons in GHC.Prim. I count TYPE and RealWorld, and that's it. For what it's worth, a weird dependency from GHC.Prim to GHC.Types actually works in practice. I put Levity in GHC.Types but (TYPE :: Levity -> TYPE 'Lifted) in GHC.Prim. No one complained. * Let's assume that we really can't clean up this mess. It still seems that several TyCons are missing from Data.Typeable.Internal. Like promoted nil and cons, and Nat, and Symbol. At the least, we should put a loud comment in the export list of GHC.Types saying that everything defined there must be accompanied by a definition in Data.Typeable.Internal. What do you think? Richard