@andrejbauer @MartinEscardo @jonmsterling @ltchen This is also why unification in *cubical* Agda can still be very frustrating... if matching on a truncated higher inductive type, for example, the user knows exactly what term(s) to use to handle the truncation case. They expect Agda to know too --- but there are infinitely many possible solutions, especially since the metas I'm thinking of are only constrained on one endpoint.

Example: α i0 =?= x, x : A, and Ap : is-prop A. Do you solve α := refl? Why not α := Ap x x? Heuristics for trying to get rid of these range from "surprising" to "prohibitively expensive" to "incorrect".

This is orthogonal to the problem of constraint *reporting* in Cubical Agda, which Jon mentioned above — and is going away in the upcoming release! *Most* endpoint constraints will be reported under the `Boundary`

heading in the goal display, though I wouldn't be surprised if you can get a constraint I haven't covered (even sticking to paths and HITs, even) — I'd consider those bugs in the boundary scavenging code, though.

@andrejbauer @MartinEscardo @jonmsterling @ltchen Then I say "that's why we have syntax for explicitly applying instance arguments."

The reason for avoiding this shortcut — we do this for all arguments, of course, not just instances — avoiding surprises coming from the implementation of the conversion checker. Bugs aside, Agda will never commit to a solution that has the potential to make future code *not* typecheck. The trivial class of examples is

foo _0 =?= foo 1

foo _0 =?= foo 2

Depending on what order we look at these constraints on, the other will fail — and if these arise from terms which are far away, the type error you get ("1 is not 2" or "2 is not 1", depending on the phase of the moon) would be surprising, frustrating, or both. This problem is only made worse by, e.g., postponement, pruning, eta-expansion, etc; all of which are required in practice.

By default, we chose not to surprise the user in inscrutable ways, at the cost of sometimes presenting them with easy-seeming problems (or worse, sometimes presenting them with these problems *after a long while*). More recently, we've implemented an option that allows users to be very confused very fast (--lossy-unification), if that's what they'd like

@MartinEscardo @jonmsterling @ltchen Part of the difference is from Lean using first-order unification. A conversion-checking problem of the form

Method instance_1 x y = Method ? x y

does not actually tell you anything about which instance should be selected to solve ?.

@JacquesC2 As others have noted, Presheaves exist as a place where we can talk about representability, which is a _really_ useful tool for doing internalization without tears.

When category theorists internalize, they generally define operations in the most “minimal” context possible, and then rely on precomposition to handle weakening the operations into an arbitrary context. This is pretty unnatural from the type-theoretic POV, where we prefer to define operations in an arbitrary context, and then state how substitution commutes through the operation. Categorically, this is defining a presheaf of structures, and then demanding that it be representable. See https://1lab.dev/Cat.Monoidal.Diagram.Monoid.Representable.html for a concrete example of this phenomena.

This insight is key to being able to avoid nightmarish pullbacks when trying to internalize categories, which only arise when we demand that composition be defined in the smallest context possible.

@totbwf purchasing a bag of NIST Standard Reference Lambda Abstractions

pretty sure i just managed to overthink my way into a migraine so i am going to log off and put as much space between me and light as possible

New little Agda feature I'm cooking on the side (actually a second attempt...) got done enough in a day that I feel comfortable sharing the prototype:

https://github.com/agda/agda/pull/6669

@agdakx Not a fan of *Eliminating-eliminating higher pattern-pattern matching*? 🥲

though I will say it's very unusual to break user code and go "Is my patch bad? No, it is the users who are wrong"

Normally when user code breaks with f ≠ g, and f, g are two adjacent variables in the context, it's because you messed up de Bruijn indices somewhere. Garden variety.

In this case it was the positivity checker just casually deciding to break transitivity of conversion by not using the polarity associated with the data type name, but with some secret info from god-knows-where. Lovecraftian

Pretty often I'll investigate a garden-variety Agda issue and end up revealing a lovecraftian Agda issue lurking right beneath

Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).

I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️

Joined Jan 2022