Opened 16 months ago

Last modified 16 months ago

#12085 new task

Premature defaulting and variable not in scope

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (3)

comment:1 Changed 16 months ago 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.)

comment:2 Changed 16 months ago 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.

comment:3 in reply to:  2 Changed 16 months ago by Iceland_jack

Ah they are both by design, interesting!

Replying to 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 (as well as being out of my depth) so I defer to the judgment of GHC developers.


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

Note: See TracTickets for help on using tickets.