Add test supplied in T20996 which uses data family result kind polymorphism

David (@dfeuer) writes:

Following @kcsongor, I've used ridiculous data family result kind polymorphism in linear-generics, and am currently working on getting it into staged-gg. If it should be removed, I'd appreciate a heads up, and I imagine Csongor would too.

What do I need by ridiculous polymorphic result kinds? Currently, data families are allowed to have result kinds that end in Type (or maybe TYPE r? I'm not sure), but not in concrete data kinds. However, they are allowed to have polymorphic result kinds. This leads to things I think most of us find at least quite weird. For example, I can write

data family Silly :: k
data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue :: SBool True
  SSSilly :: SBool Silly
type KnownBool b where
  kb :: SBool b
instance KnownBool False where kb = SFalse
instance KnownBool True where kb = STrue
instance KnownBool Silly where kb = Silly

Basically, every kind now has potentially infinitely many "legit" inhabitants.

As horrible as that is, it's rather useful for GHC's current native generics system. It's possible to use these absurdly polymorphic result kinds to probe the structure of generic representations in a relatively pleasant manner. It's a sort of "formal type application" reminiscent of the notion of a formal power series (see the test case below). I suspect a system more like kind-generics wouldn't need this extra probing power, but nothing like that is natively available as yet.

If the ridiculous result kind polymorphism is banished, we'll still be able to do what we need as long as we have stuck type families. It's just rather less ergonomical: a stuck type family has to be used with a concrete marker type argument.