X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FTyCon.lhs;h=507bff587698dd37d3538605e427b7f0f37d3d98;hb=786932468faac49aafe20b65eabc8bdf465fbc9d;hp=6f8803c365bdb9465653899d7dae78d84d77d03e;hpb=388e3356f71daffa62f1d4157e1e07e4c68f218a;p=ghc-hetmet.git diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 6f8803c..507bff5 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -8,11 +8,12 @@ The @TyCon@ datatype \begin{code} module TyCon( -- * Main TyCon data types - TyCon, FieldLabel, + TyCon, FieldLabel, AlgTyConRhs(..), visibleDataCons, TyConParent(..), SynTyConRhs(..), + CoTyConDesc(..), AssocFamilyPermutation, -- ** Constructing TyCons @@ -36,9 +37,9 @@ module TyCon( isPrimTyCon, isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, isSynTyCon, isClosedSynTyCon, isOpenSynTyCon, - isSuperKindTyCon, + isSuperKindTyCon, isDecomposableTyCon, isCoercionTyCon, isCoercionTyCon_maybe, - isForeignTyCon, isAnyTyCon, + isForeignTyCon, isAnyTyCon, tyConHasKind, isInjectiveTyCon, isDataTyCon, isProductTyCon, isEnumerationTyCon, @@ -94,9 +95,92 @@ import Maybes import Outputable import FastString import Constants +import Util +import qualified Data.Data as Data import Data.List( elemIndex ) \end{code} +----------------------------------------------- + Notes about type families +----------------------------------------------- + +Type synonym families +~~~~~~~~~~~~~~~~~~~~~~ +* Type synonym families, also known as "type functions", map directly + onto the type functions in FC: + + type family F a :: * + type instance F Int = Bool + ..etc... + +* From the user's point of view (F Int) and Bool are simply equivalent + types. + +* A Haskell 98 type synonym is a degenerate form of a type synonym + family. + +* Type functions can't appear in the LHS of a type function: + type instance F (F Int) = ... -- BAD! + +* In the future we might want to support + * closed type families (esp when we have proper kinds) + * injective type families (allow decomposition) + but we don't at the moment [2010] + +Data type families +~~~~~~~~~~~~~~~~~~ +* Data type families are declared thus + data family T a :: * + data instance T Int = T1 | T2 Bool + data instance T [a] where + X1 :: T [Int] + X2 :: a -> T [a] + +* The user does not see any "equivalent types" as he did with type + synonym families. He just sees constructors with types + T1 :: T Int + T2 :: Bool -> T Int + X1 :: T [Int] + X2 :: a -> T [a] + Note that X2 is a fully-fledged GADT constructor; that's fine + +* The conversion into FC is interesting, and is the point where I was + getting mixed up. Here's the FC version of the above declarations: + + data T a + data TI = T1 | T2 Bool + axiom ax_ti : T Int ~ TI + + data TL a where + X1 :: TL Int + X2 :: a -> TL a + axiom ax_tl :: T [a] ~ TL a + +* Notice that T is NOT translated to a FC type function; it just + becomes a "data type" with no constructors, into which TI, TL, TB + are cast using their respective axioms. + +* As a result + - T behaves just like a data type so far as decomposition is concerned + - It's fine to have T in the LHS of a type function: + type instance F (T a) = [a] + +It was this last point that confused me! The big thing is that you +should not think of a data family T as a *type function* at all, not +even an injective one! We can't allow even injective type functions +on the LHS of a type function: + type family injective G a :: * + type instance F (G Int) = Bool +is no good, even if G is injective, because consider + type instance G Int = Bool + type instance F Bool = Char + +So a data type family is not an injective type function. It's just a +data type with some axioms that connect it to other data types. These +axioms come into play when (and only when) you + - use a data constructor + - do pattern matching + %************************************************************************ %* * \subsection{The data type} @@ -124,7 +208,7 @@ data TyCon FunTyCon { tyConUnique :: Unique, tyConName :: Name, - tyConKind :: Kind, + tc_kind :: Kind, tyConArity :: Arity } @@ -133,7 +217,7 @@ data TyCon | AlgTyCon { tyConUnique :: Unique, tyConName :: Name, - tyConKind :: Kind, + tc_kind :: Kind, tyConArity :: Arity, tyConTyVars :: [TyVar], -- ^ The type variables used in the type constructor. @@ -171,7 +255,7 @@ data TyCon | TupleTyCon { tyConUnique :: Unique, tyConName :: Name, - tyConKind :: Kind, + tc_kind :: Kind, tyConArity :: Arity, tyConBoxed :: Boxity, tyConTyVars :: [TyVar], @@ -183,7 +267,7 @@ data TyCon | SynTyCon { tyConUnique :: Unique, tyConName :: Name, - tyConKind :: Kind, + tc_kind :: Kind, tyConArity :: Arity, tyConTyVars :: [TyVar], -- Bound tyvars @@ -199,14 +283,14 @@ data TyCon | PrimTyCon { tyConUnique :: Unique, tyConName :: Name, - tyConKind :: Kind, + tc_kind :: Kind, tyConArity :: Arity, -- SLPJ Oct06: I'm not sure what the significance -- of the arity of a primtycon is! primTyConRep :: PrimRep, -- ^ Many primitive tycons are unboxed, but some are -- boxed (represented by pointers). This 'PrimRep' holds -- that information. - -- Only relevant if tyConKind = * + -- Only relevant if tc_kind = * isUnLifted :: Bool, -- ^ Most primitive tycons are unlifted (may not contain bottom) -- but foreign-imported ones may be lifted @@ -216,18 +300,14 @@ data TyCon } -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@. - -- INVARIANT: coercions are always fully applied - | CoercionTyCon { + -- INVARIANT: Coercion TyCons are always fully applied + -- But note that a CoTyCon can be *over*-saturated in a type. + -- E.g. (sym g1) Int will be represented as (TyConApp sym [g1,Int]) + | CoTyCon { tyConUnique :: Unique, tyConName :: Name, tyConArity :: Arity, - coKindFun :: [Type] -> (Type,Type) - -- ^ Function that when given a list of the type arguments to the 'TyCon' - -- constructs the types that the resulting coercion relates. - -- - -- INVARIANT: 'coKindFun' is always applied to exactly 'tyConArity' args - -- E.g. for @trans (c1 :: ta=tb) (c2 :: tb=tc)@, the 'coKindFun' returns - -- the kind as a pair of types: @(ta, tc)@ + coTcDesc :: CoTyConDesc } -- | Any types. Like tuples, this is a potentially-infinite family of TyCons @@ -239,7 +319,7 @@ data TyCon | AnyTyCon { tyConUnique :: Unique, tyConName :: Name, - tyConKind :: Kind -- Never = *; that is done via PrimTyCon + tc_kind :: Kind -- Never = *; that is done via PrimTyCon -- See Note [Any types] in TysPrim } @@ -311,7 +391,7 @@ data AlgTyConRhs -- See Note [Newtype eta] - nt_co :: Maybe TyCon -- ^ A 'TyCon' (which is always a 'CoercionTyCon') that can have a 'Coercion' + nt_co :: Maybe TyCon -- ^ A 'TyCon' (which is always a 'CoTyCon') that can have a 'Coercion' -- extracted from it to create the @newtype@ from the representation 'Type'. -- -- This field is optional for non-recursive @newtype@s only. @@ -364,19 +444,13 @@ data TyConParent -- of the current 'TyCon' (not the family one). INVARIANT: -- the number of types matches the arity of the family 'TyCon' -- - -- 3) A 'CoercionTyCon' identifying the representation + -- 3) A 'CoTyCon' identifying the representation -- type with the type instance family - | FamilyTyCon + | FamilyTyCon -- See Note [Data type families] TyCon [Type] TyCon -- 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 -- | Checks the invariants of a 'TyConParent' given the appropriate type class name, if any okParent :: Name -> TyConParent -> Bool @@ -396,6 +470,20 @@ data SynTyConRhs | SynonymTyCon Type -- ^ The synonym mentions head type variables. It acts as a -- template for the expansion when the 'TyCon' is applied to some -- types. + +-------------------- +data CoTyConDesc + = CoSym | CoTrans + | CoLeft | CoRight + | CoCsel1 | CoCsel2 | CoCselR + | CoInst + + | CoAxiom -- C tvs : F lhs-tys ~ rhs-ty + { co_ax_tvs :: [TyVar] + , co_ax_lhs :: Type + , co_ax_rhs :: Type } + + | CoUnsafe \end{code} Note [Newtype coercions] @@ -407,7 +495,7 @@ newtype, to the newtype itself. For example, newtype T a = MkT (a -> a) the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> -t. This TyCon is a CoercionTyCon, so it does not have a kind on its +t. This TyCon is a CoTyCon, so it does not have a kind on its own; it basically has its own typing rule for the fully-applied version. If the newtype T has k type variables then CoT has arity at most k. In the case that the right hand side is a type application @@ -425,7 +513,7 @@ and then when we used CoT at a particular type, s, we'd say CoT @ s which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s]) -But in GHC we instead make CoT into a new piece of type syntax, CoercionTyCon, +But in GHC we instead make CoT into a new piece of type syntax, CoTyCon, (like instCoercionTyCon, symCoercionTyCon etc), which must always be saturated, but which encodes as TyConApp CoT [s] @@ -472,34 +560,42 @@ so the coercion tycon CoT must have and arity: 0 -Note [Indexed data types] (aka data type families) -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - See also Note [Wrappers for data instance tycons] in MkId.lhs +Note [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) + T2 :: T (Int,Bool) + +Notice that the 'data instance' can be a fully-fledged GADT -Then - * T is the "family TyCon" + * T is the "family TyCon". It is a data type + whose AlgTyConRhs is OpenTyCon - * We make "representation TyCon" :R1T, thus: + * For each 'data instance' we make "representation TyCon" + :R1T, thus: data :R1T b c where T1 :: forall b c. b -> c -> :R1T b c + T1 :: :R1T Int Bool + We have a bit of work to do, to unpick the result types of the + data instance declaration to get the result type in the + representation; e.g. T (Int,Bool) --> :R1T Int Bool - * It has a top-level coercion connecting it to the family TyCon + * We defind 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): + * 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 + * The representation TyCon, :R1T, has an AlgTyConParent of FamilyTyCon T [(b,c)] :Co:R1T @@ -578,7 +674,7 @@ mkFunTyCon name kind = FunTyCon { tyConUnique = nameUnique name, tyConName = name, - tyConKind = kind, + tc_kind = kind, tyConArity = 2 } @@ -598,7 +694,7 @@ mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn = AlgTyCon { tyConName = name, tyConUnique = nameUnique name, - tyConKind = kind, + tc_kind = kind, tyConArity = length tyvars, tyConTyVars = tyvars, algTcStupidTheta = stupid, @@ -626,7 +722,7 @@ mkTupleTyCon name kind arity tyvars con boxed gen_info = TupleTyCon { tyConUnique = nameUnique name, tyConName = name, - tyConKind = kind, + tc_kind = kind, tyConArity = arity, tyConBoxed = boxed, tyConTyVars = tyvars, @@ -647,7 +743,7 @@ mkForeignTyCon name ext_name kind arity = PrimTyCon { tyConName = name, tyConUnique = nameUnique name, - tyConKind = kind, + tc_kind = kind, tyConArity = arity, primTyConRep = PtrRep, -- they all do isUnLifted = False, @@ -675,7 +771,7 @@ mkPrimTyCon' name kind arity rep is_unlifted = PrimTyCon { tyConName = name, tyConUnique = nameUnique name, - tyConKind = kind, + tc_kind = kind, tyConArity = arity, primTyConRep = rep, isUnLifted = is_unlifted, @@ -688,7 +784,7 @@ mkSynTyCon name kind tyvars rhs parent = SynTyCon { tyConName = name, tyConUnique = nameUnique name, - tyConKind = kind, + tc_kind = kind, tyConArity = length tyvars, tyConTyVars = tyvars, synTcRhs = rhs, @@ -696,19 +792,20 @@ mkSynTyCon name kind tyvars rhs parent } -- | Create a coercion 'TyCon' -mkCoercionTyCon :: Name -> Arity -> ([Type] -> (Type,Type)) -> TyCon -mkCoercionTyCon name arity kindRule - = CoercionTyCon { - tyConName = name, +mkCoercionTyCon :: Name -> Arity + -> CoTyConDesc + -> TyCon +mkCoercionTyCon name arity desc + = CoTyCon { + tyConName = name, tyConUnique = nameUnique name, - tyConArity = arity, - coKindFun = kindRule - } + tyConArity = arity, + coTcDesc = desc } mkAnyTyCon :: Name -> Kind -> TyCon mkAnyTyCon name kind - = AnyTyCon { tyConName = name, - tyConKind = kind, + = AnyTyCon { tyConName = name, + tc_kind = kind, tyConUnique = nameUnique name } -- | Create a super-kind 'TyCon' @@ -823,6 +920,13 @@ isClosedSynTyCon tycon = isSynTyCon tycon && not (isOpenTyCon tycon) isOpenSynTyCon :: TyCon -> Bool isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon +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) and coercions +isDecomposableTyCon (SynTyCon {}) = False +isDecomposableTyCon (CoTyCon {}) = False +isDecomposableTyCon _other = True + -- | Is this an algebraic 'TyCon' declared with the GADT syntax? isGadtSyntaxTyCon :: TyCon -> Bool isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res @@ -831,6 +935,7 @@ isGadtSyntaxTyCon _ = False -- | Is this an algebraic 'TyCon' which is just an enumeration of values? isEnumerationTyCon :: TyCon -> Bool isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res +isEnumerationTyCon (TupleTyCon {tyConArity = arity}) = arity == 0 isEnumerationTyCon _ = False -- | Is this a 'TyCon', synonym or otherwise, that may have further instances appear? @@ -938,15 +1043,15 @@ isAnyTyCon _ = False -- | Attempt to pull a 'TyCon' apart into the arity and 'coKindFun' of -- a coercion 'TyCon'. Returns @Nothing@ if the 'TyCon' is not of the -- appropriate kind -isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, [Type] -> (Type,Type)) -isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule}) - = Just (ar, rule) +isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, CoTyConDesc) +isCoercionTyCon_maybe (CoTyCon {tyConArity = ar, coTcDesc = desc}) + = Just (ar, desc) isCoercionTyCon_maybe _ = Nothing -- | Is this a 'TyCon' that represents a coercion? isCoercionTyCon :: TyCon -> Bool -isCoercionTyCon (CoercionTyCon {}) = True -isCoercionTyCon _ = False +isCoercionTyCon (CoTyCon {}) = True +isCoercionTyCon _ = False -- | Identifies implicit tycons that, in particular, do not go into interface -- files (because they are implicitly reconstructed when the interface is @@ -966,7 +1071,7 @@ isImplicitTyCon tycon | isTyConAssoc tycon = True isTupleTyCon tycon isImplicitTyCon _other = True -- catches: FunTyCon, PrimTyCon, - -- CoercionTyCon, SuperKindTyCon + -- CoTyCon, SuperKindTyCon \end{code} @@ -1023,6 +1128,20 @@ tyConHasGenerics (AlgTyCon {hasGenerics = hg}) = hg tyConHasGenerics (TupleTyCon {hasGenerics = hg}) = hg tyConHasGenerics _ = False -- Synonyms +tyConKind :: TyCon -> Kind +tyConKind (FunTyCon { tc_kind = k }) = k +tyConKind (AlgTyCon { tc_kind = k }) = k +tyConKind (TupleTyCon { tc_kind = k }) = k +tyConKind (SynTyCon { tc_kind = k }) = k +tyConKind (PrimTyCon { tc_kind = k }) = k +tyConKind (AnyTyCon { tc_kind = k }) = k +tyConKind tc = pprPanic "tyConKind" (ppr tc) -- SuperKindTyCon and CoTyCon + +tyConHasKind :: TyCon -> Bool +tyConHasKind (SuperKindTyCon {}) = False +tyConHasKind (CoTyCon {}) = False +tyConHasKind _ = True + -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors -- could be found tyConDataCons :: TyCon -> [DataCon] @@ -1051,8 +1170,9 @@ tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other) -- | Extract an 'AlgTyConRhs' with information about data constructors from an algebraic or tuple -- 'TyCon'. Panics for any other sort of 'TyCon' algTyConRhs :: TyCon -> AlgTyConRhs -algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs -algTyConRhs (TupleTyCon {dataCon = con}) = DataTyCon { data_cons = [con], is_enum = False } +algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs +algTyConRhs (TupleTyCon {dataCon = con, tyConArity = arity}) + = DataTyCon { data_cons = [con], is_enum = arity == 0 } algTyConRhs other = pprPanic "algTyConRhs" (ppr other) \end{code} @@ -1199,9 +1319,30 @@ instance Ord TyCon where instance Uniquable TyCon where getUnique tc = tyConUnique tc +instance Outputable CoTyConDesc where + ppr CoSym = ptext (sLit "SYM") + ppr CoTrans = ptext (sLit "TRANS") + ppr CoLeft = ptext (sLit "LEFT") + ppr CoRight = ptext (sLit "RIGHT") + ppr CoCsel1 = ptext (sLit "CSEL1") + ppr CoCsel2 = ptext (sLit "CSEL2") + ppr CoCselR = ptext (sLit "CSELR") + ppr CoInst = ptext (sLit "INST") + ppr CoUnsafe = ptext (sLit "UNSAFE") + ppr (CoAxiom {}) = ptext (sLit "AXIOM") + instance Outputable TyCon where ppr tc = ppr (getName tc) instance NamedThing TyCon where getName = tyConName + +instance Data.Typeable TyCon where + typeOf _ = Data.mkTyConApp (Data.mkTyCon "TyCon") [] + +instance Data.Data TyCon where + -- don't traverse? + toConstr _ = abstractConstr "TyCon" + gunfold _ _ = error "gunfold" + dataTypeOf _ = mkNoRepType "TyCon" \end{code}