(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import typechecker labels

Yes. It looks to me like GHC isn't looking under tuples when expanding superclasses.

Really, shouldn't we have c1 and c2 be superclasses of (c1, c2)? Then this would be all automatic. Or I've misunderstood something.

c1 and c2 are already superclasses of (c1, c2). I suspect the issue is not in how constraint tuples are defined, because it I replace the constraint triple in my program with a hand-rolled one:

class    (a, b, c) => CTuple3 a b c
instance (a, b, c) => CTuple3 a b c

deriving instance (forall a. CTuple3 (Functor (WrappedF a))
                                     (Foldable (WrappedF a))
                                     (Traversable (WrappedF a))
                  ) => Traversable SomeF

Then I still get the same error as before.

Read the proposal esp Section 3.2

Would you write

instance (Functor (T a), Traversable (T a), Foldable (T a_)) where ...

No! An instance declaration is for a class, and takes the form

instance blah => C t1 .. tn where ...

where C is a class.

Same with quantified constraints, as the syntax (tries to) make clear.

I suppose that it's accepted because (,,) is a class but really I think it should be rejected.

In fact

instance (Eq (T a), Ord (T a)) where {}

is not rejected out of hand, but elicits

    * No instance for (Ord (T a))
        arising from the superclasses of an instance declaration
    * In the instance declaration for `(Eq (T a), Ord (T a))'

which is pretty confusing. I think it's because (c1, c2) has superclasses c1 and c2.

My conclusion: both in top-level and quantified instances, we should reject a tuple in the head.

OK?

Why are tuples special? After all, the issues persists even if I switch out the tuple for a hand-written class, as shown in ticket:15334#comment:156203.

If the constraint solver was ever faced with

[W] CTuple3 (Functor (WrappedF ty))
            (Foldable (WrappedF ty))
            (Traversable (WrappedF ty)

it'd probably work (although note the tricky overlap with the top level instance). But will the derived instance give rise to that wanted constraint? I think not.

For built-in tuples, I think the constraint solver probably does just decompose them eagerly, rather than look for local instances of tuples. That is special behaviour, I grant you, but I have yet to see a case in which that's not the right thing to do. Where are these strange wanted constraints going to come from?

When I write foo :: (C a, D a b) => a -> b -> a, I'm not thinking that my function expects a given tuple. I'm expecting a given C a and D a b. The parentheses-and-comma are just concrete syntax. I know it's not implemented that way, but that's the programmer's view.

Along similar lines, I would expect forall a b. (C a, D a b) to be shorthand for forall a b. C a and forall a b. D a b. There's really no other sensible interpretation (as you point out), so let's just add this as a special case, just as (C a, D a b) => ... is a special syntax for C a => D a b => ....

I would expect forall a b. (C a, D a b) to be shorthand for forall a b. C a and forall a b. D a b

I agree that there is no other sensible interpretation, but it's a pretty significant implicit rewriting of types. I'm not yet convinced that it pays its way.

But this is done for ordinary constraints, right in the parser. Here is s slice of RdrHsSyn:

checkContext :: LHsType GhcPs -> P ([AddAnn],LHsContext GhcPs)
checkContext (L l orig_t)
  = check [] (L l orig_t)
 where
  check anns (L lp (HsTupleTy _ HsBoxedOrConstraintTuple ts))
    -- (Eq a, Ord b) shows up as a tuple type. Only boxed tuples can
    -- be used as context constraints.
    = return (anns ++ mkParensApiAnn lp,L l ts)                -- Ditto ()
  ...

Sadly, I don't think we can just do this in the parser, as it would really complicate the AST. But then we should perhaps directly reject forall x. ( ... , ... ) as it won't mean what the user wants. I still favor the rewrite, but I think that, failing that, we should error more cleanly.

mentioned in commit fd0f0334

Trac metadata

Trac field	Value
Test case	- → quantified-constraints/T15334

added 1 deleted label

Ryan, how important is this to you? While it is possible to backport this to 8.6, I suspect it will be quite a bit of work. The commit in #15334 (closed) appears to depend quite heavily on 45f44e2c which is a 1 kLoC refactoring which seems to have a slew of dependencies of its own. Unless this is breaking code in the wild I think it would be best to punt this to 8.8.

As far as I can tell, the commit in #15334 (closed) only improves error messages, so I don't think it's critical for 8.6.

closed

changed milestone to %8.8.1

removed 1 deleted label

Judging from ticket:15334#comment:156702, this won't make it into 8.6. Punting to 8.8.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added 1 deleted label

added QuantifiedConstraints label

added Pnormal label

mentioned in issue #17025 (closed)

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

(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)

Child items ...

Activity