<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<font size="2"><span style="font-size:11pt">"Have you tried "-freduction-depth=0"? Does that "terminate"?"<br>
<br>
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.<br>
<br>
But I have now, since when you said it I realized it was definitely something to try.<br>
<br>
I have tried with -freduction-depth=20000, and it still fails (with the same Eq OFunction constraint).<br>
With -freduction-depth=1000000 or -freduction-depth=0, it does not terminate within a minute or two.<br>
<br>
So it does look like there is some infinite depth going on.<br>
<br>
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.<br>
</span></font></div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<font size="2"><span style="font-size:11pt"><br>
</span></font></div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<font size="2"><span style="font-size:11pt">Juan Casanova.</span></font><br>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Haskell-Cafe <haskell-cafe-bounces@haskell.org> on behalf of Viktor Dukhovni <ietf-dane@dukhovni.org><br>
<b>Sent:</b> 24 January 2021 05:06<br>
<b>To:</b> haskell-cafe@haskell.org <haskell-cafe@haskell.org><br>
<b>Subject:</b> Re: [Haskell-cafe] Puzzling "Reduction stack overflow" error message</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">This email was sent to you by someone outside the University.<br>
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.<br>
<br>
On Sun, Jan 24, 2021 at 03:15:24AM +0000, CASANOVA Juan wrote:<br>
<br>
> The following function I have is the one that throws the error:<br>
><br>
> resolve_to_constraints_metacnf :: SOMetaSignature -> SOMetaCNF -> Computation (Maybe SOMetaUnifSystem)<br>
> resolve_to_constraints_metacnf sig cnf = result<br>
> where<br>
> f1 = (ADDirect <$>) :: SOMetaliteral -> SOMetaUnifLiteral;<br>
> f2 = (f1 <$>) :: [SOMetaliteral] -> [SOMetaUnifLiteral];<br>
> f3 = (f2 <$>) :: [[SOMetaliteral]] -> [[SOMetaUnifLiteral]];<br>
> ucnf = f3 cnf :: [[SOMetaUnifLiteral]];<br>
> resolved = res_computeresolve SOResGreedyFactorH ucnf :: StateT uv Computation (Maybe SOMetaUnifSystem);<br>
> runstated = runStateT resolved (UnifVar 0);<br>
> result = fst <$> runstated<br>
><br>
> The error starts as follows:<br>
><br>
> Reduction stack overflow; size = 201<br>
> When simplifying the following type: Eq OFunction<br>
<br>
This error is reported by:<br>
<br>
solverDepthErrorTcS :: CtLoc -> TcType -> TcM a<br>
solverDepthErrorTcS loc ty<br>
= setCtLocM loc $<br>
do { ty <- zonkTcType ty<br>
; env0 <- tcInitTidyEnv<br>
; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)<br>
tidy_ty = tidyType tidy_env ty<br>
msg<br>
= vcat [ text "Reduction stack overflow; size =" <+> ppr depth<br>
, hang (text "When simplifying the following type:")<br>
2 (ppr tidy_ty)<br>
, note ]<br>
; failWithTcM (tidy_env, msg) }<br>
where<br>
depth = ctLocDepth loc<br>
note = vcat<br>
[ text "Use -freduction-depth=0 to disable this check"<br>
, text "(any upper bound you could choose might fail unpredictably with"<br>
, text " minor updates to GHC, so disabling the check is recommended if"<br>
, text " you're sure that type checking should terminate)" ]<br>
<br>
Have you tried "-freduction-depth=0"? Does that "terminate"?<br>
<br>
--<br>
Viktor.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br>
</div>
</span></font></div>
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
</body>
</html>