coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] eauto loops
Date: Mon, 27 Jun 2016 08:40:45 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
Ironport-phdr: 9a23:J4pa/xfc3gSaKMeCgCcaWav5lGMj4u6mDksu8pMizoh2WeGdxc64YR7h7PlgxGXEQZ/co6odzbGH6+a5ACdQvd6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JXvkbnrsM2PKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDWG6noZGlcflhtWCkCR8gPzWpbvuwPxs/c71SWHa56lBYsoUCivuv84ACTjjz0KYmY0

I am facing a situation where eauto loops in type class resolution. Log fragment:

Debug: (* debug eauto : *)

Debug: 1 depth=5

Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)

...

What could be causing this and how to debug? It is a bit weird, as it loops

on applying single assumption indefinitely.

Vadim

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] eauto loops, Vadim Zaliva, 06/27/2016
- Re: [Coq-Club] eauto loops, Matthieu Sozeau, 06/27/2016
  - Re: [Coq-Club] eauto loops, Vadim Zaliva, 06/28/2016
    - Re: [Coq-Club] eauto loops, Matthieu Sozeau, 06/28/2016
      - Re: [Coq-Club] eauto loops, Vadim Zaliva, 06/28/2016