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.)
My question is: could this be a bug?
Judging from the amount of random stuff I am currently digging up from hints.ml, I am taking a bet
in particular, hints and primitive projections is an explosive mix
Should I report a bug then? I don't think I can provide an example to reproduce it.
(I don't even know how to trigger a search for a
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.
ftr I am precisely tweaking code that might be causing the issue
but it might also be another bug...
Last updated: Nov 29 2023 at 19:01 UTC