[GHC] #15584: nonVoid is too conservative w.r.t. strict argument types

30 Aug 2018

      #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