[GHC] #15584: nonVoid is too conservative w.r.t. strict argument types
#15584: nonVoid is too conservative w.r.t. strict argument types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple PatternMatchWarnings | Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: #15305 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In the implementation of the pattern-match coverage checker, the `nonVoid` function checks is some `Type` is inhabitable by at least one constructor. However, `nonVoid` currently does not recursively call itself on the strict argument types of each constructor that is considered. This means that certain exhaustive functions are mistakenly flagged as non- exhaustive, such as in the following example: {{{#!hs {-# LANGUAGE EmptyCase #-} {-# OPTIONS -Wincomplete-patterns #-} module Bug where import Data.Void data V = MkV !Void data S = MkS !V f :: S -> a f x = case x of {} }}} {{{ $ /opt/ghc/head/bin/ghci Bug.hs GHCi, version 8.7.20180827: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:11:7: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: (MkS _) | 11 | f x = case x of {} | ^^^^^^^^^^^^ }}} The natural solution would be to call `nonVoid` recursively on strict argument types, so as to be able to tell that `S` in uninhabitable. But we can't just do this willy nilly, since we could run into infinite loops with recursive examples like this one: {{{#!hs data Abyss = MkAbyss !Abyss stareIntoTheAbyss :: Abyss -> a stareIntoTheAbyss x = case x of {} }}} Better solution: put a recursive type checker into `nonVoid`, and bail out if recursion is detected. Patch incoming. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15584 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15584: nonVoid is too conservative w.r.t. strict argument types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #15305 | Differential Rev(s): Phab:D5116 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5116 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15584#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15584: nonVoid is too conservative w.r.t. strict argument types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #15305 | Differential Rev(s): Phab:D5116 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): How clever do we want to be here? Users need to be able to predict, reasonably reliably, how far they should go in explaining totality to the compiler. We certainly wouldn't want GHC to complain about a redundant pattern match in {{{#!hs f :: S -> a f (MkS (MkV v)) = absurd v }}} because that's perfectly reasonable code. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15584#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15584: nonVoid is too conservative w.r.t. strict argument types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #15305 | Differential Rev(s): Phab:D5116 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:2 dfeuer]:
Users need to be able to predict, reasonably reliably, how far they should go in explaining totality to the compiler.
I agree! This proposed change would make it easier for users' to predict when a function is total. The rule is this: if it is possible to pass a well typed argument to a function //that doesn't bottom when demanded//, then that function must match that argument in order to be considered total. (The part in italics is what is new in GHC 8.8 after #15305, and further improved upon in this ticket.)
We certainly wouldn't want GHC to complain about a redundant pattern match in
{{{#!hs f :: S -> a f (MkS (MkV v)) = absurd v }}}
because that's perfectly reasonable code.
I would disagree about this being perfectly reasonable code—there's no reason to ever match on `MkS` (or `MkV`), since that is guaranteed to bottom when demanded. In other words, it's another form of unreachable code, since calling `f (MkS (MkV ⊥))` will bottom out before `MkV` (or `MkS`) are ever reached. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15584#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15584: nonVoid is too conservative w.r.t. strict argument types
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| PatternMatchWarnings
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
error/warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: #15305 | Differential Rev(s): Phab:D5116
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#15584: nonVoid is too conservative w.r.t. strict argument types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: error/warning at compile-time | pmcheck/should_compile/T15584 Blocked By: | Blocking: Related Tickets: #15305 | Differential Rev(s): Phab:D5116 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => pmcheck/should_compile/T15584 * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15584#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC