Why isn't my `out_param` getting inferred?

Stream: general

[Anne Baanen]

The following example is minimized fron trying to parametrize semilinear_map_class over an out_param (R →+* S). I expect both B.b and B.b' to work, but the second fails for some reason.

universes u v w x

variables (iA : Type u) (oA : Type v) (iB : Type w) (oB : Type x)

class A (iA : Type u) (oA : out_param $ Type v) :=
(a : iA → oA)
class B (iB : Type w) (oB : out_param $ Type x) (iA : out_param $ Type u) (oA : out_param $ Type v) [A iA oA] :=
(b : iB → iA → oB)
(b' : iB → oA → oB)

example [A iA oA] [B iB oB iA oA] (x : iB) (y : iA) : oB := B.b x y -- works

example [A iA oA] [B iB oB iA oA] (x : iB) (y : oA) : oB := B.b' x y -- fails: don't know how to synthesize placeholder
example [A iA oA] [B iB oB iA oA] (x : iB) (y : oA) : oB := @B.b' _ _ iA _ _ _ x y -- works

[Johan Commelin]

Is the [A iA oA] tripping it up?

[Anne Baanen]

I think so. Making the instance an out_param too makes everything work.

[Anne Baanen]

Here's another mysterious failure:

class to_fun (i : Type) (o : out_param Type) :=
(coe : i → o)
structure ring_hom (R S : Type) : Type := (coe : R → S)

class module (R M : Type) :=
(op : R → M → M)

class semilinear_map_class (F : Type) (R S M N : out_param $ Type) (h : out_param $ ring_hom R S)
  [module R M] [out_param $ module S N] /- `rw` fails if `[module S N]` is not an `out_param` -/
  [to_fun F (M → N)] :=
(map_smul : ∀ (f : F) (c : R) (x : M), (to_fun.coe f : M → N) (module.op c x) = module.op ((ring_hom.coe h : R → S) c) ((to_fun.coe f : M → N) x))

attribute [simp] semilinear_map_class.map_smul

variables {F R S M N : Type} {h : ring_hom R S} [module R M] [module S N] [to_fun F (M → N)] [i : semilinear_map_class F R S M N h] (f : F)
include i

set_option trace.simplify true

example (h' : S → R) (c' : S) (x : M) : module.op ((ring_hom.coe h : R → S) (h' c')) ((to_fun.coe f : M → N) x) = (to_fun.coe f : M → N) (module.op (h' c') x) :=
by rw [semilinear_map_class.map_smul] -- works

example (h' : S → R) (c' : S) (x : M) : module.op ((ring_hom.coe h : R → S) (h' c')) ((to_fun.coe f : M → N) x) = (to_fun.coe f : M → N) (module.op (h' c') x) :=
by simp only [semilinear_map_class.map_smul]
-- [simplify.failure] fail to instantiate emetas: 'semilinear_map_class.map_smul' at
-- @to_fun.coe F (M → N) _inst_3 f (@module.op R M _inst_1 (h' c') x)
-- partially instantiated lemma: @semilinear_map_class.map_smul F R ?x_2 ?x_3 M N _inst_1 ?x_7 _inst_3 ?x_9 f (h' c') x

[Anne Baanen]

According to the debugger, the error is that on the third emeta (not sure what this is) the function has_idx_metavar (don't know what that is) returns true.

[Anne Baanen]

Sorry, that was with universe variables. Without universe variables, the error is "failed to assign" instead, also on the third emeta.

[Anne Baanen]

Minified further:

section
class broken₁ (A : Type*) :=
(f : A → A)
open broken₁

class broken₂ (A : Type*) (a : out_param $ A) [out_param $ broken₁ A] :=
(f_eq : ∀ x, f x = a)
open broken₂

example (A : Type*) (a : A) [broken₁ A] [broken₂ A a] (x : A) : f x = a :=
by rw [f_eq]

example (A : Type*) (a : A) [broken₁ A] [broken₂ A a] (x : A) : f x = a :=
by simp only [f_eq] -- fail to instantiate emetas

end

[Anne Baanen]

So the specific error is: simp can't instantiate out_params of a class appearing in a simp lemma, if that class doesn't appear in the LHS of the lemma.

[Anne Baanen]

This also happens for bundled classes, but you have to use explicit instances to find the error:

class broken₁ (A : Type*) :=
(f : A → A)
open broken₁

class broken₂ (A : Type*) (a : out_param $ A)
  extends broken₁ A :=
(f_eq : ∀ x, f x = a)
open broken₂

example (A : Type*) (a : A) [broken₂ A a] (x : A) : f x = a :=
by rw [f_eq] -- works

example (A : Type*) (a : A) [broken₂ A a] (x : A) : f x = a :=
by simp only [f_eq] -- works

-- This makes `f (x : ℕ)` parse as `@@broken₁.f nat.broken₁ x`
instance nat.broken₁ : broken₁ ℕ :=
{ f := λ _, 0 }

instance nat.broken₂ : broken₂ ℕ 0 :=
{ f := λ _, 0,
  f_eq := λ _, rfl }

example (x : ℕ) : f x = 0 := by simp only [f_eq] -- doesn't work

[Anne Baanen]

The "out_param instance parameter" issue is fixed in lean#657, and the "simp can't fill out_params" issue is fixed in lean#659 :tada:

[Johan Commelin]

Will we have two Lean releases on one day?

[Eric Rodriguez]

oh man, I was already so excited for 3.36.0 that I started updating mathlib already ^^ this is amazing!

[Anne Baanen]

Let's hope there are no more bugs to be discovered through further out_param (ab)use :P