print and/or apply constraints when showing info for typed holes
Typed holes are fantastic already, but could be even better. Consider the following three examples:
f :: Eq a => a -> a -> Bool f x y = _
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.
g :: (forall a. Eq a => a -> Bool) -> Bool g f = f _
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.
data X a where Y :: X Int h :: X a -> a -> a h Y x = _
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.
|Component||Compiler (Type checker)|