GHC: Ticket #8191: Do not trim type environment when reporting type holes
http://ghc.haskell.org/trac/ghc/ticket/8191
<p>
Andres writes: I've just started playing with <code>TypeHoles</code>. (I'm writing some Haskell course
materials and would like to use them from the very beginning once they become
available.)
</p>
<p>
However, I must say that I don't understand the current notion of "relevance"
that seems to determine whether local bindings are included or not.
</p>
<p>
The current rule seems to be that bindings are included only if the
intersection between the type variables their types involve and the type
variables in the whole is non-empty. However, I think this is confusing.
</p>
<p>
Let's look at a number of examples:
</p>
<pre class="wiki">> f1 :: Int -> Int -> Int
> f1 x y = _
Found hole ‛_’ with type: Int
In the expression: _
In an equation for ‛f1’: f1 x y = _
</pre><p>
No bindings are shown.
</p>
<pre class="wiki">> f2 :: a -> a -> a
> f2 x y = _
Found hole ‛_’ with type: a
Where: ‛a’ is a rigid type variable bound by
the type signature for f2 :: a -> a -> a at List.hs:6:7
Relevant bindings include
f2 :: a -> a -> a (bound at List.hs:7:1)
x :: a (bound at List.hs:7:4)
y :: a (bound at List.hs:7:6)
In the expression: _
In an equation for ‛f2’: f2 x y = _
</pre><p>
Both <code>x</code> and <code>y</code> (and <code>f2</code>) are shown. Why should this be treated differently
from <code>f1</code>?
</p>
<pre class="wiki">> f3 :: Int -> (Int -> a) -> a
> f3 x y = _
Found hole ‛_’ with type: a
Where: ‛a’ is a rigid type variable bound by
the type signature for f3 :: Int -> (Int -> a) -> a at List.hs:9:7
Relevant bindings include
f3 :: Int -> (Int -> a) -> a (bound at List.hs:10:1)
y :: Int -> a (bound at List.hs:10:6)
In the expression: _
In an equation for ‛f3’: f3 x y = _
</pre><p>
Here, <code>y</code> is shown, but <code>x</code> isn't, even though <code>y</code> has to be applied to an Int
in order to produce an <code>a</code>. Of course, it's possible to obtain an <code>Int</code> from
elsewhere ...
</p>
<pre class="wiki">f4 :: a -> (a -> b) -> b
f4 x y = _
Found hole ‛_’ with type: b
Where: ‛b’ is a rigid type variable bound by
the type signature for f4 :: a -> (a -> b) -> b at List.hs:12:7
Relevant bindings include
f4 :: a -> (a -> b) -> b (bound at List.hs:13:1)
y :: a -> b (bound at List.hs:13:6)
In the expression: _
In an equation for ‛f4’: f4 x y = _
</pre><p>
Again, only <code>y</code> is shown, and <code>x</code> isn't. But here, the only sane way of filling
the hole is by applying <code>y</code> to <code>x</code>. Why is one more relevant than the other?
</p>
<pre class="wiki">f5 x y = _
Found hole ‛_’ with type: t2
Where: ‛t2’ is a rigid type variable bound by
the inferred type of f5 :: t -> t1 -> t2 at List.hs:15:1
Relevant bindings include
f5 :: t -> t1 -> t2 (bound at List.hs:15:1)
In the expression: _
In an equation for ‛f5’: f5 x y = _
</pre><p>
Neither <code>x</code> and <code>y</code> are included without a type signature. Even though all of
the above types are admissible, which would convince GHC that one or even
all may be relevant.
</p>
<p>
IMHO, this isn't worth it. It's a confusing rule. Just include all local bindings
in the output, always. That's potentially verbose, but easy to understand. It's
also potentially really helpful, because it trains beginning programmers to see
what types local variables get, and it's a way to obtain complex types of locally
bound variables for expert programmers. It's also much easier to explain. It
should be easier to implement, too :)
</p>
<p>
Could we please change it?
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/8191
Trac 1.2.2simonpjWed, 28 Aug 2013 14:09:45 GMT
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:1
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:1
<p>
There was quite a bit of support for this, so I went ahead and did it. There's a flag <code>-fmax-relevant-bindings=N</code> to limit the output.
</p>
<p>
Simon
</p>
TicketSimon Peyton Jones <simonpj@…>Thu, 29 Aug 2013 15:45:44 GMT
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:2
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:2
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/a1efe57ed2b5e90c0a562ead754f44821c5434c8/ghc" title="Display the full type environment when reporting type holes
This ...">a1efe57ed2b5e90c0a562ead754f44821c5434c8/ghc</a>:
</p>
<pre class="message">Display the full type environment when reporting type holes
This fixes Trac #8191.
The patch also adds and documents a new flag -fmax-relevant-bindings=N
which lets you control how many bindings in the type environment are shown.</pre>
TicketsimonpjThu, 29 Aug 2013 15:54:17 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:3
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:3
<ul>
<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>
Existing test case for holes are in place. A commit in the test suite accepts their new output.
</p>
TicketmonoidalThu, 05 Sep 2013 15:09:03 GMT
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:4
http://ghc.haskell.org/trac/ghc/ticket/8191#comment:4
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8233" title="#8233: bug: Type environment when reporting holes (closed: fixed)">#8233</a>
</p>
Ticket