diff --git a/src/main/scala/analysis/EdgeFunctionLattice.scala b/src/main/scala/analysis/EdgeFunctionLattice.scala
index 544787e04..8801a1750 100644
--- a/src/main/scala/analysis/EdgeFunctionLattice.scala
+++ b/src/main/scala/analysis/EdgeFunctionLattice.scala
@@ -24,8 +24,10 @@ trait EdgeFunction[T] extends (T => T) {
 class EdgeFunctionLattice[T, L <: Lattice[T]](val valuelattice: L) extends Lattice[EdgeFunction[T]] {
 
   val bottom: ConstEdge = ConstEdge(valuelattice.bottom)
+  def top: Nothing = ???
 
   def lub(x: EdgeFunction[T], y: EdgeFunction[T]): EdgeFunction[T] = x.joinWith(y)
+  def glb(x: EdgeFunction[T], y: EdgeFunction[T]): Nothing = ???
 
   /** Edge labeled with identity function.
     */
diff --git a/src/main/scala/analysis/GammaDomains.scala b/src/main/scala/analysis/GammaDomains.scala
index a7676c9c6..a6f0c1330 100644
--- a/src/main/scala/analysis/GammaDomains.scala
+++ b/src/main/scala/analysis/GammaDomains.scala
@@ -4,8 +4,6 @@ import ir.*
 
 type VarGammaMap = LatticeMap[Variable, LatticeSet[Variable]]
 
-implicit val variableLatticeSetTerm: LatticeSet[Variable] = LatticeSet.Bottom()
-
 /**
  * An abstract domain that determines for each variable, a set of variables whose gammas (at
  * the start of a procedure) are "affected" this variable's gamma. This is paramaterised by
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index f50ae6877..e2df72894 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -5,32 +5,78 @@ import ir.eval.BitVectorEval
 import util.StaticAnalysisLogger
 import util.assertion.*
 
-/** Basic lattice
-  */
+/**
+ * Lattice operations on the given type `T`. This is intended to be used
+ * as a [type-class]. Notably, this means that the T class should *not*
+ * directly extend [[Lattice]][T]. Rather, a separate class should be created
+ * to extend `Lattice[T]` (this is automated if you use the [given syntax]).
+ * Placing the lattice methods outside of the class itself gives us a lot
+ * more flexibility.
+ *
+ * To access the methods within this trait, you should add a
+ * "using" clause like `(using l: Lattice[DesiredType])` to the end of the
+ * parameter list of a method or class. Then, you will have access to an `l`
+ * variable containing the [[Lattice]] methods. See [given syntax] docs for
+ * more details, including how to define given instances.
+ *
+ * [type-class]: https://docs.scala-lang.org/scala3/book/ca-type-classes.html
+ * [given syntax]: https://docs.scala-lang.org/scala3/reference/contextual/previous-givens.html
+ *
+ * To invoke a method or class constructor which has a "using" clause, you will
+ * need to either:
+ *
+ * - (1) explicitly pass a value for the using parameter by suffixing `(using l)`
+ *   to the method/constructor call (where `l` is a value of the correct type), or
+ * - (2) have a `given` clause in scope which declares a [[Lattice]] value with a
+ *   compatible type. When a `given` clause appears in a different file, it may
+ *   need to be imported with `import package_name.given` - the compiler should
+ *   help you with this. Note that not all subtypes of [[Lattice]] are declared
+ *   as `given`. If you need to use a non-given instance, you can either use
+ *   (1) or, if the instance is canonical for its type, you can add a new
+ *   `given Lattice[TheType] = ...` statement.
+ */
 trait Lattice[T]:
 
   type Element = T
 
   /** The bottom element of this lattice.
     */
-  val bottom: T
+  def bottom: T
 
-  /** The top element of this lattice. Default: not implemented.
+  /** The top element of this lattice.
     */
-  def top: T = ???
+  def top: T
 
   /** The least upper bound of `x` and `y`.
     */
   def lub(x: T, y: T): T
 
-  /** The greatest lower bound of `x` and `y`
+  /** The greatest lower bound of `x` and `y`.
     */
-  def glb(x: T, y: T): T = ???
+  def glb(x: T, y: T): T
 
   /** Returns true whenever `x` <= `y`.
     */
   def leq(x: T, y: T): Boolean = lub(x, y) == y // rarely used, but easy to implement :-)
 
+  /**
+   * These convenience methods give easy access to the `join` and `meet` functions through
+   * the `.meet` and `.join` syntax.
+   *
+   * These methods are provided by the [[Lattice]] trait and can be used whenever a
+   * [[Lattice]] (with the correct type) is in scope.
+   */
+  extension (x: T)
+    def join(y: T) = lub(x, y)
+    def meet(y: T) = glb(x, y)
+
+object Lattice {
+
+  /** Summons a [[Lattice]] instance for the required type. By using this method,
+   *  the [[Lattice]] methods can be accessed by, for example, `Lattice().top`. */
+  def apply[T](using l: Lattice[T]) = l
+}
+
 trait StridedWrappedInterval
 
 case class SI(s: BigInt, l: BigInt, u: BigInt, w: BigInt) extends StridedWrappedInterval {
@@ -54,9 +100,9 @@ class SASILattice extends Lattice[StridedWrappedInterval] {
   val lowestPossibleValue: BigInt = 0
   val highestPossibleValue: BigInt = Long.MaxValue - 1
 
-  override val bottom: StridedWrappedInterval = SIBottom
+  val bottom: StridedWrappedInterval = SIBottom
 
-  override def top: StridedWrappedInterval = SITop
+  val top: StridedWrappedInterval = SITop
 
   //  def gamma(x: StridedWrappedInterval): Set[BitVecLiteral] = x match {
   //    case SIBottom => Set.empty
@@ -123,8 +169,10 @@ class SASILattice extends Lattice[StridedWrappedInterval] {
     }
   }
 
+  def glb(r: StridedWrappedInterval, t: StridedWrappedInterval): Nothing = ???
+
   /** S1[L1, U1] join S2[L2, U2] -> gcd(S1, S2)[min(L1, L2), max(U1, U2)] */
-  override def lub(r: StridedWrappedInterval, t: StridedWrappedInterval): StridedWrappedInterval = {
+  def lub(r: StridedWrappedInterval, t: StridedWrappedInterval): StridedWrappedInterval = {
     (r, t) match {
       case (SIBottom, t) => t
       case (t, SIBottom) => t
@@ -273,13 +321,15 @@ class ValueSetLattice[T] extends Lattice[ValueSet[T]] {
     override def toString = "VSTop"
   }
 
-  override val bottom: ValueSet[T] = VSBottom
+  val bottom: ValueSet[T] = VSBottom
 
-  override def top: ValueSet[T] = VSTop
+  val top: ValueSet[T] = VSTop
 
   val lattice: SASILattice = SASILattice()
 
-  override def lub(x: ValueSet[T], y: ValueSet[T]): ValueSet[T] = {
+  def glb(x: ValueSet[T], y: ValueSet[T]): Nothing = ???
+
+  def lub(x: ValueSet[T], y: ValueSet[T]): ValueSet[T] = {
     (x, y) match {
       case (VSBottom, t) => t
       case (t, VSBottom) => t
@@ -485,11 +535,11 @@ case object MAYBE_BOOL3 extends Bool3 {
   */
 class Bool3Lattice extends Lattice[Bool3] {
 
-  override val bottom: Bool3 = BOTTOM_BOOL3
+  val bottom: Bool3 = BOTTOM_BOOL3
 
-  override def top: Bool3 = MAYBE_BOOL3
+  val top: Bool3 = MAYBE_BOOL3
 
-  override def lub(x: Bool3, y: Bool3): Bool3 = {
+  def lub(x: Bool3, y: Bool3): Bool3 = {
     (x, y) match {
       case (BOTTOM_BOOL3, t) => t
       case (t, BOTTOM_BOOL3) => t
@@ -498,6 +548,8 @@ class Bool3Lattice extends Lattice[Bool3] {
       case _ => x
     }
   }
+
+  def glb(x: Bool3, y: Bool3): Nothing = ???
 }
 
 enum Flags {
@@ -526,9 +578,9 @@ case class FlagMap(m: Map[Flags, Bool3]) extends Flag {
   */
 class FlagLattice extends Lattice[Flag] {
 
-  override val bottom: Flag = BOTTOM_Flag
+  val bottom: Flag = BOTTOM_Flag
 
-  override def top: Flag = FlagMap(
+  val top: Flag = FlagMap(
     Map(
       Flags.CF -> MAYBE_BOOL3,
       Flags.ZF -> MAYBE_BOOL3,
@@ -541,7 +593,8 @@ class FlagLattice extends Lattice[Flag] {
 
   val lattice: Bool3Lattice = Bool3Lattice()
 
-  override def lub(x: Flag, y: Flag): Flag = {
+  def glb(x: Flag, y: Flag): Nothing = ???
+  def lub(x: Flag, y: Flag): Flag = {
     (x, y) match {
       case (BOTTOM_Flag, t) => t
       case (t, BOTTOM_Flag) => t
@@ -563,16 +616,22 @@ class FlagLattice extends Lattice[Flag] {
   */
 class PowersetLattice[A] extends Lattice[Set[A]] {
   val bottom: Set[A] = Set.empty
+  def top: Nothing = ???
   def lub(x: Set[A], y: Set[A]): Set[A] = x.union(y)
+  def glb(x: Set[A], y: Set[A]): Nothing = ???
 }
 
+given [A]: Lattice[Set[A]] = PowersetLattice[A]()
+
 // Single element lattice (using Option)
 class SingleElementLattice[T] extends Lattice[Option[T]] {
   val bottom: Option[T] = None
+  def top: Nothing = ???
   def lub(x: Option[T], y: Option[T]): Option[T] = (x, y) match {
     case (None, None) => None
     case _ => Some(x.getOrElse(y.get))
   }
+  def glb(x: Option[T], y: Option[T]): Nothing = ???
 }
 
 trait LiftedElement[+T]
@@ -588,7 +647,9 @@ case object LiftedBottom extends LiftedElement[Nothing] {
 class LiftLattice[T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
 
   val bottom: LiftedElement[T] = LiftedBottom
+  def top: Nothing = ???
 
+  def glb(x: LiftedElement[T], y: LiftedElement[T]): Nothing = ???
   def lub(x: LiftedElement[T], y: LiftedElement[T]): LiftedElement[T] =
     (x, y) match {
       case (LiftedBottom, t) => t
@@ -621,6 +682,7 @@ class TwoElementLattice extends Lattice[TwoElement]:
   override val bottom: TwoElement = TwoElementBottom
   override val top: TwoElement = TwoElementTop
 
+  def glb(x: TwoElement, y: TwoElement): Nothing = ???
   def lub(x: TwoElement, y: TwoElement): TwoElement = (x, y) match {
     case (TwoElementBottom, TwoElementBottom) => TwoElementBottom
     case _ => TwoElementTop
@@ -638,8 +700,9 @@ class FlatLattice[X] extends Lattice[FlatElement[X]] {
 
   val bottom: FlatElement[X] = Bottom
 
-  override val top: FlatElement[X] = Top
+  val top: FlatElement[X] = Top
 
+  def glb(x: FlatElement[X], y: FlatElement[X]): Nothing = ???
   def lub(x: FlatElement[X], y: FlatElement[X]): FlatElement[X] = (x, y) match {
     case (a, Bottom) => a
     case (Bottom, b) => b
@@ -656,8 +719,9 @@ class FlatLatticeWithDefault[X](val f: () => X) extends Lattice[FlatElement[X]]
 
   val bottom: FlatElement[X] = FlatEl(f())
 
-  override val top: FlatElement[X] = Top
+  val top: FlatElement[X] = Top
 
+  def glb(x: FlatElement[X], y: FlatElement[X]): Nothing = ???
   def lub(x: FlatElement[X], y: FlatElement[X]): FlatElement[X] = (x, y) match {
     case (a, Bottom) => a
     case (Bottom, b) => b
@@ -670,9 +734,11 @@ class FlatLatticeWithDefault[X](val f: () => X) extends Lattice[FlatElement[X]]
 
 class TupleLattice[+L1 <: Lattice[T1], +L2 <: Lattice[T2], T1, T2](val lattice1: L1, val lattice2: L2)
     extends Lattice[(T1, T2)] {
-  override val bottom: (T1, T2) = (lattice1.bottom, lattice2.bottom)
+  val bottom: (T1, T2) = (lattice1.bottom, lattice2.bottom)
 
-  override def lub(x: (T1, T2), y: (T1, T2)): (T1, T2) = {
+  def glb(x: (T1, T2), y: (T1, T2)): Nothing = ???
+
+  def lub(x: (T1, T2), y: (T1, T2)): (T1, T2) = {
     val (x1, x2) = x
     val (y1, y2) = y
     (lattice1.lub(x1, y1), lattice2.lub(x2, y2))
@@ -684,7 +750,7 @@ class TupleLattice[+L1 <: Lattice[T1], +L2 <: Lattice[T2], T1, T2](val lattice1:
     lattice1.leq(x1, y1) && lattice2.leq(x2, y2)
   }
 
-  override def top: (T1, T2) = (lattice1.top, lattice2.top)
+  def top: (T1, T2) = (lattice1.top, lattice2.top)
 }
 
 /** A lattice of maps from a set of elements of type `A` to a lattice with element `L'. Bottom is the default value.
@@ -693,6 +759,9 @@ class MapLattice[A, T, +L <: Lattice[T]](val sublattice: L) extends Lattice[Map[
   val bottom: Map[A, T] = Map().withDefaultValue(sublattice.bottom)
   def lub(x: Map[A, T], y: Map[A, T]): Map[A, T] =
     x.keys.foldLeft(y)((m, a) => m + (a -> sublattice.lub(x(a), y(a)))).withDefaultValue(sublattice.bottom)
+
+  def glb(x: Map[A, T], y: Map[A, T]): Nothing = ???
+  def top: Nothing = ???
 }
 
 /** Constant propagation lattice.
diff --git a/src/main/scala/analysis/LatticeCollections.scala b/src/main/scala/analysis/LatticeCollections.scala
index 09586c2d3..3982b72b4 100644
--- a/src/main/scala/analysis/LatticeCollections.scala
+++ b/src/main/scala/analysis/LatticeCollections.scala
@@ -3,31 +3,6 @@ package analysis
 import ir.*
 import ir.transforms.AbstractDomain
 
-import scala.annotation.implicitNotFound
-
-/** Lattice structure internal to a type.
-  */
-trait InternalLattice[T <: InternalLattice[T]] {
-  def join(other: T): T
-  def meet(other: T): T
-
-  def top: T
-  def bottom: T
-}
-
-/**
- * A Lattice over a type that implements the InternalLattice trait.
- *
- * The `term` parameter can be any term of the type L, it just needs to exist to be able to call the top and bottom methods.
- */
-class InternalLatticeLattice[L <: InternalLattice[L]](term: L) extends Lattice[L] {
-  def lub(x: L, y: L): L = x.join(y)
-  override def glb(x: L, y: L): L = x.meet(y)
-
-  val bottom: L = term.bottom
-  override def top: L = term.top
-}
-
 object LatticeSet {
 
   /** Create a FiniteSet only if `s` is non-empty, else make Bottom. */
@@ -41,7 +16,7 @@ object LatticeSet {
  * An element of a powerset lattice. This type represents Top and Bottom and finite sets, and is closed under
  * unions, intersections, and set difference.
  */
-enum LatticeSet[T] extends InternalLattice[LatticeSet[T]] {
+enum LatticeSet[T] {
   import LatticeSet.{finiteSet, diffSet}
 
   /* The set of all terms of type T */
@@ -108,9 +83,6 @@ enum LatticeSet[T] extends InternalLattice[LatticeSet[T]] {
   def --(other: LatticeSet[T]): LatticeSet[T] = this.diff(other)
   def --(other: Iterable[T]): LatticeSet[T] = this.diff(FiniteSet(other.toSet))
 
-  def top: LatticeSet[T] = Top()
-  def bottom: LatticeSet[T] = Bottom()
-
   /** Try to convert to a finitely represented set. Returns None if this set is infinite
     */
   def tryToSet: Option[Set[T]] = {
@@ -131,65 +103,52 @@ enum LatticeSet[T] extends InternalLattice[LatticeSet[T]] {
   }
 }
 
-class LatticeSetLattice[T] extends Lattice[LatticeSet[T]] {
-  import LatticeSet.{Top, Bottom}
-
-  type Element = LatticeSet[T];
-
-  def lub(a: LatticeSet[T], b: LatticeSet[T]): LatticeSet[T] = a.join(b)
-
-  override def glb(a: LatticeSet[T], b: LatticeSet[T]): LatticeSet[T] = a.meet(b)
+class LatticeSetLattice[T]() extends Lattice[LatticeSet[T]] {
+  import LatticeSet.*
 
-  override def top: LatticeSet[T] = Top()
+  val top: LatticeSet[T] = Top()
   val bottom: LatticeSet[T] = Bottom()
+
+  def lub(x: LatticeSet[T], y: LatticeSet[T]) = x.join(y)
+  def glb(x: LatticeSet[T], y: LatticeSet[T]) = x.meet(y)
 }
 
+given [T]: Lattice[LatticeSet[T]] = LatticeSetLattice()
+
 object LatticeMap {
 
   /** Create a TopMap only if `m` is non-empty, else make Top. */
-  def topMap[D, L](m: Map[D, L]): LatticeMap[D, L] = if m.isEmpty then LatticeMap.Top() else LatticeMap.TopMap(m)
+  def topMap[D, L](m: Map[D, L])(using l: Lattice[L]): LatticeMap[D, L] =
+    if m.isEmpty then LatticeMap.Top() else LatticeMap.TopMap(m)
 
   /** Create a BottomMap only if `m` is non-empty, else make Bottom. */
-  def bottomMap[D, L](m: Map[D, L]): LatticeMap[D, L] =
+  def bottomMap[D, L](m: Map[D, L])(using l: Lattice[L]): LatticeMap[D, L] =
     if m.isEmpty then LatticeMap.Bottom() else LatticeMap.BottomMap(m)
 }
 
 /** A map which defaults to either the top or bottom element of a lattice. This is more efficient to use in static
   * analyses as it is common to default most values in a map to either top or bottom.
-  *
-  * In order to call `apply`, `join` or `meet`, an implicit term of type L must be declared, and L must implement the
-  * `InternalLattice` trait. For example, to declare an implicit interval, we write (outside the scope of any classes
-  * that we are implementing)
-  * ```scala
-  * private implicit val intervalTerm: Interval = Interval.Bottom
-  * ```
   */
-enum LatticeMap[D, L] {
+enum LatticeMap[D, L](using l: Lattice[L]) {
   /* PERFORMANCE:
    * Something like an AVL tree could be more efficient, see section 4.1.4 of Antoine Miné's abstract interpretation
    * tutorial.
    */
 
   /* A map that is top everywhere */
-  case Top[D1, L1]() extends LatticeMap[D1, L1]
+  case Top[D1, L1]()(using Lattice[L1]) extends LatticeMap[D1, L1]
   /* A map that is bottom everywhere */
-  case Bottom[D1, L1]() extends LatticeMap[D1, L1]
+  case Bottom[D1, L1]()(using Lattice[L1]) extends LatticeMap[D1, L1]
   /* A Map which defaults to top and is else specified by the internal map */
-  case TopMap[D1, L1](m: Map[D1, L1]) extends LatticeMap[D1, L1]
+  case TopMap[D1, L1](m: Map[D1, L1])(using Lattice[L1]) extends LatticeMap[D1, L1]
   /* A Map which defaults to bottom and is else specified by the internal map */
-  case BottomMap[D1, L1](m: Map[D1, L1]) extends LatticeMap[D1, L1]
+  case BottomMap[D1, L1](m: Map[D1, L1])(using Lattice[L1]) extends LatticeMap[D1, L1]
 
   /** Update this map so that `from` now maps to `to` */
-  def update[L1 <: InternalLattice[L1]](pair: (D, L))(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): LatticeMap[D, L] = this.update(pair(0), pair(1))
+  def update(pair: (D, L)): LatticeMap[D, L] = this.update(pair(0), pair(1))
 
   /** Update this map so that `from` now maps to `to` */
-  def update[L1 <: InternalLattice[L1]](from: D, to: L)(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): LatticeMap[D, L] = this match {
+  def update(from: D, to: L): LatticeMap[D, L] = this match {
     case Top() => TopMap(Map(from -> to))
     case Bottom() => BottomMap(Map(from -> to))
     case TopMap(m) => if to == l.top then TopMap(m - from) else TopMap(m + (from -> to))
@@ -212,38 +171,23 @@ enum LatticeMap[D, L] {
     case BottomMap(m) => m
   }
 
-  def +[L1 <: InternalLattice[L1]](kv: (D, L))(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): LatticeMap[D, L] = update(kv._1, kv._2)
-  def ++[L1 <: InternalLattice[L1]](kv: Map[D, L])(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): LatticeMap[D, L] = kv.foldLeft(this) { (m, kv) => m + kv }
+  def +(kv: (D, L)): LatticeMap[D, L] = update(kv._1, kv._2)
+  def ++(kv: Map[D, L]): LatticeMap[D, L] = kv.foldLeft(this) { (m, kv) => m + kv }
 
   /** Evaluate the function at `v`, accounting for defaulting behaviour.
     */
-  def apply[L1 <: InternalLattice[L1]](v: D)(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): L1 = this match {
+  def apply(v: D): L = this match {
     case Top() => l.top
     case Bottom() => l.bottom
-    case TopMap(m) => m.getOrElse(v, l.top).asInstanceOf[L1]
-    case BottomMap(m) => m.getOrElse(v, l.bottom).asInstanceOf[L1]
+    case TopMap(m) => m.getOrElse(v, l.top)
+    case BottomMap(m) => m.getOrElse(v, l.bottom)
   }
 
-  def join[L1 <: InternalLattice[L1]](other: LatticeMap[D, L1])(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): LatticeMap[D, L1] =
-    latticeMapJoin(this.asInstanceOf[LatticeMap[D, L1]], other, (a, b) => a.join(b), l.top, l.bottom)
+  def join(other: LatticeMap[D, L]): LatticeMap[D, L] =
+    latticeMapJoin(this, other, (a, b) => a.join(b), l.top, l.bottom)
 
-  def meet[L1 <: InternalLattice[L1]](other: LatticeMap[D, L1])(implicit
-    s: L <:< L1,
-    @implicitNotFound("No implicit of type ${L1} was found. See LatticeMap docs for more info.") l: L1
-  ): LatticeMap[D, L1] =
-    latticeMapMeet(this.asInstanceOf[LatticeMap[D, L1]], other, (a, b) => a.meet(b), l.top, l.bottom)
+  def meet(other: LatticeMap[D, L]): LatticeMap[D, L] =
+    latticeMapMeet(this, other, (a, b) => a.meet(b), l.top, l.bottom)
 
   def top: LatticeMap[D, L] = Top()
   def bottom: LatticeMap[D, L] = Bottom()
@@ -255,7 +199,7 @@ private def latticeMapJoin[D, L](
   join: ((L, L) => L),
   top: => L,
   bottom: => L
-): LatticeMap[D, L] = {
+)(using Lattice[L]): LatticeMap[D, L] = {
   import LatticeMap.*
 
   def joinMaps(m1: Map[D, L], m2: Map[D, L], d1: L, d2: L) =
@@ -280,7 +224,7 @@ private def latticeMapMeet[D, L](
   meet: ((L, L) => L),
   top: => L,
   bottom: => L
-): LatticeMap[D, L] = {
+)(using Lattice[L]): LatticeMap[D, L] = {
   import LatticeMap.*
 
   def meetMaps(m1: Map[D, L], m2: Map[D, L], d1: L, d2: L) =
@@ -301,7 +245,7 @@ private def latticeMapMeet[D, L](
 
 /** Evaluate the map m at value d, defaulting based on the top and bottom values in the lattice l.
   */
-def latticeMapApply[D, L, LA <: Lattice[L]](m: LatticeMap[D, L], d: D, l: LA): L = {
+def latticeMapApply[D, L](m: LatticeMap[D, L], d: D)(using l: Lattice[L]): L = {
   import LatticeMap.{Top, Bottom, TopMap, BottomMap}
 
   m match {
@@ -312,10 +256,8 @@ def latticeMapApply[D, L, LA <: Lattice[L]](m: LatticeMap[D, L], d: D, l: LA): L
   }
 }
 
-class LatticeMapLattice[D, L, LA <: Lattice[L]](l: LA) extends Lattice[LatticeMap[D, L]] {
-  import LatticeMap.{Top, Bottom}
-
-  type Element = LatticeMap[D, L];
+class LatticeMapLattice[D, L](l: Lattice[L]) extends Lattice[LatticeMap[D, L]] {
+  protected given Lattice[L] = l
 
   def lub(a: LatticeMap[D, L], b: LatticeMap[D, L]): LatticeMap[D, L] =
     latticeMapJoin(a, b, (x, y) => l.lub(x, y), l.top, l.bottom)
@@ -323,14 +265,16 @@ class LatticeMapLattice[D, L, LA <: Lattice[L]](l: LA) extends Lattice[LatticeMa
   override def glb(a: LatticeMap[D, L], b: LatticeMap[D, L]): LatticeMap[D, L] =
     latticeMapMeet(a, b, (x, y) => l.glb(x, y), l.top, l.bottom)
 
-  override def top: LatticeMap[D, L] = Top()
-  val bottom: LatticeMap[D, L] = Bottom()
+  override def top: LatticeMap[D, L] = LatticeMap.Top()
+  val bottom: LatticeMap[D, L] = LatticeMap.Bottom()
 }
 
+given [D, L](using l: Lattice[L]): Lattice[LatticeMap[D, L]] = LatticeMapLattice(l)
+
 /** A domain which has terms as maps. Implementing a MapDomain involves only defining operations element wise on the
   * codomain of the map (along with the transfer function).
   */
-trait MapDomain[D, L] extends AbstractDomain[LatticeMap[D, L]] {
+trait MapDomain[D, L](using Lattice[L]) extends AbstractDomain[LatticeMap[D, L]] {
   import LatticeMap.*
 
   def joinTerm(a: L, b: L, pos: Block): L
diff --git a/src/main/scala/analysis/NumericalDomains.scala b/src/main/scala/analysis/NumericalDomains.scala
index cd0b83fed..ecd93336a 100644
--- a/src/main/scala/analysis/NumericalDomains.scala
+++ b/src/main/scala/analysis/NumericalDomains.scala
@@ -20,7 +20,7 @@ def signedInt2bv(bitSize: Int, n: BigInt): BitVecLiteral =
   if n < 0 then smt_bvneg(BitVecLiteral((-n) % BigInt(2).pow(bitSize), bitSize))
   else BitVecLiteral(n % BigInt(2).pow(bitSize), bitSize)
 
-enum Interval extends InternalLattice[Interval] {
+enum Interval {
   case Top
   case ConcreteInterval(lower: BigInt, upper: BigInt, width: Int)
   case Bottom
@@ -32,8 +32,13 @@ enum Interval extends InternalLattice[Interval] {
     case _ => true
   })
 
-  def join(other: Interval): Interval =
-    (this, other) match {
+}
+
+object IntervalLattice extends Lattice[Interval] {
+  import Interval.*
+
+  def lub(x: Interval, other: Interval): Interval =
+    (x, other) match {
       case (Top, b) => Top
       case (Bottom, b) => b
       case (ConcreteInterval(l1, u1, w1), ConcreteInterval(l2, u2, w2)) if w1 == w2 =>
@@ -42,8 +47,9 @@ enum Interval extends InternalLattice[Interval] {
         throw Exception("Joining intervals of mismatching bitvector sizes")
       case (a, b) => b.join(a)
     }
-  def meet(other: Interval): Interval =
-    (this, other) match {
+
+  override def glb(x: Interval, other: Interval): Interval =
+    (x, other) match {
       case (Top, b) => b
       case (Bottom, b) => Bottom
       case (ConcreteInterval(l1, u1, w1), ConcreteInterval(l2, u2, w2)) if w1 == w2 => {
@@ -56,11 +62,11 @@ enum Interval extends InternalLattice[Interval] {
       case (a, b) => b.meet(a)
     }
 
-  def top: Interval = Top
-  def bottom: Interval = Bottom
+  override val top: Interval = Top
+  val bottom: Interval = Bottom
 }
 
-private implicit val intervalTerm: Interval = Interval.Bottom
+given Lattice[Interval] = IntervalLattice
 
 class IntervalDomain(
   procedure: Option[Procedure] = None,
@@ -257,8 +263,6 @@ class UnsignedIntervalDomain(procedure: Option[Procedure] = None)
 class DoubleIntervalDomain(procedure: Option[Procedure] = None)
     extends PredProductDomain(SignedIntervalDomain(procedure), UnsignedIntervalDomain(procedure))
 
-class IntervalLattice extends InternalLatticeLattice[Interval](Interval.Bottom)
-
 class TopDomain extends PredicateEncodingDomain[Unit] {
   def join(a: Unit, b: Unit, pos: Block): Unit = {}
   def transfer(a: Unit, b: Command): Unit = {}
diff --git a/src/main/scala/analysis/VariableDependencyAnalysis.scala b/src/main/scala/analysis/VariableDependencyAnalysis.scala
index 3f69b0f1f..e7e029975 100644
--- a/src/main/scala/analysis/VariableDependencyAnalysis.scala
+++ b/src/main/scala/analysis/VariableDependencyAnalysis.scala
@@ -36,8 +36,9 @@ trait ProcVariableDependencyAnalysisFunctions(
   varDepsSummaries: Map[Procedure, Map[Variable, LatticeSet[Variable]]],
   procedure: Procedure,
   parameterForm: Boolean
-) extends ForwardIDEAnalysis[Variable, LatticeSet[Variable], LatticeSetLattice[Variable]] {
-  val valuelattice = LatticeSetLattice()
+)(using latticeset: Lattice[LatticeSet[Variable]])
+    extends ForwardIDEAnalysis[Variable, LatticeSet[Variable], Lattice[LatticeSet[Variable]]] {
+  val valuelattice = latticeset
   val edgelattice = EdgeFunctionLattice(valuelattice)
   import edgelattice.{IdEdge, ConstEdge}
   import LatticeSet.*
@@ -257,7 +258,7 @@ class ProcVariableDependencyAnalysis(
   varDepsSummaries: Map[Procedure, Map[Variable, LatticeSet[Variable]]],
   procedure: Procedure,
   parameterForm: Boolean = false
-) extends ForwardIDESolver[Variable, LatticeSet[Variable], LatticeSetLattice[Variable]](program),
+) extends ForwardIDESolver[Variable, LatticeSet[Variable], Lattice[LatticeSet[Variable]]](program),
       ProcVariableDependencyAnalysisFunctions(relevantGlobals, varDepsSummaries, procedure, parameterForm) {
   override def start: CFGPosition = procedure
 }
diff --git a/src/main/scala/analysis/rely_guarantee_generation/CompatibleLattices.scala b/src/main/scala/analysis/rely_guarantee_generation/CompatibleLattices.scala
index c31721d37..f3fef9359 100644
--- a/src/main/scala/analysis/rely_guarantee_generation/CompatibleLattices.scala
+++ b/src/main/scala/analysis/rely_guarantee_generation/CompatibleLattices.scala
@@ -10,8 +10,6 @@ trait InterferenceCompatibleLattice[S] extends Lattice[S] {
   def contains(s: S, v: Variable): Boolean
   // weakens s by eliminating v
   def drop(v: Variable, s: S): S
-  // greatest lower bound, i.e. meet
-  def glb(s1: S, s2: S): S
   // display s as a boogie predicate
   def toPredString(s: S): String
 }
@@ -19,12 +17,11 @@ trait InterferenceCompatibleLattice[S] extends Lattice[S] {
 /** A compatible LatticeMapLattice representing the interval domain, where each
   * element of the lattice maps Variables to Intervals, and where these
   * Intervals are ordered by the IntervalLattice.
-  * 
+  *
   * @param l: A lattice over individual intervals, like [4, 7].
   */
-class IntervalLatticeExtension()
-    extends LatticeMapLattice[Variable, Interval, IntervalLattice](IntervalLattice())
-    with InterferenceCompatibleLattice[LatticeMap[Variable, Interval]] {
+class IntervalLatticeExtension()(using lattice: Lattice[LatticeMap[Variable, Interval]])
+    extends InterferenceCompatibleLattice[LatticeMap[Variable, Interval]] {
 
   def contains(s: LatticeMap[Variable, Interval], v: Variable): Boolean =
     s.toMap.contains(v)
@@ -32,10 +29,10 @@ class IntervalLatticeExtension()
   def drop(v: Variable, s: LatticeMap[Variable, Interval]): LatticeMap[Variable, Interval] =
     s + (v -> Interval.Top)
 
-  // glb is already defined in LatticeMapLattice
-
   /* this is very bodgy but we assume here that the transfer function that is
   coupled with this lattice is SignedIntervalDomain().transfer */
   def toPredString(s: LatticeMap[Variable, Interval]): String =
     SignedIntervalDomain().toPred(s).toString()
+
+  export lattice.*
 }
diff --git a/src/test/scala/GammaDomainTests.scala b/src/test/scala/GammaDomainTests.scala
index 6489c8b72..d667e012b 100644
--- a/src/test/scala/GammaDomainTests.scala
+++ b/src/test/scala/GammaDomainTests.scala
@@ -1,4 +1,5 @@
 import analysis.*
+import analysis.given
 import ir.*
 import ir.dsl.*
 import ir.transforms.{reversePostOrder, worklistSolver}
@@ -42,7 +43,7 @@ class GammaDomainTests extends AnyFunSuite, CaptureOutput {
     val gammaResults = getMustGammaDomainResults(f, initialState)
     val reachability = getReachabilityConditions(f)
 
-    assert(latticeMapApply(gammaResults(f.labelToBlock("returnBlock")), R0, LatticeSetLattice()) == LatticeSet.Bottom())
+    assert(latticeMapApply(gammaResults(f.labelToBlock("returnBlock")), R0) == LatticeSet.Bottom())
     assert(reachability(f.labelToBlock("returnBlock")) == Predicate.True)
   }
 
@@ -64,7 +65,7 @@ class GammaDomainTests extends AnyFunSuite, CaptureOutput {
     val reachability = getReachabilityConditions(f)
 
     assert(
-      latticeMapApply(gammaResults(f.labelToBlock("returnBlock")), R0, LatticeSetLattice()) == LatticeSet
+      latticeMapApply(gammaResults(f.labelToBlock("returnBlock")), R0) == LatticeSet
         .FiniteSet(Set(R0))
     )
     // TODO is this right?!
@@ -94,7 +95,7 @@ class GammaDomainTests extends AnyFunSuite, CaptureOutput {
     val gammaResults = getMustGammaDomainResults(f, initialState)
 
     assert(
-      latticeMapApply(gammaResults(f.labelToBlock("returnBlock")), R0, LatticeSetLattice()) == LatticeSet
+      latticeMapApply(gammaResults(f.labelToBlock("returnBlock")), R0) == LatticeSet
         .FiniteSet(Set(R2))
     )
     assert(
diff --git a/src/test/scala/LatticeCollectionTests.scala b/src/test/scala/LatticeCollectionTests.scala
index 87fb6b285..a562bc105 100644
--- a/src/test/scala/LatticeCollectionTests.scala
+++ b/src/test/scala/LatticeCollectionTests.scala
@@ -1,4 +1,4 @@
-import analysis.{LatticeMap, LatticeSet}
+import analysis.{LatticeMap, LatticeSet, given}
 import org.scalacheck.{Arbitrary, Gen, Shrink}
 import org.scalatest.*
 import org.scalatest.funsuite.*
@@ -10,13 +10,11 @@ class LatticeCollectionTests extends AnyFunSuite with org.scalatestplus.scalache
   type D = Int
   type L = LatticeSet[Int]
 
-  private implicit val latticeSetTerm: LatticeSet[V] = LatticeSet.Bottom()
-
   val genFinSet: Gen[Set[V]] = Gen.nonEmptyContainerOf[Set, V](Arbitrary.arbitrary)
 
   val genLatticeSet: Gen[LatticeSet[V]] = Gen.frequency(
-    (1, LatticeSet.Top()),
-    (1, LatticeSet.Bottom()),
+    (1, LatticeSet.Top[V]()),
+    (1, LatticeSet.Bottom[V]()),
     (20, for { s <- genFinSet } yield LatticeSet.FiniteSet(s)),
     (20, for { s <- genFinSet } yield LatticeSet.DiffSet(s))
   )
@@ -32,8 +30,8 @@ class LatticeCollectionTests extends AnyFunSuite with org.scalatestplus.scalache
   )
 
   val genLatticeMap: Gen[LatticeMap[D, L]] = Gen.frequency(
-    (1, LatticeMap.Top()),
-    (1, LatticeMap.Bottom()),
+    (1, LatticeMap.Top[D, L]()),
+    (1, LatticeMap.Bottom[D, L]()),
     (20, for { m <- (genNoTopFinMap) } yield LatticeMap.TopMap(m)),
     (20, for { m <- (genNoBotFinMap) } yield LatticeMap.BottomMap(m))
   )
@@ -48,7 +46,7 @@ class LatticeCollectionTests extends AnyFunSuite with org.scalatestplus.scalache
   }
 
   @annotation.nowarn
-  implicit def shrinkLatticeMap[D, L](implicit s: Shrink[L]): Shrink[LatticeMap[D, L]] = Shrink {
+  implicit def shrinkLatticeMap(implicit s: Shrink[L]): Shrink[LatticeMap[D, L]] = Shrink {
     case LatticeMap.Top() => Stream()
     case LatticeMap.Bottom() => Stream()
     case LatticeMap.TopMap(m) => (for (m2 <- Shrink.shrink(m)) yield LatticeMap.topMap(m2))