coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq 8.6 typeclasses behavior change
- Date: Wed, 16 Nov 2016 14:33:20 +0100
- Authentication-results: mail3-smtp-sop.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:/1xkgRH7dmLV6UUlwpFGGp1GYnF86YWxBRYc798ds5kLTJ78p8uwAkXT6L1XgUPTWs2DsrQf2rGQ6vyrBTNIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZb1/IA+roQjeucUbjolvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFogqxVoAyvqQF8zY7ab46aKOdxcaHTct4BWWpNQtxcWzBdDo6mcYcCCfcKM+ZCr4n6olsDtRSwBQ+2BOPu1jBIgWL907Mg3OQ6CgHG3RErEtUQv3TSttX1NbsdUeevwKnU1zrDdOhW2Tbm5YjJdBAhu/CMUqhqfcrf00kiDgXIhUiTp4z9Jz6Y0usAv3KF4+duT+6iimoqpxtsrjSxxMogkpTFi4wWx1ze8Sh0wZw5KcOkREJne9KpEJpduieHPIVsWMwiWXtnuCMix70Gp5G7eC8KxYwpxxHBd/yHb5WI4hT/VOmLOzt4g2hleL2nixaz90iv1PH8W9Gw3VtFtCZJjNfBumoM2hHX8MSLV+Vx80W51TaKzQ/T6+VEIU4ularcLp4s2rEwmYAJsUvdBS/7g0v2g7GKdkU45+io7fjnba/8qp+bLY90hRnyMr4ylcynHeQ4Lg8OUnCH9uS7zb3v5FH2QLFXjvItiaTZq5DbJcEDpqGjGQNV04Aj6wy+Dzi8ytgYk2MHfxp5f0eMiJGsMFXTKtj5C+2+ihKiimRF3ffDa5DnGJTGKTD/maz6fP4p5khGyQE0i8xW/IlVIrAHOvP6HEHr4o+LRiQlOhC5lr60QO520ZkTDDqC
On Wed, Nov 16, 2016 at 01:23:04PM +0000, Matthieu Sozeau wrote:
> This is a deliberate change to avoid "wrong" instances which generate
> non-class goals from polluting search.
> You just need to declare the head as a class using Existing Class eq for
> example here, because you're really
> treating it as a class. Sorry for not updating the CHANGES yet, the refman
> has been updated though.
What you propose seems a bit too drastic, Existing Class marks
Eq as class "forever". A lighter work around could be the following
Class Foo (x : nat).
Class TCPremise (P : Prop).
Instance foo x : TCPremise (x = 2) -> Foo x.
Hint Extern 0 (TCPremise (_ = _)) => reflexivity : typeclass_instances.
But frankly the use case of Ralf seems reasonable, and the contortion
above pretty ugly.
Can you explain what you mean by "wrong" instances, exactly?
Best,
--
Enrico Tassi
- [Coq-Club] Coq 8.6 typeclasses behavior change, Ralf Jung, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Enrico Tassi, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Jonathan Leivent, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Robbert Krebbers, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Enrico Tassi, 11/16/2016
- Re: [Coq-Club] Coq 8.6 typeclasses behavior change, Matthieu Sozeau, 11/16/2016
Archive powered by MHonArc 2.6.18.