[GHC] #14879: QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias
#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 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 compiles fine {{{#!hs {-# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, GADTs, TypeOperators #-} class (a => b) => Implies a b instance (a => b) => Implies a b data Dict c where Dict :: c => Dict c type a :- b = Dict (Implies a b) class (forall xx. Implies b xx => Implies a xx) => Yo a b instance (forall xx. Implies b xx => Implies a xx) => Yo a b yo :: Yo a b :- Implies a b yo = Dict }}} until you replace `(=>)` with `Implies` (which should be fine?) {{{#!hs class (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b instance (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b }}} and the error message blows up {{{ $ ghci -ignore-dot-ghci SD.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( SD.hs, interpreted ) SD.hs:15:6: error: • Reduction stack overflow; size = 201 When simplifying the following type: Implies b (Implies b (Implies -->8---->8----several-hundred-lines---->8---->8---- b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) • In the expression: Dict In an equation for ‘yo’: yo = Dict | 15 | yo = Dict | ^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14879 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 Iceland_jack): For context this was to encode [https://hackage.haskell.org/package/kan- extensions-5.1/docs/Data-Functor-Yoneda.html Yoneda ((->) a) b] with constraints {{{#!hs newtype Yoneda f b = Yoneda (forall xx. (b -> xx) -> f xx) type Yo a b = Yoneda ((->) a) b lower :: forall a b. (Yo a b) -> (a -> b) lower (Yoneda yoneda) = yoneda (id @b) lift :: (a -> b) -> (Yo a b) lift f = Yoneda (. f) }}} ---- Replying to [comment:1 simonpj]:
Iceland Jack! You are torturing me.
Think of it as enhanced bug reporting In this particular case the fluke does a good thing, it behaves like the `lower` function where instead of applying to the identity function `(id @b)` the constraint solver conjures up the identity constraint `(Implies b b)`.
If we expanded more vigorously, the fluke would happen both times. I'm not sure how hard to work on this.
I'm ok with the looping situation. Would the hypothetical change make `Implies` behave more like `=>`? Making them substitutable ''may'' be a desirable property That being said! The current implementation is very impressive. If something seem unworkable there is surprisingly often some way to guide (trick) GHC into accepting it ([https://gist.github.com/Icelandjack/aeda8e98214cc52c96230af7b8724d25 quantifying over TFs], [https://ghc.haskell.org/trac/ghc/ticket/14878#comment:2 overlap], [https://gist.github.com/Icelandjack/93cf64878e286ed6378adf8fc0e7c200 overlap]). I hope that doesn't change :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14879#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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):
The current implementation is very impressive. If something seem unworkable there is surprisingly often some way to guide (trick) GHC into accepting it
Well that is good news, thanks. I hope you are going to write a paper to explain the uses of quantified constraints; and in there we can explore the boundaries and he way to guide GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14879#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 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/14879#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC