Построение иерархии классов в Coq?

Я могу наивно построить иерархию алгебраических структур в Coq, используя классы типов. У меня проблемы с поиском ресурсов по синтаксису и семантике Coq для классов типов. Однако я считаю, что следующее является правильной реализацией полугрупп, моноидов и коммутативных моноидов:

Class Semigroup {A : Type} (op : A -> A -> A) : Type := {
  op_associative : forall x y z : A, op x (op y z) = op (op x y) z
}.

Class Monoid `(M : Semigroup) (id : A) : Type := {
  id_ident_left  : forall x : A, op id x = x;
  id_ident_right : forall x : A, op x id = x
}.  

Class AbelianMonoid `(M : Monoid) : Type := {
  op_commutative : forall x y : A, op x y = op y x
}.

Если я правильно понимаю, можно добавить дополнительные параметры (например, элемент идентичности моноида), сначала объявив Моноид ] экземпляр Semigroup , затем параметризация на id: A . Однако кое-что странное происходит в записи, построенной для AbelianMonoid .

< Print Monoid.
    Record Monoid (A : Type) (op : A -> A -> A) (M : Semigroup op) 
    (id : A) : Type := Build_Monoid
    { id_ident_left : forall x : A, op id x = x;
      id_ident_right : forall x : A, op x id = x }

< Print AbelianMonoid.
    Record AbelianMonoid (A : Type) (op : A -> A -> A) 
    (M0 : Semigroup op) (id0 : A) (M : Monoid M0 id0) : 
    Type := Build_AbelianMonoid
      { op_commutative : forall x y : A, op x y = op y x }

Это произошло, когда я пытался построить класс для полугрупп.Я думал, что следующий синтаксис был правильным:

Class Semiring `(P : AbelianMonoid) `(M : Monoid) := {
    ...
}.

Однако я не мог однозначно определить правильные операторы и элементы идентичности. Печать записей выявила проблемы, описанные выше. Итак, у меня есть два вопроса: во-первых, как правильно объявить класс Monoid ; во-вторых, как устранить неоднозначность функций в суперклассах?

Что мне действительно нужно, так это хорошие ресурсы, которые четко объясняют классы типов Coq без устаревшего синтаксиса. Например, я думал, что книга Хаттона ясно объясняет классы типов в Haskell.