[Git][ghc/ghc][master] Account for TYPE vs CONSTRAINT in mkSelCo

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
bb500e2a by Simon Peyton Jones at 2023-02-28T18:55:35-05:00
Account for TYPE vs CONSTRAINT in mkSelCo

As #23018 showed, in mkRuntimeRepCo we need to account for coercions
between TYPE and COERCION.

See Note [mkRuntimeRepCo] in GHC.Core.Coercion.

- - - - -


5 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Type.hs
- + testsuite/tests/typecheck/should_compile/T23018.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -612,14 +612,40 @@ eqTyConRole tc
   | otherwise
   = pprPanic "eqTyConRole: unknown tycon" (ppr tc)
 
--- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
---   (or CONSTRAINT instead of TYPE)
--- produce a coercion @rep_co :: r1 ~ r2 at .
+-- | Given a coercion `co :: (t1 :: TYPE r1) ~ (t2 :: TYPE r2)`
+-- produce a coercion `rep_co :: r1 ~ r2`
+-- But actually it is possible that
+--     co :: (t1 :: CONSTRAINT r1) ~ (t2 :: CONSTRAINT r2)
+-- or  co :: (t1 :: TYPE r1)       ~ (t2 :: CONSTRAINT r2)
+-- or  co :: (t1 :: CONSTRAINT r1) ~ (t2 :: TYPE r2)
+-- See Note [mkRuntimeRepCo]
 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
 mkRuntimeRepCo co
-  = mkSelCo (SelTyCon 0 Nominal) kind_co
+  = assert (isTYPEorCONSTRAINT k1 && isTYPEorCONSTRAINT k2) $
+    mkSelCo (SelTyCon 0 Nominal) kind_co
   where
     kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
+    Pair k1 k2 = coercionKind kind_co
+
+{- Note [mkRuntimeRepCo]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Given
+   class C a where { op :: Maybe a }
+we will get an axiom
+   axC a :: (C a :: CONSTRAINT r1) ~ (Maybe a :: TYPE r2)
+(See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim.)
+
+Then we may call mkRuntimeRepCo on (axC ty), and that will return
+   mkSelCo (SelTyCon 0 Nominal) (Kind (axC ty)) :: r1 ~ r2
+
+So mkSelCo needs to be happy with decomposing a coercion of kind
+   CONSTRAINT r1 ~ TYPE r2
+
+Hence the use of `tyConIsTYPEorCONSTRAINT` in the assertion `good_call`
+in `mkSelCo`. See #23018 for a concrete example.  (In this context it's
+important that TYPE and CONSTRAINT have the same arity and kind, not
+merely that they are not-apart; otherwise SelCo would not make sense.)
+-}
 
 isReflCoVar_maybe :: Var -> Maybe Coercion
 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
@@ -1173,7 +1199,8 @@ mkSelCo_maybe cs co
        , Just (tc2, tys2) <- splitTyConApp_maybe ty2
        , let { len1 = length tys1
              ; len2 = length tys2 }
-       =  tc1 == tc2
+       =  (tc1 == tc2 || (tyConIsTYPEorCONSTRAINT tc1 && tyConIsTYPEorCONSTRAINT tc2))
+                      -- tyConIsTYPEorCONSTRAINT: see Note [mkRuntimeRepCo]
        && len1 == len2
        && n < len1
        && r == tyConRole (coercionRole co) tc1 n


=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -44,6 +44,13 @@ import Control.Monad   ( zipWithM )
 %*                                                                      *
 %************************************************************************
 
+This module does coercion optimisation.  See the paper
+
+   Evidence normalization in Systtem FV (RTA'13)
+   https://simon.peytonjones.org/evidence-normalization/
+
+The paper is also in the GHC repo, in docs/opt-coercion.
+
 Note [Optimising coercion optimisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Looking up a coercion's role or kind is linear in the size of the


=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -124,7 +124,7 @@ module GHC.Core.Type (
 
         -- *** Levity and boxity
         sORTKind_maybe, typeTypeOrConstraint,
-        typeLevity_maybe,
+        typeLevity_maybe, tyConIsTYPEorCONSTRAINT,
         isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
         isLiftedRuntimeRep, isUnliftedRuntimeRep, runtimeRepLevity_maybe,
         isBoxedRuntimeRep,
@@ -2652,13 +2652,18 @@ isPredTy ty = case typeTypeOrConstraint ty of
                   TypeLike       -> False
                   ConstraintLike -> True
 
------------------------------------------
 -- | Does this classify a type allowed to have values? Responds True to things
 -- like *, TYPE Lifted, TYPE IntRep, TYPE v, Constraint.
 isTYPEorCONSTRAINT :: Kind -> Bool
 -- ^ True of a kind `TYPE _` or `CONSTRAINT _`
 isTYPEorCONSTRAINT k = isJust (sORTKind_maybe k)
 
+tyConIsTYPEorCONSTRAINT :: TyCon -> Bool
+tyConIsTYPEorCONSTRAINT tc
+  = tc_uniq == tYPETyConKey || tc_uniq == cONSTRAINTTyConKey
+  where
+    !tc_uniq = tyConUnique tc
+
 isConstraintLikeKind :: Kind -> Bool
 -- True of (CONSTRAINT _)
 isConstraintLikeKind kind


=====================================
testsuite/tests/typecheck/should_compile/T23018.hs
=====================================
@@ -0,0 +1,9 @@
+module T23018 where
+
+import qualified Control.DeepSeq as DeepSeq
+
+class XX f where
+   rnf :: DeepSeq.NFData a => f a -> ()
+
+instance XX Maybe where
+   rnf = DeepSeq.rnf


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -863,3 +863,4 @@ test('T22912', normal, compile, [''])
 test('T22924', normal, compile, [''])
 test('T22985a', normal, compile, ['-O'])
 test('T22985b', normal, compile, [''])
+test('T23018', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bb500e2a2d039dc75c8bb80d47ea2349b97fbf1b

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bb500e2a2d039dc75c8bb80d47ea2349b97fbf1b
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/20230228/2da029e0/attachment-0001.html>