If you mark a record field as instance, it gets added to the instance table with a visible function type, and instance search will happily use the projection function to solve an instance headed by its codomain:
module Test111 where postulate P : Set record Q : Set where field instance p : P postulate q : Q get-p : ⦃ x : P ⦄ → P get-p ⦃ x ⦄ = x it : P it = get-p
This fails with unsolved constraint
Failed to solve the following constraints:
Q → P =< P (stuck)
because instance search solved x := λ r → Q.p r; though since the type is wrong, you can't get Agda to admit that it's done this without using underhanded methods (interactive normalisation, reflection, checking the debug buffer, etc.) If you normalise it, you get λ r → Q.p r.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4