[Git][ghc/ghc][master] Linear types: fix roles in GADTs (#18799)

[Marge Bot]

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


Commits:
32dc7698 by Krzysztof Gogolewski at 2020-10-09T08:48:15-04:00
Linear types: fix roles in GADTs (#18799)

- - - - -


4 changed files:

- compiler/GHC/Tc/TyCl/Utils.hs
- + testsuite/tests/linear/should_fail/LinearRole.hs
- + testsuite/tests/linear/should_fail/LinearRole.stderr
- testsuite/tests/linear/should_fail/all.T


Changes:

=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -580,8 +580,8 @@ irDataCon :: DataCon -> RoleM ()
 irDataCon datacon
   = setRoleInferenceVars univ_tvs $
     irExTyVars ex_tvs $ \ ex_var_set ->
-    mapM_ (irType ex_var_set)
-          (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys))
+      do mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ map scaledThing arg_tys)
+         mapM_ (markNominal ex_var_set) (map tyVarKind ex_tvs ++ map scaledMult arg_tys)  -- Field multiplicities are nominal (#18799)
       -- See Note [Role-checking data constructor arguments]
   where
     (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)


=====================================
testsuite/tests/linear/should_fail/LinearRole.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE LinearTypes, GADTs, DataKinds #-}
+
+module LinearRole where -- #18799
+
+import GHC.Types (Multiplicity(..))
+import Data.Coerce
+
+data T m a where
+  MkT :: a %m -> T m a
+
+f :: T 'One a -> T 'Many a
+f x = coerce x


=====================================
testsuite/tests/linear/should_fail/LinearRole.stderr
=====================================
@@ -0,0 +1,6 @@
+
+LinearRole.hs:12:7: error:
+    • Couldn't match type ‘'One’ with ‘'Many’
+        arising from a use of ‘coerce’
+    • In the expression: coerce x
+      In an equation for ‘f’: f x = coerce x


=====================================
testsuite/tests/linear/should_fail/all.T
=====================================
@@ -17,6 +17,7 @@ test('LinearSeq', normal, compile_fail, [''])
 test('LinearViewPattern', normal, compile_fail, [''])
 test('LinearConfusedDollar', normal, compile_fail, [''])
 test('LinearPatSyn', normal, compile_fail, [''])
+test('LinearRole', normal, compile_fail, [''])
 test('LinearGADTNewtype', normal, compile_fail, [''])
 test('LinearPartialSig', normal, compile_fail, [''])
 test('LinearKind', normal, compile_fail, [''])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/32dc7698a0c38afe2889119a2df0f2a2b8debe0a
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/20201009/ed79b41a/attachment-0001.html>