Three Dollar Quill

I mostly thought about stuff today. Here's my current stumbling block:

I want to statically prevent failure nodes from occurring in an AST. (This may be infeasible.) Currently, my solution to this is "Don't do that :)" and I'm having trouble improving on that.

Basically, something in the current and planned implementations isn't quite right, but I'm not yet sure what.

The general idea is that failure nodes are an expected consequence of the coercion mechanism, which means that they can arise in type checking, but I'd like to guarantee that they aren't in the syntax tree or inferred type, should type checking succeed. The barrier I have to this, is how to properly represent failure nodes. If I represent them as a "feature" (which is a streamlining of the current system, which works, but has amazingly bad ergonomics), then I need some higher-kinded-types magic, or possible generic associated types magic, in order to get the type I actually want.

Before I distract myself thinking about what type magic I do have access to, let's consider how to simplify things.

The most straightforward simplification would be to simply provide an argument to coerce to tell it what to pass back. This wouldn't be too big of an ergonomics hit, and it might allow for some improvements around record types. So, let's say this is definitely on the table.

The next issue is that there's a soundness hole in the current implementation, which allows for some bad casts. Practically speaking, it would be very weird for this to actually be relevant, but it bothers me. All the same, it seems likely that the correct solution is basically to slap a note on the function saying "if you call this function outside of some very specific contexts, that's on you".

That's definitely enough thinking for now, better actually wind down.

Good night.