Merge branch 'master' of ssh://darcs.haskell.org/srv/darcs/ghc into encodingencoding

6 files changed, 252 insertions, 138 deletions

diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index b1c97cdf00..134dcfac2c 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -1,4 +1,3 @@
-
 {-# OPTIONS_GHC -O #-}
 -- We always optimise this, otherwise performance of a non-optimised
 -- compiler is severely affected
@@ -903,10 +902,11 @@ instance Binary IfaceType where
     put_ bh (IfaceTyConApp (IfaceAnyTc k) []) 	       = do { putByte bh 17; put_ bh k }
 
 	-- Generic cases
-
     put_ bh (IfaceTyConApp (IfaceTc tc) tys) = do { putByte bh 18; put_ bh tc; put_ bh tys }
     put_ bh (IfaceTyConApp tc tys) 	     = do { putByte bh 19; put_ bh tc; put_ bh tys }
 
+    put_ bh (IfaceCoConApp cc tys) = do { putByte bh 20; put_ bh cc; put_ bh tys }
+
     get bh = do
 	    h <- getByte bh
 	    case h of
@@ -939,11 +939,11 @@ instance Binary IfaceType where
               17 -> do { k <- get bh; return (IfaceTyConApp (IfaceAnyTc k) []) }
 
 	      18 -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp (IfaceTc tc) tys) }
-	      _  -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp tc tys) }
+	      19  -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp tc tys) }
+	      _  -> do { cc <- get bh; tys <- get bh; return (IfaceCoConApp cc tys) }
 
 instance Binary IfaceTyCon where
 	-- Int,Char,Bool can't show up here because they can't not be saturated
-
    put_ bh IfaceIntTc  	      = putByte bh 1
    put_ bh IfaceBoolTc 	      = putByte bh 2
    put_ bh IfaceCharTc 	      = putByte bh 3
@@ -954,9 +954,9 @@ instance Binary IfaceTyCon where
    put_ bh IfaceUnliftedTypeKindTc = putByte bh 8
    put_ bh IfaceUbxTupleKindTc     = putByte bh 9
    put_ bh IfaceArgTypeKindTc      = putByte bh 10
-   put_ bh (IfaceTupTc bx ar) = do { putByte bh 11; put_ bh bx; put_ bh ar }
-   put_ bh (IfaceTc ext)      = do { putByte bh 12; put_ bh ext }
-   put_ bh (IfaceAnyTc k)     = do { putByte bh 13; put_ bh k }
+   put_ bh (IfaceTupTc bx ar)  = do { putByte bh 11; put_ bh bx; put_ bh ar }
+   put_ bh (IfaceTc ext)       = do { putByte bh 12; put_ bh ext }
+   put_ bh (IfaceAnyTc k)      = do { putByte bh 13; put_ bh k }
 
    get bh = do
 	h <- getByte bh
@@ -973,7 +973,27 @@ instance Binary IfaceTyCon where
           10 -> return IfaceArgTypeKindTc
 	  11 -> do { bx <- get bh; ar <- get bh; return (IfaceTupTc bx ar) }
 	  12 -> do { ext <- get bh; return (IfaceTc ext) }
-	  _  -> do { k <- get bh; return (IfaceAnyTc k) }
+	  _ -> do { k <- get bh; return (IfaceAnyTc k) }
+
+instance Binary IfaceCoCon where
+   put_ bh (IfaceCoAx n)       = do { putByte bh 0; put_ bh n }
+   put_ bh IfaceReflCo         = putByte bh 1
+   put_ bh IfaceUnsafeCo       = putByte bh 2
+   put_ bh IfaceSymCo          = putByte bh 3
+   put_ bh IfaceTransCo        = putByte bh 4
+   put_ bh IfaceInstCo         = putByte bh 5
+   put_ bh (IfaceNthCo d)      = do { putByte bh 6; put_ bh d }
+  
+   get bh = do
+	h <- getByte bh
+	case h of
+          0 -> do { n <- get bh; return (IfaceCoAx n) }
+	  1 -> return IfaceReflCo 
+	  2 -> return IfaceUnsafeCo
+	  3 -> return IfaceSymCo
+	  4 -> return IfaceTransCo
+	  5 -> return IfaceInstCo
+          _ -> do { d <- get bh; return (IfaceNthCo d) }
 
 instance Binary IfacePredType where
     put_ bh (IfaceClassP aa ab) = do
@@ -1013,50 +1033,50 @@ instance Binary IfaceExpr where
     put_ bh (IfaceType ab) = do
 	    putByte bh 1
 	    put_ bh ab
-    put_ bh (IfaceTuple ac ad) = do
+    put_ bh (IfaceCo ab) = do
 	    putByte bh 2
+	    put_ bh ab
+    put_ bh (IfaceTuple ac ad) = do
+	    putByte bh 3
 	    put_ bh ac
 	    put_ bh ad
     put_ bh (IfaceLam ae af) = do
-	    putByte bh 3
+	    putByte bh 4
 	    put_ bh ae
 	    put_ bh af
     put_ bh (IfaceApp ag ah) = do
-	    putByte bh 4
+	    putByte bh 5
 	    put_ bh ag
 	    put_ bh ah
--- gaw 2004
-    put_ bh (IfaceCase ai aj al ak) = do
-	    putByte bh 5
+    put_ bh (IfaceCase ai aj ak) = do
+	    putByte bh 6
 	    put_ bh ai
 	    put_ bh aj
--- gaw 2004
-            put_ bh al
 	    put_ bh ak
     put_ bh (IfaceLet al am) = do
-	    putByte bh 6
+	    putByte bh 7
 	    put_ bh al
 	    put_ bh am
     put_ bh (IfaceNote an ao) = do
-	    putByte bh 7
+	    putByte bh 8
 	    put_ bh an
 	    put_ bh ao
     put_ bh (IfaceLit ap) = do
-	    putByte bh 8
+	    putByte bh 9
 	    put_ bh ap
     put_ bh (IfaceFCall as at) = do
-	    putByte bh 9
+	    putByte bh 10
 	    put_ bh as
 	    put_ bh at
     put_ bh (IfaceExt aa) = do
-	    putByte bh 10
+	    putByte bh 11
 	    put_ bh aa
     put_ bh (IfaceCast ie ico) = do
-            putByte bh 11
+            putByte bh 12
             put_ bh ie
             put_ bh ico
     put_ bh (IfaceTick m ix) = do
-            putByte bh 12
+            putByte bh 13
             put_ bh m
             put_ bh ix
     get bh = do
@@ -1066,39 +1086,38 @@ instance Binary IfaceExpr where
 		      return (IfaceLcl aa)
 	      1 -> do ab <- get bh
 		      return (IfaceType ab)
-	      2 -> do ac <- get bh
+	      2 -> do ab <- get bh
+		      return (IfaceCo ab)
+	      3 -> do ac <- get bh
 		      ad <- get bh
 		      return (IfaceTuple ac ad)
-	      3 -> do ae <- get bh
+	      4 -> do ae <- get bh
 		      af <- get bh
 		      return (IfaceLam ae af)
-	      4 -> do ag <- get bh
+	      5 -> do ag <- get bh
 		      ah <- get bh
 		      return (IfaceApp ag ah)
-	      5 -> do ai <- get bh
+	      6 -> do ai <- get bh
 		      aj <- get bh
--- gaw 2004
-                      al <- get bh                   
 		      ak <- get bh
--- gaw 2004
-		      return (IfaceCase ai aj al ak)
-	      6 -> do al <- get bh
+		      return (IfaceCase ai aj ak)
+	      7 -> do al <- get bh
 		      am <- get bh
 		      return (IfaceLet al am)
-	      7 -> do an <- get bh
+	      8 -> do an <- get bh
 		      ao <- get bh
 		      return (IfaceNote an ao)
-	      8 -> do ap <- get bh
+	      9 -> do ap <- get bh
 		      return (IfaceLit ap)
-	      9 -> do as <- get bh
-		      at <- get bh
-		      return (IfaceFCall as at)
-	      10 -> do aa <- get bh
+	      10 -> do as <- get bh
+		       at <- get bh
+		       return (IfaceFCall as at)
+	      11 -> do aa <- get bh
 		       return (IfaceExt aa)
-              11 -> do ie <- get bh
+              12 -> do ie <- get bh
                        ico <- get bh
                        return (IfaceCast ie ico)
-              12 -> do m <- get bh
+              13 -> do m <- get bh
                        ix <- get bh
                        return (IfaceTick m ix)
               _ -> panic ("get IfaceExpr " ++ show h)
diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index e71eefe339..d30352cfa1 100644
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -100,8 +100,8 @@ mkFamInstParentInfo :: Name -> [TyVar]
 mkFamInstParentInfo tc_name tvs (family, instTys) rep_tycon
   = do { -- Create the coercion
        ; co_tycon_name <- newImplicitBinder tc_name mkInstTyCoOcc
-       ; let co_tycon = mkFamInstCoercion co_tycon_name tvs
-                                        family instTys rep_tycon
+       ; let co_tycon = mkFamInstCo co_tycon_name tvs
+                                    family instTys rep_tycon
        ; return $ FamInstTyCon family instTys co_tycon }
     
 ------------------------------------------------------
@@ -127,23 +127,15 @@ mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
 --   because the latter is part of a knot, whereas the former is not.
 mkNewTyConRhs tycon_name tycon con 
   = do	{ co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc
-	; let co_tycon = mkNewTypeCoercion co_tycon_name tycon etad_tvs etad_rhs
-              cocon_maybe | all_coercions || isRecursiveTyCon tycon 
-		          = Just co_tycon
-                	  | otherwise              
-                	  = Nothing
-	; traceIf (text "mkNewTyConRhs" <+> ppr cocon_maybe)
+	; let co_tycon = mkNewTypeCo co_tycon_name tycon etad_tvs etad_rhs
+	; traceIf (text "mkNewTyConRhs" <+> ppr co_tycon)
 	; return (NewTyCon { data_con    = con, 
 		       	     nt_rhs      = rhs_ty,
 		       	     nt_etad_rhs = (etad_tvs, etad_rhs),
- 		       	     nt_co 	 = cocon_maybe } ) }
+ 		       	     nt_co 	 = co_tycon } ) }
                              -- Coreview looks through newtypes with a Nothing
                              -- for nt_co, or uses explicit coercions otherwise
   where
-        -- If all_coercions is True then we use coercions for all newtypes
-        -- otherwise we use coercions for recursive newtypes and look through
-        -- non-recursive newtypes
-    all_coercions = True
     tvs    = tyConTyVars tycon
     inst_con_ty = applyTys (dataConUserType con) (mkTyVarTys tvs)
     rhs_ty = ASSERT( isFunTy inst_con_ty ) funArgTy inst_con_ty
@@ -156,7 +148,7 @@ mkNewTyConRhs tycon_name tycon con
   	-- has a single argument (Foo a) that is a *type class*, so
 	-- dataConInstOrigArgTys returns [].
 
-    etad_tvs :: [TyVar]	-- Matched lazily, so that mkNewTypeCoercion can
+    etad_tvs :: [TyVar]	-- Matched lazily, so that mkNewTypeCo can
     etad_rhs :: Type	-- return a TyCon without pulling on rhs_ty
 			-- See Note [Tricky iface loop] in LoadIface
     (etad_tvs, etad_rhs) = eta_reduce (reverse tvs) rhs_ty
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 950021e986..ef0ef5c5f0 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -235,12 +235,13 @@ data IfaceExpr
   = IfaceLcl    IfLclName
   | IfaceExt    IfExtName
   | IfaceType   IfaceType
-  | IfaceTuple  Boxity [IfaceExpr]              -- Saturated; type arguments omitted
-  | IfaceLam    IfaceBndr IfaceExpr
-  | IfaceApp    IfaceExpr IfaceExpr
-  | IfaceCase   IfaceExpr IfLclName IfaceType [IfaceAlt]
-  | IfaceLet    IfaceBinding  IfaceExpr
-  | IfaceNote   IfaceNote IfaceExpr
+  | IfaceCo     IfaceType		-- We re-use IfaceType for coercions
+  | IfaceTuple 	Boxity [IfaceExpr]	-- Saturated; type arguments omitted
+  | IfaceLam 	IfaceBndr IfaceExpr
+  | IfaceApp 	IfaceExpr IfaceExpr
+  | IfaceCase	IfaceExpr IfLclName [IfaceAlt]
+  | IfaceLet	IfaceBinding  IfaceExpr
+  | IfaceNote	IfaceNote IfaceExpr
   | IfaceCast   IfaceExpr IfaceCoercion
   | IfaceLit    Literal
   | IfaceFCall  ForeignCall IfaceType
@@ -600,6 +601,7 @@ pprIfaceExpr _       (IfaceLit l)       = ppr l
 pprIfaceExpr _       (IfaceFCall cc ty) = braces (ppr cc <+> ppr ty)
 pprIfaceExpr _       (IfaceTick m ix)   = braces (text "tick" <+> ppr m <+> ppr ix)
 pprIfaceExpr _       (IfaceType ty)     = char '@' <+> pprParendIfaceType ty
+pprIfaceExpr _       (IfaceCo co)       = text "@~" <+> pprParendIfaceType co
 
 pprIfaceExpr add_par app@(IfaceApp _ _) = add_par (pprIfaceApp app [])
 pprIfaceExpr _       (IfaceTuple c as)  = tupleParens c (interpp'SP as)
@@ -612,17 +614,17 @@ pprIfaceExpr add_par i@(IfaceLam _ _)
     collect bs (IfaceLam b e) = collect (b:bs) e
     collect bs e              = (reverse bs, e)
 
-pprIfaceExpr add_par (IfaceCase scrut bndr ty [(con, bs, rhs)])
-  = add_par (sep [ptext (sLit "case") <+> char '@' <+> pprParendIfaceType ty
-                        <+> pprIfaceExpr noParens scrut <+> ptext (sLit "of")
-                        <+> ppr bndr <+> char '{' <+> ppr_con_bs con bs <+> arrow,
-                  pprIfaceExpr noParens rhs <+> char '}'])
+pprIfaceExpr add_par (IfaceCase scrut bndr [(con, bs, rhs)])
+  = add_par (sep [ptext (sLit "case") 
+			<+> pprIfaceExpr noParens scrut <+> ptext (sLit "of") 
+			<+> ppr bndr <+> char '{' <+> ppr_con_bs con bs <+> arrow,
+  		  pprIfaceExpr noParens rhs <+> char '}'])
 
-pprIfaceExpr add_par (IfaceCase scrut bndr ty alts)
-  = add_par (sep [ptext (sLit "case") <+> char '@' <+> pprParendIfaceType ty
-                        <+> pprIfaceExpr noParens scrut <+> ptext (sLit "of")
-                        <+> ppr bndr <+> char '{',
-                  nest 2 (sep (map ppr_alt alts)) <+> char '}'])
+pprIfaceExpr add_par (IfaceCase scrut bndr alts)
+  = add_par (sep [ptext (sLit "case") 
+		 	<+> pprIfaceExpr noParens scrut <+> ptext (sLit "of") 
+			<+> ppr bndr <+> char '{',
+  		  nest 2 (sep (map ppr_alt alts)) <+> char '}'])
 
 pprIfaceExpr _       (IfaceCast expr co)
   = sep [pprParendIfaceExpr expr,
@@ -798,6 +800,8 @@ freeNamesIfType (IfaceTyConApp tc ts) =
 freeNamesIfType (IfaceForAllTy tv t)  =
    freeNamesIfTvBndr tv &&& freeNamesIfType t
 freeNamesIfType (IfaceFunTy s t)      = freeNamesIfType s &&& freeNamesIfType t
+freeNamesIfType (IfaceCoConApp tc ts) = 
+   freeNamesIfCo tc &&& fnList freeNamesIfType ts
 
 freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
 freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
@@ -840,16 +844,16 @@ freeNamesIfExpr :: IfaceExpr -> NameSet
 freeNamesIfExpr (IfaceExt v)      = unitNameSet v
 freeNamesIfExpr (IfaceFCall _ ty) = freeNamesIfType ty
 freeNamesIfExpr (IfaceType ty)    = freeNamesIfType ty
+freeNamesIfExpr (IfaceCo co)      = freeNamesIfType co
 freeNamesIfExpr (IfaceTuple _ as) = fnList freeNamesIfExpr as
 freeNamesIfExpr (IfaceLam b body) = freeNamesIfBndr b &&& freeNamesIfExpr body
 freeNamesIfExpr (IfaceApp f a)    = freeNamesIfExpr f &&& freeNamesIfExpr a
 freeNamesIfExpr (IfaceCast e co)  = freeNamesIfExpr e &&& freeNamesIfType co
 freeNamesIfExpr (IfaceNote _n r)  = freeNamesIfExpr r
 
-freeNamesIfExpr (IfaceCase s _ ty alts)
-  = freeNamesIfExpr s
+freeNamesIfExpr (IfaceCase s _ alts)
+  = freeNamesIfExpr s 
     &&& fnList fn_alt alts &&& fn_cons alts
-    &&& freeNamesIfType ty
   where
     fn_alt (_con,_bs,r) = freeNamesIfExpr r
 
@@ -875,6 +879,10 @@ freeNamesIfTc (IfaceTc tc) = unitNameSet tc
 -- ToDo: shouldn't we include IfaceIntTc & co.?
 freeNamesIfTc _ = emptyNameSet
 
+freeNamesIfCo :: IfaceCoCon -> NameSet
+freeNamesIfCo (IfaceCoAx tc) = unitNameSet tc
+freeNamesIfCo _ = emptyNameSet
+
 freeNamesIfRule :: IfaceRule -> NameSet
 freeNamesIfRule (IfaceRule { ifRuleBndrs = bs, ifRuleHead = f
                            , ifRuleArgs = es, ifRuleRhs = rhs })
diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs
index c97e16eef2..7817b423ae 100644
--- a/compiler/iface/IfaceType.lhs
+++ b/compiler/iface/IfaceType.lhs
@@ -9,15 +9,18 @@ This module defines interface types and binders
 module IfaceType (
 	IfExtName, IfLclName,
 
-        IfaceType(..), IfaceKind, IfacePredType(..), IfaceTyCon(..),
+        IfaceType(..), IfaceKind, IfacePredType(..), IfaceTyCon(..), IfaceCoCon(..),
 	IfaceContext, IfaceBndr(..), IfaceTvBndr, IfaceIdBndr, IfaceCoercion,
 	ifaceTyConName,
 
 	-- Conversion from Type -> IfaceType
-	toIfaceType, toIfacePred, toIfaceContext, 
+        toIfaceType, toIfaceContext,
 	toIfaceBndr, toIfaceIdBndr, toIfaceTvBndrs, 
 	toIfaceTyCon, toIfaceTyCon_name,
 
+        -- Conversion from Coercion -> IfaceType
+        coToIfaceType,
+
 	-- Printing
 	pprIfaceType, pprParendIfaceType, pprIfaceContext, 
 	pprIfaceIdBndr, pprIfaceTvBndr, pprIfaceTvBndrs, pprIfaceBndrs,
@@ -25,11 +28,13 @@ module IfaceType (
 
     ) where
 
-import TypeRep
+import Coercion
+import TypeRep hiding( maybeParen )
 import TyCon
 import Id
 import Var
 import TysWiredIn
+import TysPrim
 import Name
 import BasicTypes
 import Outputable
@@ -59,14 +64,15 @@ type IfaceTvBndr  = (IfLclName, IfaceKind)
 type IfaceKind     = IfaceType
 type IfaceCoercion = IfaceType
 
-data IfaceType
-  = IfaceTyVar    IfLclName			-- Type variable only, not tycon
+data IfaceType	   -- A kind of universal type, used for types, kinds, and coercions
+  = IfaceTyVar    IfLclName			-- Type/coercion variable only, not tycon
   | IfaceAppTy    IfaceType IfaceType
+  | IfaceFunTy    IfaceType IfaceType
   | IfaceForAllTy IfaceTvBndr IfaceType
   | IfacePredTy   IfacePredType
-  | IfaceTyConApp IfaceTyCon [IfaceType]	-- Not necessarily saturated
-						-- Includes newtypes, synonyms, tuples
-  | IfaceFunTy  IfaceType IfaceType
+  | IfaceTyConApp IfaceTyCon [IfaceType]  -- Not necessarily saturated
+					  -- Includes newtypes, synonyms, tuples
+  | IfaceCoConApp IfaceCoCon [IfaceType]  -- Always saturated
 
 data IfacePredType 	-- NewTypes are handled as ordinary TyConApps
   = IfaceClassP IfExtName [IfaceType]
@@ -75,18 +81,28 @@ data IfacePredType 	-- NewTypes are handled as ordinary TyConApps
 
 type IfaceContext = [IfacePredType]
 
-data IfaceTyCon 	-- Abbreviations for common tycons with known names
+data IfaceTyCon 	-- Encodes type consructors, kind constructors
+     			-- coercion constructors, the lot
   = IfaceTc IfExtName	-- The common case
   | IfaceIntTc | IfaceBoolTc | IfaceCharTc
   | IfaceListTc | IfacePArrTc
   | IfaceTupTc Boxity Arity 
   | IfaceAnyTc IfaceKind     -- Used for AnyTyCon (see Note [Any Types] in TysPrim)
     	       		     -- other than 'Any :: *' itself
+ 
+  -- Kind constructors
   | IfaceLiftedTypeKindTc | IfaceOpenTypeKindTc | IfaceUnliftedTypeKindTc
   | IfaceUbxTupleKindTc | IfaceArgTypeKindTc 
 
-ifaceTyConName :: IfaceTyCon -> IfExtName
-ifaceTyConName IfaceIntTc  	       = intTyConName
+  -- Coercion constructors
+data IfaceCoCon
+  = IfaceCoAx IfExtName
+  | IfaceReflCo    | IfaceUnsafeCo  | IfaceSymCo
+  | IfaceTransCo   | IfaceInstCo
+  | IfaceNthCo Int
+
+ifaceTyConName :: IfaceTyCon -> Name
+ifaceTyConName IfaceIntTc              = intTyConName
 ifaceTyConName IfaceBoolTc 	       = boolTyConName
 ifaceTyConName IfaceCharTc 	       = charTyConName
 ifaceTyConName IfaceListTc 	       = listTyConName
@@ -208,6 +224,10 @@ ppr_ty _         (IfaceTyVar tyvar)     = ppr tyvar
 ppr_ty ctxt_prec (IfaceTyConApp tc tys) = ppr_tc_app ctxt_prec tc tys
 ppr_ty _         (IfacePredTy st)       = ppr st
 
+ppr_ty ctxt_prec (IfaceCoConApp tc tys) 
+  = maybeParen ctxt_prec tYCON_PREC 
+	       (sep [ppr tc, nest 4 (sep (map pprParendIfaceType tys))])
+
 	-- Function types
 ppr_ty ctxt_prec (IfaceFunTy ty1 ty2)
   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
@@ -268,6 +288,15 @@ instance Outputable IfaceTyCon where
 			     -- so we fake it.  It's only for debug printing!
   ppr other_tc       = ppr (ifaceTyConName other_tc)
 
+instance Outputable IfaceCoCon where
+  ppr (IfaceCoAx n)  = ppr n
+  ppr IfaceReflCo    = ptext (sLit "Refl")
+  ppr IfaceUnsafeCo  = ptext (sLit "Unsafe")
+  ppr IfaceSymCo     = ptext (sLit "Sym")
+  ppr IfaceTransCo   = ptext (sLit "Trans")
+  ppr IfaceInstCo    = ptext (sLit "Inst")
+  ppr (IfaceNthCo d) = ptext (sLit "Nth:") <> int d
+
 -------------------
 pprIfaceContext :: IfaceContext -> SDoc
 -- Prints "(C a, D b) =>", including the arrow
@@ -309,18 +338,15 @@ toIfaceKind = toIfaceType
 ---------------------
 toIfaceType :: Type -> IfaceType
 -- Synonyms are retained in the interface type
-toIfaceType (TyVarTy tv) =
-  IfaceTyVar (occNameFS (getOccName tv))
-toIfaceType (AppTy t1 t2) =
-  IfaceAppTy (toIfaceType t1) (toIfaceType t2)
-toIfaceType (FunTy t1 t2) =
-  IfaceFunTy (toIfaceType t1) (toIfaceType t2)
-toIfaceType (TyConApp tc tys) =
-  IfaceTyConApp (toIfaceTyCon tc) (toIfaceTypes tys)
-toIfaceType (ForAllTy tv t) =
-  IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType t)
-toIfaceType (PredTy st) =
-  IfacePredTy (toIfacePred st)
+toIfaceType (TyVarTy tv)      = IfaceTyVar (toIfaceTyCoVar tv)
+toIfaceType (AppTy t1 t2)     = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
+toIfaceType (FunTy t1 t2)     = IfaceFunTy (toIfaceType t1) (toIfaceType t2)
+toIfaceType (TyConApp tc tys) = IfaceTyConApp (toIfaceTyCon tc) (toIfaceTypes tys)
+toIfaceType (ForAllTy tv t)   = IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType t)
+toIfaceType (PredTy st)       = IfacePredTy (toIfacePred toIfaceType st)
+
+toIfaceTyCoVar :: TyCoVar -> FastString
+toIfaceTyCoVar = occNameFS . getOccName
 
 ----------------
 -- A little bit of (perhaps optional) trickiness here.  When
@@ -364,16 +390,39 @@ toIfaceTypes :: [Type] -> [IfaceType]
 toIfaceTypes ts = map toIfaceType ts
 
 ----------------
-toIfacePred :: PredType -> IfacePredType
-toIfacePred (ClassP cls ts) = 
-  IfaceClassP (getName cls) (toIfaceTypes ts)
-toIfacePred (IParam ip t) = 
-  IfaceIParam (mapIPName getOccName ip) (toIfaceType t)
-toIfacePred (EqPred ty1 ty2) =
-  IfaceEqPred (toIfaceType ty1) (toIfaceType ty2)
+toIfacePred :: (a -> IfaceType) -> Pred a -> IfacePredType
+toIfacePred to (ClassP cls ts)  = IfaceClassP (getName cls) (map to ts)
+toIfacePred to (IParam ip t)    = IfaceIParam (mapIPName getOccName ip) (to t)
+toIfacePred to (EqPred ty1 ty2) =  IfaceEqPred (to ty1) (to ty2)
 
 ----------------
 toIfaceContext :: ThetaType -> IfaceContext
-toIfaceContext cs = map toIfacePred cs
+toIfaceContext cs = map (toIfacePred toIfaceType) cs
+
+----------------
+coToIfaceType :: Coercion -> IfaceType
+coToIfaceType (Refl ty)             = IfaceCoConApp IfaceReflCo [toIfaceType ty]
+coToIfaceType (TyConAppCo tc cos)   = IfaceTyConApp (toIfaceTyCon tc) 
+                                                    (map coToIfaceType cos)
+coToIfaceType (AppCo co1 co2)       = IfaceAppTy    (coToIfaceType co1) 
+                                                    (coToIfaceType co2)
+coToIfaceType (ForAllCo v co)       = IfaceForAllTy (toIfaceTvBndr v) 
+                                                    (coToIfaceType co)
+coToIfaceType (CoVarCo cv)          = IfaceTyVar  (toIfaceTyCoVar cv)
+coToIfaceType (AxiomInstCo con cos) = IfaceCoConApp (IfaceCoAx (coAxiomName con))
+                                                    (map coToIfaceType cos)
+coToIfaceType (UnsafeCo ty1 ty2)    = IfaceCoConApp IfaceUnsafeCo 
+                                                    [ toIfaceType ty1
+                                                    , toIfaceType ty2 ]
+coToIfaceType (SymCo co)            = IfaceCoConApp IfaceSymCo 
+                                                    [ coToIfaceType co ]
+coToIfaceType (TransCo co1 co2)     = IfaceCoConApp IfaceTransCo
+                                                    [ coToIfaceType co1
+                                                    , coToIfaceType co2 ]
+coToIfaceType (NthCo d co)          = IfaceCoConApp (IfaceNthCo d)
+                                                    [ coToIfaceType co ]
+coToIfaceType (InstCo co ty)        = IfaceCoConApp IfaceInstCo 
+                                                    [ coToIfaceType co
+                                                    , toIfaceType ty ]
 \end{code}
 
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index c3270062c2..88dbfa3664 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -59,10 +59,10 @@ import Annotations
 import CoreSyn
 import CoreFVs
 import Class
+import Kind
 import TyCon
 import DataCon
 import Type
-import Coercion
 import TcType
 import InstEnv
 import FamInstEnv
@@ -1387,14 +1387,16 @@ tyThingToIfaceDecl (ATyCon tycon)
 	= IfCon   { ifConOcc   	 = getOccName (dataConName data_con),
 		    ifConInfix 	 = dataConIsInfix data_con,
 		    ifConWrapper = isJust (dataConWrapId_maybe data_con),
-		    ifConUnivTvs = toIfaceTvBndrs (dataConUnivTyVars data_con),
-		    ifConExTvs   = toIfaceTvBndrs (dataConExTyVars data_con),
-		    ifConEqSpec  = to_eq_spec (dataConEqSpec data_con),
-		    ifConCtxt    = toIfaceContext (dataConEqTheta data_con ++ dataConDictTheta data_con),
-		    ifConArgTys  = map toIfaceType (dataConOrigArgTys data_con),
+		    ifConUnivTvs = toIfaceTvBndrs univ_tvs,
+		    ifConExTvs   = toIfaceTvBndrs ex_tvs,
+		    ifConEqSpec  = to_eq_spec eq_spec,
+		    ifConCtxt    = toIfaceContext theta,
+		    ifConArgTys  = map toIfaceType arg_tys,
 		    ifConFields  = map getOccName 
 				       (dataConFieldLabels data_con),
 		    ifConStricts = dataConStrictMarks data_con }
+        where
+          (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
 
     to_eq_spec spec = [(getOccName tv, toIfaceType ty) | (tv,ty) <- spec]
 
@@ -1402,6 +1404,8 @@ tyThingToIfaceDecl (ATyCon tycon)
     famInstToIface (Just (famTyCon, instTys)) = 
       Just (toIfaceTyCon famTyCon, map toIfaceType instTys)
 
+tyThingToIfaceDecl c@(ACoAxiom _) = pprPanic "tyThingToIfaceDecl (ACoCon _)" (ppr c)
+
 tyThingToIfaceDecl (ADataCon dc)
  = pprPanic "toIfaceDecl" (ppr dc)	-- Should be trimmed out earlier
 
@@ -1566,6 +1570,8 @@ coreRuleToIfaceRule mod rule@(Rule { ru_name = name, ru_fn = fn,
 	-- construct the same ru_rough field as we have right now;
 	-- see tcIfaceRule
     do_arg (Type ty) = IfaceType (toIfaceType (deNoteType ty))
+    do_arg (Coercion co) = IfaceType (coToIfaceType co)
+                           
     do_arg arg       = toIfaceExpr arg
 
 	-- Compute orphanhood.  See Note [Orphans] in IfaceSyn
@@ -1585,15 +1591,16 @@ bogusIfaceRule id_name
 
 ---------------------
 toIfaceExpr :: CoreExpr -> IfaceExpr
-toIfaceExpr (Var v)       = toIfaceVar v
-toIfaceExpr (Lit l)       = IfaceLit l
-toIfaceExpr (Type ty)     = IfaceType (toIfaceType ty)
-toIfaceExpr (Lam x b)     = IfaceLam (toIfaceBndr x) (toIfaceExpr b)
-toIfaceExpr (App f a)     = toIfaceApp f [a]
-toIfaceExpr (Case s x ty as) = IfaceCase (toIfaceExpr s) (getFS x) (toIfaceType ty) (map toIfaceAlt as)
-toIfaceExpr (Let b e)     = IfaceLet (toIfaceBind b) (toIfaceExpr e)
-toIfaceExpr (Cast e co)   = IfaceCast (toIfaceExpr e) (toIfaceType co)
-toIfaceExpr (Note n e)    = IfaceNote (toIfaceNote n) (toIfaceExpr e)
+toIfaceExpr (Var v)         = toIfaceVar v
+toIfaceExpr (Lit l)         = IfaceLit l
+toIfaceExpr (Type ty)       = IfaceType (toIfaceType ty)
+toIfaceExpr (Coercion co)   = IfaceCo   (coToIfaceType co)
+toIfaceExpr (Lam x b)       = IfaceLam (toIfaceBndr x) (toIfaceExpr b)
+toIfaceExpr (App f a)       = toIfaceApp f [a]
+toIfaceExpr (Case s x _ as) = IfaceCase (toIfaceExpr s) (getFS x) (map toIfaceAlt as)
+toIfaceExpr (Let b e)       = IfaceLet (toIfaceBind b) (toIfaceExpr e)
+toIfaceExpr (Cast e co)     = IfaceCast (toIfaceExpr e) (coToIfaceType co)
+toIfaceExpr (Note n e)      = IfaceNote (toIfaceNote n) (toIfaceExpr e)
 
 ---------------------
 toIfaceNote :: Note -> IfaceNote
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 8dccc72b37..9e663a8e7d 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -21,6 +21,7 @@ import BuildTyCl
 import TcRnMonad
 import TcType
 import Type
+import Coercion
 import TypeRep
 import HscTypes
 import Annotations
@@ -39,7 +40,6 @@ import TyCon
 import DataCon
 import TysWiredIn
 import TysPrim		( anyTyConOfKind )
-import Var              ( Var, TyVar )
 import BasicTypes	( Arity, nonRuleLoopBreaker )
 import qualified Var
 import VarEnv
@@ -791,20 +791,56 @@ tcIfaceType (IfaceAppTy t1 t2)    = do { t1' <- tcIfaceType t1; t2' <- tcIfaceTy
 tcIfaceType (IfaceFunTy t1 t2)    = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2; return (FunTy t1' t2') }
 tcIfaceType (IfaceTyConApp tc ts) = do { tc' <- tcIfaceTyCon tc; ts' <- tcIfaceTypes ts; return (mkTyConApp tc' ts') }
 tcIfaceType (IfaceForAllTy tv t)  = bindIfaceTyVar tv $ \ tv' -> do { t' <- tcIfaceType t; return (ForAllTy tv' t') }
-tcIfaceType (IfacePredTy st)      = do { st' <- tcIfacePredType st; return (PredTy st') }
+tcIfaceType (IfacePredTy st)      = do { st' <- tcIfacePred tcIfaceType st; return (PredTy st') }
+tcIfaceType t@(IfaceCoConApp {})  = pprPanic "tcIfaceType" (ppr t)
 
 tcIfaceTypes :: [IfaceType] -> IfL [Type]
 tcIfaceTypes tys = mapM tcIfaceType tys
 
 -----------------------------------------
-tcIfacePredType :: IfacePredType -> IfL PredType
-tcIfacePredType (IfaceClassP cls ts) = do { cls' <- tcIfaceClass cls; ts' <- tcIfaceTypes ts; return (ClassP cls' ts') }
-tcIfacePredType (IfaceIParam ip t)   = do { ip' <- newIPName ip; t' <- tcIfaceType t; return (IParam ip' t') }
-tcIfacePredType (IfaceEqPred t1 t2)  = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2; return (EqPred t1' t2') }
+tcIfacePred :: (IfaceType -> IfL a) -> IfacePredType -> IfL (Pred a)
+tcIfacePred tc (IfaceClassP cls ts)
+  = do { cls' <- tcIfaceClass cls; ts' <- mapM tc ts; return (ClassP cls' ts') }
+tcIfacePred tc (IfaceIParam ip t)
+  = do { ip' <- newIPName ip; t' <- tc t; return (IParam ip' t') }
+tcIfacePred tc (IfaceEqPred t1 t2)
+  = do { t1' <- tc t1; t2' <- tc t2; return (EqPred t1' t2') }
 
 -----------------------------------------
 tcIfaceCtxt :: IfaceContext -> IfL ThetaType
-tcIfaceCtxt sts = mapM tcIfacePredType sts
+tcIfaceCtxt sts = mapM (tcIfacePred tcIfaceType) sts
+\end{code}
+
+%************************************************************************
+%*									*
+			Coercions
+%*									*
+%************************************************************************
+
+\begin{code}
+tcIfaceCo :: IfaceType -> IfL Coercion
+tcIfaceCo (IfaceTyVar n)        = mkCoVarCo <$> tcIfaceCoVar n
+tcIfaceCo (IfaceAppTy t1 t2)    = mkAppCo <$> tcIfaceCo t1 <*> tcIfaceCo t2
+tcIfaceCo (IfaceFunTy t1 t2)    = mkFunCo <$> tcIfaceCo t1 <*> tcIfaceCo t2
+tcIfaceCo (IfaceTyConApp tc ts) = mkTyConAppCo <$> tcIfaceTyCon tc <*> mapM tcIfaceCo ts
+tcIfaceCo (IfaceCoConApp tc ts) = tcIfaceCoApp tc ts
+tcIfaceCo (IfaceForAllTy tv t)  = bindIfaceTyVar tv $ \ tv' ->
+                                  mkForAllCo tv' <$> tcIfaceCo t
+-- tcIfaceCo (IfacePredTy co)      = mkPredCo <$> tcIfacePred tcIfaceCo co
+tcIfaceCo (IfacePredTy _)      = panic "tcIfaceCo"
+
+tcIfaceCoApp :: IfaceCoCon -> [IfaceType] -> IfL Coercion
+tcIfaceCoApp IfaceReflCo    [t]     = Refl         <$> tcIfaceType t
+tcIfaceCoApp (IfaceCoAx n)  ts      = AxiomInstCo  <$> tcIfaceCoAxiom n <*> mapM tcIfaceCo ts
+tcIfaceCoApp IfaceUnsafeCo  [t1,t2] = UnsafeCo     <$> tcIfaceType t1 <*> tcIfaceType t2
+tcIfaceCoApp IfaceSymCo     [t]     = SymCo        <$> tcIfaceCo t
+tcIfaceCoApp IfaceTransCo   [t1,t2] = TransCo      <$> tcIfaceCo t1 <*> tcIfaceCo t2
+tcIfaceCoApp IfaceInstCo    [t1,t2] = InstCo       <$> tcIfaceCo t1 <*> tcIfaceType t2
+tcIfaceCoApp (IfaceNthCo d) [t]     = NthCo d      <$> tcIfaceCo t
+tcIfaceCoApp cc ts = pprPanic "toIfaceCoApp" (ppr cc <+> ppr ts)
+
+tcIfaceCoVar :: FastString -> IfL CoVar
+tcIfaceCoVar = tcIfaceLclId
 \end{code}
 
 
@@ -819,6 +855,12 @@ tcIfaceExpr :: IfaceExpr -> IfL CoreExpr
 tcIfaceExpr (IfaceType ty)
   = Type <$> tcIfaceType ty
 
+tcIfaceExpr (IfaceCo co)
+  = Coercion <$> tcIfaceCo co
+
+tcIfaceExpr (IfaceCast expr co)
+  = Cast <$> tcIfaceExpr expr <*> tcIfaceCo co
+
 tcIfaceExpr (IfaceLcl name)
   = Var <$> tcIfaceLclId name
 
@@ -853,7 +895,7 @@ tcIfaceExpr (IfaceLam bndr body)
 tcIfaceExpr (IfaceApp fun arg)
   = App <$> tcIfaceExpr fun <*> tcIfaceExpr arg
 
-tcIfaceExpr (IfaceCase scrut case_bndr ty alts)  = do
+tcIfaceExpr (IfaceCase scrut case_bndr alts)  = do
     scrut' <- tcIfaceExpr scrut
     case_bndr_name <- newIfaceName (mkVarOccFS case_bndr)
     let
@@ -868,8 +910,7 @@ tcIfaceExpr (IfaceCase scrut case_bndr ty alts)  = do
 
     extendIfaceIdEnv [case_bndr'] $ do
      alts' <- mapM (tcIfaceAlt scrut' tc_app) alts
-     ty' <- tcIfaceType ty
-     return (Case scrut' case_bndr' ty' alts')
+     return (Case scrut' case_bndr' (coreAltsType alts') alts')
 
 tcIfaceExpr (IfaceLet (IfaceNonRec (IfLetBndr fs ty info) rhs) body)
   = do	{ name 	  <- newIfaceName (mkVarOccFS fs)
@@ -898,11 +939,6 @@ tcIfaceExpr (IfaceLet (IfaceRec pairs) body)
                                 (idName id) (idType id) info
           ; return (setIdInfo id id_info, rhs') }
 
-tcIfaceExpr (IfaceCast expr co) = do
-    expr' <- tcIfaceExpr expr
-    co' <- tcIfaceType co
-    return (Cast expr' co')
-
 tcIfaceExpr (IfaceNote note expr) = do
     expr' <- tcIfaceExpr expr
     case note of
@@ -942,14 +978,13 @@ tcIfaceDataAlt :: DataCon -> [Type] -> [FastString] -> IfaceExpr
 tcIfaceDataAlt con inst_tys arg_strs rhs
   = do	{ us <- newUniqueSupply
 	; let uniqs = uniqsFromSupply us
-	; let (ex_tvs, co_tvs, arg_ids)
+	; let (ex_tvs, arg_ids)
 	              = dataConRepFSInstPat arg_strs uniqs con inst_tys
-              all_tvs = ex_tvs ++ co_tvs
 
-	; rhs' <- extendIfaceTyVarEnv all_tvs	$
+	; rhs' <- extendIfaceTyVarEnv ex_tvs	$
 		  extendIfaceIdEnv arg_ids	$
 		  tcIfaceExpr rhs
-	; return (DataAlt con, all_tvs ++ arg_ids, rhs') }
+	; return (DataAlt con, ex_tvs ++ arg_ids, rhs') }
 \end{code}
 
 
@@ -1217,6 +1252,10 @@ tcIfaceClass :: Name -> IfL Class
 tcIfaceClass name = do { thing <- tcIfaceGlobal name
 		       ; return (tyThingClass thing) }
 
+tcIfaceCoAxiom :: Name -> IfL CoAxiom
+tcIfaceCoAxiom name = do { thing <- tcIfaceGlobal name
+		         ; return (tyThingCoAxiom thing) }
+
 tcIfaceDataCon :: Name -> IfL DataCon
 tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
 		 	 ; case thing of