coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply and "Ill-typed evar instance"

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Apply and "Ill-typed evar instance"
Date: Thu, 6 Apr 2017 21:50:20 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:0ezhFxHJ3NuMh/tE2OIRup1GYnF86YWxBRYc798ds5kLTJ79rsSwAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOTA5/m/Jl8J+j6xbrx29qBNiwYHbbpqYNOZicq7HYd8WWXBMUthXWidcAo28dYwPD+8ZMOhXqYn9vVoOoge5BQKxGu3g0CRIhmT33aYn1OkuDwfG3BYhH90St3TYtsn1O70JUeCuzanF1jTDb/VM2Tf88ofEaB4hoeuVUL92bMHfylEvGhvBg1ifs4DpIT2Y2v4MvmWf9eZsSPyjhmw/pwxyoTWj3Nogh4vKi44Pzl3J+j91zJspKdGlTkNwfMSqH4FKty6AMot7WsMiTH9suCY90rAGt4C0fDQWyJQ6wR7fd+aIf5KP4hL5W+adOTZ4hHR7d7Kjnxu/9UetxvfiWsS6ylpHry5InsPRunwT1RHf8s2HReF8/kel1zaPzQfT6uRcLEA7j6XbMYAuwqUrm5odr0vDAjP2mFjwjK+KbEoo4O+o6/7oYrn+vJ+TK5d0ih3iMqQpgsGwHeM4MhEXU2eH/eS8yabs8FbiQLRKi/02irPWvIrbJcQdvK65AhVa3pwt6xalXH+a14ETmmBCJ1ZYcjqGiZLoMhfAOqPWF/C61nmqijZgwLj6N6b6A92ZI37ZkbzmO6p08FVd4As119FWoZxOXOJSaMnvU1P84YSLRiQyNBa5lr7q

On Thu, Apr 06, 2017 at 05:40:28PM +0200, Robbert Krebbers wrote:
> Hi all,
>
> could someone explain why the apply fails in the example below. Is there
> something inherently difficult going on with regard to higher-order
> unification, or may it just be a bug?
>
> -------
>
> Goal forall (P Q : Prop), exists A (R : A -> Prop),
> eq (exists x : A, R x) (exists b : bool, if b then P else Q).
> Proof. intros; eexists _, _. reflexivity. Qed.
>
> Goal forall (P Q : Prop), exists A (R : A -> Prop),
> eq (exists b : bool, if b then P else Q) (exists x : A, R x).
> Proof. intros; eexists _, _.
> (* Error: Ill-typed evar instance *)
> Fail apply eq_refl.
> Fail apply @eq_refl.
> Fail eapply @eq_refl.

It is definitely a bug. Please report it. Btw, "apply: erefl" works too.

Best
--
Enrico Tassi

[Coq-Club] Apply and "Ill-typed evar instance", Robbert Krebbers, 04/06/2017
- Re: [Coq-Club] Apply and "Ill-typed evar instance", Enrico Tassi, 04/06/2017