Opened 6 years ago

# print and/or apply constraints when showing info for typed holes

Reported by: Owned by: kosmikus normal Compiler (Type checker) 7.8.2 mentheta Unknown/Multiple Unknown/Multiple None/Unknown #9479, #14273, #15677

### Description

Typed holes are fantastic already, but could be even better. Consider the following three examples:

## Example 1

```f :: Eq a => a -> a -> Bool
f x y = _
```

GHC-7.8.2 shows:

```    Found hole ‘_’ with type: Bool
Relevant bindings include
y :: a (bound at THC.hs:4:5)
x :: a (bound at THC.hs:4:3)
f :: a -> a -> Bool (bound at THC.hs:4:1)
In the expression: _
In an equation for ‘f’: f x y = _
```

GHC additionally knows that `Eq a` holds. It would be great if it would print that, too.

## Example 2

```g :: (forall a. Eq a => a -> Bool) -> Bool
g f = f _
```

GHC-7.8.2 shows:

```    Found hole ‘_’ with type: a0
Where: ‘a0’ is an ambiguous type variable
Relevant bindings include
f :: forall a. Eq a => a -> Bool (bound at THC.hs:7:3)
g :: (forall a. Eq a => a -> Bool) -> Bool (bound at THC.hs:7:1)
In the first argument of ‘f’, namely ‘_’
In the expression: f _
In an equation for ‘g’: g f = f _
```

GHC additionally knows the `Eq a0` must hold. It would be nice if it could indicate that.

## Example 3

```data X a where
Y :: X Int

h :: X a -> a -> a
h Y x = _
```

GHC-7.8.2 shows:

```    Found hole ‘_’ with type: Int
Relevant bindings include
x :: a (bound at THC.hs:13:5)
h :: X a -> a -> a (bound at THC.hs:13:1)
In the expression: _
In an equation for ‘h’: h Y x = _
```

Interestingly, GHC shows that we have to produce an `Int`. Unfortunately, it shows that `x` is of type `a`. GHC additionally knows that `a ~ Int`. It would be nice if GHC could either apply the constraint to show that `x :: Int` or at least show the constraint.

### comment:1 follow-up:  2 Changed 6 years ago by simonpj

It would be easy to also show the in-scope "given" constraints. But how would you like to see them. For Ex 1, 2 can you show what error message you'd like to see? Something like (for Ex 1)

```    Found hole ‘_’ with type: Bool
Relevant bindings include
y :: a (bound at THC.hs:4:5)
x :: a (bound at THC.hs:4:3)
f :: a -> a -> Bool (bound at THC.hs:4:1)
Given constraints: Eq a
In the expression: _
In an equation for ‘f’: f x y = _
```

### comment:2 in reply to:  1 Changed 6 years ago by kosmikus

Yes, what you suggest would be fine. I don't attach much meaning to the word "Given", so I'd probably just say

```    Constraints: Eq a
```

For example 2, I'd be happy with a very similar line saying

```    Constraints: Eq a0
```

The situation is different from Ex 1 in the sense that `Eq a` in Ex 1 is a constraint you can use, whereas `Eq a0` in Ex 2 is a constraint that you're required to adhere to while filling the hole. But this information is already available from the fact that `a0` in Ex 2 appears only in the type of the hole itself, so I think I'd be happy enough if the constraints are shown in the same way.

For Ex 3, I'd like either

```    Found hole ‘_’ with type: Int
Relevant bindings include
x :: Int (bound at THC.hs:13:5)
```

or

```    Found hole ‘_’ with type: Int
Relevant bindings include
x :: a (bound at THC.hs:13:5)
[...]
Constraints: a ~ Int
```
Last edited 6 years ago by kosmikus (previous) (diff)

### comment:3 follow-up:  4 Changed 6 years ago by goldfire

Bikeshedding a bit, I would rather distinguish givens and wanteds in these messages. How about something slightly more verbose, like

```    Found hole ‘_’ with type: Bool
Relevant bindings include
y :: a (bound at THC.hs:4:5)
x :: a (bound at THC.hs:4:3)
f :: a -> a -> Bool (bound at THC.hs:4:1)
We know that the following constraints hold:
Eq a
In the expression: _
In an equation for ‘f’: f x y = _
```

Or, for the "wanted" case, `We require the following to hold:`

Is it also helpful to give the provenance of the constraints (e.g., that the `Eq a` above is from the type signature)? I don't know.

How do we print implication constraints? Do these come up?

### comment:4 in reply to:  3 Changed 6 years ago by kosmikus

I'd certainly also be ok with distinguishing givens and wanteds, and I agree that it may make things much clearer in practice. I'd prefer slightly shorter messages than the ones you suggest, but that's a minor point.

Regarding implication constraints: perhaps I'm missing something, but aren't these always global? I wouldn't include global knowledge in hole information.

### comment:5 Changed 4 years ago by chak

I agree with Andres that —in the presence of local constraints— the value of holes messages would be significantly higher with constraint information included. As for the verbosity, the terms "given constraints" and "wanted constraints" are probably not immediately clear for people who haven't read one of the relevant papers.

### comment:6 Changed 4 years ago by dfeuer

Related Tickets: → #9479

### comment:7 Changed 4 years ago by dfeuer

I think part of this was fixed with #9479, but I don't know if the constraints on the relevant bindings (the "easy" part) were included.

### comment:8 Changed 2 years ago by RyanGlScott

Related Tickets: #9479 → #9479, #14273