diff options
| -rw-r--r-- | compiler/deSugar/DsBinds.lhs | 13 | ||||
| -rw-r--r-- | compiler/typecheck/TcDeriv.lhs | 64 | ||||
| -rw-r--r-- | compiler/types/Coercion.lhs | 57 |
3 files changed, 112 insertions, 22 deletions
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs index a33ff9126c..1e828f8a20 100644 --- a/compiler/deSugar/DsBinds.lhs +++ b/compiler/deSugar/DsBinds.lhs @@ -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 diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index 349585e4a9..84da598581 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -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. %************************************************************************ %* * diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 251ab65cf1..90ffab7a77 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -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 |