Implicit function cleanups

[brendanzab]

Some cleanups to the implementation of implicit functions that were added in #439. I’ve broken the dependency on core::Plicity in the surface syntax, adjusted some names, and cleaned up the insertion of implicit arguments somewhat (inspired by elaboration-zoo’s implementation).

[Kmeakin]

Why replace turn surface::Param into an enum? What if we want to add other annotations to parameters, such as erasure?

[Kmeakin]

Why Vec::from_iter over the more familiar .collect()?

[brendanzab]

It formats nicer hah.

[Kmeakin]

🤷 personal preference. I don't mind either way

[Kmeakin]

Why remove implicit arrow types?

[brendanzab]

Eventually I was hoping that we could make implicit arguments named. I’m also not sure how useful implicit arrows are? Seeing as you can’t infer them based on other arguments or the return type?

[Kmeakin]

Hmm, true. Since the most common use case for implicit parameters are type parameters, unnamed type parameters wouldn't be very useful.

[brendanzab]

Why replace turn surface::Param into an enum? What if we want to add other annotations to parameters, such as erasure?

I guess I still had in my head the {A : Type} -> B syntax, where the “implicitness” is part of the parameter syntax – but as we have said before - this is ambiguous with our record syntax. We could make the erasure annotations fields on the variants… but I do see how it would be a similar problem to implicitness – where we might want to use one of those variants in the surface module? I can re-think that commit if it’s easier.