[GHC] #14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This works with the [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest change to the -XQuantifiedConstraints branch]. {{{#!hs {-# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #-} class (forall xx. (xx => a) => Implies xx b) => F a b instance (forall xx. (xx => a) => Implies xx b) => F a b class (a => b) => Implies a b instance (a => b) => Implies a b }}} but replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket. {{{#!hs class (forall xx. (xx => a) => (xx => b)) => F a b instance (forall xx. (xx => a) => (xx => b)) => F a b -- $ ghci -ignore-dot-ghci /tmp/ASD.hs -- GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted ) -- -- /tmp/ASD.hs:4:10: error: -- • Could not deduce: xx0 -- arising from the superclasses of an instance declaration -- from the context: forall (xx :: Constraint). (xx => a, xx) => b -- bound by the instance declaration at /tmp/ASD.hs:4:10-53 -- or from: (xx => a, xx) -- bound by a quantified context at /tmp/ASD.hs:1:1 -- • In the instance declaration for ‘F a b’ -- | -- 4 | instance (forall xx. (xx => a) => (xx => b)) => F a b -- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Failed, no modules loaded. -- Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14877 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)' -------------------------------------+------------------------------------- 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 Iceland_jack): * version: 8.2.2 => 8.5 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14877#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)' -------------------------------------+------------------------------------- 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): Consider the quantified constraint (QC) in {{{ instance (forall xx. (xx => a) => Implies xx b) => F a b }}} It serves as a local instance declaration. To construct the dictionary for `(F a b)` I may need to to solve a constraint `(Implies xx b)`. The QC says "if you want to solve `Implies xx b`, then it suffices to prove `xx => a`". And to prove `xx => a`, the built-in rules assume `xx` and try to prove `a`. It's quite different to say {{{ instance (forall xx. (xx => a) => (xx => b) => F a b }}} That is precisely equivalant to {{{ instance (forall xx. (xx => a, xx) => b) => F a b }}} Now the QC says "if you want to solve the goal `b`, then conjure up some constraint `xx`, and prove `(xx => a, xx)`. But how can we guess `xx`? Each QC has an instance "head", usually headed by a type constructor, sometimes by a type variable. That head is the pattern the QC can solve. `Implies xx b` is a good instance head: it matches things of that form. Plain `b` is not a good instance head! In short, I see nothing wrong here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14877#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | 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/14877#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC