@@ -1,6 +1,15 @@
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE ConstraintKinds #-}
13{-# LANGUAGE DataKinds #-}
24{-# LANGUAGE FlexibleInstances #-}
5+{-# LANGUAGE KindSignatures #-}
36{-# LANGUAGE MultiParamTypeClasses #-}
7+{-# LANGUAGE PolyKinds #-}
8+{-# LANGUAGE Rank2Types #-}
9+{-# LANGUAGE ScopedTypeVariables #-}
10+{-# LANGUAGE TypeApplications #-}
11+{-# LANGUAGE TypeFamilies #-}
12+{-# LANGUAGE TypeOperators #-}
413{-# LANGUAGE UndecidableInstances #-}
514
615-----------------------------------------------------------------------------
@@ -21,11 +30,13 @@ module Data.Generics.Product.Types
2130 --
2231 -- $example
2332 HasTypes (..)
33+ , HasTypesDeep (..)
2434 ) where
2535
2636import Data.Generics.Product.Internal.Types
37+import Data.Kind (Constraint)
2738
28−import GHC.Generics (Generic (Rep))
39+import GHC.Generics
2940import Data.Generics.Internal.VL.Traversal
3041import Data.Generics.Internal.VL.Iso
3142
@@ -38,3 +49,59 @@ instance
3849 ) => HasTypes a s where
3950 types = confusing (\f -> (repIso . gtypes) (f :> HNil))
4051 {-# INLINE types #-}
52+
53+class HasTypesDeep a s where
54+ typesDeep :: Traversal' s a
55+
56+instance
57+ ( HasConstraints' ((~) a) s
58+ ) => HasTypesDeep a s where
59+
60+ typesDeep f s = constraints' @((~) a) f s
61+
62+--------------------------------------------------------------------------------
63+type family Primitive a :: Bool where
64+ Primitive Int = 'True
65+ Primitive Char = 'True
66+ Primitive Bool = 'True
67+ Primitive _ = 'False
68+ -- TODO: more primitives, or perhaps abstract from stop condition
69+
70+-- TODO: refactor
71+-- deep constrained traversals, stopping at primitive types
72+class HasConstraints' (c :: * -> Constraint) s where
73+ constraints' :: forall g.
74+ Applicative g => (forall a. c a => a -> g a) -> s -> g s
75+
76+instance (Generic s, GHasConstraints' c (Rep s)) => HasConstraints' c s where
77+ constraints' f s = to <$> gconstraints' @c f (from s)
78+
79+class GHasConstraints' (c :: * -> Constraint) (f :: * -> *) where
80+ gconstraints' :: forall g x.
81+ Applicative g => (forall a. c a => a -> g a) -> f x -> g (f x)
82+
83+instance (GHasConstraints' c l, GHasConstraints' c r) => GHasConstraints' c (l :*: r) where
84+ gconstraints' f (l :*: r) = (:*:) <$> gconstraints' @c f l <*> gconstraints' @c f r
85+
86+instance (GHasConstraints' c l, GHasConstraints' c r) => GHasConstraints' c (l :+: r) where
87+ gconstraints' f (L1 l) = L1 <$> gconstraints' @c f l
88+ gconstraints' f (R1 r) = R1 <$> gconstraints' @c f r
89+
90+instance GRec c (Primitive a) (K1 R a) => GHasConstraints' c (K1 R a) where
91+ gconstraints' = grec @c @(Primitive a)
92+
93+instance GHasConstraints' c f => GHasConstraints' c (M1 m meta f) where
94+ gconstraints' f (M1 x) = M1 <$> gconstraints' @c f x
95+
96+instance GHasConstraints' c U1 where
97+ gconstraints' _ _ = pure U1
98+
99+class GRec (c :: * -> Constraint) (s :: Bool) (f :: * -> *) where
100+ grec :: forall g x.
101+ Applicative g => (forall a. c a => a -> g a) -> f x -> g (f x)
102+
103+instance HasConstraints' c a => GRec c 'False (K1 R a) where
104+ grec f (K1 s) = K1 <$> constraints' @c @a f s
105+
106+instance c a => GRec c 'True (K1 R a) where
107+ grec f s = kIso f s