Opened 5 years ago
Last modified 9 months ago
#9091 new feature request
print and/or apply constraints when showing info for typed holes
Reported by: | kosmikus | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.2 |
Keywords: | Cc: | mentheta | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #9479, #14273, #15677 | Differential Rev(s): | |
Wiki Page: |
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.
Change History (10)
comment:1 follow-up: 2 Changed 5 years ago by
comment:2 Changed 5 years ago by
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
comment:3 follow-up: 4 Changed 5 years ago by
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 Changed 5 years ago by
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
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
Related Tickets: | → #9479 |
---|
comment:7 Changed 3 years ago by
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
Related Tickets: | #9479 → #9479, #14273 |
---|
comment:9 Changed 21 months ago by
Cc: | mentheta added |
---|
comment:10 Changed 9 months ago by
Related Tickets: | #9479, #14273 → #9479, #14273, #15677 |
---|
I believe Example 3 is another occurrence of #15677 (in deep disguise). I'll keep that ticket open, since it contains more information how one might want to implement a fix.
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)