coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] non-automatic type class resolution

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] non-automatic type class resolution
Date: Fri, 2 Sep 2016 11:24:04 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f173.google.com
Ironport-phdr: 9a23:boziTxacp/2pAf57SZK3+T7/LSx+4OfEezUN459isYplN5qZpsSybnLW6fgltlLVR4KTs6sC0LuP9f27EjNQqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2aue3siLv3o8GbI1gQxWn1XbQnJxKv6A7Vq8M+gI14K693xAGajGFPfrF0wmVhOVKamV7Y68au8Zh/u3BSvPQg9MNEXKjScKExTLgeBzMjZTNmrPb3vAXOGFPcrkAXVX8bx0cQDg==

I added this to https://coq.inria.fr/bugs/show_bug.cgi?id=3601

-- Jonathan

On 09/01/2016 10:07 PM, Jonathan Leivent wrote:

On 09/01/2016 09:57 PM, Vadim Zaliva wrote:

...
In more complex cases, where one have several type class instance evars,
dependent on each other I suspect using this approach could become unwieldy.

I agree. Cases like this have been discussed before both on Coq-club and coqdev. It would be nice to have a way to selectively turn off typeclass resolution on a hole-by-hole basis with some convenient syntax.

-- Jonathan

[Coq-Club] non-automatic type class resolution, Vadim Zaliva, 09/02/2016
- Re: [Coq-Club] non-automatic type class resolution, Jonathan Leivent, 09/02/2016
  - Re: [Coq-Club] non-automatic type class resolution, Jonathan Leivent, 09/02/2016
  - Re: [Coq-Club] non-automatic type class resolution, Vadim Zaliva, 09/02/2016
    - Re: [Coq-Club] non-automatic type class resolution, Jonathan Leivent, 09/02/2016
      - Re: [Coq-Club] non-automatic type class resolution, Jonathan Leivent, 09/02/2016