diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-10-19 16:52:47 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-10-27 14:02:34 -0400 |
commit | 0b3d23afcad8bc14f2ba69b8dbe05c314e6e7b29 (patch) | |
tree | 1851c76146d7de2e96d367213ec1cb7d2e134aaa /compiler/GHC/Tc/Solver.hs | |
parent | f3d8ab2ef6ffe30ec91c795e0223392dd96ea61a (diff) | |
download | haskell-0b3d23afcad8bc14f2ba69b8dbe05c314e6e7b29.tar.gz |
Fix two constraint solving problems
This patch fixes two problems in the constraint solver.
* An actual bug #18555: we were floating out a constraint to eagerly,
and that was ultimately fatal. It's explained in
Note [Do not float blocked constraints] in GHC.Core.Constraint.
This is all very delicate, but it's all going to become irrelevant
when we stop floating constraints (#17656).
* A major performance infelicity in the flattener. When flattening
(ty |> co) we *never* generated Refl, even when there was nothing
at all to do. Result: we would gratuitously rewrite the constraint
to exactly the same thing, wasting work. Described in #18413, and
came up again in #18855.
Solution: exploit the special case by calling the new function
castCoercionKind1. See Note [castCoercionKind1] in
GHC.Core.Coercion
Diffstat (limited to 'compiler/GHC/Tc/Solver.hs')
-rw-r--r-- | compiler/GHC/Tc/Solver.hs | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index ab1e6d56d3..7f4bcdf871 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -2542,6 +2542,9 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs is_float_eq_candidate ct | pred <- ctPred ct , EqPred NomEq ty1 ty2 <- classifyPredType pred + , case ct of + CIrredCan {} -> False -- See Note [Do not float blocked constraints] + _ -> True -- See #18855 = float_eq ty1 ty2 || float_eq ty2 ty1 | otherwise = False @@ -2552,7 +2555,26 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs && (not (isTyVarTyVar tv1) || isTyVarTy ty2) Nothing -> False -{- Note [Float equalities from under a skolem binding] +{- Note [Do not float blocked constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As #18855 showed, we must not float an equality that is blocked. +Consider + forall a[4]. [W] co1: alpha[4] ~ Maybe (a[4] |> bco) + [W] co2: alpha[4] ~ Maybe (beta[4] |> bco]) + [W] bco: kappa[2] ~ Type + +Now co1, co2 are blocked by bco. We will eventually float out bco +and solve it at level 2. But the danger is that we will *also* +float out co2, and that is bad bad bad. Because we'll promote alpha +and beta to level 2, and then fail to unify the promoted beta +with the skolem a[4]. + +Solution: don't float out blocked equalities. Remember: we only want +to float out if we can solve; see Note [Which equalities to float]. + +(Future plan: kill floating altogether.) + +Note [Float equalities from under a skolem binding] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Which of the simple equalities can we float out? Obviously, only ones that don't mention the skolem-bound variables. But that is |