Hint Rewrite Cannot Infer Parameter

Question

I'm trying to create a Hint Rewrite database for a matrix library I've written. However when I write

Hint Rewrite kron_1_r : M_db

I get the following error:

Cannot infer the implicit parameter m of kron_1_r whose type is "nat".

kron_1_r has the type forall {m n : nat} (A : Matrix m n), A ⊗ Id 1 = A, so m and n should be inferred based on the context when autorewrite is called. I'm not sure why it wants a parameter here, or how to tell it to hold off.

Answer 1

You're running into the difference between maximally inserted implicit arguments and normal implicit arguments. The difference is exactly when you use a definition without giving any arguments, the way you are in Hint Rewrite kron_1_r. One solution is of course to use @kron_1_r, which gives the identifier without any implicit arguments.

Unfortunately there's no syntax when creating a definition to give it non-maximally inserted implicit arguments; you can only use {m : nat}. Instead, you'll need to use Arguments kron_1_r [m n] _. after creating kron_1_r to change the implicit behavior of the first two arguments (as suggested by Anton Trunov above).

It's often helpful to use About, which reports the status of implicit arguments (you get these with Print as well, but you usually get too much output when you print theorems since proof terms are large).