Why LinearMap is unable to infer implicit information?

Stream: mathlib4

[Paradoxy]

Sorry if this question is asked before, I have

variable {ι : Type*}
variable {R : Type*} [CommSemiring R]
variable {V : ι → Type*} [∀ i, AddCommMonoid (V i)] [∀ i, Module R (V i)]
 --there is actual def here
def embedV: (⨂[R] i, V i) →ₗ[R] (((i:ι) → Dual R (V i)) → R) := sorry
variable (z: ⨂[R] i, V i)
#check embedV z
/-!
function expected at
  embedV
term has type
  (⨂[?m.92599] (i : ?m.92598), ?m.92601 i) →ₗ[?m.92599] ((i : ?m.92598) → Dual ?m.92599 (?m.92601 i)) → ?m.92599Lean 4
-/

I can bypass the issue by defining

abbrev embedVEval := ⇑(embedV (R := R) (V := V))
#check embedVEval  z

But embedVEval adds unnecessary redundancy, obscuring readability and possibly the proofs.

[Etienne Marion]

Hi! can you provide a #mwe (it's a link) please? Your code does not work in the web editor (even after adding the missing imports).

[Paradoxy]

Hi @Etienne Marion , I tried the web version but it is stuck in "Waiting for Lean server to start... ". Maybe it is a global issue?

This should work:

import Mathlib.Topology.Algebra.Module.LocallyConvex
import Mathlib.LinearAlgebra.Dual.Lemmas
import Mathlib.LinearAlgebra.PiTensorProduct

open Module

open PiTensorProduct
open scoped TensorProduct

section test

variable {R : Type*} [CommRing R] [TopologicalSpace R]
variable {V : Type*} [AddCommGroup V] [Module R V]

instance instFunLike: FunLike (Dual R V) V R :=
  LinearMap.instFunLike

end test

variable {ι : Type*} [Fintype ι]
variable {R : Type*} [CommSemiring R]
variable {V : ι → Type*} [∀ i, AddCommMonoid (V i)] [∀ i, Module R (V i)]

def embedVec: (⨂[R] i, V i) →ₗ[R] (((i:ι) → Dual R (V i)) → R) := sorry

variable (z: ⨂[R] i, V i)

#check embedVec z

My file was huge, so I realized the issue actually arises from the existence of instFunLike. Not sure why.

[Etienne Marion]

It seems there was a problem in the web editor on windows machine earlier today, I don't know if it is fixed now. Anyway, I don't know what is happening here, we need someone with more knowledge. One thing I can say though is that having several instances for the same thing must never happen.

[Kenny Lau]

@Paradoxy it feels like your question might be related to a similar issue i faced here: #mathlib4 > AlgHom to RingHom coercion is bad

it's basically a bug at this stage, and the idiom (partial fix) at least for RingHom is to say RingHomClass.toRingHom instead of using an implicit coercion, as bad as this looks

for linear maps however the idiom is much more convoluted and I'm not sure if it's the best solution for linear maps.