A demo file for failure of definitional functoriality in Lean

coercions.lean

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

instance : Coe Pos Nat where
  coe := Pos.toNat

instance : Coe Nat Int where
  coe x := ↑x

instance [f : CoeTC X Y] : CoeTC (List X) (List Y) where
  coe l := List.map (f.coe) l

example (l : List Pos) : l  = ((l : List Nat) : List Int) := rfl