Opened 9 years ago

Closed 22 months ago

#4815 closed feature request (invalid)

Instance constraints should be used when deriving on associated data types

Reported by: batterseapower Owned by:
Priority: low Milestone:
Component: Compiler Version: 6.12.3
Keywords: deriving Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12863, #14462 Differential Rev(s):
Wiki Page:

Description

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.

Change History (21)

comment:1 Changed 9 years ago by simonpj

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.

comment:2 Changed 9 years ago by batterseapower

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)

comment:3 Changed 9 years ago by igloo

Milestone: 7.2.1

comment:4 Changed 8 years ago by igloo

Milestone: 7.4.17.6.1
Priority: normallow

comment:5 Changed 7 years ago by igloo

Milestone: 7.6.17.6.2

comment:6 Changed 5 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:7 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

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.

comment:8 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:9 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:10 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

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.

comment:11 Changed 3 years ago by simonpj

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.

comment:12 Changed 3 years ago by RyanGlScott

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?

comment:13 Changed 3 years ago by rwbarton

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

comment:14 Changed 3 years ago by RyanGlScott

What I mean is: if you had this code (using the example in comment:10):

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.)

comment:15 Changed 3 years ago by rwbarton

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).

comment:16 Changed 3 years ago by RyanGlScott

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?

comment:17 Changed 3 years ago by simonpj

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.

comment:18 in reply to:  17 Changed 3 years ago by RyanGlScott

Replying to 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.

comment:19 Changed 3 years ago by RyanGlScott

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

comment:20 Changed 2 years ago by RyanGlScott

Keywords: deriving added

comment:21 Changed 22 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

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, for example).
Note: See TracTickets for help on using tickets.