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.

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