Commit 683a2690 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

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.
parent a12d2d74
......@@ -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
......
......@@ -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.
......
......@@ -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
......
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