[GHC] #11333: GHCi does not discharge satisfied constraints

#11333: GHCi does not discharge satisfied constraints ----------------------------------------+-------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Linux Architecture: Unknown/Multiple | Type of failure: Other Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: ----------------------------------------+-------------------------- Don't know if this is the intended behaviour (GHCi, version 8.1.20151231), with the new extension TypeApplications. For the function [https://hackage.haskell.org/package/base-4.8.1.0/docs /Text-Show.html#v:show show]: {{{#!hs Prelude> :set -XTypeApplications Prelude> :t show show :: Show a => a -> String Prelude> :t show @Int show @Int :: Show Int => Int -> String }}} And the function [https://hackage.haskell.org/package/base/docs/Data- Typeable.html#v:eqT eqT] (`:: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)`): {{{#!hs Prelude> :set -XTypeApplications Prelude> import Data.Typeable Prelude Data.Typeable> :t eqT eqT :: forall k1 (a :: k1) (b :: k1). (Typeable a, Typeable b) => Maybe (a :~: b) Prelude Data.Typeable> :t eqT eqT :: forall k1 (a :: k1) (b :: k1). (Typeable a, Typeable b) => Maybe (a :~: b) Prelude Data.Typeable> :t eqT @Int eqT @Int :: (Typeable Int, Typeable b) => Maybe (Int :~: b) }}} Should the types of `show @Int` and `eqT @Int` not be `Int -> String` and `(Typeable b) => Maybe (Int :~: b)` respectively? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11333 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11333: GHCi does not discharge satisfied constraints ---------------------------------+---------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Linux | Architecture: Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+---------------------------------------- Comment (by Iceland_jack): This error message can be improved, mention `TypeApplications` as a possible cause alone with monom. {{{#!hs Prelude> :set -XTypeApplications Prelude> data A Prelude> :t (==) @A (==) @A :: Eq A => A -> A -> Bool Prelude> a = (==) @A <interactive>:4:1: error: • No instance for (Eq A) arising from a use of ‘==’ • When instantiating ‘a’, initially inferred to have this overly-general type: Eq A => A -> A -> Bool NB: This instantiation can be caused by the monomorphism restriction. }}} `==@A` here is also not desirable. {{{#!hs % ghci -ignore-dot-ghci GHCi, version 8.1.20160102: http://www.haskell.org/ghc/ :? for help Prelude> data A Prelude> :t (==) @A <interactive>:1:1: error: Pattern syntax in expression context: ==@A Did you mean to enable TypeApplications? }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11333#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11333: GHCi does not discharge satisfied constraints ---------------------------------+---------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1-rc1 Resolution: | Keywords: TypeApplications Operating System: Linux | Architecture: Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+---------------------------------------- Changes (by thomie): * cc: goldfire (added) * keywords: => TypeApplications * version: 8.1 => 8.0.1-rc1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11333#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11333: GHCi does not discharge satisfied constraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: fixed | TypeApplications Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: #11376 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed * related: => #11376 Comment: This appears to be fixed, even as of GHC 8.0.1: {{{ $ /opt/ghc/8.0.1/bin/ghci GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> :set -XTypeApplications λ> :t show show :: Show a => a -> String λ> :t show @Int show @Int :: Int -> String λ> import Data.Typeable λ> :t eqT eqT :: (Typeable b, Typeable a) => Maybe (a :~: b) λ> :t eqT @Int eqT @Int :: Typeable b => Maybe (Int :~: b) }}} This is a consequence of making `:type` deeply instantiate types (#11376). If you want the behavior that is shown in the original example, you can use `:type +v` (in GHC 8.2 or later): {{{ $ /opt/ghc/8.2.1/bin/ghci GHCi, version 8.2.0.20170427: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> :set -XTypeApplications λ> :type +v show show :: Show a => a -> String λ> :type +v show @Int show @Int :: Show Int => Int -> String λ> import Data.Typeable λ> :type +v eqT eqT :: forall k (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) λ> :type +v eqT @Int eqT @Int :: (Typeable Int, Typeable b) => Maybe (Int :~: b) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11333#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC