Incorrect warnings generated by exhaustiveness checker with pattern synonyms / GADT combination
The module
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module PatSynEx where
data NS (f :: k -> *) (xs :: [k]) = NS Int
data IsNS (f :: k -> *) (xs :: [k]) where
IsZ :: f x -> IsNS f (x ': xs)
IsS :: NS f xs -> IsNS f (x ': xs)
isNS :: NS f xs -> IsNS f xs
isNS = undefined
pattern Z :: () => (xs' ~ (x ': xs)) => f x -> NS f xs'
pattern Z x <- (isNS -> IsZ x)
pattern S :: () => (xs' ~ (x ': xs)) => NS f xs -> NS f xs'
pattern S p <- (isNS -> IsS p)
{-# COMPLETE Z, S #-}
data SList :: [k] -> * where
SNil :: SList '[]
SCons :: SList (x ': xs)
go :: SList ys -> NS f ys -> Int
go SCons (Z _) = 0
go SCons (S _) = 1
go SNil _ = error "inaccessible"
produces the following warnings with both GHC 8.2 and 8.3:
PatSynEx.hs:31:1: warning: [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘go’: go SCons (Z _) = ...
|
31 | go SCons (Z _) = 0
| ^^^^^^^^^^^^^^^^^^
PatSynEx.hs:32:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘go’: go SCons (S _) = ...
|
32 | go SCons (S _) = 1
| ^^^^^^^^^^^^^^^^^^
Neither warning seems correct. The first case is not inaccessible, the second case is not redundant.
The catch-all case has always been required with GHC even though it is not really reachable, but that's not the subject of this issue.
I tried to simplify the issue further by getting rid of the f
argument in NS
and IsNS
, but that made the issue disappear.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1-rc2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |