diff options
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 24 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Flatten.hs | 6 |
2 files changed, 27 insertions, 3 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 diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs index dd214ceb7c..48b9c55588 100644 --- a/compiler/GHC/Tc/Solver/Flatten.hs +++ b/compiler/GHC/Tc/Solver/Flatten.hs @@ -1206,9 +1206,11 @@ flatten_one ty@(ForAllTy {}) flatten_one (CastTy ty g) = do { (xi, co) <- flatten_one ty ; (g', _) <- flatten_co g - ; role <- getRole - ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) } + ; return (mkCastTy xi g', castCoercionKind1 co role xi ty g') } + -- It makes a /big/ difference to call castCoercionKind1 not + -- the more general castCoercionKind2. + -- See Note [castCoercionKind1] in GHC.Core.Coercion flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co |