[GHC] #15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following code: {{{#!hs {-# 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Read [https://github.com/Gertjan423/ghc-proposals/blob/quantified- constraints/proposals/0000-quantified-constraints.rst 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 => ...`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But this is done for ordinary constraints, right in the parser. Here is s slice of RdrHsSyn: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) | Keywords:
Resolution: | QuantifiedConstraints
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: quantified- valid program | constraints/T15334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => quantified-constraints/T15334 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: quantified- valid program | constraints/T15334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: quantified- valid program | constraints/T15334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: fixed | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: quantified- valid program | constraints/T15334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: merge => closed * resolution: => fixed * milestone: 8.6.1 => 8.8.1 Comment: Judging from comment:12, this won't make it into 8.6. Punting to 8.8. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15334#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC