#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