HKD: best or worst thing ever?

Many uses of HKD in the wild are only ever used to toggle between Maybe and Identity, or NonEmpty and Identity—simple cardinality restrictions, in other words. In such cases, I tend to favor the following lower-kinded approach for its simplicity:

-- For toggling between 0-or-1 and exactly-1:
data Foo opt = Foo {
  field1 :: Either opt Int,
  field2 :: Either opt String,
  field3 :: Either opt Bool
}
type FooOptionally = Foo ()
type FooDefinitely = forall a. Foo a

-- For toggling between 1-or-more and exactly-1:
data MaybeMore more a = MaybeMore a (Maybe (more, NonEmpty a))
  deriving Functor
data Foo more = Foo {
  field1 :: MaybeMore more Int,
  field2 :: MaybeMore more String,
  field3 :: MaybeMore more Bool
}
type FooPlural = Foo ()
type FooSingular = forall a. Foo a


-- Some helper patterns I usually use for matching on these things:

pattern CompletelyRight :: a -> Either Void a
pattern CompletelyRight a <- (either absurd id -> a)
  where CompletelyRight a = Right a
{-# COMPLETE CompletelyRight #-}

pattern It'sNothing :: Maybe (Void, a)
pattern It'sNothing <- (maybe () (absurd . fst) -> ())
  where It'sNothing = Nothing
{-# COMPLETE It'sNothing #-}

This avoids both giant sum types and representable invalid states, sometimes at the cost of a little extra boxing relative to HKD. It’s pretty manageable.

And how could I forget to mention the best part: the exactly-1 case is a true subtype of the others, as it intuitively ought to be! No conversion, not even a coerce, is necessary to use a FooDefinitely value where FooOptionally is desired. Try that with HKD.