A bunch of fixeswip/T9858-typeable-ben2

These fixes apply to the "do Typeable stuff at definition sites"
branch.

13 files changed, 246 insertions, 186 deletions

diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs
index fb797f11ce..8670e2104e 100644
--- a/compiler/coreSyn/MkCore.hs
+++ b/compiler/coreSyn/MkCore.hs
@@ -126,12 +126,12 @@ mkCoreLets binds body = foldr mkCoreLet body binds
 
 -- | Construct an expression which represents the application of one expression
 -- to the other
-mkCoreApp :: CoreExpr -> CoreExpr -> CoreExpr
+mkCoreApp :: SDoc -> CoreExpr -> CoreExpr -> CoreExpr
 -- Respects the let/app invariant by building a case expression where necessary
 --   See CoreSyn Note [CoreSyn let/app invariant]
-mkCoreApp fun (Type ty) = App fun (Type ty)
-mkCoreApp fun (Coercion co) = App fun (Coercion co)
-mkCoreApp fun arg       = ASSERT2( isFunTy fun_ty, ppr fun $$ ppr arg )
+mkCoreApp _ fun (Type ty) = App fun (Type ty)
+mkCoreApp _ fun (Coercion co) = App fun (Coercion co)
+mkCoreApp d fun arg       = ASSERT2( isFunTy fun_ty, ppr fun $$ ppr arg $$ d )
                           mk_val_app fun arg arg_ty res_ty
                       where
                         fun_ty = exprType fun
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 57f463ca8b..2f9953bc20 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -44,9 +44,11 @@ import TyCon
 import TcEvidence
 import TcType
 import Type
+import Kind( isKind )
 import Coercion hiding (substCo)
 import TysWiredIn ( eqBoxDataCon, coercibleDataCon, mkListTy
-                  , mkBoxedTupleTy, charTy )
+                  , mkBoxedTupleTy, charTy
+                  , typeNatKind, typeSymbolKind )
 import Id
 import MkId(proxyHashId)
 import Class
@@ -67,7 +69,6 @@ import BasicTypes hiding ( TopLevel )
 import DynFlags
 import FastString
 import Util
-import Control.Monad( zipWithM )
 import MonadUtils
 import Control.Monad(liftM)
 
@@ -801,7 +802,7 @@ dsHsWrapper (WpCompose c1 c2) e = do { e1 <- dsHsWrapper c2 e
                                      ; dsHsWrapper c1 e1 }
 dsHsWrapper (WpFun c1 c2 t1 _) e = do { x <- newSysLocalDs t1
                                       ; e1 <- dsHsWrapper c1 (Var x)
-                                      ; e2 <- dsHsWrapper c2 (e `mkCoreAppDs` e1)
+                                      ; e2 <- dsHsWrapper c2 (mkCoreAppDs (text "dsHsWrapper") e e1)
                                       ; return (Lam x e2) }
 dsHsWrapper (WpCast co)       e = ASSERT(tcCoercionRole co == Representational)
                                   dsTcCoercion co (mkCastDs e)
@@ -907,14 +908,14 @@ dsEvTypeable ty ev
 
 
 ds_ev_typeable :: Type -> EvTypeable -> DsM CoreExpr
--- Returns a CoreExpr :: TypeRep (for ty)
-ds_ev_typeable ty (EvTypeableTyCon ev_ts)
-  | Just (tc, kts) <- splitTyConApp_maybe ty
-  , (ks, ts) <- splitTyConArgs tc kts
-  = do { ctr <- dsLookupGlobalId mkPolyTyConAppName
+-- Returns a CoreExpr :: TypeRep ty
+ds_ev_typeable ty EvTypeableTyCon
+  | Just (tc, ks) <- splitTyConApp_maybe ty
+  = ASSERT( all isKind ks )
+    do { ctr <- dsLookupGlobalId mkPolyTyConAppName
                     -- mkPolyTyConApp :: TyCon -> [KindRep] -> [TypeRep] -> TypeRep
        ; tyRepTc <- dsLookupTyCon typeRepTyConName  -- TypeRep (the TyCon)
-       ; let tyRepType = mkTyConApp tyRepTc []        -- TypeRep (the Type)
+       ; let tyRepType = mkTyConApp tyRepTc []      -- TypeRep (the Type)
              mkRep cRep kReps tReps
                = mkApps (Var ctr) [ cRep
                                   , mkListExpr tyRepType kReps
@@ -928,9 +929,8 @@ ds_ev_typeable ty (EvTypeableTyCon ev_ts)
                                       ; return (mkRep kcRep [] reps) }
 
        ; tcRep <- tyConRep tc
-       ; tReps <- zipWithM getRep ev_ts ts
        ; kReps <- mapM kindRep ks
-       ; return (mkRep tcRep kReps tReps) }
+       ; return (mkRep tcRep kReps []) }
 
 ds_ev_typeable ty (EvTypeableTyApp ev1 ev2)
   | Just (t1,t2) <- splitAppTy_maybe ty
@@ -939,19 +939,21 @@ ds_ev_typeable ty (EvTypeableTyApp ev1 ev2)
        ; ctr <- dsLookupGlobalId mkAppTyName
        ; return ( mkApps (Var ctr) [ e1, e2 ] ) }
 
-ds_ev_typeable ty (EvTypeableTyLit _)
-  = do { -- dict <- dsEvTerm ev
-       ; ctr <- dsLookupGlobalId typeLitTypeRepName
-              -- typeLitTypeRep :: String -> TypeRep
-       -- ; let finst = mkTyApps (Var ctr) [ty]
-             -- proxy = mkTyApps (Var proxyHashId) [typeKind ty, ty]
-       ; let tag = Lit $ MachStr $ fastStringToByteString $ mkFastString str
-       ; return (mkApps (Var ctr) [tag]) }
+ds_ev_typeable ty (EvTypeableTyLit ev)
+  = do { fun  <- dsLookupGlobalId tr_fun
+       ; dict <- dsEvTerm ev       -- Of type KnownNat/KnownSym
+       ; let proxy = mkTyApps (Var proxyHashId) [ty_kind, ty]
+       ; return (mkApps (mkTyApps (Var fun) [ty]) [ dict, proxy ]) }
   where
-    str
-      | Just n <- isNumLitTy ty = show n
-      | Just s <- isStrLitTy ty = show s
-      | otherwise = panic "ds_ev_typeable: malformed TyLit evidence"
+    ty_kind = typeKind ty
+
+    -- tr_fun is the Name of
+    --       typeNatTypeRep    :: KnownNat    a => Proxy# a -> TypeRep
+    -- of    typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep
+    tr_fun | ty_kind `eqType` typeNatKind    = typeNatTypeRepName
+           | ty_kind `eqType` typeSymbolKind = typeSymbolTypeRepName
+           | otherwise = panic "dsEvTypeable: unknown type lit kind"
+
 
 ds_ev_typeable ty ev
   = pprPanic "dsEvTypeable" (ppr ty $$ ppr ev)
diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs
index 32bd27b495..bd3a03b969 100644
--- a/compiler/deSugar/DsExpr.hs
+++ b/compiler/deSugar/DsExpr.hs
@@ -216,8 +216,8 @@ dsExpr (HsLamCase arg matches)
        ; ([discrim_var], matching_code) <- matchWrapper CaseAlt matches
        ; return $ Lam arg_var $ bindNonRec discrim_var (Var arg_var) matching_code }
 
-dsExpr (HsApp fun arg)
-  = mkCoreAppDs <$> dsLExpr fun <*>  dsLExpr arg
+dsExpr e@(HsApp fun arg)
+  = mkCoreAppDs (text "HsApp" <+> ppr e) <$> dsLExpr fun <*>  dsLExpr arg
 
 
 {-
@@ -259,15 +259,15 @@ If \tr{expr} is actually just a variable, say, then the simplifier
 will sort it out.
 -}
 
-dsExpr (OpApp e1 op _ e2)
+dsExpr e@(OpApp e1 op _ e2)
   = -- for the type of y, we need the type of op's 2nd argument
-    mkCoreAppsDs <$> dsLExpr op <*> mapM dsLExpr [e1, e2]
+    mkCoreAppsDs (text "opapp" <+> ppr e) <$> dsLExpr op <*> mapM dsLExpr [e1, e2]
 
 dsExpr (SectionL expr op)       -- Desugar (e !) to ((!) e)
-  = mkCoreAppDs <$> dsLExpr op <*> dsLExpr expr
+  = mkCoreAppDs (text "sectionl" <+> ppr expr) <$> dsLExpr op <*> dsLExpr expr
 
 -- dsLExpr (SectionR op expr)   -- \ x -> op x expr
-dsExpr (SectionR op expr) = do
+dsExpr e@(SectionR op expr) = do
     core_op <- dsLExpr op
     -- for the type of x, we need the type of op's 2nd argument
     let (x_ty:y_ty:_, _) = splitFunTys (exprType core_op)
@@ -276,7 +276,7 @@ dsExpr (SectionR op expr) = do
     x_id <- newSysLocalDs x_ty
     y_id <- newSysLocalDs y_ty
     return (bindNonRec y_id y_core $
-            Lam x_id (mkCoreAppsDs core_op [Var x_id, Var y_id]))
+            Lam x_id (mkCoreAppsDs (text "sectionr" <+> ppr e) core_op [Var x_id, Var y_id]))
 
 dsExpr (ExplicitTuple tup_args boxity)
   = do { let go (lam_vars, args) (L _ (Missing ty))
diff --git a/compiler/deSugar/DsUtils.hs b/compiler/deSugar/DsUtils.hs
index bce5186f08..503e29de46 100644
--- a/compiler/deSugar/DsUtils.hs
+++ b/compiler/deSugar/DsUtils.hs
@@ -241,7 +241,7 @@ mkCoLetMatchResult bind = adjustMatchResult (mkCoreLet bind)
 -- let var' = viewExpr var in mr
 mkViewMatchResult :: Id -> CoreExpr -> Id -> MatchResult -> MatchResult
 mkViewMatchResult var' viewExpr var =
-    adjustMatchResult (mkCoreLet (NonRec var' (mkCoreAppDs viewExpr (Var var))))
+    adjustMatchResult (mkCoreLet (NonRec var' (mkCoreAppDs (text "mkView" <+> ppr var') viewExpr (Var var))))
 
 mkEvalMatchResult :: Id -> Type -> MatchResult -> MatchResult
 mkEvalMatchResult var ty
@@ -343,7 +343,7 @@ mkPatSynCase var ty alt fail = do
     matcher <- dsLExpr $ mkLHsWrap wrapper $ nlHsTyApp matcher [ty]
     let MatchResult _ mkCont = match_result
     cont <- mkCoreLams bndrs <$> mkCont fail
-    return $ mkCoreAppsDs matcher [Var var, ensure_unstrict cont, Lam voidArgId fail]
+    return $ mkCoreAppsDs (text "patsyn" <+> ppr var) matcher [Var var, ensure_unstrict cont, Lam voidArgId fail]
   where
     MkCaseAlt{ alt_pat = psyn,
                alt_bndrs = bndrs,
@@ -536,8 +536,8 @@ into
 which stupidly tries to bind the datacon 'True'.
 -}
 
-mkCoreAppDs  :: CoreExpr -> CoreExpr -> CoreExpr
-mkCoreAppDs (Var f `App` Type ty1 `App` Type ty2 `App` arg1) arg2
+mkCoreAppDs  :: SDoc -> CoreExpr -> CoreExpr -> CoreExpr
+mkCoreAppDs _ (Var f `App` Type ty1 `App` Type ty2 `App` arg1) arg2
   | f `hasKey` seqIdKey            -- Note [Desugaring seq (1), (2)]
   = Case arg1 case_bndr ty2 [(DEFAULT,[],arg2)]
   where
@@ -545,10 +545,10 @@ mkCoreAppDs (Var f `App` Type ty1 `App` Type ty2 `App` arg1) arg2
                    Var v1 | isLocalId v1 -> v1        -- Note [Desugaring seq (2) and (3)]
                    _                     -> mkWildValBinder ty1
 
-mkCoreAppDs fun arg = mkCoreApp fun arg  -- The rest is done in MkCore
+mkCoreAppDs s fun arg = mkCoreApp s fun arg  -- The rest is done in MkCore
 
-mkCoreAppsDs :: CoreExpr -> [CoreExpr] -> CoreExpr
-mkCoreAppsDs fun args = foldl mkCoreAppDs fun args
+mkCoreAppsDs :: SDoc -> CoreExpr -> [CoreExpr] -> CoreExpr
+mkCoreAppsDs s fun args = foldl (mkCoreAppDs s) fun args
 
 mkCastDs :: CoreExpr -> Coercion -> CoreExpr
 -- We define a desugarer-specific verison of CoreUtils.mkCast,
diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs
index e4f2f8c07c..3992b37bbd 100644
--- a/compiler/prelude/PrelNames.hs
+++ b/compiler/prelude/PrelNames.hs
@@ -212,7 +212,7 @@ basicKnownKeyNames
         typeRepIdName,
         mkPolyTyConAppName,
         mkAppTyName,
-        typeLitTypeRepName,
+        typeSymbolTypeRepName, typeNatTypeRepName,
 
         -- Dynamic
         toDynName,
@@ -228,7 +228,6 @@ basicKnownKeyNames
         fromIntegralName, realToFracName,
 
         -- String stuff
-        stringTyConName,
         fromStringName,
 
         -- Enum stuff
@@ -607,7 +606,8 @@ toInteger_RDR           = nameRdrName toIntegerName
 toRational_RDR          = nameRdrName toRationalName
 fromIntegral_RDR        = nameRdrName fromIntegralName
 
-fromString_RDR :: RdrName
+stringTy_RDR, fromString_RDR :: RdrName
+stringTy_RDR            = tcQual_RDR gHC_BASE (fsLit "String")
 fromString_RDR          = nameRdrName fromStringName
 
 fromList_RDR, fromListN_RDR, toList_RDR :: RdrName
@@ -850,12 +850,11 @@ rep1TyConName = tcQual gHC_GENERICS (fsLit "Rep1") rep1TyConKey
 
 -- Base strings Strings
 unpackCStringName, unpackCStringFoldrName,
-    unpackCStringUtf8Name, eqStringName, stringTyConName :: Name
+    unpackCStringUtf8Name, eqStringName :: Name
 unpackCStringName       = varQual gHC_CSTRING (fsLit "unpackCString#") unpackCStringIdKey
 unpackCStringFoldrName  = varQual gHC_CSTRING (fsLit "unpackFoldrCString#") unpackCStringFoldrIdKey
 unpackCStringUtf8Name   = varQual gHC_CSTRING (fsLit "unpackCStringUtf8#") unpackCStringUtf8IdKey
 eqStringName            = varQual gHC_BASE (fsLit "eqString")  eqStringIdKey
-stringTyConName         = tcQual  gHC_BASE (fsLit "String") stringTyConKey
 
 -- The 'inline' function
 inlineIdName :: Name
@@ -1060,7 +1059,8 @@ typeableClassName
   , mkPolyTyConAppName
   , mkAppTyName
   , typeRepIdName
-  , typeLitTypeRepName
+  , typeNatTypeRepName
+  , typeSymbolTypeRepName
   :: Name
 typeableClassName     = clsQual tYPEABLE_INTERNAL (fsLit "Typeable")       typeableClassKey
 typeRepTyConName      = tcQual  tYPEABLE_INTERNAL (fsLit "TypeRep")        typeRepTyConKey
@@ -1070,7 +1070,8 @@ trNameSDataConName    = dcQual  gHC_TYPES         (fsLit "TrNameS")        trNam
 typeRepIdName         = varQual tYPEABLE_INTERNAL (fsLit "typeRep#")       typeRepIdKey
 mkPolyTyConAppName    = varQual tYPEABLE_INTERNAL (fsLit "mkPolyTyConApp") mkPolyTyConAppKey
 mkAppTyName           = varQual tYPEABLE_INTERNAL (fsLit "mkAppTy")        mkAppTyKey
-typeLitTypeRepName    = varQual tYPEABLE_INTERNAL (fsLit "typeLitTypeRep") typeLitTypeRepKey
+typeNatTypeRepName    = varQual tYPEABLE_INTERNAL (fsLit "typeNatTypeRep") typeNatTypeRepKey
+typeSymbolTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeSymbolTypeRep") typeSymbolTypeRepKey
 
 
 -- Dynamic
@@ -1347,7 +1348,7 @@ ghciIoClassKey :: Unique
 ghciIoClassKey = mkPreludeClassUnique 44
 
 ---------------- Template Haskell -------------------
---      USES ClassUniques 200-299
+--      THNames.hs: USES ClassUniques 200-299
 -----------------------------------------------------
 
 {-
@@ -1494,9 +1495,6 @@ unknown2TyConKey                        = mkPreludeTyConUnique 131
 unknown3TyConKey                        = mkPreludeTyConUnique 132
 opaqueTyConKey                          = mkPreludeTyConUnique 133
 
-stringTyConKey :: Unique
-stringTyConKey                          = mkPreludeTyConUnique 134
-
 -- Generics (Unique keys)
 v1TyConKey, u1TyConKey, par1TyConKey, rec1TyConKey,
   k1TyConKey, m1TyConKey, sumTyConKey, prodTyConKey,
@@ -1584,7 +1582,7 @@ ipCoNameKey = mkPreludeTyConUnique 185
 
 
 ---------------- Template Haskell -------------------
---      USES TyConUniques 200-299
+--      THNames.hs: USES TyConUniques 200-299
 -----------------------------------------------------
 
 ----------------------- SIMD ------------------------
@@ -1664,9 +1662,14 @@ ipDataConKey :: Unique
 ipDataConKey                            = mkPreludeDataConUnique 38
 
 trTyConDataConKey, trModuleDataConKey, trNameSDataConKey :: Unique
-trTyConDataConKey                       = mkPreludeDataConUnique 185
-trModuleDataConKey                      = mkPreludeDataConUnique 186
-trNameSDataConKey                       = mkPreludeDataConUnique 187
+trTyConDataConKey                       = mkPreludeDataConUnique 40
+trModuleDataConKey                      = mkPreludeDataConUnique 41
+trNameSDataConKey                       = mkPreludeDataConUnique 42
+
+---------------- Template Haskell -------------------
+--      THNames.hs: USES DataUniques 100-150
+-----------------------------------------------------
+
 
 {-
 ************************************************************************
@@ -1922,20 +1925,22 @@ proxyHashKey :: Unique
 proxyHashKey = mkPreludeMiscIdUnique 502
 
 ---------------- Template Haskell -------------------
---      USES IdUniques 200-499
+--      THNames.hs: USES IdUniques 200-499
 -----------------------------------------------------
 
 -- Used to make `Typeable` dictionaries
 mkTyConKey
   , mkPolyTyConAppKey
   , mkAppTyKey
-  , typeLitTypeRepKey
+  , typeNatTypeRepKey
+  , typeSymbolTypeRepKey
   , typeRepIdKey
   :: Unique
 mkTyConKey            = mkPreludeMiscIdUnique 503
 mkPolyTyConAppKey     = mkPreludeMiscIdUnique 504
 mkAppTyKey            = mkPreludeMiscIdUnique 505
-typeLitTypeRepKey     = mkPreludeMiscIdUnique 506
+typeNatTypeRepKey     = mkPreludeMiscIdUnique 506
+typeSymbolTypeRepKey  = mkPreludeMiscIdUnique 507
 typeRepIdKey          = mkPreludeMiscIdUnique 508
 
 -- Dynamic
diff --git a/compiler/prelude/THNames.hs b/compiler/prelude/THNames.hs
index d3deb49ba2..c686db813c 100644
--- a/compiler/prelude/THNames.hs
+++ b/compiler/prelude/THNames.hs
@@ -445,23 +445,6 @@ unsafeName     = libFun (fsLit "unsafe") unsafeIdKey
 safeName       = libFun (fsLit "safe") safeIdKey
 interruptibleName = libFun (fsLit "interruptible") interruptibleIdKey
 
--- data Inline = ...
-noInlineDataConName, inlineDataConName, inlinableDataConName :: Name
-noInlineDataConName  = thCon (fsLit "NoInline")  noInlineDataConKey
-inlineDataConName    = thCon (fsLit "Inline")    inlineDataConKey
-inlinableDataConName = thCon (fsLit "Inlinable") inlinableDataConKey
-
--- data RuleMatch = ...
-conLikeDataConName, funLikeDataConName :: Name
-conLikeDataConName = thCon (fsLit "ConLike") conLikeDataConKey
-funLikeDataConName = thCon (fsLit "FunLike") funLikeDataConKey
-
--- data Phases = ...
-allPhasesDataConName, fromPhaseDataConName, beforePhaseDataConName :: Name
-allPhasesDataConName   = thCon (fsLit "AllPhases")   allPhasesDataConKey
-fromPhaseDataConName   = thCon (fsLit "FromPhase")   fromPhaseDataConKey
-beforePhaseDataConName = thCon (fsLit "BeforePhase") beforePhaseDataConKey
-
 -- newtype TExp a = ...
 tExpDataConName :: Name
 tExpDataConName = thCon (fsLit "TExp") tExpDataConKey
@@ -520,12 +503,42 @@ quotePatName        = qqFun (fsLit "quotePat")  quotePatKey
 quoteDecName        = qqFun (fsLit "quoteDec")  quoteDecKey
 quoteTypeName       = qqFun (fsLit "quoteType") quoteTypeKey
 
+-- data Inline = ...
+noInlineDataConName, inlineDataConName, inlinableDataConName :: Name
+noInlineDataConName  = thCon (fsLit "NoInline")  noInlineDataConKey
+inlineDataConName    = thCon (fsLit "Inline")    inlineDataConKey
+inlinableDataConName = thCon (fsLit "Inlinable") inlinableDataConKey
+
+-- data RuleMatch = ...
+conLikeDataConName, funLikeDataConName :: Name
+conLikeDataConName = thCon (fsLit "ConLike") conLikeDataConKey
+funLikeDataConName = thCon (fsLit "FunLike") funLikeDataConKey
+
+-- data Phases = ...
+allPhasesDataConName, fromPhaseDataConName, beforePhaseDataConName :: Name
+allPhasesDataConName   = thCon (fsLit "AllPhases")   allPhasesDataConKey
+fromPhaseDataConName   = thCon (fsLit "FromPhase")   fromPhaseDataConKey
+beforePhaseDataConName = thCon (fsLit "BeforePhase") beforePhaseDataConKey
+
+
+{- *********************************************************************
+*                                                                      *
+                     Class keys
+*                                                                      *
+********************************************************************* -}
+
 -- ClassUniques available: 200-299
 -- Check in PrelNames if you want to change this
 
 liftClassKey :: Unique
 liftClassKey = mkPreludeClassUnique 200
 
+{- *********************************************************************
+*                                                                      *
+                     TyCon keys
+*                                                                      *
+********************************************************************* -}
+
 -- TyConUniques available: 200-299
 -- Check in PrelNames if you want to change this
 
@@ -571,6 +584,43 @@ tExpTyConKey            = mkPreludeTyConUnique 230
 injAnnTyConKey          = mkPreludeTyConUnique 231
 kindTyConKey            = mkPreludeTyConUnique 232
 
+{- *********************************************************************
+*                                                                      *
+                     DataCon keys
+*                                                                      *
+********************************************************************* -}
+
+-- DataConUniques available: 100-150
+-- If you want to change this, make sure you check in PrelNames
+
+-- data Inline = ...
+noInlineDataConKey, inlineDataConKey, inlinableDataConKey :: Unique
+noInlineDataConKey  = mkPreludeDataConUnique 100
+inlineDataConKey    = mkPreludeDataConUnique 101
+inlinableDataConKey = mkPreludeDataConUnique 102
+
+-- data RuleMatch = ...
+conLikeDataConKey, funLikeDataConKey :: Unique
+conLikeDataConKey = mkPreludeDataConUnique 103
+funLikeDataConKey = mkPreludeDataConUnique 104
+
+-- data Phases = ...
+allPhasesDataConKey, fromPhaseDataConKey, beforePhaseDataConKey :: Unique
+allPhasesDataConKey   = mkPreludeDataConUnique 105
+fromPhaseDataConKey   = mkPreludeDataConUnique 106
+beforePhaseDataConKey = mkPreludeDataConUnique 107
+
+-- newtype TExp a = ...
+tExpDataConKey :: Unique
+tExpDataConKey = mkPreludeDataConUnique 108
+
+
+{- *********************************************************************
+*                                                                      *
+                     Id keys
+*                                                                      *
+********************************************************************* -}
+
 -- IdUniques available: 200-499
 -- If you want to change this, make sure you check in PrelNames
 
@@ -836,27 +886,6 @@ unsafeIdKey        = mkPreludeMiscIdUnique 430
 safeIdKey          = mkPreludeMiscIdUnique 431
 interruptibleIdKey = mkPreludeMiscIdUnique 432
 
--- data Inline = ...
-noInlineDataConKey, inlineDataConKey, inlinableDataConKey :: Unique
-noInlineDataConKey  = mkPreludeDataConUnique 40
-inlineDataConKey    = mkPreludeDataConUnique 41
-inlinableDataConKey = mkPreludeDataConUnique 42
-
--- data RuleMatch = ...
-conLikeDataConKey, funLikeDataConKey :: Unique
-conLikeDataConKey = mkPreludeDataConUnique 43
-funLikeDataConKey = mkPreludeDataConUnique 44
-
--- data Phases = ...
-allPhasesDataConKey, fromPhaseDataConKey, beforePhaseDataConKey :: Unique
-allPhasesDataConKey   = mkPreludeDataConUnique 45
-fromPhaseDataConKey   = mkPreludeDataConUnique 46
-beforePhaseDataConKey = mkPreludeDataConUnique 47
-
--- newtype TExp a = ...
-tExpDataConKey :: Unique
-tExpDataConKey = mkPreludeDataConUnique 48
-
 -- data FunDep = ...
 funDepIdKey :: Unique
 funDepIdKey = mkPreludeMiscIdUnique 440
diff --git a/compiler/simplCore/FloatIn.hs b/compiler/simplCore/FloatIn.hs
index 5390c48dd3..412125ae3e 100644
--- a/compiler/simplCore/FloatIn.hs
+++ b/compiler/simplCore/FloatIn.hs
@@ -25,7 +25,7 @@ import CoreUtils        ( exprIsDupable, exprIsExpandable, exprType,
 import CoreFVs          ( CoreExprWithFVs, freeVars, freeVarsOf, idRuleAndUnfoldingVars )
 import Id               ( isOneShotBndr, idType )
 import Var
-import Type             ( Type, isUnLiftedType, splitFunTy, applyTy )
+import Type             ( Type, isUnLiftedType, isFunTy, splitFunTy, applyTy )
 import VarSet
 import Util
 import UniqFM
@@ -168,7 +168,7 @@ fiExpr dflags to_drop ann_expr@(_,AnnApp {})
       = ((applyTy fun_ty ty, extra_fvs), emptyVarSet)
 
     mk_arg_fvs (fun_ty, extra_fvs) (arg_fvs, ann_arg)
-      | noFloatIntoRhs ann_arg arg_ty
+      | ASSERT( isFunTy fun_ty ) noFloatIntoRhs ann_arg arg_ty
       = ((res_ty, extra_fvs `unionVarSet` arg_fvs), emptyVarSet)
       | otherwise
       = ((res_ty, extra_fvs), arg_fvs)
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 9605ed57f8..d624a14760 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -648,10 +648,9 @@ tcGetDefaultTys
         -- Use [Integer, Double], plus modifications
         { integer_ty <- tcMetaTy integerTyConName
         ; checkWiredInTyCon doubleTyCon
-        ; string_ty <- tcMetaTy stringTyConName
         ; let deflt_tys = opt_deflt extended_defaults unitTy  -- Note [Default unitTy]
                           ++ [integer_ty, doubleTy]
-                          ++ opt_deflt ovl_strings string_ty
+                          ++ opt_deflt ovl_strings stringTy
         ; return (deflt_tys, flags) } } }
   where
     opt_deflt True  ty = [ty]
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 8b3ae04067..1cfa351125 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -740,10 +740,7 @@ data EvTerm
 -- | Instructions on how to make a 'Typeable' dictionary.
 -- See Note [Typeable evidence terms]
 data EvTypeable
-  = EvTypeableTyCon [EvTerm]
-    -- ^ Dictionary for @Typeable (T k1..kn t1..tn)@
-    -- The EvTerms are for the type args (but not the kind args)
-    -- We do not (yet) have dictionaries for kinds, (Typeable k)
+  = EvTypeableTyCon -- ^ Dictionary for @Typeable (T k1..kn)@
 
   | EvTypeableTyApp EvTerm EvTerm
     -- ^ Dictionary for @Typeable (s t)@,
@@ -783,7 +780,8 @@ inside can be EvIds.  Eg
     f x = typeRep (undefined :: Proxy [a])
 Here for the (Typeable [a]) dictionary passed to typeRep we make
 evidence
-    dl :: Typeable [a] = EvTypeable [a] (EvTypeableTyCon [EvId d]
+    dl :: Typeable [a] = EvTypeable [a]
+                            (EvTypeableTyApp EvTypeableTyCon (EvId d))
 where
     d :: Typable a
 is the lambda-bound dictionary passed into f.
@@ -1042,7 +1040,7 @@ evVarsOfCallStack cs = case cs of
 evVarsOfTypeable :: EvTypeable -> VarSet
 evVarsOfTypeable ev =
   case ev of
-    EvTypeableTyCon es    -> evVarsOfTerms es
+    EvTypeableTyCon       -> emptyVarSet
     EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
     EvTypeableTyLit e     -> evVarsOfTerm e
 
@@ -1101,16 +1099,16 @@ instance Outputable EvBind where
    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
 
 instance Outputable EvTerm where
-  ppr (EvId v)              = ppr v
-  ppr (EvCast v co)         = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
-  ppr (EvCoercion co)       = ptext (sLit "CO") <+> ppr co
-  ppr (EvSuperClass d n)    = ptext (sLit "sc") <> parens (ppr (d,n))
-  ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
-  ppr (EvLit l)             = ppr l
-  ppr (EvCallStack cs)      = ppr cs
-  ppr (EvDelayedError ty msg) =     ptext (sLit "error")
+  ppr (EvId v)                = ppr v
+  ppr (EvCast v co)           = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
+  ppr (EvCoercion co)         = ptext (sLit "CO") <+> ppr co
+  ppr (EvSuperClass d n)      = ptext (sLit "sc") <> parens (ppr (d,n))
+  ppr (EvDFunApp df tys ts)   = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
+  ppr (EvLit l)               = ppr l
+  ppr (EvCallStack cs)        = ppr cs
+  ppr (EvDelayedError ty msg) = ptext (sLit "error")
                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
-  ppr (EvTypeable _ ev) = ppr ev
+  ppr (EvTypeable ty ev)      = ppr ev <+> dcolon <+> ptext (sLit "Typeable") <+> ppr ty
 
 instance Outputable EvLit where
   ppr (EvNum n) = integer n
@@ -1125,11 +1123,9 @@ instance Outputable EvCallStack where
     = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
 
 instance Outputable EvTypeable where
-  ppr ev =
-    case ev of
-      EvTypeableTyCon  ks    -> parens (ptext (sLit "TC") <+> sep (map ppr ks))
-      EvTypeableTyApp t1 t2  -> parens (ppr t1 <+> ppr t2)
-      EvTypeableTyLit t1     -> ptext (sLit "TyLit") <> ppr t1
+  ppr EvTypeableTyCon         = ptext (sLit "TC")
+  ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
+  ppr (EvTypeableTyLit t1)    = ptext (sLit "TyLit") <> ppr t1
 
 
 ----------------------------------------------------------------------
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 1f3e3115a4..c62246fc44 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1294,9 +1294,8 @@ zonkEvTerm env (EvDelayedError ty msg)
        ; return (EvDelayedError ty' msg) }
 
 zonkEvTypeable :: ZonkEnv -> EvTypeable -> TcM EvTypeable
-zonkEvTypeable env (EvTypeableTyCon ts)
-  = do { ts' <- mapM (zonkEvTerm env) ts
-       ; return (EvTypeableTyCon ts') }
+zonkEvTypeable _ EvTypeableTyCon
+  = return EvTypeableTyCon
 zonkEvTypeable env (EvTypeableTyApp t1 t2)
   = do { t1' <- zonkEvTerm env t1
        ; t2' <- zonkEvTerm env t2
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 4b531593a8..47147d7a4d 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -14,7 +14,7 @@ import TcCanonical
 import TcFlatten
 import VarSet
 import Type
-import Kind ( isKind, isConstraintKind )
+import Kind ( isKind )
 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
 import CoAxiom( sfInteractTop, sfInteractInert )
 
@@ -23,7 +23,7 @@ import TcType
 import Name
 import PrelNames ( knownNatClassName, knownSymbolClassName,
                    callStackTyConKey, typeableClassName )
-import TysWiredIn ( ipClass )
+import TysWiredIn ( ipClass, typeNatKind, typeSymbolKind )
 import Id( idType )
 import CoAxiom ( Eqn, CoAxiom(..), CoAxBranch(..), fromBranches )
 import Class
@@ -1926,12 +1926,12 @@ matchCTuple clas tys   -- (isCTupleClass clas) holds
 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
 matchKnownNat clas [ty]     -- clas = KnownNat
   | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
-matchKnownNat _ _        = return NoInstance
+matchKnownNat _ _           = return NoInstance
 
 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
 matchKnownSymbol clas [ty]  -- clas = KnownSymbol
   | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
-matchKnownSymbol _ _     = return NoInstance
+matchKnownSymbol _ _       = return NoInstance
 
 
 makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
@@ -1973,37 +1973,35 @@ makeLitDict clas ty evLit
 -- and it was applied to the correct argument.
 matchTypeable :: Class -> [Type] -> TcS LookupInstResult
 matchTypeable clas [k,t]  -- clas = Typeable
-  | isForAllTy k                            = return NoInstance
-  | isConstraintKind k                      = return NoInstance
-  | Just _ <- isNumLitTy t                  = doTyLit knownNatClassName    t
-  | Just _ <- isStrLitTy t                  = doTyLit knownSymbolClassName t
-  | Just (tc, kts) <- splitTyConApp_maybe t = doTyConApp clas t tc kts
-  | Just (f,kt)   <- splitAppTy_maybe t     = doTyApp    clas t f kt
-  | otherwise                               = return NoInstance
-matchTypeable _ _ = return NoInstance  -- Ill-kinded, so should not happen
-
-doTyConApp :: Class -> Type -> TyCon -> [KindOrType] -> TcS LookupInstResult
--- Representation for type constructor applied to some kinds
-doTyConApp clas ty tc kts
-  | (ks, ts) <- splitTyConArgs tc kts
-  , all is_ground_kind ks
-  = return $ GenInst (map (mk_typeable_pred clas) ts)
-                     (\tReps -> EvTypeable ty $ EvTypeableTyCon
-                                (map EvId tReps))
-                     True
-  | otherwise
-  = return NoInstance
-
-  where
-    -- Representation for concrete kinds.  We just use the kind itself,
-    -- but first check to make sure that it is "simple" (i.e., made entirely
-    -- out of kind constructors).
-  is_ground_kind k
-    | Just (_, ks) <- splitTyConApp_maybe k
-    = all is_ground_kind ks
-    | otherwise
-    = False
-
+  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
+  | isForAllTy k                      = return NoInstance   -- Polytype
+  | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
+
+  -- Now cases that do work
+  | k `eqType` typeNatKind                 = doTyLit knownNatClassName    t
+  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName t
+  | Just (_, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
+  , all isGroundKind ks                    = doTyConApp t
+  | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
+
+matchTypeable _ _ = return NoInstance
+
+doTyConApp :: Type -> TcS LookupInstResult
+-- Representation for type constructor applied to some (ground) kinds
+doTyConApp ty = return $ GenInst [] (\_ -> EvTypeable ty EvTypeableTyCon) True
+
+-- Representation for concrete kinds.  We just use the kind itself,
+-- but first check to make sure that it is "simple" (i.e., made entirely
+-- out of kind constructors).
+isGroundKind :: KindOrType -> Bool
+-- Return True if (a) k is a kind and (b) it is a ground kind
+isGroundKind k
+ = isKind k && is_ground k
+ where
+   is_ground k | Just (_, ks) <- splitTyConApp_maybe k
+               = all is_ground ks
+               | otherwise
+               = False
 
 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
 -- Representation for an application of a type to a type-or-kind.
@@ -2029,15 +2027,29 @@ mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
   -- we generate a sub-goal for the appropriate class. See #10348 for what
   -- happens when we fail to do this.
 doTyLit :: Name -> Type -> TcS LookupInstResult
-doTyLit c t = do clas <- tcLookupClass c
-                 let p = mkClassPred clas [ t ]
-                 return $ GenInst [p]
-                                  (\[ev] -> EvTypeable t
-                                            $ EvTypeableTyLit $ EvId ev)
-                                  True
-
-{- Note [No Typeable for polytype or for constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+doTyLit kc t = do { kc_clas <- tcLookupClass kc
+                  ; let kc_pred    = mkClassPred kc_clas [ t ]
+                        mk_ev [ev] = EvTypeable t $ EvTypeableTyLit $ EvId ev
+                        mk_ev _    = panic "doTyLit"
+                  ; return (GenInst [kc_pred] mk_ev True) }
+
+{- Note [Typeable (T a b c)]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For type applications we always decompose using binary application,
+vai doTyApp, until we get to a *kind* instantiation.  Exmaple
+   Proxy :: forall k. k -> *
+
+To solve Typeable (Proxy (* -> *) Maybe) we
+  - First decompose with doTyApp,
+    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
+  - Then sovle (Typeable (Proxy (* -> *))) with doTyConApp
+
+If we attempt to short-cut by solving it all at once, via
+doTyCOnAPp
+
+
+Note [No Typeable for polytypes or qualified types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We do not support impredicative typeable, such as
    Typeable (forall a. a->a)
    Typeable (Eq a => a -> a)
@@ -2051,9 +2063,9 @@ a TypeRep for them.  For qualified but not polymorphic types, like
  * We don't need a TypeRep for these things.  TypeReps are for
    monotypes only.
 
-  * Perhaps we could treat `=>` as another type constructor for `Typeable`
-    purposes, and thus support things like `Eq Int => Int`, however,
-    at the current state of affairs this would be an odd exception as
-    no other class works with impredicative types.
-    For now we leave it off, until we have a better story for impredicativity.
+ * Perhaps we could treat `=>` as another type constructor for `Typeable`
+   purposes, and thus support things like `Eq Int => Int`, however,
+   at the current state of affairs this would be an odd exception as
+   no other class works with impredicative types.
+   For now we leave it off, until we have a better story for impredicativity.
 -}
diff --git a/ghc/InteractiveUI.hs b/ghc/InteractiveUI.hs
index 2dcedb0b0b..52bcb36005 100644
--- a/ghc/InteractiveUI.hs
+++ b/ghc/InteractiveUI.hs
@@ -1342,7 +1342,7 @@ defineMacro overwrite s = do
     step <- getGhciStepIO
     expr <- GHC.parseExpr definition
     -- > ghciStepIO . definition :: String -> IO String
-    let stringTy = nlHsTyVar $ getRdrName stringTyConName
+    let stringTy = nlHsTyVar stringTy_RDR
         ioM = nlHsTyVar (getRdrName ioTyConName) `nlHsAppTy` stringTy
         body = nlHsVar compose_RDR `mkHsApp` step `mkHsApp` expr
         tySig = stringTy `nlHsFunTy` ioM
@@ -1392,7 +1392,7 @@ cmdCmd str = handleSourceError GHC.printException $ do
 getGhciStepIO :: GHCi (LHsExpr RdrName)
 getGhciStepIO = do
   ghciTyConName <- GHC.getGHCiMonad
-  let stringTy = nlHsTyVar $ getRdrName stringTyConName
+  let stringTy = nlHsTyVar stringTy_RDR
       ghciM = nlHsTyVar (getRdrName ghciTyConName) `nlHsAppTy` stringTy
       ioM = nlHsTyVar (getRdrName ioTyConName) `nlHsAppTy` stringTy
       body = nlHsVar (getRdrName ghciStepIoMName)
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index f36db6a1d9..4379155c57 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -67,13 +67,14 @@ module Data.Typeable.Internal (
     rnfTypeRep,
     showsTypeRep,
     typeRepKinds,
-    typeLitTypeRep,
+    typeSymbolTypeRep, typeNatTypeRep
   ) where
 
 import GHC.Base
 import GHC.Word
 import GHC.Show
 import Data.Proxy
+import GHC.TypeLits( KnownNat, KnownSymbol, natVal', symbolVal' )
 
 import GHC.Fingerprint.Type
 import {-# SOURCE #-} GHC.Fingerprint
@@ -145,9 +146,6 @@ mkTyCon3 pkg modl name
     fingerprint :: Fingerprint
     fingerprint = fingerprintString (pkg ++ (' ':modl) ++ (' ':name))
 
-mkTypeLitTyCon :: Addr# -> TyCon
-mkTypeLitTyCon name = mkTyCon3# "base"# "GHC.TypeLits"# name
-
 isTupleTyCon :: TyCon -> Bool
 isTupleTyCon tc
   | ('(':',':_) <- tyConName tc = True
@@ -263,10 +261,6 @@ mkAppTy (TypeRep _ tc ks trs) arg_tr = mkPolyTyConApp tc ks (trs ++ [arg_tr])
    -- ensure that a TypeRep of the same shape has the same fingerprint!
    -- See Trac #5962
 
--- | An internal function, to make representations for type literals.
-typeLitTypeRep :: Addr# -> TypeRep
-typeLitTypeRep nm = mkTyConApp (mkTypeLitTyCon nm) []
-
 ----------------- Observation ---------------------
 
 -- | Observe the type constructor of a type representation
@@ -397,9 +391,9 @@ showTuple args = showChar '('
                . showChar ')'
 
 {- *********************************************************
-            TyCon definitions for GHC.Types
-
-   The Ty
+*                                                          *
+*            TyCon definitions for GHC.Types               *
+*                                                          *
 ********************************************************* -}
 
 mkGhcTypesTyCon :: Addr# -> TyCon
@@ -446,3 +440,27 @@ tcConstraint   = mkGhcTypesTyCon "Constraint"#
 
 funTc :: TyCon
 funTc = tcFun   -- Legacy
+
+{- *********************************************************
+*                                                          *
+*       TyCon/TypeRep definitions for type literals        *
+*              (Symbol and Nat)                            *
+*                                                          *
+********************************************************* -}
+
+
+mkTypeLitTyCon :: String -> TyCon
+mkTypeLitTyCon name = mkTyCon3 "base" "GHC.TypeLits" name
+
+-- | Used to make `'Typeable' instance for things of kind Nat
+typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep
+typeNatTypeRep p = typeLitTypeRep (show (natVal' p))
+
+-- | Used to make `'Typeable' instance for things of kind Symbol
+typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep
+typeSymbolTypeRep p = typeLitTypeRep (show (symbolVal' p))
+
+-- | An internal function, to make representations for type literals.
+typeLitTypeRep :: String -> TypeRep
+typeLitTypeRep nm = mkTyConApp (mkTypeLitTyCon nm) []
+