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!