#15334 closed bug (fixed)

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: quantified-constraints/T15334
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider the following code:

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind

type family F a :: Type -> Type
newtype WrappedF a b = WrapF (F a b)
deriving instance Functor (F a) => Functor (WrappedF a)
deriving instance Foldable (F a) => Foldable (WrappedF a)
deriving instance Traversable (F a) => Traversable (WrappedF a)

data SomeF b = forall a. MkSomeF (WrappedF a b)

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

This typechecks. However, the last Traversable SomeF is a bit unfortunate in that is uses three separate forall a.s. I attempted to factor this out, like so:

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

But then the file no longer typechecked!

$ /opt/ghc/8.6.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

Foo.hs:21:1: error:
    • Could not deduce (Functor (F a))
        arising from the superclasses of an instance declaration
      from the context: forall a.
                        (Functor (WrappedF a), Foldable (WrappedF a),
                         Traversable (WrappedF a))
        bound by the instance declaration at Foo.hs:(21,1)-(24,52)
    • In the instance declaration for ‘Traversable SomeF’
   |
21 | deriving instance (forall a. ( Functor (WrappedF a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Foo.hs:21:1: error:
    • Could not deduce (Foldable (F a))
        arising from the superclasses of an instance declaration
      from the context: forall a.
                        (Functor (WrappedF a), Foldable (WrappedF a),
                         Traversable (WrappedF a))
        bound by the instance declaration at Foo.hs:(21,1)-(24,52)
    • In the instance declaration for ‘Traversable SomeF’
   |
21 | deriving instance (forall a. ( Functor (WrappedF a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Foo.hs:21:1: error:
    • Could not deduce (Traversable (F a1))
        arising from a use of ‘traverse’
      from the context: forall a.
                        (Functor (WrappedF a), Foldable (WrappedF a),
                         Traversable (WrappedF a))
        bound by the instance declaration at Foo.hs:(21,1)-(24,52)
      or from: Applicative f
        bound by the type signature for:
                   traverse :: forall (f :: * -> *) a b.
                               Applicative f =>
                               (a -> f b) -> SomeF a -> f (SomeF b)
        at Foo.hs:(21,1)-(24,52)
    • In the second argument of ‘fmap’, namely ‘(traverse f a1)’
      In the expression: fmap (\ b1 -> MkSomeF b1) (traverse f a1)
      In an equation for ‘traverse’:
          traverse f (MkSomeF a1) = fmap (\ b1 -> MkSomeF b1) (traverse f a1)
      When typechecking the code for ‘traverse’
        in a derived instance for ‘Traversable SomeF’:
        To see the code I am typechecking, use -ddump-deriv
   |
21 | deriving instance (forall a. ( Functor (WrappedF a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Richard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.

Change History (14)

comment:1 Changed 15 months ago by goldfire

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.

comment:2 Changed 15 months ago by RyanGlScott

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.

comment:3 Changed 15 months ago by simonpj

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?

comment:4 Changed 15 months ago by RyanGlScott

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

comment:5 Changed 15 months ago by simonpj

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?

comment:6 Changed 15 months ago by goldfire

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

comment:7 Changed 15 months ago by Iceland_jack

Cc: Iceland_jack added

comment:8 Changed 15 months ago by simonpj

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.

comment:9 Changed 15 months ago by goldfire

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.

comment:10 Changed 15 months ago by Simon Peyton Jones <simonpj@…>

In fd0f0334/ghc:

More refactoring in TcValidity

This patch responds to Trac #15334 by making it an error to
write an instance declaration for a tuple constraint like
(Eq [a], Show [a]).

I then discovered that instance validity checking was
scattered betweeen TcInstDcls and TcValidity, so I took
the time to bring it all together, into
  TcValidity.checkValidInstHead

In doing so I discovered that there are lot of special
cases.   I have not changed them, but at least they are
all laid out clearly now.

comment:11 Changed 15 months ago by simonpj

Status: newmerge
Test Case: quantified-constraints/T15334

comment:12 Changed 15 months ago by bgamari

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 comment:10 appears to depend quite heavily on 45f44e2c9d5db2f25c52abb402f197c20579400f 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.

comment:13 Changed 15 months ago by RyanGlScott

As far as I can tell, the commit in comment:10 only improves error messages, so I don't think it's critical for 8.6.

comment:14 Changed 14 months ago by RyanGlScott

Milestone: 8.6.18.8.1
Resolution: fixed
Status: mergeclosed

Judging from comment:12, this won't make it into 8.6. Punting to 8.8.

Note: See TracTickets for help on using tickets.