search

coq-community / coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
https://coq-community.org/coq-ext-lib/
BSD 2-Clause "Simplified" License
129 stars 46 forks source link

The EqvWF_Build instance messes up with typeclass resolution #100

Open YaZko opened 4 years ago

YaZko commented 4 years ago

The EqvWF_Build instance appears to lead astray typeclass resolution when performing unrelated rewrites. Consider the following code snippet relying on itrees:

From ITree Require Import
     ITree Eq.Eq.

Goal forall {E R1 R2} (RR : R1 -> R2 -> Prop) (t1 t1': itree E R1) (t2 : itree E R2),
    eutt eq t1 t1' ->
    eutt RR t1 t2 ->
    False.
  intros * EQ1 EQ2.
  rewrite EQ1 in EQ2. (* Instantaneous *)
  Undo.

  Require Import ExtLib.Programming.Eqv.
  Fail Timeout 5 rewrite EQ1 in EQ2. (* Appears to loop, had it run a few minutes without success *)

  Remove Hints EqvWF_Build : typeclass_instances.

  rewrite EQ1 in EQ2. (* Instantaneous again *)
Abort.