panic with message "Unexpected value in tuple selection"

[nano-o]

Main> let (x,y)=(0,x+1)
[warning] at :1:5--1:18:
Defaulting the type of '::y' to [1]
Main> x
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
Revision: UNKNOWN
Branch: UNKNOWN
Location: [Eval] Cryptol.Eval.evalSel
Message: Unexpected value in tuple selection

CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.Utils.Panic
panic, called at src/Cryptol/Eval/Monad.hs:186:17 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.Eval.Monad
evalPanic, called at src/Cryptol/Eval.hs:431:29 in cryptol-2.7.0-B2fyIqbCot160gS325LyBV:Cryptol.Eval
%< ---------------------------------------------------

[brianhuffman]

This reminds me very much of #534. @yav, what do you think?

[yav]

Well, that one is already fixed, so it can't be that :-)

More seriously, when I run it there is an extra line in the panic that's not visible above:

Message:   Unexpected value in tuple selection
             <polymorphic value>

It would appear that we are trying to project from a polymorphic value, which should never happen, hence the panic. Btw, it also happens if you make the definition at the top level of a module, so there's a bug in the handling of recursive pattern bindings, not just the command line.

The equation above is translated to something like:

p = (0,x+1)
x = p.0
y = p.1

So likely what happened is that p became polymorphic (correct), but we didn't instantiate it at the use sites (incorrect).

Here is the actual output of the translation:

Main::x : [1]
Main::x = Main::__p0 .0 /* of 2 */
Main::__p0 : {a} (Literal 0 a) => (a, [1])
Main::__p0 = \{a} (Literal 0 a) ->
             Main::$mono
             where
               /* Recursive */
               Main::$mono : (a, [1])
               Main::$mono = (Cryptol::number 0 a <>,
                              (Cryptol::+) [1] <> Main::x (Cryptol::number 1 [1] <>))
               
             

/* Not recursive */
Main::y : [1]
Main::y = (Main::__p0 [0] <>) .1 /* of 2 */

The bug is that in the definition of x, __p0 is not applied to a type argument.

[brianhuffman]

I tried a slightly simplified example let (x, y) = (y, 0) with a version of Cryptol modified to show debugging output of the result of the NoPat pass:

Cryptol> let (x, y) = (y, 0)
--------------------
after nopat:
  * __p0 = (y, 0) : (_, _)
  * x := __p0.0 /* of 2 */
  * y := __p0.1 /* of 2 */
--------------------
/* Recursive */
<interactive>::y : Bit
<interactive>::y = <interactive>::__p0 .1 /* of 2 */
<interactive>::__p0 : {a} (Literal 0 a) => (Bit, a)
<interactive>::__p0 = \{a} (Literal 0 a) ->
                      (<interactive>::y, Cryptol::number 0 a <>)

/* Not recursive */
<interactive>::x : Bit
<interactive>::x = (<interactive>::__p0 [0] <>) .0 /* of 2 */

So the NoPat pass expands the original declaration into three new ones, and the := in the second and third indicates that these are "mono" declarations. The NoPat pass seems to be doing the right thing, but somewhere during type checking something gets defaulted to type Bit, which is totally wrong.

[brianhuffman]

My latest idea is that the type checker goes wrong when it is given a recursive set of bindings where some are mono and others are not. For example, with let (x, y) = (y, 0), NoPat produces three bindings:

  * __p0 = (y, 0) : (_, _)
  * x := __p0.0 /* of 2 */
  * y := __p0.1 /* of 2 */

Here, __p0 and y are mutually recursive, and y is mono but __p0 is not.