coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Missing a detail on type checking -- bad error reporting?
- Date: Mon, 27 Nov 2017 16:25:35 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f195.google.com
- Ironport-phdr: 9a23:f0wE7hUUdktOl4UAZ8c+pXgMq5vV8LGtZVwlr6E/grcLSJyIuqrYZRKEt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl9+If2wEYrPhey20fqz8tvdeVZmnj24NJB/MhSw5T7Mss0Xn4JkYvIq1x/No2VBfaJVyH1pI1C7kBP158P295lmpXcD88k9/tJNBP2pN58zSqZVWWwr
Dear all. First, thanks in advance for always being an incredibly helpful community.
I wonder what conditions precisely lead to an error at typechecking time of the form, "The term X has type T while it is expected to have type T." Here is a concrete example from the little code-base I'm working on.
The term
"{|
field_final := isFinal;
field_value := value;
field_rwt_ok := pf |}"
has type
"Field
mTipe_string
"io.compression.codecs"
io_compression_codecs_rwt"
while it is expected to have type
"Field
mTipe_string
"io_compression_codecs"
io_compression_codecs_rwt".
The type, the Field type constructor, here, is parameterized by several *values* including a string value. That, I expect, is where the problem is. What am I missing about dependent type checking? (Or is there another issue I'm missing?)
Here's a code isolate of just a few lines that exhibits the problem (in the last definition).
Should Coq produce a better error message here?
Thank you!
Kevin
===
Require Import String.
Require Export Coq.ZArith.BinInt.
(*
Machine types.
*)
Inductive MTipe := mTipe_Z | mTipe_string | mTipe_bool.
Definition mType (mt: MTipe): Type :=
match mt with
| mTipe_Z => Z
| mTipe_string => string
| mTipe_bool => bool
end.
Inductive Field (field_mtipe: MTipe) (field_name: string) (field_rwt: (mType field_mtipe) -> Prop) := mk_field {
field_final: bool
; field_value: (mType field_mtipe)
; field_rwt_ok: field_rwt field_value
}.
Definition io_compression_codecs_rwt: string -> Prop := fun s => True. (* Allow any string for now *)
Record hadoop_core_config := mk_hadoop_core_config {
field_io_compression_codecs: Field mTipe_string "io_compression_codecs" io_compression_codecs_rwt
}.
Definition mk_io_compression_codecs (isFinal: bool) (value: string) (pf: io_compression_codecs_rwt value):
Field mTipe_string "io_compression_codecs" io_compression_codecs_rwt :=
mk_field mTipe_string "io.compression.codecs" io_compression_codecs_rwt isFinal value pf.
- [Coq-Club] Missing a detail on type checking -- bad error reporting?, Kevin Sullivan, 11/27/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Matthieu Sozeau, 11/27/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Kevin Sullivan, 11/27/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Ralf Jung, 11/28/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Pierre Courtieu, 11/28/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Matthieu Sozeau, 11/27/2017
Archive powered by MHonArc 2.6.18.