search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

fix #6141: don't generalize over metas constrained by instance search #7309

Open UlfNorell opened 3 weeks ago

UlfNorell commented 3 weeks ago

Fixes #6141

UlfNorell commented 3 weeks ago

Cubical fails on this type, because the level of A is not being generalised over:

++FinRid : {n : ℕ} (U : FinVec A n) (V : FinVec A 0)
         → PathP (λ i → FinVec A (+-zero n i)) (U ++Fin V) U

The culprit is the overloaded 0 (replacing it with zero makes it go through). I haven't dug into why the level of A shows up in the constraint for the literal, or why it's not resolved at the point of generalisation.