[GHC] #5296: Add explicit type applications

[GHC]

#5296: Add explicit type applications
-------------------------------------+-------------------------------------
        Reporter:  dsf               |                   Owner:  goldfire
            Type:  feature request   |                  Status:  new
        Priority:  low               |               Milestone:  8.0.1
       Component:  Compiler (Type    |                 Version:  7.0.3
  checker)                           |
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |               Test Case:
      Blocked By:  1897              |                Blocking:
 Related Tickets:  #4466             |  Differential Revisions:  Phab:D1138
-------------------------------------+-------------------------------------

Comment (by WrenThornton):

 Replying to [comment:17 goldfire]:
 > I have two open design questions:
 >
 > 1. What to do with `:type` in GHCi? Suppose we have `pair :: forall a. a
 -> forall b. b -> (a,b)`. I ask `:type pair 3`. The real type of this
 expression is `forall b. b -> (a0, b)`, where `a0` is the type of the
 overloaded `3`. The problem is that this type loses the fact that we need
 `Num a0`. We could say `forall b. Num a0 => b -> (a0, b)`, which is a
 little closer. Would we report that without `-fprint-explicit-foralls`? It
 would be wrong to say `forall a b. Num a => b -> (a, b)` (as is done
 today, even with this patch) because we can't instantiate `a` with a
 further visible type application.

 IMO, the type  `forall a b. Num a => b -> (a, b)` is wrong for the
 expression `(pair 3)` aka `(pair @a (fromInteger @a $3))`, because the
 type `a` is fixed, albeit unknown. My first inclination would be to say
 those expressions have type `iota a. Num a => forall b. b -> (a, b)`. Of
 course, I wouldn't expect most folks to know anything about the `iota`
 quantifier, so I probably wouldn't print it that way. Do we have a
 notation for metavariables yet? We could say `Num ?a => forall b. b ->
 (?a, b)` supposing `?a` is the way we write a metavariable (rather than
 that syntax being used by ImplicitParams).

 > 2. It would be nice to be able to say `3 @Int` instead of `(3 :: Int)`.

 I agree with spj here. There's not really any benefit in terms of
 expressibility nor brevity.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5296#comment:23>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler