better test

Author: gares

tests/infer.v

@@ -8,20 +8,21 @@ HB.structure Definition foo := { T of foom T }.
 
 HB.instance Definition i := foom.Build nat plus.
 
-HB.mixin Record barm (P : foo.type) (T : indexed Type) := {
-  law : P -> T
+HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : indexed Type) := {
+  law : P -> T -> A -> B
 }.
 
 #[infer(P)]
-HB.structure Definition bar P := { T of barm P T }.
+HB.structure Definition bar A P B := { T of barm A P B T }.
 
-Fail Check bar.type_ nat.
+Fail Check bar.type_ bool nat bool.
 Print bar.phant_type.
 Print bar.type.
-Check bar.type nat.
+Check bar.type bool nat bool.
 
 Fail #[infer(P = "whatever")]
-HB.structure Definition bar1 P := { T of barm P T & foom T }.
+HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }.
 
 #[infer(P = "Type")]
-HB.structure Definition bar1 P := { T of barm P T & foom T }.
+HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }.
+Check bar1.type nat.