Opened 2 years ago

Last modified 3 months ago

#13595 patch bug

Should ‘coerce’ be levity polymorphic?

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #13592 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/364
Wiki Page:

Description

I'm not able to write coerce @Int# @Int# or coerce :: Double# -> Double#, just checking to see if its intentional or not

>>> :set -XTypeApplications
>>> :set -XMagicHash

>>> import Data.Coerce
>>> import GHC.Exts

>>>> :t coerce @Int
coerce @Int :: Coercible b Int => Int -> b
>>> :t coerce @Int#

<interactive>:1:1: error:
    Couldn't match a lifted type with an unlifted type
    When matching types
      b :: *
      Int# :: TYPE 'IntRep

<interactive>:1:9: error:
    • Expecting a lifted type, but ‘Int#’ is unlifted
    • In the type ‘Int#’
      In the expression: coerce @Int#

This was needed for #13592.

Change History (12)

comment:1 Changed 2 years ago by simonpj

Keywords: LevityPolymorphism added

Yes, you are right: I think coerce (and similarly Coercible) should have type

coerce :: forall l (a::TYPE l) (b::Type l). a -> b

More realistically than your example, I think we might reasonably want

newtype Age = MkAge Int

f :: Array# Age -> Array# Int
f a = coerce a

comment:2 Changed 2 years ago by goldfire

I agree that this is a good idea.

comment:3 Changed 2 years ago by dfeuer

To make this work, don't we need the kind to express that values (lifted or not) are represented by pointers?

comment:4 Changed 2 years ago by goldfire

Re comment:3: Why? The coerce gets completely compiled away.

comment:5 in reply to:  4 Changed 2 years ago by dfeuer

Replying to goldfire:

Re comment:3: Why? The coerce gets completely compiled away.

Oh, is that guaranteed these days? Last I read about the mechanism I don't think it was.

comment:6 Changed 2 years ago by goldfire

I believe it is. There's no other implementation for coerce than no-op. What might not be compiled away is a call like map coerce, but we have RULES for that. Regardless, levity polymorphism does not complicate that story.

comment:7 Changed 2 years ago by nomeata

Source level coerce takes a boxed coercion and unboxes it before it is a no-op. In most cases, the compiler will optimize this unboxing away, but I am actually not sure what guarantees we have here.

comment:8 Changed 2 years ago by andrewthad

Another use-case I just stumbled across is the coercion of unboxed tuple types:

coerceTuple :: (# a, (# b, c #) #) -> (# a, b, c #)
coerceTuple = coerce

This does not currently work, but it would be nice if it did.

comment:9 Changed 2 years ago by RyanGlScott

The ability to write coerceTuple is an entirely separate matter, IIUC. You're asking for the Coercible solver to have extra knowledge about unboxed tuple representations that it's currently not privy to.

With levity polymorphic coerce you could go from (# Int #) to (# Age #), where Age is a newtype around Int. But you'd need some extra juice to go from (# Int #) to, say, (# Int, (##) #).

comment:10 Changed 2 years ago by goldfire

Agreed with comment:9. I suppose we could concoct that juice, but it's separate from this ticket.

comment:11 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/364
Status: newpatch

comment:12 Changed 3 months ago by Marge Bot <ben+marge-bot@…>

In effdd948/ghc:

Implement the -XUnliftedNewtypes extension.

GHC Proposal: 0013-unlifted-newtypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
Issues: #15219, #1311, #13595, #15883
Implementation Details:
  Note [Implementation of UnliftedNewtypes]
  Note [Unifying data family kinds]
  Note [Compulsory newtype unfolding]

This patch introduces the -XUnliftedNewtypes extension. When this
extension is enabled, GHC drops the restriction that the field in
a newtype must be of kind (TYPE 'LiftedRep). This allows types
like Int# and ByteArray# to be used in a newtype. Additionally,
coerce is made levity-polymorphic so that it can be used with
newtypes over unlifted types.

The bulk of the changes are in TcTyClsDecls.hs. With -XUnliftedNewtypes,
getInitialKind is more liberal, introducing a unification variable to
return the kind (TYPE r0) rather than just returning (TYPE 'LiftedRep).
When kind-checking a data constructor with kcConDecl, we attempt to
unify the kind of a newtype with the kind of its field's type. When
typechecking a data declaration with tcTyClDecl, we again perform a
unification. See the implementation note for more on this.

Co-authored-by: Richard Eisenberg <rae@richarde.dev>
Note: See TracTickets for help on using tickets.