Make some simple primops levity-polymorphic

Fixes #17817

20 files changed, 191 insertions, 63 deletions

diff --git a/compiler/GHC/Builtin/PrimOps.hs b/compiler/GHC/Builtin/PrimOps.hs
index bbedb6f2c8..067f0e0d7c 100644
--- a/compiler/GHC/Builtin/PrimOps.hs
+++ b/compiler/GHC/Builtin/PrimOps.hs
@@ -109,14 +109,14 @@ data PrimOpInfo
   = Compare     OccName         -- string :: T -> T -> Int#
                 Type
   | GenPrimOp   OccName         -- string :: \/a1..an . T1 -> .. -> Tk -> T
-                [TyVar]
+                [TyVarBinder]
                 [Type]
                 Type
 
 mkCompare :: FastString -> Type -> PrimOpInfo
 mkCompare str ty = Compare (mkVarOccFS str) ty
 
-mkGenPrimOp :: FastString -> [TyVar] -> [Type] -> Type -> PrimOpInfo
+mkGenPrimOp :: FastString -> [TyVarBinder] -> [Type] -> Type -> PrimOpInfo
 mkGenPrimOp str tvs tys ty = GenPrimOp (mkVarOccFS str) tvs tys ty
 
 {-
@@ -607,7 +607,7 @@ primOpType op
     Compare _occ ty -> compare_fun_ty ty
 
     GenPrimOp _occ tyvars arg_tys res_ty ->
-        mkSpecForAllTys tyvars (mkVisFunTysMany arg_tys res_ty)
+        mkForAllTys tyvars (mkVisFunTysMany arg_tys res_ty)
 
 primOpResultType :: PrimOp -> Type
 primOpResultType op
@@ -722,7 +722,7 @@ isComparisonPrimOp op = case primOpInfo op of
 -- (type variables, argument types, result type)
 -- It also gives arity, strictness info
 
-primOpSig :: PrimOp -> ([TyVar], [Type], Type, Arity, DmdSig)
+primOpSig :: PrimOp -> ([TyVarBinder], [Type], Type, Arity, DmdSig)
 primOpSig op
   = (tyvars, arg_tys, res_ty, arity, primOpStrictness op arity)
   where
diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs
index e6f988e841..dd0c8f4a0b 100644
--- a/compiler/GHC/Builtin/Types.hs
+++ b/compiler/GHC/Builtin/Types.hs
@@ -114,7 +114,7 @@ module GHC.Builtin.Types (
         runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon,
 
         boxedRepDataConTyCon,
-        runtimeRepTy, liftedRepTy, unliftedRepTy,
+        runtimeRepTy, levityTy, liftedRepTy, unliftedRepTy,
 
         vecRepDataConTyCon, tupleRepDataConTyCon, sumRepDataConTyCon,
 
@@ -1478,8 +1478,9 @@ unrestrictedFunTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "->
 
 -- For information about the usage of the following type,
 -- see Note [TYPE and RuntimeRep] in module GHC.Builtin.Types.Prim
-runtimeRepTy :: Type
+runtimeRepTy, levityTy :: Type
 runtimeRepTy = mkTyConTy runtimeRepTyCon
+levityTy     = mkTyConTy levityTyCon
 
 -- Type synonyms; see Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim
 -- and Note [Prefer Type over TYPE 'LiftedRep] in GHC.Core.TyCo.Rep.
diff --git a/compiler/GHC/Builtin/Types.hs-boot b/compiler/GHC/Builtin/Types.hs-boot
index 1c341de418..e2b279d7ae 100644
--- a/compiler/GHC/Builtin/Types.hs-boot
+++ b/compiler/GHC/Builtin/Types.hs-boot
@@ -28,7 +28,7 @@ unliftedRepTyCon :: TyCon
 constraintKind :: Kind
 
 runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon :: TyCon
-runtimeRepTy :: Type
+runtimeRepTy, levityTy :: Type
 
 boxedRepDataConTyCon :: TyCon
 liftedDataConTyCon :: TyCon
diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs
index 45140e60f2..eaeda97f69 100644
--- a/compiler/GHC/Builtin/Types/Prim.hs
+++ b/compiler/GHC/Builtin/Types/Prim.hs
@@ -20,15 +20,21 @@ module GHC.Builtin.Types.Prim(
         mkTemplateAnonTyConBinders,
 
         alphaTyVars, alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar,
+        alphaTyVarSpec, betaTyVarSpec, gammaTyVarSpec, deltaTyVarSpec,
         alphaTys, alphaTy, betaTy, gammaTy, deltaTy,
         alphaTyVarsUnliftedRep, alphaTyVarUnliftedRep,
         alphaTysUnliftedRep, alphaTyUnliftedRep,
         runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep3TyVar,
+        runtimeRep1TyVarInf, runtimeRep2TyVarInf,
         runtimeRep1Ty, runtimeRep2Ty, runtimeRep3Ty,
+        levity1TyVar, levity1TyVarInf, levity1Ty,
 
         openAlphaTyVar, openBetaTyVar, openGammaTyVar,
+        openAlphaTyVarSpec, openBetaTyVarSpec, openGammaTyVarSpec,
         openAlphaTy, openBetaTy, openGammaTy,
 
+        levPolyTyVar1, levPolyTyVar1Spec, levPolyTy1,
+
         multiplicityTyVar1, multiplicityTyVar2,
 
         -- Kind constructors...
@@ -97,8 +103,8 @@ module GHC.Builtin.Types.Prim(
 import GHC.Prelude
 
 import {-# SOURCE #-} GHC.Builtin.Types
-  ( runtimeRepTy, unboxedTupleKind, liftedTypeKind
-  , vecRepDataConTyCon, tupleRepDataConTyCon
+  ( runtimeRepTy, levityTy, unboxedTupleKind, liftedTypeKind
+  , boxedRepDataConTyCon, vecRepDataConTyCon, tupleRepDataConTyCon
   , liftedRepTy, unliftedRepTy
   , intRepDataConTy
   , int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy
@@ -114,7 +120,8 @@ import {-# SOURCE #-} GHC.Builtin.Types
   , doubleElemRepDataConTy
   , mkPromotedListTy, multiplicityTy )
 
-import GHC.Types.Var    ( TyVar, mkTyVar )
+import GHC.Types.Var    ( TyVarBinder, TyVar
+                        , mkTyVar, mkTyVarBinder, mkTyVarBinders )
 import GHC.Types.Name
 import {-# SOURCE #-} GHC.Types.TyThing
 import GHC.Core.TyCon
@@ -127,7 +134,7 @@ import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Core.TyCo.Rep -- Doesn't need special access, but this is easier to avoid
                          -- import loops which show up if you import Type instead
-import {-# SOURCE #-} GHC.Core.Type ( mkTyConTy, tYPE )
+import {-# SOURCE #-} GHC.Core.Type ( mkTyConTy, mkTyConApp, tYPE )
 
 import Data.Char
 
@@ -360,6 +367,9 @@ alphaTyVars = mkTemplateTyVars $ repeat liftedTypeKind
 alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar :: TyVar
 (alphaTyVar:betaTyVar:gammaTyVar:deltaTyVar:_) = alphaTyVars
 
+alphaTyVarSpec, betaTyVarSpec, gammaTyVarSpec, deltaTyVarSpec :: TyVarBinder
+(alphaTyVarSpec:betaTyVarSpec:gammaTyVarSpec:deltaTyVarSpec:_) = mkTyVarBinders Specified alphaTyVars
+
 alphaTys :: [Type]
 alphaTys = mkTyVarTys alphaTyVars
 alphaTy, betaTy, gammaTy, deltaTy :: Type
@@ -380,11 +390,14 @@ runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep3TyVar :: TyVar
 (runtimeRep1TyVar : runtimeRep2TyVar : runtimeRep3TyVar : _)
   = drop 16 (mkTemplateTyVars (repeat runtimeRepTy))  -- selects 'q','r'
 
+runtimeRep1TyVarInf, runtimeRep2TyVarInf :: TyVarBinder
+runtimeRep1TyVarInf = mkTyVarBinder Inferred runtimeRep1TyVar
+runtimeRep2TyVarInf = mkTyVarBinder Inferred runtimeRep2TyVar
+
 runtimeRep1Ty, runtimeRep2Ty, runtimeRep3Ty :: Type
 runtimeRep1Ty = mkTyVarTy runtimeRep1TyVar
 runtimeRep2Ty = mkTyVarTy runtimeRep2TyVar
 runtimeRep3Ty = mkTyVarTy runtimeRep3TyVar
-
 openAlphaTyVar, openBetaTyVar, openGammaTyVar :: TyVar
 -- alpha :: TYPE r1
 -- beta  :: TYPE r2
@@ -392,11 +405,36 @@ openAlphaTyVar, openBetaTyVar, openGammaTyVar :: TyVar
 [openAlphaTyVar,openBetaTyVar,openGammaTyVar]
   = mkTemplateTyVars [tYPE runtimeRep1Ty, tYPE runtimeRep2Ty, tYPE runtimeRep3Ty]
 
+openAlphaTyVarSpec, openBetaTyVarSpec, openGammaTyVarSpec :: TyVarBinder
+openAlphaTyVarSpec = mkTyVarBinder Specified openAlphaTyVar
+openBetaTyVarSpec  = mkTyVarBinder Specified openBetaTyVar
+openGammaTyVarSpec = mkTyVarBinder Specified openGammaTyVar
+
 openAlphaTy, openBetaTy, openGammaTy :: Type
 openAlphaTy = mkTyVarTy openAlphaTyVar
 openBetaTy  = mkTyVarTy openBetaTyVar
 openGammaTy = mkTyVarTy openGammaTyVar
 
+levity1TyVar :: TyVar
+(levity1TyVar : _)
+  = drop 11 (mkTemplateTyVars (repeat levityTy)) -- selects 'l'
+
+levity1TyVarInf :: TyVarBinder
+levity1TyVarInf = mkTyVarBinder Inferred levity1TyVar
+
+levity1Ty :: Type
+levity1Ty = mkTyVarTy levity1TyVar
+
+levPolyTyVar1 :: TyVar
+[levPolyTyVar1] = mkTemplateTyVars [tYPE (mkTyConApp boxedRepDataConTyCon [levity1Ty])]
+-- tv :: TYPE ('BoxedRep l)
+
+levPolyTyVar1Spec :: TyVarBinder
+levPolyTyVar1Spec = mkTyVarBinder Specified levPolyTyVar1
+
+levPolyTy1 :: Type
+levPolyTy1 = mkTyVarTy levPolyTyVar1
+
 multiplicityTyVar1, multiplicityTyVar2  :: TyVar
 (multiplicityTyVar1 : multiplicityTyVar2 : _)
    = drop 13 (mkTemplateTyVars (repeat multiplicityTy))  -- selects 'n', 'm'
diff --git a/compiler/GHC/Builtin/primops.txt.pp b/compiler/GHC/Builtin/primops.txt.pp
index 3bddd10285..f56687c351 100644
--- a/compiler/GHC/Builtin/primops.txt.pp
+++ b/compiler/GHC/Builtin/primops.txt.pp
@@ -2463,8 +2463,9 @@ primop  CatchOp "catch#" GenPrimOp
    has_side_effects = True
 
 primop  RaiseOp "raise#" GenPrimOp
-   b -> o
-      -- NB: the type variable "o" is "a", but with OpenKind
+   a -> p
+      -- NB: "p" is the same as "b" except it is representation-polymorphic
+      -- (we shouldn't use "o" here as that would conflict with "a")
    with
    -- In contrast to 'raiseIO#', which throws a *precise* exception,
    -- exceptions thrown by 'raise#' are considered *imprecise*.
@@ -2831,10 +2832,10 @@ section "Weak pointers"
 
 primtype Weak# b
 
--- note that tyvar "o" denotes openAlphaTyVar
+-- Note: "v" denotes a levity-polymorphic type variable
 
 primop  MkWeakOp "mkWeak#" GenPrimOp
-   o -> b -> (State# RealWorld -> (# State# RealWorld, c #))
+   v -> b -> (State# RealWorld -> (# State# RealWorld, c #))
      -> State# RealWorld -> (# State# RealWorld, Weak# b #)
    { {\tt mkWeak# k v finalizer s} creates a weak reference to value {\tt k},
      with an associated reference to some value {\tt v}. If {\tt k} is still
@@ -2846,7 +2847,7 @@ primop  MkWeakOp "mkWeak#" GenPrimOp
    out_of_line      = True
 
 primop  MkWeakNoFinalizerOp "mkWeakNoFinalizer#" GenPrimOp
-   o -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+   v -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
    with
    has_side_effects = True
    out_of_line      = True
@@ -2883,7 +2884,7 @@ primop  FinalizeWeakOp "finalizeWeak#" GenPrimOp
    out_of_line      = True
 
 primop TouchOp "touch#" GenPrimOp
-   o -> State# RealWorld -> State# RealWorld
+   v -> State# RealWorld -> State# RealWorld
    with
    code_size = { 0 }
    has_side_effects = True
@@ -3131,8 +3132,10 @@ section "Controlling object lifetime"
 ------------------------------------------------------------------------
 
 -- See Note [keepAlive# magic] in GHC.CoreToStg.Prep.
+-- NB: "v" is the same as "a" except levity-polymorphic,
+-- and "p" is the same as "b" except representation-polymorphic
 primop KeepAliveOp "keepAlive#" GenPrimOp
-   o -> State# RealWorld -> (State# RealWorld -> p) -> p
+   v -> State# RealWorld -> (State# RealWorld -> p) -> p
    { \tt{keepAlive# x s k} keeps the value \tt{x} alive during the execution
      of the computation \tt{k}. }
    with
diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index b34c0fc8cb..d179c53ed3 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -1311,7 +1311,7 @@ mkPrimOpId prim_op
   = id
   where
     (tyvars,arg_tys,res_ty, arity, strict_sig) = primOpSig prim_op
-    ty   = mkSpecForAllTys tyvars (mkVisFunTysMany arg_tys res_ty)
+    ty   = mkForAllTys tyvars (mkVisFunTysMany arg_tys res_ty)
     name = mkWiredInName gHC_PRIM (primOpOcc prim_op)
                          (mkPrimOpIdUnique (primOpTag prim_op))
                          (AnId id) UserSyntax
diff --git a/docs/users_guide/9.4.1-notes.rst b/docs/users_guide/9.4.1-notes.rst
index 8d92d57eec..73901ad8be 100644
--- a/docs/users_guide/9.4.1-notes.rst
+++ b/docs/users_guide/9.4.1-notes.rst
@@ -21,3 +21,22 @@ Version 9.4.1
 
   Note that the explicit type applications are required, as the call to
   ``withDict`` would be ambiguous otherwise.
+
+``ghc-prim`` library
+~~~~~~~~~~~~~~~~~~~~
+
+- ``GHC.Exts.mkWeak#``, ``GHC.Exts.mkWeakNoFinalizer#``, ``GHC.Exts.touch#``
+  and ``GHC.Exts.keepAlive#`` are now levity-polymorphic instead of
+  representation-polymorphic. For instance: ::
+
+        mkWeakNoFinalizer#
+          :: forall {l :: Levity} (a :: TYPE (BoxedRep l)) (b :: Type)
+          .  a -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+
+  That is, the type signature now quantifies over a variable of type ``GHC.Exts.Levity``
+  instead of ``GHC.Exts.RuntimeRep``. In addition, this variable is now inferred,
+  instead of specified, meaning that it is no longer eligible for visible type application.
+
+- The ``GHC.Exts.RuntimeRep`` parameter to ``GHC.Exts.raise#`` is now inferred: ::
+
+        raise# :: forall (a :: Type) {r :: RuntimeRep} (b :: TYPE r). a -> b
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index 1ce61e2e61..122856346f 100644
--- a/libraries/ghc-prim/changelog.md
+++ b/libraries/ghc-prim/changelog.md
@@ -20,6 +20,26 @@
   Note that the explicit type applications are required, as the call to
   `withDict` would be ambiguous otherwise.
 
+- `mkWeak#`, `mkWeakNoFinalizer#`, `touch#` and `keepAlive#` are now
+  levity-polymorphic instead of representation-polymorphic. For instance:
+
+  ```
+  mkWeakNoFinalizer#
+    :: forall {l :: Levity} (a :: TYPE (BoxedRep l)) (b :: Type)
+    .  a -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+  ```
+
+  That is, the type signature now quantifies over a variable of type `Levity`
+  instead of `RuntimeRep`. In addition, this variable is now inferred,
+  instead of specified, meaning that it is no longer eligible for visible type application.
+
+- The `RuntimeRep` parameter to `raise#` is now inferred:
+
+  ```
+  raise# :: forall (a :: Type) {r :: RuntimeRep} (b :: TYPE r). a -> b
+  ```
+
+
 ## 0.8.0 (edit as necessary)
 
 - Change array access primops to use type with size maxing the element size:
diff --git a/testsuite/tests/codeGen/should_fail/T13233.hs b/testsuite/tests/codeGen/should_fail/T13233.hs
index f24fc03bfb..c4c0480a75 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.hs
+++ b/testsuite/tests/codeGen/should_fail/T13233.hs
@@ -5,7 +5,7 @@
 {-# LANGUAGE MagicHash #-}
 module Bug where
 
-import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
+import GHC.Exts ( TYPE, RuntimeRep )
 
 class Foo (a :: TYPE rep) where
   bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
@@ -20,8 +20,3 @@ obscure _ = ()
 
 quux :: ()
 quux = obscure (#,#)
-
-primop :: forall (rep :: RuntimeRep) (a :: TYPE rep) b c.
-          a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
-       -> State# RealWorld -> (# State# RealWorld, Weak# b #)
-primop = mkWeak#
diff --git a/testsuite/tests/codeGen/should_fail/T13233.stderr b/testsuite/tests/codeGen/should_fail/T13233.stderr
index 0208b2695a..2609e41d97 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233.stderr
@@ -18,15 +18,3 @@ T13233.hs:22:16: error:
     Levity-polymorphic arguments:
       a :: TYPE rep1
       b :: TYPE rep2
-
-T13233.hs:27:10: error:
-    Cannot use function with levity-polymorphic arguments:
-      mkWeak# :: a
-                 -> b
-                 -> (State# RealWorld -> (# State# RealWorld, c #))
-                 -> State# RealWorld
-                 -> (# State# RealWorld, Weak# b #)
-    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
-    are eta-expanded internally because they must occur fully saturated.
-    Use -fprint-typechecker-elaboration to display the full expression.)
-    Levity-polymorphic arguments: a :: TYPE rep
diff --git a/testsuite/tests/codeGen/should_fail/T13233_elab.hs b/testsuite/tests/codeGen/should_fail/T13233_elab.hs
index 8f62332af6..96adc5ff9a 100644
--- a/testsuite/tests/codeGen/should_fail/T13233_elab.hs
+++ b/testsuite/tests/codeGen/should_fail/T13233_elab.hs
@@ -8,7 +8,7 @@
 {-# LANGUAGE MagicHash #-}
 module Bug where
 
-import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
+import GHC.Exts ( TYPE, RuntimeRep )
 
 class Foo (a :: TYPE rep) where
   bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
@@ -23,11 +23,3 @@ obscure _ = ()
 
 quux :: ()
 quux = obscure (#,#)
-
--- It used to be that primops has no binding. However, as described in
--- Note [Primop wrappers] in GHC.Builtin.PrimOps we now rewrite unsaturated primop
--- applications to their wrapper, which allows safe use of levity polymorphism.
-primop :: forall (rep :: RuntimeRep) (a :: TYPE rep) b c.
-          a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
-       -> State# RealWorld -> (# State# RealWorld, Weak# b #)
-primop = mkWeak#
diff --git a/testsuite/tests/codeGen/should_fail/T13233_elab.stderr b/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
index ec9a04d726..1b84b9bf95 100644
--- a/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
@@ -12,13 +12,3 @@ T13233_elab.hs:25:16: error:
     Levity-polymorphic arguments:
       a :: TYPE rep1
       b :: TYPE rep2
-
-T13233_elab.hs:33:10: error:
-    Cannot use function with levity-polymorphic arguments:
-      mkWeak# @rep @a @b @c
-        :: a
-           -> b
-           -> (State# RealWorld -> (# State# RealWorld, c #))
-           -> State# RealWorld
-           -> (# State# RealWorld, Weak# b #)
-    Levity-polymorphic arguments: a :: TYPE rep
diff --git a/testsuite/tests/typecheck/should_compile/T17817b.hs b/testsuite/tests/typecheck/should_compile/T17817b.hs
new file mode 100644
index 0000000000..b4fac8ba87
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17817b.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+module Bug where
+
+import GHC.Exts ( Weak#, State#, RealWorld, mkWeak# )
+import GHC.Types ( UnliftedType )
+
+primop1 :: forall a b c.
+          a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
+       -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+primop1 = mkWeak# @a @b @c
+
+primop2 :: forall (a :: UnliftedType) b c.
+          a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
+       -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+primop2 = mkWeak# @a @b @c
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 7ebb9ae65c..8183fe06a7 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -789,3 +789,4 @@ test('T19742', normal, compile, [''])
 test('T18481', normal, compile, [''])
 test('T18481a', normal, compile, [''])
 test('T19775', normal, compile, [''])
+test('T17817b', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T17817.hs b/testsuite/tests/typecheck/should_fail/T17817.hs
new file mode 100644
index 0000000000..b87178f909
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/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/typecheck/should_fail/T17817.stderr b/testsuite/tests/typecheck/should_fail/T17817.stderr
new file mode 100644
index 0000000000..56753cb34b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17817.stderr
@@ -0,0 +1,13 @@
+
+T17817.hs:16:10: error:
+    Cannot use function with levity-polymorphic arguments:
+      mkWeak#
+        :: a
+           -> b
+           -> (State# RealWorld -> (# State# RealWorld, c #))
+           -> State# RealWorld
+           -> (# State# RealWorld, Weak# b #)
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
+    Levity-polymorphic arguments: a :: TYPE ('BoxedRep l)
diff --git a/testsuite/tests/typecheck/should_fail/T17817_elab.hs b/testsuite/tests/typecheck/should_fail/T17817_elab.hs
new file mode 100644
index 0000000000..7c0b09a98c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17817_elab.hs
@@ -0,0 +1,17 @@
+-- Same as T17817, but we compile with -fprint-typechecker-elaboration.
+{-# 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/typecheck/should_fail/T17817_elab.stderr b/testsuite/tests/typecheck/should_fail/T17817_elab.stderr
new file mode 100644
index 0000000000..aaa48448d2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17817_elab.stderr
@@ -0,0 +1,10 @@
+
+T17817_elab.hs:17:10: error:
+    Cannot use function with levity-polymorphic arguments:
+      mkWeak# @l @a @b @c
+        :: a
+           -> b
+           -> (State# RealWorld -> (# State# RealWorld, c #))
+           -> State# RealWorld
+           -> (# State# RealWorld, Weak# b #)
+    Levity-polymorphic arguments: a :: TYPE ('BoxedRep l)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 65f80a1e13..54af02c6f5 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -629,3 +629,5 @@ test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E4.hs', '-v0 -main-is foo'])
 test('T19415', normal, compile_fail, [''])
 test('T19615', normal, compile_fail, [''])
+test('T17817', normal, compile_fail, [''])
+test('T17817_elab', normal, compile_fail, ['-fprint-typechecker-elaboration'])
diff --git a/utils/genprimopcode/Main.hs b/utils/genprimopcode/Main.hs
index a0ea019923..f5eaf757e2 100644
--- a/utils/genprimopcode/Main.hs
+++ b/utils/genprimopcode/Main.hs
@@ -848,12 +848,13 @@ sl_name :: Entry -> String
 sl_name i = "(fsLit \"" ++ name i ++ "\") "
 
 ppTyVar :: String -> String
-ppTyVar "a" = "alphaTyVar"
-ppTyVar "b" = "betaTyVar"
-ppTyVar "c" = "gammaTyVar"
-ppTyVar "s" = "deltaTyVar"
-ppTyVar "o" = "runtimeRep1TyVar, openAlphaTyVar"
-ppTyVar "p" = "runtimeRep2TyVar, openBetaTyVar"
+ppTyVar "a" = "alphaTyVarSpec"
+ppTyVar "b" = "betaTyVarSpec"
+ppTyVar "c" = "gammaTyVarSpec"
+ppTyVar "s" = "deltaTyVarSpec"
+ppTyVar "o" = "runtimeRep1TyVarInf, openAlphaTyVarSpec"
+ppTyVar "p" = "runtimeRep2TyVarInf, openBetaTyVarSpec"
+ppTyVar "v" = "levity1TyVarInf, levPolyTyVar1Spec"
 ppTyVar _   = error "Unknown type var"
 
 ppType :: Ty -> String
@@ -888,6 +889,7 @@ ppType (TyVar "c")                      = "gammaTy"
 ppType (TyVar "s")                      = "deltaTy"
 ppType (TyVar "o")                      = "openAlphaTy"
 ppType (TyVar "p")                      = "openBetaTy"
+ppType (TyVar "v")                      = "levPolyTy1"
 
 ppType (TyApp (TyCon "State#") [x])             = "mkStatePrimTy " ++ ppType x
 ppType (TyApp (TyCon "MutVar#") [x,y])          = "mkMutVarPrimTy " ++ ppType x