Fix #16293 by cleaning up Proxy# infelicities

This bug fixes three problems related to `Proxy#`/`proxy#`:

1. Reifying it with TH claims that the `Proxy#` type constructor has
   two arguments, but that ought to be one for consistency with
   TH's treatment for other primitive type constructors like `(->)`.
   This was fixed by just returning the number of
   `tyConVisibleTyVars` instead of using `tyConArity` (which includes
   invisible arguments).
2. The role of `Proxy#`'s visible argument was hard-coded as nominal.
   Easily fixed by changing it to phantom.
3. The visibility of `proxy#`'s kind argument was specified, which
   is different from the `Proxy` constructor (which treats it as
   inferred). Some minor refactoring in `proxyHashId` fixed ths up.

   Along the way, I had to introduce a `mkSpecForAllTy` function, so
   I did some related Haddock cleanup in `Type`, where that function
   lives.

8 files changed, 64 insertions, 19 deletions

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 38af09234b..616454ff7e 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -1264,10 +1264,14 @@ proxyHashId
        (noCafIdInfo `setUnfoldingInfo` evaldUnfolding -- Note [evaldUnfoldings]
                     `setNeverLevPoly`  ty )
   where
-    -- proxy# :: forall k (a:k). Proxy# k a
-    bndrs   = mkTemplateKiTyVars [liftedTypeKind] id
-    [k,t]   = mkTyVarTys bndrs
-    ty      = mkSpecForAllTys bndrs (mkProxyPrimTy k t)
+    -- proxy# :: forall {k} (a:k). Proxy# k a
+    --
+    -- The visibility of the `k` binder is Inferred to match the type of the
+    -- Proxy data constructor (#16293).
+    [kv,tv] = mkTemplateKiTyVars [liftedTypeKind] id
+    kv_ty   = mkTyVarTy kv
+    tv_ty   = mkTyVarTy tv
+    ty      = mkInvForAllTy kv $ mkSpecForAllTy tv $ mkProxyPrimTy kv_ty tv_ty
 
 ------------------------------------------------
 unsafeCoerceId :: Id
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index 2a604ccc88..ddb1211e2e 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -855,9 +855,9 @@ mkProxyPrimTy :: Type -> Type -> Type
 mkProxyPrimTy k ty = TyConApp proxyPrimTyCon [k, ty]
 
 proxyPrimTyCon :: TyCon
-proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName binders res_kind [Nominal,Nominal]
+proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName binders res_kind [Nominal,Phantom]
   where
-     -- Kind: forall k. k -> Void#
+     -- Kind: forall k. k -> TYPE (Tuple '[])
      binders = mkTemplateTyConBinders [liftedTypeKind] id
      res_kind = unboxedTupleKind []
 
@@ -873,7 +873,7 @@ eqPrimTyCon :: TyCon  -- The representation type for equality predicates
                       -- See Note [The equality types story]
 eqPrimTyCon  = mkPrimTyCon eqPrimTyConName binders res_kind roles
   where
-    -- Kind :: forall k1 k2. k1 -> k2 -> Void#
+    -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (Tuple '[])
     binders  = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
     res_kind = unboxedTupleKind []
     roles    = [Nominal, Nominal, Nominal, Nominal]
@@ -884,7 +884,7 @@ eqPrimTyCon  = mkPrimTyCon eqPrimTyConName binders res_kind roles
 eqReprPrimTyCon :: TyCon   -- See Note [The equality types story]
 eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName binders res_kind roles
   where
-    -- Kind :: forall k1 k2. k1 -> k2 -> Void#
+    -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (Tuple '[])
     binders  = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
     res_kind = unboxedTupleKind []
     roles    = [Nominal, Nominal, Representational, Representational]
@@ -895,7 +895,7 @@ eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName binders res_kind roles
 eqPhantPrimTyCon :: TyCon
 eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName binders res_kind roles
   where
-    -- Kind :: forall k1 k2. k1 -> k2 -> Void#
+    -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (Tuple '[])
     binders  = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
     res_kind = unboxedTupleKind []
     roles    = [Nominal, Nominal, Phantom, Phantom]
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index c6e5740b35..846b50945a 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1490,7 +1490,8 @@ reifyTyCon tc
   = return (TH.PrimTyConI (reifyName tc) 2                False)
 
   | isPrimTyCon tc
-  = return (TH.PrimTyConI (reifyName tc) (tyConArity tc) (isUnliftedTyCon tc))
+  = return (TH.PrimTyConI (reifyName tc) (length (tyConVisibleTyVars tc))
+                          (isUnliftedTyCon tc))
 
   | isTypeFamilyTyCon tc
   = do { let tvs      = tyConTyVars tc
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index e0ceb24b06..142da4c79c 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -36,7 +36,8 @@ module Type (
         splitListTyConApp_maybe,
         repSplitTyConApp_maybe,
 
-        mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys,
+        mkForAllTy, mkForAllTys, mkTyCoInvForAllTys,
+        mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInvForAllTy, mkInvForAllTys,
         splitForAllTys, splitForAllVarBndrs,
@@ -1334,7 +1335,7 @@ interfaces.  Notably this plays a role in tcTySigs in TcBinds.hs.
                                 ~~~~~~~~
 -}
 
--- | Make a dependent forall over an Inferred variablem
+-- | Make a dependent forall over an 'Inferred' variable
 mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
 mkTyCoInvForAllTy tv ty
   | isCoVar tv
@@ -1343,13 +1344,13 @@ mkTyCoInvForAllTy tv ty
   | otherwise
   = ForAllTy (Bndr tv Inferred) ty
 
--- | Like mkTyCoInvForAllTy, but tv should be a tyvar
+-- | Like 'mkTyCoInvForAllTy', but tv should be a tyvar
 mkInvForAllTy :: TyVar -> Type -> Type
 mkInvForAllTy tv ty = ASSERT( isTyVar tv )
                       ForAllTy (Bndr tv Inferred) ty
 
--- | Like mkForAllTys, but assumes all variables are dependent and Inferred,
--- a common case
+-- | Like 'mkForAllTys', but assumes all variables are dependent and
+-- 'Inferred', a common case
 mkTyCoInvForAllTys :: [TyCoVar] -> Type -> Type
 mkTyCoInvForAllTys tvs ty = foldr mkTyCoInvForAllTy ty tvs
 
@@ -1357,12 +1358,17 @@ mkTyCoInvForAllTys tvs ty = foldr mkTyCoInvForAllTy ty tvs
 mkInvForAllTys :: [TyVar] -> Type -> Type
 mkInvForAllTys tvs ty = foldr mkInvForAllTy ty tvs
 
--- | Like mkForAllTys, but assumes all variables are dependent and Specified,
+-- | Like 'mkForAllTy', but assumes the variable is dependent and 'Specified',
 -- a common case
+mkSpecForAllTy :: TyVar -> Type -> Type
+mkSpecForAllTy tv ty = ASSERT( isTyVar tv )
+                       -- covar is always Inferred, so input should be tyvar
+                       ForAllTy (Bndr tv Specified) ty
+
+-- | Like 'mkForAllTys', but assumes all variables are dependent and
+-- 'Specified', a common case
 mkSpecForAllTys :: [TyVar] -> Type -> Type
-mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
-                      -- covar is always Inferred, so all inputs should be tyvar
-                      mkForAllTys [ Bndr tv Specified | tv <- tvs ]
+mkSpecForAllTys tvs ty = foldr mkSpecForAllTy ty tvs
 
 -- | Like mkForAllTys, but assumes all variables are dependent and visible
 mkVisForAllTys :: [TyVar] -> Type -> Type
diff --git a/testsuite/tests/primops/should_compile/T16293a.hs b/testsuite/tests/primops/should_compile/T16293a.hs
new file mode 100644
index 0000000000..69368c70b5
--- /dev/null
+++ b/testsuite/tests/primops/should_compile/T16293a.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+module T16293a where
+
+import Data.Coerce
+import Data.Proxy
+import GHC.Exts
+
+test1a :: () -> Proxy Int
+test1a _ = Proxy @Int
+
+test1b :: () -> Proxy# Int
+test1b _ = proxy# @Int
+
+test2a :: (() -> Proxy a) -> (() -> Proxy b)
+test2a = coerce
+
+test2b :: (() -> Proxy# a) -> (() -> Proxy# b)
+test2b = coerce
diff --git a/testsuite/tests/primops/should_compile/all.T b/testsuite/tests/primops/should_compile/all.T
index a934e4ca9e..aa7339c445 100644
--- a/testsuite/tests/primops/should_compile/all.T
+++ b/testsuite/tests/primops/should_compile/all.T
@@ -1 +1,2 @@
 test('T6135_should_compile', normal, compile, [''])
+test('T16293a', normal, compile, [''])
diff --git a/testsuite/tests/th/T16293b.hs b/testsuite/tests/th/T16293b.hs
new file mode 100644
index 0000000000..85affa5204
--- /dev/null
+++ b/testsuite/tests/th/T16293b.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TemplateHaskell #-}
+module T16293b where
+
+import Control.Monad
+import GHC.Exts
+import Language.Haskell.TH
+
+f :: ()
+f = $(do PrimTyConI _ arity _ <- reify ''Proxy#
+         unless (arity == 1) $
+           fail $ "Unexpected arity for Proxy#: " ++ show arity
+         [| () |])
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index a92cef42f1..2aaa48c127 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -464,3 +464,4 @@ test('T15471', normal, multimod_compile, ['T15471.hs', '-v0'])
 test('T16180', normal, compile_and_run, ['-package ghc'])
 test('T16183', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T16195', normal, multimod_compile, ['T16195.hs', '-v0'])
+test('T16293b', normal, compile, [''])