The reason why I created this barrier between the simple cases and complicated ones is because in the simple cases it's really trivial to add a builtin, you don't need any knowledge of the elaboration machinery, how things are represented etc -- you just write the most natural thing and it works. So pretty much anyone can do it and the simple cases cover the majority of usages. But for complicated cases you really have to take some deep dives into all this stuff and so only a trained individual can handle them. Hence I think it's worth distinguishing between "this is really simple, you don't need any extra knowledge and it'll be sufficient in the majority of cases" and "here's a shitload of material to learn before you attempt to do anything of this kind".

Which still kind of bothers me... I somewhat wish we forced people to explicitly turn things into Integers. Remind me, is there an ironclad reason why we don't do this?

I get that the builtin application machinery handles this case nicely so people can't make mistakes, it just feels like it's the wrong place to put that logic...

I get that the builtin application machinery handles this case nicely so people can't make mistakes, it just feels like it's the wrong place to put that logic...

What do you think would be the right place?

I can change the existing KnownTypeIn instance for Int to give the user a TypeError specifying how exactly they're supposed to handle Int and then the user will follow the instructions and copy-paste some code within the definition of the builtin, but... why? This is more error-prone ("ok, I'm getting some weird error when I'm trying to use Int, so I'll just use fromIntegral") and quite less convenient. I don't think there's any ironclad reason why we handle Int automatically currently, but I don't see at the moment how to change that without making things substantially worse.

There's of course the problem that currently we only special-case Int while there's also Word64 and plenty of other similar types, but I'm having hopes of creating a general TypeError saying "this type is neither built-in nor one of the special types, you either want to add a new built-in type or use an existing one, for that do blah-blah-blah".

Because it's weird magic that can confuse people. I always get confused by this because I think "wait, we only have Integer in our universe, how can this work?" I wouldn't mind having to do it explicitly...

Anyway, this is off-topic, I guess.

is this elaborate/digest terminology one you use consistently in the code too?

No, I'm going to come up with some brand new docs like this one with established terminology etc and then polish existing ones, as well as file structure etc. After so many updates the builtins machinery look quite messy (the code is fine, but how it's documented and how it's aligned is not), so I'll have a separate (or a few) PR on that.

It might be worth saying what the name of that file is.

I'm intentionally avoiding such specifics. We have way too much documentation that is terribly outdated, so nowadays I'm trying to write docs that will last. I think the person adding a new built-in function is supposed to know where the default universe is anyway.

Where exactly does that error happen? When the argument is supplied to the function, or when the function is fully applied?

(I'm wondering about this for the specification, which doesn't mention this automated conversion at all because I was unaware of it or had at last failed to register it.)

When the argument is supplied to the function, or when the function is fully applied?

The former. I'll make it clear in the docs.

Changed my mind, I think this Note shouldn't dive into the specifics of how exactly things get evaluated. I'll create a separate Note.

Perhaps emphasise that this is the Haskell type of the denotation and that's where the type variables are coming from (I know the denotation's a Haskell object, but it's easy to get confused when there are two different type systems in play).

I spent several minutes trying to come up with a way to make that clarification, but it just all looks worse. So I could say "If the Haskell type of the denotation has any constrained type variables in it", but that sounds like a denotation can have a non-Haskell type, which it can't. A builtin can have a Plutus type and a Haskell type, but a denotation is always a Haskell object. Plus, it's really unambiguous here which language is meant, because Plutus Core does not have any constraints. I agree it's easy to get confused in general, but I think in this particular case things are pretty unambiguous, given that the "denotation" term is introduced have a screen above and it's explicitly stated that a denotation is a Haskell implementation.

But if you think there's a better way of formulating that part, do write it down, I'll include it in a subsequent PR, or feel free to adjust the docs yourself.

OR ELSE?

errorWithoutStackTrace, throwTo, you name it.