From 31088dd32a4dbbed649dff0700610eb7ed7a9fca Mon Sep 17 00:00:00 2001 From: David Feuer Date: Wed, 26 Jan 2022 17:31:56 +0000 Subject: 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 --- testsuite/tests/typecheck/should_compile/T20996.hs | 111 +++++++++++++++++++++ testsuite/tests/typecheck/should_compile/all.T | 1 + 2 files changed, 112 insertions(+) create mode 100644 testsuite/tests/typecheck/should_compile/T20996.hs (limited to 'testsuite') 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, ['']) -- cgit v1.2.1