Commit 58470fb7 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Make a start towards eta-rules and injective families

* Make Any into a type family (which it should always have been)
  This is to support the future introduction of eta rules for
  product types (see email on ghc-users title "PolyKind issue"
  early Sept 2012)

* Add the *internal* data type support for
    (a) closed type families [so that you can't give
        type instance for 'Any']
    (b) injective type families [because Any is really
        injective]
  This amounts to two boolean flags on the SynFamilyTyCon
  constructor of TyCon.SynTyConRhs.

There is some knock-on effect, but all of a routine nature.

It remains to offer source syntax for either closed or
injective families.
parent af7cc995
......@@ -1404,6 +1404,18 @@ instance Binary IfaceDecl where
occ <- return $! mkOccNameFS tcName a1
return (IfaceAxiom occ a2 a3 a4)
instance Binary ty => Binary (SynTyConRhs ty) where
put_ bh (SynFamilyTyCon a b) = putByte bh 0 >> put_ bh a >> put_ bh b
put_ bh (SynonymTyCon ty) = putByte bh 1 >> put_ bh ty
get bh = do { h <- getByte bh
; case h of
0 -> do { a <- get bh
; b <- get bh
; return (SynFamilyTyCon a b) }
_ -> do { ty <- get bh
; return (SynonymTyCon ty) } }
instance Binary IfaceClsInst where
put_ bh (IfaceClsInst cls tys dfun flag orph) = do
put_ bh cls
......
......@@ -46,7 +46,7 @@ import Outputable
\begin{code}
------------------------------------------------------
buildSynTyCon :: Name -> [TyVar]
-> SynTyConRhs
-> SynTyConRhs Type
-> Kind -- ^ Kind of the RHS
-> TyConParent
-> TcRnIf m n TyCon
......
......@@ -35,6 +35,7 @@ module IfaceSyn (
#include "HsVersions.h"
import TyCon( SynTyConRhs(..) )
import IfaceType
import CoreSyn( DFunArg, dfunArgExprs )
import PprCore() -- Printing DFunArgs
......@@ -89,9 +90,7 @@ data IfaceDecl
| IfaceSyn { ifName :: OccName, -- Type constructor
ifTyVars :: [IfaceTvBndr], -- Type variables
ifSynKind :: IfaceKind, -- Kind of the *rhs* (not of the tycon)
ifSynRhs :: Maybe IfaceType -- Just rhs for an ordinary synonyn
-- Nothing for an type family declaration
}
ifSynRhs :: SynTyConRhs IfaceType }
| IfaceClass { ifCtxt :: IfaceContext, -- Context...
ifName :: OccName, -- Name of the class TyCon
......@@ -487,12 +486,12 @@ pprIfaceDecl (IfaceForeign {ifName = tycon})
pprIfaceDecl (IfaceSyn {ifName = tycon,
ifTyVars = tyvars,
ifSynRhs = Just mono_ty})
ifSynRhs = SynonymTyCon mono_ty})
= hang (ptext (sLit "type") <+> pprIfaceDeclHead [] tycon tyvars)
4 (vcat [equals <+> ppr mono_ty])
pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars,
ifSynRhs = Nothing, ifSynKind = kind })
ifSynRhs = SynFamilyTyCon {}, ifSynKind = kind })
= hang (ptext (sLit "type family") <+> pprIfaceDeclHead [] tycon tyvars)
4 (dcolon <+> ppr kind)
......@@ -797,9 +796,9 @@ freeNamesIfIdDetails (IfRecSelId tc _) = freeNamesIfTc tc
freeNamesIfIdDetails _ = emptyNameSet
-- All other changes are handled via the version info on the tycon
freeNamesIfSynRhs :: Maybe IfaceType -> NameSet
freeNamesIfSynRhs (Just ty) = freeNamesIfType ty
freeNamesIfSynRhs Nothing = emptyNameSet
freeNamesIfSynRhs :: SynTyConRhs IfaceType -> NameSet
freeNamesIfSynRhs (SynonymTyCon ty) = freeNamesIfType ty
freeNamesIfSynRhs _ = emptyNameSet
freeNamesIfContext :: IfaceContext -> NameSet
freeNamesIfContext = fnList freeNamesIfType
......
......@@ -1459,11 +1459,11 @@ tyConToIfaceDecl env tycon
| Just clas <- tyConClass_maybe tycon
= classToIfaceDecl env clas
| isSynTyCon tycon
| Just syn_rhs <- synTyConRhs_maybe tycon
= IfaceSyn { ifName = getOccName tycon,
ifTyVars = toIfaceTvBndrs tyvars,
ifSynRhs = syn_rhs,
ifSynKind = syn_ki }
ifSynRhs = to_ifsyn_rhs syn_rhs,
ifSynKind = tidyToIfaceType env1 (synTyConResKind tycon) }
| isAlgTyCon tycon
= IfaceData { ifName = getOccName tycon,
......@@ -1483,18 +1483,12 @@ tyConToIfaceDecl env tycon
where
(env1, tyvars) = tidyTyVarBndrs env (tyConTyVars tycon)
(syn_rhs, syn_ki)
= case synTyConRhs tycon of
SynFamilyTyCon ->
( Nothing
, tidyToIfaceType env1 (synTyConResKind tycon) )
SynonymTyCon ty ->
( Just (tidyToIfaceType env1 ty)
, tidyToIfaceType env1 (typeKind ty) )
to_ifsyn_rhs (SynFamilyTyCon a b) = SynFamilyTyCon a b
to_ifsyn_rhs (SynonymTyCon ty) = SynonymTyCon (tidyToIfaceType env1 ty)
ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con)
ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
ifaceConDecls DataFamilyTyCon {} = IfDataFamTyCon
ifaceConDecls (DataFamilyTyCon {}) = IfDataFamTyCon
ifaceConDecls (AbstractTyCon distinct) = IfAbstractTyCon distinct
-- The last case happens when a TyCon has been trimmed during tidying
-- Furthermore, tyThingToIfaceDecl is also used
......
......@@ -474,9 +474,9 @@ tc_iface_decl parent _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs,
; return (ATyCon tycon) }
where
mk_doc n = ptext (sLit "Type syonym") <+> ppr n
tc_syn_rhs Nothing = return SynFamilyTyCon
tc_syn_rhs (Just ty) = do { rhs_ty <- tcIfaceType ty
; return (SynonymTyCon rhs_ty) }
tc_syn_rhs (SynFamilyTyCon a b) = return (SynFamilyTyCon a b)
tc_syn_rhs (SynonymTyCon ty) = do { rhs_ty <- tcIfaceType ty
; return (SynonymTyCon rhs_ty) }
tc_iface_decl _parent ignore_prags
(IfaceClass {ifCtxt = rdr_ctxt, ifName = tc_occ,
......
......@@ -159,7 +159,7 @@ module GHC (
tyConTyVars, tyConDataCons, tyConArity,
isClassTyCon, isSynTyCon, isNewTyCon, isPrimTyCon, isFunTyCon,
isFamilyTyCon, tyConClass_maybe,
synTyConDefn, synTyConType, synTyConResKind,
synTyConRhs_maybe, synTyConDefn_maybe, synTyConResKind,
-- ** Type variables
TyVar,
......
......@@ -165,13 +165,13 @@ pprTypeForUser print_foralls ty
pprTyCon :: PrintExplicitForalls -> ShowSub -> TyCon -> SDoc
pprTyCon pefas ss tyCon
| GHC.isSynTyCon tyCon
= if GHC.isFamilyTyCon tyCon
then pprTyConHdr pefas tyCon <+> dcolon <+>
pprTypeForUser pefas (GHC.synTyConResKind tyCon)
else
let rhs_type = GHC.synTyConType tyCon
in hang (pprTyConHdr pefas tyCon <+> equals) 2 (pprTypeForUser pefas rhs_type)
| Just syn_rhs <- GHC.synTyConRhs_maybe tyCon
= case syn_rhs of
SynFamilyTyCon {} -> pprTyConHdr pefas tyCon <+> dcolon <+>
pprTypeForUser pefas (GHC.synTyConResKind tyCon)
SynonymTyCon rhs_ty -> hang (pprTyConHdr pefas tyCon <+> equals)
2 (pprTypeForUser pefas rhs_ty)
| Just cls <- GHC.tyConClass_maybe tyCon
= pprClass pefas ss cls
| otherwise
......
......@@ -654,7 +654,13 @@ The type constructor Any of kind forall k. k -> k has these properties:
primitive type:
- has a fixed unique, anyTyConKey,
- lives in the global name cache
- built with TyCon.PrimTyCon
* It is a *closed* type family, with no instances. This means that
if ty :: '(k1, k2) we add a given coercion
g :: ty ~ (Fst ty, Snd ty)
If Any was a *data* type, then we'd get inconsistency becuase 'ty'
could be (Any '(k1,k2)) and then we'd have an equality with Any on
one side and '(,) on the other
* It is lifted, and hence represented by a pointer
......@@ -711,8 +717,13 @@ anyTy :: Type
anyTy = mkTyConTy anyTyCon
anyTyCon :: TyCon
anyTyCon = mkLiftedPrimTyCon anyTyConName kind 1 PtrRep
where kind = ForAllTy kKiVar (mkTyVarTy kKiVar)
anyTyCon = mkSynTyCon anyTyConName kind [kKiVar]
syn_rhs
NoParentTyCon
where
kind = ForAllTy kKiVar (mkTyVarTy kKiVar)
syn_rhs = SynFamilyTyCon { synf_open = False, synf_injective = True }
-- NB Closed, injective
anyTypeOfKind :: Kind -> Type
anyTypeOfKind kind = mkNakedTyConApp anyTyCon [kind]
......
......@@ -476,8 +476,7 @@ mkStgAltType bndr alts = case repType (idType bndr) of
where
_is_poly_alt_tycon tc
= isFunTyCon tc
|| isPrimTyCon tc -- "Any" is lifted but primitive
|| isFamilyTyCon tc -- Type family; e.g. arising from strict
|| isFamilyTyCon tc -- Type family; e.g. Any, or arising from strict
-- function application where argument has a
-- type-family type
......
......@@ -560,7 +560,6 @@ tcFamInstDecl top_lvl decl
-- Look up the family TyCon and check for validity including
-- check that toplevel type instances are not for associated types.
; fam_tc <- tcLookupLocatedTyCon fam_tc_lname
; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
; when (isTopLevel top_lvl && isTyConAssoc fam_tc)
(addErr $ assocInClassErr fam_tc_lname)
......@@ -573,7 +572,11 @@ tcFamInstDecl1 :: TyCon -> FamInstDecl Name -> TcM FamInst
-- "type instance"
tcFamInstDecl1 fam_tc decl@(FamInstDecl { fid_tycon = fam_tc_name
, fid_defn = TySynonym {} })
= do { -- (1) do the work of verifying the synonym
= do { -- (0) Check it's an open type family
checkTc (isOpenSynFamilyTyCon fam_tc)
(notOpenFamily fam_tc)
-- (1) do the work of verifying the synonym
; (t_tvs, t_typats, t_rhs) <- tcSynFamInstDecl fam_tc decl
-- (2) check the well-formedness of the instance
......@@ -1445,4 +1448,8 @@ badFamInstDecl tc_name
= vcat [ ptext (sLit "Illegal family instance for") <+>
quotes (ppr tc_name)
, nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ]
notOpenFamily :: TyCon -> SDoc
notOpenFamily tc
= ptext (sLit "Illegal instance for closed family") <+> quotes (ppr tc)
\end{code}
......@@ -771,19 +771,20 @@ checkBootTyCon tc1 tc2
eqListBy eqSig op_stuff1 op_stuff2 &&
eqListBy eqAT ats1 ats2)
| isSynTyCon tc1 && isSynTyCon tc2
| Just syn_rhs1 <- synTyConRhs_maybe tc1
, Just syn_rhs2 <- synTyConRhs_maybe tc2
= ASSERT(tc1 == tc2)
let tvs1 = tyConTyVars tc1; tvs2 = tyConTyVars tc2
env = rnBndrs2 env0 tvs1 tvs2
eqSynRhs SynFamilyTyCon SynFamilyTyCon
= True
eqSynRhs (SynFamilyTyCon a1 b1) (SynFamilyTyCon a2 b2)
= a1 == a2 && b1 == b2
eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
= eqTypeX env t1 t2
eqSynRhs _ _ = False
in
equalLength tvs1 tvs2 &&
eqSynRhs (synTyConRhs tc1) (synTyConRhs tc2)
eqSynRhs syn_rhs1 syn_rhs2
| isAlgTyCon tc1 && isAlgTyCon tc2
= ASSERT(tc1 == tc2)
......
......@@ -1227,9 +1227,8 @@ reifyTyCon tc
(TH.FamilyD flavour (reifyName tc) tvs' kind')
instances) }
| isSynTyCon tc
= do { let (tvs, rhs) = synTyConDefn tc
; rhs' <- reifyType rhs
| Just (tvs, rhs) <- synTyConDefn_maybe tc -- Vanilla type synonym
= do { rhs' <- reifyType rhs
; tvs' <- reifyTyVars tvs
; return (TH.TyConI
(TH.TySynD (reifyName tc) tvs' rhs'))
......
......@@ -533,7 +533,8 @@ tcTyClDecl1 parent _calc_isrec
= tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
{ traceTc "type family:" (ppr tc_name)
; checkFamFlag tc_name
; tycon <- buildSynTyCon tc_name tvs' SynFamilyTyCon kind parent
; let syn_rhs = SynFamilyTyCon { synf_open = True, synf_injective = False }
; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent
; return [ATyCon tycon] }
-- "data family" declaration
......@@ -1306,8 +1307,8 @@ checkValidTyCon tc
| Just cl <- tyConClass_maybe tc
= checkValidClass cl
| isSynTyCon tc
= case synTyConRhs tc of
| Just syn_rhs <- synTyConRhs_maybe tc
= case syn_rhs of
SynFamilyTyCon {} -> return ()
SynonymTyCon ty -> checkValidType syn_ctxt ty
......
......@@ -211,9 +211,8 @@ calcClassCycles cls
-- For synonyms, try to expand them: some arguments might be
-- phantoms, after all. We can expand with impunity because at
-- this point the type synonym cycle check has already happened.
| isSynTyCon tc
, SynonymTyCon rhs <- synTyConRhs tc
, let (env, remainder) = papp (tyConTyVars tc) tys
| Just (tvs, rhs) <- synTyConDefn_maybe tc
, let (env, remainder) = papp tvs tys
rest_tys = either (const []) id remainder
= expandType seen (tc:path) (substTy (mkTopTvSubst env) rhs)
. flip (foldr (expandType seen path)) rest_tys
......
......@@ -916,8 +916,8 @@ isTauTy _ = False
isTauTyCon :: TyCon -> Bool
-- Returns False for type synonyms whose expansion is a polytype
isTauTyCon tc
| isClosedSynTyCon tc = isTauTy (snd (synTyConDefn tc))
| otherwise = True
| Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
| otherwise = True
---------------
getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
......@@ -1375,6 +1375,7 @@ orphNamesOfCo (UnsafeCo ty1 ty2) = orphNamesOfType ty1 `unionNameSets` orphNa
orphNamesOfCo (SymCo co) = orphNamesOfCo co
orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
orphNamesOfCo (NthCo _ co) = orphNamesOfCo co
orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
orphNamesOfCo (InstCo co ty) = orphNamesOfCo co `unionNameSets` orphNamesOfType ty
orphNamesOfCos :: [Coercion] -> NameSet
......
......@@ -12,7 +12,7 @@ module TyCon(
AlgTyConRhs(..), visibleDataCons,
TyConParent(..), isNoParent,
SynTyConRhs(..),
SynTyConRhs(..),
-- ** Coercion axiom constructors
CoAxiom(..),
......@@ -38,7 +38,7 @@ module TyCon(
isFunTyCon,
isPrimTyCon,
isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
isSynTyCon, isClosedSynTyCon,
isSynTyCon, isOpenSynFamilyTyCon,
isDecomposableTyCon,
isForeignTyCon,
isPromotedDataCon, isPromotedTyCon,
......@@ -66,7 +66,7 @@ module TyCon(
tyConParent,
tyConTuple_maybe, tyConClass_maybe,
tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
synTyConDefn, synTyConRhs, synTyConType,
synTyConDefn_maybe, synTyConRhs_maybe,
tyConExtName, -- External name for foreign types
algTyConRhs,
newTyConRhs, newTyConEtadRhs, unwrapNewTyCon_maybe,
......@@ -359,8 +359,8 @@ data TyCon
tyConTyVars :: [TyVar], -- Bound tyvars
synTcRhs :: SynTyConRhs, -- ^ Contains information about the
-- expansion of the synonym
synTcRhs :: SynTyConRhs Type, -- ^ Contains information about the
-- expansion of the synonym
synTcParent :: TyConParent -- ^ Gives the family declaration 'TyCon'
-- of 'TyCon's representing family instances
......@@ -566,17 +566,28 @@ isNoParent _ = False
--------------------
-- | Information pertaining to the expansion of a type synonym (@type@)
data SynTyConRhs
data SynTyConRhs ty
= -- | An ordinary type synonyn.
SynonymTyCon
Type -- This 'Type' is the rhs, and may mention from 'tyConTyVars'.
ty -- This 'Type' is the rhs, and may mention from 'tyConTyVars'.
-- It acts as a template for the expansion when the 'TyCon'
-- is applied to some types.
-- | A type synonym family e.g. @type family F x y :: * -> *@
| SynFamilyTyCon
| SynFamilyTyCon {
synf_open :: Bool, -- See Note [Closed type families]
synf_injective :: Bool
}
\end{code}
Note [Closed type families]
~~~~~~~~~~~~~~~~~~~~~~~~~
* In an open type family you can add new instances later. This is the
usual case.
* In a closed type family you can only put instnaces where the family
is defined. GHC doesn't support syntax for this yet.
Note [Promoted data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A data constructor can be promoted to become a type constructor,
......@@ -918,7 +929,7 @@ mkPrimTyCon' name kind arity rep is_unlifted
}
-- | Create a type synonym 'TyCon'
mkSynTyCon :: Name -> Kind -> [TyVar] -> SynTyConRhs -> TyConParent -> TyCon
mkSynTyCon :: Name -> Kind -> [TyVar] -> SynTyConRhs Type -> TyConParent -> TyCon
mkSynTyCon name kind tyvars rhs parent
= SynTyCon {
tyConName = name,
......@@ -1106,15 +1117,15 @@ isSynFamilyTyCon :: TyCon -> Bool
isSynFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}}) = True
isSynFamilyTyCon _ = False
isOpenSynFamilyTyCon :: TyCon -> Bool
isOpenSynFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon { synf_open = is_open } }) = is_open
isOpenSynFamilyTyCon _ = False
-- | Is this a synonym 'TyCon' that can have may have further instances appear?
isDataFamilyTyCon :: TyCon -> Bool
isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
isDataFamilyTyCon _ = False
-- | Is this a synonym 'TyCon' that can have no further instances appear?
isClosedSynTyCon :: TyCon -> Bool
isClosedSynTyCon tycon = isSynTyCon tycon && not (isFamilyTyCon tycon)
-- | Injective 'TyCon's can be decomposed, so that
-- T ty1 ~ T ty2 => ty1 ~ ty2
isInjectiveTyCon :: TyCon -> Bool
......@@ -1351,26 +1362,17 @@ tyConStupidTheta tycon = pprPanic "tyConStupidTheta" (ppr tycon)
\end{code}
\begin{code}
-- | Extract the 'TyVar's bound by a type synonym and the corresponding (unsubstituted) right hand side.
-- If the given 'TyCon' is not a type synonym, panics
synTyConDefn :: TyCon -> ([TyVar], Type)
synTyConDefn (SynTyCon {tyConTyVars = tyvars, synTcRhs = SynonymTyCon ty})
= (tyvars, ty)
synTyConDefn tycon = pprPanic "getSynTyConDefn" (ppr tycon)
-- | Extract the information pertaining to the right hand side of a type synonym (@type@) declaration. Panics
-- if the given 'TyCon' is not a type synonym
synTyConRhs :: TyCon -> SynTyConRhs
synTyConRhs (SynTyCon {synTcRhs = rhs}) = rhs
synTyConRhs tc = pprPanic "synTyConRhs" (ppr tc)
-- | Find the expansion of the type synonym represented by the given 'TyCon'. The free variables of this
-- type will typically include those 'TyVar's bound by the 'TyCon'. Panics if the 'TyCon' is not that of
-- a type synonym
synTyConType :: TyCon -> Type
synTyConType tc = case synTcRhs tc of
SynonymTyCon t -> t
_ -> pprPanic "synTyConType" (ppr tc)
-- | Extract the 'TyVar's bound by a vanilla type synonym (not familiy)
-- and the corresponding (unsubstituted) right hand side.
synTyConDefn_maybe :: TyCon -> Maybe ([TyVar], Type)
synTyConDefn_maybe (SynTyCon {tyConTyVars = tyvars, synTcRhs = SynonymTyCon ty})
= Just (tyvars, ty)
synTyConDefn_maybe _ = Nothing
-- | Extract the information pertaining to the right hand side of a type synonym (@type@) declaration.
synTyConRhs_maybe :: TyCon -> Maybe (SynTyConRhs Type)
synTyConRhs_maybe (SynTyCon {synTcRhs = rhs}) = Just rhs
synTyConRhs_maybe _ = Nothing
\end{code}
\begin{code}
......
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