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

[GHC]

#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