search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

Relations in proofs in `Data.Product.Relation.Binary.Pointwise.NonDependent` don't appear to be inferable #2174

Open MatthewDaggitt opened 1 year ago

MatthewDaggitt commented 1 year ago

When using at least ×-refl, ×-symmetric and ×-transitive, the relations R and S do not appear to be inferable. Should be made explicit?

gallais commented 1 year ago

Or we could make Pointwise a record wrapper to help inference.

JacquesCarette commented 1 year ago

It's annoying to have to 'help' the inferencer so much, but it has the huge advantage of being coherent with other Pointwise, so I'm in favour of that.

jamesmckinna commented 1 year ago

I'm always surprised when I have to help the inferencer with otherwise seemingly-constant arguments to higher-order operations (eg L84 of my recent af83f0ae1ebc75879d42957b70f2693022f36345), but that just goes to show how much I stay in 'user space' as regards Agda-as-a-tool, rather than 'kernel space' as a type-theorist/system developer. Even after one in-person AIM, I still don't feel quite ready to go 'under the hood'. One day, perhaps. Eg my naive thought is that $\beta_0$ unification ought to be able to figure some of these arguments out, and I've always supposed that it is implemented in the inferencer (or else an appropriate fast-fail heuristic for full higher-order unification... but that may be magical thinking?), but what do I know? etc.