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 follow-up: 2 Changed 18 months ago by
comment:2 Changed 18 months ago by
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
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
Keywords: | wipT2893 removed |
---|
Iceland Jack! You are torturing me. Here is what is happening.
To deal with
yo
we want to solveWe proceed as follows
So we have a Given constraint
[G] Yo a b
. So we expand its superclasss givingand try solving
Ok... now we return attention to that Wanted and try to solve it. Use the top level instance! Gives us
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
We are still stuck, so expand sueprclasses again:
And now we are in a very bad place. We have a Given quantified constraint that lets us solve ANY constraint
xx
(for anyxx
!). 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 ofImplies
in the superclass forYo
? (The instance forYo
is irrelevant; just delete it.) By a fluke. We get as beforeBut we expand the given superclasses layer by layer, so before trying to solve the Wanted we get
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.