[GHC] #14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r)

#14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- [https://hackage.haskell.org/package/reflection-2.1.2/docs/Data- Reflection.html#v:give give] from the ''reflection'' library has the following type {{{#!hs give :: forall a r. a -> (Given a => r) -> r }}} but `flip give :: r -> a -> r`! This works with our own `Given`, `give` {{{ $ ghci -ignore-dot-ghci -XRankNTypes GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help Prelude> class Given a Prelude> give :: a -> (Given a => r) -> r; give = undefined Prelude> :t flip give flip give :: c -> a -> c Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14157 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
[https://hackage.haskell.org/package/reflection-2.1.2/docs/Data- Reflection.html#v:give give] from the ''reflection'' library has the following type
{{{#!hs give :: forall a r. a -> (Given a => r) -> r }}}
but `flip give :: r -> a -> r`!
This works with our own `Given`, `give`
{{{ $ ghci -ignore-dot-ghci -XRankNTypes GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help Prelude> class Given a Prelude> give :: a -> (Given a => r) -> r; give = undefined Prelude> :t flip give flip give :: c -> a -> c Prelude> }}}
New description: [https://hackage.haskell.org/package/reflection-2.1.2/docs/Data- Reflection.html#v:give give] from the ''reflection'' library has the following type {{{#!hs give :: forall a r. a -> (Given a => r) -> r }}} but `flip give :: r -> a -> r`! Same happens with our own `Given`, `give` {{{ $ ghci -ignore-dot-ghci -XRankNTypes GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help Prelude> class Given a Prelude> give :: a -> (Given a => r) -> r; give = undefined Prelude> :t flip give flip give :: c -> a -> c Prelude> }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14157#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) Comment: This isn't limited to `flip`, since you can also trigger similar behavior with a simple redefinition of `give`: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci λ> :set -XRankNTypes λ> class Given a λ> let give :: a -> (Given a => r) -> r; give = undefined λ> let f x y = give x y λ> :type +v f f :: a -> p -> p λ> :type f f :: a -> p -> p }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14157#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: RyanGlScott (removed) Comment: This looks like correct behavior to me. Presumably, you want `flip give :: (Given a => r) -> a -> r`, but getting that would require impredicativity. The results GHC provides seem in accordance with, e.g., [http://cs.brynmawr.edu/~rae/papers/2016/type-app/visible-type-app.pdf this paper]. It is similar with the definition of `f`. Presumably, you want `f` to have the same type as `give`, but that would require inferring a higher-rank type, something that GHC avoids. Do close if you agree with this analysis. Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14157#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14157#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14157: Flipping (give :: a -> (Given a => r) -> r) has type (r -> a -> r) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I was surprised to see the constraint vanish completely! There are clearly gaps in my understanding of the type system but the reasons given make sense, my deepest thanks to you both for taking the time to respond to my tickets -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14157#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC