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
isUnLiftedType, mkForAllTys, mkTyVarTy, tyVarsOfType,
tcSplitFunTys, tcSplitForAllTys, dataConsStupidTheta
)
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,
import CoreUnfold ( mkTopUnfolding, mkCompulsoryUnfolding )
import Literal ( nullAddrLit, mkStringLit )
import TyCon ( TyCon, isNewTyCon, tyConDataCons, FieldLabel,
-- If we have e = MkT (MkS (PairInt 0 1)) and some body expecting a list of
-- ids, we get (modulo int passing)
--
-- 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
-- PairInt a b -> body [a,b]
--
-- The Ints passed around are just for creating fresh locals
-- 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
-- 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
-- where CoT is the coercion TyCon assoicated with the newtype
--
-- The call (wrapNewTypeBody T [a] e) returns the
-- body of the wrapper, namely
--
-- 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
--
-- 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
| 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
| otherwise
= result_expr
coArgs = decomposeCo (length tyVars) co
-- These InstPat functions go here to avoid circularity between DataCon and Id
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
dataConRepFSInstPat = dataConInstPat dataConRepArgTys
dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
-> DataCon
-> [Type] -- Types to instantiate the universally quantified tyvars
-> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
-> 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
-- (ex_tvs, co_tvs, arg_ids),
--
-- ex_tvs are intended to be used as binders for existential type args
-- 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
-- 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
--
-- Example.
-- The following constructor T1
-- ...
--
-- has representation type
-- ...
--
-- has representation type
--- forall a. forall a1. forall a2. forall b. (a :=: (a1,a2)) =>
+-- forall a. forall a1. forall b. (a :=: (a1,b)) =>
--- 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
dataConInstPat arg_fun fss uniqs con inst_tys
= (ex_bndrs, co_bndrs, id_bndrs)
where
inst_subst = substTyWith (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
-- make new coercion vars, instantiating kind
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
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
co_bndrs = zipWith3 mk_co_var co_uniqs co_fss eq_preds
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 :: 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 )
exprIsConApp_maybe (Cast expr co)
= -- Maybe this is over the top, but here we try to turn
-- coerce (S,T) ( x, y )
case splitNewTypeRepCo_maybe ty of {
Just(ty1,co) ->
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
Nothing ->
-- We have an expression of arity > 0, but its type isn't a function
-- Recursive newtypes
| Just(rep_ty, co) <- splitNewTypeRepCo_maybe arg_ty
-- 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,
-- Booleans
| Just (tc,_) <- splitTyConApp_maybe arg_ty,
-- Recursive newtypes
| Just (rep_ty, co) <- splitNewTypeRepCo_maybe result_ty
= resultWrapper rep_ty `thenDs` \ (maybe_ty, wrapper) ->
-- 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).
-- The type might contain foralls (eg. for dummy type arguments,
-- referring to 'Ptr a' is legal).
dc_occ = mkClassDataConOcc cls_occ
co_occs | is_newtype = [mkNewTyCoOcc tc_occ]
| otherwise = []
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
| otherwise = mkDataConWorkerOcc dc_occ -- Otherwise worker but no wrapper
is_newtype = n_sigs + n_ctxt == 1 -- Sigh
IfCon { ifConOcc = con_occ,
ifConFields = fields})})
= fields ++ [con_occ, mkDataConWrapperOcc con_occ, mkNewTyCoOcc 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
ifaceDeclSubBndrs (IfaceData {ifCons = IfDataTyCon cons})
= nub (concatMap ifConFields cons) -- Eliminate duplicate fields
-- simply coerces.
= mkWWargs rep_ty demands one_shots `thenUs` \ (wrap_args, wrap_fn_args, work_fn_args, res_ty) ->
returnUs (wrap_args,
-- 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 ->
res_ty)
| notNull demands
= getUniquesUs `thenUs` \ wrap_uniqs ->
import Type ( splitKindFunTys )
import TyCon ( tyConTyVars, tyConDataCons, tyConArity, tyConHasGenerics,
tyConStupidTheta, isProductTyCon, isDataTyCon, newTyConRhs,
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,
)
import TcType ( TcType, ThetaType, mkTyVarTys, mkTyConApp, tcTyConAppTyCon,
isUnLiftedType, mkClassPred, tyVarsOfType,
import TcUnify ( checkSigTyVars )
import TcSimplify ( tcSimplifySuperClasses )
import Type ( zipOpenTvSubst, substTheta, mkTyConApp, mkTyVarTy )
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 )
import TyCon ( TyCon, newTyConCo )
import DataCon ( classDataCon, dataConTyCon, dataConInstArgTys )
import Class ( classBigSig )
-- class Show a => Foo a b where ...
-- newtype T a = MkT (Tree [a]) deriving( Foo Int )
-- The newtype gives an FC axiom looking like
-- 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])).
--
-- 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,
-- Foo _ op1 .. opn -> Foo ds op1 .. opn
tcInstDecl2 (InstInfo { iSpec = ispec,
= ExprCoFn (mkAppCoercion -- (mkAppsCoercion
(mkTyConApp cls_tycon [])
-- rep_tys)
= ExprCoFn (mkAppCoercion -- (mkAppsCoercion
(mkTyConApp cls_tycon [])
-- rep_tys)
- (mkTyConApp co_con (map mkTyVarTy tvs)))
+ (mkSymCoercion (mkTyConApp co_con (map mkTyVarTy tvs))))
= mkCoercion unsafeCoercionTyCon [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
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...
--------------------------------------
-- Coercion Type Constructors...
-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
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])
and then when we used CoT at a particular type, s, we'd say
CoT @ s
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
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
In the vocabulary of the paper it's as if we had axiom declarations
like
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]
~~~~~~~~~~~~~~~~~~
Note [Newtype eta]
~~~~~~~~~~~~~~~~~~