The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Cedric,

 

yes, you are right. I didn’t read the output of Print properly. What added to my confusion is that the parameter for the member projection function elem1 is implicit. But your explanation on why this is, is logical and it is no issue to define that as needed.

 

Thanks & best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Cedric Auger
Sent: Friday, December 05, 2014 4:18 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Inconsistent handling of implicit record type parameters

 

 

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\...