cyclic evaluation in fixIO on launch

[abakst]

Running with --no-call-stacks appears to cause a cyclic evaluation in fixIO. For example, from the cryptol root directory:

$ cabal new-run cryptol --  --no-call-stacks tests/regression/check02.cry
Loading module Cryptol
Loading module Main
cryptol: cyclic evaluation in fixIO

Omitting --no-call-stacks drops the user into a REPL as expected.

[robdockins]

I think the fixIO call arises from this recursive monadic computation here:

cryptol/src/Cryptol/TypeCheck/Monad.hs

Line 121 in 2bdb0fa

rec ro <- return RO { iRange = inpRange info

This plays some very strange knot-tying games to lazily provide part of the computed output of the typechecking process as an input to the inference monad. This apparently makes parts of the typechecker very sensitive to strictness. 👎

Ultimately, the proximate cause is this line, which unintentionally increased the strictness demanded of a typechecked term, but only when call stacks are disabled:

cryptol/src/Cryptol/TypeCheck/Infer.hs

Line 376 in 2bdb0fa

pure $! if cs then ELocated r e' else e'

[yav]

The monadic recursion in the type checker is used to implement the dictionary passing, which is used to implement records. Basically, the issue is that we don't know how to rewrite record selections until we've solved the appropriate constraints (i.e., we've computed the dictionary). So the solution is that we rewrite with a thunk which is filled in when we solve the constraint later.

It'd be a bit tricky to get around that, I think, at least with the current IR we have, as we can't abstract over selectors... I am totally open to alternatives, or at least ideas on how make bugs like that less likely to happen, as indeed this is some pretty tricky stuff.

[robdockins]

Yeah, it's a neat solution that avoids other hacks and/or traversing the terms twice... I don't know offhand a better way to do it. Maybe we should add some big comments somewhere describing which functions need to stay lazy, though. Perhaps that would help prevent issues like this in the future?

[yav]

One idea would be to add a constructor (say Lazy Expr) to the IR and we use that whenever we want make a thunk. It would serve no purpose after type checking, so after we are done type checking we could make a pass to remove it...

The +ve is that we can be quite free about being strict (as long as we don't force the field in Lazy). The drawback is that we'd have this extra unused constructor after type-checking.