GHC: Ticket #5296: Add explicit type applications
http://ghc.haskell.org/trac/ghc/ticket/5296
<p>
This example is derived from code in my application. It works, but I can't add a signature to it. In other places it is preventing some code from compiling at all.
</p>
<pre class="wiki">{-# LANGUAGE KindSignatures, MultiParamTypeClasses, RankNTypes #-}
{-# OPTIONS -Wall #-}
module Test where
class C t1 t2 m where method :: Int -> m t2
f :: forall t1 t2 (m :: * -> *). C t1 t2 m => Int -> m t2
f x = method x
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/5296
Trac 1.0.9dsfSun, 03 Jul 2011 17:38:33 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:1
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:1
<p>
Replying to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5296" title="feature request: Add explicit type applications (closed: fixed)">dsf</a>:
</p>
<p>
To be clear, to get the module to load remove the signature from f. In my application I might be able to get things working by removing signatures, but it leads to a cascade of signature removal that is not really acceptable.
</p>
TicketdsfSun, 03 Jul 2011 18:11:25 GMTcc, blockedby set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:2
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:2
<ul>
<li><strong>cc</strong>
<em>dsf@…</em> added
</li>
<li><strong>blockedby</strong>
set to <em>1897</em>
</li>
</ul>
TicketliyangThu, 07 Jul 2011 02:44:12 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:3
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:3
<ul>
<li><strong>cc</strong>
<em>hackage.haskell.org@…</em> added
</li>
</ul>
TicketiglooSun, 17 Jul 2011 12:28:46 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:4
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:4
<ul>
<li><strong>milestone</strong>
set to <em>7.4.1</em>
</li>
</ul>
TicketsimonpjFri, 22 Jul 2011 16:11:15 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:5
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:5
<p>
The problem here is related to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1897" title="bug: Ambiguous types and rejected type signatures (closed: fixed)">#1897</a>, as you point out, but is even clearer because it doesn't even involve type families. The trouble is this. <tt>method</tt> has type
</p>
<pre class="wiki">method :: C t1 t2 m => Int -> m t2
</pre><p>
Notice that <tt>t1</tt> does not appear in <tt>method</tt>'s type. Now GHC is faced with
</p>
<pre class="wiki">From given (C t1 t2 m)
deduce wanted (C t3 t2 m)
</pre><p>
Notice the t3. The call of <tt>method</tt> means that the second and third args of C must be t2, m; but the first can be anything. So type inference is supposed to guess what type it should use for t3. Here there is a unique choice, but in general it is hard to solve problems where there is are <em>positive</em> clues, only that there is just one magic solution.
</p>
<p>
If we could supply the type arguments to the call to <tt>method</tt>, we could say this:
</p>
<pre class="wiki">f :: forall t1 t2 (m :: * -> *). C t1 t2 m => Int -> m t2
f x = method @t1 @t2 @m x
</pre><p>
Here I put the type args with a leading "@" (the notation I'm currently considering for type args). Now we'd be fine.
</p>
<p>
In short, the only Decent Solution here seems to me to be explicit type arguments. Unless anyone else has better ideas.
</p>
TicketsimonpjWed, 27 Jul 2011 06:18:28 GMTtype, summary changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:6
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:6
<ul>
<li><strong>type</strong>
changed from <em>bug</em> to <em>feature request</em>
</li>
<li><strong>summary</strong>
changed from <em>Compile succeeds without signature, but fails with the signature suggested by GHC</em> to <em>Add explicit type applications</em>
</li>
</ul>
TicketsimonpjFri, 29 Jul 2011 21:54:38 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:7
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:7
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4466" title="feature request: Add extension for type application (closed: duplicate)">#4466</a>
</p>
TicketiglooFri, 10 Feb 2012 16:15:55 GMTpriority, milestone changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:8
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:8
<ul>
<li><strong>priority</strong>
changed from <em>normal</em> to <em>low</em>
</li>
<li><strong>milestone</strong>
changed from <em>7.4.1</em> to <em>7.6.1</em>
</li>
</ul>
TicketiglooWed, 12 Sep 2012 11:13:31 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:9
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:9
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.1</em> to <em>7.6.2</em>
</li>
</ul>
TicketsweirichTue, 30 Apr 2013 16:18:37 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:10
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:10
<ul>
<li><strong>cc</strong>
<em>sweirich@…</em> added
</li>
</ul>
TicketkosmikusTue, 30 Apr 2013 18:39:13 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:11
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:11
<ul>
<li><strong>cc</strong>
<em>mail@…</em> added
</li>
</ul>
TicketskeuchelTue, 18 Jun 2013 10:00:13 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:12
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:12
<ul>
<li><strong>cc</strong>
<em>steven.keuchel@…</em> added
</li>
</ul>
TicketHamidhasanFri, 19 Jul 2013 18:28:19 GMTcc changed; difficulty set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:13
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:13
<ul>
<li><strong>cc</strong>
<em>hamidhasan14@…</em> added
</li>
<li><strong>difficulty</strong>
set to <em>Project (more than a week)</em>
</li>
</ul>
TicketjstolarekTue, 28 Jan 2014 09:40:02 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:14
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:14
<ul>
<li><strong>cc</strong>
<em>jan.stolarek@…</em> added
</li>
</ul>
TicketthoughtpoliceMon, 14 Jul 2014 13:07:28 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:15
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:15
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.2</em> to <em>7.10.1</em>
</li>
</ul>
<p>
Moving to 7.10.1.
</p>
TicketthoughtpoliceTue, 23 Dec 2014 13:33:45 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:16
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:16
<ul>
<li><strong>milestone</strong>
changed from <em>7.10.1</em> to <em>7.12.1</em>
</li>
</ul>
<p>
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
</p>
TicketgoldfireFri, 07 Aug 2015 13:07:38 GMTos, architecture changed; owner, differential set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:17
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:17
<ul>
<li><strong>owner</strong>
set to <em>goldfire</em>
</li>
<li><strong>differential</strong>
set to <em>Phab:D1138</em>
</li>
<li><strong>os</strong>
changed from <em>Linux</em> to <em>Unknown/Multiple</em>
</li>
<li><strong>architecture</strong>
changed from <em>x86_64 (amd64)</em> to <em>Unknown/Multiple</em>
</li>
</ul>
<p>
Patch available now, at <a class="ext-link" href="https://phabricator.haskell.org/D1138" title="D1138 in Phab"><span class="icon"></span>Phab:D1138</a> and at branch <tt>wip/type-app</tt>.
</p>
<p>
There are implementation notes in Phab. Here are some design notes:
</p>
<ul><li>There is no explicit <em>kind</em> instantiation. It just won't parse! This will be fixed along with <a class="ext-link" href="https://phabricator.haskell.org/D808" title="D808 in Phab"><span class="icon"></span>Phab:D808</a>.
</li></ul><ul><li>The new extension <tt>TypeApplications</tt> implies <tt>AllowAmbiguousTypes</tt>. This makes sense, because in the presence of visible type application, there is really no such thing as an ambiguous type.
</li></ul><ul><li>Suppose there is no <tt>Eq</tt> instance for <tt>T</tt> and <tt>a,b :: T</tt>. The expression <tt>a == b</tt> is clearly ill-typed. Previously, the error was reported on the <tt>==</tt>. Now it's reported on the whole expression. I think this makes sense.
</li></ul><p>
I have two open design questions:
</p>
<ol><li>What to do with <tt>:type</tt> in GHCi? Suppose we have <tt>pair :: forall a. a -> forall b. b -> (a,b)</tt>. I ask <tt>:type pair 3</tt>. The real type of this expression is <tt>forall b. b -> (a0, b)</tt>, where <tt>a0</tt> is the type of the overloaded <tt>3</tt>. The problem is that this type loses the fact that we need <tt>Num a0</tt>. We could say <tt>forall b. Num a0 => b -> (a0, b)</tt>, which is a little closer. Would we report that without <tt>-fprint-explicit-foralls</tt>? It would be wrong to say <tt>forall a b. Num a => b -> (a, b)</tt> (as is done today, even with this patch) because we can't instantiate <tt>a</tt> with a further visible type application.
</li></ol><ol start="2"><li>It would be nice to be able to say <tt>3 @Int</tt> instead of <tt>(3 :: Int)</tt>. But this doesn't work out. Writing <tt>3</tt> in code really means <tt>fromInteger $3</tt> (where <tt>$3</tt> is the internal representation for the <tt>Integer</tt> 3). <tt>fromInteger</tt> comes from the <tt>Num</tt> class; it has type <tt>forall a. Num a => Integer -> a</tt>. So, we would want <tt>3 @Int</tt> to really become <tt>fromInteger @Int $3</tt>. But this is hard to arrange for. Alternatively, we could change <tt>fromInteger</tt> to have type <tt>Integer -> forall a. Num a => a</tt>, 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 <tt>fromInteger</tt>:
</li></ol><pre class="wiki">fromIntegerVta :: Integer -> forall a. Num a => a
fromIntegerVta = fromInteger
</pre><blockquote>
<p>
Interpreting overloaded numbers in Haskell source would then use <tt>fromIntegerVta</tt>. But this is all a little painful. Is it worth it to have <tt>3 @Int</tt>?
</p>
</blockquote>
TicketsimonpjFri, 07 Aug 2015 15:38:17 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:18
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:18
<p>
Can I tell, in GHCi, whether a particular function (perhaps in scope by being imported) is amenably to VTA? Perhaps <tt>:info f</tt> tells me?
</p>
<p>
For (2) I suggest just saying <tt>(3 :: Int)</tt>. There are more exciting things to do than allow "@" in place of "::".
</p>
TicketgoldfireFri, 07 Aug 2015 15:42:34 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:19
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:19
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5296#comment:18" title="Comment 18">simonpj</a>:
</p>
<blockquote class="citation">
<p>
Can I tell, in GHCi, whether a particular function (perhaps in scope by being imported) is amenably to VTA? Perhaps <tt>:info f</tt> tells me?
</p>
</blockquote>
<p>
No. But there should be. <tt>:info</tt> would be easy to modify. But I think <tt>:type</tt> should indicate this as well somehow.
</p>
<blockquote class="citation">
<p>
For (2) I suggest just saying <tt>(3 :: Int)</tt>. There are more exciting things to do than allow "@" in place of "::".
</p>
</blockquote>
<p>
Yes, I suppose that's true.
</p>
TicketthoughtpoliceFri, 11 Sep 2015 08:38:26 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:20
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:20
<ul>
<li><strong>milestone</strong>
changed from <em>7.12.1</em> to <em>8.0.1</em>
</li>
</ul>
<p>
Milestone renamed
</p>
TicketjstolarekFri, 18 Sep 2015 09:24:18 GMTcc changed; related set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:21
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:21
<ul>
<li><strong>cc</strong>
<em>jstolarek</em> added; <em>jan.stolarek@…</em> removed
</li>
<li><strong>related</strong>
set to <em>#4466</em>
</li>
</ul>
TicketWrenThorntonSat, 19 Sep 2015 21:10:46 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:22
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:22
<ul>
<li><strong>cc</strong>
<em>wren@…</em> added
</li>
</ul>
TicketWrenThorntonSat, 19 Sep 2015 21:33:39 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:23
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:23
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5296#comment:17" title="Comment 17">goldfire</a>:
</p>
<blockquote class="citation">
<p>
I have two open design questions:
</p>
<ol><li>What to do with <tt>:type</tt> in GHCi? Suppose we have <tt>pair :: forall a. a -> forall b. b -> (a,b)</tt>. I ask <tt>:type pair 3</tt>. The real type of this expression is <tt>forall b. b -> (a0, b)</tt>, where <tt>a0</tt> is the type of the overloaded <tt>3</tt>. The problem is that this type loses the fact that we need <tt>Num a0</tt>. We could say <tt>forall b. Num a0 => b -> (a0, b)</tt>, which is a little closer. Would we report that without <tt>-fprint-explicit-foralls</tt>? It would be wrong to say <tt>forall a b. Num a => b -> (a, b)</tt> (as is done today, even with this patch) because we can't instantiate <tt>a</tt> with a further visible type application.
</li></ol></blockquote>
<p>
IMO, the type <tt>forall a b. Num a => b -> (a, b)</tt> is wrong for the expression <tt>(pair 3)</tt> aka <tt>(pair @a (fromInteger @a $3))</tt>, because the type <tt>a</tt> is fixed, albeit unknown. My first inclination would be to say those expressions have type <tt>iota a. Num a => forall b. b -> (a, b)</tt>. Of course, I wouldn't expect most folks to know anything about the <tt>iota</tt> quantifier, so I probably wouldn't print it that way. Do we have a notation for metavariables yet? We could say <tt>Num ?a => forall b. b -> (?a, b)</tt> supposing <tt>?a</tt> is the way we write a metavariable (rather than that syntax being used by ImplicitParams).
</p>
<blockquote class="citation">
<ol start="2"><li>It would be nice to be able to say <tt>3 @Int</tt> instead of <tt>(3 :: Int)</tt>.
</li></ol></blockquote>
<p>
I agree with spj here. There's not really any benefit in terms of expressibility nor brevity.
</p>
TicketgoldfireSun, 20 Sep 2015 03:40:50 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:24
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:24
<p>
Thanks for the suggestion. Unfortunately, I think that <tt>?a</tt> looks too much like ImplicitParams. But I do like the general idea.
</p>
<p>
Here's a very, very radical thought: what if we use color? We could print <tt>forall b. Num a => b -> (a, b)</tt> but put <tt>a</tt> in a different color. (Even though it's a bit of a lie, I prefer putting the <tt>forall b</tt> before the <tt>Num a</tt>, only because Haskellers are much more used to that ordering.) Non-colored terminals still get all the information they need: that <tt>b</tt> is available for type application whereas <tt>a</tt> is not. But someone with color could see the needed information very easily.
</p>
<p>
But something tells me it would be a major plumbing job to get color output... :(
</p>
TicketgoldfireMon, 21 Sep 2015 01:55:41 GMTblocking set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:25
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:25
<ul>
<li><strong>blocking</strong>
set to <em>10770</em>
</li>
</ul>
TicketgoldfireMon, 21 Dec 2015 17:40:28 GMTdifferential changed
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:26
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:26
<ul>
<li><strong>differential</strong>
changed from <em>Phab:D1138</em> to <em>Phab:D1681</em>
</li>
</ul>
TicketRichard Eisenberg <eir@…>Thu, 24 Dec 2015 19:37:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:27
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:27
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/2db18b8135335da2da9918b722699df684097be9/ghc" title="Visible type application
This re-working of the typechecker algorithm ...">2db18b81/ghc</a>:
</p>
<pre class="message">Visible type application
This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.
This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.
This patch addresses tickets #10619, #5296, #10589.</pre>
TicketgoldfireThu, 24 Dec 2015 19:39:35 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:28
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:28
<ul>
<li><strong>testcase</strong>
set to <em>typecheck/should_compile/Vta{1,2} typecheck/should_fail/VtaFail</em>
</li>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
All set now.
</p>
TicketandrewthadWed, 02 Mar 2016 20:55:29 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:29
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:29
<p>
This might be a little too late, but I wanted to raise a question about the relationship this has with AllowAmbiguousTypes. I haven't tried it out yet, but based on an earlier comment in this thread, I think that turning on VisibleTypeApplication will also turn on AllowAmbiguousTypes. I don't think that this is necessary, and I think that there are situation where it is detrimental the library users. Let's say that I have a <tt>Rec</tt> from <tt>vinyl</tt> and I'm using <tt>rget</tt> from <tt>Data.Vinyl.Lens</tt>. Today, if I have <tt>myRec :: Rec Identity '[Char,Bool,Int]</tt>, I can write <tt>rget (Proxy :: Proxy Int) myRec</tt> to get the <tt>Int</tt> value out. In the future, it may be desirable to write a function <tt>rget2</tt> that can take the argument by VisibleTypeApplication instead. So, we would call <tt>rget2 @Int myRec</tt> instead.
</p>
<p>
Here's the issue that I'm getting at. What does an end user have to enable to be able to use <tt>rget2</tt>? At the definition site, in the case of <tt>rget2</tt>, we actually don't need AllowAmbiguousTypes, but let's pretend that we did (I should have picked a different example). When a user turns on VisibleTypeApplication to be able to use a function that will otherwise have ambiguous type variable instantiation, I don't think that they should get AllowAmbiguousTypes turned on as well. If I understand correctly, AllowAmbiguousTypes is only needed to define these functions, not to use them.
</p>
TicketgoldfireWed, 02 Mar 2016 21:57:58 GMT
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:30
http://ghc.haskell.org/trac/ghc/ticket/5296#comment:30
<p>
It depends on what ambiguity means. In a language with visible type application,
</p>
<pre class="wiki">foo :: (Show a, Read a) => String -> String
</pre><p>
can be called quite easily. Thus the ambiguity check seems unhelpful here. Thus the decision to have <tt>TypeApplications</tt> turn on <tt>AllowAmbiguousTypes</tt>.
</p>
<p>
I do see what you're getting at. Perhaps this is the wrong design, and I'm happy to think about changing it (although it does seem a bit late). I will say that if you do want the ambiguity check, you can always use <tt>NoAllowAmbiguousTypes</tt>.
</p>
<p>
If you wish to pursue the issue, I think a good next step is posting to ghc-devs to see what others think.
</p>
Ticket