Commit ff3904d9 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Change GeneralizedNewtypeDeriving safety check.

Now, instead of looking at a class's roles, the GND check looks
at all of the methods in the class individually. This has the
advantage that sometimes, we can use information about the
derivation requested during the safety check. For example,
we can now derive (IArray UArray), whereas the previous check
prevented this.
parent 755bdc83
......@@ -74,6 +74,8 @@ import Util
import Control.Monad( when )
import MonadUtils
import Control.Monad(liftM)
import TcRnMonad (traceIf) -- RAE
\end{code}
%************************************************************************
......@@ -838,15 +840,18 @@ dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
-- k (trans g1# g2#)
-- thing_inside will get a coercion at the role requested
dsTcCoercion role co thing_inside
= do { us <- newUniqueSupply
= do { traceIf $ hang (text "dsTcCoercion {") 2 $ vcat [ppr role, ppr co] -- RAE
; us <- newUniqueSupply
; let eqvs_covs :: [(EqVar,CoVar)]
eqvs_covs = zipWith mk_co_var (varSetElems (coVarsOfTcCo co))
(uniqsFromSupply us)
subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
result_expr = thing_inside (ds_tc_coercion subst role co)
ds_co = ds_tc_coercion subst role co -- RAE
result_expr = thing_inside ds_co
result_ty = exprType result_expr
; traceIf $ hang (text "dsTcCoercion }") 2 (ppr ds_co) -- RAE
; return (foldr (wrap_in_case result_ty) result_expr eqvs_covs) }
where
mk_co_var :: Id -> Unique -> (Id, Id)
......@@ -875,7 +880,9 @@ ds_tc_coercion subst role tc_co
go r (TcRefl ty) = Refl r (Coercion.substTy subst ty)
go r (TcTyConAppCo tc cos) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) cos)
go r (TcAppCo co1 co2) = mkAppCo (go r co1) (go Nominal co2)
go r (TcAppCo co1 co2) = let leftCo = go r co1
rightRole = nextRole leftCo in
mkAppCoFlexible leftCo rightRole (go rightRole co2)
go r (TcForAllCo tv co) = mkForAllCo tv' (ds_tc_coercion subst' r co)
where
(subst', tv') = Coercion.substTyVarBndr subst tv
......
......@@ -39,6 +39,7 @@ import Id( idType )
import Class
import Type
import Kind( isKind )
import Coercion ( tvUsedAtNominalRole )
import ErrUtils
import MkId
import DataCon
......@@ -1472,11 +1473,24 @@ mkNewTypeEqn orig dflags tvs
-- currently generate type 'instance' decls; and cannot do
-- so for 'data' instance decls
roles_ok = let cls_roles = tyConRoles (classTyCon cls) in
not (null cls_roles) && last cls_roles /= Nominal
-- We must make sure that the class definition (and all its
-- members) never pattern-match on the last parameter.
-- See Trac #1496 and Note [Roles] in Coercion
-- We must make sure that all of the class's members
-- never pattern-match on the last parameter.
-- See Trac #1496 and Note [Roles] in Coercion.
-- Also see Note [Role checking in GND]
roles_ok = null role_errs
role_errs
= [ (id, substed_ty, is_specialized)
| id <- classMethods cls
, let ty = idType id
(_, [cls_constraint], meth_ty) = tcSplitSigmaTy ty
(_cls_tc, cls_args) = splitTyConApp cls_constraint
ordered_tvs = map (getTyVar "mkNewTypeEqn") cls_args
Just (other_tvs, gnd_tv) = snocView ordered_tvs
subst = zipOpenTvSubst other_tvs cls_tys
substed_ty = substTy subst meth_ty
is_specialized = not (meth_ty `eqType` substed_ty)
, ASSERT( _cls_tc == classTyCon cls )
tvUsedAtNominalRole gnd_tv substed_ty ]
cant_derive_err
= vcat [ ppUnless arity_ok arity_msg
......@@ -1488,9 +1502,15 @@ mkNewTypeEqn orig dflags tvs
ats_msg = ptext (sLit "the class has associated types")
roles_msg = ptext (sLit "it is not type-safe to use") <+>
ptext (sLit "GeneralizedNewtypeDeriving on this class;") $$
ptext (sLit "the last parameter of") <+>
quotes (ppr (className cls)) <+>
ptext (sLit "is at role Nominal")
vcat [ quotes (ppr id) <> comma <+>
specialized_doc <+>
quotes (ppr ty) <> comma <+>
text "cannot be converted safely"
| (id, ty, is_specialized) <- role_errs
, let specialized_doc
| is_specialized = text "specialized to type"
| otherwise = text "at type"
]
\end{code}
......@@ -1509,6 +1529,34 @@ minded way of generating the instance decl:
instance Eq [A] => Eq A -- Makes typechecker loop!
But now we require a simple context, so it's ok.
Note [Role checking in GND]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking to see if GND (GeneralizedNewtypeDeriving) is possible, we
do *not* look at the roles of the class being derived. Instead, we look
at the uses of the last type variable to that class in all the methods of
the class. (Why? Keep reading.) For example:
class Foo a b where
meth :: a b -> b
instance Foo Maybe Int where
meth = fromJust
newtype Age = MkAge Int
deriving (Foo Maybe)
According to the role rules, the `b` parameter to Foo must be at nominal
role -- after all, `a` could be a GADT. BUT, when deriving (Foo Maybe)
for Age, we in fact know that `a` is *not* a GADT. So, instead of looking
holistically at the roles for the parameters of Foo, we instead perform
the substitution on the type variables that we know (in this case,
[a |-> Maybe]) and then check each method individually.
Why check only methods, and not other things? In GND, superclass constraints
must be satisfied by the *newtype*, not the *base type*. So, we don't coerce
the base type's superclass dictionaries in GND, and we don't need to check
them here. For associated types, GND is impossible anyway, so we don't need
to look. All that is left is methods.
%************************************************************************
%* *
......
......@@ -32,7 +32,7 @@ module Coercion (
mkUnbranchedAxInstRHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkNthCo, mkNthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
mkInstCo, mkAppCo, mkAppCoFlexible, mkTyConAppCo, mkFunCo,
mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
mkNewTypeCo, maybeSubCo, maybeSubCo2,
mkAxiomRuleCo,
......@@ -45,6 +45,7 @@ module Coercion (
splitAppCo_maybe,
splitForAllCo_maybe,
nthRole, tyConRolesX,
tvUsedAtNominalRole, nextRole,
-- ** Coercion variables
mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
......@@ -894,26 +895,35 @@ mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
-- The second coercion must be Nominal, unless the first is Phantom.
-- If the first is Phantom, then the second can be either Phantom or Nominal.
mkAppCo :: Coercion -> Coercion -> Coercion
mkAppCo (Refl r ty1) (Refl _ ty2)
mkAppCo co1 co2 = mkAppCoFlexible co1 Nominal co2
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
-- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
-- | Apply a 'Coercion' to another 'Coercion'.
-- The second 'Coercion's role is given, making this more flexible than
-- 'mkAppCo'.
mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
mkAppCoFlexible (Refl r ty1) _ (Refl _ ty2)
= Refl r (mkAppTy ty1 ty2)
mkAppCo (Refl r (TyConApp tc tys)) co2
mkAppCoFlexible (Refl r (TyConApp tc tys)) r2 co2
= TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
where
zip_roles (r1:_) [] = [applyRole r1 co2]
zip_roles (r1:_) [] = [maybeSubCo2 r1 r2 co2]
zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
zip_roles _ _ = panic "zip_roles" -- but the roles are infinite...
mkAppCo (TyConAppCo r tc cos) co
mkAppCoFlexible (TyConAppCo r tc cos) r2 co
= case r of
Nominal -> TyConAppCo Nominal tc (cos ++ [co])
Nominal -> ASSERT( r2 == Nominal )
TyConAppCo Nominal tc (cos ++ [co])
Representational -> TyConAppCo Representational tc (cos ++ [co'])
where new_role = (tyConRolesX Representational tc) !! (length cos)
co' = applyRole new_role co
co' = maybeSubCo2 new_role r2 co
Phantom -> TyConAppCo Phantom tc (cos ++ [mkPhantomCo co])
mkAppCo co1 co2 = AppCo co1 co2
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
-- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
mkAppCoFlexible co1 _r2 co2 = ASSERT( _r2 == Nominal )
AppCo co1 co2
-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCo'.
......@@ -1100,6 +1110,31 @@ ltRole Representational _ = False
ltRole Nominal Nominal = False
ltRole Nominal _ = True
-- Is the given tyvar used in a nominal position anywhere?
-- This is used in the GeneralizedNewtypeDeriving check.
tvUsedAtNominalRole :: TyVar -> Type -> Bool
tvUsedAtNominalRole tv typ = let result = go Representational typ in
pprTrace "RAE1" (vcat [ppr tv, ppr typ]) $
pprTrace "RAE2" (ppr result) $
result
where go r (TyVarTy tv')
| tv == tv' = (r == Nominal)
| otherwise = False
go r (AppTy t1 t2) = go r t1 || go Nominal t2
go r (TyConApp tc args) = or $ zipWith go (tyConRolesX r tc) args
go r (FunTy t1 t2) = go r t1 || go r t2
go r (ForAllTy qtv ty)
| tv == qtv = False -- shadowed
| otherwise = go r ty
go _ (LitTy _) = False
-- if we wish to apply `co` to some other coercion, what would be its best
-- role?
nextRole :: Coercion -> Role
nextRole (Refl r (TyConApp tc tys)) = head $ dropList tys (tyConRolesX r tc)
nextRole (TyConAppCo r tc cos) = head $ dropList cos (tyConRolesX r tc)
nextRole _ = Nominal
-- See note [Newtype coercions] in TyCon
-- | Create a coercion constructor (axiom) suitable for the given
......
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