Opened 19 months ago

Last modified 16 months ago

#14879 new bug

QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This compiles fine

{-# 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?)

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> 

Change History (4)

comment:1 Changed 18 months ago 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 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.

comment:2 in reply to:  1 Changed 18 months ago by Iceland_jack

For context this was to encode Yoneda ((->) a) b with constraints

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 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 (quantifying over TFs, overlap, overlap). I hope that doesn't change :)

comment:3 Changed 18 months ago 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.

comment:4 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.