[Git][ghc/ghc][wip/T23938] Fix wrong role in mkSelCo_maybe

[Krzysztof Gogolewski (@monoidal)]

Krzysztof Gogolewski pushed to branch wip/T23938 at Glasgow Haskell Compiler / GHC


Commits:
0c93b659 by Krzysztof Gogolewski at 2023-09-07T00:09:29+02:00
Fix wrong role in mkSelCo_maybe

In the Lint failure in #23938, we start with a coercion Refl :: T a ~R T a,
and call mkSelCo (SelTyCon 1 nominal) Refl.
The function incorrectly returned Refl :: a ~R a. The returned role
should be nominal, according to the SelCo rule:

      co : (T s1..sn) ~r0 (T t1..tn)
      r = tyConRole tc r0 i
      ----------------------------------
      SelCo (SelTyCon i r) : si ~r ti

In this test case, r is nominal while r0 is representational.

- - - - -


4 changed files:

- compiler/GHC/Core/Coercion.hs
- + testsuite/tests/simplCore/should_compile/T23938.hs
- + testsuite/tests/simplCore/should_compile/T23938A.hs
- testsuite/tests/simplCore/should_compile/all.T


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1149,8 +1149,12 @@ mkSelCo_maybe cs co
     Pair ty1 ty2 = coercionKind co
 
     go cs co
-      | Just (ty, r) <- isReflCo_maybe co
-      = Just (mkReflCo r (getNthFromType cs ty))
+      | Just (ty, _) <- isReflCo_maybe co
+      = let new_role = coercionRole (SelCo cs co)
+        in Just (mkReflCo new_role (getNthFromType cs ty))
+        -- The role of the result (new_role) does not have to
+        -- be equal to the role of co, per Note [SelCo].
+        -- This was revealed by #23938.
 
     go SelForAll (ForAllCo { fco_kind = kind_co })
       = Just kind_co


=====================================
testsuite/tests/simplCore/should_compile/T23938.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE MagicHash #-}
+module T23938 where
+
+import T23938A
+import Control.Monad.ST
+
+genIndexes :: () -> ST RealWorld (GVector RealWorld (T Int))
+genIndexes = new f


=====================================
testsuite/tests/simplCore/should_compile/T23938A.hs
=====================================
@@ -0,0 +1,60 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+
+module T23938A where
+
+import GHC.Exts
+import GHC.ST
+import Data.Kind
+
+class Monad m => PrimMonad m where
+  type PrimState m
+  primitive :: (State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a
+
+instance PrimMonad (ST s) where
+  type PrimState (ST s) = s
+  primitive = ST
+  {-# INLINE primitive #-}
+
+{-# INLINE stToPrim #-}
+stToPrim (ST m) = primitive m
+
+data family MVector s a
+data instance MVector s Int = MyVector (MutableByteArray# s)
+
+data T (x :: Type)
+
+data family GVector s a
+data instance GVector s (T a) = MV_2 (MVector s a)
+
+new :: (PrimMonad m) => CVector a -> () -> m (GVector (PrimState m) (T a))
+{-# INLINE new #-}
+new e _ = stToPrim (unsafeNew e >>= \v -> ini e v >> return v)
+
+ini :: CVector a -> GVector s (T a) -> ST s ()
+ini e (MV_2 as) = basicInitialize e as
+
+unsafeNew :: (PrimMonad m) => CVector a -> m (GVector (PrimState m) (T a))
+{-# INLINE unsafeNew #-}
+unsafeNew e = stToPrim (basicUnsafeNew e >>= \(!z) -> pure (MV_2 z))
+
+data CVector a = CVector {
+  basicUnsafeNew  :: forall s. ST s (MVector s a),
+  basicInitialize :: forall s. MVector s a -> ST s ()
+}
+
+f :: CVector Int
+f = CVector {
+  basicUnsafeNew = ST (\s -> case newByteArray# 4# s of
+                              (# s', a #) -> (# s', MyVector a #)),
+
+  basicInitialize = \(MyVector dst) ->
+    ST (\s -> case setByteArray# dst 0# 0# 0# s of s' -> (# s', () #))
+}
+{-# INLINE f #-}
+


=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -497,3 +497,4 @@ test('T23567', [extra_files(['T23567A.hs'])], multimod_compile, ['T23567', '-O -
 # The -ddump-simpl of T22404 should have no let-bindings
 test('T22404', [only_ways(['optasm']), check_errmsg(r'let') ], compile, ['-ddump-simpl -dsuppress-uniques'])
 test('T23864', normal, compile, ['-O -dcore-lint -package ghc -Wno-gadt-mono-local-binds'])
+test('T23938', [extra_files(['T23938A.hs'])], multimod_compile, ['T23938', '-O -v0'])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0c93b659c892691e7275a6e655821031633af96c
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/20230906/8d08d58c/attachment-0001.html>