[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
#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