instance obfuscation

Stream: general

[Simon Hudon]

Every now and then, I use rw and I get a type class resolution problem as a side condition. If I work with traversable, I get traversable (λ x, t x) as a side condition while traversable t is in my context. Is there a way to avoid that? Also, is there a reason why type class resolution does not perform eta reduction first?

[Chris Hughes]

Usually giving the rw enough information to work out the type is good enough. So do rw @lemma α for example.

[Gabriel Ebner]

Is this a problem? Instance search should transparently apply η:

example {t} [traversable t] : traversable (λ x, t x) :=
infer_instance

[Simon Hudon]

Oh, that's curious. Maybe η is not the problem then.

[Simon Hudon]

@Chris Hughes Thanks, I will do that. I was hoping it wouldn't come done to it though