型クラス・インスタンスが生成できなというエラー

最後の行がエラー。

/-- 記法クラス -/
class LE (X : Type) where
  le : X → X → Prop

scoped infix:50 "≦" => LE.le
#check LE

section LE_Test
  variable -- セミローカルコンテキストの導入
  (A: Type) [LE A] (a b:A)
  #check a≦b
end LE_Test

/-- 全順序集合の指標 
記法クラスを extends している。
LE.le の継承共に、≦ が使用可能となる。
-/
class TotalOrder ( X : Type ) extends LE X where
  refl : ∀x:X,   x ≦ x
  trans : ∀(x y z : X), x ≦ y ∧  y ≦ z →  z ≦ z
  anti_symm : ∀(x y : X),  x≦ y ∧ y≦ x → x = y
  total : ∀(x y : X), x≦ y ∨ y≦ x

#check TotalOrder

section TO_Test
  variable (X: Type) 
  variable [TotalOrder X] 
  variable  (x y z: X)
  #check x ≦ x
  #check y ≦x 
end TO_Test

theorem TO_lefl (X: Type) [TotalOrder X] (x : X) : x≦x  := 
  TotalOrder.refl x
#check TO_lefl

/-- 記法クラス -/
class PlusZero (X : Type) where
  plus : X → X →  X
  zero : X

scoped infixl:65 "+" => PlusZero.plus
-- scoped notation "Z" => PlusZero.zero

/-- 指標クラス： 可換モノイド 
PlusZero.plus, PlusZero.zero を継承している。
-/
class CommMonoid (X : Type) extends PlusZero X where
  assoc : ∀(x y z :X ), (x + y) + z = x + (y + z)
  lunit : ∀(x :X ), zero + x = x
  runit : ∀(x :X ), x + zero = x
  comm : ∀(x y : X), x + y = y + x

/-- 距離値の空間
-/
class Distance (X : Type) extends TotalOrder X, CommMonoid X where
  positive : ∀(x : X), zero≦ x
  plus_ord_presv : ∀(x y a : X), x≦ y →  (x + a) ≦ (y + a)

variable (D : Type) [Distance D] -- OK

/-- 距離空間 -/
class MetricSp (X  : Type) where
 dist : X → X → D
 dist_zero : ∀(x y :X), dist x y = zero ↔ x = y
 dist_symm : ∀(x y :X), dist x y = dist y x
 traiangle : ∀(x y z : X), (dist x z) ≦ (dist x y) + (dist y z) 
#print MetricSp

variable (X: Type) [MetricSp X] -- failed to synthesize instance