This non-exhaustive pattern match seems exhaustive

I'm emulating a "closed typeclass" using a closed type family: * {-# LANGUAGE ExistentialQuantification #-}* * {-# LANGUAGE GADTs #-}* * {-# LANGUAGE LambdaCase #-}* * {-# LANGUAGE TypeFamilies #-}* * import GHC.Exts (Constraint)* * -- This is like* * --* * -- class Thing a -- instance Thing Int --* * type family Thing a :: Constraint where* * Thing Int = ()* * data Foo = forall a. Thing a => Foo (Bar a)* * data Bar a where* * Bar1 :: Bar Int* * Bar2 :: Bar Bool* * inspectFoo :: Foo -> ()* * inspectFoo = \case* * Foo Bar1 -> ()* * Foo Bar2 -> () -- This is required to suppress a warning* Here, it's not possible to create a Foo using "Foo Bar2", because there is no "Thing Bool" constraint in scope. Yet, when picking apart a Foo, I must still pattern match on this impossible data. Is there some smarter way to write this code? I thought of using `constraints`, and adding a catch-all clause to Thing: * type family Thing a :: Constraint where Thing Int = ()* * Thing a = Bottom* This would at least allow users of a Foo to use some * absurd :: Bottom => a* thing to discharge the Bottom constraint brought in scope by pattern matching: * inspectFoo :: Foo -> () inspectFoo = \case Foo Bar1 -> () Foo Bar2 -> absurd bottom* but better still would be to avoid having to write these impossible cases. Thanks!
participants (1)
-
Mitchell Rosen