Coercion of finset to set

Stream: general

[Michael Stoll]

import linear_algebra.finite_dimensional

variables {R : Type*} [division_ring R]
          {M : Type*} [add_comm_group M] [decidable_eq M] [module R M]

noncomputable def bar : finset M → ℕ := λ s : finset M, set.finrank R ↑s -- error
noncomputable def bar' : finset M → ℕ := λ s : finset M, set.finrank R (s : set M) -- works
def baz : finset M → Prop := λ s : finset M, set.inj_on (λ x : M, 0) ↑s -- works
def baz' : finset M → Prop := λ s : finset M, set.inj_on (λ x : M, 0) s -- works

Why does coercion of finsets to sets not work automatically with set.finrank, but does work with set.inj_on?

[Michael Stoll]

Note that #print bar' gives

noncomputable def bar' : Π (...), finset M → ℕ := λ (...) (s : finset M), set.finrank R ↑s

[Kevin Buzzard]

Probably Lean can't guess M in the first example

[Kevin Buzzard]

What's the error?

[Michael Stoll]

The error is

don't know how to synthesize placeholder
context:
R : Type u_1,
_inst_1 : division_ring R,
M : Type u_2,
_inst_2 : add_comm_group M,
_inst_3 : decidable_eq M,
_inst_4 : module R M,
s : finset M
⊢ Type ?

M is there , as far as I can see...

[Kevin Buzzard]

Sure it's there, but lean can't guess it in the first example (and that's what the error means). You tell it M explicitly in the second one. The issue that there could in theory be a coercion from finset M to set R. Silly I know but I think that's why it's asking for help.

[Michael Stoll]

I was just arriving at a similar conclusion...

[Michael Stoll]

The problem is that in set.finrank the module is implicit.

[Kevin Buzzard]

A couple of years ago when all this was dawning on me I think I had a bit of a moan about how silly all this was, but probably it's impossible to fix without editing core.

[Michael Stoll]

I guess the upshot is that when I write ↑s the target type needs to be known (to Lean, not to me :smile: ), and in this case, it isn't.

[Michael Stoll]

Thanks for enlightening me!