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

David (@treeowl) 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
>
> ```haskell
> 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.

Closes #20996

Co-authored-by: Matthew Pickering <matthewtpickering@gmail.com>

2 files changed, 112 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T20996.hs b/testsuite/tests/typecheck/should_compile/T20996.hs
new file mode 100644
index 0000000000..cf318c5d60
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20996.hs
@@ -0,0 +1,111 @@
+{-# language EmptyCase #-}
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language InstanceSigs #-}
+{-# language MultiParamTypeClasses #-}
+{-# language PolyKinds #-}
+{-# language QuantifiedConstraints #-}
+{-# language ScopedTypeVariables #-}
+{-# language StandaloneKindSignatures #-}
+{-# language TypeApplications #-}
+{-# language TypeFamilies #-}
+{-# language TypeOperators #-}
+{-# language UndecidableInstances #-}
+{-# language DataKinds #-}
+module T20996 (Generic1 (..), Rep1) where
+import GHC.Generics hiding (Generic1 (..))
+import Data.Kind
+import Data.Coerce
+import GHC.TypeLits
+
+data family LastPar :: k
+data family OtherPar :: k -> k
+
+type Generic1 :: forall {k}. (k -> Type) -> Constraint
+class Generic1 (f :: k -> Type) where
+  to1 :: forall a. Rep1 f a -> f a
+  from1 :: forall a. f a -> Rep1 f a
+
+instance forall k (f :: k -> Type).
+  (forall (a :: k). GenericQ f a) => Generic1 (f :: k -> Type) where
+
+  to1 :: forall a. Rep1 f a -> f a
+  to1 = toQ
+
+  from1 :: forall a. f a -> Rep1 f a
+  from1 = fromQ
+
+type GenericQ :: forall {k}. (k -> Type) -> k -> Constraint
+class GenericQ (f :: k -> Type) (a :: k) where
+  toQ :: Rep1 f a -> f a
+  fromQ :: f a -> Rep1 f a
+
+instance forall k (f :: k -> Type) (a :: k) rfa r1f.
+  (Generic1' rfa r1f a, rfa ~ Rep (f a), r1f ~ Rep1 f, Generic (f a)) => GenericQ f a where
+  toQ :: Rep1 f a -> f a
+  toQ = to . from1' @rfa @r1f @a
+
+  fromQ :: f a -> Rep1 f a
+  fromQ = to1' @rfa @r1f @a . from
+
+type Generic1' :: forall {k}. (Type -> Type) -> (k -> Type) -> k -> Constraint
+class Generic1' (rep :: Type -> Type) (rep1 :: k -> Type) (a :: k) where
+  to1' :: rep p -> rep1 a
+  from1' :: rep1 a -> rep p
+
+instance Generic1' f f' a => Generic1' (M1 i c f) (M1 i c f') a where
+  to1' (M1 x) = M1 (to1' @f @f' @a x)
+  from1' (M1 x) = M1 (from1' @f @f' @a x)
+
+instance (Generic1' f f' a, Generic1' g g' a) => Generic1' (f :*: g) (f' :*: g') a where
+  to1' (x :*: y) = to1' @f @f' @a x :*: to1' @g @g' @a y
+  from1' (x :*: y) = from1' @f @f' @a x :*: from1' @g @g' @a y
+
+instance (Generic1' f f' a, Generic1' g g' a) => Generic1' (f :+: g) (f' :+: g') a where
+  to1' (L1 x) = L1 (to1' @f @f' @a x)
+  to1' (R1 y) = R1 (to1' @g @g' @a y)
+  from1' (L1 x) = L1 (from1' @f @f' @a x)
+  from1' (R1 y) = R1 (from1' @g @g' @a y)
+
+instance Generic1' U1 U1 a where
+  to1' U1 = U1
+  from1' U1 = U1
+
+instance Generic1' V1 V1 a where
+  to1' x = case x of
+  from1' x = case x of
+
+-- This instance is pure gold.
+instance Coercible c (r a) => Generic1' (Rec0 c) r a where
+  to1' (K1 x) = coerce @c @(r a) x
+  from1' x = K1 (coerce @(r a) @c x)
+
+type Rep1 (f :: k -> Type) = MakeRep1' @k (Rep ((MarkOtherPars f) (LastPar :: k)))
+
+type MakeRep1' :: forall k. (Type -> Type) -> k -> Type
+type family MakeRep1' (rep :: Type -> Type) :: k -> Type where
+  MakeRep1' (M1 i c f) = M1 i c (MakeRep1' f)
+  MakeRep1' (x :+: y) = MakeRep1' x :+: MakeRep1' y
+  MakeRep1' (x :*: y) = MakeRep1' x :*: MakeRep1' y
+  MakeRep1' U1 = U1
+  MakeRep1' V1 = V1
+  MakeRep1' (Rec0 c) = MakeRep1Field (Rec0 (Unmark c)) Par1 c
+
+type MarkOtherPars :: forall k. k -> k
+type family MarkOtherPars (f :: k) :: k where
+  MarkOtherPars ((f :: j -> k) (a :: j)) = MarkOtherPars f (OtherPar a)
+  MarkOtherPars f = f
+
+type Unmark :: forall k. k -> k
+type family Unmark (f :: k) :: k where
+  Unmark LastPar = TypeError ('Text "Cannot create Generic1 instance: the last parameter appears in an invalid location.")
+  Unmark (OtherPar a) = a
+  Unmark ((f :: j -> k) (a :: j)) = Unmark f (Unmark a)
+  Unmark a = a
+
+type MakeRep1Field :: forall j k. (k -> Type) -> (j -> Type) -> j -> k -> Type
+type family MakeRep1Field fk acc c where
+  MakeRep1Field fk (_ :: b -> Type) (OtherPar _) = fk
+  MakeRep1Field fk (acc :: b -> Type) ((f :: a -> b) (x :: a)) = MakeRep1Field fk (acc :.: Unmark f) x
+  MakeRep1Field fk (acc :: k -> Type) (LastPar :: k) = acc
+  MakeRep1Field fk _ _ = fk
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index f061d86fc4..b77d78e882 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -808,3 +808,4 @@ test('T20873', normal, compile, [''])
 test('T20873b', [extra_files(['T20873b_aux.hs'])], multimod_compile, ['T20873b', '-v0'])
 test('StaticPtrTypeFamily', normal, compile, [''])
 test('T20946', normal, compile, [''])
+test('T20996', normal, compile, [''])