Polymorphic builtin types are generally quite limited: don't use them unless you have to.

If you're interested, you can read https://github.com/input-output-hk/plutus/blob/master/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs#L317

Wouldn't

nil :: forall. BuiltinProxy a -> BuiltinList a
nil _ = BuiltinList []
{-# NOINLINE nil #-}

newtype BuiltinProxy a = BuiltinProxy BuiltinUnit

work?

EDIT: looks like that's what proposed at the end of that comment. I think you should investigate that.

EDIT2: The builtin type is obscure. Does it means types in DefaultUni, i.e. unit, bool, bytestring, text, list of these, pairs of these and data, but not functions? i.e. something keen to primitive types in Java (but Java arrays are somewhat special...)

otoh, I think nil doesn't need to be BuiltinFun at all. error isn't.

Is there nil :: BuiltinList a value?

No.

EDIT: looks like that's what proposed at the end of that comment. I think you should investigate that.

Lots of other higher-priority tasks. It does sound like it would be nice to add Proxy to the set of built-in types, but for nil :: BuiltinList a to work a also needs to be constrained to be a built-in type and it would be great to really make it a constraint rather than an explicit BuiltinProxy, so this just requires time to be investigated.

EDIT2: The builtin type is obscure. Does it means types in DefaultUni, i.e. unit, bool, bytestring, text, list of these, pairs of these and data, but not functions? i.e. something keen to primitive types in Java (but Java arrays are somewhat special...)

Yes.

otoh, I think nil doesn't need to be BuiltinFun at all. error isn't.

It's an oversight that error isn't a builtin.

otoh, I think nil doesn't need to be BuiltinFun at all. error isn't.

It's an oversight that error isn't a builtin.

I meant there doesn't seem to be a problem to make a binding for polymorphic error, even it's not a BuiltinFun.

(IMO making error a BuiltinFun would be a mistake, given how special it is. EDIT: e.g. Error should always exist, even if there aren't any other builtin functions or types).

I meant there doesn't seem to be a problem to make a binding for polymorphic error, even it's not a BuiltinFun.

Ah, yeah, that wouldn't be a problem. But then we'd have some builtins in the universe and some as constructors and that is silly. Why have the whole extensible built-in functions machinery, if we're going to hardcode particular builtins anyway.

e.g. Error should always exist, even if there aren't any other builtin functions or types

Why not? Maybe some hypothetical blockchain doesn't want the implicit error effect and instead they require the validator to return a Bool (there's a huge difference between a malformed program that tries to, say, apply a non-function and a program deliberately returning an error). Plutus Core is a compilation target of Plutus Tx, but there can be other languages targeting Plutus Core and their creators may certainly not like error-as-an-implicit-effect.

Can builtin functions be partial at the moment?

Can builtin functions be partial at the moment?

Yes, we have lots of those: HeadList, DivideInteger (fails if the second argument is zero), IndexByteString etc.

An update: at some point we've realized that this point from the original message:

PlutusTx.Builtins.Internal has specialized variants, and these don't seem right. (Why use BuiltinFun when Constant would be enough?)

should've crossed our minds when we added the monomorphic mkNil* builtins. Those builtins seem to be used for "consistency" currently, although I don't really know what that means.

However while it may seem like a good idea to try use Constant instead of DefaultFun and then get the polymorphic version of mkNil via a type class in Plutus Tx or something, it would actually be worse than adding Proxy to the universe, because Proxy also allows us to also give a sensible Plutus type to the mkPair constructor-turned-builtin, which isn't something we'd be able to do without additional support on the Plutus side. We'd still need a type class (for constructing Proxy Constants), but we'd be able to use those for both lists and pairs (and other built-in types should we add any).

Relevant docs are here (same link as above, except not broken).

Low priority, but something that is worth looking into at some point.

We've added a somewhat general mkNil in #6347. It's pretty ugly and we still have to enumerate all supported types explicitly, but that'll do for now. Adding Proxy is definitely not going to happen any time soon and there's a subtask for that in #4306. Hence I'm gonna close this issue as "kinda done".