#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