[GHC] #15697: Typed holes inferring a more polymorphic type
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider these two snippets. {{{#!hs testFailure :: Char testFailure = let x = id _ in x }}} Suggestions provided were {{{ /home/sreenidhi/Experiments/TypedHole.hs:3:14: error: • Found hole: _ :: a Where: ‘a’ is a rigid type variable bound by the inferred type of x :: a at /home/sreenidhi/Experiments/TypedHole.hs:3:7-14 • In the first argument of ‘id’, namely ‘_’ In the expression: id _ In an equation for ‘x’: x = id _ • Relevant bindings include x :: a (bound at /home/sreenidhi/Experiments/TypedHole.hs:3:7) testFailure :: Char (bound at /home/sreenidhi/Experiments/TypedHole.hs:2:1) }}} whereas for this one {{{#!hs testSuccess :: Char testSuccess = _ }}} It correctly suggests {{{ /home/sreenidhi/Experiments/TypedHole.hs:7:15: error: • Found hole: _ :: Char • In the expression: _ In an equation for ‘testSuccess’: testSuccess = _ • Relevant bindings include testSuccess :: Char (bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1) Valid hole fits include testSuccess :: Char (bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1) testFailure :: Char (defined at /home/sreenidhi/Experiments/TypedHole.hs:2:1) maxBound :: forall a. Bounded a => a with maxBound @Char (imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1 (and originally defined in ‘GHC.Enum’)) minBound :: forall a. Bounded a => a with minBound @Char (imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1 (and originally defined in ‘GHC.Enum’)) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 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 sreenidhi): * Attachment "TypedHole.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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): * keywords: => TypedHoles * cc: Tritlo (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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): So, the suggestions here are correct (based on the type), but why is it not inferring that `x` is of type char? It doesn't even look like it is inferring that `a` must end up being Char. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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 ulysses4ever): * cc: ulysses4ever (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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 RyanGlScott): I suppose the correct behavior here depends on whether or not you want valid hole fit suggestions to suggest the most general type of local definitions or not. Consider the following modified example: {{{#!hs testFailure :: Char testFailure = let x :: _ x = id in x 'a' }}} You might think that the reported type of the hole would be `Char -> Char`, but it's actually `forall a. a -> a`. Indeed, `forall a. a -> a` is the most general type that you can give `x`, so from a certain perspective, it's the most "correct" answer. But perhaps it's not the one you'd desire. One idea would be to allow tweaking the generalization behavior for local definitions //à la// `MonoLocalBinds`. For instance, in the following example: {{{#!hs testFailure2 :: Bool -> (Bool, Char) testFailure2 x = let f y = (x, y) in f 'a' }}} If `MonoLocalBinds` isn't enabled, then the inferred type of `f` will be `forall b. b -> (Bool, b)`. But if `MonoLocalBinds` //is// enabled, then the inferred type of `f` will be `Char -> (Bool, Char)`. I imagine we could allow valid hole fits to tweak generalization in a similar fashion (whether generalizing should be the default here or not is unclear to me). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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 sreenidhi): I fully agree with your analysis about `testFailure` - for example I might want to write {{{#!hs test1 :: Char test1 = let x :: _ -- now x really has to be forall a. a -> a x = id in const (x 'c') (x 5) }}} But consider the following {{{#!hs test2 :: Char test2 = let x :: _ -- error: Found type wildcard ‘_’ standing for ‘Char’ x = id 'c' in x test3 :: Char test3 = let x = id _ -- error: Found hole: _ :: a in x }}} Isn't it expected that the two errors to point to the same type? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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 RyanGlScott): Replying to [comment:5 sreenidhi]:
Isn't it expected that the two errors to point to the same type?
Again, that depends on whether you're generalizing or not. If you're generalizing, then `forall a. a` is what you'd expect as the type of that hole. (You could fill it with, say, `undefined` or `let y = y in y`.) If you're not generalizing, then `Char` would be what you would expect. The bottom line is that we have a design choice here—there are situations where one behavior might be preferable over the other. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15697: Typed holes inferring a more polymorphic type -------------------------------------+------------------------------------- Reporter: sreenidhi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypedHoles 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): Thanks for breaking it down, Ryan. I think this would be covered by what I call "more specific fits", like I touched on (i.e. suggesting `pi :: Floating a => a` for `_ :: Fractional a => a`). In those fits, we could also include fits that would be suggested if `MonoLocalBinds` were enabled. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15697#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC