tyConPrimRep,
AlgTyConRhs(..), visibleDataCons,
+ SynTyConRhs(..),
isFunTyCon, isUnLiftedTyCon, isProductTyCon,
isAlgTyCon, isDataTyCon, isSynTyCon, isNewTyCon, isPrimTyCon,
- isEnumerationTyCon, isGadtSyntaxTyCon,
+ isEnumerationTyCon, isGadtSyntaxTyCon, isOpenTyCon,
isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, tupleTyConBoxity,
isRecursiveTyCon, newTyConRep, newTyConRhs, newTyConCo,
isHiBootTyCon, isSuperKindTyCon,
tyConStupidTheta,
tyConArity,
isClassTyCon, tyConClass_maybe,
- synTyConDefn, synTyConRhs,
+ synTyConDefn, synTyConRhs, synTyConType, synTyConResKind,
tyConExtName, -- External name for foreign types
maybeTyConSingleCon,
tyConKind :: Kind,
tyConArity :: Arity,
- tyConTyVars :: [TyVar], -- Scopes over (a) the [PredType] in AlgTyConRhs.DataTyCon
- -- (b) the cached types in AlgTyConRhs.NewTyCon
+ tyConTyVars :: [TyVar], -- Scopes over (a) the algTcStupidTheta
+ -- (b) the cached types in
+ -- algTyConRhs.NewTyCon
-- But not over the data constructors
- algTcSelIds :: [Id], -- Its record selectors (empty if none):
+ algTcSelIds :: [Id], -- Its record selectors (empty if none)
algTcGadtSyntax :: Bool, -- True <=> the data type was declared using GADT syntax
-- That doesn't mean it's a true GADT; only that the "where"
algTcRhs :: AlgTyConRhs, -- Data constructors in here
- algTcRec :: RecFlag, -- Tells whether the data type is part of
- -- a mutually-recursive group or not
+ algTcRec :: RecFlag, -- Tells whether the data type is part
+ -- of a mutually-recursive group or not
hasGenerics :: Bool, -- True <=> generic to/from functions are available
-- (in the exports of the data type's source module)
tyConArity :: Arity,
tyConTyVars :: [TyVar], -- Bound tyvars
- synTcRhs :: Type -- Right-hand side, mentioning these type vars.
- -- Acts as a template for the expansion when
- -- the tycon is applied to some types.
+ synTcRhs :: SynTyConRhs -- Expanded type in here
}
| PrimTyCon { -- Primitive types; cannot be defined in Haskell
-- Used when we export a data type abstractly into
-- an hi file
+ | OpenDataTyCon -- data family (further instances can appear
+ | OpenNewTyCon -- newtype family at any time)
+
| DataTyCon {
data_cons :: [DataCon],
-- The constructors; can be empty if the user declares
visibleDataCons :: AlgTyConRhs -> [DataCon]
visibleDataCons AbstractTyCon = []
+visibleDataCons OpenDataTyCon = []
+visibleDataCons OpenNewTyCon = []
visibleDataCons (DataTyCon{ data_cons = cs }) = cs
visibleDataCons (NewTyCon{ data_con = c }) = [c]
+
+data SynTyConRhs
+ = OpenSynTyCon Kind -- Type family: *result* kind given
+ | SynonymTyCon Type -- Mentioning head type vars. Acts as a template for
+ -- the expansion when the tycon is applied to some
+ -- types.
\end{code}
Note [Newtype coercions]
which is used for coercing from the representation type of the
newtype, to the newtype itself. For example,
- newtype T a = MkT [a]
+ 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
+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
+ending with the same type variables as the left hand side, we
+"eta-contract" the coercion. So if we had
+
+ newtype S a = MkT [a]
-the NewTyCon for T will contain nt_co = CoT where CoT t : [t] :=: T t.
-This TyCon is a CoercionTyCon, 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 k.
+then we would generate the arity 0 coercion CoS : S :=: []. The
+primary reason we do this is to make newtype deriving cleaner.
In the paper we'd write
- axiom CoT : (forall t. [t]) :=: (forall t. T t)
+ axiom CoT : (forall t. T t) :=: (forall t. [t])
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
(like instCoercionTyCon, symCoercionTyCon etc), which must always
be saturated, but which encodes as
- TyConAp CoT [s]
+ TyConApp CoT [s]
In the vocabulary of the paper it's as if we had axiom declarations
like
- axiom CoT t : ([t] :=: T t)
+ axiom CoT t : T t :=: [t]
Note [Newtype eta]
~~~~~~~~~~~~~~~~~~
-- unboxed tuples
isDataTyCon tc@(AlgTyCon {algTcRhs = rhs})
= case rhs of
+ OpenDataTyCon -> True
DataTyCon {} -> True
+ OpenNewTyCon -> False
NewTyCon {} -> False
AbstractTyCon -> pprPanic "isDataTyCon" (ppr tc)
isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res
isEnumerationTyCon other = False
+isOpenTyCon :: TyCon -> Bool
+isOpenTyCon (SynTyCon {synTcRhs = OpenSynTyCon _}) = True
+isOpenTyCon (AlgTyCon {algTcRhs = OpenDataTyCon }) = True
+isOpenTyCon (AlgTyCon {algTcRhs = OpenNewTyCon }) = True
+isOpenTyCon _ = False
+
isTupleTyCon :: TyCon -> Bool
-- The unit tycon didn't used to be classed as a tuple tycon
-- but I thought that was silly so I've undone it
[Type]) -- Leftover args
-- For the *typechecker* view, we expand synonyms only
-tcExpandTyCon_maybe (SynTyCon {tyConTyVars = tvs, synTcRhs = rhs }) tys
+tcExpandTyCon_maybe (SynTyCon {tyConTyVars = tvs,
+ synTcRhs = SynonymTyCon rhs }) tys
= expand tvs rhs tys
tcExpandTyCon_maybe other_tycon tys = Nothing
\begin{code}
synTyConDefn :: TyCon -> ([TyVar], Type)
-synTyConDefn (SynTyCon {tyConTyVars = tyvars, synTcRhs = ty}) = (tyvars,ty)
+synTyConDefn (SynTyCon {tyConTyVars = tyvars, synTcRhs = SynonymTyCon ty})
+ = (tyvars, ty)
synTyConDefn tycon = pprPanic "getSynTyConDefn" (ppr tycon)
-synTyConRhs :: TyCon -> Type
-synTyConRhs tc = synTcRhs tc
+synTyConRhs :: TyCon -> SynTyConRhs
+synTyConRhs (SynTyCon {synTcRhs = rhs}) = rhs
+synTyConRhs tc = pprPanic "synTyConRhs" (ppr tc)
+
+synTyConType :: TyCon -> Type
+synTyConType tc = case synTcRhs tc of
+ SynonymTyCon t -> t
+ _ -> pprPanic "synTyConType" (ppr tc)
+
+synTyConResKind :: TyCon -> Kind
+synTyConResKind (SynTyCon {synTcRhs = OpenSynTyCon kind}) = kind
+synTyConResKind tycon = pprPanic "synTyConResKind" (ppr tycon)
\end{code}
\begin{code}