Zulip Chat Archive

Stream: general

Topic: instance obfuscation


view this post on Zulip Simon Hudon (Jan 30 2019 at 17:17):

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?

view this post on Zulip Chris Hughes (Jan 30 2019 at 17:28):

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

view this post on Zulip Gabriel Ebner (Jan 30 2019 at 17:43):

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

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

view this post on Zulip Simon Hudon (Jan 30 2019 at 18:53):

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

view this post on Zulip Simon Hudon (Jan 30 2019 at 18:53):

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


Last updated: May 10 2021 at 17:39 UTC