GHC thinks pattern match is exhaustive

{-# OPTIONS_GHC -Werror #-}

module Lib where

data Value = Finite Integer | Infinity
  deriving (Eq)

instance Num Value where
  (+)         = undefined
  (*)         = undefined
  abs         = undefined
  signum      = undefined
  negate      = undefined
  fromInteger = Finite

isSpecial :: Value -> Bool
isSpecial Infinity = True
isSpecial 0        = True
isSpecial 1        = True
isSpecial _        = False

> ghc Lib.hs
[1 of 1] Compiling Lib              ( Lib.hs, Lib.o )

Lib.hs:19:1: error: [-Woverlapping-patterns, -Werror=overlapping-patterns]
    Pattern match is redundant
    In an equation for ‘isSpecial’: isSpecial 1 = ...
   |
19 | isSpecial 1        = True
   | ^^^^^^^^^^^^^^^^^^^^^^^^^

Lib.hs:20:1: error: [-Woverlapping-patterns, -Werror=overlapping-patterns]
    Pattern match is redundant
    In an equation for ‘isSpecial’: isSpecial _ = ...
   |
20 | isSpecial _        = False
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

changed weight to 7

That's pretty frightening. I'm bumping priority, but anyone can feel free to disagree with that judgment.

Trac metadata

Trac field	Value
Priority	normal → high

This looks suspiciously like #15713 (closed) (that's about overloaded strings, but otherwise pretty much the same situation). There's something fishy about exhaustiveness checking on overloaded literals in general.

marked this issue as related to #15713 (closed)

marked this issue as related to #14546 (closed)

The problem is that TmOracle.solveComplexEq doesn't have a ConLit case, in which case the dreadful catch-all

Just (standby, (True, env)) -- I HATE CATCH-ALLS

hits. Note that it returns True, signalling that 'something went wrong'. Comments say "1. A Bool (are there any constraints we cannot handle? (PmExprOther)).".

No call site of solveOneEq ever handles this case! I feel like there should have been at least a warning, if not even a panic.

---

At some point during pattern-match checking, We arrive at the point we have to match Finite _ (a Con) with 0 (a Lit). This is handled by the ConLit and LitCon cases in Check.pmcheckHd, which handles this by a fresh unification variable with a constraint equating it to the literal. It then recurses to the VarCon case, which tries to solve the equation by calling out to TmOracle.solveOneEq. Curiously, the call to applySubstComplexEq will just undo the ConLit and LitCon cases in pmcheckHd by substituting the fresh unification variable with its solution. Then, the equation (0, Finite _) hits solveComplexEq and it breaks.

The solution I think is that TmOracle needs to cope with ConLit equality, which apparently was never really handled before.

assigned to @sgraf812

marked this issue as related to #322 (closed)

I don't think this is related to the incompleteness of the solver, but rather that we don't desugar Literal patterns such as Lit 42 to x |> True ~ x == Lit 42 anymore since #11303 (comment 112272). The result is that we no longer go through the UConVar case from the paper, which will effectively split the value vector abstraction for the cases x == Lit 42 ~ True and x == Lit 42 ~ False.

Now with the ConLit case, we only check x == Lit 42 ~ True, but not x == Lit 42 ~ False, which is exactly the case that will not match the literal 42. This should be the new Uncovered set.

Upon rereading #11303 (comment 112272) I discovered that the NLit functionality does exactly what we want, but we currently don't "desugar" the LitCon case to it.

Currently, the LitCon case will desugar to Var by equating the literal to a fresh unification variable which is used as the syntactic pattern to match against. But that leads to the faulty behavior, because Var will just record an additional constraint equating the variable to the Finite _ value abstraction, so we don't propagate the uncovered set for when we don't have a Lit 0.

Instead what we need to do is desugar LitCon to LitVar, by equating a fresh variable to Finite _. LitVar takes care of 'case splitting' like in the UConVar case from the paper. Crucially, it doesn't introduce a fresh unification variable (see #11303 (comment 112272) for how this causes blowup), but rather uses NLit to record the constraint on the variable directly in the value abstraction. In effect, the Uncovered set from the Lit case is empty and the NLit case determines the whole Uncovered set. Bingo!

Note that the ConLit case is fine as it is, because it desugars to ConVar and will properly case split on possible constructors.

I implemented this in !676 (merged). It fixes the associated test case T16289, but let's see what other bugs this will fix.

mentioned in commit 7bd8ef84

mentioned in commit 0c175011

marked this issue as related to #11195 (closed)

Coincidentally, this also fixes the problems with #11195 (closed). Runtime goes down to 130ms from 10s. I wonder why, I can't spot any obvious LitCon cases in there.

No, this didn't fix anything. I compared performance on different tests.

mentioned in commit aa94e89f

mentioned in merge request !676 (merged)

mentioned in commit 8021a856

added pattern match warnings label

mentioned in commit aca30f9e

mentioned in commit 4626cf21

closed via commit 4626cf21

mentioned in issue #15713 (closed)

mentioned in issue #11303 (closed)

added Phigh label