Janno (Jun 23 2020 at 15:06): 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.)
Janno (Jun 23 2020 at 15:06):My question is: could this be a bug?
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
Pierre-Marie Pédrot (Jun 23 2020 at 15:10):in particular, hints and primitive projections is an explosive mix
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.
Janno (Jun 23 2020 at 15:12):(I don't even know how to trigger a search for a Params instance..)
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.
Pierre-Marie Pédrot (Jun 23 2020 at 15:35):ftr I am precisely tweaking code that might be causing the issue
Pierre-Marie Pédrot (Jun 23 2020 at 15:35):but it might also be another bug...
Last updated: Apr 19 2024 at 21:01 UTC