DerivingVia: Permit deriving instances at unreduced types

Motivation

Certain class instances can be given uniformly over type families, without reducing the family application. This is already possible in vanilla ghc haskell. However, trying to do the same using DerivingVia is rejected, despite the equivalent instance definition being accepted. (Extended example below)

Proposal

Drop the conservative requirement in DerivingVia that the types involved be reduced.

Motivating Example

Consider the following extension of iso-deriving:

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Coerce (coerce)
import Data.Group (Group(..))
import Data.Maybe (fromJust)
import Data.Monoid.Action (Action(..))
import Data.Semiring (Semiring(..))

class Inject a b where inj :: a -> b
class Project a b where prj :: b -> a
class (Inject a b, Project a b) => Retract a b -- ^ laws: 'prj . inj = id'
class (Inject a b, Project a b) => Section a b -- ^ laws: 'inj . prj = id'
class (Retract a b, Section a b) => Iso a b

newtype Pull s t = Emb s
newtype Push t q = Prj q

This is intended to be used as

instance (Retract s t, C t) => C (Pull s t)
instance (Section t q, C t) => C (Push t q)
deriving via (Pull s t) instance C s => C t
deriving via (Push t q) instance C t => C q

So far, so good. For example, we have

instance (Retract s t, Semiring t) => Semiring (Pull s t) where
    Emb x `plus` Emb y = Emb $ (prj::t->s) $ inj x `plus` inj y
    Emb x `times` Emb y = Emb $ (prj::t->s) $ inj x `times` inj y
    fromNatural = Emb . (prj::t->s) . fromNatural
instance (Section t q, Semiring t) => Semiring (Push t q) where
    Prj x `plus` Prj y = Prj $ (inj::t->q) $ prj x `plus` prj y
    Prj x `times` Prj y = Prj $ (inj::t->q) $ prj x `times` prj y
    fromNatural = Prj . (inj::t->q) . fromNatural

Now consider the following class, encoding the group of units of a ring

data family Unit r

class Group (Unit r) => Unital r where
  injU :: Unit r -> r
  assertUnit :: r -> Unit r
  assertUnit = fromJust . checkUnit
  checkUnit :: r -> Maybe (Unit r)
  checkUnit = Just . assertUnit

instance Unital r => Inject (Unit r) r where inj = injU
instance Unital r => Project (Unit r) r where prj = assertUnit
instance Unital r => Retract (Unit r) r

Nothing controversial here. But trying to give the following instance

newtype UAct a = UAct a
instance (Action m t, Retract s t) => Action (UAct m) (Pull s t) where
  act (UAct m) (Emb x) = Emb $ (prj::t->s) $ act m (inj x)
deriving via (Pull (Unit r) r) instance (Action m r, Unital r) => Action m (Unit r)

causes ghc to complain:

• Can't make a derived instance of
    ‘Action m (Unit r)’ with the via strategy:
    No family instance for ‘Unit r’
• In the stand-alone deriving instance for
    ‘(Action m r, Unital r) => Action m (Unit r)’

 > deriving via (Pull (Unit r) r) instance (Action m r, Unital r) => Action m (Unit r)
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

However, the equivalent instance declaration (given by explicitly running the DerivingVia algorithm) is accepted by ghc!

instance (Action m r, Unital r) => Action (UAct m) (Unit r) where
  act :: UAct m -> Unit r -> Unit r
  act = coerce
    @(UAct m -> Pull (Unit r) r -> Pull (Unit r) r)
    @(UAct m -> Unit r -> Unit r)
    act