Commit 6eabb6dd authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow recursive (undecidable) superclasses

This patch fulfils the request in Trac #11067, #10318, and #10592,
by lifting the conservative restrictions on superclass constraints.

These restrictions are there (and have been since Haskell was born) to
ensure that the transitive superclasses of a class constraint is a finite
set.  However (a) this restriction is conservative, and can be annoying
when there really is no recursion, and (b) sometimes genuinely recursive
superclasses are useful (see the tickets).

Dimitrios and I worked out that there is actually a relatively simple way
to do the job. It’s described in some detail in

   Note [The superclass story] in TcCanonical
   Note [Expanding superclasses] in TcType

In brief, the idea is to expand superclasses only finitely, but to
iterate (using a loop that already existed) if there are more
superclasses to explore.

Other small things

- I improved grouping of error messages a bit in TcErrors

- I re-centred the haddock.compiler test, which was at 9.8%
  above the norm, and which this patch pushed slightly over
parent b8ca6459
......@@ -565,6 +565,7 @@ data ExtensionFlag
| Opt_OverlappingInstances
| Opt_UndecidableInstances
| Opt_IncoherentInstances
| Opt_UndecidableSuperClasses
| Opt_MonomorphismRestriction
| Opt_MonoPatBinds
| Opt_MonoLocalBinds
......@@ -3261,6 +3262,7 @@ xFlags = [
flagSpec "TypeSynonymInstances" Opt_TypeSynonymInstances,
flagSpec "UnboxedTuples" Opt_UnboxedTuples,
flagSpec "UndecidableInstances" Opt_UndecidableInstances,
flagSpec "UndecidableSuperClasses" Opt_UndecidableSuperClasses,
flagSpec "UnicodeSyntax" Opt_UnicodeSyntax,
flagSpec "UnliftedFFITypes" Opt_UnliftedFFITypes,
flagSpec "ViewPatterns" Opt_ViewPatterns
......
This diff is collapsed.
......@@ -345,7 +345,7 @@ warnRedundantConstraints ctxt env info ev_vars
_ -> ev_vars
improving ev_var = any isImprovementPred $
transSuperClassesPred (idType ev_var)
transSuperClasses (idType ev_var)
{- Note [Redundant constraints in instance decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -406,8 +406,9 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
True, mkUserTypeErrorReporter)
, ("insoluble1", is_given_eq, True, mkGroupReporter mkEqErr)
, ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
, ("insoluble3", rigid_nom_tv_eq, True, mkSkolReporter)
, ("insoluble4", rigid_nom_eq, True, mkGroupReporter mkEqErr)
, ("skolem eq1", very_wrong, True, mkSkolReporter)
, ("skolem eq2", skolem_eq, True, mkSkolReporter)
, ("non-tv eq", non_tv_eq, True, mkSkolReporter)
, ("Out of scope", is_out_of_scope, True, mkHoleReporter)
, ("Holes", is_hole, False, mkHoleReporter)
......@@ -420,28 +421,41 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
, ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
, ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ]
rigid_nom_eq, rigid_nom_tv_eq, is_hole, is_dict,
-- rigid_nom_eq, rigid_nom_tv_eq,
is_hole, is_dict,
is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
utterly_wrong _ _ = False
is_out_of_scope ct _ = isOutOfScopeCt ct
is_hole ct _ = isHoleCt ct
is_given_eq ct pred
| EqPred {} <- pred = arisesFromGivens ct
| otherwise = False
-- I think all given residuals are equalities
is_user_type_error ct _ = isUserTypeErrorCt ct
-- Things like (Int ~N Bool)
utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
utterly_wrong _ _ = False
-- Things like (a ~N Int)
very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
very_wrong _ _ = False
-- Things like (a ~N b) or (a ~N F Bool)
skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1
skolem_eq _ _ = False
-- Skolem (i.e. non-meta) type variable on the left
rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
-- Things like (F a ~N Int)
non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
non_tv_eq _ _ = False
rigid_nom_tv_eq _ pred
| EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
| otherwise = False
-- rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
--
-- rigid_nom_tv_eq _ pred
-- | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
-- | otherwise = False
is_out_of_scope ct _ = isOutOfScopeCt ct
is_hole ct _ = isHoleCt ct
is_user_type_error ct _ = isUserTypeErrorCt ct
is_equality _ (EqPred {}) = True
is_equality _ _ = False
......@@ -457,6 +471,15 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
---------------
isSkolemTy :: TcLevel -> Type -> Bool
isSkolemTy tc_lvl ty
= case getTyVar_maybe ty of
Nothing -> False
Just tv -> isSkolemTyVar tv
|| (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
-- The latter case is for touchable SigTvs
-- we postpone untouchables to a latter test (too obscure)
isTyFun_maybe :: Type -> Maybe TyCon
isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
......@@ -476,15 +499,19 @@ type ReporterSpec
, Reporter) -- The reporter itself
mkSkolReporter :: Reporter
-- Suppress duplicates with the same LHS
-- Suppress duplicates with either the same LHS, or same location
mkSkolReporter ctxt cts
= mapM_ (reportGroup mkEqErr ctxt) (equivClasses cmp_lhs_type cts)
= mapM_ (reportGroup mkEqErr ctxt) (group cts)
where
cmp_lhs_type ct1 ct2
= case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
(EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
(eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
_ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
group [] = []
group (ct:cts) = (ct : yeses) : group noes
where
(yeses, noes) = partition (group_with ct) cts
group_with ct1 ct2
| EQ <- cmp_loc ct1 ct2 = True
| EQ <- cmp_lhs_type ct1 ct2 = True
| otherwise = False
mkHoleReporter :: Reporter
-- Reports errors one at a time
......@@ -515,7 +542,16 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
mkGroupReporter mk_err ctxt cts
= mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
where
cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
cmp_lhs_type :: Ct -> Ct -> Ordering
cmp_lhs_type ct1 ct2
= case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
(EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
(eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
_ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
cmp_loc :: Ct -> Ct -> Ordering
cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
-> [Ct] -> TcM ()
......
{-# LANGUAGE CPP #-}
module TcInteract (
solveSimpleGivens, -- Solves [EvVar],GivenLoc
solveSimpleGivens, -- Solves [Ct]
solveSimpleWanteds, -- Solves Cts
solveCallStack, -- for use in TcSimplify
......@@ -132,24 +132,18 @@ that prepareInertsForImplications will discard the insolubles, so we
must keep track of them separately.
-}
solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts
-- Solves the givens, adding them to the inert set
-- Returns any insoluble givens, which represent inaccessible code,
-- taking those ones out of the inert set
solveSimpleGivens loc givens
solveSimpleGivens :: [Ct] -> TcS Cts
solveSimpleGivens givens
| null givens -- Shortcut for common case
= return emptyCts
| otherwise
= do { go (map mk_given_ct givens)
= do { go givens
; takeGivenInsolubles }
where
mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
, ctev_pred = evVarPred ev_id
, ctev_loc = loc })
go givens = do { solveSimples (listToBag givens)
; new_givens <- runTcPluginsGiven
; when (notNull new_givens) (go new_givens)
}
; when (notNull new_givens) $
go new_givens }
solveSimpleWanteds :: Cts -> TcS WantedConstraints
-- NB: 'simples' may contain /derived/ equalities, floated
......
......@@ -81,7 +81,7 @@ module TcRnTypes(
toDerivedWC,
andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
isDroppableDerivedLoc, insolubleImplic, trulyInsoluble,
isDroppableDerivedLoc, insolubleImplic,
arisesFromGivens,
Implication(..), ImplicStatus(..), isInsolubleStatus,
......@@ -1339,7 +1339,13 @@ data Ct
= CDictCan { -- e.g. Num xi
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_class :: Class,
cc_tyargs :: [Xi] -- cc_tyargs are function-free, hence Xi
cc_tyargs :: [Xi], -- cc_tyargs are function-free, hence Xi
cc_pend_sc :: Bool -- True <=> (a) cc_class has superclasses
-- (b) we have not yet added those
-- superclasses as Givens
-- NB: cc_pend_sc is used for G/W/D. For W/D the reason
-- we need superclasses is to expose possible improvement
-- via fundeps
}
| CIrredEvCan { -- These stand for yet-unusable predicates
......@@ -1872,11 +1878,11 @@ trulyInsoluble :: TcLevel -> Ct -> Bool
-- The constraint is in the wc_insol set,
-- but we do not treat as truly isoluble
-- a) type-holes, arising from PartialTypeSignatures,
-- b) an out-of-scope variable
-- (except out-of-scope variables masquerading as type-holes)
-- Yuk!
trulyInsoluble tc_lvl insol
= isOutOfScopeCt insol
|| isRigidEqPred tc_lvl (classifyPredType (ctPred insol))
trulyInsoluble _tc_lvl insol
| CHoleCan {} <- insol = isOutOfScopeCt insol
| otherwise = True
instance Outputable WantedConstraints where
ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
......
......@@ -51,7 +51,7 @@ module TcSMonad (
emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
matchableGivens, prohibitedSuperClassSolve,
getUnsolvedInerts,
removeInertCts,
removeInertCts, getPendingScDicts, isPendingScDict,
addInertCan, addInertEq, insertFunEq,
emitInsoluble, emitWorkNC, emitWorkCt,
......@@ -558,9 +558,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
-- (b) emitDerivedShadows
, inert_dicts :: DictMap Ct
-- Dictionaries only, index is the class
-- NB: index is /not/ the whole type because FD reactions
-- need to match the class but not necessarily the whole type.
-- Dictionaries only
, inert_safehask :: DictMap Ct
-- Failed dictionary resolution due to Safe Haskell overlapping
......@@ -1568,7 +1566,7 @@ After solving the Givens we take two things out of the inert set
a) The insolubles; we return these to report inaccessible code
We return these separately. We don't want to leave them in
the inert set, lest we onfuse them with insolubles arising from
the inert set, lest we confuse them with insolubles arising from
solving wanteds
b) Any Derived CFunEqCans. Derived CTyEqCans are in the
......@@ -1633,6 +1631,35 @@ getInertGivens
$ concat (varEnvElts (inert_eqs inerts))
; return (filter isGivenCt all_cts) }
getPendingScDicts :: TcS [Ct]
-- Find all inert Given dictionaries whose cc_pend_sc flag is True
-- Set the flag to False in the inert set, and return that Ct
getPendingScDicts = updRetInertCans get_sc_dicts
where
get_sc_dicts ic@(IC { inert_dicts = dicts })
= (sc_pend_dicts, ic')
where
ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
sc_pend_dicts :: [Ct]
sc_pend_dicts = foldDicts get_pending dicts []
get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True
-- but flipping the flag
get_pending dict dicts
| Just dict' <- isPendingScDict dict = dict' : dicts
| otherwise = dicts
add :: Ct -> DictMap Ct -> DictMap Ct
add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
= addDict dicts cls tys ct
add ct _ = pprPanic "getPendingScDicts" (ppr ct)
isPendingScDict :: Ct -> Maybe Ct
isPendingScDict ct@(CDictCan { cc_pend_sc = True })
= Just (ct { cc_pend_sc = False })
isPendingScDict _ = Nothing
getUnsolvedInerts :: TcS ( Bag Implication
, Cts -- Tyvar eqs: a ~ ty
, Cts -- Fun eqs: F a ~ ty
......
......@@ -31,6 +31,7 @@ import PrelNames
import TcErrors
import TcEvidence
import TcInteract
import TcCanonical ( makeSuperClasses, mkGivensWithSuperClasses )
import TcMType as TcM
import TcRnMonad as TcM
import TcSMonad as TcS
......@@ -422,18 +423,36 @@ simplifyDefault theta
------------------
tcCheckSatisfiability :: Bag EvVar -> TcM Bool
-- Return True if satisfiable, False if definitely contradictory
tcCheckSatisfiability givens
tcCheckSatisfiability given_ids
= do { lcl_env <- TcM.getLclEnv
; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
; traceTc "checkSatisfiability {" (ppr givens)
; (res, _ev_binds) <- runTcS $
do { cts <- solveSimpleGivens given_loc (bagToList givens)
; return (not (isEmptyBag cts)) }
; traceTc "checkSatisfiability }" (ppr res)
; return (not res) }
{-
*********************************************************************************
do { traceTcS "checkSatisfiability {" (ppr given_ids)
; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
-- Need their superclasses, because (Int ~ Bool) has (Int ~~ Bool)
-- as a superclass, and it's the latter that is insoluble
; insols <- solveSimpleGivens given_cts
; insols <- try_harder insols
; traceTcS "checkSatisfiability }" (ppr insols)
; return (isEmptyBag insols) }
; return res }
where
try_harder :: Cts -> TcS Cts
-- Maybe we have to search up the superclass chain to find
-- an unsatisfiable constraint. Example: pmcheck/T3927b.
try_harder insols
| not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
= return insols -- Hurrah -- stop now.
| otherwise
= do { pending_given <- getPendingScDicts
; new_given <- makeSuperClasses pending_given
; if null new_given -- No new superclasses to try, so no point
then return emptyBag -- in continuing
else -- Some new superclasses; have a go
do { insols <- solveSimpleGivens new_given
; try_harder insols } }
{- ********************************************************************************
* *
* Inference
* *
......@@ -971,12 +990,13 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
-- of adding Derived insolubles twice; see
-- TcSMonad Note [Do not add duplicate derived insolubles]
; wc1 <- solveSimpleWanteds simples
; (no_new_scs, wc1) <- expandSuperClasses wc1
; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
; dflags <- getDynFlags
; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
(WC { wc_simple = simples1, wc_impl = implics2
, wc_insol = insols `unionBags` insols1 })
......@@ -987,10 +1007,10 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
; return final_wc }
simpl_loop :: Int -> IntWithInf -> Cts
simpl_loop :: Int -> IntWithInf -> Cts -> Bool
-> WantedConstraints
-> TcS WantedConstraints
simpl_loop n limit floated_eqs
simpl_loop n limit floated_eqs no_new_given_scs
wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
| n `intGtLimit` limit
= failTcS (hang (ptext (sLit "solveWanteds: too many iterations")
......@@ -998,7 +1018,7 @@ simpl_loop n limit floated_eqs
2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
, ppr wc ] ))
| no_floated_eqs
| isEmptyBag floated_eqs && no_new_given_scs
= return wc -- Done!
| otherwise
......@@ -1011,19 +1031,42 @@ simpl_loop n limit floated_eqs
-- NB: the floated_eqs may include /derived/ equalities
-- arising from fundeps inside an implication
; (no_new_scs, wc1) <- expandSuperClasses wc1
; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
-- solveImplications may make progress only if unifs2 holds
-- We have already tried to solve the nested implications once
-- Try again only if we have unified some meta-variables
-- (which is a bit like adding more givens
-- See Note [Cutting off simpl_loop]
; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
then return (emptyBag, implics)
else solveNestedImplications (implics `unionBags` implics1)
; simpl_loop (n+1) limit floated_eqs2
; simpl_loop (n+1) limit floated_eqs2 no_new_scs
(WC { wc_simple = simples1, wc_impl = implics2
, wc_insol = insols `unionBags` insols1 }) }
where
no_floated_eqs = isEmptyBag floated_eqs
expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
-- If there are any unsolved wanteds, expand one step of superclasses for
-- unsolved wanteds or givens
-- See Note [The superclass story] in TcCanonical
expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
| isEmptyBag unsolved -- No unsolved simple wanteds, so do not add suerpclasses
= return (True, wc)
| otherwise
= do { let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
get acc ct = case isPendingScDict ct of
Just ct' -> (ct':acc, ct')
Nothing -> (acc, ct)
; pending_given <- getPendingScDicts
; if null pending_given && null pending_wanted
then return (True, wc)
else
do { new_given <- makeSuperClasses pending_given
; new_insols <- solveSimpleGivens new_given
; new_wanted <- makeSuperClasses pending_wanted
; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
, wc_insol = insols `unionBags` new_insols }) } }
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
......@@ -1054,7 +1097,7 @@ solveImplication :: Implication -- Wanted
solveImplication imp@(Implic { ic_tclvl = tclvl
, ic_binds = m_ev_binds
, ic_skols = skols
, ic_given = givens
, ic_given = given_ids
, ic_wanted = wanteds
, ic_info = info
, ic_status = status
......@@ -1071,15 +1114,21 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
-- Solve the nested constraints
; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
<- nestImplicTcS m_ev_binds (mkVarSet (skols ++ givens)) tclvl $
do { given_insols <- solveSimpleGivens (mkGivenLoc tclvl info env) givens
; no_eqs <- getNoGivenEqs tclvl skols
<- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
do { let loc = mkGivenLoc tclvl info env
; givens_w_scs <- mkGivensWithSuperClasses loc given_ids
; given_insols <- solveSimpleGivens givens_w_scs
; residual_wanted <- solveWanteds wanteds
-- solveWanteds, *not* solveWantedsAndDrop, because
-- we want to retain derived equalities so we can float
-- them out in floatEqualities
; no_eqs <- getNoGivenEqs tclvl skols
-- Call getNoGivenEqs /after/ solveWanteds, because
-- solveWanteds can augment the givens, via expandSuperClasses,
-- to reveal given superclass equalities
; return (no_eqs, given_insols, residual_wanted) }
; (floated_eqs, residual_wanted)
......@@ -1355,27 +1404,17 @@ of progress. Trac #8474 is a classic example:
* So there is no point in attempting to re-solve
?yn:betan => [W] ?x:Int
because we'll just get the same [D] again
via solveNestedImplications, because we'll just get the
same [D] again
* If we *do* re-solve, we'll get an ininite loop. It is cut off by
the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
exponentially many) iterations!
Conclusion: we should iterate simpl_loop iff we will get more 'givens'
in the inert set when solving the nested implications. That is the
result of prepareInertsForImplications is larger. How can we tell
this?
Consider floated_eqs (all wanted or derived):
(a) [W/D] CTyEqCan (a ~ ty). This can give rise to a new given only by causing
a unification. So we count those unifications.
(b) [W] CFunEqCan (F tys ~ xi). Even though these are wanted, they
are pushed in as givens by prepareInertsForImplications. See Note
[Preparing inert set for implications] in TcSMonad. But because
of that very fact, we won't generate another copy if we iterate
simpl_loop. So we iterate if there any of these
Conclusion: we should call solveNestedImplications only if we did
some unifiction in solveSimpleWanteds; because that's the only way
we'll get more Givens (a unificaiton is like adding a Given) to
allow the implication to make progress.
-}
promoteTyVar :: TcLevel -> TcTyVar -> TcM ()
......
......@@ -1927,9 +1927,6 @@ Validity checking is done once the mutually-recursive knot has been
tied, so we can look at things freely.
-}
checkClassCycleErrs :: Class -> TcM ()
checkClassCycleErrs cls = mapM_ recClsErr (calcClassCycles cls)
checkValidTyCl :: TyCon -> TcM TyCon
checkValidTyCl tc
= setSrcSpan (getSrcSpan tc) $
......@@ -2208,9 +2205,10 @@ checkNewDataCon con
checkValidClass :: Class -> TcM ()
checkValidClass cls
= do { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
; nullary_type_classes <- xoptM Opt_NullaryTypeClasses
; fundep_classes <- xoptM Opt_FunctionalDependencies
; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
; nullary_type_classes <- xoptM Opt_NullaryTypeClasses
; fundep_classes <- xoptM Opt_FunctionalDependencies
; undecidable_super_classes <- xoptM Opt_UndecidableSuperClasses
-- Check that the class is unary, unless multiparameter type classes
-- are enabled; also recognize deprecated nullary type classes
......@@ -2225,7 +2223,11 @@ checkValidClass cls
-- Now check for cyclic superclasses
-- If there are superclass cycles, checkClassCycleErrs bails.
; checkClassCycleErrs cls
; unless undecidable_super_classes $
case checkClassCycles cls of
Just err -> setSrcSpan (getSrcSpan cls) $
addErrTc err
Nothing -> return ()
-- Check the class operations.
-- But only if there have been no earlier errors
......@@ -2541,11 +2543,6 @@ recSynErr syn_decls
sorted_decls = sortLocated syn_decls
ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
recClsErr :: [TyCon] -> TcRn ()
recClsErr cycles
= addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
badDataConTyCon :: DataCon -> Type -> Type -> SDoc
badDataConTyCon data_con res_ty_tmpl actual_res_ty
= hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
......
......@@ -13,7 +13,8 @@ files for imported data types.
module TcTyDecls(
calcRecFlags, RecTyInfo(..),
calcSynCycles, calcClassCycles,
calcSynCycles,
checkClassCycles,
-- * Roles
RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots,
......@@ -56,19 +57,18 @@ import BasicTypes
import SrcLoc
import Unique ( mkBuiltinUnique )
import Outputable
import UniqSet
import Util
import Maybes
import Data.List
import Bag
import FastString ( fastStringToByteString )
import FastString
import Control.Monad
{-
************************************************************************
* *
Cycles in class and type synonym declarations
Cycles in type synonym declarations
* *
************************************************************************
......@@ -139,123 +139,100 @@ mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
{-
Note [Superclass cycle check]
{- Note [Superclass cycle check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can't allow cycles via superclasses because it would result in the
type checker looping when it canonicalises a class constraint (superclasses
are added during canonicalisation). More precisely, given a constraint
C ty1 .. tyn
we want to instantiate all of C's superclasses, transitively, and
that set must be finite. So if
class (D b, E b a) => C a b
then when we encounter the constraint
C ty1 ty2
we'll instantiate the superclasses
(D ty2, E ty2 ty1)
and then *their* superclasses, and so on. This set must be finite!
It is OK for superclasses to be type synonyms for other classes, so
must "look through" type synonyms. Eg
type X a = C [a]
class X a => C a -- No! Recursive superclass!
We want definitions such as:
class C cls a where cls a => a -> a
class C D a => D a where
to be accepted, even though a naive acyclicity check would reject the
program as having a cycle between D and its superclass. Why? Because
when we instantiate
D ty1
we get the superclas
C D ty1
and C has no superclasses, so we have terminated with a finite set.
More precisely, the rule is this: the superclasses sup_C of a class C
are rejected iff:
The superclass cycle check for C decides if we can statically
guarantee that expanding C's superclass cycles transitively is
guaranteed to terminate. This is a Haskell98 requirement,
but one that we lift with -XUndecidableSuperClasses.
C \elem expand(sup_C)
Where expand is defined as follows:
(1) expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
(2) expand(D ty1 ... tyN) = {D}
\union sup_D[ty1/x1, ..., tyP/xP]
\union expand(ty(P+1)) ... \union expand(tyN)
where (D x1 ... xM) is a class, P = min(M,N)
(3) expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
where T is not a class
Eqn (1) is conservative; when there's a type variable at the head,
look in all the argument types. Eqn (2) expands superclasses; the
third component of the union is like Eqn (1). Eqn (3) happens mainly
when the context is a (constraint) tuple, such as (Eq a, Show a).
Furthermore, expand always looks through type synonyms.
The worry is that a superclass cycle could make the type checker loop.
More precisely, with a constraint (Given or Wanted)
C ty1 .. tyn
one approach is to instantiate all of C's superclasses, transitively.
We can only do so if that set is finite.
This potential loop occurs only through superclasses. This, for
exmaple, is fine
class C a where
op :: C b => a -> b -> b
even though C's full definition uses C.
Making the check static also makes it conservative. Eg
type family F a
class F a => C a
Here an instance of (F a) might mention C:
type instance F [a] = C a
and now we'd have a loop.
The static check works like this, starting with C
* Look at C's superclass predicates
* If any is a type-function application,
or is headed by a type variable, fail
* If any has C at the head, fail
* If any has a type class D at the head,
make the same test with D
A tricky point is: what if there is a type variable at the head?
Consider this:
class f (C f) => C f
class c => Id c
and now expand superclasses for constraint (C Id):
C Id
--> Id (C Id)
--> C Id
--> ....
Each step expands superclasses one layer, and clearly does not terminate.
-}
calcClassCycles :: Class -> [[TyCon]]
calcClassCycles cls
= nubBy eqAsCycle $
expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []