Commit 1189196c authored by Simon Peyton Jones's avatar Simon Peyton Jones

Re-do superclass solving (again); fixes #10423

TcInstDcls.tcSuperClasses was getting increasingly baroque as a
succession of tickets (#10423 being the latest) pointed out that
my cunning plan was not so cunning.

The big issue is how to restrict the evidence that we generate
for superclass constraints in an instance declaration to avoid
superclass loops.  See Note [Recursive superclasses] in TcInstDcls
which explains the plan.

The question is how to implement the plan.  The new implementation is
much neater, and is described in Note [Solving superclass constraints]
in TcInstDcls.
parent 90fde522
......@@ -320,7 +320,17 @@ newSCWorkFromFlavored flavor cls xis
= return ()
| CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
= do { given_evs <- newGivenEvVars loc (mkEvScSelectors (EvId evar) cls xis)
= do { let size = sizePred (mkClassPred cls xis)
loc' = case ctLocOrigin loc of
GivenOrigin InstSkol
-> loc { ctl_origin = GivenOrigin (InstSC size) }
GivenOrigin (InstSC n)
-> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
_ -> loc
-- See Note [Solving superclass constraints] in TcInstDcls
-- for explantation of loc'
; given_evs <- newGivenEvVars loc' (mkEvScSelectors (EvId evar) cls xis)
; emitWorkNC given_evs }
| isEmptyVarSet (tyVarsOfTypes xis)
......
......@@ -32,7 +32,7 @@ import TcDeriv
import TcEnv
import TcHsType
import TcUnify
import Coercion ( pprCoAxiom, isReflCo, mkSymCo, mkSubCo )
import Coercion ( pprCoAxiom {- , isReflCo, mkSymCo, mkSubCo -} )
import MkCore ( nO_METHOD_BINDING_ERROR_ID )
import Type
import TcEvidence
......@@ -43,8 +43,8 @@ import Class
import Var
import VarEnv
import VarSet
import PrelNames ( typeableClassName, genericClassNames
, knownNatClassName, knownSymbolClassName )
import PrelNames ( typeableClassName, genericClassNames )
-- , knownNatClassName, knownSymbolClassName )
import Bag
import BasicTypes
import DynFlags
......@@ -993,55 +993,15 @@ tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
-- See Note [Recursive superclasses] for why this is so hard!
-- In effect, be build a special-purpose solver for the first step
-- of solving each superclass constraint
tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_theta
= do { traceTc "tcSuperClasses" (ppr cls $$ ppr inst_tys $$ ppr given_cls_preds)
; (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds _fam_envs sc_theta
= do { (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
; return (ids, listToBag binds, listToBag implics) }
where
loc = getSrcSpan dfun_id
head_size = sizeTypes inst_tys
------------
given_cls_preds :: [(TcPredType, EvTerm)] -- (type of that ev_term, ev_term)
-- given_cls_preds is the list of (type, ev_term) that can be derived
-- from the dfun_evs, using the rules (sc1) and (sc2) of
-- Note [Recursive superclasses] below
-- When solving for superclasses, we search this list
given_cls_preds
= [ ev_pr | dfun_ev <- dfun_evs
, ev_pr <- super_classes (idType dfun_ev, EvId dfun_ev) ]
------------
super_classes ev_pair
= case classifyPredType pred of
ClassPred cls tys -> (pred, ev_tm) : super_classes_help ev_tm cls tys
_ -> []
where
(pred, ev_tm) = normalise_pr ev_pair
------------
super_classes_help :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
super_classes_help ev_tm cls tys -- ev_tm :: cls tys
| not (isCTupleClass cls)
, sizeTypes tys >= head_size -- Here is where we test for
= [] -- a smaller dictionary
| otherwise
= concatMap super_classes (mkEvScSelectors ev_tm cls tys)
------------
normalise_pr :: (TcPredType, EvTerm) -> (TcPredType, EvTerm)
-- Normalise type functions as much as possible
normalise_pr (pred, ev_tm)
| isReflCo norm_co = (pred, ev_tm)
| otherwise = (norm_pred, mkEvCast ev_tm tc_co)
where
(norm_co, norm_pred) = normaliseType fam_envs Nominal pred
tc_co = TcCoercion (mkSubCo norm_co)
------------
loc = getSrcSpan dfun_id
size = sizePred (mkClassPred cls inst_tys)
tc_super (sc_pred, n)
= do { (sc_implic, sc_ev_id) <- checkInstConstraints $
emit_sc_pred fam_envs sc_pred
= do { (sc_implic, sc_ev_id) <- checkInstConstraints $ \_ ->
emitWanted (ScOrigin size) sc_pred
; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
; let sc_top_ty = mkForAllTys tyvars (mkPiTypes dfun_evs sc_pred)
......@@ -1057,68 +1017,6 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
, abs_binds = emptyBag }
; return (sc_top_id, L loc bind, sc_implic) }
-------------------
emit_sc_pred fam_envs sc_pred ev_binds
| (sc_co, norm_sc_pred) <- normaliseType fam_envs Nominal sc_pred
-- sc_co :: sc_pred ~ norm_sc_pred
, ClassPred cls tys <- classifyPredType norm_sc_pred
, not (usesCustomSolver cls)
-- Some classes (e.g., `Typeable`, `KnownNat`) have custom solving
-- rules, which is why we exclude it from the short cut,
-- and fall through to calling the solver.
= do { sc_ev_tm <- emit_sc_cls_pred norm_sc_pred cls tys
; sc_ev_id <- newEvVar sc_pred
; let tc_co = TcCoercion (mkSubCo (mkSymCo sc_co))
; addTcEvBind ev_binds (mkWantedEvBind sc_ev_id (mkEvCast sc_ev_tm tc_co))
-- This is where we set the evidence for the superclass, and do so
-- (very unusually) *outside the solver*. That's why
-- checkInstConstraints passes in the evidence bindings
; return sc_ev_id }
| otherwise
= do { sc_ev_id <- emitWanted ScOrigin sc_pred
; traceTc "tcSuperClass 4" (ppr sc_pred $$ ppr sc_ev_id)
; return sc_ev_id }
-------------------
emit_sc_cls_pred sc_pred cls tys
| (ev_tm:_) <- [ ev_tm | (ev_ty, ev_tm) <- given_cls_preds
, ev_ty `tcEqType` sc_pred ]
= do { traceTc "tcSuperClass 1" (ppr sc_pred $$ ppr ev_tm)
; return ev_tm }
| otherwise
= do { inst_envs <- tcGetInstEnvs
; case lookupInstEnv False inst_envs cls tys of
([(ispec, dfun_inst_tys)], [], _) -- A single match
-> do { let dfun_id = instanceDFunId ispec
; (inst_tys, inst_theta) <- instDFunType dfun_id dfun_inst_tys
; arg_evs <- emitWanteds ScOrigin inst_theta
; let dict_app = EvDFunApp dfun_id inst_tys arg_evs
; traceTc "tcSuperClass 2" (ppr sc_pred $$ ppr dict_app)
; return dict_app }
_ -> -- No instance, so we want to report an error
-- Emitting it as an 'insoluble' prevents the solver
-- attempting to solve it (which might, wrongly, succeed)
do { sc_ev <- newWanted ScOrigin sc_pred
; emitInsoluble (mkNonCanonical sc_ev)
; traceTc "tcSuperClass 3" (ppr sc_pred $$ ppr sc_ev)
; return (ctEvTerm sc_ev) } }
-- | Do we use a custom solver, which is safe to use when solving super-class
-- constraints.
usesCustomSolver :: Class -> Bool
usesCustomSolver cls = name == typeableClassName
|| name == knownNatClassName
|| name == knownSymbolClassName
where
name = className cls
-------------------
checkInstConstraints :: (EvBindsVar -> TcM result)
-> TcM (Implication, result)
......@@ -1153,7 +1051,6 @@ encountered in practice.
See also tests tcrun020, tcrun021, tcrun033
----- THE PROBLEM --------
The problem is that it is all too easy to create a class whose
superclass is bottom when it should not be.
......@@ -1239,8 +1136,39 @@ that is *not* smaller than the target so we can't take *its*
superclasses. As a result the program is rightly rejected, unless you
add (Super (Fam a)) to the context of (i3).
Note [Silent superclass arguments] (historical interest)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Solving superclass constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
How do we ensure that every superclass witness is generated by
one of (sc1) (sc2) or (sc3) in Note [Recursive superclases].
Answer:
* Superclass "wanted" constraints have CtOrigin of (ScOrigin size)
where 'size' is the size of the instance declaration. e.g.
class C a => D a where...
instance blah => D [a] where ...
The wanted superclass constraint for C [a] has origin
ScOrigin size, where size = size( D [a] ).
* (sc1) When we rewrite such a wanted constraint, it retains its
origin. But if we apply an instance declaration, we can set the
origin to (ScOrigin infinity), thus lifting any restrictions by
making prohibitedSuperClassSolve return False.
* (sc2) ScOrigin wanted constraints can't be solved from a
superclass selection, except at a smaller type. This test is
implemented by TcInteract.prohibitedSuperClassSolve
* The "given" constraints of an instance decl have CtOrigin
GivenOrigin InstSkol.
* When we make a superclass selection from InstSkol we use
a SkolemInfo of (InstSC size), where 'size' is the size of
the constraint whose superclass we are taking. An similarly
when taking the superclass of an InstSC. This is implemented
in TcCanonical.newSCWorkFromFlavored
Note [Silent superclass arguments] (historical interest only)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
NB1: this note describes our *old* solution to the
recursive-superclass problem. I'm keeping the Note
for now, just as institutional memory.
......
......@@ -8,7 +8,7 @@ module TcInteract (
#include "HsVersions.h"
import BasicTypes ()
import BasicTypes ( infinity )
import HsTypes ( hsIPNameFS )
import FastString
import TcCanonical
......@@ -762,11 +762,21 @@ solveOneFromTheOther ev_i ev_w
-- so it's safe to continue on from this point
= return (IRDelete, False)
| CtWanted { ctev_evar = ev_id } <- ev_w
| CtWanted { ctev_loc = loc_w } <- ev_w
, prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
= return (IRDelete, False)
| CtWanted { ctev_evar = ev_id } <- ev_w -- Inert is Given or Wanted
= do { setWantedEvBind ev_id (ctEvTerm ev_i)
; return (IRKeep, True) }
| CtWanted { ctev_evar = ev_id } <- ev_i
| CtWanted { ctev_loc = loc_i } <- ev_i -- Work item is Given
, prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
= return (IRKeep, False) -- Just discard the un-usable Given
-- This never actually happens because
-- Givens get processed first
| CtWanted { ctev_evar = ev_id } <- ev_i -- Work item is Given
= do { setWantedEvBind ev_id (ctEvTerm ev_w)
; return (IRReplace, True) }
......@@ -774,51 +784,84 @@ solveOneFromTheOther ev_i ev_w
-- See Note [Replacement vs keeping]
| lvl_i == lvl_w
= do { binds <- getTcEvBindsMap
; if has_binding binds ev_w && not (has_binding binds ev_i)
then return (IRReplace, True)
else return (IRKeep, True) }
; return (same_level_strategy binds, True) }
| otherwise -- Both are Given
= return (if use_replacement then IRReplace else IRKeep, True)
where
| otherwise -- Both are Given, levels differ
= return (different_level_strategy, True)
where
pred = ctEvPred ev_i
loc_i = ctEvLoc ev_i
loc_w = ctEvLoc ev_w
lvl_i = ctLocLevel loc_i
lvl_w = ctLocLevel loc_w
different_level_strategy
| isIPPred pred, lvl_w > lvl_i = IRReplace
| lvl_w < lvl_i = IRReplace
| otherwise = IRKeep
same_level_strategy binds -- Both Given
| GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
= case ctLocOrigin loc_w of
GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
| otherwise -> IRKeep
_ -> IRReplace
| GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
= IRKeep
| has_binding binds ev_w
, not (has_binding binds ev_i)
= IRReplace
| otherwise = IRKeep
has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
use_replacement
| isIPPred pred = lvl_w > lvl_i
| otherwise = lvl_w < lvl_i
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in TcInstDcls
prohibitedSuperClassSolve from_loc solve_loc
| GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
, ScOrigin wanted_size <- ctLocOrigin solve_loc
= given_size >= wanted_size
| otherwise
= False
{-
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
we keep?
we keep? More subtle than you might think!
* For implicit parameters we want to keep the innermost (deepest)
one, so that it overrides the outer one.
See Note [Shadowing of Implicit Parameters]
* Constraints come from different levels (different_level_strategy)
* For everything else, we want to keep the outermost one. Reason: that
makes it more likely that the inner one will turn out to be unused,
and can be reported as redundant. See Note [Tracking redundant constraints]
in TcSimplify.
- For implicit parameters we want to keep the innermost (deepest)
one, so that it overrides the outer one.
See Note [Shadowing of Implicit Parameters]
It transpires that using the outermost one is reponsible for an
8% performance improvement in nofib cryptarithm2, compared to
just rolling the dice. I didn't investigate why.
- For everything else, we want to keep the outermost one. Reason: that
makes it more likely that the inner one will turn out to be unused,
and can be reported as redundant. See Note [Tracking redundant constraints]
in TcSimplify.
* If there is no "outermost" one, we keep the one that has a non-trivial
evidence binding. Note [Tracking redundant constraints] again.
Example: f :: (Eq a, Ord a) => blah
then we may find [G] sc_sel (d1::Ord a) :: Eq a
[G] d2 :: Eq a
We want to discard d2 in favour of the superclass selection from
the Ord dictionary.
It transpires that using the outermost one is reponsible for an
8% performance improvement in nofib cryptarithm2, compared to
just rolling the dice. I didn't investigate why.
* Constaints coming from the same level (i.e. same implication)
- Always get rid of InstSC ones if possible, since they are less
useful for solving. If both are InstSC, choose the one with
the smallest TypeSize
See Note [Solving superclass constraints] in TcInstDcls
- Keep the one that has a non-trivial evidence binding.
Note [Tracking redundant constraints] again.
Example: f :: (Eq a, Ord a) => blah
then we may find [G] sc_sel (d1::Ord a) :: Eq a
[G] d2 :: Eq a
We want to discard d2 in favour of the superclass selection from
the Ord dictionary.
* Finally, when there is still a choice, use IRKeep rather than
IRReplace, to avoid unnecesary munging of the inert set.
......@@ -1595,7 +1638,14 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
dict_pred = mkClassPred cls xis
dict_loc = ctEvLoc fl
dict_origin = ctLocOrigin dict_loc
deeper_loc = bumpCtLocDepth dict_loc
deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
zap_origin loc -- After applying an instance we can set ScOrigin to
-- infinity, so that prohibitedSuperClassSolve never fires
| ScOrigin {} <- dict_origin
= setCtLocOrigin loc (ScOrigin infinity)
| otherwise
= loc
solve_from_instance :: [TcPredType] -> ([EvId] -> EvTerm) -> TcS (StopOrContinue Ct)
-- Precondition: evidence term matches the predicate workItem
......@@ -1992,7 +2042,7 @@ matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS Lookup
-- First check whether there is an in-scope Given that could
-- match this constraint. In that case, do not use top-level
-- instances. See Note [Instance and Given overlap]
matchClassInst dflags inerts clas tys _
matchClassInst dflags inerts clas tys loc
| not (xopt Opt_IncoherentInstances dflags)
, not (isEmptyBag matchable_givens)
= do { traceTcS "Delaying instance application" $
......@@ -2007,8 +2057,9 @@ matchClassInst dflags inerts clas tys _
matchable_given ct
| CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl } <- ct
, isGiven fl
, CtGiven { ctev_loc = loc_g } <- fl
, Just {} <- tcUnifyTys bind_meta_tv tys sys
, not (prohibitedSuperClassSolve loc_g loc)
= ASSERT( clas_g == clas ) True
matchable_given _ = False
......
......@@ -1966,7 +1966,13 @@ data SkolemInfo
-- The rest are for non-scoped skolems
| ClsSkol Class -- Bound at a class decl
| InstSkol -- Bound at an instance decl
| InstSC TypeSize -- A "given" constraint obtained by superclass selection
-- from an InstSkol, giving the largest class from
-- which we made a superclass selection in the chain
-- See Note [Solving superclass constraints] in TcInstDcls
| DataSkol -- Bound at a data type declaration
| FamInstSkol -- Bound at a family instance decl
| PatSkol -- An existential type variable bound by a pattern for
......@@ -2006,6 +2012,7 @@ pprSkolInfo (IPSkol ips) = ptext (sLit "the implicit-parameter binding") <>
<+> pprWithCommas ppr ips
pprSkolInfo (ClsSkol cls) = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
pprSkolInfo InstSkol = ptext (sLit "the instance declaration")
pprSkolInfo (InstSC n) = ptext (sLit "the instance declaration") <> ifPprDebug (parens (ppr n))
pprSkolInfo DataSkol = ptext (sLit "a data type declaration")
pprSkolInfo FamInstSkol = ptext (sLit "a family instance declaration")
pprSkolInfo BracketSkol = ptext (sLit "a Template Haskell bracket")
......@@ -2087,7 +2094,10 @@ data CtOrigin
| RecordUpdOrigin
| ViewPatOrigin
| ScOrigin -- Typechecking superclasses of an instance declaration
| ScOrigin TypeSize -- Typechecking superclasses of an instance declaration
-- whose head has the given size
-- See Note [Solving superclass constraints] in TcInstDcls
| DerivOrigin -- Typechecking deriving
| DerivOriginDC DataCon Int
-- Checking constraints arising from this data con and field index
......@@ -2186,7 +2196,8 @@ pprCtO (PArrSeqOrigin seq) = hsep [ptext (sLit "the parallel array sequence"),
pprCtO SectionOrigin = ptext (sLit "an operator section")
pprCtO TupleOrigin = ptext (sLit "a tuple")
pprCtO NegateOrigin = ptext (sLit "a use of syntactic negation")
pprCtO ScOrigin = ptext (sLit "the superclasses of an instance declaration")
pprCtO (ScOrigin n) = ptext (sLit "the superclasses of an instance declaration")
<> ifPprDebug (parens (ppr n))
pprCtO DerivOrigin = ptext (sLit "the 'deriving' clause of a data type declaration")
pprCtO StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
pprCtO DefaultOrigin = ptext (sLit "a 'default' declaration")
......
......@@ -1074,8 +1074,8 @@ warnRedundantGivens (SigSkol ctxt _)
FunSigCtxt _ warn_redundant -> warn_redundant
ExprSigCtxt -> True
_ -> False
warnRedundantGivens InstSkol = True
warnRedundantGivens _ = False
warnRedundantGivens (InstSkol {}) = True
warnRedundantGivens _ = False
neededEvVars :: EvBindMap -> VarSet -> VarSet
-- Find all the evidence variables that are "needed",
......
......@@ -146,7 +146,9 @@ module TcType (
pprKind, pprParendKind, pprSigmaType,
pprType, pprParendType, pprTypeApp, pprTyThingCategory,
pprTheta, pprThetaArrowTy, pprClassPred
pprTheta, pprThetaArrowTy, pprClassPred,
TypeSize, sizePred, sizeType, sizeTypes
) where
......@@ -1793,3 +1795,80 @@ In turn that means you can't write
Reason: the back end falls over with panic "primRepHint:VoidRep";
and there is no compelling reason to permit it
-}
{-
************************************************************************
* *
The "Paterson size" of a type
* *
************************************************************************
-}
{-
Note [Paterson conditions on PredTypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We are considering whether *class* constraints terminate
(see Note [Paterson conditions]). Precisely, the Paterson conditions
would have us check that "the constraint has fewer constructors and variables
(taken together and counting repetitions) than the head.".
However, we can be a bit more refined by looking at which kind of constraint
this actually is. There are two main tricks:
1. It seems like it should be OK not to count the tuple type constructor
for a PredType like (Show a, Eq a) :: Constraint, since we don't
count the "implicit" tuple in the ThetaType itself.
In fact, the Paterson test just checks *each component* of the top level
ThetaType against the size bound, one at a time. By analogy, it should be
OK to return the size of the *largest* tuple component as the size of the
whole tuple.
2. Once we get into an implicit parameter or equality we
can't get back to a class constraint, so it's safe
to say "size 0". See Trac #4200.
NB: we don't want to detect PredTypes in sizeType (and then call
sizePred on them), or we might get an infinite loop if that PredType
is irreducible. See Trac #5581.
-}
type TypeSize = IntWithInf
sizeType :: Type -> TypeSize
-- Size of a type: the number of variables and constructors
sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
sizeType (TyVarTy {}) = 1
sizeType (TyConApp tc tys)
| isTypeFamilyTyCon tc = infinity -- Type-family applications can
-- expand to any arbitrary size
| otherwise = sizeTypes tys + 1
sizeType (LitTy {}) = 1
sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
sizeType (AppTy fun arg) = sizeType fun + sizeType arg
sizeType (ForAllTy _ ty) = sizeType ty
sizeTypes :: [Type] -> TypeSize
-- IA0_NOTE: Avoid kinds.
sizeTypes xs = sum (map sizeType tys)
where tys = filter (not . isKind) xs
-- Note [Size of a predicate]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~
-- We are considering whether class constraints terminate.
-- Equality constraints and constraints for the implicit
-- parameter class always termiante so it is safe to say "size 0".
-- (Implicit parameter constraints always terminate because
-- there are no instances for them---they are only solved by
-- "local instances" in expressions).
-- See Trac #4200.
sizePred :: PredType -> TypeSize
sizePred p
= case classifyPredType p of
ClassPred cls tys
| isIPClass cls -> 0 -- See Note [Size of a predicate]
| isCTupleClass cls -> maximum (0 : map sizePred tys)
| otherwise -> sizeTypes tys
EqPred {} -> 0 -- See Note [Size of a predicate]
IrredPred ty -> sizeType ty
......@@ -11,7 +11,7 @@ module TcValidity (
checkValidTheta, checkValidFamPats,
checkValidInstance, validDerivPred,
checkInstTermination, checkValidTyFamInst, checkTyFamFreeness,
checkConsistentFamInst, sizeTypes,
checkConsistentFamInst,
arityErr, badATErr
) where
......@@ -45,7 +45,6 @@ import Util
import ListSetOps
import SrcLoc
import Outputable
import BasicTypes ( IntWithInf, infinity )
import FastString
import Control.Monad
......@@ -1295,82 +1294,6 @@ famPatErr fam_tc tvs pats
2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
{-
************************************************************************
* *
The "Paterson size" of a type
* *
************************************************************************
-}
{-
Note [Paterson conditions on PredTypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We are considering whether *class* constraints terminate
(see Note [Paterson conditions]). Precisely, the Paterson conditions
would have us check that "the constraint has fewer constructors and variables
(taken together and counting repetitions) than the head.".
However, we can be a bit more refined by looking at which kind of constraint
this actually is. There are two main tricks:
1. It seems like it should be OK not to count the tuple type constructor
for a PredType like (Show a, Eq a) :: Constraint, since we don't
count the "implicit" tuple in the ThetaType itself.
In fact, the Paterson test just checks *each component* of the top level
ThetaType against the size bound, one at a time. By analogy, it should be
OK to return the size of the *largest* tuple component as the size of the
whole tuple.
2. Once we get into an implicit parameter or equality we
can't get back to a class constraint, so it's safe
to say "size 0". See Trac #4200.
NB: we don't want to detect PredTypes in sizeType (and then call
sizePred on them), or we might get an infinite loop if that PredType
is irreducible. See Trac #5581.
-}
type TypeSize = IntWithInf
sizeType :: Type -> TypeSize
-- Size of a type: the number of variables and constructors
sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
sizeType (TyVarTy {}) = 1
sizeType (TyConApp tc tys)
| isTypeFamilyTyCon tc = infinity -- Type-family applications can
-- expand to any arbitrary size