Relax inferred context simplification to allow "exotic" contexts for GeneralizedNewtypeDeriving and DerivingVia instances.

Motivation

Many GND / DerivingVia instances that seem totally sensible must in practice be turned into StandaloneDeriving because their contexts cannot be inferred. However, inferConstraintsCoerceBased is already producing a sensible context for them, and all that's failing is simplifying that context. I suspect it's possible to simplify them differently from contexts coming from other deriving mechanisms, and make these deriving clauses work.

Proposal

The following module defines a class and attempts to GND an instance of it, but fails because the inferred constraint simplifies to C [a], which doesn't match any instance head.

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Example (Thing) where

class C a where method :: a -> String

instance C [Bool] where method _ = ""

newtype Thing a = Thing [a] deriving newtype C

This happens because of the restriction described in the Note [Exotic derived instance contexts]. However, many uses of DerivingVia intuitively want to "just copy the context of the via instance". I'm having a hard time formalizing this intuition, since there can be odd situations like mutually recursive derived instances involving newtypes [1] or self-recursive newtypes [2]. But a first pass is that if the via type is imported from another module and does not use the newtype itself as a type parameter, the system of equations being simplified for the GND instance can't be recursive, and it should suffice to simplify the context in isolation.

I tried horribly hacking up a GHC build to skip all simplification for GND and DerivingVia instances just to make sure it's only the simplification that's breaking the instance, and it sort-of worked, in that it inferred a context that had unsimplified Coercible constraints but was otherwise reasonable:

b87b0c2c2947e1ccc983269180bfe604
  $fCThing ::
    (C [a],
     ([a] -> GHC.Base.String) ~R# (Thing a -> GHC.Base.String)) =>
    C (Thing a)
  DFunId
  []

These unsimplified Coercible constraints are a problem, though, since they break calling modules that don't import the relevant newtype constructors (and the stage2 GHC doesn't build). Of course this isn't meant to be a real implementation, just a way to prove to myself that inferContextCoerceBased was sufficient for these instances.

In general many of the new instances this enables would probably require UndecidableInstances, but I'm willing to enable that as necessary. Some more example modules affected by this:

A type family interfering with simplification:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Test where

import Data.Proxy (Proxy(..))
import GHC.TypeNats (Nat, KnownNat, natVal)

data SwarmOfNats = SwarmOfNats Nat Nat Nat

type family FstSwarm (x :: SwarmOfNats) :: Nat where
  FstSwarm ('SwarmOfNats x y z) = x

class C a where method :: a -> String

instance KnownNat n => C (Proxy n) where method _ = show (natVal @n Proxy)

-- Fails simplifying because the context contains a type family application.
newtype Thing swarm = Thing (Proxy (FstSwarm swarm)) deriving newtype C

-- deriving newtype instance KnownNat (FstSwarm swarm) => C (Thing swarm)

A FlexibleContexts constraint on a MPTC interfering with simplification:

{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

module Test where

-- Disregard that this technique is blatantly overkill here...

data Rope str = Leaf str | Append (Rope str) (Rope str) deriving Foldable

class C str a where method :: a -> Rope str

newtype WrappedC a = WrappedC { unWrappedC :: a }
instance C String a => Show (WrappedC a) where
  showsPrec _p x s = foldr (++) s (method (unWrappedC x))

instance C [Char] a => C [Char] (Thing a) where
  method Thing1 = Leaf "Thing1"
  method (Thing2 x) = Append (Leaf "Thing2 ") (method x)

-- Fails because the inferred context simplifies to `C [Char] a`.
data Thing a = Thing1 | Thing2 a deriving Show via WrappedC (Thing a)

-- deriving via WrappedC (Thing a) instance C [Char] a => Show (Thing a)

[1]: A GND instance that would give a recursive system:

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Test where

data Thing1 = Thing1 Thing2 Thing2 deriving Eq

newtype Thing2 = Thing2 Thing1 deriving newtype Eq

-- Eq Thing1 = Eq Thing2 u Eq Thing2
-- Eq Thing2 = Eq Thing1 u Coercible Thing2 Thing1

[2] A GND instance that would expand infinitely (but works because of the least-fixed-point simplification):

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Test where

data Proxy a = Proxy

class ShowType a where showType :: Proxy a -> String

data Thing1 a
instance ShowType a => ShowType (Thing1 a) where
  showType _ = "Thing1 " ++ showType (Proxy :: Proxy a)

newtype Weird a = Weird (Thing1 (Weird [a])) deriving newtype ShowType

-- ShowType (Weird a) = ShowType (Thing1 (Weird [a]))
--                    = ShowType (Weird [a])
--                    = ShowType (Thing1 (Weird [[a]]))
--                    = ShowType (Weird [[a]])
--                    ...