Commit 9417e579 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor occurrence-check logic

This patch does two related things

* Combines the occurrence-check logic in the on-the-fly unifier with
  that in the constraint solver.  They are both doing the same job,
  after all.  The resulting code is now in TcUnify:
     metaTyVarUpdateOK
     occCheckExpand
     occCheckForErrors (called in TcErrors)

* In doing this I disovered checking for family-free-ness and foralls
  can be unnecessarily inefficient, because it expands type synonyms.
  It's easy just to cache this info in the type syononym TyCon, which
  I am now doing.
parent 1f09b246
......@@ -24,7 +24,7 @@ module DataCon (
FieldLbl(..), FieldLabel, FieldLabelString,
-- ** Type construction
mkDataCon, buildAlgTyCon, fIRST_TAG,
mkDataCon, buildAlgTyCon, buildSynTyCon, fIRST_TAG,
-- ** Type deconstruction
dataConRepType, dataConSig, dataConInstSig, dataConFullSig,
......@@ -1310,3 +1310,11 @@ buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
rhs parent gadt_syn
where
binders = mkTyConBindersPreferAnon ktvs liftedTypeKind
buildSynTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
-> [Role] -> Type -> TyCon
buildSynTyCon name binders res_kind roles rhs
= mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
where
is_tau = isTauTy rhs
is_fam_free = isFamFreeTy rhs
......@@ -547,7 +547,7 @@ tc_iface_decl _ _ (IfaceSynonym {ifName = tc_name,
{ res_kind' <- tcIfaceType res_kind -- Note [Synonym kind loop]
; rhs <- forkM (mk_doc tc_name) $
tcIfaceType rhs_ty
; let tycon = mkSynonymTyCon tc_name binders' res_kind' roles rhs
; let tycon = buildSynTyCon tc_name binders' res_kind' roles rhs
; return (ATyCon tycon) }
where
mk_doc n = text "Type synonym" <+> ppr n
......
......@@ -454,6 +454,8 @@ tYPETyCon = mkKindTyCon tYPETyConName
unliftedTypeKindTyCon = mkSynonymTyCon unliftedTypeKindTyConName
[] liftedTypeKind []
(tYPE (TyConApp ptrRepUnliftedDataConTyCon []))
True -- no foralls
True -- family free
--------------------------
-- ... and now their names
......
......@@ -1055,15 +1055,15 @@ liftedTypeKindTyCon, starKindTyCon, unicodeStarKindTyCon :: TyCon
-- type * = tYPE 'PtrRepLifted
-- type * = tYPE 'PtrRepLifted -- Unicode variant
liftedTypeKindTyCon = mkSynonymTyCon liftedTypeKindTyConName
liftedTypeKindTyCon = buildSynTyCon liftedTypeKindTyConName
[] liftedTypeKind []
(tYPE ptrRepLiftedTy)
starKindTyCon = mkSynonymTyCon starKindTyConName
starKindTyCon = buildSynTyCon starKindTyConName
[] liftedTypeKind []
(tYPE ptrRepLiftedTy)
unicodeStarKindTyCon = mkSynonymTyCon unicodeStarKindTyConName
unicodeStarKindTyCon = buildSynTyCon unicodeStarKindTyConName
[] liftedTypeKind []
(tYPE ptrRepLiftedTy)
......
......@@ -10,7 +10,7 @@ module TcCanonical(
#include "HsVersions.h"
import TcRnTypes
import TcUnify( swapOverTyVars )
import TcUnify( swapOverTyVars, metaTyVarUpdateOK )
import TcType
import Type
import TcFlatten
......@@ -1374,7 +1374,7 @@ canEqTyVar2 :: DynFlags
-- preserved as much as possible
canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
| OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
| Just xi2' <- metaTyVarUpdateOK dflags tv1 xi2 -- No occurs check
-- Must do the occurs check even on tyvar/tyvar
-- equalities, in case have x ~ (y :: ..x...)
-- Trac #12593
......@@ -1499,12 +1499,6 @@ canEqTyVarTyVar, are these
* If either is a flatten-meta-variables, it goes on the left.
* If one is a strict sub-kind of the other e.g.
(alpha::?) ~ (beta::*)
orient them so RHS is a subkind of LHS. That way we will replace
'a' with 'b', correctly narrowing the kind.
This establishes the subkind invariant of CTyEqCan.
* Put a meta-tyvar on the left if possible
alpha[3] ~ r
......
......@@ -12,6 +12,7 @@ module TcErrors(
import TcRnTypes
import TcRnMonad
import TcMType
import TcUnify( occCheckForErrors, OccCheckResult(..) )
import TcType
import RnEnv( unknownNameSuggestions )
import Type
......@@ -1434,7 +1435,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, extra3, report] }
| OC_Forall <- occ_check_expand
| OC_Bad <- occ_check_expand
= do { let msg = vcat [ text "Cannot instantiate unification variable"
<+> quotes (ppr tv1)
, hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
......@@ -1505,8 +1506,8 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-- Consider an ambiguous top-level constraint (a ~ F a)
-- Not an occurs check, because F is a type function.
where
occ_check_expand = occurCheckExpand dflags tv1 ty2
ty1 = mkTyVarTy tv1
ty1 = mkTyVarTy tv1
occ_check_expand = occCheckForErrors dflags tv1 ty2
what = case ctLocTypeOrKind_maybe (ctLoc ct) of
Just KindLevel -> text "kind"
......
......@@ -12,6 +12,7 @@ module TcFlatten(
import TcRnTypes
import TcType
import Type
import TcUnify( occCheckExpand )
import TcEvidence
import TyCon
import TyCoRep -- performs delicate algorithm on types
......@@ -21,7 +22,6 @@ import VarEnv
import NameEnv
import Outputable
import TcSMonad as TcS
import DynFlags( DynFlags )
import Util
import Bag
......@@ -1448,8 +1448,7 @@ We must solve both!
unflatten :: Cts -> Cts -> TcS Cts
unflatten tv_eqs funeqs
= do { dflags <- getDynFlags
; tclvl <- getTcLevel
= do { tclvl <- getTcLevel
; traceTcS "Unflattening" $ braces $
vcat [ text "Funeqs =" <+> pprCts funeqs
......@@ -1460,11 +1459,11 @@ unflatten tv_eqs funeqs
-- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv]
-- ==> (unify) [W] F [fmv] ~ fmv
-- See Note [Unflatten using funeqs first]
; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs
; funeqs <- foldrBagM unflatten_funeq emptyCts funeqs
; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
-- Step 2: unify the tv_eqs, if possible
; tv_eqs <- foldrBagM (unflatten_eq dflags tclvl) emptyCts tv_eqs
; tv_eqs <- foldrBagM (unflatten_eq tclvl) emptyCts tv_eqs
; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
-- Step 3: fill any remaining fmvs with fresh unification variables
......@@ -1483,25 +1482,25 @@ unflatten tv_eqs funeqs
; zonkSimples all_flat }
where
----------------
unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts
unflatten_funeq dflags ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
unflatten_funeq :: Ct -> Cts -> TcS Cts
unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
, cc_fsk = fmv, cc_ev = ev }) rest
= do { -- fmv should be an un-filled flatten meta-tv;
-- we now fix its final value by filling it, being careful
-- to observe the occurs check. Zonking will eliminate it
-- altogether in due course
rhs' <- zonkTcType (mkTyConApp tc xis)
; case occurCheckExpand dflags fmv rhs' of
OC_OK rhs'' -- Normal case: fill the tyvar
; case occCheckExpand fmv rhs' of
Just rhs'' -- Normal case: fill the tyvar
-> do { setEvBindIfWanted ev
(EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
; unflattenFmv fmv rhs''
; return rest }
_ -> -- Occurs check
return (ct `consCts` rest) }
Nothing -> -- Occurs check
return (ct `consCts` rest) }
unflatten_funeq _ other_ct _
unflatten_funeq other_ct _
= pprPanic "unflatten_funeq" (ppr other_ct)
----------------
......@@ -1512,23 +1511,23 @@ unflatten tv_eqs funeqs
finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
----------------
unflatten_eq :: DynFlags -> TcLevel -> Ct -> Cts -> TcS Cts
unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
| isFmvTyVar tv -- Previously these fmvs were untouchable,
-- but now they are touchable
-- NB: unlike unflattenFmv, filling a fmv here does
-- bump the unification count; it is "improvement"
-- Note [Unflattening can force the solver to iterate]
= do { lhs_elim <- tryFill dflags tv rhs ev
= do { lhs_elim <- tryFill tv rhs ev
; if lhs_elim then return rest else
do { rhs_elim <- try_fill dflags tclvl ev rhs (mkTyVarTy tv)
do { rhs_elim <- try_fill tclvl ev rhs (mkTyVarTy tv)
; if rhs_elim then return rest else
return (ct `consCts` rest) } }
| otherwise
= return (ct `consCts` rest)
unflatten_eq _ _ ct _ = pprPanic "unflatten_irred" (ppr ct)
unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
----------------
finalise_eq :: Ct -> Cts -> TcS Cts
......@@ -1549,33 +1548,33 @@ unflatten tv_eqs funeqs
finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
----------------
try_fill dflags tclvl ev ty1 ty2
try_fill tclvl ev ty1 ty2
| Just tv1 <- tcGetTyVar_maybe ty1
, isTouchableOrFmv tclvl tv1
, typeKind ty1 `eqType` tyVarKind tv1
= tryFill dflags tv1 ty2 ev
= tryFill tv1 ty2 ev
| otherwise
= return False
tryFill :: DynFlags -> TcTyVar -> TcType -> CtEvidence -> TcS Bool
tryFill :: TcTyVar -> TcType -> CtEvidence -> TcS Bool
-- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv
-- If so, and if tv does not appear in 'rhs', set tv := rhs
-- bind the evidence (which should be a CtWanted) to Refl<rhs>
-- and return True. Otherwise return False
tryFill dflags tv rhs ev
tryFill tv rhs ev
= ASSERT2( not (isGiven ev), ppr ev )
do { is_filled <- isFilledMetaTyVar tv
; if is_filled then return False else
do { rhs' <- zonkTcType rhs
; case occurCheckExpand dflags tv rhs' of
OC_OK rhs'' -- Normal case: fill the tyvar
; case occCheckExpand tv rhs' of
Just rhs'' -- Normal case: fill the tyvar
-> do { setEvBindIfWanted ev
(EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
; unifyTyVar tv rhs''
; return True }
_ -> -- Occurs check
return False } }
Nothing -> -- Occurs check
return False } }
{-
Note [Unflatten using funeqs first]
......
......@@ -912,7 +912,7 @@ tcTySynRhs roles_info tc_name binders res_kind hs_ty
; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
; let roles = roles_info tc_name
tycon = mkSynonymTyCon tc_name binders res_kind roles rhs_ty
tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
; return tycon }
tcDataDefn :: RolesInfo -> Name
......
This diff is collapsed.
......@@ -31,7 +31,10 @@ module TcUnify (
matchActualFunTys, matchActualFunTysPart,
matchExpectedFunKind,
wrapFunResCoercion
wrapFunResCoercion,
occCheckExpand, metaTyVarUpdateOK,
occCheckForErrors, OccCheckResult(..)
) where
......@@ -58,6 +61,8 @@ import BasicTypes
import Name ( Name )
import Bag
import Util
import Pair( pFst )
import qualified GHC.LanguageExtensions as LangExt
import Outputable
import FastString
......@@ -1397,76 +1402,6 @@ maybe_sym :: SwapFlag -> Coercion -> Coercion
maybe_sym IsSwapped = mkSymCo
maybe_sym NotSwapped = id
----------------
metaTyVarUpdateOK :: DynFlags
-> TcTyVar -- tv :: k1
-> TcType -- ty :: k2
-> Maybe TcType -- possibly-expanded ty
-- (metaTyFVarUpdateOK tv ty)
-- We are about to update the meta-tyvar tv with ty.
-- Check (a) that tv doesn't occur in ty (occurs check)
-- (b) that ty does not have any foralls
-- (in the impredicative case), or type functions
--
-- We have two possible outcomes:
-- (1) Return the type to update the type variable with,
-- [we know the update is ok]
-- (2) Return Nothing,
-- [the update might be dodgy]
--
-- Note that "Nothing" does not mean "definite error". For example
-- type family F a
-- type instance F Int = Int
-- consider
-- a ~ F a
-- This is perfectly reasonable, if we later get a ~ Int. For now, though,
-- we return Nothing, leaving it to the later constraint simplifier to
-- sort matters out.
metaTyVarUpdateOK dflags tv ty
= case defer_me impredicative ty of
OC_OK _ -> Just ty
OC_Forall -> Nothing -- forall or type function
OC_Occurs -> occCheckExpand tv ty
where
details = tcTyVarDetails tv
impredicative = canUnifyWithPolyType dflags details
defer_me :: Bool -- True <=> foralls are ok
-> TcType
-> OccCheckResult ()
-- Checks for (a) occurrence of tv
-- (b) type family applications
-- (c) foralls if the Bool is false
-- See Note [Prevent unification with type families]
-- See Note [Refactoring hazard: checkTauTvUpdate]
-- See Note [Checking for foralls] in TcType
defer_me _ (TyVarTy tv')
| tv == tv' = OC_Occurs
| otherwise = defer_me True (tyVarKind tv')
defer_me b (TyConApp tc tys)
| isTypeFamilyTyCon tc = OC_Forall -- We use OC_Forall to signal
-- forall /or/ type function
| not (isTauTyCon tc) = OC_Forall
| otherwise = mapM (defer_me b) tys >> OC_OK ()
defer_me b (ForAllTy (TvBndr tv' _) t)
| not b = OC_Forall
| tv == tv' = OC_OK ()
| otherwise = do { defer_me True (tyVarKind tv'); defer_me b t }
defer_me _ (LitTy {}) = OC_OK ()
defer_me b (FunTy fun arg) = defer_me b fun >> defer_me b arg
defer_me b (AppTy fun arg) = defer_me b fun >> defer_me b arg
defer_me b (CastTy ty co) = defer_me b ty >> defer_me_co co
defer_me _ (CoercionTy co) = defer_me_co co
-- We don't really care if there are type families in a coercion,
-- but we still can't have an occurs-check failure
defer_me_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
| otherwise = OC_OK ()
swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
-- See Note [Canonical orientation for tyvar/tyvar equality constraints]
swapOverTyVars tv1 tv2
......@@ -2021,4 +1956,3 @@ canUnifyWithPolyType dflags details
MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags
_other -> True
-- We can have non-meta tyvars in given constraints
......@@ -50,6 +50,7 @@ module TyCon(
mightBeUnsaturatedTyCon,
isPromotedDataCon, isPromotedDataCon_maybe,
isKindTyCon, isLiftedTypeKindTyConName,
isTauTyCon, isFamFreeTyCon,
isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
isDataSumTyCon_maybe,
......@@ -619,8 +620,16 @@ data TyCon
-- This list has length = tyConArity
-- See also Note [TyCon Role signatures]
synTcRhs :: Type -- ^ Contains information about the expansion
synTcRhs :: Type, -- ^ Contains information about the expansion
-- of the synonym
synIsTau :: Bool, -- True <=> the RHS of this synonym does not
-- have any foralls, after expanding any
-- nested synonyms
synIsFamFree :: Bool -- True <=> the RHS of this synonym does mention
-- any type synonym families (data families
-- are fine), again after expanding any
-- nested synonyms
}
-- | Represents families (both type and data)
......@@ -1543,8 +1552,8 @@ mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
-- | Create a type synonym 'TyCon'
mkSynonymTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
-> [Role] -> Type -> TyCon
mkSynonymTyCon name binders res_kind roles rhs
-> [Role] -> Type -> Bool -> Bool -> TyCon
mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
= SynonymTyCon {
tyConName = name,
tyConUnique = nameUnique name,
......@@ -1554,7 +1563,9 @@ mkSynonymTyCon name binders res_kind roles rhs
tyConArity = length binders,
tyConTyVars = binderVars binders,
tcRoles = roles,
synTcRhs = rhs
synTcRhs = rhs,
synIsTau = is_tau,
synIsFamFree = is_fam_free
}
-- | Create a type family 'TyCon'
......@@ -1805,6 +1816,14 @@ isTypeSynonymTyCon :: TyCon -> Bool
isTypeSynonymTyCon (SynonymTyCon {}) = True
isTypeSynonymTyCon _ = False
isTauTyCon :: TyCon -> Bool
isTauTyCon (SynonymTyCon { synIsTau = is_tau }) = is_tau
isTauTyCon _ = True
isFamFreeTyCon :: TyCon -> Bool
isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
isFamFreeTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
isFamFreeTyCon _ = True
-- As for newtypes, it is in some contexts important to distinguish between
-- closed synonyms and synonym families, as synonym families have no unique
......
......@@ -99,7 +99,7 @@ module Type (
-- ** Predicates on types
isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
isCoercionTy_maybe, isCoercionType, isForAllTy,
isPiTy,
isPiTy, isTauTy, isFamFreeTy,
-- (Lifting and boxity)
isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
......@@ -1383,6 +1383,17 @@ partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
-- when printing errors. Assume everything is visible.
-- @isTauTy@ tests if a type has no foralls
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
isTauTy (FunTy a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTy (CastTy ty _) = isTauTy ty
isTauTy (CoercionTy _) = False -- Not sure about this
{-
%************************************************************************
......@@ -1829,6 +1840,18 @@ pprSourceTyCon tycon
| otherwise
= ppr tycon
-- @isTauTy@ tests if a type has no foralls
isFamFreeTy :: Type -> Bool
isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
isFamFreeTy (TyVarTy _) = True
isFamFreeTy (LitTy {}) = True
isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b
isFamFreeTy (FunTy a b) = isFamFreeTy a && isFamFreeTy b
isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty
isFamFreeTy (CastTy ty _) = isFamFreeTy ty
isFamFreeTy (CoercionTy _) = False -- Not sure about this
{-
************************************************************************
* *
......
......@@ -360,7 +360,7 @@ vectTypeEnv tycons vectTypeDecls vectClassDecls
origName = tyConName origTyCon
vectName = tyConName vectTyCon
mkSyn canonName ty = mkSynonymTyCon canonName [] (typeKind ty) [] ty
mkSyn canonName ty = buildSynTyCon canonName [] (typeKind ty) [] ty
defDataCons
| isAbstract = return ()
......
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