diff options
Diffstat (limited to 'test-suite/bugs/closed/3998.v')
-rw-r--r-- | test-suite/bugs/closed/3998.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v new file mode 100644 index 00000000..ced13839 --- /dev/null +++ b/test-suite/bugs/closed/3998.v @@ -0,0 +1,24 @@ +Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }. +Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *) + +Inductive I1 := C. +Inductive I2 := . + +Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }. +Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }. + +Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f. + +Class MapOps (M K : Set) := { + tgtTy: K -> Set; + update: M -> forall k:K, tgtTy k -> M +}. + +Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F := +{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }. + +Axiom ex : RecordOf _ I1FieldType. + +Definition works := (fun ex' => update ex' C true) (update ex C false). +Set Typeclasses Debug. +Definition doesnt := update (update ex C false) C true.
\ No newline at end of file |