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

[Viktor Dukhovni]

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.