From 683a26900e9170ba57c561a2dc94a3a4eb38cfdf Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Wed, 2 May 2007 10:28:11 +0000 Subject: [PATCH] Fixes to data type families - Fix two distinct bugs, one in MkId.mkDataConIds, one in DataCon.mkDataCon - Add more comments - Add a little assertion checking in TyCon Type-family tests now work. --- compiler/basicTypes/DataCon.lhs | 18 +++++++---- compiler/basicTypes/MkId.lhs | 48 +++++++++++++++-------------- compiler/types/TyCon.lhs | 63 ++++++++++++++++++++++++++++++++++----- 3 files changed, 94 insertions(+), 35 deletions(-) diff --git a/compiler/basicTypes/DataCon.lhs b/compiler/basicTypes/DataCon.lhs index ee2c685..a3504a6 100644 --- a/compiler/basicTypes/DataCon.lhs +++ b/compiler/basicTypes/DataCon.lhs @@ -246,6 +246,8 @@ data DataCon -- The declaration format is held in the TyCon (algTcGadtSyntax) dcUnivTyVars :: [TyVar], -- Universally-quantified type vars + -- INVARIANT: length matches arity of the dcRepTyCon + dcExTyVars :: [TyVar], -- Existentially-quantified type vars -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS -- FOR THE PARENT TyCon. With GADTs the data con might not even have @@ -484,20 +486,24 @@ mkDataCon name declared_infix real_stricts = map mk_dict_strict_mark theta ++ arg_stricts -- Example - -- data instance T [a] where - -- TI :: forall b. b -> T [Maybe b] + -- data instance T (b,c) where + -- TI :: forall e. e -> T (e,e) + -- -- The representation tycon looks like this: - -- data :R7T a where - -- TI :: forall b c. (c :=: Maybe b) b -> :R7T c + -- data :R7T b c where + -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1 + orig_res_ty | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tycon - , let fam_subst = zipTopTvSubst (tyConTyVars fam_tc) res_tys + , let fam_subst = zipTopTvSubst (tyConTyVars tycon) res_tys = mkTyConApp fam_tc (substTys fam_subst fam_tys) | otherwise = mkTyConApp tycon res_tys where res_tys = substTyVars (mkTopTvSubst eq_spec) univ_tvs - -- In the example above, res_tys is a singleton, (Maybe b) + -- In the example above, + -- univ_tvs = [ b1, c1 ] + -- res_tys = [ b1, b1 ] -- Representation arguments and demands -- To do: eliminate duplication with MkId diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index 6f664da..42515eb 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/compiler/basicTypes/MkId.lhs @@ -181,10 +181,12 @@ tyConFamilyCoercion_maybe and has kind The wrapper and worker of MapPair get the types + -- Wrapper $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v - $WMapPair a b v = $wMapPair a b v `cast` sym (Co123Map a b v) + $WMapPair a b v = MapPair a b v `cast` sym (Co123Map a b v) - $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v + -- Worker + MapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v This coercion is conditionally applied by wrapFamInstBody. @@ -197,11 +199,13 @@ Hence Now we want + -- Wrapper $WT1 :: forall b. b -> T [Maybe b] - $WT1 a b v = $wT1 b (Maybe b) (Maybe b) + $WT1 b v = T1 (Maybe b) b (Maybe b) v `cast` sym (Co7T (Maybe b)) - $wT1 :: forall b c. (b ~ Maybe c) => b -> :R7T c + -- Worker + T1 :: forall c b. (c ~ Maybe b) => b -> :R7T c \begin{code} mkDataConIds :: Name -> Name -> DataCon -> DataConIds @@ -220,19 +224,7 @@ mkDataConIds wrap_name wkr_name data_con where (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, res_ty) = dataConFullSig data_con - res_ty_args = tyConAppArgs res_ty - tycon = dataConTyCon data_con - - ----------- Wrapper -------------- - -- We used to include the stupid theta in the wrapper's args - -- but now we don't. Instead the type checker just injects these - -- extra constraints where necessary. - wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs - dict_tys = mkPredTys theta - wrap_ty = mkForAllTys wrap_tvs $ mkFunTys dict_tys $ - mkFunTys orig_arg_tys $ res_ty - -- NB: watch out here if you allow user-written equality - -- constraints in data constructor signatures + tycon = dataConTyCon data_con -- The representation TyCon (not family) ----------- Worker (algebraic data types only) -------------- -- The *worker* for the data constructor is the function that @@ -289,13 +281,25 @@ mkDataConIds wrap_name wkr_name data_con id_arg1 = mkTemplateLocal 1 (head orig_arg_tys) + ----------- Wrapper -------------- + -- We used to include the stupid theta in the wrapper's args + -- but now we don't. Instead the type checker just injects these + -- extra constraints where necessary. + wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs + res_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs + dict_tys = mkPredTys theta + wrap_ty = mkForAllTys wrap_tvs $ mkFunTys dict_tys $ + mkFunTys orig_arg_tys $ res_ty + -- NB: watch out here if you allow user-written equality + -- constraints in data constructor signatures + ----------- Wrappers for algebraic data types -------------- alg_wrap_id = mkGlobalId (DataConWrapId data_con) wrap_name wrap_ty alg_wrap_info alg_wrap_info = noCafIdInfo -- The NoCaf-ness is set by noCafIdInfo - `setArityInfo` alg_arity + `setArityInfo` wrap_arity -- It's important to specify the arity, so that partial -- applications are treated as values - `setUnfoldingInfo` alg_unf + `setUnfoldingInfo` wrap_unf `setAllStrictnessInfo` Just wrap_sig all_strict_marks = dataConExStricts data_con ++ dataConStrictMarks data_con @@ -312,7 +316,7 @@ mkDataConIds wrap_name wkr_name data_con -- ...(let w = C x in ...(w p q)...)... -- we want to see that w is strict in its two arguments - alg_unf = mkTopUnfolding $ Note InlineMe $ + wrap_unf = mkTopUnfolding $ Note InlineMe $ mkLams wrap_tvs $ mkLams dict_args $ mkLams id_args $ foldr mk_case con_app @@ -327,7 +331,7 @@ mkDataConIds wrap_name wkr_name data_con (dict_args,i2) = mkLocals 1 dict_tys (id_args,i3) = mkLocals i2 orig_arg_tys - alg_arity = i3-1 + wrap_arity = i3-1 mk_case :: (Id, StrictnessMark) -- Arg, strictness @@ -1127,7 +1131,7 @@ seqId -- not from GHC.Base.hi. This is important, because the strictness -- analyser will spot it as strict! -- --- Also no unfolding in lazyId: it gets "inlined" by a HACK in the worker/wrapper pass +-- Also no unfolding in lazyId: it gets "inlined" by a HACK in the worker/wrapperpass -- (see WorkWrap.wwExpr) -- We could use inline phases to do this, but that would be vulnerable to changes in -- phase numbering....we must inline precisely after strictness analysis. diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index cf2de89..50d76cf 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -204,7 +204,13 @@ data AlgTyConRhs -- The constructor represents an open family without a fixed right hand -- side. Additional instances can appear at any time. - -- + -- + -- These are introduced by either a top level decl: + -- data T a :: * + -- or an assoicated data type decl, in a class decl: + -- class C a b where + -- data T b :: * + | OpenTyCon { otArgPoss :: Maybe [Int], @@ -267,31 +273,41 @@ visibleDataCons OpenTyCon {} = [] visibleDataCons (DataTyCon{ data_cons = cs }) = cs visibleDataCons (NewTyCon{ data_con = c }) = [c] --- Both type classes as well as family instances imply implicit type --- constructors. These implicit type constructors refer to their parent +-- Both type classes as well as family instances imply implicit +-- type constructors. These implicit type constructors refer to their parent -- structure (ie, the class or family from which they derive) using a type of -- the following form. We use `TyConParent' for both algebraic and synonym -- types, but the variant `ClassTyCon' will only be used by algebraic tycons. --- + data TyConParent = NoParentTyCon -- An ordinary type constructor has no parent. | ClassTyCon -- Type constructors representing a class dictionary. - Class + Class -- INVARIANT: the classTyCon of this Class is the current tycon | FamilyTyCon -- Type constructors representing an instance of a type TyCon -- The type family [Type] -- Instance types; free variables are the tyConTyVars - -- of this TyCon + -- of the current TyCon (not the family one) + -- INVARIANT: the number of types matches the arity + -- of the family tycon TyCon -- A CoercionTyCon identifying the representation -- type with the type instance family. -- c.f. Note [Newtype coercions] + + -- -- E.g. data intance T [a] = ... -- gives a representation tycon: -- data :R7T a = ... -- axiom co a :: T [a] ~ :R7T a -- with :R7T's algTcParent = FamilyTyCon T [a] co +okParent :: Name -> TyConParent -> Bool -- Checks invariants +okParent tc_name NoParentTyCon = True +okParent tc_name (ClassTyCon cls) = tyConName (classTyCon cls) == tc_name +okParent tc_name (FamilyTyCon fam_tc tys co_tc) = tyConArity fam_tc == length tys + +-------------------- data SynTyConRhs = OpenSynTyCon Kind -- Type family: *result* kind given (Maybe [Int]) -- for associated families: for each tyvars in @@ -373,6 +389,39 @@ we get: And now Lint complains unless Foo T == Foo [], and that requires T==[] +Note [Indexed data types] (aka data type families) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + See also Note [Wrappers for data instance tycons] in MkId.lhs + +Consider + data family T a + + data instance T (b,c) where + T1 :: b -> c -> T (b,c) + +Then + * T is the "family TyCon" + + * We make "representation TyCon" :R1T, thus: + data :R1T b c where + T1 :: forall b c. b -> c -> :R1T b c + + * It has a top-level coercion connecting it to the family TyCon + + axiom :Co:R1T b c : T (b,c) ~ :R1T b c + + * The data contructor T1 has a wrapper (which is what the source-level + "T1" invokes): + + $WT1 :: forall b c. b -> c -> T (b,c) + $WT1 b c (x::b) (y::c) = T1 b c x y `cast` sym (:Co:R1T b c) + + * The representation TyCon :R1T has an AlgTyConParent of + + FamilyTyCon T [(b,c)] :Co:R1T + + + %************************************************************************ %* * \subsection{PrimRep} @@ -445,7 +494,7 @@ mkAlgTyCon name kind tyvars stupid rhs sel_ids parent is_rec gen_info gadt_syn algTcStupidTheta = stupid, algTcRhs = rhs, algTcSelIds = sel_ids, - algTcParent = parent, + algTcParent = ASSERT( okParent name parent ) parent, algTcRec = is_rec, algTcGadtSyntax = gadt_syn, hasGenerics = gen_info -- 1.7.10.4