Замена одноэлементных типов данных семейством данных

Итак, в моем текущем проекте я выполняю кучу логики на уровне типов с одноэлементными типами.

Например:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
module TypeBools where

type family (||) (a :: Bool) (b :: Bool) :: Bool where
  'False  || 'False = 'False
  'False  || 'True  = 'True
  'True   || 'False = 'True
  'True   || 'True  = 'True

data OrProof (a :: Bool) (b :: Bool) (c :: Bool) where
  OrProof :: SBool (a || b) -> OrProof a b (a || b)

data SBool (b :: Bool) where
  SFalse  :: SBool 'False
  STrue   :: SBool 'True

class Boolean b where
  sBool :: SBool b
instance Boolean 'False where
  sBool = SFalse
instance Boolean 'True where
  sBool = STrue

orProof :: (Boolean a, Boolean b) => OrProof a b (a || b)
orProof = go sBool sBool where

  go :: SBool a -> SBool b -> OrProof a b (a || b)
  go SFalse SFalse = OrProof SFalse
  go SFalse STrue = OrProof STrue
  go STrue SFalse = OrProof STrue
  go STrue STrue = OrProof STrue

И это работает очень хорошо для меня. Мне нравится не возиться с одноэлементными типами вручную, имея возможность вызывать их при необходимости через класс типов (например, класс Boolean выше), но это привело к множеству довольно похожих классов типов, которые существуют только для того, чтобы конкретизировать тип как одноэлементный. данные.

Я подумал, может быть, я мог бы абстрагировать эти несколько классов типов в одно семейство типов, например, заменив SBool и Boolean выше на:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
-- ...
class Singleton (t :: k) where
  data Sing t
  sing :: Sing t

instance Singleton 'False where
  data Sing 'False = SFalse
  sing = SFalse

instance Singleton 'True where
  data Sing 'True = STrue
  sing = STrue

type SBool b = Sing (b :: Bool)

type Boolean b = Singleton (b :: Bool)
sBool :: Boolean b => SBool b
sBool = sing

Но затем я получаю ошибки сопоставления с образцом:

TypeBools2.hs:42:13:
    Couldn't match type ‘b1’ with ‘'True’
      ‘b1’ is a rigid type variable bound by
           the type signature for
             go :: SBool a1 -> SBool b1 -> OrProof a1 b1 (a1 || b1)
           at TypeBools2.hs:40:9
    Expected type: SBool b1
      Actual type: Sing 'True
    Relevant bindings include
      go :: SBool a1 -> SBool b1 -> OrProof a1 b1 (a1 || b1)
        (bound at TypeBools2.hs:41:3)
    In the pattern: STrue
    In an equation for ‘go’: go SFalse STrue = OrProof STrue
    In an equation for ‘orProof’:
        orProof
          = go sBool sBool
          where
              go :: SBool a -> SBool b -> OrProof a b (a || b)
              go SFalse SFalse = OrProof SFalse
              go SFalse STrue = OrProof STrue
              go STrue SFalse = OrProof STrue
              go STrue STrue = OrProof STrue

Я не уверен, есть ли что-то еще, что я могу убедить компилятор в том, что b1 должен иметь тип Bool, или я просто лаю здесь не по тому дереву.