Three Dollar Quill

I decided to get back into Impliciula, and that is not working out so far. I tried to work out the elaborations of various 1ML syntactic sugars, and I just got lost. So, instead of focusing on what confused me, let's take a look at the stuff that I know is wrong.

When functions take an argument of type type, the concrete type passed has to be visible to everything downstream of the call. Last I looked, this wasn't happening for my attempt at a spec. Let's imagine we're passing type bool to id. Under 1ML semantics, this results in a mapping that takes the abstract types in id's signature to bool, thereby properly specializing the function. Under the current (very rough) draft of Impliciula semantics, this... does not happen.

The focus of what needs to happen is in the possibility of a universal type in the function's signature. Even if such a universal type exists, its variables must not be visible in the output type, and therefore they must somehow be substituted in the output type. This is all straightforward in 1ML, but I'm trying to bidirectionalize, and if that's all going to work, then it looks like checking a type needs to produce a type mapping somehow. Like, type checking needs to take an additional list of types to substitute, and to give back a substitution. Or rather, this is a possibility when checking a concrete type, but not a potentially abstracted one?

Now, here's a question: should the 1ML-like level of Impliciula have two sealing-like operations, one for sealing concrete values (like the sealing in 1ML) and one for sealing abstracted values (like the various bits of built-in ascriptions in 1ML)? They only behave differently for abstracted values; would sealing the abstraction break something?

Probably, but my understanding isn't strong enough.

Anyway, I'm a little tired of thinking, so I'm going to call this here, and put in some effort on less mentally-demanding sections of my various projects. And post this early.

Good night.