search

brownplt / pyret-lang

The Pyret language.
Other
1.06k stars 106 forks source link

Refinement with ID declared later in letrec causes internal error #1700

Open jpolitz opened 10 months ago

jpolitz commented 10 months ago

Both of these programs (with rec or letrec) cause an internal error.

image

image

rec n :: Number%(is-zero) = 10
rec is-zero = lam(x): x == 0 end

letrec n :: Number%(is-zero) = 10,
  is-zero = lam(x): x == 0 end:
  n
end

The expected behavior is this error:

image

Probably refinements assuming the IDs are safe letrec IDs when they are not guaranteed to be.