Merge TcTypeableValidity into TcTypeable, document treatment of casts

This patch:

* Implements a refactoring (suggested in
  https://gitlab.haskell.org/ghc/ghc/merge_requests/1199#note_207345)
  that moves all functions from `TcTypeableValidity` back to
  `TcTypeable`, as the former module doesn't really need to live on its
  own.
* Adds `Note [Typeable instances for casted types]` to `TcTypeable`
  explaining why the `Typeable` solver currently does not support
  types containing casts.

Resolves #16835.

8 files changed, 86 insertions, 71 deletions

diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index fdbe9d5df6..ea12b5563d 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -523,7 +523,6 @@ Library
         TcTyClsDecls
         TcTyDecls
         TcTypeable
-        TcTypeableValidity
         TcType
         TcEvidence
         TcEvTerm
diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs
index 420cbaebd0..5e3501deda 100644
--- a/compiler/typecheck/ClsInst.hs
+++ b/compiler/typecheck/ClsInst.hs
@@ -14,9 +14,9 @@ import GhcPrelude
 import TcEnv
 import TcRnMonad
 import TcType
+import TcTypeable
 import TcMType
 import TcEvidence
-import TcTypeableValidity
 import RnEnv( addUsedGRE )
 import RdrName( lookupGRE_FieldLabel )
 import InstEnv
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 8f14abe32f..e909556e06 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -12,7 +12,6 @@
 
 module TcBinds ( tcLocalBinds, tcTopBinds, tcValBinds,
                  tcHsBootSigs, tcPolyCheck,
-                 addTypecheckedBinds,
                  chooseInferredQuantifiers,
                  badBootDeclErr ) where
 
@@ -26,7 +25,6 @@ import CostCentre (mkUserCC, CCFlavour(DeclCC))
 import DynFlags
 import FastString
 import GHC.Hs
-import HscTypes( isHsBootOrSig )
 import TcSigs
 import TcRnMonad
 import TcEnv
@@ -71,21 +69,6 @@ import Data.Foldable (find)
 
 #include "HsVersions.h"
 
-{- *********************************************************************
-*                                                                      *
-               A useful helper function
-*                                                                      *
-********************************************************************* -}
-
-addTypecheckedBinds :: TcGblEnv -> [LHsBinds GhcTc] -> TcGblEnv
-addTypecheckedBinds tcg_env binds
-  | isHsBootOrSig (tcg_src tcg_env) = tcg_env
-    -- Do not add the code for record-selector bindings
-    -- when compiling hs-boot files
-  | otherwise = tcg_env { tcg_binds = foldr unionBags
-                                            (tcg_binds tcg_env)
-                                            binds }
-
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 2d59dc191b..6ce37583a0 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -25,6 +25,7 @@ module TcEnv(
         tcLookupLocatedGlobalId, tcLookupLocatedTyCon,
         tcLookupLocatedClass, tcLookupAxiom,
         lookupGlobal, ioLookupDataCon,
+        addTypecheckedBinds,
 
         -- Local environment
         tcExtendKindEnv, tcExtendKindEnvList,
@@ -103,6 +104,7 @@ import Module
 import Outputable
 import Encoding
 import FastString
+import Bag
 import ListSetOps
 import ErrUtils
 import Maybes( MaybeErr(..), orElse )
@@ -184,6 +186,15 @@ ioLookupDataCon_maybe hsc_env name = do
           pprTcTyThingCategory (AGlobal thing) <+> quotes (ppr name) <+>
                 text "used as a data constructor"
 
+addTypecheckedBinds :: TcGblEnv -> [LHsBinds GhcTc] -> TcGblEnv
+addTypecheckedBinds tcg_env binds
+  | isHsBootOrSig (tcg_src tcg_env) = tcg_env
+    -- Do not add the code for record-selector bindings
+    -- when compiling hs-boot files
+  | otherwise = tcg_env { tcg_binds = foldr unionBags
+                                            (tcg_binds tcg_env)
+                                            binds }
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 132ced5fae..09a6be7a69 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -33,7 +33,7 @@ import GhcPrelude
 
 import TcRnMonad
 import TcEnv
-import TcBinds( tcValBinds, addTypecheckedBinds )
+import TcBinds( tcValBinds )
 import TyCoRep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) )
 import TcType
 import TysWiredIn( unitTy )
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 7fa45ae8f3..1d3ec0d568 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -2183,7 +2183,6 @@ isRigidTy ty
   | isForAllTy ty                           = True
   | otherwise                               = False
 
-
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs
index f85f647632..60a0f5e3b3 100644
--- a/compiler/typecheck/TcTypeable.hs
+++ b/compiler/typecheck/TcTypeable.hs
@@ -8,20 +8,19 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 
-module TcTypeable(mkTypeableBinds) where
+module TcTypeable(mkTypeableBinds, tyConIsTypeable) where
 
 #include "HsVersions.h"
 
 import GhcPrelude
 
 import BasicTypes ( Boxity(..), neverInlinePragma, SourceText(..) )
-import TcBinds( addTypecheckedBinds )
 import IfaceEnv( newGlobalBinder )
 import TyCoRep( Type(..), TyLit(..) )
 import TcEnv
 import TcEvidence ( mkWpTyApps )
 import TcRnMonad
-import TcTypeableValidity
+import TcType
 import HscTypes ( lookupId )
 import PrelNames
 import TysPrim ( primTyCons )
@@ -46,6 +45,7 @@ import FastString ( FastString, mkFastString, fsLit )
 
 import Control.Monad.Trans.State
 import Control.Monad.Trans.Class (lift)
+import Data.Maybe ( isJust )
 import Data.Word( Word64 )
 
 {- Note [Grand plan for Typeable]
@@ -254,7 +254,7 @@ todoForTyCons mod mod_id tycons = do
               -- Do, however, make them for their promoted datacon (see #13915).
             , not $ isFamInstTyCon tc''
             , Just rep_name <- pure $ tyConRepName_maybe tc''
-            , typeIsTypeable $ dropForAlls $ tyConKind tc''
+            , tyConIsTypeable tc''
             ]
     return TypeRepTodo { mod_rep_expr    = nlHsVar mod_id
                        , pkg_fingerprint = pkg_fpr
@@ -414,6 +414,36 @@ mkTyConRepBinds stuff todo (TypeableTyCon {..})
            tycon_rep_bind = mkVarBind tycon_rep_id tycon_rep_rhs
        return $ unitBag tycon_rep_bind
 
+-- | Is a particular 'TyCon' representable by @Typeable@?. These exclude type
+-- families and polytypes.
+tyConIsTypeable :: TyCon -> Bool
+tyConIsTypeable tc =
+       isJust (tyConRepName_maybe tc)
+    && kindIsTypeable (dropForAlls $ tyConKind tc)
+
+-- | Is a particular 'Kind' representable by @Typeable@? Here we look for
+-- polytypes and types containing casts (which may be, for instance, a type
+-- family).
+kindIsTypeable :: Kind -> Bool
+-- We handle types of the form (TYPE LiftedRep) specifically to avoid
+-- looping on (tyConIsTypeable RuntimeRep). We used to consider (TYPE rr)
+-- to be typeable without inspecting rr, but this exhibits bad behavior
+-- when rr is a type family.
+kindIsTypeable ty
+  | Just ty' <- coreView ty         = kindIsTypeable ty'
+kindIsTypeable ty
+  | isLiftedTypeKind ty             = True
+kindIsTypeable (TyVarTy _)          = True
+kindIsTypeable (AppTy a b)          = kindIsTypeable a && kindIsTypeable b
+kindIsTypeable (FunTy _ a b)        = kindIsTypeable a && kindIsTypeable b
+kindIsTypeable (TyConApp tc args)   = tyConIsTypeable tc
+                                   && all kindIsTypeable args
+kindIsTypeable (ForAllTy{})         = False
+kindIsTypeable (LitTy _)            = True
+kindIsTypeable (CastTy{})           = False
+  -- See Note [Typeable instances for casted types]
+kindIsTypeable (CoercionTy{})       = False
+
 -- | Maps kinds to 'KindRep' bindings. This binding may either be defined in
 -- some other module (in which case the @Maybe (LHsExpr Id@ will be 'Nothing')
 -- or a binding which we generated in the current module (in which case it will
@@ -575,6 +605,7 @@ mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep
                  `nlHsApp` nlHsDataCon typeLitSymbolDataCon
                  `nlHsApp` nlHsLit (mkHsStringPrimLit $ mkFastString $ show s)
 
+    -- See Note [Typeable instances for casted types]
     new_kind_rep (CastTy ty co)
       = pprPanic "mkTyConKindRepBinds.go(cast)" (ppr ty $$ ppr co)
 
@@ -673,6 +704,44 @@ polymorphic types.  So instead
                  | KindRepApp KindRep KindRep
                  | KindRepFun KindRep KindRep
                  ...
+
+Note [Typeable instances for casted types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+At present, GHC does not manufacture TypeReps for types containing casts
+(#16835). In theory, GHC could do so today, but it might be dangerous tomorrow.
+
+In today's GHC, we normalize all types before computing their TypeRep.
+For example:
+
+    type family F a
+    type instance F Int = Type
+
+    data D = forall (a :: F Int). MkD a
+
+    tr :: TypeRep (MkD Bool)
+    tr = typeRep
+
+When computing the TypeRep for `MkD Bool` (or rather,
+`MkD (Bool |> Sym (FInt[0]))`), we simply discard the cast to obtain the
+TypeRep for `MkD Bool`.
+
+Why does this work? If we have a type definition with casts, then the
+only coercions that those casts can mention are either Refl, type family
+axioms, built-in axioms, and coercions built from those roots. Therefore,
+type family (and built-in) axioms will apply precisely when type normalization
+succeeds (i.e, the type family applications are reducible). Therefore, it
+is safe to ignore the cast entirely when constructing the TypeRep.
+
+This approach would be fragile in a future where GHC permits other forms of
+coercions to appear in casts (e.g., coercion quantification as described
+in #15710). If GHC permits local assumptions to appear in casts that cannot be
+reduced with conventional normalization, then discarding casts would become
+unsafe. It would be unfortunate for the Typeable solver to become a roadblock
+obstructing such a future, so we deliberately do not implement the ability
+for TypeReps to represent types with casts at the moment.
+
+If we do wish to allow this in the future, it will likely require modeling
+casts and coercions in TypeReps themselves.
 -}
 
 mkList :: Type -> [LHsExpr GhcTc] -> LHsExpr GhcTc
diff --git a/compiler/typecheck/TcTypeableValidity.hs b/compiler/typecheck/TcTypeableValidity.hs
deleted file mode 100644
index 9e30be3589..0000000000
--- a/compiler/typecheck/TcTypeableValidity.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-{-
-(c) The University of Glasgow 2006
-(c) The GRASP/AQUA Project, Glasgow University, 1992-1999
--}
-
--- | This module is separate from "TcTypeable" because the functions in this
--- module are used in "ClsInst", and importing "TcTypeable" from "ClsInst"
--- would lead to an import cycle.
-module TcTypeableValidity (tyConIsTypeable, typeIsTypeable) where
-
-import GhcPrelude
-
-import TyCoRep
-import TyCon
-import Type
-
-import Data.Maybe (isJust)
-
--- | Is a particular 'TyCon' representable by @Typeable@?. These exclude type
--- families and polytypes.
-tyConIsTypeable :: TyCon -> Bool
-tyConIsTypeable tc =
-       isJust (tyConRepName_maybe tc)
-    && typeIsTypeable (dropForAlls $ tyConKind tc)
-
--- | Is a particular 'Type' representable by @Typeable@? Here we look for
--- polytypes and types containing casts (which may be, for instance, a type
--- family).
-typeIsTypeable :: Type -> Bool
--- We handle types of the form (TYPE LiftedRep) specifically to avoid
--- looping on (tyConIsTypeable RuntimeRep). We used to consider (TYPE rr)
--- to be typeable without inspecting rr, but this exhibits bad behavior
--- when rr is a type family.
-typeIsTypeable ty
-  | Just ty' <- coreView ty         = typeIsTypeable ty'
-typeIsTypeable ty
-  | isLiftedTypeKind ty             = True
-typeIsTypeable (TyVarTy _)          = True
-typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
-typeIsTypeable (FunTy _ a b)        = typeIsTypeable a && typeIsTypeable b
-typeIsTypeable (TyConApp tc args)   = tyConIsTypeable tc
-                                   && all typeIsTypeable args
-typeIsTypeable (ForAllTy{})         = False
-typeIsTypeable (LitTy _)            = True
-typeIsTypeable (CastTy{})           = False
-typeIsTypeable (CoercionTy{})       = False