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

[GHC]

#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