Linear types: fix roles in GADTs (#18799)

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

+{-# 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

+
+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, [''])