coqtokyo_EqClass_sort2.v

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* :> を複数持つと予期せぬことがおきることがあるぞ *)
Structure S : Type := MakeS {
  sort2 :> Type;
  sort :> Type;

  op : sort -> sort -> bool;
}.

Inductive mybool := Yes | No.

Definition natS : S := @MakeS nat nat eqn.
Definition boolS : S := @MakeS mybool bool eqb.


Let f := fun (s : S) (x : s) => x.
Compute @f natS 3.
Compute @f boolS true. (* ←ここでエラー(8,9行目の順番を入れ替えるとエラーにならない) *)