Cryptol is not lazy enough (array of tuples issue)

[TomMD]

The below code does not terminate in the REPL evaluator as of commit 4874ad0. The main pattern is xs = [(0,x) | (x,_) <- xs]. If this is my invalid expectation then feel free to close.

xs : [10]([8],[8]) 
xs = take `{10} zs where zs = [(0,0)] # [ (0, z) | (z,_) <- drop `{1} zs]

vs : [10]([8],[8])
vs = take `{10} zs where zs = [ (0, z) | (z,_) <- zs]

Observe the lack of timely termination:

version 2.3.0 (4874ad0)

Loading module Cryptol
Loading module Main
Main> xs
^C

Same with vs.

[brianhuffman]

Once we write down the intended semantics of Cryptol, it should be clear whether this would be required to terminate. (I suspect that for any reasonable semantics we might choose, it should terminate.)

[robdockins]

New evaluator (#338) fixes this issue