Module.Dual and linear maps

Stream: mathlib4

[Ruben Van de Velde]

A fun issue for y'all: a linear map over a semiring can't be coerced to a function if Mathlib.LinearAlgebra.Dual is imported; upgrading R to a ring does work

import Mathlib.LinearAlgebra.Dual
import Mathlib.Algebra.Module.LinearMap

variable {R : Type*} [Ring R]

def foo {R : Type*} [Semiring R] : R →ₗ[R] R where
  toFun := id
  map_add' := sorry
  map_smul' := sorry

def bar {R : Type*} [Ring R] : R →ₗ[R] R where
  toFun := id
  map_add' := sorry
  map_smul' := sorry

example {R : Type*} [Semiring R] (p : R) : foo p = p := sorry -- fails
example {R : Type*} [Ring R] (p : R) : foo p = p := sorry -- fails
example {R : Type*} [Ring R] (p : R) : bar p = p := sorry -- works

function expected at
  foo
term has type
  ?m.2379 →ₗ[?m.2379] ?m.2379

Removing the Mathlib.LinearAlgebra.Dual import makes everything work, maybe because Module.Dual := M →ₗ[R] R is reducible?

[Eric Wieser]

Making Module.Dual not reducible had even more trouble

[Ruben Van de Velde]

Yeah, that didn't look like fun

[Eric Wieser]

This fixes it:

instance LinearMap.instCoeFun
  {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃]
  [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
CoeFun (M →ₛₗ[σ] M₃) fun x => M → M₃ := inferInstance -- or `⟨FunLike.coe⟩`

[Eric Wieser]

We had these shortcut instances in Lean 3, but they had the wrong implementation so we removed them

[Eric Wieser]

I guess the docs#LinearMap.instFunLike shortcut (that we replaced it with during porting) isn't enough

[Matthew Ballard]

How about

example {R : Type*} [Semiring R] (p : R) : foo (R := R) p = p := sorry

?

[Ruben Van de Velde]

That seems to work as well, though not so much fun in practice :)

[Matthew Ballard]

The trace is odd here

[Meta.synthInstance] [0.000107s] 💥 Semiring ?m.2810 ▼
  [] [0.000051s] new goal Semiring ?m.2810 ▶
  [] [0.000033s] 💥 apply inst✝ to Semiring ?m.2810 ▼
    [tryResolve] [0.000023s] 💥 Semiring ?m.2810 ≟ Semiring R ▼
      [isDefEq] [0.000020s] 💥 Semiring ?m.2810 =?= Semiring R ▼
        [] [0.000003s] 💥 ?m.2810 =?= R ▼
          [] ?m.2810 [nonassignable] =?= R [nonassignable]

[Matthew Ballard]

Where ?m.2810 : Type ?u.2808

[Matthew Ballard]

Universe issues?

[Matthew Ballard]

I also don't know what nonassignable means...

[Matthew Ballard]

But it seems reasonable to expect success here right?

[Matthew Ballard]

For reference this still doesn't work after removing LinearAlgebra.Dual from the imports. It just finds a CoeFun where it couldn't before.

And that is because with LinearAlgebra.Dual it ends up back at Semiring ?_ which it cannot solve

[Jireh Loreaux]

Kevin and I both witnessed this before. @Kevin Buzzard can you find the threads? I'm on mobile currently

[Matthew Ballard]

The message looks like it originates from Lean.Meta.isDefEqQuickOther (private so no docs links but here is the link to the line)

[Jireh Loreaux]

Here is the thread (which itself links to the other one that has a lot of noise): https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/instance.20breaking.20FunLike

[Jireh Loreaux]

I think the problem is docs#Module.Dual.instFunLikeDual, but we haven't determined why.

[Matthew Ballard]

I am confused as to why R is getting this nonassignable tag. From reading the code, it seems like it should be a metavariable at that point in the logic

[Matthew Ballard]

Jireh Loreaux said:

I think the problem is docs#Module.Dual.instFunLikeDual, but we haven't determined why.

Someone should check me on this but it looks like trying that instance throws off side goals one of which is Semiring ?_ which fail regardless of importing LinearAlgebra.Dual

[Matthew Ballard]

Explicitly giving R with (R := R) makes things work in all cases.

[Jireh Loreaux]

Sorry, explicitly trying which instance? The one Eric suggested?

[Kevin Buzzard]

Sorry Jireh/Matt -- I'm in a field all week

[Matthew Ballard]

$\mathbb {C}$?

[Jireh Loreaux]

Nevermind Kevin, I found it, thanks!

[Matthew Ballard]

Import LinearAlgebra.Dual and unification passes through Module.Dual.instFunLikeDual and asks for which semiring we are using. It creates Semiring ?_ as a goal which it cannot solve

[Matthew Ballard]

Don't import it and it still tries to figure out Semiring ?_ but doesn't need it to find the coercion

[Matthew Ballard]

It gets to ?_ =?= R and it fails...

[Matthew Ballard]

I think because both sides are marked nonassignable

[Jireh Loreaux]

Hmmm, is that because it's an outParam? I don't know what nonassignable is.

[Matthew Ballard]

From (rip)grepping, there is only one place where ?m.2810 [nonassignable] =?= R [nonassignable]can be thrown

[Matthew Ballard]

Here

[Matthew Ballard]

I don't know precisely what it is either but it seems like you want to assign ?_ := R

[Sebastian Ullrich]

Does it later repeat the TC synth with the metavariable instantiated?

[Matthew Ballard]

Not that I saw no

[Matthew Ballard]

Let me dump the full trace...

[Sebastian Ullrich]

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Instance.20search.20without.20type/near/361934735

[Jireh Loreaux]

Oh, I think assignable is about the mvar depth: docs#Lean.MVarId.isAssignable, but I'm sure Sebastian knows! :smiley:

[Matthew Ballard]

https://gist.github.com/mattrobball/15f8c763eaa169195367d2745e5a8e22
with code

import Mathlib.LinearAlgebra.Dual
import Mathlib.Algebra.Module.LinearMap

variable {R : Type*} [Ring R]

def foo {R : Type*} [Semiring R] : R →ₗ[R] R where
  toFun := id
  map_add' := sorry
  map_smul' := sorry

def bar {R : Type*} [Ring R] : R →ₗ[R] R where
  toFun := id
  map_add' := sorry
  map_smul' := sorry

set_option profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option synthInstance.maxHeartbeats 0 in
set_option maxHeartbeats 0 in
example {R : Type*} [Semiring R] (p : R) : foo p = p := sorry -- fails
-- example {R : Type*} [Ring R] (p : R) : foo p = p := sorry -- fails
-- example {R : Type*} [Ring R]

[Matthew Ballard]

Keyboard not cooperating with reformatting for readability... :sad:

[Matthew Ballard]

Sebastian Ullrich said:

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Instance.20search.20without.20type/near/361934735

Yeah this ones (eventually) ends up at α [nonassignable] =?= ?m.33 [assignable]

[Sebastian Ullrich]

Well this really is a vexing elaboration issue you're handing to Lean:

• When looking at foo, we don't know R yet, but Lean tries to find an instance of Semiring for it anyway; that's the trace you were looking at but ultimately not the source of the problem
• We do know that we want to apply foo : ?m.2142 →ₗ[?m.2142] ?m.2142 to an argument, so let's try to find CoeFun (?m.2142 →ₗ[?m.2142] ?m.2142) ?m.2177 (the latter mvar is from the outParam: we want TC synth to find the value of that parameter even if we expect it to be R eventually)
• For that let's try FunLike (?m.2142 →ₗ[?m.2142] ?m.2142) ?m.2184 ?m.2185; so far, so good
• How about Module.Dual.instFunLikeDual? It fits, but only if we have Semiring ?m.2142
• Now Lean is in a pickle: it can't apply this instance yet, but it also can't rule it out yet because ?m.2142 might eventually be a semiring, so it would be wrong to continue the search with the remaining, i.e. lower-priority, instances. So the only thing Lean can do is to wait and see whether it gets more information about that metavariable from another source in some later step, which here is not the case

[Sebastian Ullrich]

Basically by inserting a higher-priority (in this case, declared-later, I assume) instance than the desired one, you leave Lean unable to continue with the given amount of information

[Matthew Ballard]

What is problematic about using Semiring R to start with? I ask in general more so than here.

[Matthew Ballard]

But one mathlib actionable thing I hear is to reduce the priority of Module.Dual.instFunLikeDual

[Matthew Ballard]

#6637 it goes through with low priority for instFunLikeDual

[Sebastian Ullrich]

Note that I don't necessarily recommend tweaking priorities for this reason, it might end up in a cat-and-mouse game. Ultimately CoeFun simply needs more information than this to work robustly.

[Eric Wieser]

Eric Wieser said:

This fixes it:

instance LinearMap.instCoeFun
  {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃]
  [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
CoeFun (M →ₛₗ[σ] M₃) fun x => M → M₃ := inferInstance -- or `⟨FunLike.coe⟩`

Do you think this sort of fix helps, or does this only work because it shuffles priorities again?

[Matthew Ballard]

Isn't that also tweaking priorities with declaration order?

[Matthew Ballard]

For reference, here is the trace without importing LinearAlgebra.Dual
https://gist.github.com/mattrobball/cd2c40f191a69b23241b7f913cc67555

[Matthew Ballard]

It seems to create an assignable metavariable for Semiring itself and then succeeds in unifying it with the provided instance.

[Matthew Ballard]

As opposed to Semiring ?_

[Matthew Ballard]

I guess we could just delete instFunLikeDual also lol

[Jireh Loreaux]

But it would be nice if we understood fully why we didn't have this problem in Lean 3, and because, as Mario indicated in the other thread, it seems like a bug. Moreover, I know that this isn't the only cause of this problem. I ran into another one with StarAlgHom that de-instancing instFunLikeDual didn't fix.

[Matthew Ballard]

It seems like assignability of the metavariables created is important. I think everything succeeds if one is assignable instead of unassignable.

I am sure there is a general reason for why they are marked as unassignable and I would love to understand it more.

[Matthew Ballard]

#6637 is updated to delete instFunLikeDual.

[Jireh Loreaux]

I'm pretty sure the problem is that, for reasons I don't understand in relation to this specific issue, the metavariables don't occur at the same mvar depth. Mvars are only assignable when the current MVar depth matches the depth at which the MVar was created.

[Jireh Loreaux]

There's a discussion of this in the metaprogramming book, but I don't understand how it applies to this particular instance search.

[Matthew Ballard]

That is another thing I will need to learn.

One difference between LinearMap.instFunLike and Module.Dual.instFunLikeDual was that the first created metavariables to unify with Semiring whereas the second only created a metavariable for the argument Semiring ?_.

I don't understand why.

[Matthew Ballard]

Here is a basic example with similar behavior

variable (α : Type)

class SR (α : Type) where

def f {α : Type} : α → α := sorry

def foo {α : Type} [SR α] (_ : α → α) : Type _ := sorry

set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
def bar {α : Type} [SR α] : foo f = foo f := sorry

It looks like it tries to unify ?1 → ?1 =?= ?2 → ?2 at context depth 0 and succeeds with ?1 := ?2. Then it bumps the depth and tries to do Semiring ?1 which it cannot solve because the depth of ?1 is 0.

[Matthew Ballard]

I am still confused since reading the comments in the file makes me think that the context depth only gets bumped with the creation of new metavariables.

[Notification Bot]

This topic was moved here from #general > Module.Dual and linear maps by Kyle Miller.