Matrix mul must be imported publicly for Nat mul to work

Stream: mathlib4

[Yaël Dillies]

Adapting APAP to the module system, I encountered a weird issue regarding the heterogeneous multiplication of matrices:

module

import Mathlib.Data.Matrix.Mul

/--
error: Unknown constant `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid`

Note: A public declaration `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` exists but is imported privately; consider adding `public import Mathlib.Data.Matrix.Mul`.
-/
#guard_msgs in
public theorem foo (n : ℕ) : 2 * n = 2 * n := sorry

[Yaël Dillies]

This is probably a bug in the elaborator, since replacing 2 by m makes it work. I haven't yet had the time to make my minimisation mathlib-free, but hopefully it's quite minimal already.

[Jovan Gerbscheid]

I used set_option trace.Meta.synthInstance true to inspect the trace and encountered another bug: The type class pretty prints as

failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Which, when using the suggested set_option, is

[Error pretty printing expression: Unknown constant `termℕ`

    Note: A public declaration `termℕ` exists but is imported privately; consider adding `public import Mathlib.Data.Nat.Notation`.. Falling back to raw printer.]

[Eric Wieser]

@Sebastian Ullrich, perhaps this is of inteest to you, though it's not immediately clear how to minimize