The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Oh good grief. Well, there you have it.

On Mon, Nov 27, 2017 at 4:28 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi Kevin, "io.compression.codecs" <> "io_compression_codecs", as far as I can see.

On Mon, Nov 27, 2017 at 10:26 PM Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

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.