[GHC] #5296: Add explicit type applications

[GHC]

#5296: Add explicit type applications
-------------------------------------+-------------------------------------
        Reporter:  dsf               |                   Owner:  goldfire
            Type:  feature request   |                  Status:  new
        Priority:  low               |               Milestone:  7.12.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:                    |  Differential Revisions:  Phab:D1138
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * owner:   => goldfire
 * differential:   => Phab:D1138
 * os:  Linux => Unknown/Multiple
 * architecture:  x86_64 (amd64) => Unknown/Multiple


Comment:

 Patch available now, at Phab:D1138 and at branch `wip/type-app`.

 There are implementation notes in Phab. Here are some design notes:

 * There is no explicit ''kind'' instantiation. It just won't parse! This
 will be fixed along with Phab:D808.

 * The new extension `TypeApplications` implies `AllowAmbiguousTypes`. This
 makes sense, because in the presence of visible type application, there is
 really no such thing as an ambiguous type.

 * Suppose there is no `Eq` instance for `T` and `a,b :: T`. The expression
 `a == b` is clearly ill-typed. Previously, the error was reported on the
 `==`. Now it's reported on the whole expression. I think this makes sense.

 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.

 2. It would be nice to be able to say `3 @Int` instead of `(3 :: Int)`.
 But this doesn't work out. Writing `3` in code really means `fromInteger
 $3` (where `$3` is the internal representation for the `Integer` 3).
 `fromInteger` comes from the `Num` class; it has type `forall a. Num a =>
 Integer -> a`. So, we would want `3 @Int` to really become `fromInteger
 @Int $3`. But this is hard to arrange for. Alternatively, we could change
 `fromInteger` to have type `Integer -> forall a. Num a => a`, which would
 work swimmingly. But we can't do this, because class methods always have
 their class variables quantified first. Making this change would mean
 writing a wrapper around `fromInteger`:

 {{{
 fromIntegerVta :: Integer -> forall a. Num a => a
 fromIntegerVta = fromInteger
 }}}

     Interpreting overloaded numbers in Haskell source would then use
 `fromIntegerVta`. But this is all a little painful. Is it worth it to have
 `3 @Int`?

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