From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3325.v | 48 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 test-suite/bugs/closed/3325.v (limited to 'test-suite/bugs/closed/3325.v') diff --git a/test-suite/bugs/closed/3325.v b/test-suite/bugs/closed/3325.v new file mode 100644 index 00000000..36c065eb --- /dev/null +++ b/test-suite/bugs/closed/3325.v @@ -0,0 +1,48 @@ +Typeclasses eauto := debug. +Set Printing All. + +Axiom SProp : Set. +Axiom sp : SProp. + +(* If we hardcode valueType := nat, it goes through *) +Class StateIs := { + valueType : Type; + stateIs : valueType -> SProp +}. + +Instance NatStateIs : StateIs := { + valueType := nat; + stateIs := fun _ => sp +}. +Canonical Structure NatStateIs. + +Class LogicOps F := { land: F -> F }. +Instance : LogicOps SProp. Admitted. +Instance : LogicOps Prop. Admitted. + +Parameter (n : nat). +(* If this is a [Definition], the resolution goes through fine. *) +Notation vn := (@stateIs _ n). +Definition vn' := (@stateIs _ n). +Definition GOOD : SProp := + @land _ _ vn'. +(* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *) +Definition BAD : SProp := + @land _ _ vn. + + +Class A T := { foo : T -> Prop }. +Instance: A nat. Admitted. +Instance: A Set. Admitted. + +Class B := { U : Type ; b : U }. +Instance bi: B := {| U := nat ; b := 0 |}. +Canonical Structure bi. + +Notation b0N := (@b _ : nat). +Notation b0Ni := (@b bi : nat). +Definition b0D := (@b _ : nat). +Definition GOOD1 := (@foo _ _ b0D). +Definition GOOD2 := (let x := b0N in @foo _ _ x). +Definition GOOD3 := (@foo _ _ b0Ni). +Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *) -- cgit v1.2.3