Levity-polymorphism checker is too aggressive for uses of `coerce` on levity-polymorphic newtypes
GHC 8.10.1-alpha2 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 levity-polymorphic arguments:
coerce :: N a -> Unboxed a
Levity-polymorphic arguments: N a :: TYPE (UnboxedRep a)
|
22 | unN = coerce
| ^^^^^^
I think the program ought to be accepted. There are no levity-polymorphic 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
.