Zulip Chat Archive
Stream: mathlib4
Topic: Order.Hom.Lattice
Matej Penciak (Jan 24 2023 at 21:56):
I started this PR (https://github.com/leanprover-community/mathlib4/pull/1636) a bit ago, and I've been looking at the issues on and off over the last few days.
I think most of the errors are coming from a bunch of the instances of RelHomClass not being inferred (starting around line 188). I've tried debugging the best I can, but someone who understand this stuff better than I should probably take a look.
There are some totally unhelpful error messages like
type mismatch
map_top
has type
∀ (f : F), ↑f ⊤ = ⊤ : Prop
but is expected to have type
∀ (f : F), ↑f ⊤ = ⊤ : Prop
where if I hover over any given sub-expression all the types match up.
This is one of the files in the direction of Data.Complex.Basic, but it doesn't have a lot of immediate descendants so it's not blocking all that much right now.
Kevin Buzzard (Jan 24 2023 at 22:06):
set_option synthInstance.maxHeartbeats 2000
set_option trace.Meta.synthInstance true
-- See note [lower instance priority]
instance (priority := 100) BoundedLatticeHomClass.toBoundedOrderHomClass [Lattice α] [Lattice β]
[BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : BoundedOrderHomClass F α β :=
let foo : OrderHomClass F α β := inferInstance
sorry
gives
...
[resume] propagating (x_0 : Type _abstMVar.0) →
(x_1 : Type _abstMVar.1) →
(x_2 : Type _abstMVar.2) →
(x_3 : Type _abstMVar.3) →
(x_4 : Type _abstMVar.4) →
(x_5 : Type _abstMVar.5) →
(x_6 : Type _abstMVar.6) →
(x_7 : Type _abstMVar.7) →
(x_8 : Type _abstMVar.8) →
(x_9 : Type _abstMVar.9) →
(x_10 : Type _abstMVar.10) →
(x_11 : Type _abstMVar.11) →
(x_12 : Type _abstMVar.12) →
(x_13 : Type _abstMVar.13) →
(x_14 : Type _abstMVar.14) →
(x_15 : Type _abstMVar.15) →
(x_16 : Type _abstMVar.16) →
(x_17 : Type _abstMVar.17) →
(x_18 : Type _abstMVar.18) →
Bot
((WithTop x_0)ᵒᵈ ×
(WithTop x_1)ᵒᵈ ×
(WithTop x_2)ᵒᵈ ×
(WithTop x_3)ᵒᵈ ×
(WithTop x_4)ᵒᵈ ×
(WithTop x_5)ᵒᵈ ×
(WithTop x_6)ᵒᵈ ×
(WithTop x_7)ᵒᵈ ×
(WithTop x_8)ᵒᵈ ×
(WithTop x_9)ᵒᵈ ×
(WithTop x_10)ᵒᵈ ×
(WithTop x_11)ᵒᵈ ×
(WithTop x_12)ᵒᵈ ×
(WithTop x_13)ᵒᵈ ×
(WithTop x_14)ᵒᵈ ×
(WithTop x_15)ᵒᵈ ×
(WithTop x_16)ᵒᵈ ×
(WithTop x_17)ᵒᵈ ×
(WithTop
x_18)ᵒᵈ) to subgoal Bot
((WithTop ?m.21896)ᵒᵈ ×
(WithTop ?m.21897)ᵒᵈ ×
(WithTop ?m.21898)ᵒᵈ ×
(WithTop ?m.21899)ᵒᵈ ×
(WithTop ?m.21900)ᵒᵈ ×
(WithTop ?m.21901)ᵒᵈ ×
(WithTop ?m.21902)ᵒᵈ ×
(WithTop ?m.21903)ᵒᵈ ×
(WithTop ?m.21904)ᵒᵈ ×
(WithTop ?m.21905)ᵒᵈ ×
(WithTop ?m.21906)ᵒᵈ ×
(WithTop ?m.21907)ᵒᵈ ×
(WithTop ?m.21908)ᵒᵈ ×
(WithTop ?m.21909)ᵒᵈ ×
(WithTop ?m.21910)ᵒᵈ ×
(WithTop ?m.21911)ᵒᵈ ×
(WithTop ?m.21912)ᵒᵈ ×
(WithTop ?m.21913)ᵒᵈ ×
(WithTop
?m.21914)ᵒᵈ) of Bot
((WithTop ?m.21154)ᵒᵈ ×
(WithTop ?m.21896)ᵒᵈ ×
(WithTop ?m.21897)ᵒᵈ ×
(WithTop ?m.21898)ᵒᵈ ×
(WithTop ?m.21899)ᵒᵈ ×
(WithTop ?m.21900)ᵒᵈ ×
(WithTop ?m.21901)ᵒᵈ ×
(WithTop ?m.21902)ᵒᵈ ×
(WithTop ?m.21903)ᵒᵈ ×
(WithTop ?m.21904)ᵒᵈ ×
(WithTop ?m.21905)ᵒᵈ ×
(WithTop ?m.21906)ᵒᵈ ×
(WithTop ?m.21907)ᵒᵈ ×
(WithTop ?m.21908)ᵒᵈ ×
(WithTop ?m.21909)ᵒᵈ ×
(WithTop ?m.21910)ᵒᵈ ×
(WithTop ?m.21911)ᵒᵈ ×
(WithTop ?m.21912)ᵒᵈ × (WithTop ?m.21913)ᵒᵈ × (WithTop ?m.21914)ᵒᵈ) ▶
[resume] propagating (x_0 : Type _abstMVar.0) →
(x_1 : Type _abstMVar.1) →
(x_2 : Type _abstMVar.2) →
(x_3 : Type _abstMVar.3) →
...
Kevin Buzzard (Jan 24 2023 at 22:07):
Kevin Buzzard (Jan 24 2023 at 22:13):
Just telling Lean how to do it works:
instance (priority := 100) BoundedLatticeHomClass.toBoundedOrderHomClass [Lattice α] [Lattice β]
[BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : BoundedOrderHomClass F α β :=
{ show OrderHomClass F α β from SupHomClass.toOrderHomClass, ‹BoundedLatticeHomClass F α β› with }
Kevin Buzzard (Jan 24 2023 at 22:16):
This isn't going to end well either:
[resume] propagating Lattice α to subgoal Lattice α of Lattice (WithTop α) ▶
[resume] propagating Lattice (WithTop α) to subgoal Lattice (WithTop α) of Lattice (WithTop (WithTop α)) ▶
[resume] propagating Lattice
(WithTop (WithTop α)) to subgoal Lattice (WithTop (WithTop α)) of Lattice (WithTop (WithTop (WithTop α))) ▶
[resume] propagating Lattice
(WithTop
(WithTop
(WithTop
α))) to subgoal Lattice
(WithTop (WithTop (WithTop α))) of Lattice (WithTop (WithTop (WithTop (WithTop α)))) ▶
[resume] propagating Lattice
(WithTop
(WithTop
(WithTop
(WithTop
α)))) to subgoal Lattice
(WithTop (WithTop (WithTop (WithTop α)))) of Lattice (WithTop (WithTop (WithTop (WithTop (WithTop α))))) ▶
[resume] propagating Lattice
Kevin Buzzard (Jan 24 2023 at 22:38):
Here's the behaviour on master:
import Mathlib.Order.Hom.Basic
class SupHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] extends
FunLike F α fun _ => β where
map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b
class LatticeHomClass (F : Type _) (α β : outParam <| Type _) [Lattice α] [Lattice β] extends
SupHomClass F α β where
map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b
class BoundedLatticeHomClass (F : Type _) (α β : outParam <| Type _) [Lattice α] [Lattice β]
[BoundedOrder α] [BoundedOrder β] extends LatticeHomClass F α β where
map_top (f : F) : f ⊤ = ⊤
map_bot (f : F) : f ⊥ = ⊥
instance (priority := 100) SupHomClass.toOrderHomClass [SemilatticeSup α] [SemilatticeSup β]
[SupHomClass F α β] : OrderHomClass F α β :=
{ ‹SupHomClass F α β› with
map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }
example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
OrderHomClass F α β :=
SupHomClass.toOrderHomClass -- works
set_option synthInstance.maxHeartbeats 400 in -- to stop huge outputs crashing VS code
set_option trace.Meta.synthInstance true in
example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
OrderHomClass F α β :=
inferInstance -- loops
Kevin Buzzard (Jan 24 2023 at 22:41):
People who understand these traces better than me can usually stare at the output below and instantly go "it went wrong at precisely this point and that's your bad instance".
[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[] new goal RelHomClass F _tc.2 _tc.3 ▶
[] ✅ apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▶
[] ✅ apply @WithTop.semilatticeSup to SemilatticeSup (WithTop ?m.2939) ▶
[] ✅ apply Prod.semilatticeSup to SemilatticeSup (?m.2943 × ?m.2944) ▶
[] ✅ apply @WithTop.semilatticeSup to SemilatticeSup (WithTop ?m.2956) ▶
[] ✅ apply Prod.semilatticeSup to SemilatticeSup (?m.2960 × ?m.2961) ▶
[] ✅ apply OrderDual.semilatticeSup to SemilatticeSup ?m.2965ᵒᵈ ▶
[] ✅ apply @WithTop.semilatticeInf to SemilatticeInf (WithTop ?m.2976) ▶
[] ✅ apply Prod.semilatticeInf to SemilatticeInf (?m.2980 × ?m.2981) ▶
[] ✅ apply OrderDual.semilatticeInf to SemilatticeInf ?m.2985ᵒᵈ ▶
[] ✅ apply @WithBot.semilatticeInf to SemilatticeInf (WithBot ?m.2988) ▶
[] ✅ apply @Pi.semilatticeInf to SemilatticeInf ((i : ?m.2991) → ?m.2992 i) ▶
[] ✅ apply @WithTop.semilatticeInf to (i : ?m.2991) → SemilatticeInf (WithTop (?m.3006 i)) ▶
[] ✅ apply Prod.semilatticeInf to (i : ?m.2991) → SemilatticeInf (?m.3015 i × ?m.3016 i) ▶
[] ✅ apply OrderDual.semilatticeInf to (i : ?m.2991) → SemilatticeInf (?m.3025 i)ᵒᵈ ▶
[] ✅ apply @WithTop.semilatticeSup to (i : ?m.2991) → SemilatticeSup (WithTop (?m.3042 i)) ▶
[] ✅ apply Prod.semilatticeSup to (i : ?m.2991) → SemilatticeSup (?m.3051 i × ?m.3052 i) ▶
[] ✅ apply OrderDual.semilatticeSup to (i : ?m.2991) → SemilatticeSup (?m.3061 i)ᵒᵈ ▶
[] ✅ apply @WithBot.semilatticeSup to (i : ?m.2991) → SemilatticeSup (WithBot (?m.3069 i)) ▶
[] ✅ apply @Pi.semilatticeSup to (i : ?m.2991) → SemilatticeSup ((i_1 : ?m.3077 i) → ?m.3078 i i_1) ▶
[] ✅ apply @WithTop.semilatticeSup to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeSup (WithTop (?m.3098 i i_1)) ▶
[] ✅ apply Prod.semilatticeSup to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeSup (?m.3112 i i_1 × ?m.3113 i i_1) ▶
[] ✅ apply OrderDual.semilatticeSup to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeSup (?m.3127 i i_1)ᵒᵈ ▶
[] ✅ apply @WithTop.semilatticeInf to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeInf (WithTop (?m.3150 i i_1)) ▶
[] ✅ apply Prod.semilatticeInf to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeInf (?m.3164 i i_1 × ?m.3165 i i_1) ▶
[] ✅ apply OrderDual.semilatticeInf to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeInf (?m.3179 i i_1)ᵒᵈ ▶
[] ✅ apply @WithBot.semilatticeInf to (i : ?m.2991) → (i_1 : ?m.3077 i) → SemilatticeInf (WithBot (?m.3192 i i_1)) ▶
[] ✅ apply @Pi.semilatticeInf to (i : ?m.2991) →
(i_1 : ?m.3077 i) → SemilatticeInf ((i_2 : ?m.3205 i i_1) → ?m.3206 i i_1 i_2) ▶
[] ✅ apply @WithTop.semilatticeInf to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeInf (WithTop (?m.3232 i i_1 i_2)) ▶
[] ✅ apply Prod.semilatticeInf to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeInf (?m.3251 i i_1 i_2 × ?m.3252 i i_1 i_2) ▶
[] ✅ apply OrderDual.semilatticeInf to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeInf (?m.3271 i i_1 i_2)ᵒᵈ ▶
[] ✅ apply @WithTop.semilatticeSup to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeSup (WithTop (?m.3300 i i_1 i_2)) ▶
[] ✅ apply Prod.semilatticeSup to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeSup (?m.3319 i i_1 i_2 × ?m.3320 i i_1 i_2) ▶
[] ✅ apply OrderDual.semilatticeSup to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeSup (?m.3339 i i_1 i_2)ᵒᵈ ▶
[] ✅ apply @WithBot.semilatticeSup to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeSup (WithBot (?m.3357 i i_1 i_2)) ▶
[] ✅ apply @Pi.semilatticeSup to (i : ?m.2991) →
(i_1 : ?m.3077 i) → (i_2 : ?m.3205 i i_1) → SemilatticeSup ((i_3 : ?m.3375 i i_1 i_2) → ?m.3376 i i_1 i_2 i_3) ▶
[] ✅ apply @WithTop.semilatticeSup to (i : ?m.2991) →
(i_1 : ?m.3077 i) →
(i_2 : ?m.3205 i i_1) → (i_3 : ?m.3375 i i_1 i_2) → SemilatticeSup (WithTop (?m.3408 i i_1 i_2 i_3)) ▶
Kevin Buzzard (Jan 24 2023 at 22:42):
@Mario Carneiro you're one of those people ;-)
Kevin Buzzard (Jan 24 2023 at 22:43):
Is it this?
[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[] new goal RelHomClass F _tc.2 _tc.3 ▼
[instances] #[@OrderIsoClass.toOrderHomClass, @SupHomClass.toOrderHomClass]
[] ✅ apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[tryResolve] ✅ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ≟ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1
[] new goal SemilatticeSup _tc.0 ▼
[instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]
[] ✅ apply @WithTop.semilatticeSup to SemilatticeSup (WithTop ?m.2939) ▼
[tryResolve] ✅ SemilatticeSup (WithTop ?m.2939) ≟ SemilatticeSup (WithTop ?m.2939)
Kevin Buzzard (Jan 24 2023 at 22:45):
/-- `RelHomClass F r s` asserts that `F` is a type of functions such that all `f : F`
satisfy `r a b → s (f a) (f b)`.
The relations `r` and `s` are `outParam`s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
-/
class RelHomClass (F : Type _) {α β : outParam <| Type _} (r : outParam <| α → α → Prop)
(s : outParam <| β → β → Prop) extends FunLike F α fun _ => β where
/-- A `RelHomClass` sends related elements to related elements -/
map_rel : ∀ (f : F) {a b}, r a b → s (f a) (f b)
Mario Carneiro (Jan 24 2023 at 22:45):
It looks like the SemilatticeSup α goal in SupHomClass.toOrderHomClass is not being treated like an out-param
Kevin Buzzard (Jan 24 2023 at 22:46):
@SupHomClass.toOrderHomClass : {α : Type u_1} →
{β : Type u_2} →
{F : Type u_3} →
[inst : SemilatticeSup α] → [inst_1 : SemilatticeSup β] → [inst_2 : SupHomClass F α β] → OrderHomClass F α β
No mention of outparams there
Mario Carneiro (Jan 24 2023 at 22:47):
it looks like lean4#1852
Kevin Buzzard (Jan 24 2023 at 22:48):
Can you explain more precisely what this means? I only have the vaguest concept of what an out-param is.
Kevin Buzzard (Jan 24 2023 at 22:48):
this is all to do with when...unification?...tries to fill in a hole?
Mario Carneiro (Jan 24 2023 at 22:49):
Specifically, we have the goal OrderHomClass F ?α ?β (where ?α, ?β are forcibly made into metavariables because they are outparams) and want to find a solution to the typeclass problem which will determine ?α, ?β
Mario Carneiro (Jan 24 2023 at 22:50):
SemilatticeSup α does not have α as an outparam, so it would be a bad idea to do a typeclass search for SemilatticeSup ?α immediately, because that will enumerate all semilattices
Kevin Buzzard (Jan 24 2023 at 22:50):
which it's doing, right?
Mario Carneiro (Jan 24 2023 at 22:50):
right
Kevin Buzzard (Jan 24 2023 at 22:51):
instance (priority := 100) SupHomClass.toOrderHomClass [outparam (SemilatticeSup α)] [SemilatticeSup β]
[SupHomClass F α β] : OrderHomClass F α β :=
{ ‹SupHomClass F α β› with
map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }
/-
invalid binder annotation, type is not a class instance
?m.1448
use the command `set_option checkBinderAnnotations false` to disable the check
-/
Mario Carneiro (Jan 24 2023 at 22:51):
The correct order of evaluation here is:
SupHomClass F ?α ?β, which solves?α := αand?β := βSemilatticeSup αSemilatticeSup β
Mario Carneiro (Jan 24 2023 at 22:52):
you misspelled outParam
Mario Carneiro (Jan 24 2023 at 22:52):
it would be great if that worked, if only as a workaround, but I think that outparam annotations are ignored on instances
Kevin Buzzard (Jan 24 2023 at 22:54):
instance (priority := 100) SupHomClass.toOrderHomClass {α β : outParam <| Type _} [outParam (SemilatticeSup α)] [outParam (SemilatticeSup β)]
[outParam (SupHomClass F α β)] : OrderHomClass F α β :=
{ ‹SupHomClass F α β› with
map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }
This doesn't fix it
Mario Carneiro (Jan 24 2023 at 22:55):
Gabriel's workaround is to use {_ : SemilatticeSup α} in the instance, but I think that won't work here because SupHomClass requires HasSup instead of SemilatticeSup
Kevin Buzzard (Jan 24 2023 at 23:00):
I don't understand why this is happening
[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[] new goal RelHomClass F _tc.2 _tc.3 ▼
[instances] #[@OrderIsoClass.toOrderHomClass, @SupHomClass.toOrderHomClass]
[] ✅ apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[tryResolve] ✅ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ≟ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1
[] new goal outParam (SemilatticeSup _tc.0) ▼
[instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]
when we have this
RelHomClass : Type u_1 →
{α : outParam (Type u_2)} →
{β : outParam (Type u_3)} → outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max (max u_1 u_2) u_3)
Oh! The outParam falls off in this trace:
[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[] new goal RelHomClass F _tc.2 _tc.3 ▼
[instances] #[@OrderIsoClass.toOrderHomClass, @SupHomClass.toOrderHomClass]
[] ✅ apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
[tryResolve] ✅ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ≟ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1
[] new goal outParam (SemilatticeSup _tc.0) ▼
[instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]
[] ✅ apply @WithTop.semilatticeSup to outParam (SemilatticeSup (WithTop ?m.2962)) ▼
[tryResolve] ✅ outParam (SemilatticeSup (WithTop ?m.2962)) ≟ SemilatticeSup (WithTop ?m.2962)
[] new goal SemilatticeSup _tc.0 ▼
[instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]
The new goal was outParam (SemilatticeSup _tc.0) and then it became SemilatticeSup _tc.0
Mario Carneiro (Jan 24 2023 at 23:01):
outParam isn't really a tag on goals, it's a tag on arguments to a typeclass
Mario Carneiro (Jan 24 2023 at 23:01):
when it shows up elsewhere it's just a thing to be unfolded
Kevin Buzzard (Jan 24 2023 at 23:11):
What needs to be changed to make type class inference not try to solve SemilatticeSup _tc.0? Is this something which can be fixed in mathlib or does it need a change in core Lean? Do we need a new meme?
Kevin Buzzard (Jan 24 2023 at 23:27):
instance (priority := 100) SupHomClass.toOrderHomClass {α β : outParam <| Type _} [outParam (SemilatticeSup α)] [outParam (SemilatticeSup β)]
[outParam (SupHomClass F α β)] : OrderHomClass F α β :=
{ ‹SupHomClass F α β› with
map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }
This doesn't fix it.
Mario Carneiro (Jan 24 2023 at 23:46):
It's a core lean issue. Maybe @Gabriel Ebner has some ideas?
Gabriel Ebner (Jan 24 2023 at 23:48):
I didn't look through the whole thread yet. Does using {} instead of [] on the out-params help? Note that SupHomClass should not be an outparam.
Kevin Buzzard (Jan 25 2023 at 12:09):
Aah, in fact
instance (priority := 100) SupHomClass.toOrderHomClass {α β : outParam <| Type _}
{_ : outParam (SemilatticeSup α)} {_ : outParam (SemilatticeSup β)}
[SupHomClass F α β] : OrderHomClass F α β :=
{ ‹SupHomClass F α β› with
map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }
does fix the problem. This is the "bandaid" approach as described in lean4#1901 right? @Matej Penciak this is at least a temporary fix.
Last updated: Dec 20 2023 at 11:08 UTC