[Git][ghc/ghc][wip/T18855] Fix two constraint solving problems

Simon Peyton Jones gitlab at gitlab.haskell.org
Tue Oct 20 11:44:38 UTC 2020



Simon Peyton Jones pushed to branch wip/T18855 at Glasgow Haskell Compiler / GHC


Commits:
c3854ecf by Simon Peyton Jones at 2020-10-20T12:43:52+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,45 @@ 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 = 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 +1614,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 +2006,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/c3854ecf284de79304018c75cbdf986bd5486342

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c3854ecf284de79304018c75cbdf986bd5486342
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/54ec10a6/attachment-0001.html>


More information about the ghc-commits mailing list