>  Idris 2 implements dynamic pattern unification. In Idris 1, metavariables (that is, the implicits that need to be solved) are stored locally to a term, so solving them requires searching through the term and substituting the definition, which can be expensive. Idris 2, on the other hand, stores metavariables globally, in the mutable global context, following roughly the scheme described in Ulf Norell's thesis.

йей. Правда какие-то mixed signals: "dynamic pattern unification" — это ссылка, которая ведет на "A tutorial implementation of dynamic pattern unification", а в диссере Ульфа делается по-другому (twin contexts vs guarded constants)

хм, а эти guarded constants случайно не темпоральной логикой навеяны?

вроде нет, но интересно будет ли профит если завернуть это всё в темпоральную металогику