[GHC] #13595: Should ‘coerce’ be levity polymorphic?

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #13592 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => LevityPolymorphism Comment: 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree that this is a good idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): To make this work, don't we need the kind to express that values (lifted or not) are represented by pointers? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Re comment:3: Why? The `coerce` gets completely compiled away. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:4 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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, (##) #)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Agreed with comment:9. I suppose we could concoct that juice, but it's separate from this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13592 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/364 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/364 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13595#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC