Module error Type differ in Coq

Question

I have a hard time to figure out how to write this code.

For example, I have a signature A, a functor C takes a: A as a parameter, to be able to use C, I define a module B implements signature A

Require Import String.
Module Type A.
  Parameter toto : string -> nat. 
End A.

Module C (Import a : A).
 ...
End C.

Module B <: A.
      Definition toto (s: string) := foo s.
End B. (* COQ error *)

and support I have type foo: string -> string list-> nat.

Then at the End B., I have an error from Coq saying that: signature components for label toto do not match: types differ.

Or another way:

Module B.
 Definition too (s : string) := foo s.
End B.

Module Export D := C B.

I will get the same error at D

I understand the problem because I did not provide the string list argument in the definition of toto.

So my problem is I do not know how can I provide the argument string list in this case.

In my real code I was using Section and Record type instead of Module.

Record A : Type := mkA { too : string -> nat}.

Then I open a Section

Section B.
 Variable l: string list.
 Definition too (s: string) := foo s l.
 Definition A := mkA too.
End B.

Could you please help me to write or to understand how can I write the functor B in module correctly? Is there a way that I can define/declare a variable string list in module? Also after define in Coq I will extract it to OCaml.

Ptival Ptival · Accepted Answer · 2013-03-27T14:37:29

Well you can always do this:

Require Import String.

Parameter foo: string -> list string -> nat.

Module Type A.

  Parameter toto : string -> nat. 

End A.

Module B <: A.

  Variable (* or Parameter, or Axiom *) ls : list string.

  Definition toto (s: string) := foo s ls.

End B.

But to my understanding that only makes ls an axiom... Another solution is to delay the providing of ls:

ModuleType HasListString.

  Parameter ls : list string.

End HasListString.

Module B(LS: HasListString) : A.

  Definition toto (s: string) := foo s LS.ls.

End B.

This might not be what you need though. Without context, it's hard to give you better advice.

Module error Type differ in Coq

1 Answers