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


And I found this blog post quite exactly a description of my experience with type classes:

https://mgsloan.com/posts/inspecting-haskell-instance-resolution/

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 <haskell-cafe-bounces@haskell.org> on behalf of CASANOVA Juan <Juan.Casanova@ed.ac.uk>
Sent: 24 January 2021 17:56
To: haskell-cafe@haskell.org <haskell-cafe@haskell.org>
Subject: Re: [Haskell-cafe] Puzzling "Reduction stack overflow" error message
 
"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 <haskell-cafe-bounces@haskell.org> on behalf of Viktor Dukhovni <ietf-dane@dukhovni.org>
Sent: 24 January 2021 05:06
To: haskell-cafe@haskell.org <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.