The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Brian E. Aydemir wrote:

> Hi everyone,
>
> I'm working in Coq 8.1gamma. The errors I'm seeing from the module 
> system are confusing to me, so I'm hoping that I can find some help 
> from this list. As far as I can tell, I must be misunderstanding 
> something important about the difference between ":" and "<:" when 
> ascribing types to modules. Two small examples showing exactly what 
> confuses me are below.
>
> Thanks,
> Brian
>
> (* ********* *)
>
> All of my examples assume the following libraries are imported:
>
> Require Import DecidableType.
> Require Import DecidableTypeEx.
>
>
> EXAMPLE 1: Consider the following code.
>
> (* *** *)
> Module Type Test.
> Declare Module E : DecidableType.
> End Test.
> Module Make (X : DecidableType) <: Test with Module E := X.
> Module E : DecidableType := X.
> End Make.
> (* *** *)
>
> The "End Make" results in the following error: "User error: Signature 
> components for label t do not match". My question(s): where is this 
> label t coming from and why? If I change the line
>
> Module E : DecidableType := X.
>
> to
>
> Module E <: DecidableType := X.
>
> this example goes through without problem. I'm not sure what the 
> meaningful difference here is. In both cases, E is defined by a module 
> expression which has an appropriate module type, and I don't see what 
> the visibility of the things inside E has to do with anything.
Hi,

Module E : DecidableType := X is a generative declaration. So E.t is not 
convertible to X.t.
The constraint Module E := X is therefore not satisfied.
On the other hand, Module E <: DecidableType := X is not generative, E 
is an alias for X, with a check that its signature can be coerced to 
DecidableType. In this case the constraint is satisfied.

> EXAMPLE 2: Extending the above example, consider the following.
>
> (* *** *)
> Module Type Test.
> Declare Module E : DecidableType.
> End Test.
> Module Make (X : DecidableType) <: Test with Module E := X.
> Module E <: DecidableType := X.
> End Make.
> Module N' : DecidableType := Nat_as_DT.
> Module Q : Test with Module E := N' := Make N'.
> (* *** *)
>
> That works without problem. If I change the line
>
> Module N' : DecidableType := Nat_as_DT.
>
> to
>
> Module N' <: DecidableType := Nat_as_DT.
>
> the definition of Q gives me the error "User error: No such label OF". 
> Why is this the case? Trying to define Q directly, via
>
> Module Q : Test with Module E := Nat_as_DT := Make Nat_as_DT.
>
> results in the same error.
This one looks like a bug to me. Unless someone finds an explanation, I 
suggest you file a bug report on coq-bugs.

Cheers,
Bruno Barras.