From: Manuel M T Chakravarty Date: Wed, 20 Sep 2006 18:19:12 +0000 (+0000) Subject: Flip direction of newtype coercions, fix some comments X-Git-Tag: After_FC_branch_merge~52 X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=5e0ea427646a5474dd7c659b0713c6a62d8c99c7 Flip direction of newtype coercions, fix some comments Mon Sep 18 17:19:19 EDT 2006 Manuel M T Chakravarty * Flip direction of newtype coercions, fix some comments Sun Aug 6 20:56:23 EDT 2006 Manuel M T Chakravarty * Flip direction of newtype coercions, fix some comments Thu Aug 3 10:53:37 EDT 2006 kevind@bu.edu --- diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index 93369f5..a385e8b 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/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 diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index b798379..7344efd 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/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 diff --git a/compiler/deSugar/DsCCall.lhs b/compiler/deSugar/DsCCall.lhs index 4fe5f2d..a041665 100644 --- a/compiler/deSugar/DsCCall.lhs +++ b/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). diff --git a/compiler/iface/LoadIface.lhs b/compiler/iface/LoadIface.lhs index 599762e..f9e9114 100644 --- a/compiler/iface/LoadIface.lhs +++ b/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 diff --git a/compiler/stranal/WwLib.lhs b/compiler/stranal/WwLib.lhs index 3383cb4..f10cb22 100644 --- a/compiler/stranal/WwLib.lhs +++ b/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 -> diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index 550b274..2563b09 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/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, diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index ba57563..2db9bab 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/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 diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index cb85028..55a282d 100644 --- a/compiler/types/Coercion.lhs +++ b/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... diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 99afac9..785d085 100644 --- a/compiler/types/TyCon.lhs +++ b/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] ~~~~~~~~~~~~~~~~~~