#15584 closed bug (fixed)

nonVoid is too conservative w.r.t. strict argument types

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.5
Keywords: PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case: pmcheck/should_compile/T15584
Blocked By: Blocking:
Related Tickets: #15305 Differential Rev(s): Phab:D5116
Wiki Page:

Description

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:

{-# 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:

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.

Change History (5)

comment:1 Changed 13 months ago by RyanGlScott

Differential Rev(s): Phab:D5116
Status: newpatch

comment:2 Changed 12 months ago 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

f :: S -> a
f (MkS (MkV v)) = absurd v

because that's perfectly reasonable code.

comment:3 in reply to:  2 Changed 12 months ago by RyanGlScott

Replying to 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

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.

comment:4 Changed 12 months ago by Ryan Scott <ryan.gl.scott@…>

In e68b439/ghc:

Add a recursivity check in nonVoid

Summary:
Previously `nonVoid` outright refused to call itself
recursively to avoid the risk of hitting infinite loops when
checking recurisve types. But this is too conservative—we //can//
call `nonVoid` recursively as long as we incorporate a way to detect
the presence of recursive types, and bail out if we do detect one.
Happily, such a mechanism already exists in the form of `checkRecTc`,
so let's use it.

Test Plan: make test TEST=T15584

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15584

Differential Revision: https://phabricator.haskell.org/D5116

comment:5 Changed 12 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: pmcheck/should_compile/T15584
Note: See TracTickets for help on using tickets.