[Agda] Instance resolution question

[Apostolis Xekoukoulotakis]

```
module Test2 where


data A : Set where


CPF : Set
CPF = {{a : A}} → A

postulate
  fun : CPF → CPF
  e : CPF


bob : CPF
bob {{ctx}} = fun (e {{ctx}})


rob : CPF
rob = fun e

```

I wonder if there is a way to write "rob" instead of "bob".

Keep in mind that the candidates are definitionally equal. (it seems)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180328/f95a0ee9/attachment.html>