Interaction between opaque and instance arguments

[jespercockx]

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 = it

works 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?

[plt-amy]

I think I ran into this same on Sunday, but I wrote it off since I was trying to do something stupid anyway.

The immediate solution that pops into my head is to fix up the instance canditates according to the following rule: if we have i : {∆} → f xs and f is an opaque symbol that's unfolded in the current block, then it's replaced with i : {∆} → reduce (f xs). But it's possible that this might reduce the instance head too far, and so it would be necessary to consider an exponential number of i' : {∆} → reduce (f xs) in which different subsets of the unfolding set are allowed to reduce, which wouldn't be viable.

[nad]

Could one instead change instance search so that it never succeeds for opaque symbols?

[jespercockx]

Well one could but that solves the problem by denying it exists. A better way might be to ignore all opaque flags in the construction of the instance table, and then filter our the instances that are not legal because of opaque statements as part of the regular instance filtering.

[jespercockx]

The same bug also happens for abstract:

it : {X : Set} → {{X}} → X
it {{x}} = x

postulate
  A : Set
  a : A

abstract
  B : Set
  B = A

  instance
    b : B
    b = a

works : B
works = it

abstract
  fails : B
  fails = it