Geb error with higher-order functions

[anoma]

Geb error with higher-order functions

[rokopt]

For reference, here is the term in current syntax:

TRANS> (well-defp (list (coprod so1 so1) (fun-type (fun-type (coprod so1 so1) (coprod so1 so1)) (coprod so1 so1))) (app (lamb
      (fun-type
       (fun-type
        (coprod so1 so1)
        (coprod so1 so1))
       (coprod so1 so1))
      (app
       (index 0)
       (lamb (coprod so1 so1)
             (index 1))))
      (lamb
       (fun-type (coprod so1 so1)
                 (coprod so1 so1))
       (left so1 (unit)))))
T

[agureev]

This compiles with the new #97

[rokopt]

Can this be closed as fixed by #97 ?

[rokopt]

Can this be closed as fixed by #97 ?

It can't have been by #97 -- that only would have fixed heap exhaustions; this was a typecheck error -- but it might have been fixed by the STLC indexing changes. We'll retry this with the latest code to confirm.

[agureev]

This is fixed by #127