Amélia

Oh, thank you @andreasabel! Somehow draft PRs slipped from my mind for a second there :sweat_smile:. Either way, I don't want to pile _too many_ changes on the PR, so...

Every CI failure seems related to GHC/Cabal: ``` : cannot satisfy -package Agda-2.6.3: Agda-2.6.3-I3IgHGye0YsBsDw89hZvr1 is unusable due to missing dependencies: STMonadTrans-0.4.6-FpHzicSrDM8D6uFU5U2hJT [too many Haskell deps to paste here] ``` not...

I still don't know what was going on with CI, but I added a single blank line to the `stack-9.2.3.yaml` (to change its hash) and it started working again.

Note that this would involve refactoring the definition of `is-lex` in `Cat.Diagrams.Limit.Finite` to use the new predicates.

The fix looks good; In the future we'd have to revisit generation of hcomp clauses into types living in `Prop` if we were to e.g. make Prop univalent. For the...

It doesn't let you prove anything new, so it's not _not_ `--safe`... but it's not entirely _safe_ since there's a lot of `__IMPOSSIBLE__` to run into? So I'd say "no"

Part of #6049, still an internal error to be fixed

@jespercockx It seems like the check for "no metavariables in rewrite rules" can be defeated by hiding the metavariable in the RHS of a function. Here's a minimal reproducer: ```agda...

Naïve solution idea (might be completely out of whack since I'm new to all this): @andreasabel can we block on any meta appearing in the type when `toLType` fails, to...

As part of checking `IApplyConfluence` for the last clause, we encounter this conversion checking problem (I've cleaned up the debug output by hand since the conversion checker doesn't use `prettyTCM`):...