coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Apply and "Ill-typed evar instance"
Date: Thu, 6 Apr 2017 17:40:28 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:XRyYkhNrD5BNJVN70h0l6mtUPXoX/o7sNwtQ0KIMzox0LfX+rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkZNzA37WLZhMJ+g61UvB2vqAdyw5LWbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUTCOoOJv1XoJfnp1sSsBCwABOsC/30xTBTmHD2x7Y62PkmHAHDxgMgHtYOsHXSrNX6MKcSUPu1zLXTzTjYdfNW3izy55PWfRA7vfGMXqhwftTKxkY0CQzFlE6QpZbjPzORz+kAtXWQ4el4Ve+3lmIqpRx9riKyysouhYTFnJ8Zx1He+Slkz4s4K8W0RUp0bNK+DpdcqyWXO5F0T84mWW1kpjs2x7kAtJWmZiYF0o4nyATaa/Gfc4iH/BbjVOGJLDdjgXJlZKq/iwuo/Ui71uL8V9e70FBWoSVbiNXMrG0N2wbV6siDUvd9/0Gh1iiT1w3L9+1JL104mbDGJ5MjzbM8jIcfvEXZEiPrl0j7greadkA+9eip7+TnbK/mppiZN4JsjwHxKKUumsi+AeQ+PQgOW2mb+f+g1L345kD5WrJKgeYtnabHqpDaOccbprSnDABOyYks9Qy/Dyy83NQemXkLNEhFdw6fj4j1J1HOJ+j1Auu4g1S1iTtk2/TGPqD6DZjWNXjCkLLhfa5n5EJGyQozy8pf55NOBb0bLvLzQBy5iNuNBRggdgew3uyvXN56z8YVXX+FKq6fKqLb91GSsLEBOe6JMbUSsjzwMeRtxOTjh3U0g0RVKayg3J8Wbn+8H+96OG2DZnDmj80dEn0HtAAzVvesjlnUAm0bXGq7Q69pvmJzM4mhF4qWHo0=

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.

(* works *)
refine (eq_refl _).
Qed.

------

Best,

Robbert

[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