Commit 2ce87c70 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Re-work the newtype-deriving support

The newtype deriving mechanism is much trickier to support than it
seems at first.  Kevin didn't get it quite right when moving to FC,
and I ended up re-writing quite a bit of it.  

I think it's right now, but I have not yet tested it thoroughly.
parent 00cc4d87
......@@ -130,21 +130,20 @@ 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 tvs rhs_ty
cocon_maybe
| all_coercions || isRecursiveTyCon tycon
= Just co_tycon
| otherwise
= Nothing
; return (NewTyCon { data_con = con,
; let co_tycon = mkNewTypeCoercion co_tycon_name tycon etad_rhs
cocon_maybe | all_coercions || isRecursiveTyCon tycon
= Just co_tycon
| otherwise
= Nothing
; return (NewTyCon { data_con = con,
nt_rhs = rhs_ty,
nt_etad_rhs = etad_rhs,
nt_co = cocon_maybe,
-- Coreview looks through newtypes with a Nothing
-- for nt_co, or uses explicit coercions otherwise
nt_rhs = rhs_ty,
nt_etad_rhs = eta_reduce tvs rhs_ty,
nt_rep = mkNewTyConRep tycon rhs_ty }) }
where
-- if all_coercions is True then we use coercions for all newtypes
-- 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
......@@ -153,18 +152,20 @@ mkNewTyConRhs tycon_name tycon con
-- Instantiate the data con with the
-- type variables from the tycon
eta_reduce [] ty = ([], ty)
eta_reduce (a:as) ty | null as',
Just (fun, arg) <- splitAppTy_maybe ty',
etad_rhs :: ([TyVar], Type)
etad_rhs = eta_reduce (reverse tvs) rhs_ty
eta_reduce :: [TyVar] -- Reversed
-> Type -- Rhs type
-> ([TyVar], Type) -- Eta-reduced version (tyvars in normal order)
eta_reduce (a:as) ty | Just (fun, arg) <- splitAppTy_maybe ty,
Just tv <- getTyVar_maybe arg,
tv == a,
not (a `elemVarSet` tyVarsOfType fun)
= ([], fun) -- Successful eta reduction
| otherwise
= (a:as', ty')
where
(as', ty') = eta_reduce as ty
= eta_reduce as fun
eta_reduce tvs ty = (reverse tvs, ty)
mkNewTyConRep :: TyCon -- The original type constructor
-> Type -- The arg type of its constructor
-> Type -- Chosen representation type
......
......@@ -34,7 +34,7 @@ import Class ( className, classArity, classKey, classTyVars, classSCTheta, Clas
import Type ( zipOpenTvSubst, substTheta, pprThetaArrow, pprClassPred, mkTyVarTy )
import ErrUtils ( dumpIfSet_dyn )
import MkId ( mkDictFunId )
import DataCon ( isNullarySrcDataCon, isVanillaDataCon, dataConOrigArgTys, dataConInstOrigArgTys )
import DataCon ( isNullarySrcDataCon, isVanillaDataCon, dataConInstOrigArgTys )
import Maybes ( catMaybes )
import RdrName ( RdrName )
import Name ( Name, getSrcLoc )
......@@ -42,13 +42,13 @@ import NameSet ( duDefs )
import Type ( splitKindFunTys )
import TyCon ( tyConTyVars, tyConDataCons, tyConArity, tyConHasGenerics,
tyConStupidTheta, isProductTyCon, isDataTyCon, newTyConRhs,
isEnumerationTyCon, isRecursiveTyCon, TyCon, isNewTyCon
isEnumerationTyCon, isRecursiveTyCon, TyCon
)
import TcType ( TcType, ThetaType, mkTyVarTys, mkTyConApp, tcTyConAppTyCon,
isUnLiftedType, mkClassPred, tyVarsOfType,
isUnLiftedType, mkClassPred, tyVarsOfType, tyVarsOfTypes,
isSubArgTypeKind, tcEqTypes, tcSplitAppTys, mkAppTys )
import Var ( TyVar, tyVarKind, varName )
import VarSet ( mkVarSet, subVarSet )
import VarSet ( mkVarSet, disjointVarSet )
import PrelNames
import SrcLoc ( srcLocSpan, Located(..) )
import Util ( zipWithEqual, sortLe, notNull )
......@@ -315,10 +315,8 @@ all those.
Note [Newtype deriving superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The 'tys' here come from the partial application
in the deriving clause. The last arg is the new
instance type.
The 'tys' here come from the partial application in the deriving
clause. The last arg is the new instance type.
We must pass the superclasses; the newtype might be an instance
of them in a different way than the representation type
......@@ -386,11 +384,11 @@ makeDerivEqns overlap_flag tycl_decls
mk_eqn_help gla_exts NewType tycon deriv_tvs clas tys
| can_derive_via_isomorphism && (gla_exts || std_class_via_iso clas)
= -- Go ahead and use the isomorphism
traceTc (text "newtype deriving:" <+> ppr tycon <+> ppr rep_tys) `thenM_`
new_dfun_name clas tycon `thenM` \ dfun_name ->
returnM (Nothing, Just (InstInfo { iSpec = mk_inst_spec dfun_name,
iBinds = NewTypeDerived tycon rep_tys }))
= do { traceTc (text "newtype deriving:" <+> ppr tycon <+> ppr rep_tys)
; -- Go ahead and use the isomorphism
dfun_name <- new_dfun_name clas tycon
; return (Nothing, Just (InstInfo { iSpec = mk_inst_spec dfun_name,
iBinds = NewTypeDerived ntd_info })) }
| std_class gla_exts clas
= mk_eqn_help gla_exts DataType tycon deriv_tvs clas tys -- Go via bale-out route
......@@ -401,22 +399,32 @@ makeDerivEqns overlap_flag tycl_decls
non_std_err) -- Just complain about being a non-std instance
where
-- Here is the plan for newtype derivings. We see
-- newtype T a1...an = T (t ak...an) deriving (.., C s1 .. sm, ...)
-- newtype T a1...an = MkT (t ak+1...an) deriving (.., C s1 .. sm, ...)
-- where t is a type,
-- ak...an is a suffix of a1..an
-- ak...an do not occur free in t,
-- ak+1...an is a suffix of a1..an
-- ak+1...an do not occur free in t, nor in the s1..sm
-- (C s1 ... sm) is a *partial applications* of class C
-- with the last parameter missing
-- (T a1 .. ak) matches the kind of C's last argument
-- (and hence so does t)
--
-- We generate the instance
-- instance forall ({a1..ak} u fvs(s1..sm)).
-- C s1 .. sm t => C s1 .. sm (T a1...ak)
-- where T a1...ap is the partial application of
-- the LHS of the correct kind and p >= k
--
-- We generate the instances
-- instance C s1 .. sm (t ak...ap) => C s1 .. sm (T a1...ap)
-- where T a1...ap is the partial application of the LHS of the correct kind
-- and p >= k
-- NB: the variables below are:
-- tc_tvs = [a1, ..., an]
-- tyvars_to_keep = [a1, ..., ak]
-- rep_ty = t ak .. an
-- deriv_tvs = fvs(s1..sm) \ tc_tvs
-- tys = [s1, ..., sm]
-- rep_fn' = t
--
-- Running example: newtype T s a = MkT (ST s a) deriving( Monad )
-- We generate the instance
-- instance Monad (ST s) => Monad (T s) where
-- fail = coerce ... (fail @ ST s)
-- (Actually we don't need the coerce, because non-rec newtypes are transparent
clas_tyvars = classTyVars clas
kind = tyVarKind (last clas_tyvars)
......@@ -452,24 +460,28 @@ makeDerivEqns overlap_flag tycl_decls
rep_pred = mkClassPred clas rep_tys
-- rep_pred is the representation dictionary, from where
-- we are gong to get all the methods for the newtype dictionary
-- here we are figuring out what superclass dictionaries to use
-- see Note [Newtype deriving superclasses] above
inst_tys = (tys ++ [mkTyConApp tycon (mkTyVarTys tyvars_to_keep)])
-- Next we figure out what superclass dictionaries to use
-- See Note [Newtype deriving superclasses] above
inst_tys = tys ++ [mkTyConApp tycon (mkTyVarTys tyvars_to_keep)]
sc_theta = substTheta (zipOpenTvSubst clas_tyvars inst_tys)
(classSCTheta clas)
-- If there are no tyvars, there's no need
-- to abstract over the dictionaries we need
dict_tvs = deriv_tvs ++ tc_tvs
dict_args -- | null dict_tvs = []
| otherwise = rep_pred : sc_theta
-- Example: newtype T = MkT Int deriving( C )
-- We get the derived instance
-- instance C T
-- rather than
-- instance C Int => C T
dict_tvs = deriv_tvs ++ tyvars_to_keep
all_preds = rep_pred : sc_theta -- NB: rep_pred comes first
(dict_args, ntd_info) | null dict_tvs = ([], Just all_preds)
| otherwise = (all_preds, Nothing)
-- Finally! Here's where we build the dictionary Id
mk_inst_spec dfun_name
= mkLocalInstance dfun overlap_flag
mk_inst_spec dfun_name = mkLocalInstance dfun overlap_flag
where
dfun = mkDictFunId dfun_name dict_tvs dict_args clas inst_tys
......@@ -505,10 +517,12 @@ makeDerivEqns overlap_flag tycl_decls
-- Check that eta reduction is OK
-- (a) the dropped-off args are identical
-- (b) the remaining type args mention
-- only the remaining type variables
-- (b) the remaining type args do not mention any of teh dropped type variables
-- (c) the type class args do not mention any of teh dropped type variables
dropped_tvs = mkVarSet tyvars_to_drop
eta_ok = (args_to_drop `tcEqTypes` mkTyVarTys tyvars_to_drop)
&& (tyVarsOfType rep_fn' `subVarSet` mkVarSet tyvars_to_keep)
&& (tyVarsOfType rep_fn' `disjointVarSet` dropped_tvs)
&& (tyVarsOfTypes tys `disjointVarSet` dropped_tvs)
cant_derive_err = derivingThingErr clas tys tycon tyvars_to_keep
(vcat [ptext SLIT("even with cunning newtype deriving:"),
......
......@@ -50,8 +50,8 @@ import TcIface ( tcImportDecl )
import IfaceEnv ( newGlobalBinder )
import TcRnMonad
import TcMType ( zonkTcType, zonkTcTyVarsAndFV )
import TcType ( Type, TcKind, TcTyVar, TcTyVarSet, TcType,
substTy, tyVarsOfType, tcTyVarsOfTypes, mkTyConApp,
import TcType ( Type, TcKind, TcTyVar, TcTyVarSet, TcType, PredType,
tyVarsOfType, tcTyVarsOfTypes, mkTyConApp,
getDFunTyKey, tcTyConAppTyCon, tcGetTyVar, mkTyVarTy,
tidyOpenType, isRefineableTy
)
......@@ -362,7 +362,7 @@ findGlobals tvs tidy_env
Just d -> go tidy_env1 (d:acc) things
Nothing -> go tidy_env1 acc things
ignore_it ty = not (tvs `intersectsVarSet` tyVarsOfType ty)
ignore_it ty = tvs `disjointVarSet` tyVarsOfType ty
-----------------------
find_thing ignore_it tidy_env (ATcId { tct_id = id })
......@@ -567,20 +567,26 @@ data InstBindings
[LSig Name] -- User pragmas recorded for generating
-- specialised instances
| NewTypeDerived
TyCon -- tycon for the newtype
-- Used for deriving instances of newtypes, where the
[Type] -- witness dictionary is identical to the argument
-- dictionary. Hence no bindings, no pragmas
-- The [Type] are the representation types
-- See notes in TcDeriv
| NewTypeDerived -- Used for deriving instances of newtypes, where the
-- witness dictionary is identical to the argument
-- dictionary. Hence no bindings, no pragmas.
(Maybe [PredType])
-- Nothing => The newtype-derived instance involves type variables,
-- and the dfun has a type like df :: forall a. Eq a => Eq (T a)
-- Just (r:scs) => The newtype-defined instance has no type variables
-- so the dfun is just a constant, df :: Eq T
-- In this case we need to know waht the rep dict, r, and the
-- superclasses, scs, are. (In the Nothing case these are in the
-- dict fun's type.)
-- Invariant: these PredTypes have no free variables
-- NB: In both cases, the representation dict is the *first* dict.
pprInstInfo info = vcat [ptext SLIT("InstInfo:") <+> ppr (idType (iDFunId info))]
pprInstInfoDetails info = pprInstInfo info $$ nest 2 (details (iBinds info))
where
details (VanillaInst b _) = pprLHsBinds b
details (NewTypeDerived _ _) = text "Derived from the representation type"
details (NewTypeDerived _) = text "Derived from the representation type"
simpleInstInfoClsTy :: InstInfo -> (Class, Type)
simpleInstInfoClsTy info = case instanceHead (iSpec info) of
......
......@@ -18,6 +18,7 @@ import TcMType ( tcSkolSigType, checkValidInstance,
checkValidInstHead )
import TcType ( TcType, mkClassPred, tcSplitSigmaTy,
tcSplitDFunHead, SkolemInfo(InstSkol),
tcSplitTyConApp,
tcSplitDFunTy, mkFunTy )
import Inst ( newDictBndr, newDictBndrs, instToId, showLIE,
getOverlapFlag, tcExtendLocalInstEnv )
......@@ -32,29 +33,27 @@ import TcHsType ( kcHsSigType, tcHsKindedType )
import TcUnify ( checkSigTyVars )
import TcSimplify ( tcSimplifySuperClasses )
import Type ( zipOpenTvSubst, substTheta, mkTyConApp, mkTyVarTy,
splitFunTys, TyThing(ATyCon), isTyVarTy, tcEqType,
TyThing(ATyCon), isTyVarTy, tcEqType,
substTys, emptyTvSubst, extendTvSubst )
import Coercion ( mkSymCoercion )
import TyCon ( TyCon, tyConName, newTyConCo_maybe, tyConTyVars,
isTyConAssoc, tyConFamInst_maybe,
assocTyConArgPoss_maybe )
import DataCon ( classDataCon, dataConTyCon, dataConInstArgTys )
import Class ( Class, classBigSig, classATs )
import Var ( TyVar, Id, idName, idType, tyVarKind, tyVarName )
import VarEnv ( rnBndrs2, mkRnEnv2, emptyInScopeSet )
import Id ( mkSysLocal )
import UniqSupply ( uniqsFromSupply, splitUniqSupply )
import DataCon ( classDataCon, dataConInstArgTys )
import Class ( Class, classTyCon, classBigSig, classATs )
import Var ( TyVar, Id, idName, idType, tyVarName )
import MkId ( mkDictFunId )
import Name ( Name, getSrcLoc, nameOccName )
import NameSet ( addListToNameSet, emptyNameSet, minusNameSet,
nameSetToList )
import Maybe ( isNothing, fromJust, catMaybes )
import Maybe ( fromJust, catMaybes )
import Monad ( when )
import List ( find )
import DynFlags ( DynFlag(Opt_WarnMissingMethods) )
import SrcLoc ( srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart,
getLoc)
import ListSetOps ( minusList )
import Util ( snocView, dropList )
import Outputable
import Bag
import BasicTypes ( Activation( AlwaysActive ), InlineSpec(..) )
......@@ -472,90 +471,112 @@ tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
------------------------
-- Derived newtype instances
--
-- We need to make a copy of the dictionary we are deriving from
-- because we may need to change some of the superclass dictionaries
-- see Note [Newtype deriving superclasses] in TcDeriv.lhs
--
-- In the case of a newtype, things are rather easy
-- 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 :: T a :=: Tree [a]
-- (see Note [Newtype coercions] in TyCon for this unusual form of axiom)
--
-- So all need is to generate a binding looking like
-- 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 (sym (CoT a))) of
-- Foo _ op1 .. opn -> Foo ds op1 .. opn
--
-- If there are no superclasses, matters are simpler, because we don't need the case
-- see Note [Newtype deriving superclasses] in TcDeriv.lhs
tcInstDecl2 (InstInfo { iSpec = ispec,
iBinds = NewTypeDerived tycon rep_tys })
tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived mb_preds })
= do { let dfun_id = instanceDFunId ispec
rigid_info = InstSkol dfun_id
origin = SigOrigin rigid_info
inst_ty = idType dfun_id
; (tvs, theta, inst_head_ty) <- tcSkolSigType rigid_info inst_ty
-- inst_head_ty is a PredType
; inst_loc <- getInstLoc origin
; (tvs, theta, inst_head) <- tcSkolSigType rigid_info inst_ty
; dicts <- newDictBndrs inst_loc theta
; uniqs <- newUniqueSupply
; let (cls, cls_inst_tys) = tcSplitDFunHead inst_head
; this_dict <- newDictBndr inst_loc (mkClassPred cls rep_tys)
; let (rep_dict_id:sc_dict_ids)
| null dicts = [instToId this_dict]
| otherwise = map instToId dicts
-- (Here, we are relying on the order of dictionary
-- arguments built by NewTypeDerived in TcDeriv.)
wrap_fn = mkCoTyLams tvs <.> mkCoLams (rep_dict_id:sc_dict_ids)
; (rep_dict_id : sc_dict_ids, wrap_fn)
<- make_wrapper inst_loc tvs theta mb_preds
-- Here, we are relying on the order of dictionary
-- arguments built by NewTypeDerived in TcDeriv;
-- namely, that the rep_dict_id comes first
-- we need to find the kind that this class applies to
-- and drop trailing tvs appropriately
cls_kind = tyVarKind (head (reverse (tyConTyVars cls_tycon)))
the_tvs = drop_tail (length (fst (splitFunTys cls_kind))) tvs
coerced_rep_dict = mkHsCoerce (co_fn the_tvs cls_tycon cls_inst_tys) (HsVar rep_dict_id)
body | null sc_dict_ids = coerced_rep_dict
| otherwise = HsCase (noLoc coerced_rep_dict) $
MatchGroup [the_match] (mkFunTy in_dict_ty inst_head)
in_dict_ty = mkTyConApp cls_tycon cls_inst_tys
the_match = mkSimpleMatch [noLoc the_pat] the_rhs
the_rhs = mkHsConApp cls_data_con cls_inst_tys (map HsVar (sc_dict_ids ++ op_ids))
; let (cls, cls_inst_tys) = tcSplitDFunHead inst_head_ty
the_coercion = make_coercion cls cls_inst_tys
coerced_rep_dict = mkHsCoerce the_coercion (HsVar rep_dict_id)
(uniqs1, uniqs2) = splitUniqSupply uniqs
op_ids = zipWith (mkSysLocal FSLIT("op"))
(uniqsFromSupply uniqs1) op_tys
dict_ids = zipWith (mkSysLocal FSLIT("dict"))
(uniqsFromSupply uniqs2) (map idType sc_dict_ids)
the_pat = ConPatOut { pat_con = noLoc cls_data_con, pat_tvs = [],
pat_dicts = dict_ids,
pat_binds = emptyLHsBinds,
pat_args = PrefixCon (map nlVarPat op_ids),
pat_ty = in_dict_ty}
cls_data_con = classDataCon cls
cls_tycon = dataConTyCon cls_data_con
cls_arg_tys = dataConInstArgTys cls_data_con cls_inst_tys
; body <- make_body cls cls_inst_tys inst_head_ty sc_dict_ids coerced_rep_dict
n_dict_args = if length dicts == 0 then 0 else length dicts - 1
op_tys = drop n_dict_args cls_arg_tys
dict = mkHsCoerce wrap_fn body
; return (unitBag (noLoc $ VarBind dfun_id (noLoc dict))) }
; return (unitBag (noLoc $ VarBind dfun_id $ noLoc $ mkHsCoerce wrap_fn body)) }
where
-- For newtype T a = MkT <ty>
-- The returned coercion has kind :: C (T a):=:C <ty>
co_fn tvs cls_tycon cls_inst_tys | Just co_con <- newTyConCo_maybe tycon
= ExprCoFn (mkTyConApp cls_tycon (drop_tail 1 cls_inst_tys ++
[mkSymCoercion (mkTyConApp co_con (map mkTyVarTy tvs))]))
| otherwise
= idCoercion
drop_tail n l = take (length l - n) l
-----------------------
-- make_wrapper
-- We distinguish two cases:
-- (a) there is no tyvar abstraction in the dfun, so all dicts are constant,
-- and the new dict can just be a constant
-- (mb_preds = Just preds)
-- (b) there are tyvars, so we must make a dict *fun*
-- (mb_preds = Nothing)
-- See the defn of NewTypeDerived for the meaning of mb_preds
make_wrapper inst_loc tvs theta (Just preds) -- Case (a)
= ASSERT( null tvs && null theta )
do { dicts <- newDictBndrs inst_loc preds
; extendLIEs dicts
; return (map instToId dicts, idCoercion) }
make_wrapper inst_loc tvs theta Nothing -- Case (b)
= do { dicts <- newDictBndrs inst_loc theta
; let dict_ids = map instToId dicts
; return (dict_ids, mkCoTyLams tvs <.> mkCoLams dict_ids) }
-----------------------
-- make_coercion
-- The inst_head looks like (C s1 .. sm (T a1 .. ak))
-- But we want the coercion (C s1 .. sm (sym (CoT a1 .. ak)))
-- with kind (C s1 .. sm (T a1 .. ak) :=: C s1 .. sm <rep_ty>)
-- where rep_ty is the (eta-reduced) type rep of T
-- So we just replace T with CoT, and insert a 'sym'
-- NB: we know that k will be >= arity of CoT, because the latter fully eta-reduced
make_coercion cls cls_inst_tys
| Just (all_tys_but_last, last_ty) <- snocView cls_inst_tys
, (tycon, tc_args) <- tcSplitTyConApp last_ty -- Should not fail
, Just co_con <- newTyConCo_maybe tycon
, let co = mkSymCoercion (mkTyConApp co_con tc_args)
= ExprCoFn (mkTyConApp cls_tycon (all_tys_but_last ++ [co]))
| otherwise -- The newtype is transparent; no need for a cast
= idCoercion
where
cls_tycon = classTyCon cls
-----------------------
-- make_body
-- Two cases; see Note [Newtype deriving superclasses] in TcDeriv.lhs
-- (a) no superclasses; then we can just use the coerced dict
-- (b) one or more superclasses; then new need to do the unpack/repack
make_body cls cls_inst_tys inst_head_ty sc_dict_ids coerced_rep_dict
| null sc_dict_ids -- Case (a)
= return coerced_rep_dict
| otherwise -- Case (b)
= do { op_ids <- newSysLocalIds FSLIT("op") op_tys
; dummy_sc_dict_ids <- newSysLocalIds FSLIT("sc") (map idType sc_dict_ids)
; let the_pat = ConPatOut { pat_con = noLoc cls_data_con, pat_tvs = [],
pat_dicts = dummy_sc_dict_ids,
pat_binds = emptyLHsBinds,
pat_args = PrefixCon (map nlVarPat op_ids),
pat_ty = inst_head_ty}
the_match = mkSimpleMatch [noLoc the_pat] the_rhs
the_rhs = mkHsConApp cls_data_con cls_inst_tys $
map HsVar (sc_dict_ids ++ op_ids)
; return (HsCase (noLoc coerced_rep_dict) $
MatchGroup [the_match] (mkFunTy inst_head_ty inst_head_ty)) }
where
cls_data_con = classDataCon cls
cls_arg_tys = dataConInstArgTys cls_data_con cls_inst_tys
op_tys = dropList sc_dict_ids cls_arg_tys
------------------------
-- Ordinary instances
......
......@@ -37,14 +37,12 @@ import TypeRep
import Type ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView,
kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe,
tyVarsOfType, mkTyVarTys
coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe
)
import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isClosedNewTyCon,
newTyConRhs, newTyConCo_maybe,
isCoercionTyCon, isCoercionTyCon_maybe )
import Var ( Var, TyVar, isTyVar, tyVarKind )
import VarSet ( elemVarSet )
import Name ( BuiltInSyntax(..), Name, mkWiredInName, tcName )
import OccName ( mkOccNameFS )
import PrelNames ( symCoercionTyConKey,
......@@ -287,43 +285,17 @@ mkUnsafeCoercion ty1 ty2
-- 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 co_con_arity (mkKindingFun rule)
mkNewTypeCoercion :: Name -> TyCon -> ([TyVar], Type) -> TyCon
mkNewTypeCoercion name tycon (tvs, rhs_ty)
= mkCoercionTyCon name co_con_arity (mkKindingFun rule)
where
rule args = (TyConApp tycon tys, substTyWith tvs_eta tys rhs_eta, rest)
co_con_arity = length tvs
rule args = (TyConApp tycon tys, substTyWith tvs tys rhs_ty, rest)
where
tys = take co_con_arity args
rest = drop co_con_arity args
-- if the rhs_ty is a type application and it has a tail equal to a tail
-- of the tvs, then we eta-contract the type of the coercion
rhs_args = let (ty, ty_args) = splitAppTys rhs_ty in ty_args
n_eta_tys = count_eta (reverse rhs_args) (reverse tvs)
count_eta ((TyVarTy tv):rest_ty) (tv':rest_tv)
| tv == tv' && (not $ any (elemVarSet tv . tyVarsOfType) rest_ty)
-- if the last types are the same, and not free anywhere else
-- then eta contract
= 1 + (count_eta rest_ty rest_tv)
| otherwise -- don't
= 0
count_eta _ _ = 0
eqVar (TyVarTy tv) tv' = tv == tv'
eqVar _ _ = False
co_con_arity = (tyConArity tycon) - n_eta_tys
tvs_eta = (reverse (drop n_eta_tys (reverse tvs)))
rhs_eta
| (ty, ty_args) <- splitAppTys rhs_ty
= mkAppTys ty (reverse (drop n_eta_tys (reverse ty_args)))
-- Coercion identifying a data/newtype representation type and its family
-- instance. It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the
-- coercion tycon built here, `F' the family tycon and `R' the (derived)
......@@ -359,7 +331,8 @@ mkDataInstCoercion name tvs family instTys rep_tycon
-- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
--
-- (mkKindingFun f) is given the args [c, sym d, sym e]
mkKindingFun :: ([Type] -> (Type, Type, [Type])) -> [Type] -> Kind
mkKindingFun :: ([Type] -> (Type, Type, [Type]))
-> [Type] -> Kind
mkKindingFun f args =
let (ty1, ty2, rest) = f args in
let (argtys1, argtys2) = unzip (map coercionKind rest) in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment