-- 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
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
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.
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
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
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
-- ...(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
(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
-- 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.
-- 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],
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
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}
algTcStupidTheta = stupid,
algTcRhs = rhs,
algTcSelIds = sel_ids,
- algTcParent = parent,
+ algTcParent = ASSERT( okParent name parent ) parent,
algTcRec = is_rec,
algTcGadtSyntax = gadt_syn,
hasGenerics = gen_info
projects / ghc-hetmet.git / commitdiff