Introduce coerce :: Coercible a b -> a -> bcoercible

This is the result of the design at
http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers

The goal is to be able to convert between, say [First Int] and [Last
Int] with zero run-time overhead. To that end, we introduce a special
two parameter type class Coercible whose instances are created
automatically and on-the fly. This relies on and exploits the recent
addition of roles to core.

12 files changed, 440 insertions, 13 deletions

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index 21553ab4f9..45d94598ea 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -137,7 +137,8 @@ ghcPrimIds
     unsafeCoerceId,
     nullAddrId,
     seqId,
-    magicSingIId
+    magicSingIId,
+    coerceId
     ]
 \end{code}
 
@@ -1036,7 +1037,7 @@ they can unify with both unlifted and lifted types.  Hence we provide
 another gun with which to shoot yourself in the foot.
 
 \begin{code}
-lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName :: Name
+lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName, coerceName :: Name
 unsafeCoerceName  = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
 nullAddrName      = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#")     nullAddrIdKey      nullAddrId
 seqName           = mkWiredInIdName gHC_PRIM (fsLit "seq")           seqIdKey           seqId
@@ -1044,6 +1045,7 @@ realWorldName     = mkWiredInIdName gHC_PRIM (fsLit "realWorld#")    realWorldPr
 lazyIdName        = mkWiredInIdName gHC_MAGIC (fsLit "lazy")         lazyIdKey           lazyId
 coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
 magicSingIName    = mkWiredInIdName gHC_PRIM (fsLit "magicSingI")    magicSingIKey magicSingIId
+coerceName        = mkWiredInIdName gHC_PRIM (fsLit "coerce")        coerceKey          coerceId
 \end{code}
 
 \begin{code}
@@ -1118,6 +1120,21 @@ magicSingIId = pcMiscPrelId magicSingIName ty info
   info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
   ty   = mkForAllTys [alphaTyVar] alphaTy
 
+--------------------------------------------------------------------------------
+
+coerceId :: Id
+coerceId = pcMiscPrelId coerceName ty info
+  where
+    info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
+                       `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
+    eqRTy = mkTyConApp coercibleTyCon [alphaTy, betaTy]
+    eqRPrimTy = mkTyConApp eqReprPrimTyCon [liftedTypeKind, alphaTy, betaTy]
+    ty   = mkForAllTys [alphaTyVar, betaTyVar] (mkFunTys [eqRTy, alphaTy] betaTy)
+
+    [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy,eqRPrimTy]
+    rhs = mkLams [alphaTyVar,betaTyVar,eqR,x] $
+          mkWildCase (Var eqR) eqRTy betaTy $
+	  [(DataAlt coercibleDataCon, [eq], Cast (Var x) (CoVarCo eq))]
 \end{code}
 
 Note [Unsafe coerce magic]
diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs
index c6fc2be21f..656ffa8184 100644
--- a/compiler/coreSyn/MkCore.lhs
+++ b/compiler/coreSyn/MkCore.lhs
@@ -28,6 +28,9 @@ module MkCore (
         -- * Constructing/deconstructing equality evidence boxes
         mkEqBox,
         
+        -- * Constructing Coercible evidence
+        mkCoercible,
+
         -- * Constructing general big tuples
         -- $big_tuples
         mkChunkified,
@@ -305,6 +308,11 @@ mkEqBox co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ p
   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` [ty1, ty2] `App` Coercion co
+  where Pair ty1 ty2 = coercionKind co
+        k = typeKind ty1
 \end{code}
 
 %************************************************************************
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index a1f5e77b5f..0323ea1847 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -44,12 +44,12 @@ import Unique( Unique )
 import Digraph
 
 
-import TyCon      ( isTupleTyCon, tyConDataCons_maybe )
+import TyCon      ( isTupleTyCon, tyConDataCons_maybe, unwrapNewTyCon_maybe )
 import TcEvidence
 import TcType
 import Type
 import Coercion hiding (substCo)
-import TysWiredIn ( eqBoxDataCon, tupleCon )
+import TysWiredIn ( eqBoxDataCon, coercibleTyCon, coercibleDataCon, tupleCon )
 import Id
 import Class
 import DataCon	( dataConWorkId )
@@ -785,6 +785,49 @@ dsEvTerm (EvLit l) =
     EvNum n -> mkIntegerExpr n
     EvStr s -> mkStringExprFS s
 
+-- Note [Coercible Instances]
+dsEvTerm (EvCoercible (EvCoercibleRefl ty)) = do
+  return $ mkCoercible $ mkReflCo Representational ty
+
+dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
+  ntEvs <- mapM (mapEvCoercibleArgM dsEvTerm) evs
+  wrapInEqRCases ntEvs $ \cos -> do
+    return $ mkCoercible $
+      mkTyConAppCo Representational tyCon cos
+
+dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
+  ntEv <- dsEvTerm v
+  wrapInEqRCase ntEv $ \co -> do
+          return $ mkCoercible $
+                connect lor co $
+                mkUnbranchedAxInstCo Representational coAxiom tys
+  where Just (_, _, coAxiom) = unwrapNewTyCon_maybe tyCon
+        connect CLeft co2 co1 = mkTransCo co1 co2
+        connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
+
+wrapInEqRCase :: CoreExpr -> (Coercion -> DsM CoreExpr) -> DsM CoreExpr
+wrapInEqRCase e mkBody = do
+  cov <- newSysLocalDs (mkCoercionType Representational ty1 ty2)
+  body' <- mkBody (mkCoVarCo cov)
+  return $
+        ASSERT (tc == coercibleTyCon)
+        mkWildCase
+                e
+                (exprType e)
+                (exprType body')
+                [(DataAlt coercibleDataCon, [cov], body')]
+  where
+  Just (tc, [ty1, ty2]) = splitTyConApp_maybe (exprType e)
+
+wrapInEqRCases :: [EvCoercibleArg CoreExpr] -> ([Coercion] -> DsM CoreExpr) -> DsM CoreExpr
+wrapInEqRCases (EvCoercibleArgN t:es) mkBody =
+  wrapInEqRCases es (\cos -> mkBody (mkReflCo Nominal t:cos))
+wrapInEqRCases (EvCoercibleArgR e:es) mkBody = wrapInEqRCase e $ \co ->
+  wrapInEqRCases es (\cos -> mkBody (co:cos))
+wrapInEqRCases (EvCoercibleArgP t1 t2:es) mkBody =
+  wrapInEqRCases es (\cos -> mkBody (mkUnivCo Phantom t1 t2:cos))
+wrapInEqRCases [] mkBody = mkBody []
+
 ---------------------------------------
 dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
 -- This is the crucial function that moves 
diff --git a/compiler/prelude/PrelInfo.lhs b/compiler/prelude/PrelInfo.lhs
index 4a39977797..0ef5b32eb3 100644
--- a/compiler/prelude/PrelInfo.lhs
+++ b/compiler/prelude/PrelInfo.lhs
@@ -130,7 +130,7 @@ ghcPrimExports
  = map (Avail . idName) ghcPrimIds ++
    map (Avail . idName . primOpId) allThePrimOps ++
    [ AvailTC n [n] 
-   | tc <- funTyCon : primTyCons, let n = tyConName tc  ]
+   | tc <- funTyCon : coercibleTyCon : primTyCons, let n = tyConName tc  ]
 \end{code}
 
 
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index acac400c04..dfb3f82b7b 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -352,7 +352,7 @@ genericTyConNames = [
 pRELUDE :: Module
 pRELUDE         = mkBaseModule_ pRELUDE_NAME
 
-gHC_PRIM, gHC_PRIMWRAPPERS, gHC_TYPES, gHC_GENERICS, gHC_MAGIC,
+gHC_PRIM, gHC_PRIMWRAPPERS, gHC_TYPES, gHC_GENERICS, gHC_MAGIC, gHC_COERCIBLE,
     gHC_CLASSES, gHC_BASE, gHC_ENUM, gHC_GHCI, gHC_CSTRING,
     gHC_SHOW, gHC_READ, gHC_NUM, gHC_INTEGER_TYPE, gHC_LIST,
     gHC_TUPLE, dATA_TUPLE, dATA_EITHER, dATA_STRING, dATA_FOLDABLE, dATA_TRAVERSABLE, dATA_MONOID,
@@ -370,6 +370,7 @@ gHC_TYPES       = mkPrimModule (fsLit "GHC.Types")
 gHC_MAGIC       = mkPrimModule (fsLit "GHC.Magic")
 gHC_CSTRING     = mkPrimModule (fsLit "GHC.CString")
 gHC_CLASSES     = mkPrimModule (fsLit "GHC.Classes")
+gHC_COERCIBLE   = mkPrimModule (fsLit "GHC.Coercible")
 
 gHC_BASE        = mkBaseModule (fsLit "GHC.Base")
 gHC_ENUM        = mkBaseModule (fsLit "GHC.Enum")
@@ -1486,6 +1487,11 @@ doubleX2PrimTyConKey = mkPreludeTyConUnique 171
 int32X4PrimTyConKey  = mkPreludeTyConUnique 172
 int64X2PrimTyConKey  = mkPreludeTyConUnique 173
 
+ntTyConKey:: Unique
+ntTyConKey = mkPreludeTyConUnique 174
+coercibleTyConKey :: Unique
+coercibleTyConKey = mkPreludeTyConUnique 175
+
 ---------------- Template Haskell -------------------
 --      USES TyConUniques 200-299
 -----------------------------------------------------
@@ -1504,7 +1510,7 @@ unitTyConKey = mkTupleTyConUnique BoxedTuple 0
 charDataConKey, consDataConKey, doubleDataConKey, falseDataConKey,
     floatDataConKey, intDataConKey, nilDataConKey, ratioDataConKey,
     stableNameDataConKey, trueDataConKey, wordDataConKey,
-    ioDataConKey, integerDataConKey, eqBoxDataConKey :: Unique
+    ioDataConKey, integerDataConKey, eqBoxDataConKey, coercibleDataConKey :: Unique
 charDataConKey                          = mkPreludeDataConUnique  1
 consDataConKey                          = mkPreludeDataConUnique  2
 doubleDataConKey                        = mkPreludeDataConUnique  3
@@ -1544,6 +1550,8 @@ gtDataConKey                            = mkPreludeDataConUnique 29
 integerGmpSDataConKey, integerGmpJDataConKey :: Unique
 integerGmpSDataConKey                   = mkPreludeDataConUnique 30
 integerGmpJDataConKey                   = mkPreludeDataConUnique 31
+
+coercibleDataConKey                     = mkPreludeDataConUnique 32
 \end{code}
 
 %************************************************************************
@@ -1710,6 +1718,9 @@ undefinedKey                  = mkPreludeMiscIdUnique 155
 
 magicSingIKey :: Unique
 magicSingIKey              = mkPreludeMiscIdUnique 156
+
+coerceKey :: Unique
+coerceKey                     = mkPreludeMiscIdUnique 157
 \end{code}
 
 Certain class operations from Prelude classes.  They get their own
diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs
index d8c880f1c3..443c09cf1e 100644
--- a/compiler/prelude/TysWiredIn.lhs
+++ b/compiler/prelude/TysWiredIn.lhs
@@ -68,6 +68,7 @@ module TysWiredIn (
 
         -- * Equality predicates
         eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon,
+        coercibleTyCon, coercibleDataCon, coercibleClass,
 
         mkWiredInTyConName -- This is used in TcTypeNats to define the
                            -- built-in functions for evaluation.
@@ -88,6 +89,7 @@ import Type             ( mkTyConApp )
 import DataCon
 import Var
 import TyCon
+import Class            ( Class, mkClass )
 import TypeRep
 import RdrName
 import Name
@@ -147,6 +149,7 @@ wiredInTyCons = [ unitTyCon     -- Not treated like other tuples, because
               , listTyCon
               , parrTyCon
               , eqTyCon
+              , coercibleTyCon
               , typeNatKindCon
               , typeSymbolKindCon
               ]
@@ -172,6 +175,10 @@ eqTyConName, eqBoxDataConName :: Name
 eqTyConName      = mkWiredInTyConName   BuiltInSyntax gHC_TYPES (fsLit "~")   eqTyConKey      eqTyCon
 eqBoxDataConName = mkWiredInDataConName UserSyntax    gHC_TYPES (fsLit "Eq#") eqBoxDataConKey eqBoxDataCon
 
+coercibleTyConName, coercibleDataConName :: Name
+coercibleTyConName   = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "Coercible")  coercibleTyConKey   coercibleTyCon
+coercibleDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "MkCoercible") coercibleDataConKey coercibleDataCon
+
 charTyConName, charDataConName, intTyConName, intDataConName :: Name
 charTyConName     = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "Char") charTyConKey charTyCon
 charDataConName   = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "C#") charDataConKey charDataCon
@@ -451,6 +458,26 @@ eqBoxDataCon = pcDataCon eqBoxDataConName args [TyConApp eqPrimTyCon (map mkTyVa
     k = mkTyVarTy kv
     a:b:_ = tyVarList k
     args = [kv, a, b]
+
+
+coercibleTyCon :: TyCon
+coercibleTyCon = mkClassTyCon
+    coercibleTyConName kind tvs [Representational, Representational]
+    rhs coercibleClass NonRecursive
+  where kind = mkArrowKinds [liftedTypeKind, liftedTypeKind] constraintKind
+        a:b:_ = tyVarList liftedTypeKind
+        tvs = [a, b]
+        rhs = DataTyCon [coercibleDataCon] False
+
+coercibleDataCon :: DataCon
+coercibleDataCon = pcDataCon coercibleDataConName args [TyConApp eqReprPrimTyCon (liftedTypeKind : map mkTyVarTy args)] coercibleTyCon
+  where
+    a:b:_ = tyVarList liftedTypeKind
+    args = [a, b]
+
+coercibleClass :: Class
+coercibleClass = mkClass (tyConTyVars coercibleTyCon) [] [] [] [] [] coercibleTyCon
+
 \end{code}
 
 \begin{code}
diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index 094c2f55e6..a59dfd624d 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -2279,6 +2279,62 @@ primop  TraceMarkerOp "traceMarker#" GenPrimOp
    has_side_effects = True
    out_of_line      = True
 
+------------------------------------------------------------------------
+section "Safe coercions"
+------------------------------------------------------------------------
+
+pseudoop   "coerce"
+   Coercible a b => a -> b
+   { The function {\tt coerce} allows you to safely convert between values of
+     types that have the same representation with no run-time overhead. In the
+     simplest case you can use it instead of a newtype constructor, to go from
+     the newtype's concrete type to the abstract type. But it also works in
+     more complicated settings, e.g. converting a list of newtypes to a list of
+     concrete types.
+   }
+
+primclass Coercible a b
+   { This two-parameter class has instances for types {\tt a} and {\tt b} if
+     the compiler can infer that they have the same representation. This class
+     does not have regular instances; instead they are created on-the-fly during
+     type-checking. Trying to manually declare an instance of {\tt Coercible}
+     is an error.
+
+     Nevertheless one can pretend that the following three kinds of instances
+     exist. First, as a trivial base-case:
+
+     {\tt instance a a}
+
+     Furthermore, for every type constructor there is
+     an instance that allows to coerce under the type constructor. For
+     example, let {\tt D} be a prototypical type constructor ({\tt data} or {\tt
+     newtype}) with three type arguments, which have roles Nominal,
+     Representational resp. Phantom. Then there is an instance of the form
+
+     {\tt instance Coercible b b' => Coercible (D a b c) (D a b' c')}
+
+     Note that the nominal type arguments are equal, the representational type
+     arguments can differ, but need to have a {\tt Coercible} instance
+     themself, and the phantom type arguments can be changed arbitrarily.
+
+     In SafeHaskell code, this instance is only usable if the constructors of
+     every type constructor used in the definition of {\tt D} (including
+     those of {\tt D} itself) is in scope.
+
+     The third kind of instance exists for every {\tt newtype NT = MkNT T} and
+     comes in two variants, namely
+
+     {\tt instance Coercible a T => Coercible a NT}
+
+     {\tt instance Coercible T b => Coercible NT b}
+
+     This instance is only usable if the constructor {\tt MkNT} is in scope.
+
+     If, as a library author of a type constructor like {\tt Set a}, you
+     want to prevent a user of your module to write
+     {\tt coerce :: Set T -> Set NT},
+     you need to set the role of {\tt Set}'s type parameter to Nominal.
+   }
 
 ------------------------------------------------------------------------
 section "Float SIMD Vectors" 
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 3851c7ef02..a1d2f1c6cd 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -27,8 +27,11 @@ import Unify            ( tcMatchTys )
 import Inst
 import InstEnv
 import TyCon
+import DataCon
 import TcEvidence
+import TysWiredIn       ( coercibleClass )
 import Name
+import RdrName          ( lookupGRE_Name )
 import Id 
 import Var
 import VarSet
@@ -42,7 +45,7 @@ import FastString
 import Outputable
 import SrcLoc
 import DynFlags
-import Data.List        ( partition, mapAccumL )
+import Data.List        ( partition, mapAccumL, zip4 )
 \end{code}
 
 %************************************************************************
@@ -934,7 +937,9 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
   = do { let (is_ambig, ambig_msg) = mkAmbigMsg ct
        ; (ctxt, binds_msg) <- relevantBindings True ctxt ct
        ; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
-       ; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
+       ; safe_mod <- safeLanguageOn `fmap` getDynFlags
+       ; rdr_env <- getGlobalRdrEnv
+       ; return (ctxt, cannot_resolve_msg safe_mod rdr_env is_ambig binds_msg ambig_msg) }
 
   | not safe_haskell   -- Some matches => overlap errors
   = return (ctxt, overlap_msg)
@@ -949,8 +954,9 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
     givens      = getUserGivens ctxt
     all_tyvars  = all isTyVarTy tys
 
-    cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
-      = vcat [ addArising orig (no_inst_herald <+> pprParendType pred)
+    cannot_resolve_msg safe_mod rdr_env has_ambig_tvs binds_msg ambig_msg
+      = vcat [ addArising orig (no_inst_herald <+> pprParendType pred $$
+                                coercible_msg safe_mod rdr_env)
              , vcat (pp_givens givens)
              , ppWhen (has_ambig_tvs && not (null unifiers && null givens))
                (vcat [ ambig_msg, binds_msg, potential_msg ])
@@ -1064,6 +1070,78 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
                     ]
              ]
 
+    -- This function tries to reconstruct why a "Coercible ty1 ty2" constraint
+    -- is left over. Therefore its logic has to stay in sync with
+    -- getCoericbleInst in TcInteract. See Note [Coercible Instances]
+    coercible_msg safe_mod rdr_env
+      | clas /= coercibleClass = empty
+      | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
+        Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
+        tc1 == tc2
+      = nest 2 $ vcat $
+          -- Only for safe haskell: First complain if tc is abstract, only if
+          -- not check if the type constructors therein are abstract
+          (if safe_mod
+           then case tyConAbstractMsg rdr_env tc1 empty of
+                    Just msg ->
+                       [ msg $$ ptext (sLit "as required in SafeHaskell mode") ]
+                    Nothing ->
+                       [ msg
+                       | tc <- tyConsOfTyCon tc1
+                       , Just msg <- return $
+                           tyConAbstractMsg rdr_env tc $
+                             parens $ ptext (sLit "used within") <+> quotes (ppr tc1)
+                       ]
+           else []
+          ) ++
+          [ fsep [ hsep [ ptext $ sLit "because the", speakNth n, ptext $ sLit "type argument"]
+                 , hsep [ ptext $ sLit "of", quotes (ppr tc1), ptext $ sLit "has role Nominal,"]
+                 , ptext $ sLit "but the arguments"
+                 , quotes (ppr t1)
+                 , ptext $ sLit "and"
+                 , quotes (ppr t2)
+                 , ptext $ sLit "differ" ]
+          | (n,Nominal,t1,t2) <- zip4 [1..] (tyConRoles tc1) tyArgs1 tyArgs2
+          , not (t1 `eqType` t2)
+          ]
+      | Just (tc,_) <- splitTyConApp_maybe ty1,
+        Just msg <- coercible_msg_for_tycon rdr_env tc
+      = msg
+      | Just (tc,_) <- splitTyConApp_maybe ty2,
+        Just msg <- coercible_msg_for_tycon rdr_env tc
+      = msg
+      | otherwise
+      = nest 2 $ hsep [ ptext $ sLit "because", quotes (ppr ty1),
+                        ptext $ sLit "and", quotes (ppr ty2),
+                        ptext $ sLit "are different types." ]
+      where
+        (clas, ~[ty1,ty2]) = getClassPredTys (ctPred ct)
+
+    dataConMissing rdr_env tc =
+        all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc))
+
+    coercible_msg_for_tycon rdr_env tc
+        | isRecursiveTyCon tc
+        = Just $ nest 2 $ hsep [ ptext $ sLit "because", quotes (ppr tc)
+                               , ptext $ sLit "is a recursive type constuctor" ]
+        | isNewTyCon tc
+        = tyConAbstractMsg rdr_env tc empty
+        | otherwise
+        = Nothing
+
+    tyConAbstractMsg rdr_env tc occExpl
+        | isAbstractTyCon tc || dataConMissing rdr_env tc = Just $ vcat $
+            [ fsep [ ptext $ sLit "because the type constructor", quotes (ppr tc) <+> occExpl
+                   , ptext $ sLit "is abstract" ]
+            | isAbstractTyCon tc
+            ] ++
+            [ fsep [ ptext (sLit "because the constructor") <> plural (tyConDataCons tc)
+                   , ptext (sLit "of") <+> quotes (ppr tc) <+> occExpl
+                   , isOrAre (tyConDataCons tc) <+> ptext (sLit "not imported") ]
+            | dataConMissing rdr_env tc
+            ]
+        | otherwise = Nothing
+
 show_fixes :: [SDoc] -> SDoc
 show_fixes []     = empty
 show_fixes (f:fs) = sep [ ptext (sLit "Possible fix:")
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index ffdce640fd..09c0333447 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -16,6 +16,7 @@ module TcEvidence (
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
   EvTerm(..), mkEvCast, evVarsOfTerm, 
   EvLit(..), evTermCoercion,
+  EvCoercible(..), EvCoercibleArg(..), mapEvCoercibleArgM,
 
   -- TcCoercion
   TcCoercion(..), LeftOrRight(..), pickLR,
@@ -534,6 +535,9 @@ data EvTerm
   | EvLit EvLit                  -- Dictionary for class "SingI" for type lits.
                                  -- Note [SingI and EvLit]
 
+  | EvCoercible EvCoercible      -- Dictionary for "Coercible a b"
+                                 -- Note [Coercible Instances]
+
   deriving( Data.Data, Data.Typeable)
 
 
@@ -542,6 +546,22 @@ data EvLit
   | EvStr FastString
     deriving( Data.Data, Data.Typeable)
 
+data EvCoercible
+  = EvCoercibleRefl Type
+  | EvCoercibleTyCon TyCon [EvCoercibleArg EvTerm]
+  | EvCoercibleNewType LeftOrRight TyCon [Type] EvTerm
+    deriving( Data.Data, Data.Typeable)
+
+data EvCoercibleArg a
+  = EvCoercibleArgN Type
+  | EvCoercibleArgR a
+  | EvCoercibleArgP Type Type
+    deriving( Data.Data, Data.Typeable)
+
+mapEvCoercibleArgM :: Monad m => (a -> m b) -> EvCoercibleArg a -> m (EvCoercibleArg b)
+mapEvCoercibleArgM _ (EvCoercibleArgN t)     = return (EvCoercibleArgN t)
+mapEvCoercibleArgM f (EvCoercibleArgR v)     = do { v' <- f v; return (EvCoercibleArgR v') }
+mapEvCoercibleArgM _ (EvCoercibleArgP t1 t2) = return (EvCoercibleArgP t1 t2)
 \end{code}
 
 Note [Coercion evidence terms]
@@ -654,6 +674,12 @@ evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo c
 evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
 evVarsOfTerm (EvLit _)            = emptyVarSet
+evVarsOfTerm (EvCoercible evnt)   = evVarsOfEvCoercible evnt
+
+evVarsOfEvCoercible :: EvCoercible -> VarSet
+evVarsOfEvCoercible (EvCoercibleRefl _)          = emptyVarSet
+evVarsOfEvCoercible (EvCoercibleTyCon _ evs)     = evVarsOfTerms [v | EvCoercibleArgR v <- evs ]
+evVarsOfEvCoercible (EvCoercibleNewType _ _ _ v) = evVarsOfTerm v
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet 
@@ -716,11 +742,23 @@ instance Outputable EvTerm where
   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
   ppr (EvLit l)          = ppr l
+  ppr (EvCoercible co)   = ptext (sLit "Coercible") <+> ppr co
   ppr (EvDelayedError ty msg) =     ptext (sLit "error") 
                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
 
 instance Outputable EvLit where
   ppr (EvNum n) = integer n
   ppr (EvStr s) = text (show s)
+
+instance Outputable EvCoercible where
+  ppr (EvCoercibleRefl ty) = ppr ty
+  ppr (EvCoercibleTyCon tyCon evs) = ppr tyCon <+> hsep (map ppr evs)
+  ppr (EvCoercibleNewType CLeft tyCon tys v) = ppr (tyCon `mkTyConApp` tys) <+> char ';' <+> ppr v
+  ppr (EvCoercibleNewType CRight tyCon tys v) =ppr v <+> char ';' <+> ppr (tyCon `mkTyConApp` tys)
+
+instance Outputable a => Outputable (EvCoercibleArg a) where
+  ppr (EvCoercibleArgN t)     = ptext (sLit "N:") <+> ppr t
+  ppr (EvCoercibleArgR v)     = ptext (sLit "R:") <+> ppr v
+  ppr (EvCoercibleArgP t1 t2) = ptext (sLit "P:") <+> parens (ppr (t1,t2))
 \end{code}
 
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 363e691348..d79e717f93 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -1178,6 +1178,9 @@ zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
 zonkEvTerm env (EvTupleMk tms)    = do { tms' <- mapM (zonkEvTerm env) tms
                                        ; return (EvTupleMk tms') }
 zonkEvTerm _   (EvLit l)          = return (EvLit l)
+zonkEvTerm env (EvCoercible evnt) = do { evnt' <- zonkEvCoercible env evnt
+                                       ; return (EvCoercible evnt')
+                                       }
 zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
                                        ; return (EvSuperClass d' n) }
 zonkEvTerm env (EvDFunApp df tys tms)
@@ -1188,6 +1191,16 @@ zonkEvTerm env (EvDelayedError ty msg)
   = do { ty' <- zonkTcTypeToType env ty
        ; return (EvDelayedError ty' msg) }
 
+
+zonkEvCoercible :: ZonkEnv -> EvCoercible -> TcM EvCoercible
+zonkEvCoercible _   (EvCoercibleRefl ty) = return (EvCoercibleRefl ty)
+zonkEvCoercible env (EvCoercibleTyCon tyCon evs) = do
+        evs' <- mapM (mapEvCoercibleArgM (zonkEvTerm env)) evs
+        return (EvCoercibleTyCon tyCon evs')
+zonkEvCoercible env (EvCoercibleNewType l tyCon tys v) = do
+        v' <- zonkEvTerm env v
+        return (EvCoercibleNewType l tyCon tys v')
+
 zonkTcEvBinds :: ZonkEnv -> TcEvBinds -> TcM (ZonkEnv, TcEvBinds)
 zonkTcEvBinds env (TcEvBinds var) = do { (env', bs') <- zonkEvBindsVar env var
                                        ; return (env', EvBinds bs') }
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 9b970c96e6..6154416b9e 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -26,11 +26,14 @@ import InstEnv( lookupInstEnv, instanceDFunId )
 import Var
 import TcType
 import PrelNames (singIClassName, ipClassNameKey )
+import TysWiredIn ( coercibleClass )
 import Id( idType )
 import Class
 import TyCon
+import DataCon
 import Name
-
+import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
+                 is_decl, Provenance(Imported), gre_prov )
 import FunDeps
 
 import TcEvidence
@@ -45,7 +48,7 @@ import Maybes( orElse )
 import Bag
 
 import Control.Monad ( foldM )
-import Data.Maybe(catMaybes)
+import Data.Maybe ( catMaybes, mapPaybe )
 
 import VarEnv
 
@@ -1724,6 +1727,11 @@ data LookupInstResult
   = NoInstance
   | GenInst [CtEvidence] EvTerm 
 
+instance Outputable LookupInstResult where
+  ppr NoInstance = text "NoInstance"
+  ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
+
+
 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
 
 matchClassInst _ clas [ k, ty ] _
@@ -1768,6 +1776,15 @@ matchClassInst _ clas [ k, ty ] _
 
   unexpected = panicTcS (text "Unexpected evidence for SingI")
 
+matchClassInst _ clas [ ty1, ty2 ] _
+  | clas == coercibleClass =  do
+      traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
+      rdr_env <- getGlobalRdrEnvTcS
+      safeMode <- safeLanguageOn `fmap` getDynFlags
+      ev <- getCoericbleInst safeMode rdr_env ty1 ty2
+      traceTcS "matchClassInst returned" $ ppr ev
+      return ev
+
 matchClassInst inerts clas tys loc
    = do { dflags <- getDynFlags
         ; untch <- getUntouchables
@@ -1848,8 +1865,117 @@ matchClassInst inerts clas tys loc
        | otherwise = False -- No overlap with a solved, already been taken care of 
                            -- by the overlap check with the instance environment.
      matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
+
+-- See Note [Coercible Instances]
+-- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
+getCoericbleInst :: Bool -> GlobalRdrEnv -> TcType -> TcType -> TcS LookupInstResult
+getCoericbleInst safeMode rdr_env ty1 ty2
+  | ty1 `eqType` ty2
+  = do return $ GenInst []
+              $ EvCoercible (EvCoercibleRefl ty1)
+
+  | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
+    Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
+    tc1 == tc2,
+    nominalArgsAgree tc1 tyArgs1 tyArgs2,
+    not safeMode || all (dataConsInScope rdr_env) (tyConsOfTyCon tc1)
+  = do -- Mark all used data constructors as used
+       when safeMode $ mapM_ (markDataConsAsUsed rdr_env) (tyConsOfTyCon tc1)
+       -- We want evidence for all type arguments of role R
+       arg_evs <- flip mapM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \(r,ta1,ta2) ->
+         case r of Nominal -> return (Nothing, EvCoercibleArgN ta1 {- == ta2, due to nominalArgsAgree -})
+                   Representational -> do
+                        ct_ev <- requestCoercible ta1 ta2
+                        return (freshGoal ct_ev, EvCoercibleArgR (getEvTerm ct_ev))
+                   Phantom -> do
+                        return (Nothing, EvCoercibleArgP ta1 ta2)
+       return $ GenInst (mapMaybe fst arg_evs)
+              $ EvCoercible (EvCoercibleTyCon tc1 (map snd arg_evs))
+
+  | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
+    Just (_, _, _) <- unwrapNewTyCon_maybe tc,
+    not (isRecursiveTyCon tc),
+    dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
+  = do markDataConsAsUsed rdr_env tc
+       let concTy = newTyConInstRhs tc tyArgs 
+       ct_ev <- requestCoercible concTy ty2
+       return $ GenInst (freshGoals [ct_ev])
+              $ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
+
+  | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
+    Just (_, _, _) <- unwrapNewTyCon_maybe tc,
+    not (isRecursiveTyCon tc),
+    dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
+  = do markDataConsAsUsed rdr_env tc
+       let concTy = newTyConInstRhs tc tyArgs 
+       ct_ev <- requestCoercible ty1 concTy
+       return $ GenInst (freshGoals [ct_ev])
+              $ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
+
+  | otherwise
+  = return NoInstance
+
+
+nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool
+nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2
+  where ok (r,t1,t2) = r /= Nominal || t1 `eqType` t2
+
+dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool
+dataConsInScope rdr_env tc = not hidden_data_cons
+  where
+    data_con_names = map dataConName (tyConDataCons tc)
+    hidden_data_cons = not (isWiredInName (tyConName tc)) &&
+                       (isAbstractTyCon tc || any not_in_scope data_con_names)
+    not_in_scope dc  = null (lookupGRE_Name rdr_env dc)
+
+markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
+markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
+  [ mkRdrQual (is_as (is_decl imp_spec)) occ
+  | dc <- tyConDataCons tc
+  , let dc_name = dataConName dc
+        occ  = nameOccName dc_name
+        gres = lookupGRE_Name rdr_env dc_name
+  , not (null gres)
+  , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
+
+requestCoercible :: TcType -> TcType -> TcS MaybeNew
+requestCoercible ty1 ty2 = newWantedEvVar (coercibleClass `mkClassPred` [ty1, ty2]) 
+
 \end{code}
 
+Note [Coercible Instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The class Coercible is special: There are no regular instances, and the user
+cannot even define them. Instead, the type checker will create instances and
+their evidence out of thin air, in getCoericbleInst. The following “instances”
+are present:
+
+ 1. instance Coercible a a
+    for any type a.
+ 2. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
+       Coercible (C t1_r  t2_r  ... t1_p  t2_p  ... t1_n t2_n ...)
+                 (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
+    for a type constructor C where
+     * the nominal type arguments are not changed,
+     * the phantom type arguments may change arbitrarily
+     * the representational type arguments are again Coercible
+    Furthermore in Safe Haskell code, we check that
+     * the data constructors of C are in scope and
+     * the data constructors of all type constructors used in the definition of C are in scope.
+       This is required as otherwise the previous check can be circumvented by
+       just adding a local data type around C.
+ 3. instance Coercible r b => Coercible (NT t1 t2 ...) b
+    instance Coercible a r => Coercible a (NT t1 t2 ...)
+    for a newtype constructor NT where
+     * NT is not recursive
+     * r is the concrete type of NT, instantiated with the arguments t1 t2 ... 
+     * the data constructors of NT are in scope.
+     
+These three shapes of instances correspond to the three constructors of
+EvCoercible (defined in EvEvidence). They are assembled here and turned to Core
+by dsEvTerm in DsBinds.
+
+
 Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Assume that we have an inert set that looks as follows:
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index 1d68ede3b7..677da1c88e 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -22,6 +22,7 @@ import TcSimplify ( simplifyTop )
 import TypeRep
 import TcType
 import TcMType
+import TysWiredIn ( coercibleClass )
 import Type
 import Unify( tcMatchTyX )
 import Kind
@@ -746,6 +747,9 @@ checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
 checkValidInstHead ctxt clas cls_args
   = do { dflags <- getDynFlags
 
+       ; checkTc (clas `notElem` abstractClasses)
+                 (instTypeErr clas cls_args abstract_class_msg)
+
            -- Check language restrictions; 
            -- but not for SPECIALISE isntance pragmas
        ; let ty_args = dropWhile isKind cls_args
@@ -796,6 +800,12 @@ checkValidInstHead ctxt clas cls_args
                 text "No parameters in the instance head." $$
                 text "Use -XNullaryTypeClasses if you want to allow this.")
 
+    abstract_class_msg =
+                text "The class is abstract, manual instances are not permitted."
+
+abstractClasses :: [ Class ]
+abstractClasses = [ coercibleClass ]
+
 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
 instTypeErr cls tys msg
   = hang (ptext (sLit "Illegal instance declaration for")