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.2.2.dev0dsfSun, 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="#5296: 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="#1897: 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. <code>method</code> has type
</p>
<pre class="wiki">method :: C t1 t2 m => Int -> m t2
</pre><p>
Notice that <code>t1</code> does not appear in <code>method</code>'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 <code>method</code> 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 <code>method</code>, 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="#4466: 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 <code>wip/type-app</code>.
</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 <code>TypeApplications</code> implies <code>AllowAmbiguousTypes</code>. 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 <code>Eq</code> instance for <code>T</code> and <code>a,b :: T</code>. The expression <code>a == b</code> is clearly ill-typed. Previously, the error was reported on the <code>==</code>. 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 <code>:type</code> in GHCi? Suppose we have <code>pair :: forall a. a -> forall b. b -> (a,b)</code>. I ask <code>:type pair 3</code>. The real type of this expression is <code>forall b. b -> (a0, b)</code>, where <code>a0</code> is the type of the overloaded <code>3</code>. The problem is that this type loses the fact that we need <code>Num a0</code>. We could say <code>forall b. Num a0 => b -> (a0, b)</code>, which is a little closer. Would we report that without <code>-fprint-explicit-foralls</code>? It would be wrong to say <code>forall a b. Num a => b -> (a, b)</code> (as is done today, even with this patch) because we can't instantiate <code>a</code> with a further visible type application.
</li></ol><ol start="2"><li>It would be nice to be able to say <code>3 @Int</code> instead of <code>(3 :: Int)</code>. But this doesn't work out. Writing <code>3</code> in code really means <code>fromInteger $3</code> (where <code>$3</code> is the internal representation for the <code>Integer</code> 3). <code>fromInteger</code> comes from the <code>Num</code> class; it has type <code>forall a. Num a => Integer -> a</code>. So, we would want <code>3 @Int</code> to really become <code>fromInteger @Int $3</code>. But this is hard to arrange for. Alternatively, we could change <code>fromInteger</code> to have type <code>Integer -> forall a. Num a => a</code>, 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 <code>fromInteger</code>:
</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 <code>fromIntegerVta</code>. But this is all a little painful. Is it worth it to have <code>3 @Int</code>?
</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 <code>:info f</code> tells me?
</p>
<p>
For (2) I suggest just saying <code>(3 :: Int)</code>. 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 <code>:info f</code> tells me?
</p>
</blockquote>
<p>
No. But there should be. <code>:info</code> would be easy to modify. But I think <code>:type</code> should indicate this as well somehow.
</p>
<blockquote class="citation">
<p>
For (2) I suggest just saying <code>(3 :: Int)</code>. 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 <code>:type</code> in GHCi? Suppose we have <code>pair :: forall a. a -> forall b. b -> (a,b)</code>. I ask <code>:type pair 3</code>. The real type of this expression is <code>forall b. b -> (a0, b)</code>, where <code>a0</code> is the type of the overloaded <code>3</code>. The problem is that this type loses the fact that we need <code>Num a0</code>. We could say <code>forall b. Num a0 => b -> (a0, b)</code>, which is a little closer. Would we report that without <code>-fprint-explicit-foralls</code>? It would be wrong to say <code>forall a b. Num a => b -> (a, b)</code> (as is done today, even with this patch) because we can't instantiate <code>a</code> with a further visible type application.
</li></ol></blockquote>
<p>
IMO, the type <code>forall a b. Num a => b -> (a, b)</code> is wrong for the expression <code>(pair 3)</code> aka <code>(pair @a (fromInteger @a $3))</code>, because the type <code>a</code> is fixed, albeit unknown. My first inclination would be to say those expressions have type <code>iota a. Num a => forall b. b -> (a, b)</code>. Of course, I wouldn't expect most folks to know anything about the <code>iota</code> quantifier, so I probably wouldn't print it that way. Do we have a notation for metavariables yet? We could say <code>Num ?a => forall b. b -> (?a, b)</code> supposing <code>?a</code> 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 <code>3 @Int</code> instead of <code>(3 :: Int)</code>.
</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 <code>?a</code> 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 <code>forall b. Num a => b -> (a, b)</code> but put <code>a</code> in a different color. (Even though it's a bit of a lie, I prefer putting the <code>forall b</code> before the <code>Num a</code>, only because Haskellers are much more used to that ordering.) Non-colored terminals still get all the information they need: that <code>b</code> is available for type application whereas <code>a</code> 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 <code>Rec</code> from <code>vinyl</code> and I'm using <code>rget</code> from <code>Data.Vinyl.Lens</code>. Today, if I have <code>myRec :: Rec Identity '[Char,Bool,Int]</code>, I can write <code>rget (Proxy :: Proxy Int) myRec</code> to get the <code>Int</code> value out. In the future, it may be desirable to write a function <code>rget2</code> that can take the argument by VisibleTypeApplication instead. So, we would call <code>rget2 @Int myRec</code> 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 <code>rget2</code>? At the definition site, in the case of <code>rget2</code>, 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 <code>TypeApplications</code> turn on <code>AllowAmbiguousTypes</code>.
</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 <code>NoAllowAmbiguousTypes</code>.
</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