Linear types: fix roles in GADTs (#18799)

3 files changed, 19 insertions, 0 deletions

diff --git a/testsuite/tests/linear/should_fail/LinearRole.hs b/testsuite/tests/linear/should_fail/LinearRole.hs
new file mode 100644
index 0000000000..403935f4ce
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/linear/should_fail/LinearRole.stderr b/testsuite/tests/linear/should_fail/LinearRole.stderr
new file mode 100644
index 0000000000..6d499c4d70
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T
index 5fa6fdb18f..95cb337711 100644
--- a/testsuite/tests/linear/should_fail/all.T
+++ b/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, [''])