Strange "synthesize placeholder" error

Stream: general

[Michael Stoll]

import tactic

def weight (n d : ℕ) : Type := fin n.succ → ℕ

open_locale big_operators

variables {n d : ℕ}

def wsum (w : weight n d) : ℕ := ∑ j, w j

#check ∀ (w : weight n d) (σ : equiv.perm (fin n.succ)), wsum (w ∘ σ) = wsum w -- no problem here

example : ∀ (w : weight n d) (σ : equiv.perm (fin n.succ)), wsum (w ∘ σ) = wsum w := sorry

gives an error (at "wsum"):
don't know how to synthesize placeholder
context:
n d : ℕ,
w : weight n d,
σ : equiv.perm (fin n.succ)
⊢ ℕ

What is going on here?
Note that removing all ds leads to something that does typecheck... :confused:

[Michael Stoll]

I can do

lemma test : ∀ (w : weight n d) (σ : equiv.perm (fin n.succ)),
let w' : weight n d := w ∘ σ in wsum w' = wsum w := sorry

but then I don't know how I can use the lemma -- rw test or simp [test] does not work.

[Junyan Xu]

You probably need to make d explicit in wsum. When you do w ∘ σ, the type of w gets unfolded to a fin n.succ → ℕ and d can no longer be inferred.

[Eric Rodriguez]

(I don't see why removing the d causes issues, if I do it locally it seems fine)

[Eric Rodriguez]

example : ∀ (w : weight n d) (σ : equiv.perm (fin n.succ)), @wsum n d (w ∘ σ) = wsum w := sorry also works, or maybe also a weight.comp method that preserves d by definition

[Kyle Miller]

I'd expect

example : ∀ (w : weight n d) (σ : equiv.perm (fin n.succ)), wsum (w ∘ σ : weight n d) = wsum w := sorry

to work

[Eric Rodriguez]

it doesn't, that is the show X, from _ vs (_ : X) issue again Kyle

[Kyle Miller]

Oh well, too bad type ascriptions don't act as hints when elaborating function arguments...

[Kyle Miller]

Depending on what the intent is, one potential solution is to define a custom composition function, like wsum.perm, that returns weight n d.

[Kyle Miller]

Another is to change wsum to not take a weight n d, but a fin n -> nat

[Kyle Miller]

and yet another is to turn weight into a structure so that d cannot be erased from the type through unfolding

[Michael Stoll]

OK, thanks. I can live with the @ variant.