Amélia

I wrote it so I could [attach docs to TYPE and friends](https://1lab.dev/1Lab.Prim.Type.html), and the cubical primitives too. Admittedly rather niche 🙂

In light of #6049, `Agda.Primitive.Cubical` would be locked behind `--cubical-compatible`, rather than `--cubical` itself? As you mention we need stuff from that module to generate hcomp/transpIx helpers and clauses.

Part of #6049

No longer a panic as of 569375ea62, now this is the same error message issue as #6001. Should this be closed as a duplicate?

I went and changed `hcomp` to use the more precise type all throughout the cubical library in that PR there. It was mostly pretty smooth but there were some definite...

The way I'm accounting for inference is by not messing with it, at all. Inference and subtyping are indeed really hard to fit together, which is why, in a roundabout...

Re. the meta freezing aside, I tried it with an explicit `outS` and the constraint still gets postponed rather than solved, so that must be it.

I'm not sure how the situation in the `_ = s` example is any different than what you can convince Agda to do using instance search: ```agda record def (a...

To clarify, the situation in both examples is: If left completely to its own devices, Agda will make a choice, in either case: It won't insert instance arguments (so `_...

Alright, I think I understand the problems you're raising... but I don't want to just drop the feature: it's far too handy. I've been thinking about how to adapt Kovacs'...