X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FTyCon.lhs;h=507bff587698dd37d3538605e427b7f0f37d3d98;hb=111bc9a9a9bd0ae96b0ee1e261abac4ddd48c0e1;hp=43fb5242979e5039dddb90be2cc2653ab7f17712;hpb=cd0e2c0cc3005c3f5e74eeda57dc9cebbe1bac7e;p=ghc-hetmet.git diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 43fb524..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, CoTyConKindChecker, + TyCon, FieldLabel, AlgTyConRhs(..), visibleDataCons, TyConParent(..), SynTyConRhs(..), + CoTyConDesc(..), AssocFamilyPermutation, -- ** Constructing TyCons @@ -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} @@ -199,7 +283,7 @@ data TyCon | PrimTyCon { tyConUnique :: Unique, tyConName :: Name, - tc_kind :: Kind, + tc_kind :: Kind, tyConArity :: Arity, -- SLPJ Oct06: I'm not sure what the significance -- of the arity of a primtycon is! @@ -217,13 +301,13 @@ data TyCon -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@. -- INVARIANT: Coercion TyCons are always fully applied - -- But note that a CoercionTyCon can be over-saturated in a type. + -- 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]) - | CoercionTyCon { + | CoTyCon { tyConUnique :: Unique, tyConName :: Name, tyConArity :: Arity, - coKindFun :: CoTyConKindChecker + coTcDesc :: CoTyConDesc } -- | Any types. Like tuples, this is a potentially-infinite family of TyCons @@ -250,23 +334,6 @@ data TyCon tyConName :: Name } -type CoTyConKindChecker = forall m. Monad m => CoTyConKindCheckerFun m - -type CoTyConKindCheckerFun m - = (Type -> m Kind) -- Kind checker for types - -> (Type -> m (Type,Type)) -- and for coercions - -> Bool -- True => apply consistency checks - -> [Type] -- Exactly right number of args - -> m (Type, Type) -- Kind of this application - - -- ^ Function that when given a list of the type arguments to the 'TyCon' - -- constructs the types that the resulting coercion relates. - -- Returns Nothing if ill-kinded. - -- - -- 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)@ - -- | Names of the fields in an algebraic record type type FieldLabel = Name @@ -324,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. @@ -377,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 @@ -409,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] @@ -420,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 @@ -438,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] @@ -485,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) -Then - * T is the "family TyCon" +Notice that the 'data instance' can be a fully-fledged GADT - * We make "representation TyCon" :R1T, thus: + * T is the "family TyCon". It is a data type + whose AlgTyConRhs is OpenTyCon + + * 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 @@ -710,21 +793,14 @@ mkSynTyCon name kind tyvars rhs parent -- | Create a coercion 'TyCon' mkCoercionTyCon :: Name -> Arity - -> CoTyConKindChecker + -> CoTyConDesc -> TyCon -mkCoercionTyCon name arity rule_fn - = CoercionTyCon { +mkCoercionTyCon name arity desc + = CoTyCon { tyConName = name, tyConUnique = nameUnique name, tyConArity = arity, -#ifdef DEBUG - coKindFun = \ ty co fail args -> - ASSERT2( length args == arity, ppr name ) - rule_fn ty co fail args -#else - coKindFun = rule_fn -#endif - } + coTcDesc = desc } mkAnyTyCon :: Name -> Kind -> TyCon mkAnyTyCon name kind @@ -799,11 +875,6 @@ isNewTyCon :: TyCon -> Bool isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True isNewTyCon _ = False -tyConHasKind :: TyCon -> Bool -tyConHasKind (SuperKindTyCon {}) = False -tyConHasKind (CoercionTyCon {}) = False -tyConHasKind _ = True - -- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it expands -- into, and (possibly) a coercion from the representation type to the @newtype@. -- Returns @Nothing@ if this is not possible. @@ -850,11 +921,11 @@ isOpenSynTyCon :: TyCon -> Bool isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon isDecomposableTyCon :: TyCon -> Bool --- True iff we can deocmpose (T a b c) into ((T a b) c) +-- 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 (CoercionTyCon {}) = False -isDecomposableTyCon _other = True +isDecomposableTyCon (SynTyCon {}) = False +isDecomposableTyCon (CoTyCon {}) = False +isDecomposableTyCon _other = True -- | Is this an algebraic 'TyCon' declared with the GADT syntax? isGadtSyntaxTyCon :: TyCon -> Bool @@ -864,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? @@ -971,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 :: Monad m => TyCon -> Maybe (Arity, CoTyConKindCheckerFun m) -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 @@ -999,7 +1071,7 @@ isImplicitTyCon tycon | isTyConAssoc tycon = True isTupleTyCon tycon isImplicitTyCon _other = True -- catches: FunTyCon, PrimTyCon, - -- CoercionTyCon, SuperKindTyCon + -- CoTyCon, SuperKindTyCon \end{code} @@ -1063,7 +1135,12 @@ 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) +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 @@ -1093,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} @@ -1241,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}