[GHC] #14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} data D c where D :: c => D c proof :: (forall xx. f xx) => D (f a) proof = D }}} Running this program with [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:28 wip/T2893] gives {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 174-quantifiedconstraints.hs, interpreted ) 174-quantifiedconstraints.hs:9:9: error: • Could not deduce: f a arising from a use of ‘D’ from the context: forall xx. f xx bound by the type signature for: proof :: forall (f :: * -> Constraint) a. (forall xx. f xx) => D (f a) at 174-quantifiedconstraints.hs:8:1-37 • In the expression: D In an equation for ‘proof’: proof = D • Relevant bindings include proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1) | 9 | proof = D | ^ }}} How can I instantiate `xx` to `a`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedContexts Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * keywords: => QuantifiedContexts -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedContexts wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * keywords: QuantifiedContexts => QuantifiedContexts wipT2893 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedContexts wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Currently this is by-design, but we could change the design. These forall-constraints currently behave just like a local version of a top-level instance declaration, and those are all for classes. You can't say {{{ instance ... => f Int }}} although it'd make sense to do so. So similarly you currently can't do that with the local-foralld constraints. * If we retain the restriction to class constraints only, we should reject the type signature with a civilised error message. * How bad is the restriction? You can always say {{{ class f a => C f a proof :: (forall xx. C f xx) => D (f a) }}} Would that do? Or what do your use-cases look like? It'd be a moderate pain to generalise the facility, mainly because `InstEnv` (in which we look up instances) has class constraints as a deeply-baked-in assumption. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: QuantifiedContexts wipT2893 => QuantifiedConstraints, wipT2893 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by sjoerd_visscher): How about adding the workaround internally? I.e. add {{{ class c => SomeInteralClass c instance c => SomeInternalClass c }}} and translate `(forall xx. f xx)` to `(forall xx. SomeInternalClass (f xx))` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Only moderate? ;-) I have listed some things this rules out as Phabricator comments: * ([https://phabricator.haskell.org/D4353#121416 Phab]) A (categorical) vocabulary for constraints: `uncurry :: (a => b => c) :- ((a, b) => c)` * ([https://phabricator.haskell.org/D4353#121383 Phab]) Defining `(>>=) @(Free cls)` needs a `cls` instance for `Free cls b` but it can't range over `b`. {{{#!hs newtype Free cls a = Free (forall xx. cls xx => (a -> xx) -> xx) bind :: cls (Free cls b) => Free cls a -> (a -> Free cls b) -> Free cls b bind (Free free) f = free f }}} Instead: {{{#!hs instance (forall xx. cls (Free cls xx)) => Monad (Free cls) }}} * ([https://phabricator.haskell.org/D4353#121403 Phab]) Works: but what we really want is an instance of `Free mon` for any `forall xx. Monoid xx => mon xx` {{{#!hs instance Foldable (Free Monoid) where foldMap :: Monoid m => (a -> m) -> (Free Monoid a -> m) foldMap f (Free free) = free f instance Foldable (Free Monoid) where foldMap :: Monoid m => (a -> m) -> (Free Monoid a -> m) foldMap f (Free free) = free f }}} Your `class f a => C f a` solution didn't work for me (using latest version): here is my [https://gist.github.com/Icelandjack/6b42e7e19c7f130f2ca947495e09ca54 full code and error messages]. Echoing Sjoerd if there is a mechanical translation `class f a => C f a` can GHC do it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:3 simonpj]:
Currently this is by-design, but we could change the design.
I'm +1 on change but that's easy to say, is it a task that takes deep GHC knowhow?
How bad is the restriction?
Hard to say. If it's a matter of encoding them class aliases then it is a huge improvement over the current situation, otherwise may rule out a lot of fun examples. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:5 sjoerd_visscher]:
How about adding the workaround internally? I.e. add
{{{ class c => SomeInteralClass c instance c => SomeInternalClass c }}}
and translate `(forall xx. f xx)` to `(forall xx. SomeInternalClass (f xx))`
That's one idea. But does that idea even work if you write it out by hand? I tried: {{{#!hs {-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} {-# Language FlexibleInstances #-} {-# Language UndecidableInstances #-} {-# Language UndecidableSuperClasses #-} class c => SomeInternalClass c instance c => SomeInternalClass c data D c where D :: c => D c proof :: (forall xx. SomeInternalClass (f xx)) => D (f a) proof = D }}} But that fails with: {{{ Bug.hs:15:9: error: • Could not deduce: f a arising from a use of ‘D’ from the context: forall xx. SomeInternalClass (f xx) bound by the type signature for: proof :: forall (f :: * -> Constraint) a. (forall xx. SomeInternalClass (f xx)) => D (f a) at Bug.hs:14:1-57 • In the expression: D In an equation for ‘proof’: proof = D • Relevant bindings include proof :: D (f a) (bound at Bug.hs:15:1) | 15 | proof = D | ^ }}} Granted, it does work if you change the `proof` to: {{{#!hs proof :: (forall xx. SomeInternalClass (f xx)) => D (SomeInternalClass (f a)) proof = D }}} But that would require pervasively inserting `SomeInternalClass` everywhere in your program, and not just on the quantified constraints which lack an explicit type class constructor. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I have fixed this (on branch `wip/TT2893`); and updated the proposal to reflect it Would you like to try now? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Thank you! I played with it yesterday and it works great with a few kinks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Great! Keep identifying the kinks; it's extremely helpful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed Comment: This featurette was fixed in c477f53799deb46b4987ac788ad67d1bcbb8eb0c. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: QuantifiedConstraints, wipT2893 => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC