#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