From 24960efed96bb266b7cb6c0bce672f049c682475 Mon Sep 17 00:00:00 2001 From: Will Jones Date: Tue, 17 Apr 2012 13:03:25 +0100 Subject: [PATCH 1/5] Added the InjFamilyTyCon constructor to TyConRhs. --- compiler/iface/BinIface.hs | 6 +- compiler/iface/IfaceSyn.lhs | 4 +- compiler/iface/MkIface.lhs | 8 +- compiler/iface/TcIface.lhs | 7 +- compiler/typecheck/TcTyClsDecls.lhs | 206 ++++++++++++++++++----------------- compiler/types/TyCon.lhs | 8 +- 6 files changed, 126 insertions(+), 113 deletions(-) diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs index eff699f..ab9a0bf 100644 --- a/compiler/iface/BinIface.hs +++ b/compiler/iface/BinIface.hs @@ -1324,12 +1324,13 @@ instance Binary IfaceDecl where put_ bh a7 put_ bh a8 - put_ bh (IfaceSyn a1 a2 a3 a4) = do + put_ bh (IfaceSyn a1 a2 a3 a4 a5) = do putByte bh 3 put_ bh (occNameFS a1) put_ bh a2 put_ bh a3 put_ bh a4 + put_ bh a5 put_ bh (IfaceClass a1 a2 a3 a4 a5 a6 a7) = do putByte bh 4 @@ -1372,8 +1373,9 @@ instance Binary IfaceDecl where a2 <- get bh a3 <- get bh a4 <- get bh + a5 <- get bh occ <- return $! mkOccNameFS tcName a1 - return (IfaceSyn occ a2 a3 a4) + return (IfaceSyn occ a2 a3 a4 a5) 4 -> do a1 <- get bh a2 <- get bh a3 <- get bh diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs index d3e44fe..326cf3c 100644 --- a/compiler/iface/IfaceSyn.lhs +++ b/compiler/iface/IfaceSyn.lhs @@ -82,8 +82,10 @@ data IfaceDecl | IfaceSyn { ifName :: OccName, -- Type constructor ifTyVars :: [IfaceTvBndr], -- Type variables ifSynKind :: IfaceKind, -- Kind of the *rhs* (not of the tycon) - ifSynRhs :: Maybe IfaceType -- Just rhs for an ordinary synonyn + ifSynRhs :: Maybe IfaceType, -- Just rhs for an ordinary synonym -- Nothing for an type family declaration + ifInjSyn :: Bool -- True iff the declaration + -- defines an injective family } | IfaceClass { ifCtxt :: IfaceContext, -- Context... diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs index 3c8050c..7181827 100644 --- a/compiler/iface/MkIface.lhs +++ b/compiler/iface/MkIface.lhs @@ -1452,7 +1452,8 @@ tyThingToIfaceDecl (ATyCon tycon) = IfaceSyn { ifName = getOccName tycon, ifTyVars = toIfaceTvBndrs tyvars, ifSynRhs = syn_rhs, - ifSynKind = syn_ki } + ifSynKind = syn_ki, + ifInjSyn = isInjectiveTyCon tycon } | isAlgTyCon tycon = IfaceData { ifName = getOccName tycon, @@ -1473,8 +1474,11 @@ tyThingToIfaceDecl (ATyCon tycon) tyvars = tyConTyVars tycon (syn_rhs, syn_ki) = case synTyConRhs tycon of - SynFamilyTyCon -> (Nothing, toIfaceType (synTyConResKind tycon)) SynonymTyCon ty -> (Just (toIfaceType ty), toIfaceType (typeKind ty)) + _ -> (Nothing, toIfaceType (synTyConResKind tycon)) + -- In the latter case, we either have a type family + -- (SynFamilyTyCon) or an injective type family + -- (InjFamilyTyCon). ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con) diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs index badb3c7..9cd42d6 100644 --- a/compiler/iface/TcIface.lhs +++ b/compiler/iface/TcIface.lhs @@ -464,7 +464,8 @@ tc_iface_decl parent _ (IfaceData {ifName = occ_name, tc_iface_decl parent _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs, ifSynRhs = mb_rhs_ty, - ifSynKind = kind }) + ifSynKind = kind, + ifInjSyn = inj_syn}) = bindIfaceTyVars_AT tv_bndrs $ \ tyvars -> do { tc_name <- lookupIfaceTop occ_name ; rhs_kind <- tcIfaceType kind -- Note [Synonym kind loop] @@ -473,8 +474,8 @@ tc_iface_decl parent _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs, ; tycon <- buildSynTyCon tc_name tyvars rhs rhs_kind parent ; return (ATyCon tycon) } where - mk_doc n = ptext (sLit "Type syonym") <+> ppr n - tc_syn_rhs Nothing = return SynFamilyTyCon + mk_doc n = ptext (sLit "Type synonym") <+> ppr n + tc_syn_rhs Nothing = return (if inj_syn then InjFamilyTyCon else SynFamilyTyCon) tc_syn_rhs (Just ty) = do { rhs_ty <- tcIfaceType ty ; return (SynonymTyCon rhs_ty) } diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 89a018d..b96acb5 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -16,10 +16,10 @@ TcTyClsDecls: Typecheck type and class declarations module TcTyClsDecls ( tcTyAndClassDecls, tcAddImplicits, - -- Functions used by TcInstDcls to check + -- Functions used by TcInstDcls to check -- data/type family instance declarations kcTyDefn, tcConDecls, dataDeclChecks, checkValidTyCon, - tcSynFamInstDecl, tcFamTyPats, + tcSynFamInstDecl, tcFamTyPats, tcAddFamInstCtxt, wrongKindOfFamily, badATErr, wrongATArgErr ) where @@ -122,7 +122,7 @@ tcTyClGroup boot_details tyclds names_w_poly_kinds <- kcTyClGroup tyclds ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds) - -- Step 2: type-check all groups together, returning + -- Step 2: type-check all groups together, returning -- the final TyCons and Classes ; tyclss <- fixM $ \ rec_tyclss -> do { let rec_flags = calcRecFlags boot_details rec_tyclss @@ -157,7 +157,7 @@ tcTyClGroup boot_details tyclds tcAddImplicits :: [TyThing] -> TcM TcGblEnv tcAddImplicits tyclss - = tcExtendGlobalEnvImplicit implicit_things $ + = tcExtendGlobalEnvImplicit implicit_things $ tcRecSelBinds rec_sel_binds where implicit_things = concatMap implicitTyThings tyclss @@ -201,7 +201,7 @@ Note [Kind checking for type and class decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Kind checking is done thus: - 1. Make up a kind variable for each parameter of the *data* type, + 1. Make up a kind variable for each parameter of the *data* type, and class, decls, and extend the kind environment (which is in the TcLclEnv) @@ -259,7 +259,7 @@ kcTyClGroup decls = do { mod <- getModule ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls)) - -- Kind checking; + -- Kind checking; -- 1. Bind kind variables for non-synonyms -- 2. Kind-check synonyms, and bind kinds of those synonyms -- 3. Kind-check non-synonyms @@ -281,7 +281,7 @@ kcTyClGroup decls -- Step 4: generalisation -- Kind checking done for this group -- Now we have to kind generalize the flexis - ; res <- mapM generalise (tyClsBinders decls) + ; res <- mapM generalise (tyClsBinders decls) ; traceTc "kcTyClGroup result" (ppr res) ; return res }}} @@ -309,7 +309,7 @@ getInitialKinds :: LTyClDecl Name -> TcM [(Name, TcTyThing)] -- -- ALSO for each datacon, return (dc, ANothing) -- See Note [ANothing] in TcRnTypes --- +-- -- No family instances are passed to getInitialKinds getInitialKinds (L _ decl) @@ -328,7 +328,7 @@ getInitialKinds (L _ decl) = return [] get_res_kind (ClassDecl {}) = return constraintKind - get_res_kind (TyDecl { tcdTyDefn = TyData { td_kindSig = Nothing } }) + get_res_kind (TyDecl { tcdTyDefn = TyData { td_kindSig = Nothing } }) = return liftedTypeKind get_res_kind _ = newMetaKindVar -- Warning: you might be tempted to return * for all data decls @@ -337,10 +337,10 @@ getInitialKinds (L _ decl) -- with *no* tvs in the HsTyDefn get_tvs (TyFamily {tcdTyVars = tvs}) = tvs - get_tvs (ClassDecl {tcdTyVars = tvs}) = tvs + get_tvs (ClassDecl {tcdTyVars = tvs}) = tvs get_tvs (TyDecl {tcdTyVars = tvs}) = tvs get_tvs (ForeignType {}) = [] - + ---------------- kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM (TcLclEnv) -- Kind bindings kcSynDecls [] = getLclEnv @@ -385,7 +385,7 @@ kcTyClDecl (TyDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdTyDefn = defn } kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs , tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats}) - = kcTyClTyVars name hs_tvs $ \ res_k -> + = kcTyClTyVars name hs_tvs $ \ res_k -> do { _ <- tcHsContext ctxt ; _ <- unifyKind res_k constraintKind ; mapM_ (wrapLocM kcTyClDecl) ats @@ -409,7 +409,7 @@ kcTyDefn :: HsTyDefn Name -> Kind -> TcM () kcTyDefn (TyData { td_ND = new_or_data, td_ctxt = ctxt , td_cons = cons, td_kindSig = mb_kind }) res_k = do { _ <- tcHsContext ctxt - ; mapM_ (wrapLocM (kcConDecl new_or_data)) cons + ; mapM_ (wrapLocM (kcConDecl new_or_data)) cons ; kcResultKind mb_kind res_k } kcTyDefn (TySynonym { td_synRhs = rhs_ty }) res_k = discardResult (tcCheckLHsType rhs_ty res_k) @@ -419,7 +419,7 @@ kcConDecl :: NewOrData -> ConDecl Name -> TcM () kcConDecl new_or_data (ConDecl { con_name = name, con_qvars = ex_tvs , con_cxt = ex_ctxt, con_details = details, con_res = res }) = addErrCtxt (dataConCtxt name) $ - tcHsTyVarBndrs ex_tvs $ \ _ -> + tcHsTyVarBndrs ex_tvs $ \ _ -> do { _ <- tcHsContext ex_ctxt ; mapM_ (tcHsConArgType new_or_data) (hsConDeclArgTys details) ; _ <- tcConRes res @@ -429,10 +429,10 @@ kcConDecl new_or_data (ConDecl { con_name = name, con_qvars = ex_tvs kcResultKind :: Maybe (HsBndrSig (LHsKind Name)) -> Kind -> TcM () kcResultKind Nothing res_k = discardResult (unifyKind res_k liftedTypeKind) - -- type family F a + -- type family F a -- defaults to type family F a :: * kcResultKind (Just (HsBSig k ns)) res_k - = do { let kvs = map mkKindSigVar ns + = do { let kvs = map mkKindSigVar ns ; k' <- tcExtendTyVarEnv kvs (tcLHsKind k) ; discardResult (unifyKind k' res_k) } \end{code} @@ -448,7 +448,7 @@ Note [Type checking recursive type and class declarations] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At this point we have completed *kind-checking* of a mutually recursive group of type/class decls (done in kcTyClGroup). However, -we discarded the kind-checked types (eg RHSs of data type decls); +we discarded the kind-checked types (eg RHSs of data type decls); note that kcTyClDecl returns (). There are two reasons: * It's convenient, because we don't have to rebuild a @@ -456,7 +456,7 @@ note that kcTyClDecl returns (). There are two reasons: * It's necessary, because after kind-generalisation, the TyCons/Classes may now be kind-polymorphic, and hence need - to be given kind arguments. + to be given kind arguments. Example: data T f a = MkT (f a) (T f a) @@ -464,7 +464,7 @@ During kind-checking, we give T the kind T :: k1 -> k2 -> * and figure out constraints on k1, k2 etc. Then we generalise to get T :: forall k. (k->*) -> k -> * So now the (T f a) in the RHS must be elaborated to (T k f a). - + However, during tcTyClDecl of T (above) we will be in a recursive "knot". So we aren't allowed to look at the TyCon T itself; we are only allowed to put it (lazily) in the returned structures. But when @@ -522,7 +522,7 @@ tcTyClDecl1 _parent calc_isrec (TyDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdTyDefn = defn }) = ASSERT( isNoParent _parent ) - tcTyClTyVars tc_name tvs $ \ tvs' kind -> + tcTyClTyVars tc_name tvs $ \ tvs' kind -> tcTyDefn calc_isrec tc_name tvs' kind defn tcTyClDecl1 _parent calc_isrec @@ -531,13 +531,13 @@ tcTyClDecl1 _parent calc_isrec , tcdFDs = fundeps, tcdSigs = sigs , tcdATs = ats, tcdATDefs = at_defs }) = ASSERT( isNoParent _parent ) - do + do { (tvs', ctxt', fds', sig_stuff, gen_dm_env) <- tcTyClTyVars class_name tvs $ \ tvs' kind -> do { MASSERT( isConstraintKind kind ) ; ctxt' <- tcHsContext ctxt - ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt' + ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt' -- Squeeze out any kind unification variables ; fds' <- mapM (addLocM tc_fundep) fundeps @@ -561,8 +561,8 @@ tcTyClDecl1 _parent calc_isrec | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas , let gen_dm_tau = expectJust "tcTyClDecl1" $ lookupNameEnv gen_dm_env (idName sel_id) - , let gen_dm_ty = mkSigmaTy tvs' - [mkClassPred clas (mkTyVarTys tvs')] + , let gen_dm_ty = mkSigmaTy tvs' + [mkClassPred clas (mkTyVarTys tvs')] gen_dm_tau ] class_ats = map ATyCon (classATs clas) @@ -582,7 +582,7 @@ tcTyClDecl1 _ _ \end{code} \begin{code} -tcTyDefn :: (Name -> RecFlag) -> Name +tcTyDefn :: (Name -> RecFlag) -> Name -> [TyVar] -> Kind -> HsTyDefn Name -> TcM [TyThing] -- NB: not used for newtype/data instances (whether associated or not) @@ -642,7 +642,7 @@ Note [Associated type defaults] The following is an example of associated type defaults: class C a where - data D a + data D a type F a b :: * type F a Z = [a] -- Default @@ -670,8 +670,8 @@ tcClassATs class_name parent ats at_defs at_defs_map :: NameEnv [LFamInstDecl Name] -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs' - at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv - (famInstDeclName at_def) [at_def]) + at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv + (famInstDeclName at_def) [at_def]) emptyNameEnv at_defs tc_at at = do { [ATyCon fam_tc] <- addLocM (tcTyClDecl1 parent @@ -695,12 +695,12 @@ tcDefaultAssocDecl fam_tc (L loc decl) ------------------------- tcSynFamInstDecl :: TyCon -> FamInstDecl Name -> TcM ([TyVar], [Type], Type) --- Placed here because type family instances appear as --- default decls in class declarations +-- Placed here because type family instances appear as +-- default decls in class declarations tcSynFamInstDecl fam_tc (FamInstDecl { fid_pats = pats, fid_defn = defn@(TySynonym hs_ty) }) = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc) - ; tcFamTyPats fam_tc pats (kcTyDefn defn) $ \tvs' pats' res_kind -> + ; tcFamTyPats fam_tc pats (kcTyDefn defn) $ \tvs' pats' res_kind -> do { rhs_ty <- tcCheckLHsType hs_ty res_kind ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty ; traceTc "tcSynFamInstDecl" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty)) @@ -726,7 +726,7 @@ tcFamTyPats :: TyCon -- Check the type patterns of a type or data family instance -- type instance F = -- The 'tyvars' are the free type variables of pats --- +-- -- NB: The family instance declaration may be an associated one, -- nested inside an instance decl, thus -- instance C [a] where @@ -747,7 +747,7 @@ tcFamTyPats fam_tc (HsBSig arg_pats tyvars) kind_checker thing_inside -- Instantiate with meta kind vars ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs - ; let (arg_kinds, res_kind) + ; let (arg_kinds, res_kind) = splitKindFunTysN fam_arity $ substKiWith fam_kvs fam_arg_kinds fam_body @@ -770,7 +770,7 @@ Note [Quantifying over family patterns] We need to quantify over two different lots of kind variables: First, the ones that come from tcTyVarBndrsKindGen, as usual - data family Dist a + data family Dist a -- Proxy :: forall k. k -> * data instance Dist (Proxy a) = DP @@ -783,7 +783,7 @@ which we pick up using kindGeneralizeKinds: -- Any :: forall k. k data instance Dist Any = DA -- Generates data DistAny k = DA - -- ax7 k :: Dist k (Any k) ~ DistAny k + -- ax7 k :: Dist k (Any k) ~ DistAny k -- The 'k' comes from kindGeneralizeKinds (Any k) Note [Associated type instances] @@ -795,7 +795,7 @@ We allow this: type T (S y) Int = y type T Z Int = Char -Note that +Note that a) The variable 'x' is not bound by the class decl b) 'x' is instantiated to a non-type-variable in the instance c) There are several type instance decls for T in the instance @@ -812,7 +812,7 @@ Note [Checking consistent instantiation] type T [p] y Int = (p,y,y) -- Induces the family instance TyCon -- type TR p y = (p,y,y) -So we +So we * Form the mini-envt from the class type variables a,b to the instance decl types [p],Int: [a->[p], b->Int] @@ -843,7 +843,7 @@ dataDeclChecks tc_name new_or_data stupid_theta cons -- Check that a newtype has exactly one constructor -- Do this before checking for empty data decls, so that -- we don't suggest -XEmptyDataDecls for newtypes - ; checkTc (new_or_data == DataType || isSingleton cons) + ; checkTc (new_or_data == DataType || isSingleton cons) (newtypeConError tc_name (length cons)) -- Check that there's at least one condecl, @@ -852,7 +852,7 @@ dataDeclChecks tc_name new_or_data stupid_theta cons ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file? ; checkTc (not (null cons) || empty_data_decls || is_boot) (emptyConDeclsErr tc_name) } - + ----------------------------------- tcConDecls :: NewOrData -> Bool -> TyCon -> ([TyVar], Type) -> [LConDecl Name] -> TcM [DataCon] @@ -863,7 +863,7 @@ tcConDecl :: NewOrData -> Bool -- True <=> -XExistentialQuantificaton or -XGADTs -> TyCon -- Representation tycon -> ([TyVar], Type) -- Return type template (with its template tyvars) - -> ConDecl Name + -> ConDecl Name -> TcM DataCon tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types @@ -872,8 +872,8 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types , con_details = details, con_res = res_ty }) = addErrCtxt (dataConCtxt name) $ do { traceTc "tcConDecl 1" (ppr name) - ; (tvs', (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) - <- tcHsTyVarBndrsGen tvs $ + ; (tvs', (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) + <- tcHsTyVarBndrsGen tvs $ do { ctxt' <- tcHsContext ctxt ; details' <- tcConArgs new_or_data details ; res_ty' <- tcConRes res_ty @@ -887,7 +887,7 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types ; return (ftvs, (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) } - -- Substitute, to account for the kind + -- Substitute, to account for the kind -- unifications done by tcHsTyVarBndrsGen ; traceTc "tcConDecl 2" (ppr name) ; let ze = mkTyVarZonkEnv tvs' @@ -914,10 +914,10 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types } tcConArgs :: NewOrData -> HsConDeclDetails Name -> TcM (Bool, [Name], [(TcType, HsBang)]) -tcConArgs new_or_data (PrefixCon btys) +tcConArgs new_or_data (PrefixCon btys) = do { btys' <- mapM (tcConArg new_or_data) btys ; return (False, [], btys') } -tcConArgs new_or_data (InfixCon bty1 bty2) +tcConArgs new_or_data (InfixCon bty1 bty2) = do { bty1' <- tcConArg new_or_data bty1 ; bty2' <- tcConArg new_or_data bty2 ; return (True, [], [bty1', bty2']) } @@ -942,16 +942,16 @@ tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty ; return (ResTyGADT res_ty') } -- Example --- data instance T (b,c) where +-- data instance T (b,c) where -- TI :: forall e. e -> T (e,e) -- -- The representation tycon looks like this: --- data :R7T b c where +-- data :R7T b c where -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1 -- In this case orig_res_ty = T (e,e) rejigConRes :: ([TyVar], Type) -- Template for result type; e.g. - -- data instance T [a] b c = ... + -- data instance T [a] b c = ... -- gives template ([a,b,c], T [a] b c) -> [TyVar] -- where MkT :: forall x y z. ... -> ResType Type @@ -976,7 +976,7 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty) -- Univ tyvars Eq-spec -- a a~(x,y) -- b b~z - -- z + -- z -- Existentials are the leftover type vars: [x,y] -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z) = (univ_tvs, ex_tvs, eq_spec, res_ty) @@ -985,14 +985,14 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty) -- This 'Just' pattern is sure to match, because if not -- checkValidDataCon will complain first. The 'subst' -- should not be looked at until after checkValidDataCon - -- We can't check eagerly because we are in a "knot" in + -- We can't check eagerly because we are in a "knot" in -- which 'tycon' is not yet fully defined -- /Lazily/ figure out the univ_tvs etc -- Each univ_tv is either a dc_tv or a tmpl_tv (univ_tvs, eq_spec) = foldr choose ([], []) tidy_tmpl_tvs choose tmpl (univs, eqs) - | Just ty <- lookupTyVar subst tmpl + | Just ty <- lookupTyVar subst tmpl = case tcGetTyVar_maybe ty of Just tv | not (tv `elem` univs) -> (tv:univs, eqs) @@ -1005,14 +1005,14 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty) -- NB: tmpl_tvs and dc_tvs are distinct, but -- we want them to be *visibly* distinct, both for -- interface files and general confusion. So rename - -- the tc_tvs, since they are not used yet (no + -- the tc_tvs, since they are not used yet (no -- consequential renaming needed) (_, tidy_tmpl_tvs) = mapAccumL tidy_one init_occ_env tmpl_tvs init_occ_env = initTidyOccEnv (map getOccName dc_tvs) tidy_one env tv = (env', setTyVarName tv (tidyNameOcc name occ')) where name = tyVarName tv - (env', occ') = tidyOccName env (getOccName name) + (env', occ') = tidyOccName env (getOccName name) {- Note [Substitution in template variables kinds] @@ -1078,7 +1078,7 @@ conRepresentibleWithH98Syntax -- (i) The field is marked '!!', or -- (ii) The field is marked '!', and the -funbox-strict-fields flag is on. -- --- We have turned off unboxing of newtypes because coercions make unboxing +-- We have turned off unboxing of newtypes because coercions make unboxing -- and reboxing more complicated chooseBoxingStrategy :: TcType -> HsBang -> TcM HsBang chooseBoxingStrategy arg_ty bang @@ -1101,18 +1101,18 @@ chooseBoxingStrategy arg_ty bang -- Returns HsUnpack if we can unpack arg_ty -- fail_bang if we know what arg_ty is but we can't unpack it -- HsStrict if it's abstract, so we don't know whether or not we can unbox it - can_unbox fail_bang arg_ty + can_unbox fail_bang arg_ty = case splitTyConApp_maybe arg_ty of Nothing -> fail_bang - Just (arg_tycon, tycon_args) - | isAbstractTyCon arg_tycon -> HsStrict + Just (arg_tycon, tycon_args) + | isAbstractTyCon arg_tycon -> HsStrict -- See Note [Don't complain about UNPACK on abstract TyCons] | not (isRecursiveTyCon arg_tycon) -- Note [Recusive unboxing] - , isProductTyCon arg_tycon - -- We can unbox if the type is a chain of newtypes + , isProductTyCon arg_tycon + -- We can unbox if the type is a chain of newtypes -- with a product tycon at the end - -> if isNewTyCon arg_tycon + -> if isNewTyCon arg_tycon then can_unbox fail_bang (newTyConInstRhs arg_tycon tycon_args) else HsUnpack @@ -1123,7 +1123,7 @@ Note [Don't complain about UNPACK on abstract TyCons] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We are going to complain about UnpackFailed, but if we say data T = MkT {-# UNPACK #-} !Wobble -and Wobble is a newtype imported from a module that was compiled +and Wobble is a newtype imported from a module that was compiled without optimisation, we don't want to complain. Because it might be fine when optimsation is on. I think this happens when Haddock is working over (say) GHC souce files. @@ -1180,12 +1180,12 @@ checkValidTyCl decl AnId _ -> return () -- Generic default methods are checked -- with their parent class _ -> panic "checkValidTyCl" - ; traceTc "Done validity of" (ppr thing) + ; traceTc "Done validity of" (ppr thing) } ------------------------- -- For data types declared with record syntax, we require --- that each constructor that has a field 'f' +-- that each constructor that has a field 'f' -- (a) has the same result type -- (b) has the same type for 'f' -- module alpha conversion of the quantified type variables @@ -1195,23 +1195,25 @@ checkValidTyCl decl -- fields can never meet. E.g -- data T where -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T --- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T +-- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T -- Here we do not complain about f1,f2 because they are existential checkValidTyCon :: TyCon -> TcM () -checkValidTyCon tc +checkValidTyCon tc | Just cl <- tyConClass_maybe tc = checkValidClass cl - | isSynTyCon tc + | isSynTyCon tc = case synTyConRhs tc of - SynFamilyTyCon {} -> return () SynonymTyCon ty -> checkValidType syn_ctxt ty + _ -> return () + -- The latter case covers both type families and injective type + -- families. | otherwise = do { -- Check the context on the data decl ; traceTc "cvtc1" (ppr tc) ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc) - + -- Check arg types of data constructors ; traceTc "cvtc2" (ppr tc) ; mapM_ (checkValidDataCon tc) data_cons @@ -1230,7 +1232,7 @@ checkValidTyCon tc -- dataConFieldLabels may return the empty list, which is fine -- See Note [GADT record selectors] in MkId.lhs - -- We must check (a) that the named field has the same + -- We must check (a) that the named field has the same -- type in each constructor -- (b) that those constructors have the same result type -- @@ -1238,7 +1240,7 @@ checkValidTyCon tc -- and (worse) we don't know how the correspond to each other. E.g. -- C1 :: forall a b. { f :: a, g :: b } -> T a b -- C2 :: forall d c. { f :: c, g :: c } -> T c d - -- + -- -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's -- result type against other candidates' types BOTH WAYS ROUND. -- If they magically agrees, take the substitution and @@ -1258,7 +1260,7 @@ checkValidTyCon tc checkOne (_, con2) -- Do it bothways to ensure they are structurally identical = do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2 ; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 } - where + where (tvs2, _, _, res2) = dataConSig con2 ts2 = mkVarSet tvs2 fty2 = dataConFieldType con2 label @@ -1277,7 +1279,7 @@ checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2 checkValidDataCon :: TyCon -> DataCon -> TcM () checkValidDataCon tc con = setSrcSpan (srcLocSpan (getSrcLoc con)) $ - addErrCtxt (dataConCtxt con) $ + addErrCtxt (dataConCtxt con) $ do { traceTc "Validity of data con" (ppr con) ; let tc_tvs = tyConTyVars tc res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs) @@ -1297,7 +1299,7 @@ checkValidDataCon tc con ; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con)) } where - ctxt = ConArgCtxt (dataConName con) + ctxt = ConArgCtxt (dataConName con) check_bang (HsUnpackFailed, n) = addWarnTc (cant_unbox_msg n) check_bang _ = return () @@ -1314,7 +1316,7 @@ checkNewDataCon con -- Return type is (T a b c) ; checkTc (null ex_tvs && null theta) (newtypeExError con) -- No existentials - ; checkTc (not (any isBanged (dataConStrictMarks con))) + ; checkTc (not (any isBanged (dataConStrictMarks con))) (newtypeStrictError con) -- No strictness } @@ -1349,7 +1351,7 @@ checkValidClass cls (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls unary = count isTypeVar tyvars == 1 -- Ignore kind variables - check_op constrained_class_methods (sel_id, dm) + check_op constrained_class_methods (sel_id, dm) = addErrCtxt (classOpCtxt sel_id tau) $ do { checkValidTheta ctxt (tail theta) -- The 'tail' removes the initial (C a) from the @@ -1383,14 +1385,14 @@ checkValidClass cls | otherwise = (theta1, mkPhiTy (tail theta1) tau1) -- Ugh! The function might have a type like -- op :: forall a. C a => forall b. (Eq b, Eq a) => tau2 - -- With -XConstrainedClassMethods, we want to allow this, even though the inner - -- forall has an (Eq a) constraint. Whereas in general, each constraint + -- With -XConstrainedClassMethods, we want to allow this, even though the inner + -- forall has an (Eq a) constraint. Whereas in general, each constraint -- in the context of a for-all must mention at least one quantified -- type variable. What a mess! check_at_defs (fam_tc, defs) = do mapM_ (\(ATD _tvs pats rhs _loc) -> checkValidFamInst pats rhs) defs - tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ + tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ mapM_ (check_loc_at_def fam_tc) defs check_loc_at_def fam_tc (ATD _tvs pats _rhs loc) @@ -1401,7 +1403,7 @@ checkValidClass cls -- not the *family* TyVars (there may be more of these) check_arg fam_tc_tv at_ty = checkTc ( not (fam_tc_tv `elem` tyvars) - || mkTyVarTy fam_tc_tv `eqType` at_ty) + || mkTyVarTy fam_tc_tv `eqType` at_ty) (wrongATArgErr at_ty (mkTyVarTy fam_tc_tv)) checkFamFlag :: Name -> TcM () @@ -1445,7 +1447,7 @@ Consider this (Trac #4169): When we typecheck 'ast' we have done the first pass over the class decl (in tcTyClDecls), but we have not yet typechecked the default-method -declarations (becuase they can mention value declarations). So we +declarations (becuase they can mention value declarations). So we must bring the default method Ids into scope first (so they can be seen when typechecking the [d| .. |] quote, and typecheck them later. @@ -1458,7 +1460,7 @@ mkRecSelBinds tycons = ValBindsOut [(NonRecursive, b) | b <- binds] sigs where (sigs, binds) = unzip rec_sels - rec_sels = map mkRecSelBind [ (tc,fld) + rec_sels = map mkRecSelBind [ (tc,fld) | ATyCon tc <- tycons , fld <- tyConFields tc ] @@ -1467,21 +1469,21 @@ mkRecSelBind (tycon, sel_name) = (L sel_loc (IdSig sel_id), unitBag (L sel_loc sel_bind)) where sel_loc = getSrcSpan tycon - sel_id = Var.mkExportedLocalVar rec_details sel_name + sel_id = Var.mkExportedLocalVar rec_details sel_name sel_ty vanillaIdInfo rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty } -- Find a representative constructor, con1 - all_cons = tyConDataCons tycon + all_cons = tyConDataCons tycon cons_w_field = [ con | con <- all_cons - , sel_name `elem` dataConFieldLabels con ] + , sel_name `elem` dataConFieldLabels con ] con1 = ASSERT( not (null cons_w_field) ) head cons_w_field -- Selector type; Note [Polymorphic selectors] field_ty = dataConFieldType con1 sel_name data_ty = dataConOrigResTy con1 data_tvs = tyVarsOfType data_ty - is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs) + is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs) (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors] | otherwise = mkForAllTys (varSetElemsKvsFirst $ @@ -1509,24 +1511,24 @@ mkRecSelBind (tycon, sel_name) -- We do this explicitly so that we get a nice error message that -- mentions this particular record selector deflt | not (any is_unused all_cons) = [] - | otherwise = [mkSimpleMatch [nlWildPat] + | otherwise = [mkSimpleMatch [nlWildPat] (nlHsApp (nlHsVar (getName rEC_SEL_ERROR_ID)) (nlHsLit msg_lit))] -- Do not add a default case unless there are unmatched -- constructors. We must take account of GADTs, else we -- get overlap warning messages from the pattern-match checker - is_unused con = not (con `elem` cons_w_field + is_unused con = not (con `elem` cons_w_field || dataConCannotMatch inst_tys con) inst_tys = tyConAppArgs data_ty unit_rhs = mkLHsTupleExpr [] - msg_lit = HsStringPrim $ mkFastString $ + msg_lit = HsStringPrim $ mkFastString $ occNameString (getOccName sel_name) --------------- tyConFields :: TyCon -> [FieldLabel] -tyConFields tc +tyConFields tc | isAlgTyCon tc = nub (concatMap dataConFieldLabels (tyConDataCons tc)) | otherwise = [] \end{code} @@ -1544,10 +1546,10 @@ from clear that this test should succeed at all! Note [Naughty record selectors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A "naughty" field is one for which we can't define a record +A "naughty" field is one for which we can't define a record selector, because an existential type variable would escape. For example: data T = forall a. MkT { x,y::a } -We obviously can't define +We obviously can't define x (MkT v _) = v Nevertheless we *do* put a RecSelId into the type environment so that if the user tries to use 'x' as a selector we can bleat @@ -1556,10 +1558,10 @@ Hence the sel_naughty flag, to identify record selectors that don't really exist In general, a field is "naughty" if its type mentions a type variable that isn't in the result type of the constructor. Note that this *allows* -GADT record selectors (Note [GADT record selectors]) whose types may look +GADT record selectors (Note [GADT record selectors]) whose types may look like sel :: T [a] -> a -For naughty selectors we make a dummy binding +For naughty selectors we make a dummy binding sel = () for naughty selectors, so that the later type-check will add them to the environment, and they'll be exported. The function is never called, because @@ -1569,7 +1571,7 @@ Note [GADT record selectors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ For GADTs, we require that all constructors with a common field 'f' have the same result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon] -E.g. +E.g. data T where T1 { f :: Maybe a } :: T [a] T2 { f :: Maybe a, y :: b } :: T [a] @@ -1600,7 +1602,7 @@ Note [Selector running example] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It's OK to combine GADTs and type families. Here's a running example: - data instance T [a] where + data instance T [a] where T1 { fld :: b } :: T [Maybe b] The representation type looks like this @@ -1614,7 +1616,7 @@ The selector we want for fld looks like this: fld :: forall b. T [Maybe b] -> b fld = /\b. \(d::T [Maybe b]). - case d `cast` :CoR7T (Maybe b) of + case d `cast` :CoR7T (Maybe b) of T1 (x::b) -> x The scrutinee of the case has type :R7T (Maybe b), which can be @@ -1638,19 +1640,19 @@ tcAddFamInstCtxt :: FamInstDecl Name -> TcM a -> TcM a tcAddFamInstCtxt (FamInstDecl { fid_tycon = tc, fid_defn = defn }) thing_inside = addErrCtxt ctxt thing_inside where - ctxt = hsep [ptext (sLit "In the") <+> pprTyDefnFlavour defn + ctxt = hsep [ptext (sLit "In the") <+> pprTyDefnFlavour defn <+> ptext (sLit "instance declaration for"), quotes (ppr tc)] resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc resultTypeMisMatch field_name con1 con2 - = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, + = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma], nest 2 $ ptext (sLit "but have different result types")] fieldTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc fieldTypeMisMatch field_name con1 con2 - = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, + = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, ptext (sLit "give different types for field"), quotes (ppr field_name)] dataConCtxt :: Outputable a => a -> SDoc @@ -1677,7 +1679,7 @@ classFunDepsErr cls noClassTyVarErr :: Class -> Var -> SDoc noClassTyVarErr clas op = sep [ptext (sLit "The class method") <+> quotes (ppr op), - ptext (sLit "mentions none of the type variables of the class") <+> + ptext (sLit "mentions none of the type variables of the class") <+> ppr clas <+> hsep (map ppr (classTyVars clas))] recSynErr :: [LTyClDecl Name] -> TcRn () @@ -1707,7 +1709,7 @@ badDataConTyCon data_con res_ty_tmpl actual_res_ty badATErr :: Name -> Name -> SDoc badATErr clas op - = hsep [ptext (sLit "Class"), quotes (ppr clas), + = hsep [ptext (sLit "Class"), quotes (ppr clas), ptext (sLit "does not have an associated type"), quotes (ppr op)] badGadtDecl :: Name -> SDoc @@ -1747,7 +1749,7 @@ newtypePredError con newtypeFieldErr :: DataCon -> Int -> SDoc newtypeFieldErr con_name n_flds - = sep [ptext (sLit "The constructor of a newtype must have exactly one field"), + = sep [ptext (sLit "The constructor of a newtype must have exactly one field"), nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds] badSigTyDecl :: Name -> SDoc diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index d8de92f..7785ef5 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -584,6 +584,10 @@ data SynTyConRhs -- | A type synonym family e.g. @type family F x y :: * -> *@ | SynFamilyTyCon + + -- | An injective type synonym family e.g. + -- @injective family F x y :: * -> *@ + | InjFamilyTyCon \end{code} Note [Promoted data constructors] @@ -1132,10 +1136,8 @@ isClosedSynTyCon tycon = isSynTyCon tycon && not (isFamilyTyCon tycon) -- | Injective 'TyCon's can be decomposed, so that -- T ty1 ~ T ty2 => ty1 ~ ty2 isInjectiveTyCon :: TyCon -> Bool +isInjectiveTyCon (SynTyCon {synTcRhs = InjFamilyTyCon}) = True isInjectiveTyCon tc = not (isSynTyCon tc) - -- Ultimately we may have injective associated types - -- in which case this test will become more interesting - -- -- It'd be unusual to call isInjectiveTyCon on a regular H98 -- type synonym, because you should probably have expanded it first -- But regardless, it's not injective! -- 1.7.0.4 From a3ce27ac6f7250eb5ce0a0931d68449eff796f7b Mon Sep 17 00:00:00 2001 From: Will Jones Date: Tue, 17 Apr 2012 15:21:49 +0100 Subject: [PATCH 2/5] Added the InjectiveFamily flavour to HsSyn. --- compiler/deSugar/DsMeta.hs | 5 +++-- compiler/hsSyn/HsDecls.lhs | 12 +++++++----- compiler/typecheck/TcTyClsDecls.lhs | 9 +++++++++ 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs index feccbf7..0ed0023 100644 --- a/compiler/deSugar/DsMeta.hs +++ b/compiler/deSugar/DsMeta.hs @@ -317,8 +317,9 @@ repLFunDep (L _ (xs, ys)) = do xs' <- mapM lookupBinder xs -- represent family declaration flavours -- repFamilyFlavour :: FamilyFlavour -> DsM (Core TH.FamFlavour) -repFamilyFlavour TypeFamily = rep2 typeFamName [] -repFamilyFlavour DataFamily = rep2 dataFamName [] +repFamilyFlavour TypeFamily = rep2 typeFamName [] +repFamilyFlavour InjectiveFamily = notHandled "Exotic family flavour" (ppr InjectiveFamily) +repFamilyFlavour DataFamily = rep2 dataFamName [] -- Represent instance declarations -- diff --git a/compiler/hsSyn/HsDecls.lhs b/compiler/hsSyn/HsDecls.lhs index d573be5..48c6f83 100644 --- a/compiler/hsSyn/HsDecls.lhs +++ b/compiler/hsSyn/HsDecls.lhs @@ -502,6 +502,7 @@ data NewOrData data FamilyFlavour = TypeFamily -- ^ @type family ...@ + | InjectiveFamily -- ^ @injective family ...@ | DataFamily -- ^ @data family ...@ deriving (Data, Typeable) \end{code} @@ -579,6 +580,11 @@ countTyClDecls decls \end{code} \begin{code} +instance Outputable FamilyFlavour where + ppr TypeFamily = ptext (sLit "type family") + ppr InjectiveFamily = ptext (sLit "injective family") + ppr DataFamily = ptext (sLit "data family") + instance OutputableBndr name => Outputable (TyClDecl name) where @@ -587,12 +593,8 @@ instance OutputableBndr name ppr (TyFamily {tcdFlavour = flavour, tcdLName = ltycon, tcdTyVars = tyvars, tcdKindSig = mb_kind}) - = pp_flavour <+> pp_vanilla_decl_head ltycon tyvars [] <+> pp_kind + = ppr flavour <+> pp_vanilla_decl_head ltycon tyvars [] <+> pp_kind where - pp_flavour = case flavour of - TypeFamily -> ptext (sLit "type family") - DataFamily -> ptext (sLit "data family") - pp_kind = case mb_kind of Nothing -> empty Just kind -> dcolon <+> ppr kind diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index b96acb5..0870377 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -505,6 +505,15 @@ tcTyClDecl1 parent _calc_isrec ; tycon <- buildSynTyCon tc_name tvs' SynFamilyTyCon kind parent ; return [ATyCon tycon] } + -- "injective family" declaration +tcTyClDecl1 parent _calc_isrec + (TyFamily {tcdFlavour = InjectiveFamily, tcdLName = L _ tc_name, tcdTyVars = tvs}) + = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do + { traceTc "injective family:" (ppr tc_name) + ; checkFamFlag tc_name + ; tycon <- buildSynTyCon tc_name tvs' InjFamilyTyCon kind parent + ; return [ATyCon tycon] } + -- "data family" declaration tcTyClDecl1 parent _calc_isrec (TyFamily {tcdFlavour = DataFamily, tcdLName = L _ tc_name, tcdTyVars = tvs}) -- 1.7.0.4 From c85a9269f6a6a5c9a0fe0421bd80866557ed0888 Mon Sep 17 00:00:00 2001 From: Will Jones Date: Tue, 17 Apr 2012 15:29:54 +0100 Subject: [PATCH 3/5] Added the ITinjective token and an appropriate parser rule. --- compiler/parser/Lexer.x | 2 ++ compiler/parser/Parser.y.pp | 4 ++++ 2 files changed, 6 insertions(+), 0 deletions(-) diff --git a/compiler/parser/Lexer.x b/compiler/parser/Lexer.x index 378a25c..e99d213 100644 --- a/compiler/parser/Lexer.x +++ b/compiler/parser/Lexer.x @@ -467,6 +467,7 @@ data Token | ITprimcallconv | ITmdo | ITfamily + | ITinjective | ITgroup | ITby | ITusing @@ -641,6 +642,7 @@ reservedWordsFM = listToUFM $ bit inRulePragBit), ( "mdo", ITmdo, bit recursiveDoBit), ( "family", ITfamily, bit tyFamBit), + ( "injective", ITinjective, bit tyFamBit), ( "group", ITgroup, bit transformComprehensionsBit), ( "by", ITby, bit transformComprehensionsBit), ( "using", ITusing, bit transformComprehensionsBit), diff --git a/compiler/parser/Parser.y.pp b/compiler/parser/Parser.y.pp index fc6a950..e3ac395 100644 --- a/compiler/parser/Parser.y.pp +++ b/compiler/parser/Parser.y.pp @@ -241,6 +241,7 @@ incorrect. 'unsafe' { L _ ITunsafe } 'mdo' { L _ ITmdo } 'family' { L _ ITfamily } + 'injective' { L _ ITinjective } 'stdcall' { L _ ITstdcallconv } 'ccall' { L _ ITccallconv } 'capi' { L _ ITcapiconv } @@ -628,6 +629,9 @@ ty_decl :: { LTyClDecl RdrName } -- infix type constructors to be declared {% mkTyFamily (comb3 $1 $3 $4) TypeFamily $3 (unLoc $4) } + | 'injective' 'family' type opt_kind_sig + {% mkTyFamily (comb3 $1 $3 $4) InjectiveFamily $3 (unLoc $4) } + -- ordinary data type or newtype declaration | data_or_newtype capi_ctype tycl_hdr constrs deriving {% mkTyData (comb4 $1 $3 $4 $5) (unLoc $1) $2 $3 -- 1.7.0.4 From eafb9d94c95bcbba605a53b1e2c8abb00337d1a5 Mon Sep 17 00:00:00 2001 From: Will Jones Date: Tue, 17 Apr 2012 17:21:34 +0100 Subject: [PATCH 4/5] Injective family constraints are now decomposable. --- compiler/iface/IfaceSyn.lhs | 8 ++++++-- compiler/main/GHC.hs | 2 +- compiler/main/PprTyThing.hs | 8 +++++--- compiler/typecheck/TcCanonical.lhs | 4 ++-- compiler/types/TyCon.lhs | 5 +++-- 5 files changed, 17 insertions(+), 10 deletions(-) diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs index 326cf3c..1ec6e36 100644 --- a/compiler/iface/IfaceSyn.lhs +++ b/compiler/iface/IfaceSyn.lhs @@ -463,10 +463,14 @@ pprIfaceDecl (IfaceSyn {ifName = tycon, 4 (vcat [equals <+> ppr mono_ty]) pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars, - ifSynRhs = Nothing, ifSynKind = kind }) - = hang (ptext (sLit "type family") <+> pprIfaceDeclHead [] tycon tyvars) + ifSynRhs = Nothing, ifSynKind = kind, + ifInjSyn = inj_syn}) + = hang (pp_type <+> ptext (sLit "family") <+> pprIfaceDeclHead [] tycon tyvars) 4 (dcolon <+> ppr kind) + where + pp_type = ptext (sLit (if inj_syn then "type" else "injective")) + pprIfaceDecl (IfaceData {ifName = tycon, ifCType = cType, ifCtxt = context, ifTyVars = tyvars, ifCons = condecls, diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs index 15e488b..eae39cb 100644 --- a/compiler/main/GHC.hs +++ b/compiler/main/GHC.hs @@ -151,7 +151,7 @@ module GHC ( TyCon, tyConTyVars, tyConDataCons, tyConArity, isClassTyCon, isSynTyCon, isNewTyCon, isPrimTyCon, isFunTyCon, - isFamilyTyCon, tyConClass_maybe, + isFamilyTyCon, isInjectiveTyCon, tyConClass_maybe, synTyConDefn, synTyConType, synTyConResKind, -- ** Type variables diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs index 1ee18f8..f4d0eb8 100644 --- a/compiler/main/PprTyThing.hs +++ b/compiler/main/PprTyThing.hs @@ -116,9 +116,11 @@ pprTyConHdr pefas tyCon GHC.isFunTyCon tyCon = take (GHC.tyConArity tyCon) GHC.alphaTyVars | otherwise = GHC.tyConTyVars tyCon - keyword | GHC.isSynTyCon tyCon = sLit "type" - | GHC.isNewTyCon tyCon = sLit "newtype" - | otherwise = sLit "data" + keyword | GHC.isSynTyCon tyCon + && GHC.isInjectiveTyCon tyCon = sLit "injective" + | GHC.isSynTyCon tyCon = sLit "type" + | GHC.isNewTyCon tyCon = sLit "newtype" + | otherwise = sLit "data" opt_family | GHC.isFamilyTyCon tyCon = ptext (sLit "family") diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index eb642b5..ca25a55 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -810,10 +810,10 @@ canEq d fl ty1 ty2 | Just ty2' <- tcView ty2 = canEq d fl ty1 ty2' canEq d fl ty1@(TyConApp fn tys) ty2 - | isSynFamilyTyCon fn, length tys == tyConArity fn + | isSynFamilyTyCon fn, not (isInjectiveTyCon fn), length tys == tyConArity fn = canEqLeaf d fl ty1 ty2 canEq d fl ty1 ty2@(TyConApp fn tys) - | isSynFamilyTyCon fn, length tys == tyConArity fn + | isSynFamilyTyCon fn, not (isInjectiveTyCon fn), length tys == tyConArity fn = canEqLeaf d fl ty1 ty2 canEq d fl ty1 ty2 diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 7785ef5..2f58bd2 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -1098,8 +1098,7 @@ isSynTyCon _ = False isDecomposableTyCon :: TyCon -> Bool -- True iff we can decompose (T a b c) into ((T a b) c) -- Specifically NOT true of synonyms (open and otherwise) -isDecomposableTyCon (SynTyCon {}) = False -isDecomposableTyCon _other = True +isDecomposableTyCon tc = not (isSynTyCon tc) || isInjectiveTyCon tc -- | Is this an algebraic 'TyCon' declared with the GADT syntax? isGadtSyntaxTyCon :: TyCon -> Bool @@ -1116,12 +1115,14 @@ isEnumerationTyCon _ = False -- | Is this a 'TyCon', synonym or otherwise, that may have further instances appear? isFamilyTyCon :: TyCon -> Bool isFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}}) = True +isFamilyTyCon (SynTyCon {synTcRhs = InjFamilyTyCon {}}) = True isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True isFamilyTyCon _ = False -- | Is this a synonym 'TyCon' that can have may have further instances appear? isSynFamilyTyCon :: TyCon -> Bool isSynFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}}) = True +isSynFamilyTyCon (SynTyCon {synTcRhs = InjFamilyTyCon {}}) = True isSynFamilyTyCon _ = False -- | Is this a synonym 'TyCon' that can have may have further instances appear? -- 1.7.0.4 From f6e2db111214c4aca1ff95b962504c71bd7bd282 Mon Sep 17 00:00:00 2001 From: Will Jones Date: Wed, 18 Apr 2012 15:31:36 +0100 Subject: [PATCH 5/5] Injective families may be used to resolve ambiguity. --- compiler/typecheck/FamInst.lhs | 10 +++++----- compiler/typecheck/TcUnify.lhs | 32 ++++++++++++++++++++++++++++---- compiler/types/FamInstEnv.lhs | 34 ++++++++++++++++++++++++++++++++-- 3 files changed, 65 insertions(+), 11 deletions(-) diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs index e3f646c..586773a 100644 --- a/compiler/typecheck/FamInst.lhs +++ b/compiler/typecheck/FamInst.lhs @@ -50,12 +50,12 @@ check whether the instances in the two modules are consistent, *unless* we can be certain that the instances of the two modules have already been checked for consistency during the compilation of modules that we import. -Why do we need to check? Consider - module X1 where module X2 where - data T1 data T2 +Why do we need to check? Consider + module X1 where module X2 where + data T1 data T2 type instance F T1 b = Int type instance F a T2 = Char - f1 :: F T1 a -> Int f2 :: Char -> F a T2 - f1 x = x f2 x = x + f1 :: F T1 a -> Int f2 :: Char -> F a T2 + f1 x = x f2 x = x Now if we import both X1 and X2 we could make (f2 . f1) :: Int -> Char. Notice that neither instance is an orphan. diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index d22fbda..309bb62 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -43,6 +43,8 @@ module TcUnify ( import HsSyn import TypeRep +import FamInst +import FamInstEnv import TcErrors ( unifyCtxt ) import TcMType import TcIface @@ -604,10 +606,32 @@ uType_np origin orig_ty1 orig_ty2 -- Always defer if a type synonym family (type function) -- is involved. (Data families behave rigidly.) - go ty1@(TyConApp tc1 _) ty2 - | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2 - go ty1 ty2@(TyConApp tc2 _) - | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2 + go ty1@(TyConApp tc1 tys) ty2 + | isSynFamilyTyCon tc1 && isInjectiveTyCon tc1 + = do { envs <- tcGetFamInstEnvs + ; let lhs = lookupFamInstLHS envs tc1 ty2 + ; cos <- + case lhs of + Just (TyConApp _ tys') -> zipWithM (uType origin) tys tys' + _ -> return [] + + ; let co = mkTcTyConAppCo tc1 cos + ; return co + } + | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2 + go ty1 ty2@(TyConApp tc2 tys) + | isSynFamilyTyCon tc2 && isInjectiveTyCon tc2 + = do { envs <- tcGetFamInstEnvs + ; let lhs = lookupFamInstLHS envs tc2 ty1 + ; cos <- + case lhs of + Just (TyConApp _ tys') -> zipWithM (uType origin) tys tys' + _ -> return [] + + ; let co = mkTcTyConAppCo tc2 cos + ; return co + } + | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2 go (TyConApp tc1 tys1) (TyConApp tc2 tys2) -- See Note [Mismatched type lists and application decomposition] diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index c7b9ded..08edb92 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -24,7 +24,8 @@ module FamInstEnv ( identicalFamInst, famInstEnvElts, familyInstances, lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvConflicts', - + lookupFamInstLHS, + -- Normalisation topNormaliseType, normaliseType, normaliseTcApp ) where @@ -36,7 +37,7 @@ import Unify import Type import TypeRep import TyCon -import Coercion +import Coercion hiding (substTy) import VarSet import VarEnv import Name @@ -667,4 +668,33 @@ normaliseType env (ForAllTy tyvar ty1) in (mkForAllCo tyvar coi, ForAllTy tyvar nty1) normaliseType _ ty@(TyVarTy _) = (Refl ty,ty) + +-- |Find the left-hand side of a type family instance declaration that matches +-- with the given type. Such a lookup typically only makes sense when the +-- family in question is injective. +-- +-- For example, given an environment containing the +-- following: +-- +-- > injective family F a :: * +-- > type instance F Int = Bool +-- > type instance F Bool = Int +-- +-- > injective family G a :: * +-- > type instance G a = a +-- +-- @lookupFamInstLHS envs F Bool@ would return @F Int@ and @lookupFamInstLHS +-- envs G Char@ would return @G Char@. +lookupFamInstLHS :: FamInstEnvs -> TyCon -> Type -> Maybe Type +lookupFamInstLHS envs tc ty + = case lhss of + (lhs : _) -> Just lhs + _ -> Nothing + where + lhss = do + fam_inst <- familyInstances envs tc + let co = famInstAxiom fam_inst + case tcUnifyTys instanceBindFun [coAxiomRHS co] [ty] of + Just subst -> [substTy subst (coAxiomLHS co)] + Nothing -> [] \end{code} -- 1.7.0.4