Levitypolymorphism checker is too aggressive for uses of `coerce` on levitypolymorphic newtypes
GHC 8.10.1alpha2 rejects this program:
{# LANGUAGE DataKinds, FlexibleContexts, MagicHash, PolyKinds, RankNTypes, StandaloneKindSignatures, TypeFamilies, UnliftedNewtypes #}
module M where
import Data.Coerce
import Data.Kind
import GHC.Exts (RuntimeRep(..), TYPE)
type UnboxedRep :: Type > RuntimeRep
type family UnboxedRep a
type Unboxed :: forall (a :: Type) > TYPE (UnboxedRep a)
type family Unboxed a
 The above definitions allow us to define, say
 type instance UnboxedRep Int = 'IntRep
 type instance Unboxed Int = Int#
 but those definitions are not necessary for this issue.
newtype N a = N (Unboxed a)
unN :: Coercible (N a) (Unboxed a) => N a > Unboxed a
unN = coerce
M.hs:22:7: error:
Cannot use function with levitypolymorphic arguments:
coerce :: N a > Unboxed a
Levitypolymorphic arguments: N a :: TYPE (UnboxedRep a)

22  unN = coerce
 ^^^^^^
I think the program ought to be accepted. There are no levitypolymorphic arguments here; surely the code generator has no trouble with unN
, which simply returns a function? Indeed, both of the following definitions are accepted:
f :: (N a > Unboxed a) > N a > Unboxed a
f = id
type C :: TYPE r1 > TYPE r2 > Constraint
class C a b where
m :: a > b
g :: C (N a) (Unboxed a) => N a > Unboxed a
g = m
Even more bizarre, the following instance of C
is accepted, too:
instance Coercible a b => C a b where
m = coerce
So I have no idea why unN
is rejected, but it seems like something funny is going on with coerce
.