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.

3 files changed, 46 insertions, 7 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index bab53e323b..6459136973 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/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@.
+-- | 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
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 6e10eae9e2..60718db082 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/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
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 8bab8462be..7474630c83 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/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