Requiring Show1 for Show, Eq1 for Eq, etc., is inconvenient

[robrix]

Once upon a time, fastsum had separate Apply and Apply1 typeclasses s.t. we could use Apply for Show and Apply1 for Functor. We eventually got rid of the former because compile times were already far too high, and instead used Show1 to provide our Show instance.

However, while it’s easy to derive Show instances, Show1 is not derivable, so you have to do a bunch of extra work just to show your Sums.

[robrix]

I’m pretty sure we can’t do this with PolyKinds either, because the type of Apply applies the class parameter to g and not to (g a):

class Apply (c :: (* -> *) -> Constraint) (fs :: [* -> *]) where
  apply :: (forall g . c g => g a -> b) -> Sum fs a -> b

[robrix]

We could maybe use another typeclass as a trampoline?

class Up1 (c :: * -> Constraint) f where
  up1 :: c a => (forall g . c (g a) => g a -> b) -> f a -> b

instance (Apply (Up1 Show) fs, Show a) => Show (Sum fs a) where
  showsPrec d = apply @(Up1 Show) (up1 @Show (showsPrec d))

That’s kind of a way of simulating quantified class constraints, I suppose. Specifically, we’re simulating this:

(forall a. Show a => Show (f a))

and this works out fine because we actually don’t have to prove that for all a, because we know a and we know it has a Show instance.

Worth a shot I suppose.

[robrix]

That much works, but the problem appears to be that we can’t actually define an instance of Up1, because the instance we want to write:

instance Up1 c f where
  up1 f g = f g

won’t typecheck because it can’t prove c (f a) 😞

[ocharles]

Maybe just wait for quantified constraints?

[robrix]

@ocharles: I think quantified constraints will help, but not solve the problem completely—we’ll still need to define an Apply analogue for * -> Constraint typeclasses, AFAICS. Guess we’ll find out for sure shortly, tho.