Re: [GHC] #11984: Pattern match incompleteness / inaccessibility discrepancy

2 Mar 2018

      #11984: Pattern match incompleteness / inaccessibility discrepancy
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.1
      Resolution:  fixed             |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  T11984
      Blocked By:                    |             Blocking:
 Related Tickets:  #14098            |  Differential Rev(s):  Phab:D4434
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * status:  patch => closed
 * testcase:   => T11984
 * resolution:   => fixed
 * milestone:   => 8.6.1

Old description:
...
Consider this module:
{{{
{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
module Bug where
data family Sing (a :: k)
data Schema = Sch [Bool]
data instance Sing (x :: Schema) where
  SSch :: Sing x -> Sing ('Sch x)
data instance Sing (x :: [k]) where
  SNil :: Sing '[]
  SCons :: Sing a -> Sing b -> Sing (a ': b)
data G a where
  GCons :: G ('Sch (a ': b))
eval :: G s -> Sing s -> ()
eval GCons s =
        case s of
          -- SSch SNil -> undefined
          SSch (SCons _ _) -> undefined
}}}
Upon seeing this, GHC says
{{{
Bug.hs:21:9: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (SSch SNil)
}}}
So I uncomment the second-to-last line, inducing GHC to say
{{{
Bug.hs:22:16: error:
    • Couldn't match type ‘a : b’ with ‘'[]’
      Inaccessible code in
        a pattern with constructor: SNil :: forall k. Sing '[],
        in a case alternative
    • In the pattern: SNil
      In the pattern: SSch SNil
      In a case alternative: SSch SNil -> undefined
}}}
Thankfully, this pattern is much rarer than it once was, but it's a bit
sad that it's still possible.
New description:

 Consider this module:

 {{{#!hs
 {-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}

 module Bug where

 data family Sing (a :: k)

 data Schema = Sch [Bool]

 data instance Sing (x :: Schema) where
   SSch :: Sing x -> Sing ('Sch x)

 data instance Sing (x :: [k]) where
   SNil :: Sing '[]
   SCons :: Sing a -> Sing b -> Sing (a ': b)

 data G a where
   GCons :: G ('Sch (a ': b))

 eval :: G s -> Sing s -> ()
 eval GCons s =
         case s of
           -- SSch SNil -> undefined
           SSch (SCons _ _) -> undefined
 }}}

 Upon seeing this, GHC says

 {{{
 Bug.hs:21:9: warning: [-Wincomplete-patterns]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: (SSch SNil)
 }}}

 So I uncomment the second-to-last line, inducing GHC to say

 {{{
 Bug.hs:22:16: error:
     • Couldn't match type ‘a : b’ with ‘'[]’
       Inaccessible code in
         a pattern with constructor: SNil :: forall k. Sing '[],
         in a case alternative
     • In the pattern: SNil
       In the pattern: SSch SNil
       In a case alternative: SSch SNil -> undefined
 }}}

 Thankfully, this pattern is much rarer than it once was, but it's a bit
 sad that it's still possible.

--

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:14
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler