Missing type representations

When I say

{-# LANGUAGE DataKinds #-}

module Bug where

import Data.Typeable

foo = typeRep (Proxy :: Proxy '[])

I get

GHC error in desugarer lookup in Bug:
  Can't find interface-file declaration for variable tc'[]
    Probable cause: bug in .hi-boot file, or inconsistent .hi file
    Use -ddump-if-trace to get an idea of which file caused the error
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 7.11.20151120 for x86_64-apple-darwin):
	initDs IOEnv failure

And I think there may be more trouble. Below are notes I have written to ghc-devs:

---

I'm a bit confused by the new handling of Typeable.

1. 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?
2. Even more bizarre would be putting TyCon/Module info for GHC.Prim stuff (I'm thinking about the super-magical TYPE from my branch) 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.

1. 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.
2. Data.Typeable.Internal uses mkGhcTypesTyCon, which refers to GHC.Types. But this function is used also for things from GHC.Prim, like (->). Solving Typeable (->) works fine. But I'm sure there's trouble lurking here.