Is it possible to write an alias for coerce?

Question

Let's say for the purposes of this question I want to make an alias of coerce. I start with the obvious

import Data.Coerce

q = coerce

a bit surprisingly this gives rise an error:

coerce.hs:3:5: error:
    • Couldn't match representation of type ‘a0’ with that of ‘b0’
        arising from a use of ‘coerce’
    • In the expression: coerce
      In an equation for ‘q’: q = coerce
    • Relevant bindings include q :: a0 -> b0 (bound at coerce.hs:4:1)
  |
4 | q = coerce
  |     ^^^^^^

This error is quite opaque so I slapped the type signature¹ of coerce onto q:

{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Coerce
import GHC.Exts

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = coerce

But this gives rise to the error:

coerce.hs:8:5: error:
    Cannot use function with levity-polymorphic arguments:
      coerce :: a -> b
    Levity-polymorphic arguments: a :: TYPE k
  |
8 | q = coerce
  |     ^^^^^^

This error is not very helpful. It informs me there is an issue with levity polymorphism and that is about it.

What is really quite curious to me is that when I make q bottom:

{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Coerce
import GHC.Exts

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = q

The error goes away and the code compiles fine.

I'm left unsure whether such an alias is possible, or what even the issue with the alias is.

Is such an alias possible where q maintains the type of coerce? What issue is the compiler running into with my code?

---

^{1: As pointed out by the comments this type signature only has levity polymorphism in since base-4.13 or ghc 8.8. For the purposes of this question we want the levity polymorphism.}

Answer 1

It doesn't look like this is possible, but you can get really close. Note: it may well be possible to shorten this.

blop
  :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) q r.
     Coercible a b
  => q :~: (a -> a)
  -> r :~: (a -> b)
  -> Coercion q r
blop Refl Refl = Coercion

bloverce
  :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) q r.
     Coercible a b
  => q :~: (a -> a)
  -> r :~: (a -> b)
  -> q -> r
bloverce qaa rab = case blop qaa rab of Coercion -> coerce

gloerce
  :: forall (r :: RuntimeRep).
     (forall (x :: TYPE r). x -> x) -> Coe r
gloerce kid = Coe (bloverce Refl Refl (kid :: a -> a) :: forall (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b)

newtype Coe (r :: RuntimeRep) = Coe (forall (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b)

As long as you can provide the polymorphic identity function for a certain runtime representation, you can use gloerce to get its coerce.

Of course, this is all fairly silly in practice: in the rare cases when you need a representation-polymorphic coercion function, you can just use coerce directly.

Answer 2

@dfeuer's answer covers a workaround, but I think issue #17670 explains why this is happening. Because coerce is a primop, it must be fully saturated, so any use is implicitly eta-expanded. When you write:

q = coerce

you're really writing:

q = \x -> coerce x

The initial error message you get is actually a result of the monomorphism restriction. If you write either:

q x = coerce x

or add the NoMonomorphismRestriction extension, the program is accepted. Unfortunately, the resulting q isn't levity polymorphic. It's instantiated with lifted types.

If try to force the issue by adding an appropriate polymorphic type signature:

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = coerce

then bleeding edge versions of GHC (e.g., "8.11" built from source last month) give an elaborated error message:

BadCoerce.hs:11:5: error:
    Cannot use function with levity-polymorphic arguments:
      coerce :: a -> 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 k

Ultimately, you're running up against the prohibition that no variable (in this case an implicit variable introduced to eta-expand coerce) is permitted to be levity polymorphic. The reason q = q works is that there's no eta expansion and so no variable involved. Try q x = q x and it will fail with "a levity-polymorphic type is not allowed here" error message.