Closed
Description
I noticed a rather unfortunate interaction between opaque declarations and instance arguments. Consider the following example:
it : {X : Set} → {{X}} → X
it {{x}} = x
postulate
A : Set
a : A
opaque
B : Set
B = A
instance
b : B
b = a
works : B
works = it
opaque
unfolding B
fails : B
fails = itworks works, but fails fails:
No instance of type B was found in scope.
when checking that the expression it has type B
This is not really surprising given the current implementation of instance search: in this case the instance is attached to the opaque type B, but inside the body of fails the type reduces to A and there are no instances for type A in the instance table.
I'm not sure what's the best way to solve it, but it feels like we need some kind of unfolding-aware instance table. @plt-amy do you have an idea?