Opened 5 months ago

Last modified 5 months ago

#13717 new bug

Pattern synonym exhaustiveness checks don't play well with EmptyCase

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.2.1-rc1
Keywords: PatternSynonyms, PatternMatchWarnings Cc: mpickering, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by dfeuer)

In #8779, mpickering added a COMPLETE pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with EmptyCase. Suppose I write

newtype Fin (n :: Nat) = Fin Natural  -- constructor not exported

pattern FZ :: () => n ~ 'S m => Fin n
pattern FS :: () => n ~ 'S m => Fin m -> Fin n
{-# COMPLETE FZ, FS #-}

I would very much like to be able to write

finZAbsurd :: Fin 'Z -> Void
finZAbsurd x = case x of

but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this:

When checking empty case, check that at least one complete pattern set is impossible.

In this case, it would see two complete pattern sets: the built-in {Fin} and the user-decreed {FZ, FS}. Since neither FZ nor FS have matching types, we should conclude that the empty case is fine.

Change History (6)

comment:1 Changed 5 months ago by dfeuer

Description: modified (diff)

comment:2 Changed 5 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 5 months ago by RyanGlScott

I tried to reproduce this error, but I couldn't. I don't know what implementations for FZ and FS you had in mind, so I tried whipping up my own example from scratch:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -Wall #-}
module T (T(TInt, TBool), tCharAbsurd1) where

import Data.Void

data T a where
  MkTInt  :: T Int
  MkTBool :: T Bool

pattern TInt :: () => n ~ Int => T n
pattern TInt = MkTInt

pattern TBool :: () => n ~ Bool => T n
pattern TBool = MkTBool
{-# COMPLETE TInt, TBool #-}

tCharAbsurd1 :: T Char -> Void
tCharAbsurd1 x = case x of {}

This, however, compiles without any warnings. I even tried using T in another module:

{-# LANGUAGE EmptyCase #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

import Data.Void
import T

tCharAbsurd2 :: T Char -> Void
tCharAbsurd2 x = case x of {}

This too compiles without warning:

$ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling T                ( T.hs, interpreted )
[2 of 2] Compiling Bug              ( Bug.hs, interpreted )
Ok, modules loaded: Bug, T.

How did you get this supposed pattern coverage warning?

comment:4 Changed 5 months ago by dfeuer

Here's a full reproduction:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE Trustworthy #-}

module Fin (Nat (..), Fin (FZ, FS)) where
import Numeric.Natural
import Unsafe.Coerce

data Nat = Z | S Nat

-- Fin *must* be exported abstractly (or placed in an Unsafe
-- module) to maintain type safety.
newtype Fin (n :: Nat) = Fin Natural

data FinView n where
  VZ :: FinView ('S n)
  VS :: !(Fin n) -> FinView ('S n)

viewFin :: Fin n -> FinView n
viewFin (Fin 0) = unsafeCoerce VZ
viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1)))

pattern FZ :: () => n ~ 'S m => Fin n
pattern FZ <- (viewFin -> VZ) where
  FZ = Fin 0

pattern FS :: () => n ~ 'S m => Fin m -> Fin n
pattern FS m <- (viewFin -> VS m) where
  FS (Fin m) = Fin (1 + m)

{-# COMPLETE FZ, FS #-}

finZAbsurd :: Fin 'Z -> a
finZAbsurd x = case x of

Obviously, finZAbsurd is not really total, because I could pass it Fin 12 :: Fin 'Z, but

  1. My Complete pragma has explicitly stated that this will never happen, and
  2. GHC is willing to buy my white lie if I give at least one pattern, so it should be willing to buy it if I don't give any.
Last edited 5 months ago by dfeuer (previous) (diff)

comment:5 Changed 5 months ago by dfeuer

For the record, I can implement finZAbsurd in a messier way that the pattern checker accepts:

finZAbsurd :: Fin 'Z -> a
finZAbsurd = finZAbsurd' Refl
  where
    finZAbsurd' :: n :~: 'Z -> Fin n -> a
    finZAbsurd' pf FZ = case pf of
    finZAbsurd' pf (FS _) = case pf of

but that's a lot uglier.

comment:6 Changed 5 months ago by RyanGlScott

dfeuer, thanks. Now I see why my example didn't trigger any warnings: the definition of the T type itself (i.e., the fact that it was a GADT) was what ruled out the possibility of matching on any of its constructors in tCharAbsurd. On the other hand, Fin does not have this property, and you're relying on the types of the conlikes in its COMPLETE set to rule out the possibility of matching anything.

Note: See TracTickets for help on using tickets.