Do not trim type environment when reporting type holes
Andres writes: I've just started playing with TypeHoles
. (I'm writing some Haskell course
materials and would like to use them from the very beginning once they become
available.)
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.
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.
Let's look at a number of examples:
> f1 :: Int -> Int -> Int
> f1 x y = _
Found hole ‛_’ with type: Int
In the expression: _
In an equation for ‛f1’: f1 x y = _
No bindings are shown.
> 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 = _
Both x
and y
(and f2
) are shown. Why should this be treated differently
from f1
?
> 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 = _
Here, y
is shown, but x
isn't, even though y
has to be applied to an Int
in order to produce an a
. Of course, it's possible to obtain an Int
from
elsewhere ...
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 = _
Again, only y
is shown, and x
isn't. But here, the only sane way of filling
the hole is by applying y
to x
. Why is one more relevant than the other?
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 = _
Neither x
and y
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.
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 :)
Could we please change it?
Trac metadata
Trac field | Value |
---|---|
Version | 7.6.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |