Say I have a typeclass:
data Proxy a = Proxy
class Fixed a where
fixed :: Proxy a -> Int
The definition for fixed is quite trivial so I derive it using GHC.Generics:
class GFixed f where
gfixed :: Proxy (f a) -> Int
instance (GFixed f, GFixed g) => GFixed (f :*: g) where ...
instance (GFixed f, GFixed g) => GFixed (f :+: g) where ...
instance GFixed f => GFixed (M1 i c f) where ...
instance Fixed a => GFixed (K1 i a) where ...
....
default fixed :: (Generic a, GFixed (Rep a)) => Proxy a -> Int
fixed _ = fixed (Proxy :: Proxy (Rep a b))
I don't include an instance for GFixed U1 because it doesn't make sense to have an instance
of Fixed for void types. My understanding of Generics machinery is not very good - specifically, what the types of M1 and K1 mean. The question is as follows: can I restrict GFixed at the type level, so that the default definition of fixed doesn't work with recursive types?
For example, if I write:
data Void
instance Fixed Void
I get a type error: No instance for (GFixed V1). I would like to get type error for things like instance Fixed [Int].
After a little bit of work, it turns out this is fairly simple, it even works on mutually recursive types. I'm sure there are some edge cases where it fails but I haven't found any.
{-# LANGUAGE
MultiParamTypeClasses
, FunctionalDependencies
, DataKinds
, TypeOperators
, TypeFamilies
, FlexibleContexts
, FlexibleInstances
, UndecidableInstances
, PolyKinds
, ConstraintKinds
, DeriveGeneric
, OverlappingInstances
#-}
module IsRecursive where
import GHC.Generics
import Data.Proxy
type family (:||) (a :: Bool) (b :: Bool) :: Bool where
True :|| x = True
x :|| True = True
a :|| b = False
data T2 a b
type family Elem (x :: k) (xs :: [k]) :: Bool where
Elem x '[] = False
Elem x (x ': xs) = True
Elem x (y ': xs) = Elem x xs
class IsRecursive' (tys :: [* -> *]) (rep :: * -> *) (r :: *) | tys rep -> r where
isRecursive' :: Proxy tys -> Proxy rep -> Proxy r
isRecursive' _ _ = Proxy
-- These types have recursive `Rep`s but aren't recursive because there is no `Rep` for primitive types
instance IsRecursive' tys (K1 R Int) (T2 False tys)
instance IsRecursive' tys (K1 R Double) (T2 False tys)
instance IsRecursive' tys (K1 R Char) (T2 False tys)
instance IsRecursive' tys (K1 R Float) (T2 False tys)
-- Recursive instances - unwrap one layer of `Rep` and look inside
instance IsRecursive' tys U1 (T2 False tys)
instance IsRecursive' tys (Rep c) r => IsRecursive' tys (K1 i c) r
instance (IsRecursive' tys f (T2 r0 tys0), IsRecursive' tys g (T2 r1 tys1), r2 ~ (r0 :|| r1)) => IsRecursive' tys (f :+: g) (T2 r2 tys1)
instance (IsRecursive' tys f (T2 r0 tys0), IsRecursive' tys g (T2 r1 tys1), r2 ~ (r0 :|| r1)) => IsRecursive' tys (f :*: g) (T2 r2 tys1)
instance (IsRecursive' tys f r) => IsRecursive' tys (M1 i c f) r
-- This is where the magic happens
-- Datatype declaration reps are represented as `M1 D`
-- When one is encountered, save it in the list so far and continue recursion
instance (IsRecDataDec (Elem tyrep tys) tyrep tys f r, tyrep ~ (M1 D c f)) => IsRecursive' tys (M1 D c f) r
-- Context reduction is strict, so this class makes sure we
-- only recurse if `Elem tyrep tys == False`; otherwise every recursive type
-- would cause a stack overflow
class IsRecDataDec (b :: Bool) (c :: * -> *) (tys :: [* -> *]) (f :: * -> *) (r :: *) | b c tys f -> r
instance IsRecDataDec True c tys f (T2 True (c ': tys))
instance IsRecursive' (c ': tys) f r => IsRecDataDec False c tys f r
class IsRecursive t
instance IsRecursive' '[] (Rep t) (T2 True tys) => IsRecursive t
data TBool (b :: Bool) = TBool
instance Show (TBool True) where show _ = "True"
instance Show (TBool False) where show _ = "False"
isRecursive :: IsRecursive' '[] (Rep t) (T2 r tys) => t -> TBool r
isRecursive _ = TBool
-- test cases
data K = K K deriving Generic
data A = A B deriving Generic
data B = B Q deriving Generic
data Q = Q A deriving Generic