The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

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.


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.