The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

To be clear, the code for 8.2 is slightly different.  We can not declare 
a subtype on OT_inner since this is unsupported.  "Include" must be 
changed to "Include Type" for compatibility.

Require Import OrderedType.
Require Import FMaps.

Module Type OT_inner.
(* I need any module her.  Normally, I would be using a functor, but any 
module will do. *)
  Declare Module Inner : OrderedType.
  Include Type OrderedType.OrderedType.
End OT_inner.

(* Module type copied excactly from FMap.Sord, only difference is input 
(X:OT) *)
Module List_Sord2 (X:OT_inner) (D:OrderedType) <: FMapInterface.Sord 
with Module Data := D with Module MapS.E := X.
  Module Inner := D.
  Module Sord := (FMapList.Make_ord X D).
  Include Sord.

(* Produces no error*)
End List_Sord2.



On 11/30/2010 05:53 PM, M. Scott Doerrie wrote:
> The following will type check in Coq 8.2 but not Coq 8.3.  Something I 
> don't understand is being lost in the definitions of module declarations.
>
> Require Import OrderedType.
> Require Import FMaps.
>
> Module Type OT_inner <: OrderedType.
> (* I need any module her.  Normally, I would be using a functor, but 
> any module will do. *)
>   Declare Module Inner : OrderedType.
>   Include OrderedType.OrderedType.
> End OT_inner.
>
> (* Module type copied excactly from FMap.Sord, only difference is 
> input (X:OT_inner) *)
> Module List_Sord2 (X:OT_inner) (D:OrderedType) <: FMapInterface.Sord 
> with Module Data := D with Module MapS.E := X.
>   Module Inner := D.
>   Module Sord := (FMapList.Make_ord X D).
>   Include Sord.
>
> (* produces error:
>    Error: The field Inner is missing in Top.List_Sord2.MapS.E.
>    However, the type of functor FMapList.Mak_ord <: Sord with Module 
> Data := D with Module MapS.E := X.
>    X has field Inner. *)
>
> End List_Sord2.