Re: [Haskell-cafe] Puzzling "Reduction stack overflow" error message

24 Jan 2021

      "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  on behalf of Viktor Dukhovni 
Sent: 24 January 2021 05:06
To: haskell-cafe@haskell.org 
Subject: Re: [Haskell-cafe] Puzzling "Reduction stack overflow" error message

This email was sent to you by someone outside the University.
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.

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.
_______________________________________________
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.