Opened 18 months ago
Closed 16 months ago
#14990 closed bug (fixed)
"Valid refinement suggestions" have the wrong types
Reported by: | goldfire | Owned by: | Tritlo |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.5 |
Keywords: | Cc: | Tritlo, Iceland_jack | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D4444 | |
Wiki Page: |
Description
I've recently discovered that the "valid suggestions" feature for typed holes is quite powerful. For example, if I say
module Bug where import Prelude (Integer, Num(..)) x :: Integer x = _ 5
and compile it with
> ghc Bug.hs -frefinement-level-substitutions=2
I get
Bug.hs:6:5: error: • Found hole: _ :: Integer -> Integer • In the expression: _ In the expression: _ 5 In an equation for ‘x’: x = _ 5 • Relevant bindings include x :: Integer (bound at Bug.hs:6:1) Valid substitutions include negate :: forall a. Num a => a -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) abs :: forall a. Num a => a -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) signum :: forall a. Num a => a -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) fromInteger :: forall a. Num a => Integer -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) Valid refinement substitutions include (-) _ :: forall a. Num a => a -> a -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) (*) _ :: forall a. Num a => a -> a -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) (+) _ :: forall a. Num a => a -> a -> a (imported from ‘Prelude’ at Bug.hs:3:26-32 (and originally defined in ‘GHC.Num’)) | 6 | x = _ 5 | ^
Note the refinement suggestions, that look not only for single identifiers that fill the hole but for function calls that could, as well.
However, the formatting of the refinement suggestions is incorrect, stating, for example, that (+) _ :: forall a. Num a => a -> a -> a
. This is plain wrong. We could say (+) _ :: a0 -> a0
where Num a0
, and that would be right, but even better would be something like
(+) x1 :: Integer -> Integer where x1 :: Integer
Now, I know that the first parameter to (+)
must be an integer.
In a more polymorphic situation, it could be
(+) x1 :: a0 -> a0 where x1 :: a0 (Num a0) holds
Change History (12)
comment:1 Changed 18 months ago by
Cc: | Tritlo added |
---|
comment:2 Changed 18 months ago by
Cc: | Iceland_jack added |
---|
comment:3 Changed 18 months ago by
Owner: | set to Tritlo |
---|
comment:4 Changed 18 months ago by
One issue that pops up: Is it more or less useful to have the type of the expression rather than the type of the function being suggested? In this case, it would be (-) (_ :: Integer) :: Integer -> Integer
, as specified by the type of the hole. In fact, if we show the specialized type, it would be the type of the hole in all situations, since that's what we're looking for in the first place! Right?
comment:5 Changed 18 months ago by
How does the following look (ignore the double mention of f
in the valid substitution list)?
tref.hs:4:5: error: • Found hole: _ :: [Integer] -> Integer • In the expression: _ In an equation for ‘f’: f = _ • Relevant bindings include f :: [Integer] -> Integer (bound at tref.hs:4:1) Valid substitutions include f :: [Integer] -> Integer (bound at tref.hs:4:1) main :: forall a. a (bound at tref.hs:7:1) f :: [Integer] -> Integer (defined at tref.hs:4:1) Valid refinement substitutions include foldl1 (_ :: Integer -> Integer -> Integer) where foldl1 :: forall (t :: * -> *). Data.Foldable.Foldable t => forall a. (a -> a -> a) -> t a -> a (imported from ‘Prelude’ at tref.hs:1:17-22 (and originally defined in ‘Data.Foldable’)) foldr1 (_ :: Integer -> Integer -> Integer) where foldr1 :: forall (t :: * -> *). Data.Foldable.Foldable t => forall a. (a -> a -> a) -> t a -> a (imported from ‘Prelude’ at tref.hs:1:47-52 (and originally defined in ‘Data.Foldable’)) foldl (_ :: Integer -> Integer -> Integer) (_ :: Integer) where foldl :: forall (t :: * -> *). Data.Foldable.Foldable t => forall b a. (b -> a -> b) -> b -> t a -> b (imported from ‘Prelude’ at tref.hs:1:33-37 (and originally defined in ‘Data.Foldable’)) foldr (_ :: Integer -> Integer -> Integer) (_ :: Integer) where foldr :: forall (t :: * -> *). Data.Foldable.Foldable t => forall a b. (a -> b -> b) -> b -> t a -> b (imported from ‘Prelude’ at tref.hs:1:40-44 (and originally defined in ‘Data.Foldable’))
comment:6 Changed 18 months ago by
You ask a good question about IDE usage. I don't have a good answer there... the Num a0
constraint is something more for the programmer to know about than to have literally in the code anywhere.
As for the new output, I like it! Thanks!
comment:7 Changed 17 months ago by
Status: | new → patch |
---|
comment:8 Changed 17 months ago by
Differential Rev(s): | → Phab:D4444 |
---|
Yes, I agree! Of course the type displayed should be the type of the actual expression and not just the type of the function suggested. That only works in the single identifier case.
In the current version, it now shows the type of the additional holes, like this:
Having any constraints known constraints on these would be very helpful, I agree, and the types of the functions themselves should be the type of the entire expression.
In the more polymorphic case, it would say:
However, I worry that this might then become less useful for IDEs in the future. I think it would be best to have something displayed that can directly replace the hole. How would you present the
(Num a0)
constraint so that it would be picked up by the hole itself? Is it possible to useScopedTypeVariables
maybe? And have it say(+) (_ :: a0) :: Num a0 => a0 -> a0
? Or would it have to be((+) :: Num a0 => a0 -> a0 -> a0) (_ :: a0) :: a0 -> a0
for the constraint to be picked up?