#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