From e2c0cd1cb7fd06ef37f87f64e1164766820c16ea Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 15 Sep 2014 12:12:41 +0200 Subject: Avoid backtracking in typeclass search if a solution for a closed non-dependent or propositional constraint has already been found (same behavior as before previous patch). --- test-suite/typeclasses/backtrack.v | 43 +++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) (limited to 'test-suite/typeclasses') diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v index d3e21898d..112112f0c 100644 --- a/test-suite/typeclasses/backtrack.v +++ b/test-suite/typeclasses/backtrack.v @@ -38,4 +38,45 @@ Unset Typeclasses Unique Solutions. Definition foo' (b b' : B) := _ : B. Set Typeclasses Unique Solutions. -Definition foo'' (d d' : D) := _ : D. \ No newline at end of file +Definition foo'' (d d' : D) := _ : D. + +(** Cut backtracking *) +Module BacktrackGreenCut. + Unset Typeclasses Unique Solutions. + Class C (A : Type) := c : A. + + Class D (A : Type) : Type := { c_of_d :> C A }. + + Instance D1 : D unit. + Admitted. + + Instance D2 : D unit. + Admitted. + + (** Two instances of D unit, but when searching for [C unit], no + backtracking on the second instance should be needed except + in dependent cases. Check by adding an unresolvable constraint. + *) + + Variable f : D unit -> C bool -> True. + Fail Definition foo := f _ _. + + Fail Definition foo' := let y := _ : D unit in let x := _ : C bool in f _ x. + + Unset Typeclasses Strict Resolution. + Class Transitive (A : Type) := { trans : True }. + Class PreOrder (A : Type) := { preorder_trans :> Transitive A }. + Class PartialOrder (A : Type) := { partialorder_trans :> Transitive A }. + Class PartialOrder' (A : Type) := { partialorder_trans' :> Transitive A }. + + Instance: PreOrder nat. Admitted. + Instance: PartialOrder nat. Admitted. + + Class NoInst (A : Type) := {}. + + Variable foo : forall `{ T : Transitive nat } `{ NoInst (let x:=@trans _ T in nat) }, nat. + + Fail Definition bar := foo. + + +End BacktrackGreenCut. -- cgit v1.2.3