Would at least need syntax like `case x of (PSyn 42 |) -> ...`, where `|` delimits the "parameters" (visible version of "required constraints") from the "match variables" (visible versions of "provided constraints")

At least in Haskell, there's a semantic difference, though. You can't "parameterize" a pattern synonym. So `case x of ((==) 42 -> True) -> ...` where 42 is supposed to be a parameter of the pattern synonym is not really expressible in Haskell.

How about pair syntax? Or a more general record destructing syntax (that's how it works in Lean)

I would make that depends on whether macro expansion (_) happens before ANFisation in your language. Is there some precedent? It would be important to decide coherently.

In Lean, it would be A), I think.

As to <<loop>>: this is just the runtime detecting that a thunk that is already under evaluation is evaluated again. The first eval overwrites the thunk tag with a special tag for a "black hole". Evaluating a black hole crashes with the panic.

A classic... I keep losing hours to this as well. Solution is to implement a linter as described here: github.com/ghc-proposal...

Apparently they do support first class functions since 2022: effekt-lang.org/evolution

You might enjoy effekt-lang.org#intro-polymo.... I think their notion of implicit effect polymorphism is pretty usable

Have you tried Lean's InfoView? :)

(Even after stack alloc it will be far slower to call an unknown function in tailRec than to jump to it's address directly, so I'm not sure whether this idea is practical)

If it really is primitive (so can't inline it), then the compiler needs special support for the closure passed to tailRec. It will never escape and hence its fvs can be allocated on the stack.

But how do you mutually recursive tail calls with tailRec?

I had assumed that the goal here is to implement tail call opt for this one special case. If you inline it, how can you still detect the special case? Or do you mean that your compiler can still spot tail recursion after inlining tailRec? In that case, what is so primitive about tailRec?

But it's not really efficient unless the compiler inlines it for you

Your contributions to the community are amazing. Badly socialized people will always be assholes 🤷🏻 Though I suspect your point is rather that we should call out this behaviour for the health of our community. Fair point...

I would very much like to be liked or loathed like this