[GHC] #12085: Premature defaulting and variable not in scope
#12085: Premature defaulting and variable not in scope -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators, UnboxedTuples, UnicodeSyntax, ViewPatterns, QuasiQuotes, TypeInType, ApplicativeDo, TypeApplications, AllowAmbiguousTypes #-} import Data.Kind todo :: forall (a::Type). (Read a, Show a) => String todo = show @a (read @a "42") }}} there are two things I notice, even with `AllowAmbiguousTypes` the `a` gets defaulted prematurely {{{ $ ghci -ignore-dot-ghci -fwarn-type-defaults /tmp/tl0z.hs GHCi, version 8.0.0.20160511: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/tl0z.hs, interpreted ) Ok, modules loaded: Main. *Main> :t todo <interactive>:1:1: warning: [-Wtype-defaults] Defaulting the following constraints to type ‘()’ (Read a0) arising from a use of ‘it’ at <interactive>:1:1 (Show a0) arising from a use of ‘it’ at <interactive>:1:1 foo :: String *Main> }}} instead of something like `todo :: forall a. (Read a, Show a) => String`, it can be applied to types {{{ *Main> foo @Int "42" *Main> foo @Float "42.0" }}} ---- The second thing is that if you want to add an argument independent of `a` {{{#!hs -- ghci> foo @Int False -- "100" -- ghci> foo @Float True -- "42.0" foo :: forall (a::Type). (Read a, Show a) => Bool -> String foo b = show @a (read @a (if b then "42" else "100")) }}} I found no way to define it as {{{#!hs -- ghci> foo False @Int -- "100" -- ghci> foo True @Float -- "42.0" foo :: Bool -> forall (a::Type). (Read a, Show a) => String foo b = show @a (read @a (if b then "42" else "100")) }}} to which GHC persists {{{ $ ghci -ignore-dot-ghci -fwarn-type-defaults /tmp/tl0z.hs GHCi, version 8.0.0.20160511: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/tl0z.hs, interpreted ) /tmp/tl0z.hs:10:15: error: Not in scope: type variable ‘a’ /tmp/tl0z.hs:10:24: error: Not in scope: type variable ‘a’ Failed, modules loaded: none. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12085 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12085: Premature defaulting and variable not in scope -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): For the first part, `:type` instantiates, defaults, and re-generalises, because `:type <expr>` works on an arbitrary expression `<expr>`. You may want `:info`. See the extensive debate on #11376. So I think everything is behaving as designed there. (You may want to propose a design change.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12085#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12085: Premature defaulting and variable not in scope -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): For the second, a type signature brings into scope ''only'' the type variables in the ''leading'' or top-level `forall`. So in {{{ foo :: forall (a::Type). (Read a, Show a) => Bool -> String foo b = ...type variable 'a' is in scope here... }}} But for ''non-top-level'' foralls, nothing is brought into scope {{{ bar :: Bool -> forall (a::Type). (Read a, Show a) => Bool -> String bar b = ...type variable 'a' is NOT NOT in scope here... }}} This is again by design, and I think it's documented. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12085#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
So I think everything is behaving as designed there. (You may want to
#12085: Premature defaulting and variable not in scope -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Ah they are both by design, interesting! Replying to [comment:1 simonpj]: propose a design change.) If I were to propose one, it would look something like this: {{{ ghci> :type todo todo :: String ghci> :set -XAllowAmbiguousTypes ghci> :type todo todo :: forall a. (Read a, Show a) => String }}} I haven't read #11376 (as well as being out of my depth) so I defer to the judgment of GHC developers. ---- Replying to [comment:2 simonpj]:
For the second, a type signature brings into scope ''only'' the type variables in the ''leading'' or top-level `forall`. So in
I'm not familiar with the terminology, what is a ‘''leading''’ forall?
But for ''non-top-level'' foralls, nothing is brought into scope
`[…]`
This is again by design, and I think it's documented.
Searching for “''non-top-level'' foralls” only gives this thread, I guess there isn't a formal name for it. I found these references in the user guide
`[…]` it is possible to declare type arguments somewhere other than the beginning of a type” regarding `RankNTypes`.
That is, you can nest foralls arbitrarily deep in function arrows
The `-XRankNTypes` option is also required for any type with a forall or context to the right of an arrow (e.g. `f :: Int -> forall a. a->a`, or `g :: Int -> Ord a => a -> a`).
but I didn't find information about scoping. Is there a fundamental reason this couldn't work: {{{#!hs one :: forall a. Int -> ... one in_scope = {- ‘a’ is in scope -} two :: Int -> forall a. ... two not_in_scope = {- ‘a’ is in scope -} }}} This is not a feature I desperately need -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12085#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC