Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Inconsistent handling of implicit record type parameters

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inconsistent handling of implicit record type parameters


Chronological Thread 
  • From: Cedric Auger <sedrikov AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Inconsistent handling of implicit record type parameters
  • Date: Fri, 5 Dec 2014 16:18:07 +0100


2014-12-05 15:53 GMT+01:00 <michael.soegtrop AT intel.com>:
Dear Coq users,

I have a problem with implicit record type arguments defined via {} binders.
Print and Print Implicit show different status on wether such parameters are
implicit or not, and it doesn't work as expected. Please have a look at the
Coq code below. Is therer an explanation for this behaviour, or is this a bug?


For me, in your example Print and Print Implicit seem to be consistent.
Both tell that mkRecTest has no implicit arguments (although RecTest itself has implicit arguments).
Until you decide to put the first argument of mkRecTest (par) implicit, and then both report it as implicit.

To sum up, when you write:

Record RecTest {par : nat} : Type := mkRecTest
{
  elem1 : nat
}.

You tell coq to consider "par" as implicit for RecTest, but you do not tell what to do with the "par" argument of mkRecTest. Coq uses an heuristic which tells that it is probably a bad idea to set this argument as implicit, as it cannot easily infer it. For instance, "mkRecTest 8 : RecTest" does not provide much information on the "par" parameter.

Best regards,

Michael


Record RecTest {par : nat} : Type := mkRecTest
{
  elem1 : nat
}.

Print mkRecTest.

(*
Record RecTest (par : nat) : Type := mkRecTest { elem1 : nat }

For RecTest: Argument par is implicit and maximally inserted
For RecTest: Argument scope is [nat_scope]
For mkRecTest: Argument scopes are [nat_scope nat_scope]

=> This is what I expected
*)

Print Implicit mkRecTest.

(*
mkRecTest : forall par : nat, nat -> RecTest

=> Here par is not mentioned as implicit
=> Also I have to give the argument explicitly
*)

Definition test : @RecTest 1 := mkRecTest _ 1.

(* Define par more explicitly as implicit *)

Arguments mkRecTest [par] _.

Print mkRecTest.

(*
Record RecTest (par : nat) : Type := mkRecTest { elem1 : nat }

For RecTest: Argument par is implicit and maximally inserted
For mkRecTest: Argument par is implicit
For RecTest: Argument scope is [nat_scope]
For mkRecTest: Argument scopes are [nat_scope nat_scope]
*)

Print Implicit mkRecTest.

(*
mkRecTest : forall par : nat, nat -> RecTest

Argument par is implicit
*)

Definition test2 : @RecTest 1 := mkRecTest 1.

(* => Now everything works fine *)



--
.../Sedrikov\...



Archive powered by MHonArc 2.6.18.

Top of Page