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