TC stuck on metavariable

Stream: lean4

[Tomas Skrivan]

I'm again fighting with TC and unfortunately I do not have mwe yet.

tl;dr - the question: How do I set up and example that tests definatorial equality? for example Module ℝ Y =?= Module ℝ ?m.7927 is doing something weird inside of TC, how do I compartmentalize it and test it directly?

---

The problem is rather odd, this example fails:

example : ∀ (i : X), IsSmooth λ (x : T) => ∥x[i]∥² := by infer_instance -- fails

(A bit of context, T implements GetElem T X Y (fun _ _ => True) and Y is vector space with a norm. )

The odd thing is that when you move the argument (i : X) before the the colon it suddenly works:

example  (i : X) :  IsSmooth λ (x : T) => ∥x[i]∥² := by infer_instance -- works

---

The TC error is:

error: typeclass instance problem is stuck, it is often due to metavariables
  ∀ (i : X), IsSmooth fun x => ∥x[i]∥²

TC tracing abruptly ends with message

[Meta.synthInstance.tryResolve] Module ℝ Y =?= Module ℝ ?m.7927

by inspecting the code, this should be always followed by one of these:

[Meta.synthInstance.tryResolve] "success"
[Meta.synthInstance.tryResolve] "failure assigning"
[Meta.synthInstance.tryResolve] "failure"

Unless, there is there is an exception thrown in (← isDefEq mvarTypeBody instTypeBody) or (← isDefEq mvar instVal). This is happening inside of tryResolveCore.

So there must be a problem with checking the definatorialy equality. Hence the question at the top. How do I set up a test for Module ℝ Y =?= Module ℝ ?m.7927?

[Tomas Skrivan]

After some investigation, the call (← isDefEq mvarTypeBody instTypeBody) throws an exception. The message data of the exception is "internal exception #0", what does that mean?

[Tomas Skrivan]

And for the caught exception e the e.getRef is <missing> and e.hasSyntheticSorry is false.

[Tomas Skrivan]

Interestingly enough, switching to isDefEqGuarded solves the TC problem but causes bunch of other problems. For example #check 1 errors with OfNat ?m.8278 1. In general, type deduction seems a bit broken after it.

[Tomas Skrivan]

I have found the problematic instance:

instance (T X Y : Type) [FunType T X Y] [AddCommMonoid Y] [DistribMulAction ℝ Y] : Module ℝ T := Module.mk sorry sorry

It should be more or less direct copy from mathlib as mathlib4 does not have modules yet.

The class FunType T X Y is saying that T behaves like X -> Y. This class extends GetElem T X Y (fun _ _ => True).

This instance was giving me troubles in the past but priority tweak fixed it. This time I have to mark it as local to resolve the problem, but that is not an ideal solution. Hopefully I should be able to produce mwe now.

---

Anyone is working with modules in Lean 4? What is your definition? How do you define scalar multiplication? My MulAction extends HMul:

class MulAction (α : Type u) (β : Type v) [Monoid α] extends HMul α β β :=
(one_smul : ∀ b : β, (1 : α) * b = b)
(mul_smul : ∀ (x y : α) (b : β), (x * y) * b = x * y * b)