import TcEnv ( TyThing(..),
tcLookupLocated, tcLookupLocatedGlobal,
tcExtendGlobalEnv, tcExtendKindEnv, tcExtendKindEnvTvs,
- tcExtendRecEnv, tcLookupTyVar )
-import TcTyDecls ( calcTyConArgVrcs, calcRecFlags, calcClassCycles, calcSynCycles )
+ tcExtendRecEnv, tcLookupTyVar, InstInfo )
+import TcTyDecls ( calcRecFlags, calcClassCycles, calcSynCycles )
import TcClassDcl ( tcClassSigs, tcAddDeclCtxt )
import TcHsType ( kcHsTyVars, kcHsLiftedSigType, kcHsType,
kcHsContext, tcTyVarBndrs, tcHsKindedType, tcHsKindedContext,
import TcMType ( newKindVar, checkValidTheta, checkValidType,
-- checkFreeness,
UserTypeCtxt(..), SourceTyCtxt(..) )
-import TcType ( TcKind, TcType, tyVarsOfType, mkPhiTy,
+import TcType ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
mkArrowKind, liftedTypeKind, mkTyVarTys,
tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
-import Type ( splitTyConApp_maybe,
+import Type ( PredType(..), splitTyConApp_maybe, mkTyVarTy,
+ newTyConInstRhs
-- pprParendType, pprThetaArrow
)
-import Kind ( mkArrowKinds, splitKindFunTys )
import Generics ( validGenericMethodType, canDoGenerics )
import Class ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
-import TyCon ( TyCon, ArgVrcs, AlgTyConRhs( AbstractTyCon ),
+import TyCon ( TyCon, AlgTyConRhs( AbstractTyCon ),
tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
- tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName )
-import DataCon ( DataCon, dataConWrapId, dataConName,
- dataConFieldLabels, dataConTyCon,
- dataConTyVars, dataConFieldType, dataConResTys )
+ tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName,
+ isNewTyCon )
+import DataCon ( DataCon, dataConUserType, dataConName,
+ dataConFieldLabels, dataConTyCon, dataConAllTyVars,
+ dataConFieldType, dataConResTys )
import Var ( TyVar, idType, idName )
import VarSet ( elemVarSet, mkVarSet )
import Name ( Name, getSrcLoc )
import Util ( zipLazy, isSingleton, notNull, sortLe )
import List ( partition )
import SrcLoc ( Located(..), unLoc, getLoc, srcLocSpan )
-import ListSetOps ( equivClasses )
+import ListSetOps ( equivClasses, minusList )
import List ( delete )
import Digraph ( SCC(..) )
import DynFlags ( DynFlag( Opt_GlasgowExts, Opt_Generics,
to check all the side conditions on validity. We could not
do this before because we were in a mutually recursive knot.
-
+Identification of recursive TyCons
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
-@TyThing@s. @rec_vrcs@ is a finite map from @Name@s to @ArgVrcs@s.
+@TyThing@s.
+
+Identifying a TyCon as recursive serves two purposes
+
+1. Avoid infinite types. Non-recursive newtypes are treated as
+"transparent", like type synonyms, after the type checker. If we did
+this for all newtypes, we'd get infinite types. So we figure out for
+each newtype whether it is "recursive", and add a coercion if so. In
+effect, we are trying to "cut the loops" by identifying a loop-breaker.
+
+2. Avoid infinite unboxing. This is nothing to do with newtypes.
+Suppose we have
+ data T = MkT Int T
+ f (MkT x t) = f t
+Well, this function diverges, but we don't want the strictness analyser
+to diverge. But the strictness analyser will diverge because it looks
+deeper and deeper into the structure of T. (I believe there are
+examples where the function does something sane, and the strictness
+analyser still diverges, but I can't see one now.)
+
+Now, concerning (1), the FC2 branch currently adds a coercion for ALL
+newtypes. I did this as an experiment, to try to expose cases in which
+the coercions got in the way of optimisations. If it turns out that we
+can indeed always use a coercion, then we don't risk recursive types,
+and don't need to figure out what the loop breakers are.
+
+For newtype *families* though, we will always have a coercion, so they
+are always loop breakers! So you can easily adjust the current
+algorithm by simply treating all newtype families as loop breakers (and
+indeed type families). I think.
\begin{code}
tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
; traceTc (text "tcTyAndCl" <+> ppr mod)
; (syn_tycons, alg_tyclss) <- fixM (\ ~(rec_syn_tycons, rec_alg_tyclss) ->
do { let { -- Calculate variances and rec-flag
- ; (syn_decls, alg_decls_pre) = partition (isSynDecl . unLoc) decls
- ; alg_decls = alg_decls_pre ++
- concat [tcdATs decl -- add AT decls
- | declLoc <- alg_decls_pre
- , let decl = unLoc declLoc
- , isClassDecl decl] }
-
+ ; (syn_decls, alg_decls) = partition (isSynDecl . unLoc)
+ decls }
-- Extend the global env with the knot-tied results
-- for data types and classes
--
-- Kind-check the declarations
{ (kc_syn_decls, kc_alg_decls) <- kcTyClDecls syn_decls alg_decls
- ; let { calc_vrcs = calcTyConArgVrcs (rec_syn_tycons ++ rec_alg_tyclss)
- ; calc_rec = calcRecFlags boot_details rec_alg_tyclss
- ; tc_decl = addLocM (tcTyClDecl calc_vrcs calc_rec) }
+ ; let { calc_rec = calcRecFlags boot_details rec_alg_tyclss
+ ; tc_decl = addLocM (tcTyClDecl calc_rec) }
-- Type-check the type synonyms, and extend the envt
- ; syn_tycons <- tcSynDecls calc_vrcs kc_syn_decls
+ ; syn_tycons <- tcSynDecls kc_syn_decls
; tcExtendGlobalEnv syn_tycons $ do
-- Type-check the data types and classes
%************************************************************************
\begin{code}
-tcSynDecls :: (Name -> ArgVrcs) -> [LTyClDecl Name] -> TcM [TyThing]
-tcSynDecls calc_vrcs [] = return []
-tcSynDecls calc_vrcs (decl : decls)
- = do { syn_tc <- addLocM (tcSynDecl calc_vrcs) decl
- ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls calc_vrcs decls)
+tcSynDecls :: [LTyClDecl Name] -> TcM [TyThing]
+tcSynDecls [] = return []
+tcSynDecls (decl : decls)
+ = do { syn_tc <- addLocM tcSynDecl decl
+ ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls decls)
; return (syn_tc : syn_tcs) }
-tcSynDecl calc_vrcs
+tcSynDecl
(TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
= tcTyVarBndrs tvs $ \ tvs' -> do
{ traceTc (text "tcd1" <+> ppr tc_name)
; rhs_ty' <- tcHsKindedType rhs_ty
- ; return (ATyCon (buildSynTyCon tc_name tvs' rhs_ty' (calc_vrcs tc_name))) }
+ ; return (ATyCon (buildSynTyCon tc_name tvs' rhs_ty')) }
--------------------
-tcTyClDecl :: (Name -> ArgVrcs) -> (Name -> RecFlag)
- -> TyClDecl Name -> TcM TyThing
+tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM TyThing
-tcTyClDecl calc_vrcs calc_isrec decl
- = tcAddDeclCtxt decl (tcTyClDecl1 calc_vrcs calc_isrec decl)
+tcTyClDecl calc_isrec decl
+ = tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
-tcTyClDecl1 calc_vrcs calc_isrec
+tcTyClDecl1 calc_isrec
(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
= tcTyVarBndrs tvs $ \ tvs' -> do
-- Check that we don't use GADT syntax in H98 world
; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
+ -- Check that the stupid theta is empty for a GADT-style declaration
+ ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
+
-- Check that there's at least one condecl,
- -- or else we're reading an interface file, or -fglasgow-exts
+ -- or else we're reading an hs-boot file, or -fglasgow-exts
; checkTc (not (null cons) || gla_exts || is_boot)
(emptyConDeclsErr tc_name)
{ data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data
tycon final_tvs))
cons
- ; let tc_rhs
- | null cons && is_boot -- In a hs-boot file, empty cons means
- = AbstractTyCon -- "don't know"; hence Abstract
- | otherwise
- = case new_or_data of
- DataType -> mkDataTyConRhs data_cons
- NewType -> ASSERT( isSingleton data_cons )
- mkNewTyConRhs tycon (head data_cons)
- ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs arg_vrcs is_rec
- (want_generic && canDoGenerics data_cons)
+ ; tc_rhs <-
+ if null cons && is_boot -- In a hs-boot file, empty cons means
+ then return AbstractTyCon -- "don't know"; hence Abstract
+ else case new_or_data of
+ DataType -> return (mkDataTyConRhs data_cons)
+ NewType ->
+ ASSERT( isSingleton data_cons )
+ mkNewTyConRhs tc_name tycon (head data_cons)
+ ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
+ (want_generic && canDoGenerics data_cons) h98_syntax
})
; return (ATyCon tycon)
}
where
- arg_vrcs = calc_vrcs tc_name
is_rec = calc_isrec tc_name
h98_syntax = case cons of -- All constructors have same shape
L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
other -> True
-tcTyClDecl1 calc_vrcs calc_isrec
+tcTyClDecl1 calc_isrec
(ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs,
tcdCtxt = ctxt, tcdMeths = meths,
tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
-- need to look up its recursiveness and variance
tycon_name = tyConName (classTyCon clas)
tc_isrec = calc_isrec tycon_name
- tc_vrcs = calc_vrcs tycon_name
in
buildClass class_name tvs' ctxt' fds'
- sig_stuff tc_isrec tc_vrcs)
+ sig_stuff tc_isrec)
; return (AClass clas) }
where
tc_fundep (tvs1, tvs2) = do { tvs1' <- mappM tcLookupTyVar tvs1 ;
; return (tvs1', tvs2') }
-tcTyClDecl1 calc_vrcs calc_isrec
+tcTyClDecl1 calc_isrec
(ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
- = returnM (ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0 []))
+ = returnM (ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0))
-----------------------------------
tcConDecl :: Bool -- True <=> -funbox-strict_fields
= do { let tc_datacon field_lbls arg_ty
= do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
; buildDataCon (unLoc name) False {- Prefix -}
- True {- Vanilla -} [NotMarkedStrict]
+ [NotMarkedStrict]
(map unLoc field_lbls)
- tc_tvs [] [arg_ty']
- tycon (mkTyVarTys tc_tvs) }
+ tc_tvs [] -- No existentials
+ [] [] -- No equalities, predicates
+ [arg_ty']
+ tycon }
-- Check that a newtype has no existential stuff
; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
(ConDecl name _ tvs ctxt details res_ty)
= tcTyVarBndrs tvs $ \ tvs' -> do
{ ctxt' <- tcHsKindedContext ctxt
- ; (data_tc, res_ty_args) <- tcResultType tycon tc_tvs res_ty
+ ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
; let
- con_tvs = case res_ty of
- ResTyH98 -> tc_tvs ++ tvs'
- ResTyGADT _ -> tryVanilla tvs' res_ty_args
-
- -- Vanilla iff result type matches the quantified vars exactly,
- -- and there is no existential context
- -- Must check the context too because of implicit params; e.g.
- -- data T = (?x::Int) => MkT Int
- is_vanilla = res_ty_args `tcEqTypes` mkTyVarTys con_tvs
- && null (unLoc ctxt)
-
tc_datacon is_infix field_lbls btys
= do { let bangs = map getBangStrictness btys
; arg_tys <- mappM tcHsBangType btys
- ; buildDataCon (unLoc name) is_infix is_vanilla
+ ; buildDataCon (unLoc name) is_infix
(argStrictness unbox_strict tycon bangs arg_tys)
(map unLoc field_lbls)
- con_tvs ctxt' arg_tys
- data_tc res_ty_args }
+ univ_tvs ex_tvs eq_preds ctxt' arg_tys
+ data_tc }
-- NB: we put data_tc, the type constructor gotten from the constructor
-- type signature into the data constructor; that way
-- checkValidDataCon can complain if it's wrong.
}
-tcResultType :: TyCon -> [TyVar] -> ResType Name -> TcM (TyCon, [TcType])
-tcResultType tycon tvs ResTyH98 = return (tycon, mkTyVarTys tvs)
-tcResultType _ _ (ResTyGADT res_ty) = tcLHsConResTy res_ty
-
-tryVanilla :: [TyVar] -> [TcType] -> [TyVar]
--- (tryVanilla tvs tys) returns a permutation of tvs.
--- It tries to re-order the tvs so that it exactly
--- matches the [Type], if that is possible
-tryVanilla tvs (ty:tys) | Just tv <- tcGetTyVar_maybe ty -- The type is a tyvar
- , tv `elem` tvs -- That tyvar is in the list
- = tv : tryVanilla (delete tv tvs) tys
-tryVanilla tvs tys = tvs -- Fall through case
-
+tcResultType :: TyCon
+ -> [TyVar] -- data T a b c = ...
+ -> [TyVar] -- where MkT :: forall a b c. ...
+ -> ResType Name
+ -> TcM ([TyVar], -- Universal
+ [TyVar], -- Existential
+ [(TyVar,Type)], -- Equality predicates
+ TyCon) -- TyCon given in the ResTy
+ -- We don't check that the TyCon given in the ResTy is
+ -- the same as the parent tycon, becuase we are in the middle
+ -- of a recursive knot; so it's postponed until checkValidDataCon
+
+tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
+ = return (tc_tvs, dc_tvs, [], decl_tycon)
+ -- In H98 syntax the dc_tvs are the existential ones
+ -- data T a b c = forall d e. MkT ...
+ -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
+
+tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
+ -- E.g. data T a b c where
+ -- MkT :: forall x y z. T (x,y) z z
+ -- Then we generate
+ -- ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
+
+ = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
+ -- NB: tc_tvs and dc_tvs are distinct
+ ; let univ_tvs = choose_univs [] tc_tvs res_tys
+ -- Each univ_tv is either a dc_tv or a tc_tv
+ ex_tvs = dc_tvs `minusList` univ_tvs
+ eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys,
+ tv `elem` tc_tvs]
+ ; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
+ where
+ -- choose_univs uses the res_ty itself if it's a type variable
+ -- and hasn't already been used; otherwise it uses one of the tc_tvs
+ choose_univs used tc_tvs []
+ = ASSERT( null tc_tvs ) []
+ choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys)
+ | Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
+ = tv : choose_univs (tv:used) tc_tvs res_tys
+ | otherwise
+ = tc_tv : choose_univs used tc_tvs res_tys
-------------------
argStrictness :: Bool -- True <=> -funbox-strict_fields
-- We attempt to unbox/unpack a strict field when either:
-- (i) The field is marked '!!', or
-- (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
-
+--
+-- We have turned off unboxing of newtypes because coercions make unboxing
+-- and reboxing more complicated
chooseBoxingStrategy :: Bool -> TyCon -> TcType -> HsBang -> StrictnessMark
chooseBoxingStrategy unbox_strict_fields tycon arg_ty bang
= case bang of
HsNoBang -> NotMarkedStrict
- HsStrict | unbox_strict_fields && can_unbox -> MarkedUnboxed
- HsUnbox | can_unbox -> MarkedUnboxed
+ HsStrict | unbox_strict_fields
+ && can_unbox arg_ty -> MarkedUnboxed
+ HsUnbox | can_unbox arg_ty -> MarkedUnboxed
other -> MarkedStrict
where
- can_unbox = case splitTyConApp_maybe arg_ty of
- Nothing -> False
- Just (arg_tycon, _) -> not (isRecursiveTyCon tycon) &&
- isProductTyCon arg_tycon
+ -- we can unbox if the type is a chain of newtypes with a product tycon
+ -- at the end
+ can_unbox arg_ty = case splitTyConApp_maybe arg_ty of
+ Nothing -> False
+ Just (arg_tycon, tycon_args) ->
+ not (isRecursiveTyCon tycon) &&
+ isProductTyCon arg_tycon &&
+ (if isNewTyCon arg_tycon then
+ can_unbox (newTyConInstRhs arg_tycon tycon_args)
+ else True)
\end{code}
%************************************************************************
-- of the constructor.
checkValidTyCon :: TyCon -> TcM ()
-checkValidTyCon tc
+checkValidTyCon tc
| isSynTyCon tc
= checkValidType syn_ctxt syn_rhs
| otherwise
get_fields con = dataConFieldLabels con `zip` repeat con
-- dataConFieldLabels may return the empty list, which is fine
- -- Note: The complicated checkOne logic below is there to accomodate
- -- for different return types. Add res_ty to the mix,
- -- comparing them in two steps, all for good error messages.
- -- Plan: Use Unify.tcMatchTys to compare the first candidate's
- -- result type against other candidates' types (check bothways).
- -- If they magically agrees, take the substitution and
- -- apply them to the latter ones, and see if they match perfectly.
- -- check_fields fields@((first_field_label, field_ty) : other_fields)
+ -- See Note [GADT record selectors] in MkId.lhs
+ -- We must check (a) that the named field has the same
+ -- type in each constructor
+ -- (b) that those constructors have the same result type
+ --
+ -- However, the constructors may have differently named type variable
+ -- and (worse) we don't know how the correspond to each other. E.g.
+ -- C1 :: forall a b. { f :: a, g :: b } -> T a b
+ -- C2 :: forall d c. { f :: c, g :: c } -> T c d
+ --
+ -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
+ -- result type against other candidates' types BOTH WAYS ROUND.
+ -- If they magically agrees, take the substitution and
+ -- apply them to the latter ones, and see if they match perfectly.
check_fields fields@((label, con1) : other_fields)
-- These fields all have the same name, but are from
-- different constructors in the data type
-- NB: this check assumes that all the constructors of a given
-- data type use the same type variables
where
- tvs1 = mkVarSet (dataConTyVars con1)
+ tvs1 = mkVarSet (dataConAllTyVars con1)
res1 = dataConResTys con1
fty1 = dataConFieldType con1 label
= do { checkFieldCompat label con1 con2 tvs1 res1 res2 fty1 fty2
; checkFieldCompat label con2 con1 tvs2 res2 res1 fty2 fty1 }
where
- tvs2 = mkVarSet (dataConTyVars con2)
+ tvs2 = mkVarSet (dataConAllTyVars con2)
res2 = dataConResTys con2
fty2 = dataConFieldType con2 label
= setSrcSpan (srcLocSpan (getSrcLoc con)) $
addErrCtxt (dataConCtxt con) $
do { checkTc (dataConTyCon con == tc) (badDataConTyCon con)
- ; checkValidType ctxt (idType (dataConWrapId con)) }
-
- -- This checks the argument types and
- -- ambiguity of the existential context (if any)
- --
- -- Note [Sept 04] Now that tvs is all the tvs, this
- -- test doesn't actually check anything
--- ; checkFreeness tvs ex_theta }
+ ; checkValidType ctxt (dataConUserType con) }
where
ctxt = ConArgCtxt (dataConName con)
--- (tvs, ex_theta, _, _, _) = dataConSig con
-
-------------------------------
checkValidClass :: Class -> TcM ()
= vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
, nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow GADTs")) ]
+badStupidTheta tc_name
+ = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
+
newtypeConError tycon n
= sep [ptext SLIT("A newtype must have exactly one constructor,"),
nest 2 $ ptext SLIT("but") <+> quotes (ppr tycon) <+> ptext SLIT("has") <+> speakN n ]