variants - total matching

example.hs

type A = Variant (ConsL "Age" Int (ConsL "Name" Text NilL))
demo :: A
demo = LeftV 1
demo' :: A
demo' = RightV (LeftV "x")

match :: String
match = runAccessor demo $ ConsA show $ ConsA Text.unpack NilA

variants.hs

--------------------------------------------------------------------------------
-- Variants

-- | A variant; one of the given choices.
data Variant xs where
  LeftV :: forall k a xs. a -> Variant (ConsL k a xs)
  RightV :: forall k a xs k'' a''. Variant (ConsL k'' a'' xs) -> Variant (ConsL k a (ConsL k'' a'' xs))

-- | Accessor of a given variant. A record whose fields all correspond
-- to the constructors of a sum type, and whose types are all `a ->
-- r` instead of `a`.
data Accessor (xs :: List) r where
  NilA  :: Accessor 'NilL r
  ConsA :: forall k a r xs. (a -> r) -> Accessor xs r -> Accessor (ConsL k a xs) r

-- | Run a total case-analysis against a variant, given an accessor
-- record.
runAccessor :: Variant xs -> Accessor xs r -> r
runAccessor (LeftV a) (ConsA f _) = f a
runAccessor (RightV xs) (ConsA _ ys) = runAccessor xs ys