Flip direction of newtype coercions, fix some comments

Mon Sep 18 17:19:19 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Flip direction of newtype coercions, fix some comments
  Sun Aug  6 20:56:23 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Flip direction of newtype coercions, fix some comments
    Thu Aug  3 10:53:37 EDT 2006  kevind@bu.edu

compiler/basicTypes/MkId.lhs

@@ -57,7 +57,7 @@ import TcType		( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy,
 			  isUnLiftedType, mkForAllTys, mkTyVarTy, tyVarsOfType,
 			  tcSplitFunTys, tcSplitForAllTys, dataConsStupidTheta
 			)
-import CoreUtils	( exprType, dataConOrigInstPat )
+import CoreUtils	( exprType, dataConOrigInstPat, mkCoerce )
 import CoreUnfold 	( mkTopUnfolding, mkCompulsoryUnfolding )
 import Literal		( nullAddrLit, mkStringLit )
 import TyCon		( TyCon, isNewTyCon, tyConDataCons, FieldLabel,
@@ -592,7 +592,7 @@ mkRecordSelId tycon field_label
 -- If we have e = MkT (MkS (PairInt 0 1)) and some body expecting a list of
 -- ids, we get (modulo int passing)
 --
---   case (e `cast` (sym CoT)) `cast` (sym CoS) of
+--   case (e `cast` CoT) `cast` CoS of
 --     PairInt a b -> body [a,b]
 --
 -- The Ints passed around are just for creating fresh locals
@@ -782,26 +782,26 @@ wrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 -- The wrapper for the data constructor for a newtype looks like this:
 --	newtype T a = MkT (a,Int)
 --	MkT :: forall a. (a,Int) -> T a
---	MkT = /\a. \(x:(a,Int)). x `cast` CoT a
+--	MkT = /\a. \(x:(a,Int)). x `cast` sym (CoT a)
 -- where CoT is the coercion TyCon assoicated with the newtype
 --
 -- The call (wrapNewTypeBody T [a] e) returns the
 -- body of the wrapper, namely
---	e `cast` CoT [a]
+--	e `cast` (CoT [a])
 --
 -- If a coercion constructor is prodivided in the newtype, then we use
 -- it, otherwise the wrap/unwrap are both no-ops 
 --
 wrapNewTypeBody tycon args result_expr
   | Just co_con <- newTyConCo tycon
-  = Cast result_expr (mkTyConApp co_con args)
+  = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) result_expr
   | otherwise
   = result_expr
 
 unwrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 unwrapNewTypeBody tycon args result_expr
   | Just co_con <- newTyConCo tycon
-  = Cast result_expr (mkSymCoercion (mkTyConApp co_con args))
+  = mkCoerce (mkTyConApp co_con args) result_expr
   | otherwise
   = result_expr
 

compiler/coreSyn/CoreUtils.lhs

@@ -681,8 +681,8 @@ deepCast ty tyVars co
     coArgs = decomposeCo (length tyVars) co
 
 -- These InstPat functions go here to avoid circularity between DataCon and Id
-dataConOrigInstPat   = dataConInstPat dataConOrigArgTys (repeat (FSLIT("ipv")))
-dataConRepInstPat    = dataConInstPat dataConRepArgTys (repeat (FSLIT("ipv")))
+dataConOrigInstPat  = dataConInstPat dataConOrigArgTys (repeat (FSLIT("ipv")))
+dataConRepInstPat   = dataConInstPat dataConRepArgTys (repeat (FSLIT("ipv")))
 dataConRepFSInstPat = dataConInstPat dataConRepArgTys
 
 dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
@@ -691,7 +691,7 @@ dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
                   -> DataCon
 	          -> [Type]                -- Types to instantiate the universally quantified tyvars
 	       -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
--- dataConInstPat arg_fun us fss con inst_tys returns a triple 
+-- dataConInstPat arg_fun fss us con inst_tys returns a triple 
 -- (ex_tvs, co_tvs, arg_ids),
 --
 --   ex_tvs are intended to be used as binders for existential type args
@@ -700,7 +700,7 @@ dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
 --     of these vars have been instantiated by the inst_tys and the ex_tys
 --
 --   arg_ids are indended to be used as binders for value arguments, including
---     dicts, and have their types instantiated with inst_tys and ex_tys
+--     dicts, and their types have been instantiated with inst_tys and ex_tys
 --
 -- Example.
 --  The following constructor T1
@@ -710,15 +710,15 @@ dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
 --    ...
 --
 --  has representation type 
---   forall a. forall a1. forall a2. forall b. (a :=: (a1,a2)) => 
+--   forall a. forall a1. forall b. (a :=: (a1,b)) => 
 --     Int -> b -> T a
 --
---  dataConInstPat us T1 (a1',a2') will return
+--  dataConInstPat fss us T1 (a1',b') will return
 --
---  ([a1'', a2'', b''],[c :: (a1',a2'):=:(a1'',a2'')],[x :: Int,y :: b''])
+--  ([a1'', b''], [c :: (a1', b'):=:(a1'', b'')], [x :: Int, y :: b''])
 --
---  where the double-primed variables are created from the unique list input
---  getting names from the FS list input
+--  where the double-primed variables are created with the FastStrings and
+--  Uniques given as fss and us
 dataConInstPat arg_fun fss uniqs con inst_tys 
   = (ex_bndrs, co_bndrs, id_bndrs)
   where 
@@ -751,9 +751,10 @@ dataConInstPat arg_fun fss uniqs con inst_tys
     inst_subst = substTyWith (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
 
       -- make new coercion vars, instantiating kind
-    mk_co_var uniq fs eq_pred = mkCoVar new_name (inst_subst (mkPredTy eq_pred))
+    mk_co_var uniq fs eq_pred = mkCoVar new_name co_kind
        where
          new_name = mkSysTvName uniq fs
+         co_kind  = inst_subst (mkPredTy eq_pred)
 
     co_bndrs = zipWith3 mk_co_var co_uniqs co_fss eq_preds
 
@@ -764,7 +765,6 @@ dataConInstPat arg_fun fss uniqs con inst_tys
 exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr])
 -- Returns (Just (dc, [x1..xn])) if the argument expression is 
 -- a constructor application of the form (dc x1 .. xn)
-
 exprIsConApp_maybe (Cast expr co)
   = 	-- Maybe this is over the top, but here we try to turn
 	-- 	coerce (S,T) ( x, y )
@@ -1173,7 +1173,7 @@ eta_expand n us expr ty
 
     	case splitNewTypeRepCo_maybe ty of {
  	  Just(ty1,co) -> 
-              mkCoerce co (eta_expand n us (mkCoerce (mkSymCoercion co) expr) ty1) ;
+              mkCoerce (mkSymCoercion co) (eta_expand n us (mkCoerce co expr) ty1) ;
  	  Nothing  -> 
 
 	-- We have an expression of arity > 0, but its type isn't a function

compiler/deSugar/DsCCall.lhs

@@ -161,7 +161,7 @@ unboxArg arg
 
   -- Recursive newtypes
   | Just(rep_ty, co) <- splitNewTypeRepCo_maybe arg_ty
-  = unboxArg (mkCoerce (mkSymCoercion co) arg)
+  = unboxArg (mkCoerce co arg)
       
   -- Booleans
   | Just (tc,_) <- splitTyConApp_maybe arg_ty, 
@@ -401,7 +401,7 @@ resultWrapper result_ty
   -- Recursive newtypes
   | Just (rep_ty, co) <- splitNewTypeRepCo_maybe result_ty
   = resultWrapper rep_ty `thenDs` \ (maybe_ty, wrapper) ->
-    returnDs (maybe_ty, \e -> mkCoerce co (wrapper e))
+    returnDs (maybe_ty, \e -> mkCoerce (mkSymCoercion co) (wrapper e))
 
   -- The type might contain foralls (eg. for dummy type arguments,
   -- referring to 'Ptr a' is legal).

compiler/iface/LoadIface.lhs

@@ -359,7 +359,7 @@ ifaceDeclSubBndrs IfaceClass { ifCtxt = sc_ctxt,
     dc_occ  = mkClassDataConOcc cls_occ	
     co_occs | is_newtype = [mkNewTyCoOcc tc_occ]
 	    | otherwise  = []
-    dcww_occ | is_newtype = mkDataConWrapperOcc dc_occ	-- Newtypes have wrapper but no worker
+    dcww_occ -- | is_newtype = mkDataConWrapperOcc dc_occ	-- Newtypes have wrapper but no worker
 	     | otherwise  = mkDataConWorkerOcc dc_occ	-- Otherwise worker but no wrapper
     is_newtype = n_sigs + n_ctxt == 1			-- Sigh 
 
@@ -371,7 +371,6 @@ ifaceDeclSubBndrs (IfaceData {ifName = tc_occ,
 				         IfCon { ifConOcc = con_occ, 
 						 ifConFields = fields})})
   = fields ++ [con_occ, mkDataConWrapperOcc con_occ, mkNewTyCoOcc tc_occ]
-	-- Wrapper, no worker; see MkId.mkDataConIds
 
 ifaceDeclSubBndrs (IfaceData {ifCons = IfDataTyCon cons})
   = nub (concatMap ifConFields cons) 	-- Eliminate duplicate fields

compiler/stranal/WwLib.lhs

@@ -238,8 +238,8 @@ mkWWargs fun_ty demands one_shots
 	-- simply coerces.
   = mkWWargs rep_ty demands one_shots	`thenUs` \ (wrap_args, wrap_fn_args, work_fn_args, res_ty) ->
     returnUs (wrap_args,
-	      \ e -> Cast (wrap_fn_args e) co,
-	      \ e -> work_fn_args (Cast e (mkSymCoercion co)),
+	      \ e -> Cast (wrap_fn_args e) (mkSymCoercion co),
+	      \ e -> work_fn_args (Cast e co),
 	      res_ty)
   | notNull demands
   = getUniquesUs 		`thenUs` \ wrap_uniqs ->

compiler/typecheck/TcDeriv.lhs

@@ -42,8 +42,7 @@ import NameSet		( duDefs )
 import Type		( splitKindFunTys )
 import TyCon		( tyConTyVars, tyConDataCons, tyConArity, tyConHasGenerics,
 			  tyConStupidTheta, isProductTyCon, isDataTyCon, newTyConRhs,
-			  isEnumerationTyCon, isRecursiveTyCon, TyCon, isNewTyCon,
-                          newTyConCo
+			  isEnumerationTyCon, isRecursiveTyCon, TyCon, isNewTyCon
 			)
 import TcType		( TcType, ThetaType, mkTyVarTys, mkTyConApp, tcTyConAppTyCon,
 			  isUnLiftedType, mkClassPred, tyVarsOfType,

compiler/typecheck/TcInstDcls.lhs

@@ -27,7 +27,7 @@ import TcHsType		( kcHsSigType, tcHsKindedType )
 import TcUnify		( checkSigTyVars )
 import TcSimplify	( tcSimplifySuperClasses )
 import Type		( zipOpenTvSubst, substTheta, mkTyConApp, mkTyVarTy )
-import Coercion         ( mkAppCoercion, mkAppsCoercion )
+import Coercion         ( mkAppCoercion, mkAppsCoercion, mkSymCoercion )
 import TyCon            ( TyCon, newTyConCo )
 import DataCon		( classDataCon, dataConTyCon, dataConInstArgTys )
 import Class		( classBigSig )
@@ -320,12 +320,12 @@ tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
 -- 	class Show a => Foo a b where ...
 -- 	newtype T a = MkT (Tree [a]) deriving( Foo Int )
 -- The newtype gives an FC axiom looking like
---	axiom CoT a :: Tree [a] = T a
+--	axiom CoT a ::  T a :=: Tree [a]
 --
 -- So all need is to generate a binding looking like
 -- 	dfunFooT :: forall a. (Foo Int (Tree [a], Show (T a)) => Foo Int (T a)
 --	dfunFooT = /\a. \(ds:Show (T a)) (df:Foo (Tree [a])).
---		  case df `cast` (Foo Int (CoT a)) of
+--		  case df `cast` (Foo Int (sym (CoT a))) of
 --		     Foo _ op1 .. opn -> Foo ds op1 .. opn
 
 tcInstDecl2 (InstInfo { iSpec = ispec, 
@@ -388,7 +388,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec,
 	  = ExprCoFn (mkAppCoercion -- (mkAppsCoercion 
                                      (mkTyConApp cls_tycon []) 
                                      -- rep_tys)
-                       		    (mkTyConApp co_con (map mkTyVarTy tvs)))
+                       		    (mkSymCoercion (mkTyConApp co_con (map mkTyVarTy tvs))))
 	  | otherwise
 	  = idCoercion
 

compiler/types/Coercion.lhs

@@ -284,20 +284,13 @@ mkUnsafeCoercion ty1 ty2
   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 
 
--- Make the coercion associated with a newtype.  If we have
---
---   newtype T a b = MkT (Int, a, b)
---
--- Then (mkNewTypeCoercion CoT T [a,b] (Int, a, b)) creates the coercion
--- CoT, such kinding rule such that
---
---   CoT S U :: (Int, S, U) :=: T S U
+-- See note [Newtype coercions] in TyCon
 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 mkNewTypeCoercion name tycon tvs rhs_ty 
   = ASSERT (length tvs == tyConArity tycon)
     mkCoercionTyCon name (tyConArity tycon) rule
   where
-    rule args = mkCoKind (substTyWith tvs args rhs_ty) (TyConApp tycon args)
+    rule args = mkCoKind (TyConApp tycon args) (substTyWith tvs args rhs_ty)
 
 --------------------------------------
 -- Coercion Type Constructors...

compiler/types/TyCon.lhs

@@ -240,13 +240,13 @@ newtype, to the newtype itself. For example,
 
    newtype T a = MkT [a]
 
-the NewTyCon for T will contain nt_co = CoT where CoT t : [t] :=: T t.
+the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: [t].
 This TyCon is a CoercionTyCon, so it does not have a kind on its own;
 it basically has its own typing rule for the fully-applied version.
 If the newtype T has k type variables then CoT has arity k.
 
 In the paper we'd write
-	axiom CoT : (forall t. [t]) :=: (forall t. T t)
+	axiom CoT : (forall t. T t) :=: (forall t. [t])
 and then when we used CoT at a particular type, s, we'd say
 	CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
@@ -254,10 +254,10 @@ which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
 But in GHC we instead make CoT into a new piece of type syntax
 (like instCoercionTyCon, symCoercionTyCon etc), which must always
 be saturated, but which encodes as
-	TyConAp CoT [s]
+	TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like
-	axiom CoT t : ([t] :=: T t)
+	axiom CoT t :  T t :=: [t]
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~