Puzzling "Reduction stack overflow" error message
Hello Haskell Cafe, I almost feel guilty for posting this since I almost never read messages from this list. But I guess others do and do so because they want to so it's an asymmetry that is fine, and which probably won't be like that forever (I'll get to reading them again at a different stage of my life I'm feeling better). I also have very bad experience with asking "complex" Haskell questions in Stack Overflow, with people either not replying or replying stuff that indicates they did not understand the question. Digression aside, I have encountered this error before and it is a nasty one, but this time I am just wildly puzzled by what it's trying to tell me. This is part of a very large program (and I think the huge stack of types and instances is what is hiding the problem here), but I'll try to condense it into a small bit. The following function I have is the one that throws the error: resolve_to_constraints_metacnf :: SOMetaSignature -> SOMetaCNF -> Computation (Maybe SOMetaUnifSystem) resolve_to_constraints_metacnf sig cnf = result where f1 = (ADDirect <$>) :: SOMetaliteral -> SOMetaUnifLiteral; f2 = (f1 <$>) :: [SOMetaliteral] -> [SOMetaUnifLiteral]; f3 = (f2 <$>) :: [[SOMetaliteral]] -> [[SOMetaUnifLiteral]]; ucnf = f3 cnf :: [[SOMetaUnifLiteral]]; resolved = res_computeresolve SOResGreedyFactorH ucnf :: StateT uv Computation (Maybe SOMetaUnifSystem); runstated = runStateT resolved (UnifVar 0); result = fst <$> runstated The error starts as follows: Reduction stack overflow; size = 201 When simplifying the following type: Eq OFunction The rest is the standard for this type of errors. OFunction does not appear explicitly on my function signature, but if we look at the definitions of SOMetaSignature, SOMetaCNF, SOMetaLiteral, SOMetaUnifLiteral and SOMetaUnifSystem, we see they are type aliases for parameterised types, all of which include OFunction as one of their parameters. Here's an example: type SOMetaUnifLiteral = Literal (AtomDependant CAtomPF CTermF LambdaCNF SOPredicate OPredicate OFunction OVariable SOAMVariable SOMVariable UnifVariable) (Yes, I know how tedious it is to have so many type parameters, tell me about it). And perhaps also relevantly, this is the signature of res_computeresolve (which type checks): res_computeresolve :: (ResLiteral l r mt, Heuristics h [Literal l] () (ResStep l) m) => h -> [[Literal l]] -> mt m (Maybe r) (note, might be relevant, that ResLiteral requires mt to be a MonadTrans and MFunctor, which StateT, the type it gets instantiated to in the calling function, is. m gets instantiated to Computation which is a Monad I implemented myself (and works fine).) Now, the natural thing to think is to track the Constraints to find which one is asking for an Eq OFunction and how that works. It definitely is a constraint that I use all over the place. But, here is the puzzling thing. Eq OFunction is clearly implemented. OFunction is a really simple type. Here is the basic definition: data OFunction = OFun Int Int deriving (Eq, Ord) So, why is it having such a hard time proving Eq OFunction, if it is a really simple type with a derived instance of Eq (which has worked thus far without any issues)? My suspicion is that the message is bugged, and the stack overflow is not on that specific instance, but rather on some type variable on a larger instance that it can never entirely instantiate no matter how many constraints it resolves. This is why I added those inline type signatures to the triple fmap, to try to help GHC know what the types should look like. But I am still getting the error, and I really don't know what else to do now. Sorry for the long message, but since I don't know where the error is coming from, I wanted to give some context, and my entire program is tens of thousands of lines of codes by now... I hope people are able to skim and find the relevant bit that tells them what's likely the stupid mistake I am making. Thanks in advance, Juan. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
On Sun, Jan 24, 2021 at 03:15:24AM +0000, CASANOVA Juan wrote:
The following function I have is the one that throws the error:
resolve_to_constraints_metacnf :: SOMetaSignature -> SOMetaCNF -> Computation (Maybe SOMetaUnifSystem) resolve_to_constraints_metacnf sig cnf = result where f1 = (ADDirect <$>) :: SOMetaliteral -> SOMetaUnifLiteral; f2 = (f1 <$>) :: [SOMetaliteral] -> [SOMetaUnifLiteral]; f3 = (f2 <$>) :: [[SOMetaliteral]] -> [[SOMetaUnifLiteral]]; ucnf = f3 cnf :: [[SOMetaUnifLiteral]]; resolved = res_computeresolve SOResGreedyFactorH ucnf :: StateT uv Computation (Maybe SOMetaUnifSystem); runstated = runStateT resolved (UnifVar 0); result = fst <$> runstated
The error starts as follows:
Reduction stack overflow; size = 201 When simplifying the following type: Eq OFunction
This error is reported by: solverDepthErrorTcS :: CtLoc -> TcType -> TcM a solverDepthErrorTcS loc ty = setCtLocM loc $ do { ty <- zonkTcType ty ; env0 <- tcInitTidyEnv ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty) tidy_ty = tidyType tidy_env ty msg = vcat [ text "Reduction stack overflow; size =" <+> ppr depth , hang (text "When simplifying the following type:") 2 (ppr tidy_ty) , note ] ; failWithTcM (tidy_env, msg) } where depth = ctLocDepth loc note = vcat [ text "Use -freduction-depth=0 to disable this check" , text "(any upper bound you could choose might fail unpredictably with" , text " minor updates to GHC, so disabling the check is recommended if" , text " you're sure that type checking should terminate)" ] Have you tried "-freduction-depth=0"? Does that "terminate"? -- Viktor.
"Have you tried "-freduction-depth=0"? Does that "terminate"?"
I had not before you said it. While there is a long tower of constraints, there are no recursive ones that I know of that might drastically increase the depth so I was inclined, by the heuristic that normally just going deeper doesn't solve this kind of problems, not to do it.
But I have now, since when you said it I realized it was definitely something to try.
I have tried with -freduction-depth=20000, and it still fails (with the same Eq OFunction constraint).
With -freduction-depth=1000000 or -freduction-depth=0, it does not terminate within a minute or two.
So it does look like there is some infinite depth going on.
Thank you for your suggestion anyway. Any more ideas? Mostly I am looking for potential explanations for why it would have an issue with infinite reduction with a constraint that's trivially satisfiable, and then I can try to rationalize that and see how it could apply to my case.
Juan Casanova.
________________________________
From: Haskell-Cafe
The following function I have is the one that throws the error:
resolve_to_constraints_metacnf :: SOMetaSignature -> SOMetaCNF -> Computation (Maybe SOMetaUnifSystem) resolve_to_constraints_metacnf sig cnf = result where f1 = (ADDirect <$>) :: SOMetaliteral -> SOMetaUnifLiteral; f2 = (f1 <$>) :: [SOMetaliteral] -> [SOMetaUnifLiteral]; f3 = (f2 <$>) :: [[SOMetaliteral]] -> [[SOMetaUnifLiteral]]; ucnf = f3 cnf :: [[SOMetaUnifLiteral]]; resolved = res_computeresolve SOResGreedyFactorH ucnf :: StateT uv Computation (Maybe SOMetaUnifSystem); runstated = runStateT resolved (UnifVar 0); result = fst <$> runstated
The error starts as follows:
Reduction stack overflow; size = 201 When simplifying the following type: Eq OFunction
This error is reported by: solverDepthErrorTcS :: CtLoc -> TcType -> TcM a solverDepthErrorTcS loc ty = setCtLocM loc $ do { ty <- zonkTcType ty ; env0 <- tcInitTidyEnv ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty) tidy_ty = tidyType tidy_env ty msg = vcat [ text "Reduction stack overflow; size =" <+> ppr depth , hang (text "When simplifying the following type:") 2 (ppr tidy_ty) , note ] ; failWithTcM (tidy_env, msg) } where depth = ctLocDepth loc note = vcat [ text "Use -freduction-depth=0 to disable this check" , text "(any upper bound you could choose might fail unpredictably with" , text " minor updates to GHC, so disabling the check is recommended if" , text " you're sure that type checking should terminate)" ] Have you tried "-freduction-depth=0"? Does that "terminate"? -- Viktor. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
I fixed it!
As I expected, it was a combination of two really silly, really easy to fix, errors.
1. In the line of the error, I was trying to give it a type annotation to make it easier for the type checker, but I forgot to replace the type variable "uv" with the actual type I want it to be using: "UnifVariable".
2. When I fixed this, I got the actual error that was producing this: It was not finding the instance I was expecting it to find. The reason is that I have two types "UnifSystem" and "FullUnifSystem", the latter of which is a wrapper with some extra info for the previous one. The instance is for UnifSystem, but I was feeding it FullUnifSystem to the function, so of course it was not finding the instance (and instead going into some infinite reduction trying to find an instance by replacing the variable "uv" with some magic type that didn't exist).
Change FullUnifSystem to UnifSystem (which is what I wanted since the beginning anyway) and now it works.
As a reflection, I know these are some of the dangers of using UndecidableInstances, but I found some interesting suggestions for the GHC compiler when trying to debug this, that I wish were already implemented:
https://gitlab.haskell.org/ghc/ghc/-/issues/15613
#15613: GHCi command, tracing steps of instance resolution for Constraint or expression · Issues · Glasgow Haskell Compiler / GHC · GitLabhttps://gitlab.haskell.org/ghc/ghc/-/issues/15613
Another GHCi command (#15610 (closed)), :elab <constraint> traces instance resolution for <constraint>.This is already something people do by hand (ticket:10318# ...
gitlab.haskell.org
And I found this blog post quite exactly a description of my experience with type classes:
https://mgsloan.com/posts/inspecting-haskell-instance-resolution/
[https://mgsloan.com/images/haskell-placeholder-banner.jpg]https://mgsloan.com/posts/inspecting-haskell-instance-resolution/
Inspecting Haskell Instance Resolutionhttps://mgsloan.com/posts/inspecting-haskell-instance-resolution/
An old prototype: explain-instance. I've wanted a solution to this for a long time. 5 years ago, I wrote a prototype, in the form of a Template Haskell library which takes a rather wild approach.It would be much better to implement it directly in GHC, but at the time I was much more familiar with Template Haskell, and the perverse cleverness of the approach has some appeal.
mgsloan.com
I even downloaded Michael Sloan's ExplainInstances extension to try to help me figure this out, but I couldn't get it to work due to some module version issues.
If Michael reads this, I fully support your interest in sorting out this problem. This is not the first time I lose a lot of time trying to debug silly errors like this because I need to reverse engineer what the type checker is trying to do.
Thanks to Viktor for the reply again, and to anyone who may have dedicated more than 10 seconds thinking about this.
Juan Casanova.
________________________________
From: Haskell-Cafe
The following function I have is the one that throws the error:
resolve_to_constraints_metacnf :: SOMetaSignature -> SOMetaCNF -> Computation (Maybe SOMetaUnifSystem) resolve_to_constraints_metacnf sig cnf = result where f1 = (ADDirect <$>) :: SOMetaliteral -> SOMetaUnifLiteral; f2 = (f1 <$>) :: [SOMetaliteral] -> [SOMetaUnifLiteral]; f3 = (f2 <$>) :: [[SOMetaliteral]] -> [[SOMetaUnifLiteral]]; ucnf = f3 cnf :: [[SOMetaUnifLiteral]]; resolved = res_computeresolve SOResGreedyFactorH ucnf :: StateT uv Computation (Maybe SOMetaUnifSystem); runstated = runStateT resolved (UnifVar 0); result = fst <$> runstated
The error starts as follows:
Reduction stack overflow; size = 201 When simplifying the following type: Eq OFunction
This error is reported by: solverDepthErrorTcS :: CtLoc -> TcType -> TcM a solverDepthErrorTcS loc ty = setCtLocM loc $ do { ty <- zonkTcType ty ; env0 <- tcInitTidyEnv ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty) tidy_ty = tidyType tidy_env ty msg = vcat [ text "Reduction stack overflow; size =" <+> ppr depth , hang (text "When simplifying the following type:") 2 (ppr tidy_ty) , note ] ; failWithTcM (tidy_env, msg) } where depth = ctLocDepth loc note = vcat [ text "Use -freduction-depth=0 to disable this check" , text "(any upper bound you could choose might fail unpredictably with" , text " minor updates to GHC, so disabling the check is recommended if" , text " you're sure that type checking should terminate)" ] Have you tried "-freduction-depth=0"? Does that "terminate"? -- Viktor. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
participants (2)
-
CASANOVA Juan -
Viktor Dukhovni