Should GND infer an instance context when deriving method-free classes?

This is a design question that emerged from code that I originally discovered here and here. To recap, it's now possible to have code like this:

{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}
class C a where
  type T a

newtype Identity a = Identity a deriving C

Compiling this (with -Wredundant-constraints) generates this code:

instance C a => C (Identity a) where
  type T (Identity a) = T a

But now GHC will complain:

• Redundant constraint: C a
• In the instance declaration for ‘C (Identity a)’

This warning makes sense from the perspective that the C a constraint isn't ever used by the associated type family instance. So the question arises: should GND avoid generating an instance context for the representation type in the event it's deriving a class with no methods?

Fortunately, patching GHC to do this is trivial:

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 4722f16..df2d3d5 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -1272,7 +1272,8 @@ mkNewTypeEqn dflags overlap_mode tvs
             [ let (Pair t1 t2) = mkCoerceClassMethEqn cls dfun_tvs inst_tys rep_inst_ty m
               in mkPredOrigin (DerivOriginCoerce meth t1 t2) TypeLevel
                               (mkReprPrimEqPred t1 t2)
-            | meth <- classMethods cls ]
+            | meth <- meths ]
+        meths = classMethods cls
 
                 -- If there are no tyvars, there's no need
                 -- to abstract over the dictionaries we need
@@ -1281,7 +1282,11 @@ mkNewTypeEqn dflags overlap_mode tvs
                 --              instance C T
                 -- rather than
                 --              instance C Int => C T
-        all_preds = rep_pred_o : coercible_constraints ++ sc_theta -- NB: rep_pred comes 
+        all_preds = if null meths then [] else [rep_pred_o]
+                    -- See Note [GND and method-free classes]
+                       ++ coercible_constraints
+                       ++ sc_theta
+                       -- NB: rep_pred_o comes first
 
         -------------------------------------------------------------------
         --  Figuring out whether we can only do this newtype-deriving thing

After implementing this patch, I ran the testsuite, and there were some surprising results. One thing that shocked me was that the program reported in #6088 (closed), which had previously failed due to a patch resulting from #8984 (closed), was now passing!

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}  
{-# LANGUAGE EmptyDataDecls #-}

module T6088 where

class C a

newtype A n = A Int

type family Pos n
data True

instance (Pos n ~ True) => C (A n)

newtype B n = B (A n) deriving (C)

That is because previously, GHC was trying to generate an instance like this:

instance (Pos n ~ True) => C (B n)

And this was rejected, since we don't infer exotic equality constraints when deriving. But with this patch, it now generates:

instance {- Empty context => -} C (B n)

Which is certainly valid. But is it what a user would expect? I'm not so sure.

As hvr notes in #11369, sometimes empty classes are used to enforce invariants, like in the following case:

class Throws e

readFoo :: Throws IOError => FilePath -> IO Foo
readFoo fn = {- ...  -}

What if you wanted to have a Throws instance for a newtype? You'd probably want something like this:

newtype Id a = MkId a

instance Throws a => Throws (Id a)

Which feels like something GND should be able to take care of with ease. But to your surprise, you try this:

newtype Id a = MkId a
  deriving Throws

And now GHC generates not the instance above, but rather just:

instance Throws (Identity a)

So it's possible that we would lose some of the expressiveness of GND by implementing this change. Is that acceptable? I'm not sure, so I though I'd solicit feedback here.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture