Commit ddbb97d0 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Another major improvement of "improvement"

I wasn't very happy with my fix to Trac #10009. This is much better.

The main idea is that the inert set now contains a "model", which
embodies *all* the (nominal) equalities that we know about, with
a view to exposing unifications.  This requires a lot fewer iterations
of the solver than before.

There are extensive comments in
 TcSMonad:  Note [inert_model: the inert model]
            Note [Adding an inert canonical constraint the InertCans]

The big changes are

  * New inert_model field in InertCans

  * Functions addInertEq, addInertCan deal with adding a
    constraint, maintaining the model

  * A nice improvement is that unification variables can
    unify with fmvs, so that from, say   alpha ~ fmv
    we get              alpha := fmv
    See Note [Orientation of equalities with fmvs] in TcFlatten
    It's still not perfect, as the Note explains

New flag -fconstraint-solver-iterations=n, allows us to control
the number of constraint solver iterations, and in particular
will flag up when it's more than a small number.

Performance is generally slightly better:
T5837 is a lot better for some reason.
parent ca39b96e
......@@ -88,7 +88,7 @@ module BasicTypes(
SourceText,
IntWithInf, infinity, treatZeroAsInf, mkIntWithInf
IntWithInf, infinity, treatZeroAsInf, mkIntWithInf, intGtLimit
) where
import FastString
......@@ -1165,6 +1165,10 @@ instance Num IntWithInf where
(-) = panic "subtracting IntWithInfs"
intGtLimit :: Int -> IntWithInf -> Bool
intGtLimit _ Infinity = False
intGtLimit n (Int m) = n > m
-- | Add two 'IntWithInf's
plusWithInf :: IntWithInf -> IntWithInf -> IntWithInf
plusWithInf Infinity _ = Infinity
......
......@@ -25,6 +25,11 @@ mAX_CTUPLE_SIZE = 16 -- Should match the number of decls in GHC.Classes
mAX_REDUCTION_DEPTH :: Int
mAX_REDUCTION_DEPTH = 200
-- | Default maximum constraint-solver iterations
-- Typically there should be very few
mAX_SOLVER_ITERATIONS :: Int
mAX_SOLVER_ITERATIONS = 4
wORD64_SIZE :: Int
wORD64_SIZE = 8
......
......@@ -691,6 +691,8 @@ data DynFlags = DynFlags {
mainModIs :: Module,
mainFunIs :: Maybe String,
reductionDepth :: IntWithInf, -- ^ Typechecker maximum stack depth
solverIterations :: IntWithInf, -- ^ Number of iterations in the constraints solver
-- Typically only 1 is needed
thisPackage :: PackageKey, -- ^ name of package currently being compiled
......@@ -1440,6 +1442,7 @@ defaultDynFlags mySettings =
mainModIs = mAIN,
mainFunIs = Nothing,
reductionDepth = treatZeroAsInf mAX_REDUCTION_DEPTH,
solverIterations = treatZeroAsInf mAX_SOLVER_ITERATIONS,
thisPackage = mainPackageKey,
......@@ -2593,6 +2596,8 @@ dynamic_flags = [
(sepArg (\s d -> d{ ruleCheck = Just s }))
, defFlag "freduction-depth"
(intSuffix (\n d -> d{ reductionDepth = treatZeroAsInf n }))
, defFlag "fconstraint-solver-iterations"
(intSuffix (\n d -> d{ solverIterations = treatZeroAsInf n }))
, defFlag "fcontext-stack"
(intSuffixM (\n d ->
do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
......
......@@ -316,9 +316,6 @@ situation can't happen.
newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
-- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored flavor cls xis
| CtWanted {} <- flavor
= return ()
| CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
= do { let size = sizePred (mkClassPred cls xis)
loc' = case ctLocOrigin loc of
......@@ -342,7 +339,7 @@ newSCWorkFromFlavored flavor cls xis
impr_theta = filter isImprovementPred sc_rec_theta
loc = ctEvLoc flavor
; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
; mapM_ (emitNewDerived loc) impr_theta }
; emitNewDeriveds loc impr_theta }
{-
......@@ -623,7 +620,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-> TcS (StopOrContinue Ct)
can_eq_app ev s1 t1 s2 t2
| CtDerived { ctev_loc = loc } <- ev
= do { emitNewDerived loc (mkTcEqPred t1 t2)
= do { emitNewDerivedEq loc (mkTcEqPred t1 t2)
; canEqNC ev NomEq s1 s2 }
| CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
= do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
......@@ -947,9 +944,13 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2
= do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
; stopWith ev "Equal tyvars" }
| incompat_kind = incompat
| isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
| isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
| incompat_kind = incompatibleKind ev xi1 k1 xi2 k2
-- We don't do this any more
-- See Note [Orientation of equalities with fmvs] in TcSMonad
-- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
-- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
| same_kind = if swap_over then do_swap else no_swap
| k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
| otherwise = no_swap -- k2_sub_k1
......@@ -976,12 +977,21 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2
continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
, cc_rhs = xi2, cc_eq_rel = eq_rel })
-- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
{- We don't do this any more
See Note [Orientation of equalities with fmvs] in TcSMonad
-- tv1 is the flatten meta-var
do_fmv swapped tv1 xi1 xi2 co1 co2
| same_kind
= canon_eq swapped tv1 xi1 xi2 co1 co2
| otherwise -- Presumably tv1 `subKind` tv2, which is the wrong way round
= ASSERT2( tyVarKind tv1 `isSubKind` typeKind xi2,
| otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
-- at a kind that has some interesting sub-kind structure.
-- Since the two kinds are not the same, we must have
-- tv1 `subKind` tv2, which is the wrong way round
-- e.g. (fmv::*) ~ (a::OpenKind)
-- So make a new meta-var and use that:
-- fmv ~ (beta::*)
-- (a::OpenKind) ~ (beta::*)
= ASSERT2( k1_sub_k2,
ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
......@@ -991,8 +1001,7 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2
tv_ty xi2)
; emitWorkNC [new_ev]
; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
incompat = incompatibleKind ev xi1 k1 xi2 k2
-}
swap_over
-- If tv1 is touchable, swap only if tv2 is also
......@@ -1050,7 +1059,7 @@ incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible
do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
-- Create a derived kind-equality, and solve it
; emitNewDerived kind_co_loc (mkTcEqPred k1 k2)
; emitNewDerivedEq kind_co_loc (mkTcEqPred k1 k2)
-- Put the not-currently-soluble thing into the inert set
; continueWith (CIrredEvCan { cc_ev = new_ev }) }
......@@ -1279,7 +1288,7 @@ as well as in old_pred; that is important for good error messages.
-}
rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
rewriteEvidence old_ev@(CtDerived {}) new_pred _co
= -- If derived, don't even look at the coercion.
-- This is very important, DO NOT re-order the equations for
-- rewriteEvidence to put the isTcReflCo test first!
......@@ -1287,18 +1296,15 @@ rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
-- was produced by flattening, may contain suspended calls to
-- (ctEvTerm c), which fails for Derived constraints.
-- (Getting this wrong caused Trac #7384.)
do { mb_ev <- newDerived loc new_pred
; case mb_ev of
Just new_ev -> continueWith new_ev
Nothing -> stopWith old_ev "Cached derived" }
continueWith (old_ev { ctev_pred = new_pred })
rewriteEvidence old_ev new_pred co
| isTcReflCo co -- See Note [Rewriting with Refl]
= return (ContinueWith (old_ev { ctev_pred = new_pred }))
= continueWith (old_ev { ctev_pred = new_pred })
rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
; return (ContinueWith new_ev) }
; continueWith new_ev }
where
-- mkEvCast optimises ReflCo
new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
......@@ -1340,23 +1346,20 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap
--
-- It's all a form of rewwriteEvidence, specialised for equalities
rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
| CtDerived {} <- old_ev -- Don't force the evidence for a Derived
= continueWith (old_ev { ctev_pred = new_pred })
| NotSwapped <- swapped
, isTcReflCo lhs_co -- See Note [Rewriting with Refl]
, isTcReflCo rhs_co
= return (ContinueWith (old_ev { ctev_pred = new_pred }))
| CtDerived {} <- old_ev
= do { mb <- newDerived loc' new_pred
; case mb of
Just new_ev -> continueWith new_ev
Nothing -> stopWith old_ev "Cached derived" }
= continueWith (old_ev { ctev_pred = new_pred })
| CtGiven { ctev_evar = old_evar } <- old_ev
= do { let new_tm = EvCoercion (lhs_co
`mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
`mkTcTransCo` mkTcSymCo rhs_co)
; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
; return (ContinueWith new_ev) }
; continueWith new_ev }
| CtWanted { ctev_evar = evar } <- old_ev
= do { new_evar <- newWantedEvVarNC loc' new_pred
......@@ -1366,7 +1369,7 @@ rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
`mkTcTransCo` rhs_co
; setWantedEvBind evar (EvCoercion co)
; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
; return (ContinueWith new_evar) }
; continueWith new_evar }
| otherwise
= panic "rewriteEvidence"
......@@ -1469,7 +1472,7 @@ unify_derived loc role orig_ty1 orig_ty2
Nothing -> bale_out }
go _ _ = bale_out
bale_out = emitNewDerived loc (mkTcEqPredRole role orig_ty1 orig_ty2)
bale_out = emitNewDerivedEq loc (mkTcEqPredRole role orig_ty1 orig_ty2)
maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
maybeSym IsSwapped co = mkTcSymCo co
......
This diff is collapsed.
This diff is collapsed.
......@@ -63,7 +63,7 @@ module TcRnTypes(
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
insolubleImplic, trulyInsoluble,
isDroppableDerivedLoc, insolubleImplic, trulyInsoluble,
Implication(..), ImplicStatus(..), isInsolubleStatus,
SubGoalDepth, initialSubGoalDepth,
......@@ -87,6 +87,8 @@ module TcRnTypes(
getEvBindsTcPluginM_maybe,
CtFlavour(..), ctEvFlavour,
CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
eqCanRewrite, eqCanRewriteFR, canDischarge, canDischargeF,
-- Pretty printing
pprEvVarTheta,
......@@ -1293,17 +1295,18 @@ dropDerivedInsols :: Cts -> Cts
dropDerivedInsols insols = filterBag keep insols
where -- insols can include Given
keep ct
| isDerivedCt ct = keep_orig (ctLocOrigin (ctLoc ct))
| isDerivedCt ct = not (isDroppableDerivedLoc (ctLoc ct))
| otherwise = True
keep_orig :: CtOrigin -> Bool
keep_orig (KindEqOrigin {}) = True
keep_orig (GivenOrigin {}) = True
keep_orig (FunDepOrigin1 {}) = True
keep_orig (FunDepOrigin2 {}) = True
-- keep_orig (FunDepOrigin1 _ loc _ _) = keep_orig (ctLocOrigin loc)
-- keep_orig (FunDepOrigin2 _ orig _ _) = keep_orig orig
keep_orig _ = False
isDroppableDerivedLoc :: CtLoc -> Bool
-- Note [Dropping derived constraints]
isDroppableDerivedLoc loc
= case ctLocOrigin loc of
KindEqOrigin {} -> False
GivenOrigin {} -> False
FunDepOrigin1 {} -> False
FunDepOrigin2 {} -> False
_ -> True
{- Note [Dropping derived constraints]
......@@ -1331,6 +1334,14 @@ But (tiresomely) we do keep *some* Derived insolubles:
- For Wanteds it is arguably better to get a fundep error than
a no-instance error (Trac #9612)
Moreover, we keep *all* derived insolubles under some circumstances:
* They are looked at by simplifyInfer, to decide whether to
generalise. Example: [W] a ~ Int, [W] a ~ Bool
We get [D] Int ~ Bool, and indeed the constraints are insoluble,
and we want simplifyInfer to see that, even though we don't
ultimately want to generate an (inexplicable) error message from
To distinguish these cases we use the CtOrigin.
......@@ -1803,6 +1814,93 @@ ctEvFlavour (CtWanted {}) = Wanted
ctEvFlavour (CtGiven {}) = Given
ctEvFlavour (CtDerived {}) = Derived
-- | Whether or not one 'Ct' can rewrite another is determined by its
-- flavour and its equality relation
type CtFlavourRole = (CtFlavour, EqRel)
-- | Extract the flavour and role from a 'CtEvidence'
ctEvFlavourRole :: CtEvidence -> CtFlavourRole
ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
-- | Extract the flavour and role from a 'Ct'
ctFlavourRole :: Ct -> CtFlavourRole
ctFlavourRole = ctEvFlavourRole . cc_ev
{- Note [eqCanRewrite]
~~~~~~~~~~~~~~~~~~~
(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of
a can-rewrite relation, see Definition [Can-rewrite relation]
With the solver handling Coercible constraints like equality constraints,
the rewrite conditions must take role into account, never allowing
a representational equality to rewrite a nominal one.
Note [Wanteds do not rewrite Wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't allow Wanteds to rewrite Wanteds, because that can give rise
to very confusing type error messages. A good example is Trac #8450.
Here's another
f :: a -> Bool
f x = ( [x,'c'], [x,True] ) `seq` True
Here we get
[W] a ~ Char
[W] a ~ Bool
but we do not want to complain about Bool ~ Char!
Note [Deriveds do rewrite Deriveds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
However we DO allow Deriveds to rewrite Deriveds, because that's how
improvement works; see Note [The improvement story] in TcInteract.
However, for now at least I'm only letting (Derived,NomEq) rewrite
(Derived,NomEq) and not doing anything for ReprEq. If we have
eqCanRewriteFR (Derived, NomEq) (Derived, _) = True
then we lose the property of Note [Can-rewrite relation]
R2. If f1 >= f, and f2 >= f,
then either f1 >= f2 or f2 >= f1
Consider f1 = (Given, ReprEq)
f2 = (Derived, NomEq)
f = (Derived, ReprEq)
I thought maybe we could never get Derived ReprEq constraints, but
we can; straight from the Wanteds during improvment. And from a Derived
ReprEq we could conceivably get a Derived NomEq improvment (by decomposing
a type constructor with Nomninal role), and hence unify.
Note [canRewriteOrSame]
~~~~~~~~~~~~~~~~~~~~~~~
canRewriteOrSame is similar but
* returns True for Wanted/Wanted.
* works for all kinds of constraints, not just CTyEqCans
See the call sites for explanations.
-}
eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
eqCanRewrite ev1 ev2 = ctEvFlavourRole ev1 `eqCanRewriteFR` ctEvFlavourRole ev2
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
-- Very important function!
-- See Note [eqCanRewrite]
-- See Note [Wanteds do not rewrite Wanteds]
-- See Note [Deriveds do rewrite Deriveds]
eqCanRewriteFR (Given, NomEq) (_, _) = True
eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True
eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
eqCanRewriteFR _ _ = False
canDischarge :: CtEvidence -> CtEvidence -> Bool
-- See Note [canRewriteOrSame]
canDischarge ev1 ev2 = ctEvFlavour ev1 `canDischargeF` ctEvFlavour ev2
canDischargeF :: CtFlavour -> CtFlavour -> Bool
canDischargeF Given _ = True
canDischargeF Wanted Wanted = True
canDischargeF Wanted Derived = True
canDischargeF Derived Derived = True
canDischargeF _ _ = False
{-
************************************************************************
* *
......
This diff is collapsed.
......@@ -18,12 +18,11 @@ import Bag
import Class ( classKey )
import Class ( Class )
import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes
, Opt_FlexibleContexts ) )
import ErrUtils ( emptyMessages )
import FastString
import Id ( idType )
, Opt_FlexibleContexts )
, DynFlags( solverIterations ) )
import Inst
import Kind ( isKind, defaultKind_maybe )
import Id ( idType )
import Kind ( isKind, isSubKind, defaultKind_maybe )
import ListSetOps
import Maybes ( isNothing )
import Name
......@@ -45,6 +44,9 @@ import Unify ( tcMatchTy )
import Util
import Var
import VarSet
import BasicTypes ( IntWithInf, intGtLimit )
import ErrUtils ( emptyMessages )
import FastString
import Control.Monad ( unless )
import Data.List ( partition )
......@@ -862,7 +864,8 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
; final_wc <- simpl_loop 0 floated_eqs
; dflags <- getDynFlags
; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
(WC { wc_simple = simples1, wc_impl = implics2
, wc_insol = insols `unionBags` insols1 })
......@@ -873,13 +876,16 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
; return final_wc }
simpl_loop :: Int -> Cts
simpl_loop :: Int -> IntWithInf -> Cts
-> WantedConstraints
-> TcS WantedConstraints
simpl_loop n floated_eqs
simpl_loop n limit floated_eqs
wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
| n > 10
= do { traceTcS "solveWanteds: loop!" (ppr wc); return wc }
| n `intGtLimit` limit
= failTcS (hang (ptext (sLit "solveWanteds: too many iterations")
<+> parens (ptext (sLit "limit =") <+> ppr limit))
2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
, ppr wc ] ))
| no_floated_eqs
= return wc -- Done!
......@@ -888,22 +894,20 @@ simpl_loop n floated_eqs
= do { traceTcS "simpl_loop, iteration" (int n)
-- solveSimples may make progress if either float_eqs hold
; (unifs_happened1, wc1) <- if no_floated_eqs
then return (False, emptyWC)
else reportUnifications $
solveSimpleWanteds (floated_eqs `unionBags` simples)
-- Put floated_eqs first so they get solved first
-- NB: the floated_eqs may include /derived/ equalities
-- arising from fundeps inside an implication
; (unifs1, wc1) <- reportUnifications $
solveSimpleWanteds (floated_eqs `unionBags` simples)
-- Put floated_eqs first so they get solved first
-- NB: the floated_eqs may include /derived/ equalities
-- arising from fundeps inside an implication
; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
-- solveImplications may make progress only if unifs2 holds
; (floated_eqs2, implics2) <- if not unifs_happened1 && isEmptyBag implics1
; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
then return (emptyBag, implics)
else solveNestedImplications (implics `unionBags` implics1)
; simpl_loop (n+1) floated_eqs2
; simpl_loop (n+1) limit floated_eqs2
(WC { wc_simple = simples1, wc_impl = implics2
, wc_insol = insols `unionBags` insols1 }) }
......@@ -970,6 +974,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; (floated_eqs, residual_wanted)
<- floatEqualities skols no_given_eqs residual_wanted
; traceTcS "solveImplication 2" (ppr given_insols $$ ppr residual_wanted)
; let final_wanted = residual_wanted `addInsols` given_insols
; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
......@@ -1565,6 +1570,30 @@ floatEqualities skols no_given_eqs wanteds@(WC { wc_simple = simples })
(float_eqs, remaining_simples) = partitionBag (usefulToFloat is_useful) simples
is_useful pred = tyVarsOfType pred `disjointVarSet` skol_set
usefulToFloat :: (TcPredType -> Bool) -> Ct -> Bool
usefulToFloat is_useful_pred ct -- The constraint is un-flattened and de-canonicalised
= is_meta_var_eq pred && is_useful_pred pred
where
pred = ctPred ct
-- Float out alpha ~ ty, or ty ~ alpha
-- which might be unified outside
-- See Note [Do not float kind-incompatible equalities]
is_meta_var_eq pred
| EqPred NomEq ty1 ty2 <- classifyPredType pred
, let k1 = typeKind ty1
k2 = typeKind ty2
= case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
(Just tv1, _) | isMetaTyVar tv1
, k2 `isSubKind` k1
-> True
(_, Just tv2) | isMetaTyVar tv2
, k1 `isSubKind` k2
-> True
_ -> False
| otherwise
= False
{- Note [Float equalities from under a skolem binding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which of the simple equalities can we float out? Obviously, only
......@@ -1588,6 +1617,13 @@ We had a very complicated rule previously, but this is nice and
simple. (To see the notes, look at this Note in a version of
TcSimplify prior to Oct 2014).
Note [Do not float kind-incompatible equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality.
If we float the equality outwards, we'll get *another* Derived
insoluble equality one level out, so the same error will be reported
twice. So we refrain from floating such equalities.
Note [Skolem escape]
~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
......
......@@ -25,7 +25,7 @@ module TcType (
-- TcLevel
TcLevel(..), topTcLevel, pushTcLevel,
strictlyDeeperThan, sameDepthAs, fskTcLevel,
strictlyDeeperThan, sameDepthAs, fmvTcLevel,
--------------------------------
-- MetaDetails
......@@ -485,15 +485,14 @@ the whole implication disappears but when we pop out again we are left with
uf will get unified *once more* to (F Int).
-}
fskTcLevel :: TcLevel
fskTcLevel = TcLevel 0 -- 0 = Outside the outermost level:
-- flatten skolems
fmvTcLevel :: TcLevel -> TcLevel
fmvTcLevel (TcLevel n) = TcLevel (n-1)
topTcLevel :: TcLevel
topTcLevel = TcLevel 1 -- 1 = outermost level
pushTcLevel :: TcLevel -> TcLevel
pushTcLevel (TcLevel us) = TcLevel (us+1)
pushTcLevel (TcLevel us) = TcLevel (us + 2)
strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
......
......@@ -711,9 +711,19 @@
</row>
</thead>
<tbody>
<row>
<entry><option>-fconstraint-solver-iterations=</option><replaceable>n</replaceable></entry>
<entry>Set the iteration limit for the type-constraint solver.
The default limit is 4. Typically one iteration
suffices; so please yell if you find you need to set
it higher than the default. Zero means infinity. </entry>
<entry>dynamic</entry>
<entry></entry>
</row>
<row>
<entry><option>-freduction-depth=</option><replaceable>n</replaceable></entry>
<entry>set the <link linkend="undecidable-instances">limit for type simplification</link>. Default is 200.</entry>
<entry>Set the <link linkend="undecidable-instances">limit for type simplification</link>.
Default is 200; zero means infinity.</entry>
<entry>dynamic</entry>
<entry></entry>
</row>
......
T2544.hs:17:12:
Couldn't match type ‘IxMap l’ with ‘IxMap i0’
NB: ‘IxMap’ is a type function, and may not be injective
The type variable ‘i0’ is ambiguous
Expected type: IxMap (l :|: r) [Int]
Actual type: BiApp (IxMap i0) (IxMap i1) [Int]
Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
In the expression: BiApp empty empty
In an equation for ‘empty’: empty = BiApp empty empty
T2544.hs:17:18: error:
Couldn't match type ‘IxMap i0’ with ‘IxMap l’
NB: ‘IxMap’ is a type function, and may not be injective
The type variable ‘i0’ is ambiguous
Expected type: IxMap l [Int]
Actual type: IxMap i0 [Int]
Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
In the first argument of ‘BiApp’, namely ‘empty’
In the expression: BiApp empty empty
T2544.hs:17:24: error:
Couldn't match type ‘IxMap i1’ with ‘IxMap r’
NB: ‘IxMap’ is a type function, and may not be injective
The type variable ‘i1’ is ambiguous
Expected type: IxMap r [Int]
Actual type: IxMap i1 [Int]
Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
In the second argument of ‘BiApp’, namely ‘empty’
In the expression: BiApp empty empty
T2627b.hs:20:24:
Occurs check: cannot construct the infinite type:
b0 ~ Dual (Dual b0)
The type variable ‘b0’ is ambiguous
In the expression: conn undefined undefined