From 60229e9ee23afd302766475462767516cc294409 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 18 Jun 2019 20:17:00 -0400 Subject: 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. --- compiler/ghc.cabal.in | 1 - compiler/typecheck/ClsInst.hs | 2 +- compiler/typecheck/TcBinds.hs | 17 ------- compiler/typecheck/TcEnv.hs | 11 +++++ compiler/typecheck/TcTyDecls.hs | 2 +- compiler/typecheck/TcType.hs | 1 - compiler/typecheck/TcTypeable.hs | 77 ++++++++++++++++++++++++++++++-- compiler/typecheck/TcTypeableValidity.hs | 46 ------------------- 8 files changed, 86 insertions(+), 71 deletions(-) delete mode 100644 compiler/typecheck/TcTypeableValidity.hs 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 -- cgit v1.2.1