TypeHoles behaviour

23 Aug 2013

      Hi.

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?

Cheers,
  Andres

-- 
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com