Instance constraints should be used when deriving on associated data types

Consider this program:

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}

class Eq (Associated a) => Foo a where
    data Associated a

instance Foo a => Foo (Maybe a) where
    data Associated (Maybe a) = AssociatedMaybe (Associated a)
                              deriving (Eq)

This does not compile, giving this error message:

/Users/mbolingbroke/Junk/Repro.hs:9:40:
    No instance for (Eq (Associated a))
      arising from the 'deriving' clause of a data type declaration
                   at /Users/mbolingbroke/Junk/Repro.hs:9:40-41
    Possible fix:
      add an instance declaration for (Eq (Associated a))
      or use a standalone 'deriving instance' declaration instead,
         so you can specify the instance context yourself
    When deriving the instance for (Eq (Associated (Maybe a)))

However, this is surprising because I clearly state that a is Foo, and hence (Associated a) has an Eq instance by the superclass constraint on Foo.

If I point this out explicitly using standalone deriving it works:

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving, FlexibleInstances #-}

class Eq (Associated a) => Foo a where
    data Associated a

instance Foo a => Foo (Maybe a) where
    data Associated (Maybe a) = AssociatedMaybe (Associated a)
--                              deriving (Eq)

deriving instance Foo a => Eq (Associated (Maybe a))

So I think the default behaviour for "deriving" on an associated data family should be to include the constraints from the enclosing instance. For now the workaround is just to use standalone deriving.

Trac metadata

Trac field	Value
Version	6.12.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request Trac import labels

It's not clear that you always want this. Suppose your data decl was

instance Foo a => Foo (Maybe a) where
    data Associated (Maybe a) = AssociatedMaybe a
                              deriving (Eq)

Here, Eq a would be enough. Wouldn't you expect this

instance Eq a => Eq (Associated (Maybe a))

rather than

instance Foo a => Eq (Associated a)

? Maybe standalone deriving is the Right Way, not just a workaround.

But if you ever have a value of type "Associated (Maybe a)" then you pretty much know that there must be a "Foo a" instance by looking at the "Foo (Maybe a)" instance. So you aren't losing much generality in practice by requiring that stronger constraint, rather than the weaker Eq constraint.

(I haven't tried it, but perhaps it's possible to add new instances to an associated data family outside of the instance itself? In which case the logic above is not valid, but since this is a rather uncommon use case I don't think this should argue against my proposed behaviour change. And anyway if you know the weaker constraint is enough and you *really want* to use it because you're going to extend the data family outside an instance itself for some reason, then you can use standalone deriving with the weaker constraint)

It seems to me that just using the instances' constraints is a reasonable thing to do by default, as it stands the very best change of allowing deriving to work. I personally prefer a more reliable deriving mechanism to one that works less often but when it does, generates more general type class instances.

(BTW, personally I find it slightly surprising that you can even mention the type "Associated a" without mentioning "Foo a" in your type signature, though I can kind of see the reasoning)

changed milestone to %7.2.1

changed milestone to %7.6.1

changed weight to 3

Trac metadata

Trac field	Value
Priority	normal → low

changed milestone to %7.6.2

changed milestone to %7.10.1

Moving to 7.10.1.

removed milestone

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

changed milestone to %8.0.1

Milestone renamed

I feel like batterseapower is arguing for a change in the way associated family instances work at a fundamental level. To illustrate what I mean, consider this code:

{-# LANGUAGE TypeFamilies #-}

class C a where
  data D a
  c :: a -> a -> Bool

instance Eq a => C [a] where
  newtype D [a] = DList [a]
  c = (==)

dlist :: D [a]
dlist = DList []

Notice that I was able to construct a value of type D [a] without needing an Eq a constraint! That flies in the face of the fact that the C [a] instance does seem to require an Eq a constraint—rather, it requires an Eq a constraint, but only when typechecking its associated methods.

For better or worse, the D [a] family instance appears to be pretty much independent of the C [a] instance (and its methods).

So if we accept batterseapower's proposal above and propagate class constraints down to the associated family instances as well, would it be correct to say that my example code would now fail to typecheck? Is this desirable behavior? I don't really understand the intricacies of associated family instances that well, so perhaps there is a reason that the current design is the way it is. I'd need Simon's judgment to know for sure.

I think Max was asking for something less fundamental. He just wanted the deriving clause on the original instance decl to infer an instance context of Eq (Associated a). That's usually not allowed for deriving clauses but he argues that in the context of a class instance decl, it should.

So it's just to do with the relatively narrow question of "what context does one infer for a deriving clause?".

Since the standalone deriving clause is available, I'm inclined to say "use the standalone route". It's just clearer. But I'm not terribly bothered.

I would also be inclined to say "use the standalone route", for the reason that I don't see any reason why the deriving clause would infer Eq (Associated a) given the current state of things. I was merely imagining a hypothetical scenario in which data family instances //would// reasonable infer such a constraint when deriving instances. If data family instances were more tightly intermingled with their parent instances in terms of instance contexts, I could envision this being the case.

P.S. Do you know why GHC decides DList [] :: D [a] instead of DList [] :: Eq a => D [a]? That is, why GHC chose to make associated data family instance contexts separate from their parent instances' contexts?

Can data family (or type family) instances even have contexts? What is that supposed to mean?

What I mean is: if you had this code (using the example in ticket:4815#comment:126587):

c' :: [a] -> [a] -> Bool
c' = c

then it would fail to typecheck, as there's no Eq a constraint, as mandated by the context in instance Eq a => C [a]. What I am asking is simply: should this Eq a constraint also be required for the associated family instances as well? That is, should this typecheck, even though it has no Eq a constraint?

dlist :: D [a]
dlist = DList []

(Currently, it //does// typecheck.)

I would expect it to type check, because an associated family instance is sugar for an ordinary data family instance and I can't understand what it would mean to put a constraint on such an instance (or why I would want to; it feels like the old datatype contexts).

Ah, the comparison to -XDatatypeContexts is definitely a compelling argument for the current behavior. I'll quit my job as devil's advocate, then.

In that case, that cements my opinion that associated data family instances should be totally unrelated to the instance context of the parent instance, and moreover, that the bug is really just a duplicate of #11008 in disguise, as the fix for this issue would be improving GHC's ability to infer exotic constraints.

Should we close it?

I think it's more than just #11008.

The question of this ticket is just "what context should GHC infer for a 'deriving' clause." But the ticket concerns the specific case of a data instance inside a class instance decl, thus:

instance <context> => C (T a b) where
  data D (T a b) = D1 a | D2 b

Now arguably, whether or not the deriving Eq part needs <context> it would do no harm to add it, so we get the derived instance

instance <context> => Eq (DT a b) where
 (==) = <blah>

(where DT is the representation data type for D (T a b)). The point is that <context> might help satisfy the Eq constraints arising from <blah>.

Max argues that <context> must already be satisfied (because the class instance holds). But that's not really true

f x y = D1 x == D2 y

Here we need equality on DT but we don't need C (T a b). So <context> might be over-constraining.

So I'm unconvinced that this is worth the bother.

Replying to [ticket:4815#comment:126622 simonpj]:

So I'm unconvinced that this is worth the bother.

I completely agree, not only because it might be over-constraining, but in some cases it might even yield redundant constraints, as in this example:

{-# LANGUAGE TypeFamilies #-}

class C a where
  data D a
  c :: a -> a -> Bool

instance Eq a => C [a] where
  newtype D [a] = DList [a] deriving Show
  c = (==)

This would, under the proposal in this ticket, yield:

instance (Eq a, Show a) => Show (D [a])

which isn't what we want at all.

mentioned in issue #12863 (closed)

See also #12863 (closed) for another occurrence of this design question.

Trac metadata

Trac field	Value
Related	- → #12863 (closed)

added deriving label

mentioned in issue #14462 (closed)

closed

I'm going to close this, since:

1. The consensus appears to be that this isn't desirable.
2. We're operating under this consensus in other tickets (see #14462 (closed), for example).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid
Related	#12863 (closed) → #12863 (closed), #14462 (closed)

added Plow label