[GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 (Type checker) | Keywords: GADTs | Operating System: Linux Architecture: x86 | Type of failure: Incorrect | warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- From [https://www.youtube.com/watch?v=6snteFntvjM A Practical Introduction to Haskell GADTs] from LambdaConf 2015, example from attachment Hole.hs: {{{#!hs {-# LANGUAGE GADTs #-} data STy ty where SInt :: STy Int SBool :: STy Bool SMaybe :: STy a -> STy (Maybe a) zero :: STy ty -> ty zero ty = case ty of SInt -> 5 SBool -> False SMaybe a -> _ }}} When running with "GHCi, version 7.11.20151226": {{{ % ghci -ignore-dot-ghci /tmp/Hole.hs GHCi, version 7.11.20151226: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/Hole.hs, interpreted ) /tmp/Hole.hs:12:15: error: • Found hole: _ :: ty Where: ‘ty’ is a rigid type variable bound by the type signature for: zero :: forall ty. STy ty -> ty at /tmp/Hole.hs:8:9 • In the expression: _ In a case alternative: SMaybe a -> _ In the expression: case ty of { SInt -> 5 SBool -> False SMaybe a -> _ } • Relevant bindings include a :: STy a (bound at /tmp/Hole.hs:12:10) ty :: STy ty (bound at /tmp/Hole.hs:9:6) zero :: STy ty -> ty (bound at /tmp/Hole.hs:9:1) Failed, modules loaded: none. Prelude> }}} when older versions (GHCi version 7.10.2) refine the type of `_` to `Maybe a`: {{{ % ghci-7.10.2 -ignore-dot-ghci /tmp/Hole.hs GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/Hole.hs, interpreted ) /tmp/Hole.hs:12:15: Found hole ‘_’ with type: Maybe a Where: ‘a’ is a rigid type variable bound by a pattern with constructor SMaybe :: forall a. STy a -> STy (Maybe a), in a case alternative at /tmp/Hole.hs:12:3 Relevant bindings include a :: STy a (bound at /tmp/Hole.hs:12:10) ty :: STy ty (bound at /tmp/Hole.hs:9:6) zero :: STy ty -> ty (bound at /tmp/Hole.hs:9:1) In the expression: _ In a case alternative: SMaybe a -> _ In the expression: case ty of { SInt -> 5 SBool -> False SMaybe a -> _ } Failed, modules loaded: none. Prelude> }}} Regression? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "Hole.hs" added. GHC 7.11 does not refine the typed hole -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "Hole.log" added. ghci-7.11.20151226 -v -ignore-dot-ghci /tmp/Hole.hs &> /tmp/Hole.log -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire Comment: I'm sure this is from the visible type application stuff. Will take a look. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: #12468 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #12468 Comment: See #12468, where SPJ argues that the current behavior is not necessarily wrong, and proposes that we should instead report something to the effect of: {{{ • Found hole: _ :: ty ... • NB: ty ~ Maybe a }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: #12468 | 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/11325#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: #12468 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I've confirmed that the 7.10 behaviour is restored, but I didn't add a second test ... the test for #12468 seems sufficient. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11325: Type of hole does not get refined after pattern matching on [GADT] constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: fixed | Keywords: GADTs Operating System: Linux | Architecture: x86 Type of failure: Incorrect | Test Case: warning at compile-time | Blocked By: | Blocking: Related Tickets: #12468 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC