# 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]])
-- ...
```