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_param
s 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