[Git][ghc/ghc][wip/T18855] Fix two constraint solving problems
Simon Peyton Jones
gitlab at gitlab.haskell.org
Tue Oct 20 10:37:29 UTC 2020
Simon Peyton Jones pushed to branch wip/T18855 at Glasgow Haskell Compiler / GHC
Commits:
53beedaf by Simon Peyton Jones at 2020-10-20T11:36:10+01:00
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
- - - - -
9 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- + testsuite/tests/polykinds/T18855.hs
- testsuite/tests/polykinds/all.T
- testsuite/tests/typecheck/should_fail/T10709b.stderr
- testsuite/tests/typecheck/should_fail/T12589.stderr
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -42,7 +42,8 @@ module GHC.Core.Coercion (
mkAxiomInstCo, mkProofIrrelCo,
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
- mkKindCo, castCoercionKind, castCoercionKindI,
+ mkKindCo,
+ castCoercionKind, castCoercionKind1, castCoercionKind2,
mkFamilyTyConAppCo,
mkHeteroCoercionType,
@@ -1513,24 +1514,47 @@ instCoercions g ws
; return (piResultTy <$> g_tys <*> w_tys, g') }
-- | Creates a new coercion with both of its types casted by different casts
--- @castCoercionKind g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
+-- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
-- has type @(t1 |> h1) ~r (t2 |> h2)@.
-- @h1@ and @h2@ must be nominal.
-castCoercionKind :: Coercion -> Role -> Type -> Type
+castCoercionKind2 :: Coercion -> Role -> Type -> Type
-> CoercionN -> CoercionN -> Coercion
-castCoercionKind g r t1 t2 h1 h2
+castCoercionKind2 g r t1 t2 h1 h2
= mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
+-- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@
+-- That is, it's a specialised form of castCoercionKind, where the two
+-- kind coercions are identical
+-- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,
+-- has type @(t1 |> h) ~r (t2 |> h)@.
+-- @h@ must be nominal.
+-- See Note [castCoercionKind1]
+castCoercionKind1 :: Coercion -> Role -> Type -> Type
+ -> CoercionN -> Coercion
+castCoercionKind1 g r t1 t2 h
+ = case g of
+ Refl t -> refl_shortcut t
+ GRefl _ t MRefl -> refl_shortcut t
+ GRefl _ _ (MCo kind_co)
+ -> GRefl r (mkCastTy t1 h)
+ (MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h))
+ _ -> castCoercionKind2 g r t1 t2 h h
+ where
+ refl_shortcut t = ASSERT2 (t1 `eqType` t2 && t1 `eqType` t
+ , ppr t $$ ppr t1 $$ ppr t2 )
+ mkReflCo r (mkCastTy t1 h)
+
-- | Creates a new coercion with both of its types casted by different casts
-- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
-- has type @(t1 |> h1) ~r (t2 |> h2)@.
-- @h1@ and @h2@ must be nominal.
-- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
--- Use @castCoercionKind@ instead if @t1@, @t2@, and @r@ are known beforehand.
-castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion
-castCoercionKindI g h1 h2
- = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
- where (Pair t1 t2, r) = coercionKindRole g
+-- Use @castCoercionKind2@ instead if @t1@, @t2@, and @r@ are known beforehand.
+castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
+castCoercionKind g h1 h2
+ = castCoercionKind2 g r t1 t2 h1 h2
+ where
+ (Pair t1 t2, r) = coercionKindRole g
mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
-- ^ Given a family instance 'TyCon' and its arg 'Coercion's, return the
@@ -1592,6 +1616,23 @@ mkCoCast c g
(tc, _) = splitTyConApp (coercionLKind g)
co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
+{- Note [castCoercionKind1]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+castCoercionKind1 deals with the very important special case of castCoercionKind2
+where the two kind coercions are identical. In that case we can exploit the
+situation where the main coercion is reflexive, via the special cases for Refl
+and GRefl.
+
+This is important when flattening (ty |> co). We flatten ty, yielding
+ fco :: ty ~ ty'
+and now we want a coercion xco between
+ xco :: (ty |> co) ~ (ty' |> co)
+That's exactly what castCoercionKind1 does. And it's very very common for
+fco to be Refl. In that case we do NOT want to get some terrible composition
+of mkLeftCoherenceCo and mkRightCoherenceCo, which is what castCoercionKind2
+has to do in its full generality. See #18413.
+-}
+
{-
%************************************************************************
%* *
@@ -1967,8 +2008,8 @@ ty_co_subst !lc role ty
else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
go r ty@(LitTy {}) = ASSERT( r == Nominal )
mkNomReflCo ty
- go r (CastTy ty co) = castCoercionKindI (go r ty) (substLeftCo lc co)
- (substRightCo lc co)
+ go r (CastTy ty co) = castCoercionKind (go r ty) (substLeftCo lc co)
+ (substRightCo lc co)
go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co)
(substRightCo lc co)
where kco = go Nominal (coercionType co)
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -1447,7 +1447,7 @@ normalise_type ty
= do { (nco, nty) <- go ty
; lc <- getLC
; let co' = substRightCo lc co
- ; return (castCoercionKind nco Nominal ty nty co co'
+ ; return (castCoercionKind2 nco Nominal ty nty co co'
, mkCastTy nty co') }
go (CoercionTy co)
= do { lc <- getLC
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1454,7 +1454,7 @@ ty_co_match menv subst (TyVarTy tv1) co lkco rkco
= if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
then Nothing -- occurs check failed
else Just $ extendVarEnv subst tv1' $
- castCoercionKindI co (mkSymCo lkco) (mkSymCo rkco)
+ castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
| otherwise
= Nothing
=====================================
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
=====================================
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
=====================================
testsuite/tests/polykinds/T18855.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+module Bug where
+
+import Data.Kind
+
+type family Apply (f :: a -> b) (x :: a) :: b
+
+type F :: forall a.
+ forall (p :: forall bOne. Either a bOne -> Type)
+ -> forall bTwo.
+ forall (e :: Either a bTwo)
+ -> Apply p e
+
+type family F
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -225,3 +225,4 @@ test('T18451', normal, compile_fail, [''])
test('T18451a', normal, compile_fail, [''])
test('T18451b', normal, compile_fail, [''])
test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
+test('T18855', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T10709b.stderr
=====================================
@@ -11,44 +11,44 @@ T10709b.hs:6:22: error:
x4 = (replicateM 2 . mask) (\ _ -> return ())
T10709b.hs:7:22: error:
- • Couldn't match type ‘t0’ with ‘forall a. IO a -> IO a’
+ • Couldn't match type ‘t0’ with ‘forall a1. IO a1 -> IO a1’
Expected: (t0 -> IO a) -> IO a
Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
Cannot instantiate unification variable ‘t0’
- with a type involving polytypes: forall a. IO a -> IO a
+ with a type involving polytypes: forall a1. IO a1 -> IO a1
• In the second argument of ‘(.)’, namely ‘mask’
In the expression: (replicateM 2 . mask) (\ x -> undefined x)
In an equation for ‘x5’:
x5 = (replicateM 2 . mask) (\ x -> undefined x)
T10709b.hs:8:22: error:
- • Couldn't match type ‘p0’ with ‘forall a. IO a -> IO a’
+ • Couldn't match type ‘p0’ with ‘forall a1. IO a1 -> IO a1’
Expected: (p0 -> IO a) -> IO a
Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
Cannot instantiate unification variable ‘p0’
- with a type involving polytypes: forall a. IO a -> IO a
+ with a type involving polytypes: forall a1. IO a1 -> IO a1
• In the second argument of ‘(.)’, namely ‘mask’
In the expression: (replicateM 2 . mask) (id (\ _ -> undefined))
In an equation for ‘x6’:
x6 = (replicateM 2 . mask) (id (\ _ -> undefined))
T10709b.hs:9:22: error:
- • Couldn't match type ‘b0’ with ‘forall a. IO a -> IO a’
+ • Couldn't match type ‘b0’ with ‘forall a1. IO a1 -> IO a1’
Expected: (b0 -> IO a) -> IO a
Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
Cannot instantiate unification variable ‘b0’
- with a type involving polytypes: forall a. IO a -> IO a
+ with a type involving polytypes: forall a1. IO a1 -> IO a1
• In the second argument of ‘(.)’, namely ‘mask’
In the expression: (replicateM 2 . mask) (const undefined)
In an equation for ‘x7’:
x7 = (replicateM 2 . mask) (const undefined)
T10709b.hs:10:22: error:
- • Couldn't match type ‘a0’ with ‘forall a. IO a -> IO a’
+ • Couldn't match type ‘a0’ with ‘forall a1. IO a1 -> IO a1’
Expected: (a0 -> IO a) -> IO a
Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
Cannot instantiate unification variable ‘a0’
- with a type involving polytypes: forall a. IO a -> IO a
+ with a type involving polytypes: forall a1. IO a1 -> IO a1
• In the second argument of ‘(.)’, namely ‘mask’
In the expression:
(replicateM 2 . mask) ((\ x -> undefined x) :: a -> b)
=====================================
testsuite/tests/typecheck/should_fail/T12589.stderr
=====================================
@@ -1,12 +1,2 @@
T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t
-
-T12589.hs:13:5: error:
- • Couldn't match expected type ‘t1’
- with actual type ‘(forall a. Bounded a => f0 a) -> h0 f0 xs0’
- Cannot instantiate unification variable ‘t1’
- with a type involving polytypes:
- (forall a. Bounded a => f0 a) -> h0 f0 xs0
- • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
- In the expression: minBound & hcpure (Proxy @Bounded)
- In an equation for ‘a’: a = minBound & hcpure (Proxy @Bounded)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/53beedaf2bdd9b9cd3d396b6fe8b92a0e7f69ca2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/53beedaf2bdd9b9cd3d396b6fe8b92a0e7f69ca2
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201020/f78411d0/attachment-0001.html>
More information about the ghc-commits
mailing list