#14990: "Valid refinement suggestions" have the wrong types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: Tritlo (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14990#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14990: "Valid refinement suggestions" have the wrong types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Tritlo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Tritlo): * owner: (none) => Tritlo Comment: 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: {{{ • 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 abs :: forall a. Num a => a -> a signum :: forall a. Num a => a -> a fromInteger :: forall a. Num a => Integer -> a Valid refinement substitutions include (-) (_ :: Integer) :: forall a. Num a => a -> a -> a (*) (_ :: Integer) :: forall a. Num a => a -> a -> a (+) (_ :: Integer) :: forall a. Num a => a -> a -> a }}} 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: {{{ (+) (_ :: a0) :: a0 -> a0 where (Num a0) }}} 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 use `ScopedTypeVariables` maybe? And have it say `(+) (_ :: a0) :: Num a0 => a0 -> a0`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14990#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14990: "Valid refinement suggestions" have the wrong types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Tritlo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Tritlo): 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’)) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14990#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14990: "Valid refinement suggestions" have the wrong types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Tritlo Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Tritlo): * status: new => patch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14990#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14990: "Valid refinement suggestions" have the wrong types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Tritlo Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"e0b44e2eccd4053852b6c4c3de75a714301ec080/ghc" e0b44e2/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e0b44e2eccd4053852b6c4c3de75a714301ec080" Improved Valid Hole Fits I've changed the name from `Valid substitutions` to `Valid hole fits`, since "substitution" already has a well defined meaning within the theory. As part of this change, the flags and output is reanamed, with substitution turning into hole-fit in most cases. "hole fit" was already used internally in the code, it's clear and shouldn't cause any confusion. In this update, I've also reworked how we manage side-effects in the hole we are considering. This allows us to consider local bindings such as where clauses and arguments to functions, suggesting e.g. `a` for `head (x:xs) where head :: [a] -> a`. It also allows us to find suggestions such as `maximum` for holes of type `Ord a => a -> [a]`, and `max` when looking for a match for the hole in `g = foldl1 _`, where `g :: Ord a => [a] -> a`. We also show much improved output for refinement hole fits, and fixes #14990. We now show the correct type of the function, but we also now show what the arguments to the function should be e.g. `foldl1 (_ :: Integer -> Integer -> Integer)` when looking for `[Integer] -> Integer`. I've moved the bulk of the code from `TcErrors.hs` to a new file, `TcHoleErrors.hs`, since it was getting too big to not live on it's own. This addresses the considerations raised in #14969, and takes proper care to set the `tcLevel` of the variables to the right level before passing it to the simplifier. We now also zonk the suggestions properly, which improves the output of the refinement hole fits considerably. This also filters out suggestions from the `GHC.Err` module, since even though `error` and `undefined` are indeed valid hole fits, they are "trivial", and almost never useful to the user. We now find the hole fits using the proper manner, namely by solving nested implications. This entails that the givens are passed along using the implications the hole was nested in, which in turn should mean that there will be fewer weird bugs in the typed holes. I've also added a new sorting method (as suggested by SPJ) and sort by the size of the types needed to turn the hole fits into the type of the hole. This gives a reasonable approximation to relevance, and is much faster than the subsumption check. I've also added a flag to toggle whether to use this new sorting algorithm (as is done by default) or the subsumption algorithm. This fixes #14969 I've also added documentation for these new flags and update the documentation according to the new output. Reviewers: bgamari, goldfire Reviewed By: bgamari Subscribers: simonpj, rwbarton, thomie, carter GHC Trac Issues: #14969, #14990, #10946 Differential Revision: https://phabricator.haskell.org/D4444 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14990#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14990: "Valid refinement suggestions" have the wrong types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Tritlo Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Comment (by Tritlo): Yes, this has been fixed with e0b44e2/ghc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14990#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler