[GHC] #12468: GADTs don't refine hole types
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: | Owner: benjamin.hodgson | Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: MacOS X Architecture: | Type of failure: Incorrect Unknown/Multiple | warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Apologies if this is a dupe. I did look! {{{ #!haskell {-# LANGUAGE GADTs #-} data T a where I :: T Int f :: T a -> a f I = _ }}} This gives the type error: {{{ • Found hole: _ :: a Where: ‘a’ is a rigid type variable bound by the type signature for: f :: forall a. T a -> a at test.hs:6:6 • In the expression: _ In an equation for ‘f’: f I = _ • Relevant bindings include f :: T a -> a (bound at test.hs:7:1) }}} It should say something about `a` being `Int` in this branch. I'm using GHC 8.0.1 on OSX El Capitan. I think this may be a regression; I have a vague memory of it working with GHC 7.10. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I don't think this is a bug. Yes we have an equality in scope; but a value of type `a` and one of type `Int` are both equally valid things to fill the hole with. E.g. {{{ f :: T a -> a -> a f I x = _ }}} I could fill the hole with `(3::Int)` or with `x`. Neitehr is better than the other. Another way to say this is that type equalities are not normalising; they are equalities, not left-to-right rewrite rules. Suppose we had `a ~ b` in scope. Should report the hole as having type `a` or `b`? What if it was `a ~ [b]`? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by benjamin.hodgson): Thanks for the reply! I see what you mean about `a` and `Int` both being good options to show for the hole type. However, I do think it would still be helpful to have ''some'' indicator in the error message of the fact that the context gives us a useful equality. Something along the lines of: {{{ • Found hole: _ :: a ... • NB: a ~ [b] }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
However, I do think it would still be helpful to have some indicator in the error message of the fact that the context gives us an equality. After all, such information can be very useful when you're trying to fill in a hole. Something along the lines of:
Yes, that's plausible and do-able; along the lines of displaying the "relevant bindings". Does anyone want to have a go? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * type: bug => feature request -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #11325 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * os: MacOS X => Unknown/Multiple * related: => #11325 Comment: As noted in #11325, this is actually a regression from GHC 7.10 to 8.0. In GHC 7.10.3, you get the behavior that you seek: {{{ $ /opt/ghc/7.10.3/bin/ghci Bug.hs GHCi, version 7.10.3: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:7:7: Found hole ‘_’ with type: Int Relevant bindings include f :: T a -> a (bound at Bug.hs:7:1) In the expression: _ In an equation for ‘f’: f I = _ Failed, modules loaded: none. }}} As opposed to the current behavior: {{{ $ /opt/ghc/8.0.1/bin/ghci Bug.hs GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:7:7: error: • Found hole: _ :: a Where: ‘a’ is a rigid type variable bound by the type signature for: f :: forall a. T a -> a at Bug.hs:6:6 • In the expression: _ In an equation for ‘f’: f I = _ • Relevant bindings include f :: T a -> a (bound at Bug.hs:7:1) Failed, modules loaded: none. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #11325 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): On second thoughts, I don't think I'd fully realised that there was a type signature to guide the type checker. Yes, it probably does make sense to "normalise" the hole with all the "givens". And it's very easy to do, a 2-line change. Patch coming -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #11325 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"433b80dec1cfef787fc1327a9eada1791b11c12e/ghc" 433b80d/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="433b80dec1cfef787fc1327a9eada1791b11c12e" Ensure that insolubles are fully rewritten I was alerted to this by Trac #12468 and #11325. We were treating insolubles (and "hole" constraints are treated as insoluble) inconsistently. In some places we were carefully rewriting them e.g. Note [Make sure that insolubles are fully rewritten] in TcCanonical. But in TcSimplify we weren't feeding them into the solver. As a result, "hole" constraints were not being rewritten, which some users found confusing, and I think rightly so. This patch also fixes a bug in TcSMonad.emitInsoluble, in which two different "hole" constriants could be treated (bogusly) as duplicates, thereby losing one. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12468: GADTs don't refine hole types -------------------------------------+------------------------------------- Reporter: benjamin.hodgson | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: gadt/T12468 Blocked By: | Blocking: Related Tickets: #11325 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => gadt/T12468 * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC