Module 4 · Lesson 2

Implementing Instances

Instances connect types to type classes. Learn to write them for your own types and understand how Lean resolves them.

Basic Instance Syntax

Declare an instance with instance:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Anonymous instance (most common)
6instance : ToString Point where
7  toString p := s!"({p.x}, {p.y})"
8
9-- Named instance (useful for debugging)
10instance instBEqPoint : BEq Point where
11  beq p1 p2 := p1.x == p2.x && p1.y == p2.y
12
13#eval toString (Point.mk 3.0 4.0)  -- "(3.000000, 4.000000)"
14#eval Point.mk 1.0 2.0 == Point.mk 1.0 2.0  -- true

Implementing Common Type Classes

BEq: Equality

The BEq type class provides the == operator. You implement the beq method which takes two values and returnstrue if they should be considered equal.

lean

1inductive Color where
2  | red | green | blue
3
4instance : BEq Color where
5  beq c1 c2 := match c1, c2 with
6    | .red, .red => true
7    | .green, .green => true
8    | .blue, .blue => true
9    | _, _ => false
10
11#eval Color.red == Color.red    -- true
12#eval Color.red == Color.blue   -- false

Ord: Ordering

The Ord type class enables the comparison operators<, >, <=, and >=. You implement compare which returns .lt, .eq, or .gt.

lean

1instance : Ord Color where
2  compare c1 c2 := match c1, c2 with
3    | .red, .red => .eq
4    | .red, _ => .lt
5    | .green, .red => .gt
6    | .green, .green => .eq
7    | .green, .blue => .lt
8    | .blue, .blue => .eq
9    | .blue, _ => .gt
10
11#eval compare Color.red Color.blue  -- Ordering.lt
12
13-- NOTE: Ord alone does NOT give you <, >, <=, >=. Those come from the
14-- separate LT and LE classes. This fails:
15--   #eval Color.green < Color.blue
16--   error: failed to synthesize LT Color
17--
18-- Derive them from your Ord instance if you want the operators:
19instance : LT Color := ltOfOrd
20instance : LE Color := leOfOrd
21
22#eval Color.green < Color.blue      -- true

Hashable

The Hashable type class enables using your type as keys inHashMap and elements in HashSet. You must ensure that equal values produce equal hashes.

lean

1instance : Hashable Color where
2  hash c := match c with
3    | .red => 0
4    | .green => 1
5    | .blue => 2

Repr: Debug Representation

The Repr type class controls how values appear in #evaloutput and debugging. Unlike ToString, Repr typically shows the constructor form so you can copy-paste the output back as valid code.

lean

1instance : Repr Point where
2  reprPrec p _ := s!"Point.mk {p.x} {p.y}"
3
4#eval (Point.mk 1.0 2.0 : Point)  -- Point.mk 1.000000 2.000000

Instances for Parameterized Types

When your type has parameters, instances can require constraints on those parameters:

lean

1structure Pair (α β : Type) where
2  fst : α
3  snd : β
4
5-- Require both types to have BEq
6instance [BEq α] [BEq β] : BEq (Pair α β) where
7  beq p1 p2 := p1.fst == p2.fst && p1.snd == p2.snd
8
9-- Now this works for any Pair of equatable types
10#eval Pair.mk 1 "a" == Pair.mk 1 "a"   -- true
11#eval Pair.mk 1 "a" == Pair.mk 2 "a"   -- false

Key Takeaway

Instance constraints propagate: if Pair needs BEqfor its elements, then Pair Nat String works becauseNat and String have BEq instances.

Recursive Instances

lean

1-- Instance for List requires instance for elements
2instance [BEq α] : BEq (List α) where
3  beq xs ys := match xs, ys with
4    | [], [] => true
5    | x :: xs, y :: ys => x == y && beq xs ys
6    | _, _ => false
7
8#eval [1, 2, 3] == [1, 2, 3]   -- true
9#eval [1, 2] == [1, 2, 3]     -- false

Using deriving

For simple types, deriving generates instances automatically:

lean

1-- Derive multiple instances at once
2structure Person where
3  name : String
4  age : Nat
5  deriving Repr, BEq, Hashable
6
7-- Works immediately
8#eval Person.mk "Alice" 30 == Person.mk "Alice" 30  -- true
9#eval repr (Person.mk "Bob" 25)  -- Person.mk "Bob" 25
10
11-- For inductive types too
12inductive Status where
13  | pending
14  | active
15  | completed
16  deriving Repr, BEq, Hashable, Ord

💡

Use derivingwhen possible—it's less error-prone than manual instances. Write manual instances for custom behavior.

Default Method Implementations

Type classes can provide default implementations:

lean

1class Printable (α : Type) where
2  format : α → String
3  -- Default implementation using format
4  print : α → IO Unit := fun x => IO.println (format x)
5
6-- Only need to implement format
7instance : Printable Nat where
8  format n := s!"Number: {n}"
9
10-- print comes for free
11#eval (Printable.print 42 : IO Unit)  -- prints "Number: 42"

Instance Priority

When multiple instances could apply, priority determines which wins:

lean

1-- HIGHER number = higher priority = tried FIRST.
2-- The named levels are: low (100) < default (1000) < high (10000).
3class Tag (α : Type) where
4  name : α → String
5
6instance (priority := 100) : Tag Nat where name _ := "low-100"
7instance (priority := 900) : Tag Nat where name _ := "high-900"
8
9#eval Tag.name 1     -- "high-900"
10
11-- The named forms read better than raw numbers:
12instance (priority := high) : ToString Bool where
13  toString b := if b then "yes" else "no"
14
15#eval toString true  -- "yes"

Debugging Instance Search

"Failed to synthesize" is the most common wall you will hit. These four commands turn it from a guessing game into a diagnosis:

lean

1-- 1. Ask for the instance directly. The error is the same, but isolated
2--    from whatever else was going on in your expression.
3#check (inferInstance : BEq Nat)          -- ok
4-- #check (inferInstance : BEq (Nat → Nat))  -- fails, and says why
5
6-- 2. Watch the search. Verbose, but it shows every candidate tried
7--    and exactly which sub-goal failed.
8set_option trace.Meta.synthInstance true in
9#check (inferInstance : BEq (List Nat))
10
11-- 3. The trace above ends with a line like "result List.instBEq" —
12--    that is the instance's real name. Print it to see how it is built.
13#print List.instBEq
14
15-- 4. Make hidden instances visible in the goal display.
16set_option pp.explicit true in
17#check (1 == 1)

The three causes, in the order they actually occur:

A missing link in the chain. You asked for ToString (List MyType) but never wrote ToString MyType. The error names the innerfailure — read it, do not skim it.
A metavariable. If the error mentions ?m or says the type argument is a metavariable, the type is not determined yet and Lean refuses to guess. Add a type ascription, e.g. (xs : List Nat).
A missing import. Instances arrive with their module. If Std.HashMap is not imported, its instances do not exist, no matter how correct your code looks.

Deep Dive: Instance Search

When Lean sees x == y, it:

Determines the type of x
Searches for a BEq instance for that type
If the type has parameters, recursively finds instances for them
Uses the found instance to call BEq.beq

This happens at compile time, so there's no runtime overhead.

Orphan Instances

An "orphan instance" is an instance for a type you don't own, in a module that doesn't define the type or the class. Use with caution:

lean

1-- In your module: instance for external type
2-- This is an "orphan" - can cause conflicts
3
4instance : ToString (List Nat) where
5  toString xs := s!"[{String.intercalate ", " (xs.map toString)}]"
6
7-- Better: wrap in your own type
8structure MyList (α : Type) where
9  items : List α
10
11instance [ToString α] : ToString (MyList α) where
12  toString xs := s!"MyList: {xs.items}"

⚠

Orphan instances can conflict if another library defines the same instance. Prefer wrapping types or defining instances where the type is defined.

Exercise: BEq for a Structure

Define a BEq instance for a simple structure.

lean

1structure User where
2  id : Nat
3  name : String
4
5instance : BEq User where
6  beq a b := a.id == b.id && a.name == b.name
7
8#eval ({ id := 1, name := "A" } : User) == { id := 1, name := "A" }

The Concept Next: Custom Type Classes