Roleify TcCoercion

Previously, TcCoercion were only used to represent boxed Nominal
coercions. In order to also talk about boxed Representational coercions
in the type checker, we add Roles to TcCoercion. Again, we closely
mirror Coercion.

The roles are verified by a few assertions, and at the latest after
conversion to Coercion. I have put my trust in the comprehensiveness of
the testsuite here, but any role error after desugaring popping up now
might be caused by this refactoring.

20 files changed, 307 insertions, 221 deletions

diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs
index 068dd6bd4b..aa027b094f 100644
--- a/compiler/coreSyn/MkCore.lhs
+++ b/compiler/coreSyn/MkCore.lhs
@@ -25,11 +25,8 @@ module MkCore (
         -- * Floats
         FloatBind(..), wrapFloat,
 
-        -- * Constructing/deconstructing equality evidence boxes
+        -- * Constructing equality evidence boxes
         mkEqBox,
-        
-        -- * Constructing Coercible evidence
-        mkCoercible,
 
         -- * Constructing general big tuples
         -- $big_tuples
@@ -302,17 +299,17 @@ mkStringExprFS str
 
 \begin{code}
 
+-- This take a ~# b (or a ~# R b) and returns a ~ b (or Coercible a b)
 mkEqBox :: Coercion -> CoreExpr
 mkEqBox co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
-             Var (dataConWorkId eqBoxDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
-  where Pair ty1 ty2 = coercionKind co
-        k = typeKind ty1
-
-mkCoercible :: Coercion -> CoreExpr
-mkCoercible co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
-             Var (dataConWorkId coercibleDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
+             Var (dataConWorkId datacon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
   where Pair ty1 ty2 = coercionKind co
         k = typeKind ty1
+        datacon = case coercionRole co of 
+            Nominal ->          eqBoxDataCon
+            Representational -> coercibleDataCon
+            Phantom ->          pprPanic "mkEqBox does not support boxing phantom coercions"
+                                         (ppr co)
 \end{code}
 
 %************************************************************************
diff --git a/compiler/deSugar/DsArrows.lhs b/compiler/deSugar/DsArrows.lhs
index 3b9c0e1552..763106f2b3 100644
--- a/compiler/deSugar/DsArrows.lhs
+++ b/compiler/deSugar/DsArrows.lhs
@@ -626,7 +626,7 @@ dsCmd _ids local_vars _stack_ty _res_ty (HsCmdArrForm op _ args) env_ids = do
 
 dsCmd ids local_vars stack_ty res_ty (HsCmdCast coercion cmd) env_ids = do
     (core_cmd, env_ids') <- dsCmd ids local_vars stack_ty res_ty cmd env_ids
-    wrapped_cmd <- dsHsWrapper (WpCast coercion) core_cmd
+    wrapped_cmd <- dsHsWrapper (mkWpCast coercion) core_cmd
     return (wrapped_cmd, env_ids')
 
 dsCmd _ _ _ _ _ c = pprPanic "dsCmd" (ppr c)
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 2fccba1aee..85b1cc6e4d 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -66,7 +66,6 @@ import Maybes
 import OrdList
 import Bag
 import BasicTypes hiding ( TopLevel )
-import Pair
 import DynFlags
 import FastString
 import ErrUtils( MsgDoc )
@@ -707,7 +706,8 @@ dsHsWrapper (WpTyApp ty)      e = return $ App e (Type ty)
 dsHsWrapper (WpLet ev_binds)  e = do bs <- dsTcEvBinds ev_binds
                                      return (mkCoreLets bs e)
 dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 =<< dsHsWrapper c2 e
-dsHsWrapper (WpCast co)       e = dsTcCoercion Representational co (mkCast e) 
+dsHsWrapper (WpCast co)       e = ASSERT (tcCoercionRole co == Representational)
+                                  dsTcCoercion co (mkCast e)
 dsHsWrapper (WpEvLam ev)      e = return $ Lam ev e 
 dsHsWrapper (WpTyLam tv)      e = return $ Lam tv e 
 dsHsWrapper (WpEvApp evtrm)   e = liftM (App e) (dsEvTerm evtrm)
@@ -741,7 +741,7 @@ dsEvTerm (EvId v) = return (Var v)
 
 dsEvTerm (EvCast tm co) 
   = do { tm' <- dsEvTerm tm
-       ; dsTcCoercion Representational co $ mkCast tm' }
+       ; dsTcCoercion co $ (mkCast tm' . mkSubCo) }
                         -- 'v' is always a lifted evidence variable so it is
                         -- unnecessary to call varToCoreExpr v here.
 
@@ -749,7 +749,7 @@ dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
                                      ; return (Var df `mkTyApps` tys `mkApps` tms') }
 
 dsEvTerm (EvCoercion (TcCoVarCo v)) = return (Var v)  -- See Note [Simple coercions]
-dsEvTerm (EvCoercion co)            = dsTcCoercion Nominal co mkEqBox
+dsEvTerm (EvCoercion co)            = dsTcCoercion co mkEqBox
 
 dsEvTerm (EvTupleSel v n)
    = do { tm' <- dsEvTerm v
@@ -788,12 +788,12 @@ dsEvTerm (EvLit l) =
 
 -- Note [Coercible Instances]
 dsEvTerm (EvCoercible (EvCoercibleRefl ty)) = do
-  return $ mkCoercible $ mkReflCo Representational ty
+  return $ mkEqBox $ mkReflCo Representational ty
 
 dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
   ntEvs <- mapM (mapEvCoercibleArgM dsEvTerm) evs
   wrapInEqRCases ntEvs $ \cos -> do
-    return $ mkCoercible $
+    return $ mkEqBox $
       mkTyConAppCo Representational tyCon cos
 
 dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
@@ -801,7 +801,7 @@ dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
   famenv <- dsGetFamInstEnvs
   let Just (_, ntCo) = instNewTyConTF_maybe famenv tyCon tys
   wrapInEqRCase ntEv $ \co -> do
-          return $ mkCoercible $ connect lor co ntCo
+          return $ mkEqBox $ connect lor co ntCo
   where connect CLeft co2 co1 = mkTransCo co1 co2
         connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
 
@@ -829,7 +829,7 @@ wrapInEqRCases (EvCoercibleArgP t1 t2:es) mkBody =
 wrapInEqRCases [] mkBody = mkBody []
 
 ---------------------------------------
-dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
+dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
 -- This is the crucial function that moves 
 -- from TcCoercions to Coercions; see Note [TcCoercions] in Coercion
 -- e.g.  dsTcCoercion (trans g1 g2) k
@@ -837,14 +837,14 @@ dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
 --         case g2 of EqBox g2# ->
 --         k (trans g1# g2#)
 -- thing_inside will get a coercion at the role requested
-dsTcCoercion role co thing_inside
+dsTcCoercion co thing_inside
   = do { 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) 
+             result_expr = thing_inside (ds_tc_coercion subst co)
              result_ty   = exprType result_expr
 
        ; return (foldr (wrap_in_case result_ty) result_expr eqvs_covs) }
@@ -855,46 +855,44 @@ dsTcCoercion role co thing_inside
          eq_nm = idName eqv
          occ = nameOccName eq_nm
          loc = nameSrcSpan eq_nm
-         ty  = mkCoercionType Nominal ty1 ty2
+         ty  = mkCoercionType (getEqPredRole (evVarPred eqv)) ty1 ty2
          (ty1, ty2) = getEqPredTys (evVarPred eqv)
 
-    wrap_in_case result_ty (eqv, cov) body 
-      = Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
+    wrap_in_case result_ty (eqv, cov) body
+      = case getEqPredRole (evVarPred eqv) of
+         Nominal          -> Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
+         Representational -> Case (Var eqv) eqv result_ty [(DataAlt coercibleDataCon, [cov], body)]
+         Phantom          -> panic "wrap_in_case/phantom"
 
-ds_tc_coercion :: CvSubst -> Role -> TcCoercion -> Coercion
--- If the incoming TcCoercion if of type (a ~ b), 
---                 the result is of type (a ~# b)
--- The VarEnv maps EqVars of type (a ~ b) to Coercions of type (a ~# b)
+ds_tc_coercion :: CvSubst -> TcCoercion -> Coercion
+-- If the incoming TcCoercion if of type (a ~ b)   (resp.  Coercible a b)
+--                 the result is of type (a ~# b)  (reps.  a ~# b)
+-- The VarEnv maps EqVars of type (a ~ b) to Coercions of type (a ~# b) (resp. and so on)
 -- No need for InScope set etc because the 
-ds_tc_coercion subst role tc_co
-  = go role tc_co
+ds_tc_coercion subst tc_co
+  = go tc_co
   where
-    go Phantom co
-      = mkUnivCo Phantom ty1 ty2
-      where Pair ty1 ty2 = tcCoercionKind 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)      = let leftCo    = go r co1
+    go (TcRefl r ty)            = Refl r (Coercion.substTy subst ty)
+    go (TcTyConAppCo r tc cos)  = mkTyConAppCo r tc (map go cos)
+    go (TcAppCo co1 co2)        = let leftCo    = go co1
                                       rightRole = nextRole leftCo in
-                                  mkAppCoFlexible leftCo rightRole (go rightRole co2)
-    go r (TcForAllCo tv co)     = mkForAllCo tv' (ds_tc_coercion subst' r co)
+                                  mkAppCoFlexible leftCo rightRole (go co2)
+    go (TcForAllCo tv co)       = mkForAllCo tv' (ds_tc_coercion subst' co)
                               where
                                 (subst', tv') = Coercion.substTyVarBndr subst tv
-    go r (TcAxiomInstCo ax ind tys)
-                                = mkAxInstCo r ax ind (map (Coercion.substTy subst) tys)
-    go r (TcSymCo co)           = mkSymCo (go r co)
-    go r (TcTransCo co1 co2)    = mkTransCo (go r co1) (go r co2)
-    go r (TcNthCo n co)         = mkNthCoRole r n (go r co) -- the 2nd r is a harmless lie
-    go r (TcLRCo lr co)         = maybeSubCo r $ mkLRCo lr (go Nominal co)
-    go r (TcInstCo co ty)       = mkInstCo (go r co) ty
-    go r (TcLetCo bs co)        = ds_tc_coercion (ds_co_binds bs) r co
-    go r (TcCastCo co1 co2)     = maybeSubCo r $ mkCoCast (go Nominal co1)
-                                                          (go Nominal co2)
-    go r (TcCoVarCo v)          = maybeSubCo r $ ds_ev_id subst v
-    go _ (TcAxiomRuleCo co ts cs) = AxiomRuleCo co
-                                      (map (Coercion.substTy subst) ts)
-                                      (map (go Nominal) cs)
+    go (TcAxiomInstCo ax ind cos)
+                                = AxiomInstCo ax ind (map go cos)
+    go (TcPhantomCo ty1 ty2)    = UnivCo Phantom ty1 ty2
+    go (TcSymCo co)             = mkSymCo (go co)
+    go (TcTransCo co1 co2)      = mkTransCo (go co1) (go co2)
+    go (TcNthCo n co)           = mkNthCo n (go co)
+    go (TcLRCo lr co)           = mkLRCo lr (go co)
+    go (TcInstCo co ty)         = mkInstCo (go co) ty
+    go (TcSubCo co)             = mkSubCo (go co)
+    go (TcLetCo bs co)          = ds_tc_coercion (ds_co_binds bs) co
+    go (TcCastCo co1 co2)       = mkCoCast (go co1) (go co2)
+    go (TcCoVarCo v)            = ds_ev_id subst v
+    go (TcAxiomRuleCo co ts cs) = AxiomRuleCo co (map (Coercion.substTy subst) ts) (map go cs)
 
 
 
@@ -908,9 +906,9 @@ ds_tc_coercion subst role tc_co
     ds_scc _ (CyclicSCC other) = pprPanic "ds_scc:cyclic" (ppr other $$ ppr tc_co)
 
     ds_co_term :: CvSubst -> EvTerm -> Coercion
-    ds_co_term subst (EvCoercion tc_co) = ds_tc_coercion subst Nominal tc_co
+    ds_co_term subst (EvCoercion tc_co) = ds_tc_coercion subst tc_co
     ds_co_term subst (EvId v)           = ds_ev_id subst v
-    ds_co_term subst (EvCast tm co)     = mkCoCast (ds_co_term subst tm) (ds_tc_coercion subst Nominal co)
+    ds_co_term subst (EvCast tm co)     = mkCoCast (ds_co_term subst tm) (ds_tc_coercion subst co)
     ds_co_term _ other = pprPanic "ds_co_term" (ppr other $$ ppr tc_co)
 
     ds_ev_id :: CvSubst -> EqVar -> Coercion
diff --git a/compiler/deSugar/DsExpr.lhs b/compiler/deSugar/DsExpr.lhs
index 2c8c490531..1fda49b567 100644
--- a/compiler/deSugar/DsExpr.lhs
+++ b/compiler/deSugar/DsExpr.lhs
@@ -32,6 +32,7 @@ import HsSyn
 -- NB: The desugarer, which straddles the source and Core worlds, sometimes
 --     needs to see source types
 import TcType
+import Coercion ( Role(..) )
 import TcEvidence
 import TcRnMonad
 import Type
@@ -533,11 +534,11 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
 
                         -- Tediously wrap the application in a cast
                         -- Note [Update for GADTs]
-                 wrap_co = mkTcTyConAppCo tycon
+                 wrap_co = mkTcTyConAppCo Nominal tycon
                                 [ lookup tv ty | (tv,ty) <- univ_tvs `zip` out_inst_tys ]
                  lookup univ_tv ty = case lookupVarEnv wrap_subst univ_tv of
                                         Just co' -> co'
-                                        Nothing  -> mkTcReflCo ty
+                                        Nothing  -> mkTcReflCo Nominal ty
                  wrap_subst = mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var))
                                        | ((tv,_),eq_var) <- eq_spec `zip` eqs_vars ]
 
@@ -547,7 +548,7 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
                                          , pat_args = PrefixCon $ map nlVarPat arg_ids
                                          , pat_ty = in_ty }
            ; let wrapped_rhs | null eq_spec = rhs
-                             | otherwise    = mkLHsWrap (WpCast wrap_co) rhs
+                             | otherwise    = mkLHsWrap (mkWpCast (mkTcSubCo wrap_co)) rhs
            ; return (mkSimpleMatch [pat] wrapped_rhs) }
 
 \end{code}
diff --git a/compiler/deSugar/Match.lhs b/compiler/deSugar/Match.lhs
index 2aebe47847..7a905104a2 100644
--- a/compiler/deSugar/Match.lhs
+++ b/compiler/deSugar/Match.lhs
@@ -996,11 +996,11 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
 
     ---------
     eq_co :: TcCoercion -> TcCoercion -> Bool
-    -- Just some simple cases
-    eq_co (TcRefl t1)             (TcRefl t2)             = eqType t1 t2
-    eq_co (TcCoVarCo v1)          (TcCoVarCo v2)          = v1==v2
-    eq_co (TcSymCo co1)           (TcSymCo co2)           = co1 `eq_co` co2
-    eq_co (TcTyConAppCo tc1 cos1) (TcTyConAppCo tc2 cos2) = tc1==tc2 && eq_list eq_co cos1 cos2
+    -- Just some simple cases (should the r1 == r2 rather be an ASSERT?)
+    eq_co (TcRefl r1 t1)             (TcRefl r2 t2)             = r1 == r2 && eqType t1 t2
+    eq_co (TcCoVarCo v1)             (TcCoVarCo v2)             = v1==v2
+    eq_co (TcSymCo co1)              (TcSymCo co2)              = co1 `eq_co` co2
+    eq_co (TcTyConAppCo r1 tc1 cos1) (TcTyConAppCo r2 tc2 cos2) = r1 == r2 && tc1==tc2 && eq_list eq_co cos1 cos2
     eq_co _ _ = False
 
 patGroup :: DynFlags -> Pat Id -> PatGroup
diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs
index 7fc354bac9..a27197161f 100644
--- a/compiler/hsSyn/HsUtils.lhs
+++ b/compiler/hsSyn/HsUtils.lhs
@@ -440,12 +440,10 @@ mkHsWrap co_fn e | isIdHsWrapper co_fn = e
 		 | otherwise	       = HsWrap co_fn e
 
 mkHsWrapCo :: TcCoercion -> HsExpr id -> HsExpr id
-mkHsWrapCo co e | isTcReflCo co = e
-                | otherwise     = mkHsWrap (WpCast co) e
+mkHsWrapCo co e = mkHsWrap (coToHsWrapper co) e
 
 mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id
-mkLHsWrapCo co (L loc e) | isTcReflCo co = L loc e
-                         | otherwise     = L loc (mkHsWrap (WpCast co) e)
+mkLHsWrapCo co (L loc e) = L loc (mkHsWrapCo co e)
 
 mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id
 mkHsCmdCast co cmd | isTcReflCo co = cmd
@@ -453,7 +451,7 @@ mkHsCmdCast co cmd | isTcReflCo co = cmd
 
 coToHsWrapper :: TcCoercion -> HsWrapper
 coToHsWrapper co | isTcReflCo co = idHsWrapper
-                 | otherwise     = WpCast co
+                 | otherwise     = mkWpCast (mkTcSubCo co)
 
 mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
 mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
@@ -461,7 +459,7 @@ mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
 
 mkHsWrapPatCo :: TcCoercion -> Pat id -> Type -> Pat id
 mkHsWrapPatCo co pat ty | isTcReflCo co = pat
-                        | otherwise     = CoPat (WpCast co) pat ty
+                        | otherwise     = CoPat (mkWpCast co) pat ty
 
 mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
 mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index e26d921953..5019426c88 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -48,6 +48,7 @@ import InstEnv
 import FunDeps
 import TcMType
 import Type
+import Coercion ( Role(..) )
 import TcType
 import Class
 import Unify
@@ -222,7 +223,7 @@ instCallConstraints orig preds
        ; return (mkWpEvApps evs) }
   where
     go pred 
-     | Just (ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
+     | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
      = do  { co <- unifyType ty1 ty2
            ; return (EvCoercion co) }
      | otherwise
diff --git a/compiler/typecheck/TcArrows.lhs b/compiler/typecheck/TcArrows.lhs
index f5309006b6..48dec60520 100644
--- a/compiler/typecheck/TcArrows.lhs
+++ b/compiler/typecheck/TcArrows.lhs
@@ -30,6 +30,7 @@ import TcEvidence
 import Id( mkLocalId )
 import Inst
 import Name
+import Coercion ( Role(..) )
 import TysWiredIn
 import VarSet 
 import TysPrim
@@ -93,7 +94,7 @@ tcProc pat cmd exp_ty
 	; let cmd_env = CmdEnv { cmd_arr = arr_ty }
         ; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
 			  tcCmdTop cmd_env cmd (unitTy, res_ty)
-        ; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo res_ty))
+        ; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo Nominal res_ty))
         ; return (pat', cmd', res_co) }
 \end{code}
 
@@ -323,11 +324,11 @@ tc_cmd _ cmd _
 
 matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercion, [TcType], TcType)
 matchExpectedCmdArgs 0 ty 
-  = return (mkTcReflCo ty, [], ty)
+  = return (mkTcReflCo Nominal ty, [], ty)
 matchExpectedCmdArgs n ty
   = do { (co1, [ty1, ty2]) <- matchExpectedTyConApp pairTyCon ty  
        ; (co2, tys, res_ty) <- matchExpectedCmdArgs (n-1) ty2
-       ; return (mkTcTyConAppCo pairTyCon [co1, co2], ty1:tys, res_ty) }
+       ; return (mkTcTyConAppCo Nominal pairTyCon [co1, co2], ty1:tys, res_ty) }
 \end{code}
 
 
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index f23527b5ff..b3b1a3f5c3 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -243,7 +243,7 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
     -- co : t -> IP "x" t
     toDict ipClass x ty =
       case unwrapNewTyCon_maybe (classTyCon ipClass) of
-        Just (_,_,ax) -> HsWrap $ WpCast $ mkTcSymCo $ mkTcUnbranchedAxInstCo ax [x,ty]
+        Just (_,_,ax) -> HsWrap $ mkWpCast $ mkTcSymCo $ mkTcUnbranchedAxInstCo Representational ax [x,ty]
         Nothing       -> panic "The dictionary for `IP` is not a newtype?"
 
 
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 3c81c34c53..5b594b851f 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -235,7 +235,7 @@ canClassNC ev cls tys
 
 canClass ev cls tys
   = do { (xis, cos) <- flattenMany FMFullFlatten ev tys
-       ; let co = mkTcTyConAppCo (classTyCon cls) cos
+       ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
              xi = mkClassPred cls xis
        ; mb <- rewriteCtFlavor ev xi co
        ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
@@ -491,7 +491,7 @@ flatten f ctxt ty
        ; if eqType xi ty then return (ty,co) else return (xi,co) }
        -- Small tweak for better error messages
 
-flatten _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
+flatten _ _ xi@(LitTy {}) = return (xi, mkTcReflCo Nominal xi)
 
 flatten f ctxt (TyVarTy tv)
   = flattenTyVar f ctxt tv
@@ -504,14 +504,14 @@ flatten f ctxt (AppTy ty1 ty2)
 flatten f ctxt (FunTy ty1 ty2)
   = do { (xi1,co1) <- flatten f ctxt ty1
        ; (xi2,co2) <- flatten f ctxt ty2
-       ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
+       ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
 
 flatten f ctxt (TyConApp tc tys)
   -- For a normal type constructor or data family application, we just
   -- recursively flatten the arguments.
   | not (isSynFamilyTyCon tc)
     = do { (xis,cos) <- flattenMany f ctxt tys
-         ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
+         ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
 
   -- Otherwise, it's a type function application, and we have to
   -- flatten it away as well, and generate a new given equality constraint
@@ -529,7 +529,7 @@ flatten f ctxt (TyConApp tc tys)
          ; (ret_co, rhs_xi) <-
              case f of
                FMSubstOnly ->
-                 return (mkTcReflCo fam_ty, fam_ty)
+                 return (mkTcReflCo Nominal fam_ty, fam_ty)
                FMFullFlatten ->
                  do { mb_ct <- lookupFlatEqn tc xi_args
                     ; case mb_ct of
@@ -561,7 +561,7 @@ flatten f ctxt (TyConApp tc tys)
                   -- Emit the flat constraints
          ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
                                             --    cf Trac #5655
-                  , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args) $
+                  , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo Nominal tc cos_args) $
                     cos_rest
                   )
          }
@@ -651,7 +651,7 @@ flattenFinalTyVar f ctxt tv
     do { let knd = tyVarKind tv
        ; (new_knd, _kind_co) <- flatten f ctxt knd
        ; let ty = mkTyVarTy (setVarType tv new_knd)
-       ; return (ty, mkTcReflCo ty) }
+       ; return (ty, mkTcReflCo Nominal ty) }
 \end{code}
 
 Note [Non-idempotent inert substitution]
@@ -712,7 +712,7 @@ canEqNC ev ty1 ty2
   | tcEqType ty1 ty2      -- Dealing with equality here avoids
                           -- later spurious occurs checks for a~a
   = if isWanted ev then
-      setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop
+      setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo Nominal ty1)) >> return Stop
     else
       return Stop
 
@@ -781,7 +781,8 @@ canEqNC ev ty1 ty2
       = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
                  xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
                  xevdecomp x = let xco = evTermCoercion x
-                               in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
+                               in [ EvCoercion (mkTcLRCo CLeft xco)
+                                  , EvCoercion (mkTcLRCo CRight xco)]
            ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
            ; canEvVarsCreated ctevs }
 
@@ -799,7 +800,7 @@ canDecomposableTyConApp ev tc1 tys1 tc2 tys2
     -- Fail straight away for better error messages
   = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
   | otherwise
-  = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
+  = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
              xev = XEvTerm xcomp xdecomp
        ; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
@@ -1085,7 +1086,7 @@ canEqLeafFun ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
           -- Fancy higher-dimensional coercion between equalities!
           -- SPJ asks why?  Why not just co : F xis1 ~ F tys1?
        ; let fam_head = mkTyConApp fn xis1
-             xco = mkHdEqPred ty2 (mkTcTyConAppCo fn cos1) co2
+             xco = mkHdEqPred ty2 (mkTcTyConAppCo Nominal fn cos1) co2
              -- xco :: (F xis1 ~ xi2) ~ (F tys1 ~ ty2)
 
        ; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
@@ -1117,7 +1118,8 @@ canEqLeafTyVar ev tv s2              -- ev :: tv ~ s2
 
            (Just tv1, Just tv2) | tv1 == tv2
               -> do { when (isWanted ev) $
-                      setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo xi1)) co)
+                      ASSERT ( tcCoercionRole co == Nominal )
+                      setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo Nominal xi1)) co)
                     ; return Stop }
 
            (Just tv1, _) -> do { dflags <- getDynFlags
@@ -1188,7 +1190,7 @@ mkHdEqPred :: Type -> TcCoercion -> TcCoercion -> TcCoercion
 -- Make a higher-dimensional equality
 --    co1 :: s1~t1,  co2 :: s2~t2
 -- Then (mkHdEqPred t2 co1 co2) :: (s1~s2) ~ (t1~t2)
-mkHdEqPred t2 co1 co2 = mkTcTyConAppCo eqTyCon [mkTcReflCo (defaultKind (typeKind t2)), co1, co2]
+mkHdEqPred t2 co1 co2 = mkTcTyConAppCo Nominal eqTyCon [mkTcReflCo Nominal (defaultKind (typeKind t2)), co1, co2]
    -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I truly hate this (DV)
 \end{code}
 
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 6551d81bcb..ea0c3b59d7 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -7,7 +7,7 @@ module TcEvidence (
 
   -- HsWrapper
   HsWrapper(..), 
-  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, 
+  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast,
   idHsWrapper, isIdHsWrapper, pprHsWrapper,
 
   -- Evidence bindings
@@ -22,20 +22,21 @@ module TcEvidence (
   TcCoercion(..), LeftOrRight(..), pickLR,
   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
   mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, 
-  mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
+  mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos, mkTcSubCo,
   mkTcAxiomRuleCo,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
-  isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe
+  isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
+  tcCoercionRole, eqVarRole
 
   ) where
 #include "HsVersions.h"
 
 import Var
-import Coercion( LeftOrRight(..), pickLR )
+import Coercion( LeftOrRight(..), pickLR, nthRole )
 import PprCore ()   -- Instance OutputableBndr TyVar
 import TypeRep  -- Knows type representation
 import TcType
-import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys, coAxNthLHS )
+import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys, getEqPredRole, coAxNthLHS )
 import TysPrim( funTyCon )
 import TyCon
 import CoAxiom
@@ -68,8 +69,8 @@ boxed type (a ~ b). After we are done with typechecking the
 desugarer finds the free variables, unboxes them, and creates a
 resulting real Coercion with kosher free variables.
 
-We can use most of the Coercion "smart constructors" to build TcCoercions. However,
-mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
+We can use most of the Coercion "smart constructors" to build TcCoercions.
+However, mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
 
 The data type is similar to Coercion.Coercion, with the following
 differences
@@ -77,42 +78,36 @@ differences
     This is what lets us unify two for-all types and generate
     equality constraints underneath
 
-  * The kind of a TcCoercion is  t1 ~  t2 
-             of a Coercion   is  t1 ~# t2
+  * The kind of a TcCoercion is  t1 ~  t2  (resp. Coercible t1 t2)
+             of a Coercion   is  t1 ~# t2  (resp. t1 ~#R t2)
 
-  * TcCoercions are essentially all at role Nominal -- the type-checker
-    reasons only about nominal equality, not representational.
-    --> Exception: there can be newtype axioms wrapped up in TcCoercions.
-                   These, of course, are only used in casts, so the desugarer
-                   will still produce the right 'Coercion's.
-
-  * TcAxiomInstCo takes Types, not Coercions as arguments;
-    the generality is required only in the Simplifier
-
-  * UnsafeCo aren't required
+  * UnsafeCo aren't required, but we do have TcPhandomCo
 
   * Representation invariants are weaker:
      - we are allowed to have type synonyms in TcTyConAppCo
      - the first arg of a TcAppCo can be a TcTyConAppCo
+     - TcSubCo is not applied as deep as done with mkSubCo
     Reason: they'll get established when we desugar to Coercion
 
 \begin{code}
 data TcCoercion 
-  = TcRefl TcType
-  | TcTyConAppCo TyCon [TcCoercion]
+  = TcRefl Role TcType
+  | TcTyConAppCo Role TyCon [TcCoercion]
   | TcAppCo TcCoercion TcCoercion
   | TcForAllCo TyVar TcCoercion 
   | TcInstCo TcCoercion TcType
-  | TcCoVarCo EqVar               -- variable always at role N
-  | TcAxiomInstCo (CoAxiom Branched) Int [TcType] -- Int specifies branch number
-                                                  -- See [CoAxiom Index] in Coercion.lhs
-  -- This is number of types and coercions are expected to macth to CoAxiomRule
+  | TcCoVarCo EqVar
+  | TcAxiomInstCo (CoAxiom Branched) Int [TcCoercion] -- Int specifies branch number
+                                                      -- See [CoAxiom Index] in Coercion.lhs
+  -- This is number of types and coercions are expected to match to CoAxiomRule
   -- (i.e., the CoAxiomRules are always fully saturated)
   | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
+  | TcPhantomCo TcType TcType
   | TcSymCo TcCoercion
   | TcTransCo TcCoercion TcCoercion
   | TcNthCo Int TcCoercion
   | TcLRCo LeftOrRight TcCoercion
+  | TcSubCo TcCoercion
   | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
   | TcLetCo TcEvBinds TcCoercion
   deriving (Data.Data, Data.Typeable)
@@ -124,8 +119,8 @@ isEqVar v = case tyConAppTyCon_maybe (varType v) of
                Nothing -> False
 
 isTcReflCo_maybe :: TcCoercion -> Maybe TcType
-isTcReflCo_maybe (TcRefl ty) = Just ty
-isTcReflCo_maybe _           = Nothing
+isTcReflCo_maybe (TcRefl _ ty) = Just ty
+isTcReflCo_maybe _             = Nothing
 
 isTcReflCo :: TcCoercion -> Bool
 isTcReflCo (TcRefl {}) = True
@@ -135,41 +130,71 @@ getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
 getTcCoVar_maybe (TcCoVarCo v) = Just v
 getTcCoVar_maybe _             = Nothing
 
-mkTcReflCo :: TcType -> TcCoercion
+mkTcReflCo :: Role -> TcType -> TcCoercion
 mkTcReflCo = TcRefl
 
-mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
-mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
+mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
+mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
 
-mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
-mkTcTyConAppCo tc cos   -- No need to expand type synonyms
-                        -- See Note [TcCoercions]
+mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
+mkTcTyConAppCo role tc cos -- No need to expand type synonyms
+                           -- See Note [TcCoercions]
   | Just tys <- traverse isTcReflCo_maybe cos 
-  = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]
-
-  | otherwise = TcTyConAppCo tc cos
-
-mkTcAxInstCo :: CoAxiom br -> Int -> [TcType] -> TcCoercion
-mkTcAxInstCo ax ind tys
-  | arity == n_tys = TcAxiomInstCo ax_br ind tys
+  = TcRefl role (mkTyConApp tc tys)  -- See Note [Refl invariant]
+
+  | otherwise = TcTyConAppCo role tc cos
+
+-- input coercion is Nominal
+-- mkSubCo will do some normalisation. We do not do it for TcCoercions, but
+-- defer that to desugaring; just to reduce the code duplication a little bit
+mkTcSubCo :: TcCoercion -> TcCoercion
+mkTcSubCo co = ASSERT2 ( tcCoercionRole co == Nominal, ppr co)
+               TcSubCo co
+
+maybeTcSubCo2_maybe :: Role   -- desired role
+                    -> Role   -- current role
+                    -> TcCoercion -> Maybe TcCoercion
+maybeTcSubCo2_maybe Representational Nominal = Just . mkTcSubCo
+maybeTcSubCo2_maybe Nominal Representational = const Nothing
+maybeTcSubCo2_maybe Phantom _                = panic "maybeTcSubCo2_maybe Phantom" -- not supported (not needed at the moment)
+maybeTcSubCo2_maybe _ Phantom                = const Nothing
+maybeTcSubCo2_maybe _ _                      = Just
+
+maybeTcSubCo2 :: Role  -- desired role
+              -> Role  -- current role
+              -> TcCoercion -> TcCoercion
+maybeTcSubCo2 r1 r2 co
+  = case maybeTcSubCo2_maybe r1 r2 co of
+      Just co' -> co'
+      Nothing  -> pprPanic "maybeTcSubCo2" (ppr r1 <+> ppr r2 <+> ppr co)
+
+mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion
+mkTcAxInstCo role ax index tys
+  | ASSERT2 ( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) )
+    arity == n_tys = maybeTcSubCo2 role ax_role $ TcAxiomInstCo ax_br index rtys
   | otherwise      = ASSERT( arity < n_tys )
-                     foldl TcAppCo (TcAxiomInstCo ax_br ind (take arity tys))
-                                   (map TcRefl (drop arity tys))
+                     maybeTcSubCo2 role ax_role $ 
+                     foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys))
+                                   (drop arity rtys)
   where
-    n_tys = length tys
-    arity = coAxiomArity ax ind
-    ax_br = toBranchedAxiom ax
+    n_tys     = length tys
+    ax_br     = toBranchedAxiom ax
+    branch    = coAxiomNthBranch ax_br index
+    arity     = length $ coAxBranchTyVars branch
+    ax_role   = coAxiomRole ax
+    arg_roles = coAxBranchRoles branch
+    rtys      = zipWith mkTcReflCo (arg_roles ++ repeat Nominal) tys
 
 mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
 mkTcAxiomRuleCo = TcAxiomRuleCo
 
-mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> TcCoercion
-mkTcUnbranchedAxInstCo ax tys
-  = mkTcAxInstCo ax 0 tys
+mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion
+mkTcUnbranchedAxInstCo role ax tys
+  = mkTcAxInstCo role ax 0 tys
 
 mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
 -- No need to deal with TyConApp on the left; see Note [TcCoercions]
-mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)
+mkTcAppCo (TcRefl r ty1) (TcRefl _ ty2) = TcRefl r (mkAppTy ty1 ty2)
 mkTcAppCo co1 co2                       = TcAppCo co1 co2
 
 mkTcSymCo :: TcCoercion -> TcCoercion
@@ -178,36 +203,36 @@ mkTcSymCo    (TcSymCo co) = co
 mkTcSymCo co              = TcSymCo co
 
 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
-mkTcTransCo (TcRefl _) co = co
-mkTcTransCo co (TcRefl _) = co
-mkTcTransCo co1 co2       = TcTransCo co1 co2
+mkTcTransCo (TcRefl {}) co = co
+mkTcTransCo co (TcRefl {}) = co
+mkTcTransCo co1 co2        = TcTransCo co1 co2
 
 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
-mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
-mkTcNthCo n co          = TcNthCo n co
+mkTcNthCo n (TcRefl r ty) = TcRefl r (tyConAppArgN n ty)
+mkTcNthCo n co            = TcNthCo n co
 
 mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
-mkTcLRCo lr (TcRefl ty) = TcRefl (pickLR lr (tcSplitAppTy ty))
-mkTcLRCo lr co          = TcLRCo lr co
+mkTcLRCo lr (TcRefl r ty) = TcRefl r (pickLR lr (tcSplitAppTy ty))
+mkTcLRCo lr co            = TcLRCo lr co
 
 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
 
 mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
-mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)
-mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co
+mkTcForAllCo tv (TcRefl r ty) = ASSERT( isTyVar tv ) TcRefl r (mkForAllTy tv ty)
+mkTcForAllCo tv  co           = ASSERT( isTyVar tv ) TcForAllCo tv co
 
 mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
-mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)
-mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
+mkTcForAllCos tvs (TcRefl r ty) = ASSERT( all isTyVar tvs ) TcRefl r (mkForAllTys tvs ty)
+mkTcForAllCos tvs co            = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
 
 mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion
-mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)
-mkTcInstCos co tys          = foldl TcInstCo co tys
+mkTcInstCos (TcRefl r ty) tys = TcRefl r (applyTys ty tys)
+mkTcInstCos co tys            = foldl TcInstCo co tys
 
 mkTcCoVarCo :: EqVar -> TcCoercion
--- ipv :: s ~ t  (the boxed equality type)
+-- ipv :: s ~ t  (the boxed equality type) or Coercible s t (the boxed representational equality type)
 mkTcCoVarCo ipv = TcCoVarCo ipv
   -- Previously I checked for (ty ~ ty) and generated Refl,
   -- but in fact ipv may not even (visibly) have a (t1 ~ t2) type, because
@@ -220,24 +245,28 @@ mkTcCoVarCo ipv = TcCoVarCo ipv
 tcCoercionKind :: TcCoercion -> Pair Type
 tcCoercionKind co = go co 
   where 
-    go (TcRefl ty)            = Pair ty ty
+    go (TcRefl _ ty)          = Pair ty ty
     go (TcLetCo _ co)         = go co
     go (TcCastCo _ co)        = case getEqPredTys (pSnd (go co)) of
                                    (ty1,ty2) -> Pair ty1 ty2
-    go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
+    go (TcTyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
     go (TcInstCo co ty)       = go_inst co [ty]
     go (TcCoVarCo cv)         = eqVarKind cv
-    go (TcAxiomInstCo ax ind tys)
+    go (TcAxiomInstCo ax ind cos)
       = let branch = coAxiomNthBranch ax ind
-            tvs    = coAxBranchTyVars branch
-        in Pair (substTyWith tvs tys (coAxNthLHS ax ind)) 
-                (substTyWith tvs tys (coAxBranchRHS branch))
+            tvs = coAxBranchTyVars branch
+            Pair tys1 tys2 = sequenceA (map go cos)
+        in ASSERT( cos `equalLength` tvs )
+           Pair (substTyWith tvs tys1 (coAxNthLHS ax ind))
+                (substTyWith tvs tys2 (coAxBranchRHS branch))
+    go (TcPhantomCo ty1 ty2)  = Pair ty1 ty2
     go (TcSymCo co)           = swap (go co)
     go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
     go (TcNthCo d co)         = tyConAppArgN d <$> go co
     go (TcLRCo lr co)         = (pickLR lr . tcSplitAppTy) <$> go co
+    go (TcSubCo co)           = go co
     go (TcAxiomRuleCo ax ts cs) =
        case coaxrProves ax ts (map tcCoercionKind cs) of
          Just res -> res
@@ -247,6 +276,9 @@ tcCoercionKind co = go co
     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
     go_inst co               tys = (`applyTys` tys) <$> go co
 
+eqVarRole :: EqVar -> Role
+eqVarRole cv = getEqPredRole (varType cv)
+
 eqVarKind :: EqVar -> Pair Type
 eqVarKind cv
  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
@@ -254,23 +286,48 @@ eqVarKind cv
    Pair ty1 ty2
  | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
 
+tcCoercionRole :: TcCoercion -> Role
+tcCoercionRole = go
+  where
+    go (TcRefl r _)           = r
+    go (TcTyConAppCo r _ _)   = r
+    go (TcAppCo co _)         = go co
+    go (TcForAllCo _ co)      = go co
+    go (TcCoVarCo cv)         = eqVarRole cv
+    go (TcAxiomInstCo ax _ _) = coAxiomRole ax
+    go (TcPhantomCo _ _)      = Phantom
+    go (TcSymCo co)           = go co
+    go (TcTransCo co1 _)      = go co1 -- same as go co2
+    go (TcNthCo n co)         = let Pair ty1 _ = tcCoercionKind co
+                                    (tc, _) = tcSplitTyConApp ty1
+                                in nthRole (go co) tc n
+    go (TcLRCo _ _)           = Nominal
+    go (TcInstCo co _)        = go co
+    go (TcSubCo _)            = Representational
+    go (TcAxiomRuleCo c _ _)  = coaxrRole c
+    go (TcCastCo c _)         = go c
+    go (TcLetCo _ c)          = go c
+
+
 coVarsOfTcCo :: TcCoercion -> VarSet
 -- Only works on *zonked* coercions, because of TcLetCo
 coVarsOfTcCo tc_co
   = go tc_co
   where
-    go (TcRefl _)                = emptyVarSet
-    go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos
+    go (TcRefl _ _)              = emptyVarSet
+    go (TcTyConAppCo _ _ cos)    = foldr (unionVarSet . go) emptyVarSet cos
     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
     go (TcCastCo co1 co2)        = go co1 `unionVarSet` go co2
     go (TcForAllCo _ co)         = go co
     go (TcInstCo co _)           = go co
     go (TcCoVarCo v)             = unitVarSet v
-    go (TcAxiomInstCo {})        = emptyVarSet
+    go (TcAxiomInstCo _ _ cos)   = foldr (unionVarSet . go) emptyVarSet cos
+    go (TcPhantomCo _ _)         = emptyVarSet
     go (TcSymCo co)              = go co
     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
     go (TcNthCo _ co)            = go co
     go (TcLRCo  _ co)            = go co
+    go (TcSubCo co)              = go co
     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
                                    `minusVarSet` get_bndrs bs
     go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
@@ -297,12 +354,12 @@ pprTcCo       co = ppr_co TopPrec   co
 pprParendTcCo co = ppr_co TyConPrec co
 
 ppr_co :: Prec -> TcCoercion -> SDoc
-ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)
+ppr_co _ (TcRefl r ty) = angleBrackets (ppr ty) <> ppr_role r
 
-ppr_co p co@(TcTyConAppCo tc [_,_])
+ppr_co p co@(TcTyConAppCo _ tc [_,_])
   | tc `hasKey` funTyConKey = ppr_fun_co p co
 
-ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
+ppr_co p (TcTyConAppCo r tc cos) = pprTcApp   p ppr_co tc cos <> ppr_role r
 ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
@@ -316,15 +373,17 @@ ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $
 ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
 
 ppr_co p (TcAxiomInstCo con ind cos)
-  = pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map (ppr_type TyConPrec) cos)
+  = pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map pprParendTcCo cos)
 
 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
                                ppr_co FunPrec co1
                                <+> ptext (sLit ";")
                                <+> ppr_co FunPrec co2
+ppr_co p (TcPhantomCo t1 t2)  = pprPrefixApp p (ptext (sLit "PhantomCo")) [pprParendType t1, pprParendType t2]
 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
 ppr_co p (TcLRCo lr co)       = pprPrefixApp p (ppr lr) [pprParendTcCo co]
+ppr_co p (TcSubCo co)         = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co]
 ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
                                   $ ppr_tc_axiom_rule_co co ts ps
 
@@ -342,14 +401,18 @@ ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps
                   vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
                   ptext (sLit ")")
 
-
-
+ppr_role :: Role -> SDoc
+ppr_role r = underscore <> pp_role
+  where pp_role = case r of
+                    Nominal          -> char 'N'
+                    Representational -> char 'R'
+                    Phantom          -> char 'P'
 
 ppr_fun_co :: Prec -> TcCoercion -> SDoc
 ppr_fun_co p co = pprArrowChain p (split co)
   where
     split :: TcCoercion -> [SDoc]
-    split (TcTyConAppCo f [arg,res])
+    split (TcTyConAppCo _ f [arg,res])
       | f `hasKey` funTyConKey
       = ppr_co FunPrec arg : split res
     split co = [ppr_co TopPrec co]
@@ -382,6 +445,7 @@ data HsWrapper
 
   | WpCast TcCoercion         -- A cast:  [] `cast` co
                               -- Guaranteed not the identity coercion
+                              -- At role Representational
 
         -- Evidence abstraction and application
         -- (both dictionaries and coercions)
@@ -403,6 +467,10 @@ WpHole <.> c = c
 c <.> WpHole = c
 c1 <.> c2    = c1 `WpCompose` c2
 
+mkWpCast :: TcCoercion -> HsWrapper
+mkWpCast co = ASSERT2 (tcCoercionRole co == Representational, ppr co)
+              WpCast co
+
 mkWpTyApps :: [Type] -> HsWrapper
 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
 
@@ -493,10 +561,10 @@ data EvBind = EvBind EvVar EvTerm
 data EvTerm
   = EvId EvId                    -- Any sort of evidence Id, including coercions
 
-  | EvCoercion TcCoercion        -- (Boxed) coercion bindings 
+  | EvCoercion TcCoercion        -- (Boxed) coercion bindings
                                  -- See Note [Coercion evidence terms]
 
-  | EvCast EvTerm TcCoercion     -- d |> co
+  | EvCast EvTerm TcCoercion     -- d |> co, the coerction being at role nominal
 
   | EvDFunApp DFunId             -- Dictionary instance application
        [Type] [EvTerm]
@@ -643,7 +711,8 @@ The story for kind `Symbol` is analogous:
 \begin{code}
 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
 mkEvCast ev lco
-  | isTcReflCo lco = ev
+  | ASSERT2 (tcCoercionRole lco == Nominal, (vcat [ptext (sLit "Coercion of wrong role passed to mkEvCast:"), ppr ev, ppr lco]))
+    isTcReflCo lco = ev
   | otherwise      = EvCast ev lco
 
 emptyTcEvBinds :: TcEvBinds
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index 2c462970bb..ccd11967d2 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -201,7 +201,7 @@ tcExpr (HsIPVar x) res_ty
   -- Coerces a dictionry for `IP "x" t` into `t`.
   fromDict ipClass x ty =
     case unwrapNewTyCon_maybe (classTyCon ipClass) of
-      Just (_,_,ax) -> HsWrap $ WpCast $ mkTcUnbranchedAxInstCo ax [x,ty]
+      Just (_,_,ax) -> HsWrap $ mkWpCast $ mkTcUnbranchedAxInstCo Representational ax [x,ty]
       Nothing       -> panic "The dictionary for `IP` is not a newtype?"
 
 tcExpr (HsLam match) res_ty
@@ -334,7 +334,7 @@ tcExpr (OpApp arg1 op fix arg2) res_ty
 
        ; let op' = L loc (HsWrap (mkWpTyApps [a_ty, b_ty]) (HsVar op_id))
        ; return $ mkHsWrapCo (co_res) $
-         OpApp (mkLHsWrapCo (mkTcFunCo co_a co_b) $
+         OpApp (mkLHsWrapCo (mkTcFunCo Nominal co_a co_b) $
                 mkLHsWrapCo co_arg1 arg1')
                op' fix
                (mkLHsWrapCo co_a arg2') }
@@ -720,7 +720,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
 
         -- Step 7: make a cast for the scrutinee, in the case that it's from a type family
         ; let scrut_co | Just co_con <- tyConFamilyCoercion_maybe tycon
-                       = WpCast (mkTcUnbranchedAxInstCo co_con scrut_inst_tys)
+                       = mkWpCast (mkTcUnbranchedAxInstCo Representational co_con scrut_inst_tys)
                        | otherwise
                        = idHsWrapper
         -- Phew!
@@ -1232,14 +1232,14 @@ tcTagToEnum loc fun_name arg res_ty
         -- and returns a coercion between the two
     get_rep_ty ty tc tc_args
       | not (isFamilyTyCon tc)
-      = return (mkTcReflCo ty, tc, tc_args)
+      = return (mkTcReflCo Nominal ty, tc, tc_args)
       | otherwise
       = do { mb_fam <- tcLookupFamInst tc tc_args
            ; case mb_fam of
                Nothing -> failWithTc (tagToEnumError ty doc3)
                Just (FamInstMatch { fim_instance = rep_fam
                                   , fim_tys      = rep_args })
-                   -> return ( mkTcSymCo (mkTcUnbranchedAxInstCo co_tc rep_args)
+                   -> return ( mkTcSymCo (mkTcUnbranchedAxInstCo Nominal co_tc rep_args)
                              , rep_tc, rep_args )
                  where
                    co_tc  = famInstAxiom rep_fam
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 8b136f56e2..1470e931c0 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -712,7 +712,7 @@ zonkCmd   :: ZonkEnv -> HsCmd TcId    -> TcM (HsCmd Id)
 zonkLCmd  env cmd  = wrapLocM (zonkCmd env) cmd
 
 zonkCmd env (HsCmdCast co cmd)
-  = do { co' <- zonkTcLCoToLCo env co
+  = do { co' <- zonkTcCoToCo env co
        ; cmd' <- zonkCmd env cmd
        ; return (HsCmdCast co' cmd') }
 zonkCmd env (HsCmdArrApp e1 e2 ty ho rl)
@@ -782,7 +782,7 @@ zonkCoFn env WpHole   = return (env, WpHole)
 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                     ; (env2, c2') <- zonkCoFn env1 c2
                                     ; return (env2, WpCompose c1' c2') }
-zonkCoFn env (WpCast co) = do { co' <- zonkTcLCoToLCo env co
+zonkCoFn env (WpCast co) = do { co' <- zonkTcCoToCo env co
                               ; return (env, WpCast co') }
 zonkCoFn env (WpEvLam ev)   = do { (env', ev') <- zonkEvBndrX env ev
                                  ; return (env', WpEvLam ev') }
@@ -1171,10 +1171,10 @@ zonkVect _ (HsVectInstIn _) = panic "TcHsSyn.zonkVect: HsVectInstIn"
 zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm
 zonkEvTerm env (EvId v)           = ASSERT2( isId v, ppr v )
                                     return (EvId (zonkIdOcc env v))
-zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
+zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcCoToCo env co
                                        ; return (EvCoercion co') }
 zonkEvTerm env (EvCast tm co)     = do { tm' <- zonkEvTerm env tm
-                                       ; co' <- zonkTcLCoToLCo env co
+                                       ; co' <- zonkTcCoToCo env co
                                        ; return (mkEvCast tm' co') }
 zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
                                        ; return (EvTupleSel tm' n) }
@@ -1235,8 +1235,8 @@ zonkEvBind env (EvBind var term)
          -- This has a very big effect on some programs (eg Trac #5030)
        ; let ty' = idType var'
        ; case getEqPredTys_maybe ty' of
-           Just (ty1, ty2) | ty1 `eqType` ty2
-                  -> return (EvBind var' (EvCoercion (mkTcReflCo ty1)))
+           Just (r, ty1, ty2) | ty1 `eqType` ty2
+                  -> return (EvBind var' (EvCoercion (mkTcReflCo r ty1)))
            _other -> do { term' <- zonkEvTerm env term
                         ; return (EvBind var' term') } }
 \end{code}
@@ -1393,35 +1393,40 @@ zonkTypeZapping tv
        ; return ty }
 
 
-zonkTcLCoToLCo :: ZonkEnv -> TcCoercion -> TcM TcCoercion
+zonkTcCoToCo :: ZonkEnv -> TcCoercion -> TcM TcCoercion
 -- NB: zonking often reveals that the coercion is an identity
 --     in which case the Refl-ness can propagate up to the top
 --     which in turn gives more efficient desugaring.  So it's
 --     worth using the 'mk' smart constructors on the RHS
-zonkTcLCoToLCo env co
+zonkTcCoToCo env co
   = go co
   where
     go (TcLetCo bs co)        = do { (env', bs') <- zonkTcEvBinds env bs
-                                   ; co' <- zonkTcLCoToLCo env' co
+                                   ; co' <- zonkTcCoToCo env' co
                                    ; return (TcLetCo bs' co') }
     go (TcCoVarCo cv)         = return (mkTcCoVarCo (zonkEvVarOcc env cv))
-    go (TcRefl ty)            = do { ty' <- zonkTcTypeToType env ty
-                                   ; return (TcRefl ty') }
-    go (TcTyConAppCo tc cos)  = do { cos' <- mapM go cos; return (mkTcTyConAppCo tc cos') }
-    go (TcAxiomInstCo ax ind tys)
-                              = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax ind tys') }
+    go (TcRefl r ty)          = do { ty' <- zonkTcTypeToType env ty
+                                   ; return (TcRefl r ty') }
+    go (TcTyConAppCo r tc cos)
+                              = do { cos' <- mapM go cos; return (mkTcTyConAppCo r tc cos') }
+    go (TcAxiomInstCo ax ind cos)
+                              = do { cos' <- mapM go cos; return (TcAxiomInstCo ax ind cos') }
     go (TcAppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
                                    ; return (mkTcAppCo co1' co2') }
     go (TcCastCo co1 co2)     = do { co1' <- go co1; co2' <- go co2
                                    ; return (TcCastCo co1' co2') }
-    go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co')  }
-    go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co')  }
-    go (TcLRCo lr co)         = do { co' <- go co; return (mkTcLRCo lr co')  }
+    go (TcPhantomCo ty1 ty2)  = do { ty1' <- zonkTcTypeToType env ty1
+                                   ; ty2' <- zonkTcTypeToType env ty2
+                                   ; return (TcPhantomCo ty1' ty2') }
+    go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co') }
+    go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co') }
+    go (TcLRCo lr co)         = do { co' <- go co; return (mkTcLRCo lr co') }
     go (TcTransCo co1 co2)    = do { co1' <- go co1; co2' <- go co2
-                                   ; return (mkTcTransCo co1' co2')  }
+                                   ; return (mkTcTransCo co1' co2') }
     go (TcForAllCo tv co)     = ASSERT( isImmutableTyVar tv )
                                 do { co' <- go co; return (mkTcForAllCo tv co') }
     go (TcInstCo co ty)       = do { co' <- go co; ty' <- zonkTcTypeToType env ty; return (TcInstCo co' ty') }
+    go (TcSubCo co)           = do { co' <- go co; return (mkTcSubCo co') }
     go (TcAxiomRuleCo co ts cs) = do { ts' <- zonkTcTypeToTypes env ts
                                      ; cs' <- mapM go cs
                                      ; return (TcAxiomRuleCo co ts' cs')
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 31318d3108..e3657ae898 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -101,7 +101,7 @@ solveInteractGiven loc fsks givens
                                                      , ctev_loc = loc }
                           | ev_id <- givens ]
 
-    fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
+    fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo Nominal tv_ty)
                                                    , ctev_pred = pred
                                                    , ctev_loc = loc }
                         | tv <- fsks
@@ -988,7 +988,7 @@ solveWithIdentity wd tv xi
                -- cf TcUnify.uUnboundKVar
 
        ; setWantedTyBind tv xi'
-       ; let refl_evtm = EvCoercion (mkTcReflCo xi')
+       ; let refl_evtm = EvCoercion (mkTcReflCo Nominal xi')
 
        ; when (isWanted wd) $
               setEvBind (ctev_evar wd) refl_evtm
@@ -1835,9 +1835,9 @@ matchClassInst _ clas [ ty ] _
                       $ idType meth         -- forall n. KnownNat n => SNat n
         , Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep
         -> return $
-           let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axRep  [ty]
-               co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [ty]
-           in GenInst [] $ EvCast (EvLit evLit) (mkTcTransCo co1 co2)
+           let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo Representational axRep  [ty]
+               co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo Representational axDict [ty]
+           in GenInst [] $ mkEvCast (EvLit evLit) (mkTcTransCo co1 co2)
 
       _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
                      $$ vcat (map (ppr . idType) (classMethods clas)))
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index ee93eb6d5a..4de5375c55 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -809,7 +809,7 @@ zonkFlats binds_var untch cts
       , not (tv `elemVarSet` tyVarsOfType ty_lhs)   -- Do not construct an infinite type
       = ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
         do { writeMetaTyVar tv ty_lhs
-           ; let evterm = EvCoercion (mkTcReflCo ty_lhs)
+           ; let evterm = EvCoercion (mkTcReflCo Nominal ty_lhs)
                  evvar  = ctev_evar (cc_ev zct)
            ; when (isWantedCt orig_ct) $         -- Can be derived (Trac #8129)
              addTcEvBind binds_var evvar evterm
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index ae7ef7330d..f43fe3dea0 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -219,11 +219,11 @@ tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
   | otherwise 
   = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
        ; traceTc "tcPatBndr(no-sig)" (ppr bndr_id $$ ppr (idType bndr_id))
-       ; return (mkTcReflCo pat_ty, bndr_id) }
+       ; return (mkTcReflCo Nominal pat_ty, bndr_id) }
 
 tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
   = do { bndr <- mkLocalBinder bndr_name pat_ty
-       ; return (mkTcReflCo pat_ty, bndr) }
+       ; return (mkTcReflCo Nominal pat_ty, bndr) }
 
 ------------
 newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
@@ -773,7 +773,7 @@ matchExpectedConTy data_tc pat_ty
        ; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
        	     -- co1 : T (ty1,ty2) ~ pat_ty
 
-       ; let co2 = mkTcUnbranchedAxInstCo co_tc tys
+       ; let co2 = mkTcUnbranchedAxInstCo Nominal co_tc tys
        	     -- co2 : T (ty1,ty2) ~ T7 ty1 ty2
 
        ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys) }
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 3adb15855e..3fed94b100 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1423,7 +1423,7 @@ newFlattenSkolem ev fam_ty
 
        ; let rhs_ty = mkTyVarTy tv
              ctev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
-                            , ctev_evtm = EvCoercion (mkTcReflCo fam_ty)
+                            , ctev_evtm = EvCoercion (mkTcReflCo Nominal fam_ty)
                             , ctev_loc =  ctev_loc ev }
        ; dflags <- getDynFlags
        ; updInertTcS $ \ is@(IS { inert_fsks = fsks }) ->
@@ -1704,6 +1704,7 @@ rewriteCtFlavor (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
 
 rewriteCtFlavor (CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
   = do { new_evar <- newWantedEvVar loc new_pred
+       ; ASSERT ( tcCoercionRole co == Nominal ) return ()
        ; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
        ; case new_evar of
             Fresh ctev -> return (Just ctev)
@@ -1722,13 +1723,13 @@ matchFam tycon args
            Nothing -> return Nothing
            Just (FamInstMatch { fim_instance = famInst
                               , fim_tys      = inst_tys })
-             -> let co = mkTcUnbranchedAxInstCo (famInstAxiom famInst) inst_tys
+             -> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys
                     ty = pSnd $ tcCoercionKind co
                 in return $ Just (co, ty) }
 
   | Just ax <- isClosedSynFamilyTyCon_maybe tycon
   , Just (ind, inst_tys) <- chooseBranch ax args
-  = let co = mkTcAxInstCo ax ind inst_tys
+  = let co = mkTcAxInstCo Nominal ax ind inst_tys
         ty = pSnd (tcCoercionKind co)
     in return $ Just (co, ty)
 
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 4a24504860..c67ffcfdd3 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -131,7 +131,7 @@ matchExpectedFunTys herald arity orig_ty
     -- then   co : ty ~ t1 -> .. -> tn -> ty_r
 
     go n_req ty
-      | n_req == 0 = return (mkTcReflCo ty, [], ty)
+      | n_req == 0 = return (mkTcReflCo Nominal ty, [], ty)
 
     go n_req ty
       | Just ty' <- tcView ty = go n_req ty'
@@ -139,7 +139,7 @@ matchExpectedFunTys herald arity orig_ty
     go n_req (FunTy arg_ty res_ty)
       | not (isPredTy arg_ty)
       = do { (co, tys, ty_r) <- go (n_req-1) res_ty
-           ; return (mkTcFunCo (mkTcReflCo arg_ty) co, arg_ty:tys, ty_r) }
+           ; return (mkTcFunCo Nominal (mkTcReflCo Nominal arg_ty) co, arg_ty:tys, ty_r) }
 
     go n_req ty@(TyVarTy tv)
       | ASSERT( isTcTyVar tv) isMetaTyVar tv
@@ -222,7 +222,7 @@ matchExpectedTyConApp tc orig_ty
 
     go ty@(TyConApp tycon args) 
        | tc == tycon  -- Common case
-       = return (mkTcReflCo ty, args)
+       = return (mkTcReflCo Nominal ty, args)
 
     go (TyVarTy tv)
        | ASSERT( isTcTyVar tv) isMetaTyVar tv
@@ -267,7 +267,7 @@ matchExpectedAppTy orig_ty
       | Just ty' <- tcView ty = go ty'
 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
-      = return (mkTcReflCo orig_ty, (fun_ty, arg_ty))
+      = return (mkTcReflCo Nominal orig_ty, (fun_ty, arg_ty))
 
     go (TyVarTy tv)
       | ASSERT( isTcTyVar tv) isMetaTyVar tv
@@ -604,7 +604,7 @@ uType origin orig_ty1 orig_ty2
     go (FunTy fun1 arg1) (FunTy fun2 arg2)
       = do { co_l <- uType origin fun1 fun2
            ; co_r <- uType origin arg1 arg2
-           ; return $ mkTcFunCo co_l co_r }
+           ; return $ mkTcFunCo Nominal co_l co_r }
 
         -- Always defer if a type synonym family (type function)
       	-- is involved.  (Data families behave rigidly.)
@@ -617,11 +617,11 @@ uType origin orig_ty1 orig_ty2
       -- See Note [Mismatched type lists and application decomposition]
       | tc1 == tc2, length tys1 == length tys2
       = do { cos <- zipWithM (uType origin) tys1 tys2
-           ; return $ mkTcTyConAppCo tc1 cos }
+           ; return $ mkTcTyConAppCo Nominal tc1 cos }
 
     go (LitTy m) ty@(LitTy n)
       | m == n
-      = return $ mkTcReflCo ty
+      = return $ mkTcReflCo Nominal ty
 
 	-- See Note [Care with type applications]
         -- Do not decompose FunTy against App; 
@@ -769,7 +769,7 @@ uUnfilledVar :: CtOrigin
 
 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
   | tv1 == tv2  -- Same type variable => no-op
-  = return (mkTcReflCo (mkTyVarTy tv1))
+  = return (mkTcReflCo Nominal (mkTyVarTy tv1))
 
   | otherwise  -- Distinct type variables
   = do  { lookup2 <- lookupTcTyVar tv2
@@ -1044,7 +1044,7 @@ lookupTcTyVar tyvar
 updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion
 updateMeta tv1 ref1 ty2
   = do { writeMetaTyVarRef tv1 ref1 ty2
-       ; return (mkTcReflCo ty2) }
+       ; return (mkTcReflCo Nominal ty2) }
 \end{code}
 
 Note [Unifying untouchables]
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 35e40f3649..27bad5c7d4 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -1021,7 +1021,7 @@ mkSubCo (Refl Nominal ty) = Refl Representational ty
 mkSubCo (TyConAppCo Nominal tc cos)
   = TyConAppCo Representational tc (applyRoles tc cos)
 mkSubCo (UnivCo Nominal ty1 ty2) = UnivCo Representational ty1 ty2
-mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co )
+mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
              SubCo co
 
 
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 9940f73082..d45cd8c6ef 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -56,7 +56,7 @@ module Type (
         -- Deconstructing predicate types
         PredTree(..), classifyPredType,
         getClassPredTys, getClassPredTys_maybe,
-        getEqPredTys, getEqPredTys_maybe,
+        getEqPredTys, getEqPredTys_maybe, getEqPredRole,
 
         -- ** Common type constructors
         funTyCon,
@@ -161,7 +161,8 @@ import Class
 import TyCon
 import TysPrim
 import {-# SOURCE #-} TysWiredIn ( eqTyCon, typeNatKind, typeSymbolKind )
-import PrelNames ( eqTyConKey, ipClassNameKey, openTypeKindTyConKey,
+import PrelNames ( eqTyConKey, coercibleTyConKey,
+                   ipClassNameKey, openTypeKindTyConKey,
                    constraintKindTyConKey, liftedTypeKindTyConKey )
 import CoAxiom
 
@@ -994,15 +995,27 @@ getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
 getEqPredTys :: PredType -> (Type, Type)
 getEqPredTys ty
   = case splitTyConApp_maybe ty of
-      Just (tc, (_ : ty1 : ty2 : tys)) -> ASSERT( tc `hasKey` eqTyConKey && null tys )
-                                          (ty1, ty2)
+      Just (tc, (_ : ty1 : ty2 : tys)) ->
+        ASSERT( null tys && (tc `hasKey` eqTyConKey || tc `hasKey` coercibleTyConKey) )
+        (ty1, ty2)
       _ -> pprPanic "getEqPredTys" (ppr ty)
 
-getEqPredTys_maybe :: PredType -> Maybe (Type, Type)
+getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
 getEqPredTys_maybe ty
   = case splitTyConApp_maybe ty of
-      Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
+      Just (tc, [_, ty1, ty2])
+        | tc `hasKey` eqTyConKey -> Just (Nominal, ty1, ty2)
+        | tc `hasKey` coercibleTyConKey -> Just (Representational, ty1, ty2)
       _ -> Nothing
+
+getEqPredRole :: PredType -> Role
+getEqPredRole ty
+  = case splitTyConApp_maybe ty of
+      Just (tc, [_, _, _])
+        | tc `hasKey` eqTyConKey -> Nominal
+        | tc `hasKey` coercibleTyConKey -> Representational
+      _ -> pprPanic "getEqPredRole" (ppr ty)
+
 \end{code}
 
 %************************************************************************