diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2019-06-14 11:07:46 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-06-15 23:35:03 -0400 |
commit | 25ee60cdae6ddedaf6b4677c6327c0f31c81073a (patch) | |
tree | 7cd719be751cda761613ac86ae8f11181e1b7a09 | |
parent | 57b718481d5363ab33df4c7814f74897418f79d7 (diff) | |
download | haskell-25ee60cdae6ddedaf6b4677c6327c0f31c81073a.tar.gz |
Synchronize ClsInst.doTyConApp with TcTypeable validity checks (#15862)
Issue #15862 demonstrated examples of type constructors on which
`TcTypeable.tyConIsTypeable` would return `False`, but the `Typeable`
constraint solver in `ClsInst` (in particular, `doTyConApp`) would
try to generate `Typeable` evidence for anyway, resulting in
disaster. This incongruity was caused by the fact that `doTyConApp`
was using a weaker validity check than `tyConIsTypeable` to determine
if a type constructor warrants `Typeable` evidence or not. The
solution, perhaps unsurprisingly, is to use `tyConIsTypeable` in
`doTyConApp` instead.
To avoid import cycles between `ClsInst` and `TcTypeable`, I factored
out `tyConIsTypeable` into its own module, `TcTypeableValidity`.
Fixes #15862.
-rw-r--r-- | compiler/ghc.cabal.in | 1 | ||||
-rw-r--r-- | compiler/typecheck/ClsInst.hs | 3 | ||||
-rw-r--r-- | compiler/typecheck/TcTypeable.hs | 36 | ||||
-rw-r--r-- | compiler/typecheck/TcTypeableValidity.hs | 46 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15862.hs | 36 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15862.stderr | 28 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
7 files changed, 116 insertions, 35 deletions
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index e1f0bec2b0..d380d96707 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -525,6 +525,7 @@ Library TcTyClsDecls TcTyDecls TcTypeable + TcTypeableValidity TcType TcEvidence TcEvTerm diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs index 58b9734b05..420cbaebd0 100644 --- a/compiler/typecheck/ClsInst.hs +++ b/compiler/typecheck/ClsInst.hs @@ -16,6 +16,7 @@ import TcRnMonad import TcType import TcMType import TcEvidence +import TcTypeableValidity import RnEnv( addUsedGRE ) import RdrName( lookupGRE_FieldLabel ) import InstEnv @@ -432,7 +433,7 @@ doFunTy clas ty arg_ty ret_ty -- of monomorphic kind (e.g. all kind variables have been instantiated). doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult doTyConApp clas ty tc kind_args - | Just _ <- tyConRepName_maybe tc + | tyConIsTypeable tc = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args) , cir_mk_ev = mk_ev , cir_what = BuiltinInstance } diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs index 3488957366..eb679e6daf 100644 --- a/compiler/typecheck/TcTypeable.hs +++ b/compiler/typecheck/TcTypeable.hs @@ -17,10 +17,11 @@ import GhcPrelude import BasicTypes ( Boxity(..), neverInlinePragma, SourceText(..) ) import TcBinds( addTypecheckedBinds ) import IfaceEnv( newGlobalBinder ) -import TyCoRep( Type(..), TyLit(..), isLiftedTypeKind ) +import TyCoRep( Type(..), TyLit(..) ) import TcEnv import TcEvidence ( mkWpTyApps ) import TcRnMonad +import TcTypeableValidity import HscTypes ( lookupId ) import PrelNames import TysPrim ( primTyCons ) @@ -45,7 +46,6 @@ 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] @@ -412,38 +412,6 @@ mkTyConRepBinds stuff todo (TypeableTyCon {..}) tycon_rep_bind = mkVarBind tycon_rep_id tycon_rep_rhs return $ unitBag tycon_rep_bind --- | Here is where we define the set of Typeable types. These exclude type --- families and polytypes. -tyConIsTypeable :: TyCon -> Bool -tyConIsTypeable tc = - isJust (tyConRepName_maybe tc) - && typeIsTypeable (dropForAlls $ tyConKind tc) - -- Ensure that the kind of the TyCon, with its initial foralls removed, - -- is representable (e.g. has no higher-rank polymorphism or type - -- synonyms). - --- | 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 - -- | 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 diff --git a/compiler/typecheck/TcTypeableValidity.hs b/compiler/typecheck/TcTypeableValidity.hs new file mode 100644 index 0000000000..9e30be3589 --- /dev/null +++ b/compiler/typecheck/TcTypeableValidity.hs @@ -0,0 +1,46 @@ +{- +(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 diff --git a/testsuite/tests/typecheck/should_fail/T15862.hs b/testsuite/tests/typecheck/should_fail/T15862.hs new file mode 100644 index 0000000000..c98b5939d1 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15862.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UnboxedSums #-} +module Bug where + +import Data.Kind +import Type.Reflection + +newtype Foo = MkFoo (forall a. a) + +foo :: TypeRep MkFoo +foo = typeRep @MkFoo + +type family F a +type instance F Int = Type + +data Bar = forall (a :: F Int). MkBar a + +bar :: TypeRep (MkBar True) +bar = typeRep + +data Quux = MkQuux (# Bool | Int #) + +quux :: TypeRep MkQuux +quux = typeRep + +data Quuz :: (Type ~ Type) => Type where + MkQuuz :: Quuz + +quuz :: TypeRep MkQuuz +quuz = typeRep diff --git a/testsuite/tests/typecheck/should_fail/T15862.stderr b/testsuite/tests/typecheck/should_fail/T15862.stderr new file mode 100644 index 0000000000..97fbfab166 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15862.stderr @@ -0,0 +1,28 @@ + +T15862.hs:17:7: error: + • No instance for (Typeable 'MkFoo) arising from a use of ‘typeRep’ + GHC can't yet do polykinded + Typeable ('MkFoo :: (forall a. a) -> Foo) + • In the expression: typeRep @MkFoo + In an equation for ‘foo’: foo = typeRep @MkFoo + +T15862.hs:25:7: error: + • No instance for (Typeable 'MkBar) arising from a use of ‘typeRep’ + GHC can't yet do polykinded Typeable ('MkBar :: Bool -> Bar) + • In the expression: typeRep + In an equation for ‘bar’: bar = typeRep + +T15862.hs:30:8: error: + • No instance for (Typeable 'MkQuux) + arising from a use of ‘typeRep’ + GHC can't yet do polykinded + Typeable ('MkQuux :: (# Bool | Int #) -> Quux) + • In the expression: typeRep + In an equation for ‘quux’: quux = typeRep + +T15862.hs:36:8: error: + • No instance for (Typeable 'MkQuuz) + arising from a use of ‘typeRep’ + GHC can't yet do polykinded Typeable ('MkQuuz :: Quuz) + • In the expression: typeRep + In an equation for ‘quuz’: quuz = typeRep diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 7ee15ebc4c..0b0ae59391 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -503,6 +503,7 @@ test('T15797', normal, compile_fail, ['']) test('T15799', normal, compile_fail, ['']) test('T15801', normal, compile_fail, ['']) test('T15816', normal, compile_fail, ['']) +test('T15862', normal, compile_fail, ['']) test('T16059a', normal, compile_fail, ['']) test('T16059c', [extra_files(['T16059b.hs'])], multimod_compile_fail, ['T16059c', '-v0']) |