GDeciding1 missing instance for (f :.: g)

[fizruk]

This missing instance disables using deciding1 for datatypes like this:

data Tree a = Leaf a | Node [Tree a] deriving Generic1

To fix this missing instance Deciding1 and deciding1 have to gain extra parameters:

class (Generic1 t, GDeciding1 q1 q (Rep1 t)) => Deciding1 q1 q t where
  deciding1 :: Decidable f => p1 q1 -> p q
    -> (forall g b. q1 g => f b -> f (g b))  -- used for (f :.: g)
    -> (forall b. q b => f b)                -- used for K1
    -> f a                                   -- used for Par1
    -> f (t a)

GDeciding1 then can have an instance for (f :.: g):

instance (q1 f, GDeciding1 q1 q g) => GDeciding1 q1 q (f :.: g) where
  gdeciding1 p1 p g q r = contramap unComp1 (g (gdeciding1 p1 p g q r))

Examples:

-- | It's impossible to have an instance of Void1 unless f a ~ Void.
class Void1 f where absurd1 :: f a -> b

geq1 :: Deciding1 Void1 Eq f => (a -> a -> Bool) -> f a -> f a -> Bool
geq1 f = getEquivalence $ deciding1
  (Proxy :: Proxy Void1) (Proxy :: Proxy Eq)
  (const $ Equivalence absurd1) (Equivalence (==)) (Equivalence f)

-- | Every type has an instance of Unit1.
-- Unit1 a ~ ()
class Unit1 a
instance Unit1 a

gfoldMap :: (Deciding1 Foldable Unit1 f, Monoid m) => (a -> m) -> f a -> m
gfoldMap = flip . getOp $ deciding1
  (Proxy :: Proxy Foldable) (Proxy :: Proxy Unit1) 
  (Op . foldMap . getOp) (Op mempty) (Op (flip id))