升级到Angular 6后构建失败(Build failing after upgrading to Angular 6)

 你是对的：Coq中的类型类只是具有特殊管道和推理的记录（还有单方法类型类的特殊情况，但它不会以任何方式影响这个答案）。 因此，您选择类型类而不是“纯”依赖记录的唯一原因是受益于您使用它们得到的特殊推理：使用普通依赖记录进行推理并不是非常强大，并且不允许您省略很多信息。 
 
 作为示例，请考虑以下代码，该代码定义了一个monoid类型类，使用自然数进行实例化： 
 
Class monoid A := Monoid {
  op : A -> A -> A;
  id : A;
  opA : forall x y z, op x (op y z) = op (op x y) z;
  idL : forall x, op id x = x;
  idR : forall x, op x id = x
}.

Require Import Arith.

Instance nat_plus_monoid : monoid nat := {|
  op := plus;
  id := 0;
  opA := plus_assoc;
  idL := plus_O_n;
  idR := fun n => eq_sym (plus_n_O n)
|}.
 
 使用类型类推断，我们可以使用任何直接用于nat任何monoid的定义，而不提供类型类参数，例如 
 
Definition times_3 (n : nat) := op n (op n n).
 
 但是，如果通过“ Record和Definition替换“ Class和Instance将上述定义转换为常规记录，则相同的定义将失败： 
 
Toplevel input, characters 38-39: Error: In environment n : nat The term "n" has type "nat" while it is expected to have type  "monoid ?11".
 
 对类型类的唯一警告是实例推理引擎有时会有点丢失，导致出现难以理解的错误消息。 话虽这么说，但鉴于这种可能性甚至在那里都没有，它并不是真正的依赖记录。 

You are right: type classes in Coq are just records with special plumbing and inference (there's also the special case of single-method type classes, but it doesn't really affect this answer in any way). Therefore, the only reason you would choose type classes over "pure" dependent records is to benefit from the special inference that you get with them: inference with plain dependent records is not very powerful and doesn't allow you to omit much information.
 
As an example, consider the following code, which defines a monoid type class, instantiating it with natural numbers:
 
Class monoid A := Monoid {
  op : A -> A -> A;
  id : A;
  opA : forall x y z, op x (op y z) = op (op x y) z;
  idL : forall x, op id x = x;
  idR : forall x, op x id = x
}.

Require Import Arith.

Instance nat_plus_monoid : monoid nat := {|
  op := plus;
  id := 0;
  opA := plus_assoc;
  idL := plus_O_n;
  idR := fun n => eq_sym (plus_n_O n)
|}.
 
Using type class inference, we can use any definitions that work for any monoid directly with nat, without supplying the type class argument, e.g.
 
Definition times_3 (n : nat) := op n (op n n).
 
However, if you make the above definition into a regular record by replacing Class and Instance by Record and Definition, the same definition fails:
 
Toplevel input, characters 38-39: Error: In environment n : nat The term "n" has type "nat" while it is expected to have type  "monoid ?11".
 
The only caveat with type classes is that the instance inference engine gets a bit lost sometimes, causing hard-to-understand error messages to appear. That being said, it's not really a disadvantage over dependent records, given that this possibility isn't even available there.