Opened 21 months ago

Closed 5 months ago

#11333 closed bug (fixed)

GHCi does not discharge satisfied constraints

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: TypeApplications Cc: goldfire
Operating System: Linux Architecture: Unknown/Multiple
Type of failure: Other Test Case:
Blocked By: Blocking:
Related Tickets: #11376 Differential Rev(s):
Wiki Page:

Description

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?

Change History (4)

comment:1 Changed 21 months ago by Iceland_jack

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?

comment:2 Changed 21 months ago by thomie

Cc: goldfire added
Keywords: TypeApplications added
Version: 8.18.0.1-rc1

comment:3 Changed 20 months ago by thomie

Component: CompilerCompiler (Type checker)

comment:4 Changed 5 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

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)
Note: See TracTickets for help on using tickets.