Introduce Concrete# for representation polymorphism checks

PHASE 1: we never rewrite Concrete# evidence.

This patch migrates all the representation polymorphism checks to
the typechecker, using a new constraint form

  Concrete# :: forall k. k -> TupleRep '[]

Whenever a type `ty` must be representation-polymorphic
(e.g. it is the type of an argument to a function), we emit a new
`Concrete# ty` Wanted constraint. If this constraint goes
unsolved, we report a representation-polymorphism error to the user.
The 'FRROrigin' datatype keeps track of the context of the
representation-polymorphism check, for more informative error messages.

This paves the way for further improvements, such as
allowing type families in RuntimeReps and improving the soundness
of typed Template Haskell. This is left as future work (PHASE 2).

fixes #17907 #20277 #20330 #20423 #20426

updates haddock submodule

-------------------------
Metric Decrease:
    T5642
-------------------------

141 files changed, 2340 insertions, 0 deletions

diff --git a/testsuite/tests/rep-poly/LevPolyLet.hs b/testsuite/tests/rep-poly/LevPolyLet.hs
new file mode 100644
index 0000000000..fc8db1657b
--- /dev/null
+++ b/testsuite/tests/rep-poly/LevPolyLet.hs
@@ -0,0 +1,18 @@
+{-# language DataKinds #-}
+{-# language KindSignatures #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+
+module LevPolyLet
+  ( example
+  ) where
+
+import GHC.Exts
+
+-- This should be rejected because of the let binding.
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)).
+     (Int -> a)
+  -> Bool
+example f =
+  let x = f 42
+   in undefined
diff --git a/testsuite/tests/rep-poly/LevPolyLet.stderr b/testsuite/tests/rep-poly/LevPolyLet.stderr
new file mode 100644
index 0000000000..24456e99a8
--- /dev/null
+++ b/testsuite/tests/rep-poly/LevPolyLet.stderr
@@ -0,0 +1,6 @@
+
+LevPolyLet.hs:17:7: error:
+    • The binder ‘x’ does not have a fixed runtime representation:
+        a :: TYPE ('BoxedRep v)
+    • In the expression: let x = f 42 in undefined
+      In an equation for ‘example’: example f = let x = f 42 in undefined
diff --git a/testsuite/tests/rep-poly/PandocArrowCmd.hs b/testsuite/tests/rep-poly/PandocArrowCmd.hs
new file mode 100644
index 0000000000..3b868c3d17
--- /dev/null
+++ b/testsuite/tests/rep-poly/PandocArrowCmd.hs
@@ -0,0 +1,49 @@
+
+{-
+
+this test file was extracted from Text.Pandoc.Readers.Odt.ContentReader,
+which caused a panic in GHC.Tc.Class.Instance.hasFixedRuntimeRep:
+
+error: panic! (the 'impossible' happened)
+
+  hasFixedRuntimeRep: not of form 'TYPE rep'
+  ty = c_anCXp[tau:0]
+  ki = k_anCXl[tau:0]
+  frrOrig = The arrow command `returnA -< anchorElem_anC3K'
+            does not have a fixed runtime representation.
+
+-}
+
+{-# LANGUAGE Arrows #-}
+{-# OPTIONS_GHC -Wno-missing-methods #-}
+
+module PandocArrowCmd where
+
+import Control.Arrow
+import Control.Category
+
+maybeAddAnchorFrom :: OdtReader i p
+                   -> OdtReaderSafe i i
+maybeAddAnchorFrom anchorReader =
+  keepingTheValue_etc_etc
+  >>>
+  proc (inlines, fAnchorElem) -> do
+  case fAnchorElem of
+    Right anchorElem -> returnA -< anchorElem
+    Left _           -> returnA -< inlines
+
+-----
+
+keepingTheValue_etc_etc :: OdtReader i (b, Either a b)
+keepingTheValue_etc_etc = undefined
+
+data OdtState
+type OdtReader      a b = ArrowState OdtState a b
+type OdtReaderSafe  a b = ArrowState OdtState a (Either () b)
+
+newtype ArrowState state a b = ArrowState
+  { runArrowState :: (state, a) -> (state, b) }
+
+instance Category    (ArrowState s) where {}
+instance Arrow       (ArrowState s) where {}
+instance ArrowChoice (ArrowState s) where {}
diff --git a/testsuite/tests/rep-poly/RepPolyApp.hs b/testsuite/tests/rep-poly/RepPolyApp.hs
new file mode 100644
index 0000000000..862e419f36
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyApp.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyApp where
+
+import Data.Kind
+import GHC.Exts
+import Prelude ( undefined )
+
+foo :: forall rep (a :: TYPE rep). ( a -> a ) -> a
+foo f = f ( undefined :: a )
diff --git a/testsuite/tests/rep-poly/RepPolyApp.stderr b/testsuite/tests/rep-poly/RepPolyApp.stderr
new file mode 100644
index 0000000000..ee7e914b02
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyApp.stderr
@@ -0,0 +1,9 @@
+
+RepPolyApp.hs:11:11: error:
+    • The function argument
+        ‘(undefined :: a)’
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the first argument of ‘f’, namely ‘(undefined :: a)’
+      In the expression: f (undefined :: a)
+      In an equation for ‘foo’: foo f = f (undefined :: a)
diff --git a/testsuite/tests/rep-poly/RepPolyArrowCmd.hs b/testsuite/tests/rep-poly/RepPolyArrowCmd.hs
new file mode 100644
index 0000000000..f010c58e7a
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyArrowCmd.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE Arrows #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyArrowCmd where
+
+import Data.Kind
+import GHC.Exts
+import Prelude ( undefined )
+
+first :: forall r (a :: TYPE r) (b :: TYPE r). a -> b
+first = undefined
+
+(>>>) :: forall r (a :: TYPE r) (b :: TYPE r) (c :: TYPE r). a -> b -> c
+(>>>) = undefined
+
+arr :: forall r (a :: TYPE r) (b :: TYPE r). (a -> b) -> (a -> b)
+arr = undefined
+
+returnA :: forall r (a :: TYPE r). a -> a
+returnA = undefined
+
+foo :: forall r (a :: TYPE r). a -> a
+foo = proc x -> returnA -< x
diff --git a/testsuite/tests/rep-poly/RepPolyArrowCmd.stderr b/testsuite/tests/rep-poly/RepPolyArrowCmd.stderr
new file mode 100644
index 0000000000..0541ef43ab
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyArrowCmd.stderr
@@ -0,0 +1,7 @@
+
+RepPolyArrowCmd.hs:26:17: error:
+    • The arrow command ‘returnA -< x’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: proc x -> returnA -< x
+      In an equation for ‘foo’: foo = proc x -> returnA -< x
diff --git a/testsuite/tests/rep-poly/RepPolyArrowFun.hs b/testsuite/tests/rep-poly/RepPolyArrowFun.hs
new file mode 100644
index 0000000000..62ff9f0809
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyArrowFun.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE Arrows #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyArrowFun where
+
+import Data.Kind
+import GHC.Exts
+import Prelude ( undefined )
+
+arr :: forall r (arr :: Type -> Type -> TYPE r) a b. (a -> b) -> arr a b
+arr = undefined
+
+(.) :: forall r (arr :: Type -> Type -> TYPE r) a b c. arr b c -> arr a b -> arr a c
+(.) = undefined
+
+(>>>) :: forall r (arr :: Type -> Type -> TYPE r) a b c. arr a b -> arr b c -> arr a c
+(>>>) = undefined
+
+first :: forall r (arr :: Type -> Type -> TYPE r) a b c d. arr a b -> arr c d
+first = undefined
+
+returnA :: forall r (arr :: Type -> Type -> TYPE r) a. ( () ~ () ) => arr a a
+returnA = undefined
+
+foo :: forall r (arr :: Type -> Type -> TYPE r) a. () -> arr a a
+foo _ = proc x -> undefined -< x
diff --git a/testsuite/tests/rep-poly/RepPolyArrowFun.stderr b/testsuite/tests/rep-poly/RepPolyArrowFun.stderr
new file mode 100644
index 0000000000..f4ce90d51d
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyArrowFun.stderr
@@ -0,0 +1,30 @@
+
+RepPolyArrowFun.hs:29:9: error:
+    • • The return type of the arrow function
+          ‘arr’
+        does not have a fixed runtime representation:
+          arr b c :: TYPE r
+      • The return type of the arrow function
+          ‘(>>>)’
+        does not have a fixed runtime representation:
+          arr a1 c1 :: TYPE r
+      • The return type of the arrow function
+          ‘first’
+        does not have a fixed runtime representation:
+          arr (b1, d) (c2, d) :: TYPE r
+    • When checking that ‘arr’ (needed by a syntactic construct)
+        has the required type: forall b c. (b -> c) -> arr b c
+        arising from a proc expression at RepPolyArrowFun.hs:29:9-32
+      In the expression: proc x -> undefined -< x
+      In an equation for ‘foo’: foo _ = proc x -> undefined -< x
+
+RepPolyArrowFun.hs:29:19: error:
+    • In the first order arrow application of
+        ‘undefined’
+      to
+        ‘x’,
+      the function does not have a fixed runtime representation:
+        arr a a :: TYPE r
+    • In the command: undefined -< x
+      In the expression: proc x -> undefined -< x
+      In an equation for ‘foo’: foo _ = proc x -> undefined -< x
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack1.bkp b/testsuite/tests/rep-poly/RepPolyBackpack1.bkp
new file mode 100644
index 0000000000..1ae2ebf92e
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack1.bkp
@@ -0,0 +1,18 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RoleAnnotations #-}
+
+unit number-unknown where
+  signature NumberUnknown where
+    import GHC.Types
+    import GHC.Exts
+    data Rep (l :: Levity) :: RuntimeRep
+    data Number (l :: Levity) :: TYPE (Rep l)
+    plus :: Number l -> Number l -> Number l
+    multiply :: Number l -> Number l -> Number l
+  module NumberStuff where
+    import NumberUnknown
+    funcA :: Number l -> Number l -> Number l
+    funcA x y = plus x (multiply x y)
+    -- should get a representation polymorphism error: 'Rep l' is not fixed.
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
new file mode 100644
index 0000000000..6c4c9901cd
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
@@ -0,0 +1,44 @@
+[1 of 1] Processing number-unknown
+  [1 of 2] Compiling NumberUnknown[sig] ( number-unknown\NumberUnknown.hsig, nothing )
+  [2 of 2] Compiling NumberStuff      ( number-unknown\NumberStuff.hs, nothing )
+
+RepPolyBackpack1.bkp:17:5: error:
+    The type of the first pattern in the equation for ‘funcA’
+    does not have a fixed runtime representation:
+      Number l :: TYPE (Rep l)
+
+RepPolyBackpack1.bkp:17:22: error:
+    • The function argument
+        ‘x’
+      does not have a fixed runtime representation:
+        Number l :: TYPE (Rep l)
+    • In the first argument of ‘plus’, namely ‘x’
+      In the expression: plus x (multiply x y)
+      In an equation for ‘funcA’: funcA x y = plus x (multiply x y)
+
+RepPolyBackpack1.bkp:17:24: error:
+    • The function argument
+        ‘(multiply x y)’
+      does not have a fixed runtime representation:
+        Number l :: TYPE (Rep l)
+    • In the second argument of ‘plus’, namely ‘(multiply x y)’
+      In the expression: plus x (multiply x y)
+      In an equation for ‘funcA’: funcA x y = plus x (multiply x y)
+
+RepPolyBackpack1.bkp:17:34: error:
+    • The function argument
+        ‘x’
+      does not have a fixed runtime representation:
+        Number l :: TYPE (Rep l)
+    • In the first argument of ‘multiply’, namely ‘x’
+      In the second argument of ‘plus’, namely ‘(multiply x y)’
+      In the expression: plus x (multiply x y)
+
+RepPolyBackpack1.bkp:17:36: error:
+    • The function argument
+        ‘y’
+      does not have a fixed runtime representation:
+        Number l :: TYPE (Rep l)
+    • In the second argument of ‘multiply’, namely ‘y’
+      In the second argument of ‘plus’, namely ‘(multiply x y)’
+      In the expression: plus x (multiply x y)
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack2.bkp b/testsuite/tests/rep-poly/RepPolyBackpack2.bkp
new file mode 100644
index 0000000000..8d032dce75
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack2.bkp
@@ -0,0 +1,146 @@
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+unit prel where
+
+  module UnboxedPrelude where
+    import Data.Kind
+    import GHC.Exts
+    type Num# :: forall (r :: RuntimeRep). TYPE r -> Constraint
+    class Num# a where
+      add# :: a -> a -> a
+      mul# :: a -> a -> a
+    instance Num# Int# where
+      add# = (+#)
+      mul# = (*#)
+
+  module IntRep where
+    import GHC.Exts
+    type Rep :: RuntimeRep
+    type Rep = 'IntRep
+
+  module NilReps where
+    import GHC.Exts
+    type Reps :: [RuntimeRep]
+    type Reps = '[]
+
+
+unit rep where
+
+  dependency prel
+
+  signature Rep where
+    import GHC.Exts
+    data Rep :: RuntimeRep
+
+  module Defs where
+    import GHC.Exts
+    import Rep
+    import UnboxedPrelude
+    foo :: forall (a :: TYPE Rep). Num# a => a -> a -> a
+    foo x y = mul# x ( add# x y )
+    bar :: forall (a :: TYPE Rep) (b :: TYPE Rep). Num# a => (# a, a, b #) -> (# b, a #)
+    bar (# x, y, z #) = (# z, foo x y #)
+
+
+unit reps where
+
+  signature Reps where
+    import GHC.Exts
+    data Reps :: [RuntimeRep]
+
+  module TupleRep where
+    import GHC.Exts
+    import Reps
+    type Rep = 'TupleRep Reps
+
+  module SumRep where
+    import GHC.Exts
+    import Reps
+    type Rep = 'SumRep Reps
+
+
+unit cons where
+
+  signature Head where
+    import GHC.Exts
+    data Rep :: RuntimeRep
+
+  signature Tail where
+    import GHC.Exts
+    data Reps :: [RuntimeRep]
+
+  module ConsRep where
+    import GHC.Exts
+    import qualified Head
+    import qualified Tail
+    type Reps :: [ RuntimeRep ]
+    type Reps = Head.Rep ': Tail.Reps
+
+unit unit0 where
+  dependency prel
+  dependency cons [Head = prel:IntRep, Tail = prel:NilReps] (ConsRep as Reps1.IntRep_)
+  dependency reps [Reps = prel:NilReps] (TupleRep as TupleRep0_ )
+
+  module Reps1.IntRep ( module Reps1.IntRep_ ) where
+    import Reps1.IntRep_
+
+  module TupleRep0 ( module TupleRep0_ ) where
+    import TupleRep0_
+
+unit unit1 where
+
+  dependency unit0
+  dependency cons [Head = unit0:TupleRep0, Tail = unit0:Reps1.IntRep] (ConsRep as Reps2.TupleRep0.IntRep_)
+
+  module Reps2.TupleRep0.IntRep ( module Reps2.TupleRep0.IntRep_ ) where
+    import Reps2.TupleRep0.IntRep_
+
+unit unit2 where
+
+  dependency unit1
+  dependency reps [Reps = unit1:Reps2.TupleRep0.IntRep] (SumRep as Sum2.TupleRep0.IntRep_)
+
+  module Sum2.TupleRep0.IntRep ( module Sum2.TupleRep0.IntRep_ ) where
+    import Sum2.TupleRep0.IntRep_
+
+unit main where
+
+  dependency prel
+  dependency unit2
+  dependency rep  [Rep = unit2:Sum2.TupleRep0.IntRep] (Defs as Defs.Sum2.Tuple0.IntRep)
+
+  module Main where
+    import GHC.Exts
+    import UnboxedPrelude ( Num#(..) )
+    import Defs.Sum2.Tuple0.IntRep ( bar )
+
+    type MaybeInt# = (# (# #) | Int# #)
+
+    showMaybeInt# :: MaybeInt# -> String
+    showMaybeInt# (# _ | #) = "(Nothing# :: MaybeInt#)"
+    showMaybeInt# (# | i #) = "(Just# " <> show (I# i) <> " :: MaybeInt#)"
+
+    instance Num# MaybeInt# where
+
+      add# (# _ | #) _ = (# (# #) | #)
+      add# _ (# _ | #) = (# (# #) | #)
+      add# (# | x #) (# | y #) = (# | add# x y #)
+
+      mul# (# _ | #) _ = (# (# #) | #)
+      mul# _ (# _ | #) = (# (# #) | #)
+      mul# (# | x #) (# | y #) = (# | mul# x y #)
+
+    main :: IO ()
+    main =
+      case bar (# (# | 3# #), (# | 17# #), (# (# #) | #) #) of
+        (# a, b #) -> do
+          putStrLn $ showMaybeInt# a
+          putStrLn $ showMaybeInt# b
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack2.stdout b/testsuite/tests/rep-poly/RepPolyBackpack2.stdout
new file mode 100644
index 0000000000..4faa01fcf5
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack2.stdout
@@ -0,0 +1,2 @@
+(Nothing# :: MaybeInt#)
+(Just# 60 :: MaybeInt#)
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack3.bkp b/testsuite/tests/rep-poly/RepPolyBackpack3.bkp
new file mode 100644
index 0000000000..21f4c8fb14
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack3.bkp
@@ -0,0 +1,20 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE TypeFamilies #-}
+
+unit sig where
+  signature Sig where
+    import GHC.Exts
+    data Rep :: RuntimeRep
+
+unit impl where
+  module Impl where
+    import Data.Kind
+    import GHC.Exts
+    type family T :: RuntimeRep
+    type Rep = T
+
+unit main where
+  dependency sig[Sig=impl:Impl]
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack3.stderr b/testsuite/tests/rep-poly/RepPolyBackpack3.stderr
new file mode 100644
index 0000000000..5b187eb186
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack3.stderr
@@ -0,0 +1,20 @@
+[1 of 3] Processing sig
+  [1 of 1] Compiling Sig[sig]         ( sig\Sig.hsig, nothing )
+[2 of 3] Processing impl
+  Instantiating impl
+  [1 of 1] Compiling Impl             ( impl\Impl.hs, RepPolyBackpack3.out\impl\Impl.o )
+[3 of 3] Processing main
+  Instantiating main
+  [1 of 1] Including sig[Sig=impl:Impl]
+    Instantiating sig[Sig=impl:Impl]
+    [1 of 1] Compiling Sig[sig]         ( sig\Sig.hsig, RepPolyBackpack3.out\sig\sig-Absk5cIXTXe6UYhGMYGber\Sig.o )
+
+RepPolyBackpack3.bkp:17:5: error:
+    • Type constructor ‘Rep’ has conflicting definitions in the module
+      and its hsig file
+      Main module: type Rep :: GHC.Types.RuntimeRep
+                   type Rep = T :: GHC.Types.RuntimeRep
+      Hsig file:  type Rep :: GHC.Types.RuntimeRep
+                  data Rep
+      Illegal type family application in implementation of abstract data.
+    • while checking that impl:Impl implements signature Sig in sig[Sig=impl:Impl]
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack4.bkp b/testsuite/tests/rep-poly/RepPolyBackpack4.bkp
new file mode 100644
index 0000000000..8f151278cb
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack4.bkp
@@ -0,0 +1,40 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+unit number-unknown where
+  signature NumberUnknown where
+    import GHC.Types
+    import GHC.Exts
+    data Rep :: RuntimeRep
+    data Number :: TYPE Rep
+    plus :: Number -> Number -> Number
+  module NumberStuff where
+    import NumberUnknown
+    funcA :: (# Number, Number #) -> (# Number, Number #) -> Number
+    funcA (# x1, x2 #) _ = plus x1 x2
+
+unit number-int where
+  module NumberUnknown where
+    import GHC.Types
+    type Rep = 'BoxedRep 'Lifted
+    type Number = Int
+    plus :: Int -> Int -> Int
+    plus = (+)
+
+unit number-unboxed-int where
+  module NumberUnknown where
+    import GHC.Types
+    import GHC.Prim
+    type Rep = IntRep
+    type Number = Int#
+    plus :: Int# -> Int# -> Int#
+    plus = (+#)
+
+unit main where
+  dependency number-unknown[NumberUnknown=number-unboxed-int:NumberUnknown]
+  module Main where
+    import NumberStuff
+    import GHC.Types
+    main = print (I# (funcA (# 2#, 3# #) (# 4#, 5# #)))
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack4.stdout b/testsuite/tests/rep-poly/RepPolyBackpack4.stdout
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack4.stdout
@@ -0,0 +1 @@
+5
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack5.bkp b/testsuite/tests/rep-poly/RepPolyBackpack5.bkp
new file mode 100644
index 0000000000..691094d7c9
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack5.bkp
@@ -0,0 +1,46 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UnliftedDatatypes #-}
+
+unit number-unknown where
+  signature NumberUnknown where
+    import GHC.Types
+    import GHC.Exts
+    data Rep (l :: Levity) :: RuntimeRep
+    data Number l :: TYPE (Rep l)
+    fromInt :: Int -> Number l
+    internal_toInt :: Number Lifted -> Int
+    -- representation-polymorphism in return position: no problem
+  module SomeNumber where
+    import GHC.Types
+    import NumberUnknown
+    someNumber :: proxy l -> Number l
+    someNumber _ = fromInt 1728
+    toInt :: Number Lifted -> Int
+    toInt = internal_toInt
+
+unit number-int where
+  module NumberUnknown where
+    import GHC.Types
+    type Rep = 'BoxedRep
+
+    type Number :: forall (l :: Levity) -> TYPE (Rep l)
+    data Number l = MkNumber Int
+    type role Number nominal
+
+    fromInt :: Int -> Number l
+    fromInt = MkNumber
+    internal_toInt (MkNumber i) = i
+
+unit main where
+  dependency number-unknown[NumberUnknown=number-int:NumberUnknown]
+  module Main where
+    import SomeNumber
+    import Data.Proxy
+    import GHC.Exts
+    main =
+      case someNumber (Proxy @Lifted) of
+        number -> print (toInt number)
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack5.stdout b/testsuite/tests/rep-poly/RepPolyBackpack5.stdout
new file mode 100644
index 0000000000..54c9fc81b3
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBackpack5.stdout
@@ -0,0 +1 @@
+1728
diff --git a/testsuite/tests/rep-poly/RepPolyBinder.hs b/testsuite/tests/rep-poly/RepPolyBinder.hs
new file mode 100644
index 0000000000..0ddcbb5093
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBinder.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module RepPolyBinder where
+
+import GHC.Exts
+
+myId :: forall rep (x :: TYPE rep). x -> x
+myId = undefined
+
+foo :: forall rep1 (a :: TYPE rep1) rep2 (b :: TYPE rep2). a -> b -> ()
+foo bndr_a pat@(myId -> bndr_b) = ()
diff --git a/testsuite/tests/rep-poly/RepPolyBinder.stderr b/testsuite/tests/rep-poly/RepPolyBinder.stderr
new file mode 100644
index 0000000000..83489470e9
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyBinder.stderr
@@ -0,0 +1,8 @@
+
+RepPolyBinder.hs:11:1: error:
+    • The type of the first pattern in the equation for ‘foo’
+      does not have a fixed runtime representation:
+        a :: TYPE rep1
+    • The type of the second pattern in the equation for ‘foo’
+      does not have a fixed runtime representation:
+        b :: TYPE rep2
diff --git a/testsuite/tests/rep-poly/RepPolyClassMethod.hs b/testsuite/tests/rep-poly/RepPolyClassMethod.hs
new file mode 100644
index 0000000000..1f41c22ce7
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyClassMethod.hs
@@ -0,0 +1,10 @@
+
+{-# LANGUAGE DataKinds, StandaloneKindSignatures #-}
+
+module RepPolyClassMethod where
+
+import GHC.Exts
+
+type C :: forall rep. TYPE rep -> Constraint
+class C a where
+  methC :: a
diff --git a/testsuite/tests/rep-poly/RepPolyClassMethod.stderr b/testsuite/tests/rep-poly/RepPolyClassMethod.stderr
new file mode 100644
index 0000000000..2731c542c1
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyClassMethod.stderr
@@ -0,0 +1,8 @@
+
+RepPolyClassMethod.hs:10:12: error:
+    • Expected a type, but ‘a’ has kind ‘TYPE rep’
+      ‘rep’ is a rigid type variable bound by
+        the class declaration for ‘C’
+        at RepPolyClassMethod.hs:8:18-20
+    • In the type signature: methC :: a
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/rep-poly/RepPolyDeferred.hs b/testsuite/tests/rep-poly/RepPolyDeferred.hs
new file mode 100644
index 0000000000..b0aa59c95a
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDeferred.hs
@@ -0,0 +1,8 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+
+module RepPolyDeferred where
+
+import GHC.Exts
+
+foo :: forall rep (a :: TYPE rep). a -> a
+foo bndr_a = bndr_a
diff --git a/testsuite/tests/rep-poly/RepPolyDeferred.stderr b/testsuite/tests/rep-poly/RepPolyDeferred.stderr
new file mode 100644
index 0000000000..ff8fcc7688
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDeferred.stderr
@@ -0,0 +1,5 @@
+
+RepPolyDeferred.hs:8:1: error:
+    The type of the first pattern in the equation for ‘foo’
+    does not have a fixed runtime representation:
+      a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyDoBind.hs b/testsuite/tests/rep-poly/RepPolyDoBind.hs
new file mode 100644
index 0000000000..0a4354fc43
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoBind.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyDoBind where
+
+import Data.Kind ( Type)
+import GHC.Exts
+import Prelude ( undefined )
+
+(>>=)
+  :: forall
+        rep
+        ( ma :: TYPE rep )
+        ( a  :: Type )
+        ( mb :: TYPE rep )
+        ( mc :: TYPE rep )
+  .  ma -> ( a -> mb ) -> mc
+(>>=) = undefined
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = do
+  a <- undefined
+  return ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoBind.stderr b/testsuite/tests/rep-poly/RepPolyDoBind.stderr
new file mode 100644
index 0000000000..69974a54a7
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoBind.stderr
@@ -0,0 +1,14 @@
+
+RepPolyDoBind.hs:26:3: error:
+    • The first argument to (>>=),
+      arising from the ‘do’ statement,
+      does not have a fixed runtime representation:
+        ma0 :: TYPE rep
+    • In a stmt of a 'do' block: a <- undefined
+      In the expression:
+        do a <- undefined
+           return ()
+      In an equation for ‘foo’:
+          foo _
+            = do a <- undefined
+                 return ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoBody1.hs b/testsuite/tests/rep-poly/RepPolyDoBody1.hs
new file mode 100644
index 0000000000..3d4b1425cd
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoBody1.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyDoBody1 where
+
+import GHC.Exts
+import Prelude ( undefined )
+
+(>>)
+  :: forall
+        rep
+        ( ma :: TYPE rep )
+        ( mb :: TYPE rep )
+        ( mc :: TYPE rep )
+  .  ma -> mb -> mc
+(>>) = undefined
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = do
+  undefined :: ma
+  return ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr
new file mode 100644
index 0000000000..4e33390474
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr
@@ -0,0 +1,18 @@
+
+RepPolyDoBody1.hs:24:3: error:
+    • • The first argument to (>>),
+        arising from the ‘do’ statement,
+        does not have a fixed runtime representation:
+          ma :: TYPE rep
+      • The second argument to (>>),
+        arising from the ‘do’ statement,
+        does not have a fixed runtime representation:
+          mb0 :: TYPE rep
+    • In a stmt of a 'do' block: undefined :: ma
+      In the expression:
+        do undefined :: ma
+         return ()
+      In an equation for ‘foo’:
+          foo _
+            = do undefined :: ma
+               return ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoBody2.hs b/testsuite/tests/rep-poly/RepPolyDoBody2.hs
new file mode 100644
index 0000000000..c65f3441b4
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoBody2.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyDoBody2 where
+
+import GHC.Exts
+import Prelude ( undefined )
+
+(>>)
+  :: forall
+        rep
+        ( mb :: TYPE rep )
+        ( mc :: TYPE rep )
+  .  () -> mb -> mc
+(>>) = undefined
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = do
+  undefined :: ()
+  return ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr
new file mode 100644
index 0000000000..0154f2105e
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr
@@ -0,0 +1,14 @@
+
+RepPolyDoBody2.hs:23:3: error:
+    • The second argument to (>>),
+      arising from the ‘do’ statement,
+      does not have a fixed runtime representation:
+        mb0 :: TYPE rep
+    • In a stmt of a 'do' block: undefined :: ()
+      In the expression:
+        do undefined :: ()
+         return ()
+      In an equation for ‘foo’:
+          foo _
+            = do undefined :: ()
+               return ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoReturn.hs b/testsuite/tests/rep-poly/RepPolyDoReturn.hs
new file mode 100644
index 0000000000..d240c345ad
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyDoReturn.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyDoReturn where
+
+import GHC.Exts
+import Prelude ( undefined )
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = do
+  return ()
diff --git a/testsuite/tests/rep-poly/RepPolyLeftSection1.hs b/testsuite/tests/rep-poly/RepPolyLeftSection1.hs
new file mode 100644
index 0000000000..a0385401ca
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyLeftSection1.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module RepPolyLeftSection1 where
+
+import GHC.Exts
+
+f :: forall a r (b :: TYPE r). a -> b -> b
+f = undefined
+
+test1 :: forall r (b :: TYPE r). b -> b
+test1 = ( undefined `f` )
+
diff --git a/testsuite/tests/rep-poly/RepPolyLeftSection2.hs b/testsuite/tests/rep-poly/RepPolyLeftSection2.hs
new file mode 100644
index 0000000000..d243089209
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyLeftSection2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module RepPolyLeftSection2 where
+
+import GHC.Exts
+
+f :: forall r (a :: TYPE r). a -> a -> a
+f = undefined
+
+test1 :: forall r (a :: TYPE r). a -> a
+test1 = ( undefined `f` )
+
diff --git a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr
new file mode 100644
index 0000000000..79d0bc867e
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr
@@ -0,0 +1,9 @@
+
+RepPolyLeftSection2.hs:14:11: error:
+    • The function argument
+        ‘undefined’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: undefined
+      In the expression: undefined `f`
+      In an equation for ‘test1’: test1 = (undefined `f`)
diff --git a/testsuite/tests/rep-poly/RepPolyMagic.hs b/testsuite/tests/rep-poly/RepPolyMagic.hs
new file mode 100644
index 0000000000..befe72854b
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMagic.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module RepPolyMagic where
+
+import GHC.Exts
+import GHC.Magic
+
+foo :: forall a r (b :: TYPE r). a -> b -> b
+foo = seq
+
+bar :: forall r (a :: TYPE r). (a -> a) -> (a -> a)
+bar = oneShot
diff --git a/testsuite/tests/rep-poly/RepPolyMagic.stderr b/testsuite/tests/rep-poly/RepPolyMagic.stderr
new file mode 100644
index 0000000000..3c83b2c3ec
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMagic.stderr
@@ -0,0 +1,16 @@
+
+RepPolyMagic.hs:12:7: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The second argument of ‘seq’
+      does not have a fixed runtime representation:
+        b :: TYPE r
+    • In the expression: seq
+      In an equation for ‘foo’: foo = seq
+
+RepPolyMagic.hs:15:7: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The second argument of ‘oneShot’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: oneShot
+      In an equation for ‘bar’: bar = oneShot
diff --git a/testsuite/tests/rep-poly/RepPolyMatch.hs b/testsuite/tests/rep-poly/RepPolyMatch.hs
new file mode 100644
index 0000000000..35c3f807c4
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMatch.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyMatch where
+
+import GHC.Exts
+
+match :: forall rep (a :: TYPE rep). a -> ()
+match = \ case {}
diff --git a/testsuite/tests/rep-poly/RepPolyMatch.stderr b/testsuite/tests/rep-poly/RepPolyMatch.stderr
new file mode 100644
index 0000000000..f52a699002
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMatch.stderr
@@ -0,0 +1,7 @@
+
+RepPolyMatch.hs:11:9: error:
+    • The type of the first pattern in the case alternative
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the expression: \case
+      In an equation for ‘match’: match = \case
diff --git a/testsuite/tests/rep-poly/RepPolyMcBind.hs b/testsuite/tests/rep-poly/RepPolyMcBind.hs
new file mode 100644
index 0000000000..eee975b1db
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMcBind.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE MonadComprehensions #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyMcBind where
+
+import Data.Kind ( Type )
+import GHC.Exts
+import Prelude ( undefined )
+
+(>>=)
+  :: forall
+        rep
+        ( ma :: TYPE rep )
+        ( a  :: Type )
+        ( mb :: TYPE rep )
+        ( mc :: TYPE rep )
+  .  ma -> ( a -> mb ) -> mc
+(>>=) = undefined
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = [ () | x <- undefined :: ma ]
diff --git a/testsuite/tests/rep-poly/RepPolyMcBind.stderr b/testsuite/tests/rep-poly/RepPolyMcBind.stderr
new file mode 100644
index 0000000000..6468e4d73e
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMcBind.stderr
@@ -0,0 +1,9 @@
+
+RepPolyMcBind.hs:26:16: error:
+    • The first argument to (>>=),
+      arising from the monad comprehension,
+      does not have a fixed runtime representation:
+        ma :: TYPE rep
+    • In a stmt of a monad comprehension: x <- undefined :: ma
+      In the expression: [() | x <- undefined :: ma]
+      In an equation for ‘foo’: foo _ = [() | x <- undefined :: ma]
diff --git a/testsuite/tests/rep-poly/RepPolyMcBody.hs b/testsuite/tests/rep-poly/RepPolyMcBody.hs
new file mode 100644
index 0000000000..7ee8a7fa7c
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMcBody.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE MonadComprehensions #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyMcBody where
+
+import Data.Kind ( Type )
+import GHC.Exts
+import Prelude ( Bool(..), undefined )
+
+(>>)
+  :: forall
+        rep
+        ( ma :: TYPE rep )
+        ( a  :: Type )
+        ( mb :: TYPE rep )
+        ( mc :: TYPE rep )
+  .  ma -> ( a -> mb ) -> mc
+(>>) = undefined
+
+guard :: forall rep (b :: TYPE rep). Bool -> b
+guard = undefined
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = [ () | True ]
diff --git a/testsuite/tests/rep-poly/RepPolyMcBody.stderr b/testsuite/tests/rep-poly/RepPolyMcBody.stderr
new file mode 100644
index 0000000000..631e28cbc7
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMcBody.stderr
@@ -0,0 +1,9 @@
+
+RepPolyMcBody.hs:30:16: error:
+    • The first argument to (>>),
+      arising from the monad comprehension,
+      does not have a fixed runtime representation:
+        ma0 :: TYPE rep
+    • In a stmt of a monad comprehension: True
+      In the expression: [() | True]
+      In an equation for ‘foo’: foo _ = [() | True]
diff --git a/testsuite/tests/rep-poly/RepPolyMcGuard.hs b/testsuite/tests/rep-poly/RepPolyMcGuard.hs
new file mode 100644
index 0000000000..8977c6bc29
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMcGuard.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE MonadComprehensions #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyMcGuard where
+
+import Data.Kind ( Type )
+import GHC.Exts
+import Prelude ( Bool(..), undefined )
+
+(>>)
+  :: forall
+        rep
+        ( ma :: TYPE rep )
+        ( a  :: Type )
+        ( mb :: TYPE rep )
+        ( mc :: TYPE rep )
+  .  ma -> ( a -> mb ) -> mc
+(>>) = undefined
+
+guard :: forall rep (a :: TYPE rep) (b :: TYPE rep). a -> b
+guard = undefined
+
+return :: forall rep (ma :: TYPE rep). () -> ma
+return = undefined
+
+foo :: forall rep (ma :: TYPE rep). () -> ma
+foo _ = [ () | undefined ]
diff --git a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr
new file mode 100644
index 0000000000..1d7036cb0a
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr
@@ -0,0 +1,13 @@
+
+RepPolyMcGuard.hs:30:16: error:
+    • • The first argument to (>>),
+        arising from the monad comprehension,
+        does not have a fixed runtime representation:
+          ma0 :: TYPE rep
+      • The argument to ‘guard’,
+        arising from the monad comprehension,
+        does not have a fixed runtime representation:
+          a0 :: TYPE rep
+    • In a stmt of a monad comprehension: undefined
+      In the expression: [() | undefined]
+      In an equation for ‘foo’: foo _ = [() | undefined]
diff --git a/testsuite/tests/rep-poly/RepPolyNPlusK.hs b/testsuite/tests/rep-poly/RepPolyNPlusK.hs
new file mode 100644
index 0000000000..dee6fbf6e2
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyNPlusK.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE RebindableSyntax, NPlusKPatterns #-}
+
+module RepPolyNPlusK where
+
+import Prelude
+  ( Integer, Bool, undefined )
+import GHC.Exts
+
+fromInteger :: forall rep (a :: TYPE rep). Integer -> a
+fromInteger = undefined
+
+(+) :: forall rep (a :: TYPE rep). a -> a -> a
+(+) = undefined
+
+(-) :: forall rep (a :: TYPE rep). a -> a -> a
+(-) = undefined
+
+(>=) :: forall rep (a :: TYPE rep). a -> a -> Bool
+(>=) = undefined
+
+foo :: forall rep1 (a :: TYPE rep1). a -> ()
+foo (bndr_a+2) = ()
diff --git a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
new file mode 100644
index 0000000000..cb5f9c3ac4
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
@@ -0,0 +1,5 @@
+
+RepPolyNPlusK.hs:22:1: error:
+    The type of the first pattern in the equation for ‘foo’
+    does not have a fixed runtime representation:
+      a :: TYPE rep1
diff --git a/testsuite/tests/rep-poly/RepPolyNewtypePat1.hs b/testsuite/tests/rep-poly/RepPolyNewtypePat1.hs
new file mode 100644
index 0000000000..8ca2b06a4a
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyNewtypePat1.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module RepPolyNewtypePat1 where
+
+import GHC.Exts
+
+type X :: TYPE rep -> TYPE rep
+newtype X a = MkX a
+
+bar :: forall rep (a :: TYPE rep). X a -> a
+bar (MkX bndr_a) = bndr_a
diff --git a/testsuite/tests/rep-poly/RepPolyNewtypePat1.stderr b/testsuite/tests/rep-poly/RepPolyNewtypePat1.stderr
new file mode 100644
index 0000000000..c2f391f928
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyNewtypePat1.stderr
@@ -0,0 +1,5 @@
+
+RepPolyNewtypePat1.hs:16:1: error:
+    The type of the first pattern in the equation for ‘bar’
+    does not have a fixed runtime representation:
+      X a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyNewtypePat2.hs b/testsuite/tests/rep-poly/RepPolyNewtypePat2.hs
new file mode 100644
index 0000000000..b92d911ecf
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyNewtypePat2.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module RepPolyNewtypePat2 where
+
+import Data.Kind
+import GHC.Exts
+
+type X :: TYPE rep -> TYPE rep
+newtype X a = MkX a
+
+bar :: forall (a :: Type). X a -> a
+bar (MkX bndr_a) = bndr_a
diff --git a/testsuite/tests/rep-poly/RepPolyPatBind.hs b/testsuite/tests/rep-poly/RepPolyPatBind.hs
new file mode 100644
index 0000000000..7b811b0fc7
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatBind.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolyPatBind where
+
+import Data.Kind
+import GHC.Exts
+
+foo :: forall rep (a :: TYPE rep). () -> a
+foo _ =
+  let
+    x, y :: a
+    (# x, y #) = undefined
+  in x
diff --git a/testsuite/tests/rep-poly/RepPolyPatBind.stderr b/testsuite/tests/rep-poly/RepPolyPatBind.stderr
new file mode 100644
index 0000000000..b372027ea9
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatBind.stderr
@@ -0,0 +1,15 @@
+
+RepPolyPatBind.hs:18:5: error:
+    • The binder ‘x’ does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the expression:
+        let
+          x, y :: a
+          (# x, y #) = undefined
+        in x
+      In an equation for ‘foo’:
+          foo _
+            = let
+                x, y :: a
+                (# x, y #) = undefined
+              in x
diff --git a/testsuite/tests/rep-poly/RepPolyPatSynArg.hs b/testsuite/tests/rep-poly/RepPolyPatSynArg.hs
new file mode 100644
index 0000000000..a69836cbf9
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatSynArg.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module RepPolyPatSynArg where
+
+import Data.Kind
+import GHC.Exts
+
+type X :: TYPE rep -> Type
+data X a = MkX
+
+pattern Pat :: forall rep (a :: TYPE rep). a -> X a
+pattern Pat bndr_a <- ( undefined -> bndr_a )
diff --git a/testsuite/tests/rep-poly/RepPolyPatSynArg.stderr b/testsuite/tests/rep-poly/RepPolyPatSynArg.stderr
new file mode 100644
index 0000000000..6b9b7f5473
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatSynArg.stderr
@@ -0,0 +1,4 @@
+
+RepPolyPatSynArg.hs:17:1: error:
+    The pattern synonym argument does not have a fixed runtime representation:
+    • a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyPatSynRes.hs b/testsuite/tests/rep-poly/RepPolyPatSynRes.hs
new file mode 100644
index 0000000000..2f19b8ec0b
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatSynRes.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module RepPolyPatSynRes where
+
+import GHC.Exts
+
+pattern Pat :: forall rep (a :: TYPE rep). ( () ~ () ) => a
+pattern Pat <- ( undefined -> True )
diff --git a/testsuite/tests/rep-poly/RepPolyPatSynRes.stderr b/testsuite/tests/rep-poly/RepPolyPatSynRes.stderr
new file mode 100644
index 0000000000..d857ba135d
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatSynRes.stderr
@@ -0,0 +1,4 @@
+
+RepPolyPatSynRes.hs:13:1: error:
+    The pattern synonym scrutinee does not have a fixed runtime representation:
+    • a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyPatSynUnliftedNewtype.hs b/testsuite/tests/rep-poly/RepPolyPatSynUnliftedNewtype.hs
new file mode 100644
index 0000000000..cc69635e1a
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatSynUnliftedNewtype.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module RepPolyPatSynUnliftedNewtype where
+
+import GHC.Exts
+
+type X :: TYPE rep -> TYPE rep
+newtype X a = MkX a
+
+pattern Pat :: forall rep (a :: TYPE rep). a -> X a
+pattern Pat bndr_a <- MkX bndr_a
diff --git a/testsuite/tests/rep-poly/RepPolyPatSynUnliftedNewtype.stderr b/testsuite/tests/rep-poly/RepPolyPatSynUnliftedNewtype.stderr
new file mode 100644
index 0000000000..0f1923944b
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyPatSynUnliftedNewtype.stderr
@@ -0,0 +1,8 @@
+
+RepPolyPatSynUnliftedNewtype.hs:16:1: error:
+    The pattern synonym scrutinee does not have a fixed runtime representation:
+    • X a :: TYPE rep
+
+RepPolyPatSynUnliftedNewtype.hs:16:1: error:
+    The pattern synonym argument does not have a fixed runtime representation:
+    • a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyRecordPattern.hs b/testsuite/tests/rep-poly/RepPolyRecordPattern.hs
new file mode 100644
index 0000000000..33a7d9482b
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRecordPattern.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module RepPolyRecordPattern where
+
+import GHC.Exts
+
+newtype X (a :: TYPE rep) = MkX { fld :: a }
+
+class C rep (a :: TYPE rep) where
+  meth :: () -> a
+
+upd :: forall rep (a :: TYPE rep). X a -> a
+upd ( MkX bndr_a ) = bndr_a
diff --git a/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr b/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr
new file mode 100644
index 0000000000..de3d9b66cc
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr
@@ -0,0 +1,10 @@
+
+RepPolyRecordPattern.hs:7:35: error:
+    The type of the first pattern in the equation for ‘fld’
+    does not have a fixed runtime representation:
+      X a :: TYPE rep
+
+RepPolyRecordPattern.hs:13:1: error:
+    The type of the first pattern in the equation for ‘upd’
+    does not have a fixed runtime representation:
+      X a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.hs b/testsuite/tests/rep-poly/RepPolyRecordUpdate.hs
new file mode 100644
index 0000000000..9ef3a0f897
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module RepPolyRecordUpdate where
+
+import GHC.Exts
+
+newtype X (a :: TYPE rep) = MkX { fld :: a }
+
+class C rep (a :: TYPE rep) where
+  meth :: () -> a
+
+upd :: C rep a => X b -> X a
+upd x = x { fld = meth () }
diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
new file mode 100644
index 0000000000..91e7742f59
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
@@ -0,0 +1,12 @@
+
+RepPolyRecordUpdate.hs:7:35: error:
+    The type of the first pattern in the equation for ‘fld’
+    does not have a fixed runtime representation:
+      X a :: TYPE rep
+
+RepPolyRecordUpdate.hs:13:9: error:
+    • The record update at field ‘fld’ does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the ‘fld’ field of a record
+      In the expression: x {fld = meth ()}
+      In an equation for ‘upd’: upd x = x {fld = meth ()}
diff --git a/testsuite/tests/rep-poly/RepPolyRightSection.hs b/testsuite/tests/rep-poly/RepPolyRightSection.hs
new file mode 100644
index 0000000000..23fe545bf5
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRightSection.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module RepPolyRightSection where
+
+import GHC.Exts
+
+g :: forall r (a :: TYPE r) b. a -> b -> a
+g = undefined
+
+test2 :: forall r (a :: TYPE r). a -> a
+test2 = ( `g` undefined )
diff --git a/testsuite/tests/rep-poly/RepPolyRightSection.stderr b/testsuite/tests/rep-poly/RepPolyRightSection.stderr
new file mode 100644
index 0000000000..3209cdfff6
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRightSection.stderr
@@ -0,0 +1,8 @@
+
+RepPolyRightSection.hs:14:11: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The third argument of ‘rightSection’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: `g` undefined
+      In an equation for ‘test2’: test2 = (`g` undefined)
diff --git a/testsuite/tests/rep-poly/RepPolyRule1.hs b/testsuite/tests/rep-poly/RepPolyRule1.hs
new file mode 100644
index 0000000000..9bf156ac6a
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRule1.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds, PolyKinds #-}
+
+module RepPolyRule1 where
+
+import GHC.Exts
+
+f :: forall rep (a :: TYPE rep). a -> a
+f = undefined
+{-# NOINLINE f #-}
+
+{-# RULES "f_id" forall (x :: (a :: TYPE rep)). f x = x #-}
diff --git a/testsuite/tests/rep-poly/RepPolyRule1.stderr b/testsuite/tests/rep-poly/RepPolyRule1.stderr
new file mode 100644
index 0000000000..45305c5b72
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRule1.stderr
@@ -0,0 +1,9 @@
+
+RepPolyRule1.hs:11:51: error:
+    • The function argument
+        ‘x’
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the first argument of ‘f’, namely ‘x’
+      In the expression: f x
+      When checking the rewrite rule "f_id"
diff --git a/testsuite/tests/rep-poly/RepPolyRule2.hs b/testsuite/tests/rep-poly/RepPolyRule2.hs
new file mode 100644
index 0000000000..2163a67129
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRule2.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds, PolyKinds, StandaloneKindSignatures, TypeFamilyDependencies #-}
+
+module RepPolyRule2 where
+
+import GHC.Exts
+
+type F :: RuntimeRep -> RuntimeRep
+type family F rep  = r | r -> rep where
+  F IntRep  = WordRep
+  F WordRep = IntRep
+  F rep     = rep
+
+f :: forall rep (a :: TYPE (F rep)). a -> a
+f = undefined
+
+{-# NOINLINE f #-}
+{-# RULES "f_id" forall (x :: (a :: TYPE (F rep))). f x = x #-}
diff --git a/testsuite/tests/rep-poly/RepPolyRule2.stderr b/testsuite/tests/rep-poly/RepPolyRule2.stderr
new file mode 100644
index 0000000000..70a5af4687
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRule2.stderr
@@ -0,0 +1,9 @@
+
+RepPolyRule2.hs:17:55: error:
+    • The function argument
+        ‘x’
+      does not have a fixed runtime representation:
+        a :: TYPE (F rep)
+    • In the first argument of ‘f’, namely ‘x’
+      In the expression: f x
+      When checking the rewrite rule "f_id"
diff --git a/testsuite/tests/rep-poly/RepPolyRule3.hs b/testsuite/tests/rep-poly/RepPolyRule3.hs
new file mode 100644
index 0000000000..c8fccaf5d5
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyRule3.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds, PolyKinds, StandaloneKindSignatures, TypeFamilyDependencies #-}
+
+module RepPolyRule3 where
+
+import GHC.Exts
+
+type F :: RuntimeRep -> RuntimeRep
+type family F rep  = r | r -> rep where
+  F IntRep  = WordRep
+  F WordRep = IntRep
+  F rep     = rep
+
+g :: forall rep (a :: TYPE (F rep)). a -> a
+g = undefined
+
+{-# NOINLINE g #-}
+{-# RULES "g_id" forall (x :: (a :: TYPE (F WordRep))). g x = x #-}
+
+h :: forall rep (a :: TYPE (F rep)). a -> a
+h = undefined
+
+{-# NOINLINE h #-}
+{-# RULES "h_id" forall (x :: (a :: TYPE IntRep)). h x = x #-}
diff --git a/testsuite/tests/rep-poly/RepPolySum.hs b/testsuite/tests/rep-poly/RepPolySum.hs
new file mode 100644
index 0000000000..d58b9d1b02
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolySum.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolySum1 where
+
+import GHC.Exts
+
+foo :: forall (rep :: RuntimeRep) (a :: TYPE rep). () -> (# Int# | a #)
+foo _ = (# | bar () #)
+  where
+    bar :: () -> a
+    bar _ = undefined
+
+-- This one crucially must also cause an error,
+-- even though there are no representation-polymorphic values.
+-- See GHC ticket #20277.
+baz :: forall (rep :: RuntimeRep) (a :: TYPE rep). () -> (# Int# | a #)
+baz _ = (# 17# | #)
diff --git a/testsuite/tests/rep-poly/RepPolySum.stderr b/testsuite/tests/rep-poly/RepPolySum.stderr
new file mode 100644
index 0000000000..f4f7bd09fe
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolySum.stderr
@@ -0,0 +1,17 @@
+
+RepPolySum.hs:11:9: error:
+    • The unboxed sum result type does not have a fixed runtime representation:
+        (# Int# | a #) :: TYPE ('SumRep '[ 'IntRep, rep])
+    • In the expression: (# | bar () #)
+      In an equation for ‘foo’:
+          foo _
+            = (# | bar () #)
+            where
+                bar :: () -> a
+                bar _ = undefined
+
+RepPolySum.hs:20:9: error:
+    • The unboxed sum result type does not have a fixed runtime representation:
+        (# Int# | a #) :: TYPE ('SumRep '[ 'IntRep, rep])
+    • In the expression: (# 17# | #)
+      In an equation for ‘baz’: baz _ = (# 17# | #)
diff --git a/testsuite/tests/rep-poly/RepPolyTuple.hs b/testsuite/tests/rep-poly/RepPolyTuple.hs
new file mode 100644
index 0000000000..d5f49cfc81
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyTuple.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolyTuple where
+
+import GHC.Exts
+
+foo :: forall (r :: RuntimeRep) (a :: TYPE r). () -> (# a, a, a #)
+foo _ = (# bar (), bar (), bar () #)
+  where
+    bar :: forall (r :: RuntimeRep) (a :: TYPE r). () -> a
+    bar _ = undefined
diff --git a/testsuite/tests/rep-poly/RepPolyTuple.stderr b/testsuite/tests/rep-poly/RepPolyTuple.stderr
new file mode 100644
index 0000000000..1c2c701fb2
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyTuple.stderr
@@ -0,0 +1,11 @@
+
+RepPolyTuple.hs:11:9: error:
+    • The tuple argument in first position does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: (# bar (), bar (), bar () #)
+      In an equation for ‘foo’:
+          foo _
+            = (# bar (), bar (), bar () #)
+            where
+                bar :: forall (r :: RuntimeRep) (a :: TYPE r). () -> a
+                bar _ = undefined
diff --git a/testsuite/tests/rep-poly/RepPolyTupleSection.hs b/testsuite/tests/rep-poly/RepPolyTupleSection.hs
new file mode 100644
index 0000000000..9b0087ae38
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyTupleSection.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolyTupleSection where
+
+import GHC.Exts
+
+foo :: forall (r :: RuntimeRep) (a :: TYPE r). a -> (# Int#, a #)
+foo = (# 3#, #)
diff --git a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr
new file mode 100644
index 0000000000..b4d08d02de
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr
@@ -0,0 +1,6 @@
+
+RepPolyTupleSection.hs:11:7: error:
+    • The tuple section does not have a fixed runtime representation in the second position:
+        a :: TYPE r
+    • In the expression: (# 3#, #)
+      In an equation for ‘foo’: foo = (# 3#, #)
diff --git a/testsuite/tests/rep-poly/RepPolyUnboxedPatterns.hs b/testsuite/tests/rep-poly/RepPolyUnboxedPatterns.hs
new file mode 100644
index 0000000000..601c65d0e8
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyUnboxedPatterns.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UnboxedTuples, MagicHash #-}
+
+module RepPolyUnboxedPatterns where
+
+import GHC.Exts
+
+foo :: forall rep1 (a :: TYPE rep1) rep2 (b :: TYPE rep2). (# a, b #) -> ()
+foo (# bndr_a, bndr_b #) = ()
+
+bar :: forall rep1 (a :: TYPE rep1) rep2 (b :: TYPE rep2). (# a | b #) -> ()
+bar (# bndr_a | #) = ()
+bar (# | bndr_b #) = ()
diff --git a/testsuite/tests/rep-poly/RepPolyUnboxedPatterns.stderr b/testsuite/tests/rep-poly/RepPolyUnboxedPatterns.stderr
new file mode 100644
index 0000000000..ced2503ca9
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyUnboxedPatterns.stderr
@@ -0,0 +1,10 @@
+
+RepPolyUnboxedPatterns.hs:8:1: error:
+    The type of the first pattern in the equation for ‘foo’
+    does not have a fixed runtime representation:
+      (# a, b #) :: TYPE ('TupleRep '[rep1, rep2])
+
+RepPolyUnboxedPatterns.hs:11:1: error:
+    The type of the first pattern in the equation for ‘bar’
+    does not have a fixed runtime representation:
+      (# a | b #) :: TYPE ('SumRep '[rep1, rep2])
diff --git a/testsuite/tests/rep-poly/RepPolyUnliftedDatatype.hs b/testsuite/tests/rep-poly/RepPolyUnliftedDatatype.hs
new file mode 100644
index 0000000000..c5a985567d
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyUnliftedDatatype.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UnliftedDatatypes #-}
+
+module RepPolyUnliftedDatatype where
+
+import Data.Kind
+import GHC.Exts
+
+type D :: forall (l :: Levity) -> TYPE (BoxedRep l)
+data D l = forall x. (Show x, Eq x, Ord x, Read x) => MkD x Int x
+  -- the constraints are to ensure we are not including them
+  -- in the calculation of the arity
+
+foo :: forall (l :: Levity). () -> D l
+foo _ = MkD False 12 True
diff --git a/testsuite/tests/rep-poly/RepPolyWildcardPattern.hs b/testsuite/tests/rep-poly/RepPolyWildcardPattern.hs
new file mode 100644
index 0000000000..4bc6df0323
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyWildcardPattern.hs
@@ -0,0 +1,6 @@
+module RepPolyWildcardPattern where
+
+import GHC.Exts
+
+foo :: forall rep (a :: TYPE rep). a -> ()
+foo _ = ()
diff --git a/testsuite/tests/rep-poly/RepPolyWildcardPattern.stderr b/testsuite/tests/rep-poly/RepPolyWildcardPattern.stderr
new file mode 100644
index 0000000000..f5bb0cca08
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyWildcardPattern.stderr
@@ -0,0 +1,5 @@
+
+RepPolyWildcardPattern.hs:6:1: error:
+    The type of the first pattern in the equation for ‘foo’
+    does not have a fixed runtime representation:
+      a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/RepPolyWrappedVar.hs b/testsuite/tests/rep-poly/RepPolyWrappedVar.hs
new file mode 100644
index 0000000000..bcc552d443
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyWrappedVar.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MagicHash #-}
+
+module RepPolyWrappedVar where
+
+import GHC.Exts
+
+primop :: forall (l :: Levity) (a :: TYPE ('BoxedRep l)).
+          a -> Int -> (State# RealWorld -> (# State# RealWorld, Bool #))
+       -> State# RealWorld -> (# State# RealWorld, Weak# Int #)
+primop = mkWeak# @a @Int @Bool
diff --git a/testsuite/tests/rep-poly/RepPolyWrappedVar.stderr b/testsuite/tests/rep-poly/RepPolyWrappedVar.stderr
new file mode 100644
index 0000000000..d89a54115e
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyWrappedVar.stderr
@@ -0,0 +1,8 @@
+
+RepPolyWrappedVar.hs:15:10: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The first argument of ‘mkWeak#’
+      does not have a fixed runtime representation:
+        a :: TYPE ('BoxedRep l)
+    • In the expression: mkWeak# @a @Int @Bool
+      In an equation for ‘primop’: primop = mkWeak# @a @Int @Bool
diff --git a/testsuite/tests/rep-poly/RepPolyWrappedVar2.hs b/testsuite/tests/rep-poly/RepPolyWrappedVar2.hs
new file mode 100644
index 0000000000..f00f9d851c
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyWrappedVar2.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+
+module RepPolyWrappedVar2 where
+
+import GHC.Exts
+
+foo = unsafeCoerce# @IntRep @AddrRep
diff --git a/testsuite/tests/rep-poly/T11473.hs b/testsuite/tests/rep-poly/T11473.hs
new file mode 100644
index 0000000000..ebfeeb8a13
--- /dev/null
+++ b/testsuite/tests/rep-poly/T11473.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, RankNTypes #-}
+
+module T11473 where
+
+import GHC.Exts
+import GHC.Types
+
+type family Boxed (a :: k) :: *
+type instance Boxed Char# = Char
+type instance Boxed Char  = Char
+
+class BoxIt (a :: TYPE lev) where
+    boxed :: a -> Boxed a
+
+instance BoxIt Char# where boxed x = C# x
+instance BoxIt Char  where boxed = id
+
+hello :: forall (r :: RuntimeRep). forall (a :: TYPE r). BoxIt a => a -> Boxed a
+hello x = boxed x
+{-# NOINLINE hello #-}
+
+main :: IO ()
+main = do
+    print $ boxed 'c'#
+    print $ boxed 'c'
+    print $ hello 'c'
+    print $ hello 'c'#
diff --git a/testsuite/tests/rep-poly/T11473.stderr b/testsuite/tests/rep-poly/T11473.stderr
new file mode 100644
index 0000000000..fdfa418318
--- /dev/null
+++ b/testsuite/tests/rep-poly/T11473.stderr
@@ -0,0 +1,14 @@
+
+T11473.hs:19:1: error:
+    The type of the first pattern in the equation for ‘hello’
+    does not have a fixed runtime representation:
+      a :: TYPE r
+
+T11473.hs:19:17: error:
+    • The function argument
+        ‘x’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the first argument of ‘boxed’, namely ‘x’
+      In the expression: boxed x
+      In an equation for ‘hello’: hello x = boxed x
diff --git a/testsuite/tests/rep-poly/T11724.hs b/testsuite/tests/rep-poly/T11724.hs
new file mode 100644
index 0000000000..23412e9df9
--- /dev/null
+++ b/testsuite/tests/rep-poly/T11724.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+
+module T11724 where
+
+import GHC.Exts
+
+data Foo (r :: RuntimeRep) (a :: TYPE r) = Foo a
diff --git a/testsuite/tests/rep-poly/T11724.stderr b/testsuite/tests/rep-poly/T11724.stderr
new file mode 100644
index 0000000000..1c63de3d1a
--- /dev/null
+++ b/testsuite/tests/rep-poly/T11724.stderr
@@ -0,0 +1,6 @@
+
+T11724.hs:7:44: error:
+    • The data constructor field does not have a fixed runtime representation:
+      • a :: TYPE r
+    • In the definition of data constructor ‘Foo’
+      In the data type declaration for ‘Foo’
diff --git a/testsuite/tests/rep-poly/T12709.hs b/testsuite/tests/rep-poly/T12709.hs
new file mode 100644
index 0000000000..6a7e37a5d2
--- /dev/null
+++ b/testsuite/tests/rep-poly/T12709.hs
@@ -0,0 +1,30 @@
+{-# Language PolyKinds, ViewPatterns, RebindableSyntax,
+             MagicHash, NoImplicitPrelude #-}
+
+module T12709 where
+
+import GHC.Types
+import Prelude hiding (Num (..))
+import qualified Prelude as P
+import GHC.Prim
+
+data BoxUnbox = BUB Int Int#
+
+class Num (a :: TYPE rep) where
+  (+) :: a -> a -> a
+
+  fromInteger :: Integer -> a
+
+instance Num Int where
+  (+) = (P.+)
+  fromInteger = P.fromInteger
+
+instance Num Int# where
+  (+) = (+#)
+  fromInteger (fromInteger -> I# n) = n
+
+a :: BoxUnbox
+a = let u :: Num (a :: TYPE rep) => a
+        u = 1 + 2 + 3 + 4
+     in
+        BUB u u
diff --git a/testsuite/tests/rep-poly/T12709.stderr b/testsuite/tests/rep-poly/T12709.stderr
new file mode 100644
index 0000000000..5b70aea4d7
--- /dev/null
+++ b/testsuite/tests/rep-poly/T12709.stderr
@@ -0,0 +1,36 @@
+
+T12709.hs:28:13: error:
+    • The function argument
+        ‘1’
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the first argument of ‘(+)’, namely ‘1’
+      In the first argument of ‘(+)’, namely ‘1 + 2’
+      In the first argument of ‘(+)’, namely ‘1 + 2 + 3’
+
+T12709.hs:28:17: error:
+    • The function argument
+        ‘2’
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the second argument of ‘(+)’, namely ‘2’
+      In the first argument of ‘(+)’, namely ‘1 + 2’
+      In the first argument of ‘(+)’, namely ‘1 + 2 + 3’
+
+T12709.hs:28:21: error:
+    • The function argument
+        ‘3’
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the second argument of ‘(+)’, namely ‘3’
+      In the first argument of ‘(+)’, namely ‘1 + 2 + 3’
+      In the expression: 1 + 2 + 3 + 4
+
+T12709.hs:28:25: error:
+    • The function argument
+        ‘4’
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the second argument of ‘(+)’, namely ‘4’
+      In the expression: 1 + 2 + 3 + 4
+      In an equation for ‘u’: u = 1 + 2 + 3 + 4
diff --git a/testsuite/tests/rep-poly/T12973.hs b/testsuite/tests/rep-poly/T12973.hs
new file mode 100644
index 0000000000..765e02f34b
--- /dev/null
+++ b/testsuite/tests/rep-poly/T12973.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RebindableSyntax, PolyKinds, ExplicitForAll #-}
+
+module T12973 where
+
+import qualified Prelude as P
+import GHC.Exts
+
+class Num (a :: TYPE r) where
+  (+) :: a -> a -> a
+  fromInteger :: P.Integer -> a
+
+foo :: forall r (a :: TYPE r). Num a => a
+foo = 3 + 4
+
+
diff --git a/testsuite/tests/rep-poly/T12973.stderr b/testsuite/tests/rep-poly/T12973.stderr
new file mode 100644
index 0000000000..cc03e032e3
--- /dev/null
+++ b/testsuite/tests/rep-poly/T12973.stderr
@@ -0,0 +1,18 @@
+
+T12973.hs:13:7: error:
+    • The function argument
+        ‘3’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the first argument of ‘(+)’, namely ‘3’
+      In the expression: 3 + 4
+      In an equation for ‘foo’: foo = 3 + 4
+
+T12973.hs:13:11: error:
+    • The function argument
+        ‘4’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the second argument of ‘(+)’, namely ‘4’
+      In the expression: 3 + 4
+      In an equation for ‘foo’: foo = 3 + 4
diff --git a/testsuite/tests/rep-poly/T13105.hs b/testsuite/tests/rep-poly/T13105.hs
new file mode 100644
index 0000000000..b2b23c7442
--- /dev/null
+++ b/testsuite/tests/rep-poly/T13105.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE UnicodeSyntax, MagicHash, DataKinds, PolyKinds, TypeFamilies #-}
+
+-- from Conal Elliott
+-- Actually, this *should* work. But I want to put it in the testsuite
+-- as a succeeding "compile_fail" test to make sure that we don't panic.
+
+module RepRep where
+
+import GHC.Exts
+
+type family RepRep a ∷ RuntimeRep
+
+class HasRep a where
+  type Rep a ∷ TYPE (RepRep a)
+  repr ∷ a → Rep a
+  abst ∷ Rep a → a
+
+type instance RepRep Int = IntRep
+
+instance HasRep Int where
+  type Rep Int = Int#
+  abst n = I# n
+  repr (I# n) = n
diff --git a/testsuite/tests/rep-poly/T13233.hs b/testsuite/tests/rep-poly/T13233.hs
new file mode 100644
index 0000000000..c4c0480a75
--- /dev/null
+++ b/testsuite/tests/rep-poly/T13233.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MagicHash #-}
+module Bug where
+
+import GHC.Exts ( TYPE, RuntimeRep )
+
+class Foo (a :: TYPE rep) where
+  bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
+
+baz :: forall rep (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
+baz = bar (#,#)
+
+obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
+                   (a :: TYPE rep1) (b :: TYPE rep2).
+                   a -> b -> (# a, b #)) -> ()
+obscure _ = ()
+
+quux :: ()
+quux = obscure (#,#)
diff --git a/testsuite/tests/rep-poly/T13233.stderr b/testsuite/tests/rep-poly/T13233.stderr
new file mode 100644
index 0000000000..248b71c49d
--- /dev/null
+++ b/testsuite/tests/rep-poly/T13233.stderr
@@ -0,0 +1,19 @@
+
+T13233.hs:14:11: error:
+    • The data constructor argument in first position
+      does not have a fixed runtime representation:
+        a :: TYPE rep
+    • In the first argument of ‘bar’, namely ‘(#,#)’
+      In the expression: bar (#,#)
+      In an equation for ‘baz’: baz = bar (#,#)
+
+T13233.hs:22:16: error:
+    • • The data constructor argument in first position
+        does not have a fixed runtime representation:
+          a :: TYPE rep1
+      • The data constructor argument in second position
+        does not have a fixed runtime representation:
+          b :: TYPE rep2
+    • In the first argument of ‘obscure’, namely ‘(#,#)’
+      In the expression: obscure (#,#)
+      In an equation for ‘quux’: quux = obscure (#,#)
diff --git a/testsuite/tests/rep-poly/T13929.hs b/testsuite/tests/rep-poly/T13929.hs
new file mode 100644
index 0000000000..f0801e8e0e
--- /dev/null
+++ b/testsuite/tests/rep-poly/T13929.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Main where
+
+import GHC.Exts
+import Data.Kind
+import GHC.Generics
+
+class GUnbox (f :: Type -> Type) (r :: RuntimeRep) where
+    type GUnboxed f r :: TYPE r
+    gunbox :: f p -> GUnboxed f r
+
+instance (GUnbox f rf, GUnbox g rg) => GUnbox (f :*: g) ('TupleRep '[rf, rg]) where
+    type GUnboxed (f :*: g) ('TupleRep '[rf, rg]) = (# GUnboxed f rf, GUnboxed g rg #)
+    -- if I remove implementation of `gunbox` it compiles successfully
+    gunbox (x :*: y) = (# gunbox x, gunbox y #)
+
+instance (GUnbox f rf, GUnbox g rg) => GUnbox (f :+: g) ('SumRep '[rf, rg]) where
+    type GUnboxed (f :+: g) ('SumRep '[rf, rg]) = (# GUnboxed f rf | GUnboxed g rg #)
+    gunbox (L1 l) = (# gunbox l | #)
+    gunbox (R1 r) = (# | gunbox r #)
+
+main :: IO ()
+main = pure ()
diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr
new file mode 100644
index 0000000000..2b4d8a9768
--- /dev/null
+++ b/testsuite/tests/rep-poly/T13929.stderr
@@ -0,0 +1,27 @@
+
+T13929.hs:29:24: error:
+    • • The tuple argument in first position does not have a fixed runtime representation:
+          GUnboxed f rf :: TYPE rf
+      • The tuple argument in second position does not have a fixed runtime representation:
+          GUnboxed g rg :: TYPE rg
+    • In the expression: (# gunbox x, gunbox y #)
+      In an equation for ‘gunbox’:
+          gunbox (x :*: y) = (# gunbox x, gunbox y #)
+      In the instance declaration for
+        ‘GUnbox (f :*: g) ('TupleRep '[rf, rg])’
+
+T13929.hs:33:21: error:
+    • The unboxed sum result type does not have a fixed runtime representation:
+        GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg])
+    • In the expression: (# gunbox l | #)
+      In an equation for ‘gunbox’: gunbox (L1 l) = (# gunbox l | #)
+      In the instance declaration for
+        ‘GUnbox (f :+: g) ('SumRep '[rf, rg])’
+
+T13929.hs:34:21: error:
+    • The unboxed sum result type does not have a fixed runtime representation:
+        GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg])
+    • In the expression: (# | gunbox r #)
+      In an equation for ‘gunbox’: gunbox (R1 r) = (# | gunbox r #)
+      In the instance declaration for
+        ‘GUnbox (f :+: g) ('SumRep '[rf, rg])’
diff --git a/testsuite/tests/rep-poly/T14561.hs b/testsuite/tests/rep-poly/T14561.hs
new file mode 100644
index 0000000000..dede8ba2f8
--- /dev/null
+++ b/testsuite/tests/rep-poly/T14561.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module T14561 where
+
+import GHC.Types
+import Unsafe.Coerce
+
+badId :: forall r (a :: TYPE r). a -> a
+badId = unsafeCoerce#
+-- Un-saturated application of a representation-polymorphic
+-- function that must be eta-expanded
+
+goodId :: forall (a :: Type). a -> a
+goodId = unsafeCoerce#
+-- But this one is OK
diff --git a/testsuite/tests/rep-poly/T14561.stderr b/testsuite/tests/rep-poly/T14561.stderr
new file mode 100644
index 0000000000..d6815cbdcf
--- /dev/null
+++ b/testsuite/tests/rep-poly/T14561.stderr
@@ -0,0 +1,8 @@
+
+T14561.hs:12:9: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The first argument of ‘unsafeCoerce#’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: unsafeCoerce#
+      In an equation for ‘badId’: badId = unsafeCoerce#
diff --git a/testsuite/tests/rep-poly/T14561b.hs b/testsuite/tests/rep-poly/T14561b.hs
new file mode 100644
index 0000000000..cf36208b04
--- /dev/null
+++ b/testsuite/tests/rep-poly/T14561b.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module T14561 where
+
+import Data.Coerce
+import GHC.Exts
+
+badId :: forall r (a :: TYPE r). a -> a
+badId = coerce
+-- Un-saturated application of a representation-polymorphic
+-- function that must be eta-expanded
diff --git a/testsuite/tests/rep-poly/T14561b.stderr b/testsuite/tests/rep-poly/T14561b.stderr
new file mode 100644
index 0000000000..e7a919bb86
--- /dev/null
+++ b/testsuite/tests/rep-poly/T14561b.stderr
@@ -0,0 +1,8 @@
+
+T14561b.hs:12:9: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The first argument of ‘coerce’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: coerce
+      In an equation for ‘badId’: badId = coerce
diff --git a/testsuite/tests/rep-poly/T14765.hs b/testsuite/tests/rep-poly/T14765.hs
new file mode 100644
index 0000000000..b124252bb4
--- /dev/null
+++ b/testsuite/tests/rep-poly/T14765.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE MagicHash, PolyKinds, ExplicitForAll #-}
+
+module T14765 where
+
+import GHC.Exts
+
+fold :: forall rep a (r :: TYPE rep).
+          (r -> a -> Proxy# r -> r) -> (Proxy# r -> r) -> [a] -> r
+fold f k [] = k proxy#
+fold f k (x : xs) = fold f (f (k proxy#) x) xs
diff --git a/testsuite/tests/rep-poly/T14765.stderr b/testsuite/tests/rep-poly/T14765.stderr
new file mode 100644
index 0000000000..3e580cc884
--- /dev/null
+++ b/testsuite/tests/rep-poly/T14765.stderr
@@ -0,0 +1,9 @@
+
+T14765.hs:11:31: error:
+    • The function argument
+        ‘(k proxy#)’
+      does not have a fixed runtime representation:
+        r :: TYPE rep
+    • In the first argument of ‘f’, namely ‘(k proxy#)’
+      In the second argument of ‘fold’, namely ‘(f (k proxy#) x)’
+      In the expression: fold f (f (k proxy#) x) xs
diff --git a/testsuite/tests/rep-poly/T17021.hs b/testsuite/tests/rep-poly/T17021.hs
new file mode 100644
index 0000000000..f02c2f7e42
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17021.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+module T17021 where
+
+import Data.Kind
+import GHC.Exts
+
+type family Id (x :: a) :: a where
+  Id x = x
+
+newtype T :: TYPE (Id LiftedRep) where
+  MkT :: Int -> T
+
+f :: T
+f = MkT 42
diff --git a/testsuite/tests/rep-poly/T17360.hs b/testsuite/tests/rep-poly/T17360.hs
new file mode 100644
index 0000000000..fc82675271
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17360.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE PolyKinds #-}
+module T17360 where
+
+import GHC.Exts
+
+newtype Id (a :: TYPE r) = Id a
+
+foo :: forall r (a :: TYPE r). Id a -> Id a
+foo x = x
diff --git a/testsuite/tests/rep-poly/T17360.stderr b/testsuite/tests/rep-poly/T17360.stderr
new file mode 100644
index 0000000000..5b9c25bc70
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17360.stderr
@@ -0,0 +1,5 @@
+
+T17360.hs:11:1: error:
+    The type of the first pattern in the equation for ‘foo’
+    does not have a fixed runtime representation:
+      Id a :: TYPE r
diff --git a/testsuite/tests/rep-poly/T17536.hs b/testsuite/tests/rep-poly/T17536.hs
new file mode 100644
index 0000000000..2361cc269f
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17536.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}
+
+module T17536 where
+
+import Data.Kind
+import GHC.Exts
+
+data A (r :: RuntimeRep)
+
+type family IsA r where
+  IsA (A _) = Char
+  IsA _     = Int
+
+f :: IsA (A UnliftedRep)
+f = 'a'
diff --git a/testsuite/tests/rep-poly/T17536b.hs b/testsuite/tests/rep-poly/T17536b.hs
new file mode 100644
index 0000000000..6edcd10d25
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17536b.hs
@@ -0,0 +1,20 @@
+
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T17536b where
+
+import Data.Kind
+import GHC.Exts
+
+type P :: forall (r :: RuntimeRep). TYPE r -> Type
+data P a where
+  L :: P Int
+  U :: P Int#
+
+g :: forall r (a :: TYPE r). P a -> a -> a
+g L = \ _ -> 0
+g U = \ _ -> 3#
diff --git a/testsuite/tests/rep-poly/T17817.hs b/testsuite/tests/rep-poly/T17817.hs
new file mode 100644
index 0000000000..b87178f909
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17817.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MagicHash #-}
+module Bug where
+
+import GHC.Exts ( TYPE, RuntimeRep(BoxedRep), Levity
+                , Weak#, State#, RealWorld, mkWeak#
+                )
+
+primop :: forall (l :: Levity) (a :: TYPE ('BoxedRep l)) b c.
+          a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
+       -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+primop = mkWeak#
diff --git a/testsuite/tests/rep-poly/T17817.stderr b/testsuite/tests/rep-poly/T17817.stderr
new file mode 100644
index 0000000000..84eed10838
--- /dev/null
+++ b/testsuite/tests/rep-poly/T17817.stderr
@@ -0,0 +1,8 @@
+
+T17817.hs:16:10: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The first argument of ‘mkWeak#’
+      does not have a fixed runtime representation:
+        a :: TYPE ('BoxedRep l)
+    • In the expression: mkWeak#
+      In an equation for ‘primop’: primop = mkWeak#
diff --git a/testsuite/tests/rep-poly/T18170a.hs b/testsuite/tests/rep-poly/T18170a.hs
new file mode 100644
index 0000000000..567dce7c01
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18170a.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T18170a where
+
+import Language.Haskell.TH.Lib
+
+import T18170c
+
+import Data.Proxy
+import GHC.Exts
+import GHC.Types
+
+
+-- Generating a monomorphic program is sound, and hence a workaround for
+-- normal representation polymorphic restrictions.
+
+workaround1 :: Int
+workaround1 = $$repPolyApp id 5
+
+workaround2 :: () -> Int#
+workaround2 _ = $$repPolyApp ( \ (x :: Int#) -> x +# 6# ) 11#
diff --git a/testsuite/tests/rep-poly/T18170b.hs b/testsuite/tests/rep-poly/T18170b.hs
new file mode 100644
index 0000000000..d215532a11
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18170b.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T18170b where
+
+import Language.Haskell.TH.Lib
+
+import T18170c
+
+import GHC.Exts
+import GHC.Types
+
+-- Representation-polymorphic function application: should be rejected.
+unsound :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2)
+        . (a -> b) -> a -> b
+unsound = $$repPolyApp
diff --git a/testsuite/tests/rep-poly/T18170c.hs b/testsuite/tests/rep-poly/T18170c.hs
new file mode 100644
index 0000000000..8927ea17df
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18170c.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T18170c where
+
+import Language.Haskell.TH.Lib
+
+import GHC.Exts
+import GHC.Types
+
+import Unsafe.Coerce
+
+-- Representation-polymorphism should be allowed here
+-- as long as 'r1' is monomorphised at splice site.
+repPolyApp
+  :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2)
+  . CodeQ ( (a -> b) -> a -> b )
+repPolyApp = [|| \ f x -> f x ||]
+
diff --git a/testsuite/tests/rep-poly/T18481.hs b/testsuite/tests/rep-poly/T18481.hs
new file mode 100644
index 0000000000..8cf8362899
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18481.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+module Bug where
+
+import GHC.Exts
+
+type Id :: TYPE r -> TYPE r
+newtype Id a where
+  MkId :: forall r (a :: TYPE r). a -> Id a
+
+idBool :: Id Bool
+idBool = MkId @LiftedRep @Bool True
diff --git a/testsuite/tests/rep-poly/T18481a.hs b/testsuite/tests/rep-poly/T18481a.hs
new file mode 100644
index 0000000000..b5b29a8af7
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18481a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UnliftedDatatypes, PolyKinds, DataKinds, TypeApplications #-}
+
+module T18481a where
+
+import Data.Kind
+import GHC.Types( Levity(..), RuntimeRep(..), TYPE )
+
+type T :: TYPE (BoxedRep r) -> TYPE (BoxedRep r)
+data T a = MkT Int
+
+f :: T Bool
+f = MkT @Lifted @Bool 42
diff --git a/testsuite/tests/rep-poly/T18534.hs b/testsuite/tests/rep-poly/T18534.hs
new file mode 100644
index 0000000000..7877ff47ee
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18534.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+
+module Test where
+
+import GHC.Exts
+
+data Test (a :: TYPE r) = Test !a
diff --git a/testsuite/tests/rep-poly/T18534.stderr b/testsuite/tests/rep-poly/T18534.stderr
new file mode 100644
index 0000000000..d56e696604
--- /dev/null
+++ b/testsuite/tests/rep-poly/T18534.stderr
@@ -0,0 +1,6 @@
+
+T18534.hs:7:27: error:
+    • The data constructor field does not have a fixed runtime representation:
+      • a :: TYPE r
+    • In the definition of data constructor ‘Test’
+      In the data type declaration for ‘Test’
diff --git a/testsuite/tests/rep-poly/T19615.hs b/testsuite/tests/rep-poly/T19615.hs
new file mode 100644
index 0000000000..8d71ca925e
--- /dev/null
+++ b/testsuite/tests/rep-poly/T19615.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes     #-}
+{-# LANGUAGE PolyKinds      #-}
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE TypeFamilies #-}
+module T19615 where
+
+import GHC.Exts
+
+class Call (r :: RuntimeRep) where
+  type Lev (a :: TYPE r)
+  lift' :: (a :: TYPE r) -> (Lev a -> b) -> b
+  mapF  :: forall r' (a :: TYPE r) (b :: TYPE r'). Call r' => (a -> b) -> Lev a -> Lev b
+
+instance Call LiftedRep where
+  type Lev a = a
+  lift' a k = k a
+  mapF f x = lift' (f x) id
diff --git a/testsuite/tests/rep-poly/T19615.stderr b/testsuite/tests/rep-poly/T19615.stderr
new file mode 100644
index 0000000000..e263dc7cd0
--- /dev/null
+++ b/testsuite/tests/rep-poly/T19615.stderr
@@ -0,0 +1,9 @@
+
+T19615.hs:17:20: error:
+    • The function argument
+        ‘(f x)’
+      does not have a fixed runtime representation:
+        b :: TYPE r'
+    • In the first argument of ‘lift'’, namely ‘(f x)’
+      In the expression: lift' (f x) id
+      In an equation for ‘mapF’: mapF f x = lift' (f x) id
diff --git a/testsuite/tests/rep-poly/T19709a.hs b/testsuite/tests/rep-poly/T19709a.hs
new file mode 100644
index 0000000000..8c0e5fd665
--- /dev/null
+++ b/testsuite/tests/rep-poly/T19709a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TemplateHaskell, ExplicitForAll, PolyKinds #-}
+
+module T19709a where
+
+import GHC.Exts
+
+$( let levid :: forall (r :: RuntimeRep) (a :: TYPE r). a -> a
+       levid x = x
+   in return [] )
diff --git a/testsuite/tests/rep-poly/T19709a.stderr b/testsuite/tests/rep-poly/T19709a.stderr
new file mode 100644
index 0000000000..b4d0cce931
--- /dev/null
+++ b/testsuite/tests/rep-poly/T19709a.stderr
@@ -0,0 +1,10 @@
+
+T19709a.hs:8:8: error:
+    • The type of the first pattern in the equation for ‘levid’
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression:
+        let
+          levid :: forall (r :: RuntimeRep) (a :: TYPE r). a -> a
+          levid x = x
+        in return []
diff --git a/testsuite/tests/rep-poly/T19709b.hs b/testsuite/tests/rep-poly/T19709b.hs
new file mode 100644
index 0000000000..629172a892
--- /dev/null
+++ b/testsuite/tests/rep-poly/T19709b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TemplateHaskell, ExplicitForAll, PolyKinds, TypeApplications #-}
+
+module T19709b where
+
+import GHC.Exts
+import Language.Haskell.TH
+
+$( let levfun :: forall (r :: RuntimeRep) (a :: TYPE r). a -> ()
+       levfun = error "e1"  -- NB: this, so far, is OK: no representation-polymorphic binder
+
+   in levfun (error @Any "e2")  -- but this is very naughty: representation-polymorphic argument
+      `seq` return [] )
diff --git a/testsuite/tests/rep-poly/T19709b.stderr b/testsuite/tests/rep-poly/T19709b.stderr
new file mode 100644
index 0000000000..2f228c257a
--- /dev/null
+++ b/testsuite/tests/rep-poly/T19709b.stderr
@@ -0,0 +1,9 @@
+
+T19709b.hs:11:14: error:
+    • The function argument
+        ‘(error @Any "e2")’
+      does not have a fixed runtime representation:
+        a0 :: TYPE Any
+    • In the first argument of ‘levfun’, namely ‘(error @Any "e2")’
+      In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’
+      In the expression: levfun (error @Any "e2") `seq` return []
diff --git a/testsuite/tests/rep-poly/T20113.hs b/testsuite/tests/rep-poly/T20113.hs
new file mode 100644
index 0000000000..da01589dfb
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20113.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE PolyKinds, UnliftedNewtypes, NoFieldSelectors #-}
+import GHC.Exts
+
+newtype Y (a :: TYPE rep) = MkY { y_fld :: a }
diff --git a/testsuite/tests/rep-poly/T20113.stderr b/testsuite/tests/rep-poly/T20113.stderr
new file mode 100644
index 0000000000..4ea6546309
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20113.stderr
@@ -0,0 +1,5 @@
+
+T20113.hs:4:35: error:
+    The type of the first pattern in the equation for ‘$sel:y_fld:MkY’
+    does not have a fixed runtime representation:
+      Y a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/T20277.hs b/testsuite/tests/rep-poly/T20277.hs
new file mode 100644
index 0000000000..539332bee7
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20277.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module T20277 where
+
+import GHC.Exts
+
+-- This one crucially must cause an error,
+-- even though there are no representation-polymorphic values.
+-- See GHC ticket #20277.
+baz :: forall (rep :: RuntimeRep) (a :: TYPE rep). () -> (# Int# | a #)
+baz _ = (# 17# | #)
diff --git a/testsuite/tests/rep-poly/T20277.stderr b/testsuite/tests/rep-poly/T20277.stderr
new file mode 100644
index 0000000000..9445c55c79
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20277.stderr
@@ -0,0 +1,6 @@
+
+T20277.hs:14:9: error:
+    • The unboxed sum result type does not have a fixed runtime representation:
+        (# Int# | a #) :: TYPE ('SumRep '[ 'IntRep, rep])
+    • In the expression: (# 17# | #)
+      In an equation for ‘baz’: baz _ = (# 17# | #)
diff --git a/testsuite/tests/rep-poly/T20330a.hs b/testsuite/tests/rep-poly/T20330a.hs
new file mode 100644
index 0000000000..2e4fbfd9c8
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20330a.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module T20330 where
+
+import GHC.Exts
+
+ok1 :: forall (r :: RuntimeRep) (z :: TYPE r). z -> z
+ok1 = raise# (5 :: Int)
+
+ok2 = (raise# :: forall (r :: RuntimeRep) (z :: TYPE r). Int -> z -> z)
diff --git a/testsuite/tests/rep-poly/T20330b.hs b/testsuite/tests/rep-poly/T20330b.hs
new file mode 100644
index 0000000000..a77b2b43a9
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20330b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+
+module T20330b where
+
+import GHC.Exts
+
+foo :: forall w r (z :: TYPE r). w -> z -> z
+foo = raise# @w @(z -> z)
diff --git a/testsuite/tests/rep-poly/T20363.hs b/testsuite/tests/rep-poly/T20363.hs
new file mode 100644
index 0000000000..a28e483ffb
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20363.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T20363 where
+
+import GHC.Exts
+
+data Nat = Zero | Suc Nat
+
+type NestedTupleRep :: Nat -> RuntimeRep -> RuntimeRep
+type family NestedTupleRep n r where
+  NestedTupleRep Zero    r = TupleRep '[]
+  NestedTupleRep (Suc n) r = TupleRep '[ r, NestedTupleRep n r ]
+
+type NestedTuple
+        :: forall ( n :: Nat )
+        -> forall ( r :: RuntimeRep )
+        .  forall ( a :: TYPE r )
+        -> TYPE ( NestedTupleRep n r )
+type family NestedTuple n a where
+  NestedTuple Zero    @r a = (# #)
+  NestedTuple (Suc n) @r a = (# a, NestedTuple n @r a #)
+
+type NestedTupleNT
+        :: forall ( n :: Nat )
+        -> forall ( r :: RuntimeRep )
+        .  forall ( a :: TYPE r )
+        -> TYPE ( NestedTupleRep n r )
+newtype NestedTupleNT n (a :: TYPE r) = MkNT ( NestedTuple n a )
+
+test1a :: NestedTuple Zero Addr# -> Int
+test1a (# #) = 0
+
+test2a :: NestedTuple (Suc Zero) Addr# -> Addr#
+test2a (# i, (# #) #) = i
+
+test1b :: NestedTupleNT Zero Addr# -> Int
+test1b ( MkNT (# #) ) = 0
+
+test2b :: NestedTupleNT (Suc Zero) Addr# -> Addr#
+test2b ( MkNT (# i, (# #) #) ) = i
diff --git a/testsuite/tests/rep-poly/T20363b.hs b/testsuite/tests/rep-poly/T20363b.hs
new file mode 100644
index 0000000000..52158cbe13
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20363b.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T20363b where
+
+import GHC.Exts
+
+data Nat = Zero | Suc Nat
+
+type NestedTupleRep :: Nat -> RuntimeRep -> RuntimeRep
+type family NestedTupleRep n r where
+  NestedTupleRep Zero    r = TupleRep '[]
+  NestedTupleRep (Suc n) r = TupleRep '[ r, NestedTupleRep n r ]
+
+type NestedTuple
+        :: forall ( n :: Nat )
+        -> forall ( r :: RuntimeRep )
+        .  forall ( a :: TYPE r )
+        -> TYPE ( NestedTupleRep n r )
+type family NestedTuple n a where
+  NestedTuple Zero    @r a = (# #)
+  NestedTuple (Suc n) @r a = (# a, NestedTuple n @r a #)
+
+type NestedTupleNT
+        :: forall ( n :: Nat )
+        -> forall ( r :: RuntimeRep )
+        .  forall ( a :: TYPE r )
+        -> TYPE ( NestedTupleRep n r )
+newtype NestedTupleNT n (a :: TYPE r) = MkNT ( NestedTuple n a )
+
+test1a :: NestedTuple Zero Addr# -> Int
+test1a (# #) = 0
+
+test2a :: NestedTuple (Suc Zero) Addr# -> Addr#
+test2a (# i, (# #) #) = i
+
+test1b :: NestedTupleNT Zero Addr# -> Int
+test1b ( MkNT (# #) ) = 0
+
+test2b :: NestedTupleNT (Suc Zero) Addr# -> Addr#
+test2b ( MkNT (# i, (# #) #) ) = i
+
+test1c :: Int
+test1c = test1b ( MkNT (# #) )
+
+test2c :: () -> Addr#
+test2c _ = test1b ( MkNT (# nullAddr#, (# #) #) )
diff --git a/testsuite/tests/rep-poly/T20423.hs b/testsuite/tests/rep-poly/T20423.hs
new file mode 100644
index 0000000000..da1a1602a3
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20423.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE StandaloneKindSignatures, MagicHash, ExplicitForAll, PolyKinds,
+             DataKinds, UnliftedDatatypes, PatternSynonyms #-}
+
+module T20423 where
+
+import GHC.Exts
+
+type LPInt :: forall (l :: Levity) -> TYPE (BoxedRep l)
+data LPInt l = MkI Int#
+
+pattern MkIPS :: Int# -> LPInt lev
+pattern MkIPS n = MkI n
diff --git a/testsuite/tests/rep-poly/T20423.stderr b/testsuite/tests/rep-poly/T20423.stderr
new file mode 100644
index 0000000000..521538788e
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20423.stderr
@@ -0,0 +1,4 @@
+
+T20423.hs:11:1: error:
+    The pattern synonym scrutinee does not have a fixed runtime representation:
+    • LPInt lev :: TYPE ('BoxedRep lev)
diff --git a/testsuite/tests/rep-poly/T20423b.hs b/testsuite/tests/rep-poly/T20423b.hs
new file mode 100644
index 0000000000..9918093b66
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20423b.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE StandaloneKindSignatures, MagicHash, ExplicitForAll, PolyKinds,
+             DataKinds, UnliftedDatatypes, PatternSynonyms, ViewPatterns,
+             GADTs #-}
+
+module T20423b where
+
+import GHC.Exts
+
+type LPGADT :: forall (l :: Levity) -> TYPE (BoxedRep l)
+data LPGADT l where
+  MkLifted   :: Int  -> LPGADT Lifted
+  MkUnlifted :: Int# -> LPGADT Unlifted
+
+getInt# :: LPGADT l -> Int#
+getInt# = undefined
+
+pattern MkIPS :: Int# -> LPGADT l
+pattern MkIPS i# <- ( getInt# -> i# )
diff --git a/testsuite/tests/rep-poly/T20423b.stderr b/testsuite/tests/rep-poly/T20423b.stderr
new file mode 100644
index 0000000000..18ada55c38
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20423b.stderr
@@ -0,0 +1,4 @@
+
+T20423b.hs:17:1: error:
+    The pattern synonym scrutinee does not have a fixed runtime representation:
+    • LPGADT l :: TYPE ('BoxedRep l)
diff --git a/testsuite/tests/rep-poly/T20426.hs b/testsuite/tests/rep-poly/T20426.hs
new file mode 100644
index 0000000000..c3227f0a82
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20426.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE StandaloneKindSignatures, MagicHash, ExplicitForAll, PolyKinds,
+             DataKinds, UnliftedDatatypes, PatternSynonyms, ViewPatterns,
+             GADTs #-}
+
+module T20426 where
+
+import GHC.Exts
+
+type LPGADT :: forall (l :: Levity) -> TYPE (BoxedRep l)
+data LPGADT l where
+  MkLifted   :: Int  -> LPGADT Lifted
+  MkUnlifted :: Int# -> LPGADT Unlifted
+
+getInt# :: LPGADT l -> Int#
+getInt# (MkLifted (I# i#)) = i#
+getInt# (MkUnlifted i#)    = i#
diff --git a/testsuite/tests/rep-poly/T20426.stderr b/testsuite/tests/rep-poly/T20426.stderr
new file mode 100644
index 0000000000..d6ef0f272f
--- /dev/null
+++ b/testsuite/tests/rep-poly/T20426.stderr
@@ -0,0 +1,5 @@
+
+T20426.hs:15:1: error:
+    The type of the first pattern in the equation for ‘getInt#’
+    does not have a fixed runtime representation:
+      LPGADT l :: TYPE ('BoxedRep l)
diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.hs b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.hs
new file mode 100644
index 0000000000..f5fd1092ca
--- /dev/null
+++ b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module Goof where
+
+import GHC.Exts (coerce)
+import GHC.Types (RuntimeRep,TYPE,Coercible)
+
+goof :: forall (rep :: RuntimeRep) (x :: TYPE rep) (y :: TYPE rep).
+  Coercible x y => x -> y
+goof = coerce
diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
new file mode 100644
index 0000000000..344ef39328
--- /dev/null
+++ b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
@@ -0,0 +1,8 @@
+
+UnliftedNewtypesCoerceFail.hs:15:8: error:
+    • Unsaturated use of a representation-polymorphic primitive function.
+      The first argument of ‘coerce’
+      does not have a fixed runtime representation:
+        x :: TYPE rep
+    • In the expression: coerce
+      In an equation for ‘goof’: goof = coerce
diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.hs b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.hs
new file mode 100644
index 0000000000..f5d134e3b1
--- /dev/null
+++ b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+
+module UnliftedNewtypesLevityBinder where
+
+import GHC.Types (RuntimeRep,TYPE,Coercible)
+
+newtype Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+  IdentC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a
+
+bad :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a
+bad = IdentC
diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
new file mode 100644
index 0000000000..d4746f75c2
--- /dev/null
+++ b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
@@ -0,0 +1,7 @@
+
+UnliftedNewtypesLevityBinder.hs:16:7: error:
+    • The newtype constructor argument
+      does not have a fixed runtime representation:
+        a :: TYPE r
+    • In the expression: IdentC
+      In an equation for ‘bad’: bad = IdentC
diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T
new file mode 100644
index 0000000000..51038a56e8
--- /dev/null
+++ b/testsuite/tests/rep-poly/all.T
@@ -0,0 +1,83 @@
+
+test('T11473', normal, compile_fail, [''])
+test('T11724', normal, compile_fail, [''])
+test('T12709', normal, compile_fail, [''])
+test('T12973', normal, compile_fail, [''])
+test('T13105', expect_broken(17201), compile, [''])
+test('T13233', normal, compile_fail, [''])
+test('T13929', normal, compile_fail, [''])
+test('T14561', normal, compile_fail, [''])
+test('T14561b', normal, compile_fail, [''])
+test('T14765', normal, compile_fail, [''])
+test('T17021', expect_broken(17201), compile, [''])
+test('T17360', normal, compile_fail, [''])
+test('T17536', expect_broken(17536), compile, [''])
+test('T17536b', expect_broken(17201), compile, [''])
+test('T17817', normal, compile_fail, [''])
+test('T18170a', [extra_files(['T18170c.hs'])], multimod_compile, ['T18170a.hs', '-v0'])
+test('T18170b', [extra_files(['T18170c.hs']), expect_broken(19893)], multimod_compile_fail, ['T18170b.hs', '-v0'])
+# T18170b isn't actually broken, but it causes a Core Lint error
+# even though the program is (correctly) rejected by the typechecker
+test('T18481', normal, compile, [''])
+test('T18481a', normal, compile, [''])
+test('T18534', normal, compile_fail, [''])
+test('T19615', normal, compile_fail, [''])
+test('T19709a', normal, compile_fail, [''])
+test('T19709b', normal, compile_fail, [''])
+test('T20113', normal, compile_fail, [''])
+test('T20277', normal, compile_fail, [''])
+test('T20330a', normal, compile, [''])
+test('T20330b', normal, compile, [''])
+test('T20363', normal, compile, [''])
+test('T20363b', expect_broken(17201), compile, [''])
+test('T20423', normal, compile_fail, [''])
+test('T20423b', normal, compile_fail, [''])
+test('T20426', normal, compile_fail, [''])
+
+test('LevPolyLet', normal, compile_fail, [''])
+test('PandocArrowCmd', normal, compile, [''])
+test('RepPolyApp', normal, compile_fail, [''])
+test('RepPolyArrowCmd', normal, compile_fail, [''])
+test('RepPolyArrowFun', normal, compile_fail, [''])
+test('RepPolyBackpack1', normal, backpack_compile_fail, [''])
+test('RepPolyBackpack2', normal, backpack_run, [''])
+test('RepPolyBackpack3', normal, backpack_compile_fail, [''])
+test('RepPolyBackpack4', normal, backpack_run, [''])
+test('RepPolyBackpack5', normal, backpack_run, [''])
+test('RepPolyBinder', normal, compile_fail, [''])
+test('RepPolyClassMethod', normal, compile_fail, [''])
+test('RepPolyDeferred', normal, compile_fail, [''])
+test('RepPolyDoBind', normal, compile_fail, [''])
+test('RepPolyDoBody1', normal, compile_fail, [''])
+test('RepPolyDoBody2', normal, compile_fail, [''])
+test('RepPolyDoReturn', normal, compile, [''])
+test('RepPolyLeftSection1', normal, compile, [''])
+test('RepPolyLeftSection2', normal, compile_fail, [''])
+test('RepPolyMagic', normal, compile_fail, [''])
+test('RepPolyMatch', normal, compile_fail, [''])
+test('RepPolyMcBind', normal, compile_fail, [''])
+test('RepPolyMcBody', normal, compile_fail, [''])
+test('RepPolyMcGuard', normal, compile_fail, [''])
+test('RepPolyNewtypePat1', normal, compile_fail, [''])
+test('RepPolyNewtypePat2', normal, compile, [''])
+test('RepPolyNPlusK', normal, compile_fail, [''])
+test('RepPolyPatBind', normal, compile_fail, [''])
+test('RepPolyPatSynArg', normal, compile_fail, [''])
+test('RepPolyPatSynRes', normal, compile_fail, [''])
+test('RepPolyPatSynUnliftedNewtype', normal, compile_fail, [''])
+test('RepPolyRecordPattern', normal, compile_fail, [''])
+test('RepPolyRecordUpdate', normal, compile_fail, [''])
+test('RepPolyRightSection', normal, compile_fail, [''])
+test('RepPolyRule1', normal, compile_fail, [''])
+test('RepPolyRule2', normal, compile_fail, [''])
+test('RepPolyRule3', expect_broken(17201), compile, [''])
+test('RepPolySum', normal, compile_fail, [''])
+test('RepPolyTuple', normal, compile_fail, [''])
+test('RepPolyTupleSection', normal, compile_fail, [''])
+test('RepPolyUnboxedPatterns', normal, compile_fail, [''])
+test('RepPolyUnliftedDatatype', normal, compile, [''])
+test('RepPolyWildcardPattern', normal, compile_fail, [''])
+test('RepPolyWrappedVar', normal, compile_fail, [''])
+test('RepPolyWrappedVar2', normal, compile, [''])
+test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
+test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])