Commit 25ee60cd authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

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.
parent 57b71848
Pipeline #7192 passed with stages
in 313 minutes and 11 seconds
......@@ -525,6 +525,7 @@ Library
TcTyClsDecls
TcTyDecls
TcTypeable
TcTypeableValidity
TcType
TcEvidence
TcEvTerm
......
......@@ -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 }
......
......@@ -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
......
{-
(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
{-# 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
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
......@@ -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'])
......
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