Pattern match incompleteness / inaccessibility discrepancy
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.