Opened 4 years ago
Closed 2 years 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 4 years ago by
comment:2 Changed 4 years ago by
Cc: | goldfire added |
---|---|
Keywords: | TypeApplications added |
Version: | 8.1 → 8.0.1-rc1 |
comment:3 Changed 4 years ago by
Component: | Compiler → Compiler (Type checker) |
---|
comment:4 Changed 2 years ago by
Related Tickets: | → #11376 |
---|---|
Resolution: | → fixed |
Status: | new → 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). 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)
This error message can be improved, mention
TypeApplications
as a possible cause alone with monom.==@A
here is also not desirable.