Opened 2 years ago

Closed 2 years ago

Last modified 2 years ago

#13060 closed bug (invalid)

Visible type application doesn't work for functions with inferred types

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

Description

GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/feuerbach/.ghci
Prelude> :set -XTypeApplications -fprint-explicit-kinds -fprint-explicit-foralls
Prelude> :t id
id :: forall {a}. a -> a
Prelude> :t id @Int
id @Int :: Int -> Int
Prelude> let foo :: a -> a; foo = id
Prelude> :t foo
foo :: forall {a}. a -> a
Prelude> :t foo @Int
foo @Int :: Int -> Int
Prelude> let bar = id
Prelude> :t bar
bar :: forall {a}. a -> a
Prelude> :t bar @Int

<interactive>:1:1: error:
    • Cannot apply expression of type ‘a0 -> a0’
      to a visible type argument ‘Int’
    • In the expression: bar @Int

Change History (3)

comment:1 Changed 2 years ago by goldfire

This is by design, but there are two competing elements of the design at work here:

  1. We really don't want type application to work with inferred types, as doing so would be very very fragile in the general case. See Section 3 of the Visible Type Applications paper.
  1. In GHC 8.0, GHCi forgets information about the distinction between specified and inferred type variables, by design. See comment:16:ticket:11376 and below. The short version is that Simon advocated for the current design (which instantiates all types and then regeneralizes), while I advocated for just reporting the type. I lost the debate, and so GHCi loses information about type variables.

These two design points lead to the confusing (but correct) interaction above. The good news is that HEAD (and, therefore, GHC 8.2) will have :type +v, which will not instantiate. You will see that :type +v id reports forall a. a -> a and :type +v bar reports forall {a}. a -> a, making the difference between these types clear(er).

To be honest, I'm not sure if there's any way to make this clearer to users, who are understandably befuddled by your interaction. (Hence my standpoint in the debate in the commentary on #11376.) Concrete suggestions are very welcome. Otherwise, feel free to close the ticket.

comment:2 Changed 2 years ago by Feuerbach

Resolution: invalid
Status: newclosed

Thanks Richard, this makes sense.

I agree that depending on the inferred order of type variables in actual code would be a bad idea.

In my case, I was just trying to evaluate something quickly in ghci like this:

*Main> description decoGrid 

<interactive>:64:1: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘description’
      prevents the constraint ‘(LayoutModifier
                                  (Decoration DefaultDecoration DefaultShrinker)
                                  a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instance exist:
        one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: description decoGrid
      In an equation for ‘it’: it = description decoGrid

<interactive>:64:13: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘decoGrid’
      prevents the constraint ‘(Eq a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance Eq XEvent -- Defined in ‘Graphics.X11.Xlib.Event’
        instance Eq FontSet -- Defined in ‘Graphics.X11.Xlib.Extras’
        instance Eq FontStruct -- Defined in ‘Graphics.X11.Xlib.Font’
        ...plus 61 others
        ...plus 138 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the first argument of ‘description’, namely ‘decoGrid’
      In the expression: description decoGrid
      In an equation for ‘it’: it = description decoGrid
*Main> :t decoGrid 
decoGrid
  :: forall {a}.
     Eq a =>
     ModifiedLayout
       (Decoration DefaultDecoration DefaultShrinker) Grid a
*Main> -- ok, so I need to apply decoGrid to the right type param
*Main> description (decoGrid @Window)

<interactive>:67:14: error:
    • Cannot apply expression of type ‘ModifiedLayout
                                         (Decoration DefaultDecoration DefaultShrinker) Grid a0’
      to a visible type argument ‘Window’
    • In the first argument of ‘description’, namely
        ‘(decoGrid @Window)’
      In the expression: description (decoGrid @Window)
      In an equation for ‘it’: it = description (decoGrid @Window)
*Main> -- this works:
*Main> :set -XPartialTypeSignatures -Wno-partial-type-signatures
*Main> description (decoGrid :: _ Window)
"DefaultDecoration Grid"

comment:3 Changed 2 years ago by rwbarton

Well (I don't know whether this is documented anywhere but) that should not be the confusing part--forall {a}. means you can't use a type application to specify the type. The confusing part is the behavior of :t id and :t foo. But :info will show you the difference.

Note: See TracTickets for help on using tickets.