[GHC] #13768: Incorrect warnings generated by exhaustiveness checker with pattern synonyms / GADT combination

30 May 2017

      #13768: Incorrect warnings generated by exhaustiveness checker with pattern
synonyms / GADT combination
-------------------------------------+-------------------------------------
           Reporter:  kosmikus       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13768
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler