Use GHC.Generics to restrict generic function domain

Question

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].

Answer 1

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

Answer 2

The documentation is moderately helpful for the meanings of the constructors. M1 specifies meta-information (such as the names of record selectors), and K1 is a bit of a grab-bag of various things with kind *. If you want to disallow all recursion, you'll need to ensure that no instance in scope matches K1 R a. You'll still want some of the other K instances in scope, so you should change

instance Fixed a => GFixed (K1 i a) where

to

instance Fixed a => GFixed (K1 P a) where

I don't know if there are other values that can be the first parameter to K1, but if any arise it should be safe to add them, except for K1 R of course.