#14879: QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias -------------------------------------+------------------------------------- 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): Iceland Jack! You are torturing me. Here is what is happening. To deal with `yo` we want to solve {{{ [W] Implies (Yo a b) (Implies a b) }}} We proceed as follows {{{ [W] Implies (Yo a b) (Implies a b) ===> (apply instance) [W] (forall {}. Yo a b => Implies a b) -- A quantified constraint ===> build implication constraint forall {}. [G] Yo a b => [W] Implies a b }}} So we have a Given constraint `[G] Yo a b`. So we expand its superclasss giving {{{ [G] (forall xx. Implies (Implies b xx) (Implies a xx)) }}} and try solving {{{ forall {}. [G] Yo a b [G] (forall xx. Implies (Implies b xx) (Implies a xx)) => [W] Implies a b }}} Ok... now we return attention to that Wanted and try to solve it. Use the top level instance! Gives us {{{ forall {}. [G] Yo a b [G] (forall xx. Implies (Implies b xx) (Implies a xx)) => [W] Implies a b ===> (top level instance) forall {}. [G] Yo a b [G] (forall xx. Implies (Implies b xx) (Implies a xx)) => [W] (a => b) ===> (build implication constraint) forall {}. [G] Yo a b [G] (forall xx. Implies (Implies b xx) (Implies a xx)) => forall {}. [G] a => [W] b }}} Now we seem to be stuck so we expand another layer of superclasses. We can take the superclasses of that quantified constraint (as in [https://github.com/Gertjan423/ghc-proposals/blob/quantified- constraints/proposals/0000-quantified-constraints.rst Section 3.4 of the proposal]) giving us {{{ forall {}. [G] Yo a b [G] (forall xx. Implies (Implies b xx) (Implies a xx)) [G] (forall xx. Implies b xx => Implies a xx) --- Next superclass => forall {}. [G] a => [W] b }}} We are still stuck, so expand sueprclasses again: {{{ forall {}. [G] Yo a b [G] (forall xx. Implies (Implies b xx) (Implies a xx)) [G] (forall xx. Implies b xx => Implies a xx) [G] (forall xx. Implies b xx => a => xx) --- Next superclass => forall {}. [G] a => [W] b }}} And now we are in a very bad place. We have a Given quantified constraint that lets us solve ANY constraint `xx` (for any `xx`!). But in solving it, we just get another bigger problem to solve. So solving diverges. I hvae no idea what you are trying to do, but GHC seems to be behaving quite reasonably. Why does it "work" you have `=>` instead of `Implies` in the superclass for `Yo`? (The instance for `Yo` is irrelevant; just delete it.) By a fluke. We get as before {{{ forall {}. [G] Yo a b => [W] Implies a b }}} But we expand the given superclasses layer by layer, so before trying to solve the Wanted we get {{{ forall {}. [G] Yo a b [G] (forall xx. Implies b xx => Implies a xx) -- Superclass! => [W] Implies a b }}} Now it just happens that the wanted matches the quantified constraint, we can apply that local instance decl giving `[W] Implies b b` which we can solve. ---------------- There are several difficulties here. * First, your setup is weird. If you expand superclasses enough, you get to prove any constraint whatsoever, and that is plainly stupid. * I don't like flukes. Maybe we should not make use the local instance (quantified constraint) if the constraint we are solving also matches a global instance. Curerntly we make the local ones "shadow" the global ones. * The superclass expansion is a bit less aggressive than I expected; I'm not sure why. If we expanded more vigorously, the fluke would happen both times. I'm not sure how hard to work on this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14879#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler