Use no-return in cptypes

[gus-massa]

There are a few things that I don't understand, so this is more a long question with a proof of concept than a finished PR.

---

When cptypes detects an error that is not obvious, use $app/no-return so the other passes can notice it. But cp0 transform $app/no-return to special flags in preinfo, so let's add the flags directly instead.

After this change, in the second leap cp0 can notice that cptypes detected an error and apply more reductions. See the example at the bottom of cptypes.ms Also, there is an old example in cp0.ms that has type problems on purpose, and is broken with an explicit use of $app/no-return.

I'm worry that this is wrong for some primitives that write/read the continuation attachment. Is there an obvious example? Is there a not obvious example?

Is it wrong with lambdas instead of primitives? I'm almost sure it is, but I'd like to see an example to be sure what to care about . (Anyway, probably lambdas will be left for a PR in the future.)

---

If this make sense and is (almost) correct, I'd like to take a look if the same change can be applied in more parts of cptypes, and do some refactor and cleanup.

[mflatt]

This looks like the right idea to me.

I can't think of a reason that it would go wrong with continuation attachments. If it can, it seems like it would be a general cp0 issue with the no-return flag that we'd need to fix there.

The flag is not intended to be constrained to primitives, so it should be fine if the target of the call is created with lambda. As an example, the Racket implementation uses $app/no-return to call non-primitive procedures that format and throw exceptions.

[gus-massa]

I was worried about

ChezScheme/s/prims.ss

Lines 540 to 544 in 73803e1

	;; Implies no-inline, and in unsafe mode, asserts that the
	;; application will not return and that it does not inspect/change
	;; the immediate continuation attachment (so it can be moved to a
	;; more-tail position)
	(define $app/no-return

[mflatt]

I see. There are no uses of continuation marks/attachments in any primitives, so I think this is ok for primitives.

It complicates adding the no-return flag to calls of non-primitives, since the optimizer would need to prove the extra constraint on the called function — a little more work, but probably straightforward in many cases.

[gus-massa]

I'll take a look and post a not-draft version is a few days.

---

About lambdas, do you have an example? My idea is to ignore them for now and `add them much later (2027?), perhaps with code to handle this-lambda-will-never-raise an-error too. Do you have an example that may be problematic?

[gus-massa]

Updated.

I still don't like err/obvious for errors caused by arity or in expressions already marked with no-return. Do you have a better idea?

I didn't update the release notes. This seams to be too internal. But if you prefer, I can add something like

The type recovery pass now marks primitive calls with type error with the no-return flag, so other passes of the compiler can notice that they will raise an error.

[mflatt]

You're looking for an alternate name of the variable err/obvious? Maybe something like err/immed to mean that the error is immediately apparent from the call form already? I'm not sure that's what you're looking for, though.

I can appreciate the feeling that the change is too small to mention, but given the current conventions, I would be inclined add a little more to the current "Type recovery improvements" first sentence — maybe something like , and it records must-error information that is inferred by type recovery so that it can be used by other optimization passes.

[mflatt]

For no-return lambda, I'm not sure whether this is what you're looking for, but it's an example where $app/no-return allows cptypes to convert + to fl+. In principle, the $app/no-return itself could be inferred because fail always calls errorf.

(expand/optimize
 '(lambda (x)
    (let ([fail (lambda ()
                  (errorf "argument is no good ~s"
                          ;; something large enough to prevent inlining:
                          (let loop ([x x])
                            (cond
                              [(something1? x)
                               (loop (revise1 x))]
                              [(something2? x)
                               (loop (revise2 x))]
                              [(something3? x)
                               (loop (revise3 x))]
                              [else
                               x]))))])
      (unless (flonum? x)
        (#%$app/no-return fail))
      (when (zero? x)
        ;; call second time to prevent inlining of single call
        (#%$app/no-return fail))
      (+ 3.0 x))))

[gus-massa]

Fixed, renaming to err/immed and release notes.