# TypeHoles behaviour

Simon Peyton-Jones simonpj at microsoft.com
Wed Aug 28 16:14:15 CEST 2013

```OK I've done this.  Patch will land shortly.

Thank you for a well-articulated message.

Simon

| -----Original Message-----
| bounces at haskell.org] On Behalf Of Andres Löh
| Sent: 23 August 2013 21:02
| Subject: TypeHoles behaviour
|
| 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
|
| --