#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This ''might'' also affect data families too, but maybe not, since you have to specify the kind in the data family declaration: {{{ $ /opt/ghc/head/bin/ghci GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help λ> :set -fprint-explicit-kinds -XTypeInType -XTypeApplications -XTypeFamilies λ> data family Fam (a :: k) λ> data instance Fam a = FamCon λ> famCon :: Fam a; famCon = FamCon λ> :t famCon famCon :: forall k (a :: k). Fam k a λ> :t famCon @Int famCon @Int :: Fam * Int λ> :t FamCon FamCon :: forall k (a :: k). Fam k a λ> :t FamCon @Int FamCon @Int :: Fam Int a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): `-XTypeInType` switches on a menagerie of extensions, including `-XPolyKinds`: {{{ $ /opt/ghc/head/bin/ghci GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help λ> :set -XTypeInType λ> :showi language base language is: Haskell2010 with the following modifiers: -XDataKinds -XNoDatatypeContexts -XExtendedDefaultRules -XKindSignatures -XNoMonomorphismRestriction -XNondecreasingIndentation -XPolyKinds -XTypeInType }}} `-XTypeApplications` enables some others, too: {{{ $ /opt/ghc/head/bin/ghci GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help λ> :set -XTypeApplications λ> :showi language base language is: Haskell2010 with the following modifiers: -XAllowAmbiguousTypes -XNoDatatypeContexts -XExtendedDefaultRules -XNoMonomorphismRestriction -XNondecreasingIndentation -XTypeApplications }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire * keywords: TypeInType => TypeApplications Comment: Yes, to comment:4. And there does seem to be a discrepancy between the handling of kinds in datatype/class declarations and functions. I have a guess as to why. I'll look into this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by kosmikus): I also noticed that {{{ $ ghci -XTypeInType -XTypeApplications -XScopedTypeVariables -fprint- explicit-foralls GHCi, version 7.11.20151229: http://www.haskell.org/ghc/ :? for help Prelude> data Prox a = Prox Prelude> prox1 :: forall a . Prox a; prox1 = Prox Prelude> prox2 :: forall (a :: k) . Prox a; prox2 = Prox Prelude> :t prox1 prox1 :: forall {k} (a :: k). Prox a Prelude> :t prox2 prox2 :: forall k (a :: k). Prox a }}} Is this difference in treatment deliberate? I would have expected that for `k` to be explicit, I'd have to write {{{ Prelude> prox3 :: forall k (a :: k). Prox a; prox3 = Prox }}} Is there a way to mention a type/kind variable but to still make it implicit? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Old description:

Originally reported [https://mail.haskell.org/pipermail/ghc- devs/2016-January/010915.html here]. When applying types via `-XTypeApplications`, the type/kind that gets instantiated seems to be different depending on whether you're using functions, datatypes, or typeclasses.

Here's an example contrasting functions and datatypes:

{{{ $ /opt/ghc/head/bin/ghci GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help λ> :set -fprint-explicit-kinds -XTypeApplications -XTypeInType λ> data Prox a = Prox λ> prox :: Prox a; prox = Prox λ> :t prox prox :: forall k (a :: k). Prox k a λ> :t prox @Int prox @Int :: Prox * Int λ> :t Prox Prox :: forall k (a :: k). Prox k a λ> :t Prox @Int Prox @Int :: Prox Int a }}}

This is the core of the problem: with a function, `Int` seems to be applied to type variable `a`, whereas with data types, `Int` appears to be applied to the kind variable `k`. This confuses me, since `k` wasn't specified anywhere in the definition of `Prox`.

Andres Löh also [https://mail.haskell.org/pipermail/ghc- devs/2016-January/010916.html observed] a similar discrepancy between functions and typeclasses:

{{{ λ> :set -XScopedTypeVariables λ> class C a where c :: () λ> d :: forall a. C a => (); d = c @_ @a λ> :t d d :: forall k (a :: k). C k a => () λ> :t d @Int d @Int :: C * Int => () λ> :t c c :: forall k (a :: k). C k a => () λ> :t c @Int c @Int :: C Int a => () λ> :t c @_ @Int c @_ @Int :: C * Int => () }}}

New description: Originally reported [https://mail.haskell.org/pipermail/ghc- devs/2016-January/010915.html here]. When applying types via `-XTypeApplications`, the type/kind that gets instantiated seems to be different depending on whether you're using functions, datatypes, or typeclasses. Here's an example contrasting functions and datatypes: {{{ $ /opt/ghc/head/bin/ghci GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help λ> :set -fprint-explicit-kinds -XTypeApplications -XTypeInType λ> data Prox a = Prox λ> prox :: Prox a; prox = Prox λ> :t prox prox :: forall k (a :: k). Prox k a λ> :t prox @Int prox @Int :: Prox * Int λ> :t Prox Prox :: forall k (a :: k). Prox k a λ> :t Prox @Int Prox @Int :: Prox Int a }}} This is the core of the problem: with a function, `Int` seems to be applied to type variable `a`, whereas with data types, `Int` appears to be applied to the kind variable `k`. This confuses me, since `k` wasn't specified anywhere in the definition of `Prox`. Andres Löh also [https://mail.haskell.org/pipermail/ghc- devs/2016-January/010916.html observed] a similar discrepancy between functions and typeclasses: {{{ λ> :set -XScopedTypeVariables λ> class C a where c :: () λ> d :: forall a. C a => (); d = c @_ @a λ> :t d d :: forall k (a :: k). C k a => () λ> :t d @Int d @Int :: C * Int => () λ> :t c c :: forall k (a :: k). C k a => () λ> :t c @Int c @Int :: C Int a => () λ> :t c @_ @Int c @_ @Int :: C * Int => () }}} EDIT: See also documentation infelicity in comment:9. -- Comment (by goldfire): Replying to [comment:8 rwbarton]:

Based on experimentation, the rule seems to be: all type variables mentioned in the type signature are explicit, from left to right as they appear in the signature. I guess `k` counts as to the left of `a` in `a :: k`, though, since it is implicitly quantified earlier.

Here are the rules: * All variables mentioned by name are specified. * To get the ordering, list all the variables ordered left-to-right by first occurrence. Then do a stable topological sort based on dependencies. The second bullet is why `k` goes before `a` even though `a` is mentioned first. There is a note about this in the manual, but it doesn't discuss the topological sort part. Will fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Please merge the above commit to 8.0. Not setting "merge" status on the ticket because the bigger problem is not yet solved. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another troubling aspect of this that I discovered recently: GHC appears to quantify type variables in typeclass methods differently now. Compare this (GHC 7.10.3): {{{ $ /opt/ghc/7.10.3/bin/ghci -fprint-explicit-foralls GHCi, version 7.10.3: http://www.haskell.org/ghc/ :? for help λ> import GHC.Generics λ> :t datatypeName datatypeName :: forall d (t :: * -> (* -> *) -> * -> *) (f :: * -> *) a. Datatype d => t d f a -> [Char] }}} to this (GHC 8.0): {{{ $ /opt/ghc/8.0.1/bin/ghci -fprint-explicit-foralls GHCi, version 8.0.0.20160323: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci λ> import GHC.Generics λ> :t datatypeName datatypeName :: forall {k} (d :: k). Datatype d => forall {k1} (t :: k -> (* -> *) -> k1 -> *) (f :: * -> *) (a :: k1). t d f a -> [Char] }}} I'm not sure what's going on with the GHC 8.0-reported type signature at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I suppose the behavior is unchanged, but cosmetically, the type signature's appearance seems off, especially when combined with `-XTypeApplications`: {{{ $ /opt/ghc/8.0.1/bin/ghci GHCi, version 8.0.0.20160324: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci λ> :set -XTypeApplications -XDataKinds -fprint-explicit-foralls λ> import GHC.Generics λ> :t datatypeName @('MetaData "Void" "Data.Void" "base" 'False) datatypeName @('MetaData "Void" "Data.Void" "base" 'False) :: Datatype ('MetaData "Void" "Data.Void" "base" 'False) => forall {k1} (t :: Meta -> (* -> *) -> k1 -> *) (f :: * -> *) (a :: k1). t ('MetaData "Void" "Data.Void" "base" 'False) f a -> [Char] }}} 1. You would expect the context to go away once you apply `'MetaData "Void" "Data.Void" "base" 'False`. 2. You certainly wouldn't expect the context to appear //before// the list of quantified type variables. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): You're talking about `Note [Instantiate when inferring a type]` in !TcBinds. Yes. When we infer a type, we instantiate. The Note has the details, but this design makes it so that values with inferred types never have any variables available for type application. This is good. With `:type`, though, we don't want to instantiate, because doing so might change specified variables to invisible ones. Or in cases like `forall a. (a ~ Int) => ...`, instantiating and then solving will actually get rid of a variable. Instantiating ''when there are no more specified variables'' isn't ruinous, but I'm sure implementing the special case will cause confusion. Given that this is, essentially, a pretty-printing issue, maybe it should be controlled by `-fprint-explicit-foralls`? With the flag set, we never instantiate. Otherwise, we always instantiate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But this would lead to confusing behavior if there are any uninstantiated specified variables. If we did instantiation, then `:t f` would answer `Int -> Int -> Int`. That's reasonable enough, but then it's quite surprising when `:t f @Int` is accepted! In a somewhat similar scenario, say `bar :: forall a b. Show a => a -> b -> a`. What should `:t bar @Int` say? I offer 4 choices: 1. `forall b. Show Int => Int -> b -> Int` 2. `forall b. Int -> b -> Int` 3. `forall {b}. Int -> b -> Int` 4. `Int -> b -> Int` Here is how these could be produced: 1. This is what is currently done. No instantiation at `:type`. 2. This would require some new algorithm that instantiates a type and regeneralizes, being very careful to somehow notice when the instantiated variable arose from a specified variable and mark the re-generalized variable as specified. This becomes quite hard (both to implement and to specify) when equality constraints are in the mix and might combine a specified variable with an invisible one. 3. Instantiate and regeneralize. But now it looks like `bar @Int @Bool` should be rejected, even though it's actually OK. 4. Instantiate and do not regeneralize. Here, the user can't know that `bar @Int @Bool` is OK, but at least we're not suggesting that it should be rejected. As you can see, I prefer (1). It's conceivable to make a different choice when there are no top-level specified variables (so that a further type parameter would be an error), but I don't think we should. (Before arguing against me here, consider `quux :: forall a. Int -> forall b. Show a => b -> a -> Bool`. What should `:type quux @Int` say?) Another option I'd be happy with: Option (1) when `-fprint-explicit- foralls` is on, and option (3) when it's not. This might be surprising to users, but the benefits may outweigh the costs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Grumble. Option (3) gives me no way to see what the next type parameter should be if I've already written a handful. I suppose we could introduce a new GHCi command that doesn't instantiate. I do agree that choosing (3) will be less surprising to more users than my option (1). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Look in `TcRnDriver.tcRnExpr`. After the `tcInferSigma`, but still in the `pushLevelAndCaptureConstraints`, use `deeplyInstantiate` and `mkLHsWrap`. I'm afraid I can't conveniently test this right now, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"b3ecd047c432405b57b429fdeaad43f5dcd1ee24/ghc" b3ecd047/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b3ecd047c432405b57b429fdeaad43f5dcd1ee24" Elaborate test for #11376 This just adds the Prox stuff from the Description in Trac #11376 to the test case, The class stuff seems weird becuase the type is ambiguous }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): After more thought, I think this is a move in the wrong direction. The evidence I use to make my case is [https://phabricator.haskell.org/rGHCf2a2b79fa8d1c702b17e195a70734b06625e0153... this change]. Because of the change proposed (and implemented) here, GHC effectively erases information about specified vs. inferred variables before printing a type. One could argue that this information is recoverable with `:info`, but this is not easily true for data constructors, which print out their definition with `:info`, not their type. And, personally, when I want the type of a function, I just say `:type`, not `:info`, even when that expression is just a bare function. If (1) from comment:21 is considered abhorrent (and I admit it's unsavory), then I think we should strive for (2). Here is an attempt at a specification & implementation for (2): In `:type`, we do no type instantation, but we ''do'' try to solve constraints, by looking for any constraints in the type (even nested to the right of arrows), plucking them out of the type, and trying to solve them (by emitted wanteds and running the solver directly from `tcRnExpr`). Any unsolved constraints are then put back in the type, being careful to keep things well-scoped. Even after writing that, I don't like it at all. But with the patch as written, we're actively throwing away information that's hard to come by otherwise. == A new, crazy idea == Currently, GHCi stores the result of an evaluation in `it`. I propose storing the type of an evaluation (or call to `:type`) in `It` (so that `it :: It`). And then a new directive `:simplify` takes a type and simplifies it as much as possible, much like `simpliferInfer` does. So a user could say `:t length @[]`, get something with an unsolved `Foldable` constraint, and then just say `:simp It` and get what they want. We could even have `:type` try to simplify and report both types if they are different. I'm not suggesting this for 8.0, but I think it's a better plan than this patch, which I advocate reverting. Note: my comment:23 admission was thinking about the large mass of users that don't know about visible type application. But only those use visible type application will be bitten by the strange behavior! So I take back comment:23. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): What about for data constructors? Without your patch: {{{

:type Proxy Proxy :: forall {k} (t :: k). Proxy t }}}

This is now useful information that `k` is not specified but `t` is. With your patch (assumedly -- I don't have this locally): {{{

:type Proxy Proxy :: forall {k} {t :: k}. Proxy t }}}

I now don't know which is specified and which is generalized. So I could use `:info`: {{{

:info Proxy type role Proxy phantom data Proxy (t :: k) = Proxy -- Defined in ‘Data.Proxy’ instance forall k (s :: k). Bounded (Proxy s) -- Defined in ‘Data.Proxy’ instance forall k (s :: k). Enum (Proxy s) -- Defined in ‘Data.Proxy’ instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’ instance Monad Proxy -- Defined in ‘Data.Proxy’ instance Functor Proxy -- Defined in ‘Data.Proxy’ instance forall k (s :: k). Ord (Proxy s) -- Defined in ‘Data.Proxy’ instance forall k (s :: k). Read (Proxy s) -- Defined in ‘Data.Proxy’ instance forall k (s :: k). Show (Proxy s) -- Defined in ‘Data.Proxy’ instance Applicative Proxy -- Defined in ‘Data.Proxy’ instance Foldable Proxy -- Defined in ‘Data.Foldable’ instance Traversable Proxy -- Defined in ‘Data.Traversable’ instance forall k (s :: k). Monoid (Proxy s) -- Defined in ‘Data.Proxy’ }}}

There's an awful lot of information I have no interest in, and the very piece of information I do want -- the specificity of the variables -- is missing. It's missing because GHC helpfully says `data Proxy (t :: k) = ...` even though `Data.Proxy` declares `data Proxy t = ...`. The former would make `k` specified. But the latter, actual definition, means that `k` is not specified. I can exhibit the same problems with a class method. Take `Control.Category`'s `id`: Without your patch: {{{

:type C.id C.id :: forall {k} (cat :: k -> k -> *). Category cat => forall (a :: k). cat a a }}} Very helpful info.

With your patch (assumedly): {{{

:type C.id C.id :: forall {k} {a :: k} {cat :: k -> k -> *}. Category cat => cat a a }}} Here I decided to swap the order of `cat` and `a`, because it's quite conceivable that this would happen.

And now `:info`: {{{

:info C.id class Category (cat :: k -> k -> *) where Control.Category.id :: forall (a :: k). cat a a ... }}} Once again, I can't tell that `k` is unspecified. And even if I could somehow, I'd still have to do some work to reconstruct the type from this information.

I'm sure record selectors would have the same problem. Bottom line: I don't think Simon's proposal to use `:info` for bare names quite does it. I'm sympathetic to disliking (1) and I, too, desire to keep things simple. But I don't think we've quite figured this out yet. I actually think there's a really easy solution: have `:type` print ''both'' the uninstantiated type and the instantiated one (if they're different, by more than the ordering of invisible things). `tcRnExpr` could return two `Type`s -- it has both types we want to hand. We could even only do this new behavior when `-fprint-explicit-foralls` is enabled (because otherwise, the user isn't seeing specificity anyway). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Specificity is indeed specialized. However, the problematic output from `:type` that your patch fixes will happen only with visible type application. So, we're already focusing on a specialized audience. I could live with your last proposal -- that `:type <identifier>` is, essentially, a separate command from the normal `:type`. But how long will it be until someone posts a bug report complaining that `:t (blah)` is different from `:t blah`? This is the sort of "computer trying to be smart" behavior that I find so irritating in a variety of programs. It is indeed possible (and easy) to specify, but that specification will be buried in some bullet in the manual. What this all boils down to is that we really do need two commands: One that gives the raw, uninstantiated type; and one that tells us what type an identifier would be inferred to have if assigned to an expression. These are different, and both are useful! So maybe we should just introduce a new command. `:type` should clearly have the instantiated behavior, and the new one can be uninstantiated. I'm uninspired about the name of the new command. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => merge Comment: For 8.0.1 we will merge the commits in comment:26 and comment:27 and punt the rest for later. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: fixed | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"40db277f1dedd4df7e75cc0eb35aa7e1e1ded02a/ghc" 40db277f/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="40db277f1dedd4df7e75cc0eb35aa7e1e1ded02a" Fix `print-explicit-runtime-reps` (#11786). By fixing splitting of IfaceTypes in splitIfaceSigmaTy. Test Plan: make test TEST="T11549 T11376 T11786" Reviewers: goldfire, bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #11786, #11376 Differential Revision: https://phabricator.haskell.org/D4733 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11376#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler