Interaction between opaque and instance arguments

[jespercockx]

Interaction between opaque and instance arguments

[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