Opened 15 months ago
Closed 14 months ago
#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
comment:2 Changed 15 months ago by
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
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
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
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
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
Cc: | Iceland_jack added |
---|
comment:8 Changed 15 months ago by
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
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:11 Changed 15 months ago by
Status: | new → merge |
---|---|
Test Case: | → quantified-constraints/T15334 |
comment:12 Changed 15 months ago by
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
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
Milestone: | 8.6.1 → 8.8.1 |
---|---|
Resolution: | → fixed |
Status: | merge → closed |
Judging from comment:12, this won't make it into 8.6. Punting to 8.8.
Yes. It looks to me like GHC isn't looking under tuples when expanding superclasses.
Really, shouldn't we have
c1
andc2
be superclasses of(c1, c2)
? Then this would be all automatic. Or I've misunderstood something.