[GHC] #11156: Type-changing record update catch-all in sum type doesn't typecheck
#11156: Type-changing record update catch-all in sum type doesn't typecheck -------------------------------------+------------------------------------- Reporter: afarmer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Apologies for the confusing title/summary, but that is about as succinct as I could be. Rather than try to describe this in english, here is the smallest example I could repro with. I want to write this: {{{ import Data.Char data R a = Foo { x :: a, y :: a } | Bar { x :: a } | Baz { x :: a } ordify :: R Char -> R Int ordify r@(Foo {}) = r { x = ord (x r), y = ord (y r) } ordify r = r { x = ord (x r) } }}} But that fails to typecheck: {{{ $ ghci Test.hs GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Test.hs, interpreted ) Test.hs:10:21: Couldn't match type ‘Char’ with ‘Int’ Expected type: R Int Actual type: R Char In the expression: r In the expression: r {x = ord (x r)} Failed, modules loaded: none. }}} Instead, I have to resort to enumerating all the remaining constructors: {{{ import Data.Char data R a = Foo { x :: a, y :: a } | Bar { x :: a } | Baz { x :: a } ordify :: R Char -> R Int ordify r@(Foo {}) = r { x = ord (x r), y = ord (y r) } ordify (Bar x) = Bar (ord x) ordify (Baz x) = Baz (ord x) }}} The sum type has the property that every constructor has the field x, and some constructors have fields which are also parameterized over x's type 'a'. I would expect my first example, with the catch-all record-update to typecheck, but it doesn't. I suspect GHC thinks the catch-all case of ordify might be passed a Foo constructor, in which case the record update would be ill-typed, even though that is impossible due to the first case matching Foo explicitly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11156 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11156: Type-changing record update catch-all in sum type doesn't typecheck -------------------------------------+------------------------------------- Reporter: afarmer | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: GHC typechecks this {{{ ordify :: R Char -> R Int ordify r@(Foo {}) = r { x = ord (x r), y = ord (y r) } ordify r = r { x = ord (x r) } }}} as if you had written this: {{{ ordify :: R Char -> R Int ordify r@(Foo {}) = r { x = ord (x r), y = ord (y r) } ordify r = case r of Foo x y -> Foo (ord x) y -- Eeek! Bar x -> Bar (ord x) Baz x -> Bar (ord x) }}} The `Eeek!` line elicits the complaint. You may say that the `Foo` case is already dealt with, so this branch of the case is dead code, but in general that require sophisticated reasoning, certainly more than the type checker can do. So I don't see a way to fix this; sorry. I'll close as "invalid" because GHC is behaving as advertised; but the goal is not invalid of course! Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11156#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11156: Type-changing record update catch-all in sum type doesn't typecheck -------------------------------------+------------------------------------- Reporter: afarmer | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): This is analogous to wanting this function to typecheck: {{{ plusOne :: Int -> Int plusOne n = if True then n + 1 else 'A' -- unreachable }}} But the Haskell 98/Haskell 2010 standard says it should not typecheck: "The type of e1 must be Bool; e2 and e3 must have the same type, which is also the type of the entire conditional expression." The same for the original program, though the typing rules for record update are more complicated. But they similarly do not depend on knowledge about the value of the record-to-be-updated. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11156#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11156: Type-changing record update catch-all in sum type doesn't typecheck -------------------------------------+------------------------------------- Reporter: afarmer | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by afarmer): Yeah, I figured it wouldn't be easy to fix, and the workaround isn't too onerous. However, it does seem like a bit of a wart. I had to stare at it for many minutes before I realized what was probably going on... the error seems really non-obvious unless you understand how record updates desugar, so I just wanted to document it. I wondered if the new overlapping/missing patterns algorithm could be adapted to spot the impossible case, but I'm sure the effort-to-payoff ratio is much too high. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11156#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC