Zulip Chat Archive

Stream: general

Topic: Why isn't my `out_param` getting inferred?


Anne Baanen (Dec 20 2021 at 13:28):

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 (Dec 20 2021 at 13:33):

Is the [A iA oA] tripping it up?

Anne Baanen (Dec 20 2021 at 13:34):

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

Anne Baanen (Dec 20 2021 at 16:49):

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 (Dec 20 2021 at 16:51):

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 (Dec 20 2021 at 17:00):

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

Anne Baanen (Dec 20 2021 at 17:15):

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 (Dec 20 2021 at 17:16):

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 (Dec 20 2021 at 17:33):

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 (Jan 04 2022 at 15:15):

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 (Jan 04 2022 at 15:28):

Will we have two Lean releases on one day?

Eric Rodriguez (Jan 04 2022 at 15:30):

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

Anne Baanen (Jan 04 2022 at 15:35):

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


Last updated: Dec 20 2023 at 11:08 UTC