Premature defaulting and variable not in scope

{-# 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

-- 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

-- 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> 

Trac metadata

Trac field	Value
Version	8.0.1
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Ttask Trac import TypeApplications labels

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 (closed).

So I think everything is behaving as designed there. (You may want to propose a design change.)

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.

Ah they are both by design, interesting!

Replying to [ticket:12085#comment:120510 simonpj]:

So I think everything is behaving as designed there. (You may want to 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 (closed) (as well as being out of my depth) so I defer to the judgment of GHC developers.

---

Replying to [ticket:12085#comment:120511 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:

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

added Pnormal label