[Haskell-cafe] This non-exhaustive pattern match seems exhaustive

[Mitchell Rosen]

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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160615/34091f60/attachment.html>