coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Easy question re: implicit parameters

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Guillaume Melquiond <guillaume.melquiond AT inria.fr>
Subject: Re: [Coq-Club] Easy question re: implicit parameters
Date: Sat, 16 Sep 2017 10:29:00 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:kpn7uRVlvrrw4FkvMS0gzXfXlznV8LGtZVwlr6E/grcLSJyIuqrYZhaEt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aMlzFOAF0PuX4HJLJx4Tyjrjqus6bXwIdjz2kJLh2MR+erAPLt8BQj5EmYoksyx/Nq2ZNdqxzyGdxOFOUmRq0ssit/Zpn+jlVtrQk+spZTKT9eagQTLpCDT1gPXpjt+PxshyWdwKL6DM+T2MZ2k5KHg7KxBTiX9LqrTC8sfByjnrJdfbqRKw5DGzxp5xgTwXl3WJeb2Y0

Hi,

>> An idea could be to also provide the [A : Type] syntax in binders for
>> non-maximal implicits, similar to what Arguments accepts.
>
> Is there a use for non-maximal implicit arguments outside of legacy
> code? If not, adding a new binder syntax is not worth it.

The problem with maximally inserted arguments is that just writing
"identifier" will already try to infer some arguments:

identifier : forall {T: Type} {_ : SomeTypeClass T}, ...

This does a completely unconstrained type class search, which is not
going to succeed. When doing Iris proofs with our custom tactic
language, we regularly have to write "@identifier" as otherwise applying
the tactic diverges.

Kind regards,
Ralf

RE: [Coq-Club] Easy question re: implicit parameters, (continued)