Commit 60229e9e authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Merge TcTypeableValidity into TcTypeable, document treatment of casts

This patch:

* Implements a refactoring (suggested in
  !1199 (comment 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.
parent 53b0c6e0
......@@ -523,7 +523,6 @@ Library
TcTyClsDecls
TcTyDecls
TcTypeable
TcTypeableValidity
TcType
TcEvidence
TcEvTerm
......
......@@ -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
......
......@@ -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 }
{-
************************************************************************
* *
......
......@@ -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 }
{-
************************************************************************
* *
......
......@@ -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 )
......
......@@ -2183,7 +2183,6 @@ isRigidTy ty
| isForAllTy ty = True
| otherwise = False
{-
************************************************************************
* *
......
......@@ -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
......
{-
(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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment