Compile-time solution to Jane Street's mock interview (https://www.youtube.com/watch?v=V8DGdPkBBxg)

conversion.lean

class Convertible {α : Type} (u : α) (v : α) where
  ratio : Float

-- Reflexivity
instance : Convertible u u where
  ratio := 1

-- Symmetry
instance [sym : Convertible u v]: Convertible v u where
  ratio := 1 / sym.ratio

-- Transitivity
instance [c₁ : Convertible u v] [c₂ : Convertible v w]: Convertible u w where
  ratio := c₁.ratio * c₂.ratio

-- Base facts
inductive unit where | m | ft | inch | hr | min | sec
instance : Convertible unit.m unit.ft where ratio := 3.28
instance : Convertible unit.ft unit.inch where ratio := 12
instance : Convertible unit.hr unit.min where ratio := 60
instance : Convertible unit.min unit.sec where ratio := 60

-- Solver
def convert (x : Float) (u v : unit) [c : Convertible u v]: Float := x * c.ratio

-- Interview's examples
#eval convert 2 unit.m unit.inch -- 78.72
#eval convert 13 unit.inch unit.m -- 0.330285
#eval convert 13 unit.inch unit.hr -- "failed to synthesize instance"