[GHC] #8447: A combination of type-level comparison and subtraction does not work for 0
#8447: A combination of type-level comparison and subtraction does not work for 0 -------------------------------------+------------------------------------- Reporter: nushio | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 7.6.3 checker) | Operating System: Linux Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- The following function on type level naturals {{{ Diff x y = If (x <=? y) (y-x) (x-y) }}} does not work when either x or y is 0. https://github.com/nushio3/practice/blob/ea8a1716b1d6221ce32d77432b6de3f38e6... /type-nats/int-bug.hs I've tested this code on ghc 7.7.20130926 since I couldn't build the really latest ghc. I'm sorry if it is already fixed on the ghc head. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8447 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8447: A combination of type-level comparison and subtraction does not work for 0 ----------------------------------------------+---------------------------- Reporter: nushio | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Changes (by simonpj): * cc: diatchki (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8447#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8447: A combination of type-level comparison and subtraction does not work for 0 ----------------------------------------------+---------------------------- Reporter: nushio | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by carter): This seems to tie into having good coverage checking for pattern matching, at least naively. (and the fact that we currently don't really have a solver for type level nats). thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8447#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8447: A combination of type-level comparison and subtraction does not work for 0
----------------------------------------------+----------------------------
Reporter: nushio | Owner:
Type: bug | Status: new
Priority: low | Milestone:
Component: Compiler (Type checker) | Version: 7.6.3
Resolution: | Keywords:
Operating System: Linux | Architecture:
Type of failure: GHC rejects valid program | Unknown/Multiple
Test Case: | Difficulty: Unknown
Blocking: | Blocked By:
| Related Tickets:
----------------------------------------------+----------------------------
Comment (by Iavor S. Diatchki
#8447: A combination of type-level comparison and subtraction does not work for 0 ----------------------------------------------+---------------------------- Reporter: nushio | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by diatchki): Hello, the issue here is that type functions are kind of strict at the moment, so we evaluate both branched of the `If` are checked, and then we have some code that spots the one is impossible. GHC used to reason like this: 0 - 5 ~ r --> 5 + r ~ 0 --> (5 ~ 0, r ~ 0) --> Impossible For the time being I've weakened things a bit, so this does not happen anymore. However, we should probably try to think of a more general solution because we really want GHC to be good at reasoning, rather than bad! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8447#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8447: A combination of type-level comparison and subtraction does not work for 0 -------------------------------------+------------------------------------- Reporter: nushio | Owner: Type: bug | Status: infoneeded Priority: low | Milestone: Component: Compiler | Version: 7.6.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: Linux | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => infoneeded Comment: nushio: could you please attach a testcase for the testsuite. The github link you posted seems to be missing some pieces. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8447#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC