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 Changed 5 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 5 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 5 years ago by kosmikus (previous) (diff)

comment:3 Changed 5 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 5 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

comment:7 Changed 3 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

comment:9 Changed 21 months ago by mentheta

Cc: mentheta added

comment:10 Changed 9 months ago by RyanGlScott

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.

Note: See TracTickets for help on using tickets.