revisit cast errors
Closed this issue · 3 comments
ivoysey commented
I closed #14 because the last theorem was false -- some errors do step. For example if d1 steps but d2 is a cast error, d1 (d2) is both an error and steps.
This goes against my (the) intuition that the branches of progress ought to be disjoint as a principle. We should either change casts so that they accumulate through evaluation but stepping happens beyond them or figure out a good reason why it's ok that the branches aren't disjoint.
cyrus- commented
the 2/6 version of the notes posted on slack have an initial design for this idea. the new forms/rules/clauses are starred in red for easy diffing. let me know what you think.
cyrus- commented
"this idea" being "treat failed casts as indeterminate forms"