Stream: Coq devs & plugin devs

Topic: Potential bug with Params and prim. projections?


view this post on Zulip Janno (Jun 23 2020 at 15:06):

I don't understand Params and when it's used but I've got a (closed source) development here that goes off searching for Params (@proj param) ?N and never finds anything even though there is an instance of type Params (@proj) 1. My naive understanding was that it would never search for an application, only for the head. proj is a primitive projection. I can avoid this by registering the instance it is looking for but that seems silly. The performance hit from the failed search is not enormous but it grows linearly with the number of Params instances. (Unless one can afford Hint Opaque proj : typeclass_instances which sadly breaks a lot of code in this particular code base.)

view this post on Zulip Janno (Jun 23 2020 at 15:06):

My question is: could this be a bug?

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 15:09):

Judging from the amount of random stuff I am currently digging up from hints.ml, I am taking a bet

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 15:10):

in particular, hints and primitive projections is an explosive mix

view this post on Zulip Janno (Jun 23 2020 at 15:12):

Should I report a bug then? I don't think I can provide an example to reproduce it.

view this post on Zulip Janno (Jun 23 2020 at 15:12):

(I don't even know how to trigger a search for a Params instance..)

view this post on Zulip Matthieu Sozeau (Jun 23 2020 at 15:33):

It is setoid_rewrite that triggers search for Params instances and it might well be buggy for projections. As they should have no parameters by definition, it should be an easy fix though.

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 15:35):

ftr I am precisely tweaking code that might be causing the issue

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 15:35):

but it might also be another bug...


Last updated: Oct 16 2021 at 03:02 UTC