Re: [GHC] #13060: Visible type application doesn't work for functions with inferred types

3 Jan 2017

      #13060: Visible type application doesn't work for functions with inferred types
-------------------------------------+-------------------------------------
        Reporter:  Feuerbach         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (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 [http://cs.brynmawr.edu/~rae/papers/2016/type-app/visible-type-app.pdf
 Visible Type Applications] paper.

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13060#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler