Type Mismatch Error

Stream: new members

[Finn Mortimore]

I am trying to add an instance that shows CompleteLattice implies ChainCompletePartialOrder, but I am encountering a type mismatch error. Would be grateful if someone could explain how to resolve this and what's going wrong (I am under the assumption it's something to do with the way the PartialOrder instance of CompleteLattice is inferred). All the relevant code is below:

import Mathlib.Order.Preorder.Chain
import Mathlib.Data.Set.Lattice

variable {α : Type*}

@[ext]
structure NonemptyChain (α : Type*) [LE α] where
  /-- The underlying set of a nonempty chain -/
  carrier : Set α
  Nonempty' : carrier.Nonempty
  isChain' : IsChain (· ≤ ·) carrier

instance {α : Type*} [LE α] : SetLike (NonemptyChain α) α where
  coe := NonemptyChain.carrier
  coe_injective' _ _ := NonemptyChain.ext

/-- A chain complete partial order (CCPO) is a nonempty partial order such that every
nonempty chain has a supremum (which we call `cSup`) -/
class ChainCompletePartialOrder (α : Type*) extends PartialOrder α where
  /-- The supremum of a nonempty chain -/
  cSup : NonemptyChain α → α
  /-- `cSup` is an upper bound of the nonempty chain -/
  le_cSup (c : NonemptyChain α) (x : α) : x ∈ c.carrier → x ≤ cSup c
  /-- `cSup` is a lower bound of the set of upper bounds of the nonempty chain -/
  cSup_le (c : NonemptyChain α) (x : α) : (∀ y ∈ c.carrier, y ≤ x) → cSup c ≤ x

variable [ChainCompletePartialOrder α] {x : α} {f : α → α}

instance [CompleteLattice α] : ChainCompletePartialOrder α where
  cSup c := sSup c
  le_cSup c x hx := le_sSup hx
  cSup_le c x h := sSup_le h

[Yaël Dillies]

You should remove the [ChainCompletePartialOrder α] from the variable above

[Kenny Lau]

Finn Mortimore said:

what's going wrong

what's going wrong is that you have a variable [ChainCompletePartialOrder α] which installs a meaning of ≤ for α, but then you also have instance [CompleteLattice α] : which installs a completely unrelated meaning, and these two are conflicting

[Finn Mortimore]

Thank you both!