[Git][ghc/ghc][wip/T23362] Fix coercion optimisation for SelCo (#23362)

[Krzysztof Gogolewski (@monoidal)]

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


Commits:
50e82f6f by Krzysztof Gogolewski at 2023-05-11T15:03:04+02:00
Fix coercion optimisation for SelCo (#23362)

setNominalRole_maybe is supposed to output a nominal coercion.
In the SelCo case, it was not updating the stored role to Nominal,
causing #23362.

- - - - -


3 changed files:

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


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1355,7 +1355,7 @@ mkProofIrrelCo r kco        g1 g2 = mkUnivCo (ProofIrrelProv kco) r
 -- | Converts a coercion to be nominal, if possible.
 -- See Note [Role twiddling functions]
 setNominalRole_maybe :: Role -- of input coercion
-                     -> Coercion -> Maybe Coercion
+                     -> Coercion -> Maybe CoercionN
 setNominalRole_maybe r co
   | r == Nominal = Just co
   | otherwise = setNominalRole_maybe_helper co
@@ -1380,10 +1380,19 @@ setNominalRole_maybe r co
       = AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
     setNominalRole_maybe_helper (ForAllCo tv kind_co co)
       = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
-    setNominalRole_maybe_helper (SelCo n co)
+    setNominalRole_maybe_helper (SelCo cs co) =
       -- NB, this case recurses via setNominalRole_maybe, not
       -- setNominalRole_maybe_helper!
-      = SelCo n <$> setNominalRole_maybe (coercionRole co) co
+      case cs of
+        SelTyCon n _r ->
+          -- Remember to update the role in SelTyCon to nominal;
+          -- not doing this caused #23362.
+          -- See the typing rule in Note [SelCo] in GHC.Core.TyCo.Rep.
+          SelCo (SelTyCon n Nominal) <$> setNominalRole_maybe (coercionRole co) co
+        SelFun fs ->
+          SelCo (SelFun fs) <$> setNominalRole_maybe (coercionRole co) co
+        SelForAll ->
+          pprPanic "setNominalRole_maybe: the coercion should already be nominal" (ppr co)
     setNominalRole_maybe_helper (InstCo co arg)
       = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
     setNominalRole_maybe_helper (UnivCo prov _ co1 co2)


=====================================
testsuite/tests/simplCore/should_compile/T23362.hs
=====================================
@@ -0,0 +1,21 @@
+module T23362 where
+
+import Unsafe.Coerce
+import Data.Kind
+
+type Phantom :: Type -> Type
+data Phantom a = MkPhantom
+
+newtype Id a = MkId a
+newtype First a = MkFirst (Id a)
+data Second a = MkSecond (First a)
+data Third a = MkThird !(Second a)
+
+a :: Second (Phantom Int)
+a = MkSecond (MkFirst (MkId MkPhantom))
+
+uc :: Second (Phantom Int) -> Second (Phantom Bool)
+uc = unsafeCoerce
+
+b :: Third (Phantom Bool)
+b = MkThird (uc a)


=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -477,3 +477,4 @@ test('T23012', normal, compile, ['-O'])
 test('RewriteHigherOrderPatterns', normal, compile, ['-O -ddump-rule-rewrites -dsuppress-all -dsuppress-uniques'])
 test('T23024', normal, multimod_compile, ['T23024', '-O -v0'])
 test('T23026', normal, compile, ['-O'])
+test('T23362', normal, compile, ['-O'])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/50e82f6fe83f2eca5e095b78393c7e50a11bdbf5
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/20230511/6bcc94e0/attachment-0001.html>