GHCi does not discharge satisfied constraints

Don't know if this is the intended behaviour (GHCi, version 8.1.20151231), with the new extension TypeApplications.

For the function show:

Prelude> :set -XTypeApplications 
Prelude> :t show
show :: Show a => a -> String
Prelude> :t show @Int
show @Int :: Show Int => Int -> String

And the function eqT (:: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)):

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?

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

This error message can be improved, mention TypeApplications as a possible cause alone with monom.

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.

% 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?

Trac metadata

Trac field	Value
Version	8.1 → 8.0.1-rc1

added TypeApplications label

Trac metadata

Trac field	Value
Component	Compiler → Compiler (Type checker)

closed

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 (closed)). 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)

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Related	- → #11376 (closed)

added Pnormal label