Coq : Using a parametrized Type from within a Module

Question

I'm trying to use Modules in my project and I made this small example to show what I'm struggling with.

Module Type A.
  Parameter t : Type.
End A.

Module a : A.
  Definition t := nat.
End a.

Module B.
  Module Import InstanceOfA := a.
  Definition x : t := 2.
  Definition sum (t1 t2 : t) : nat :=  t1 + t2.    
End B.

Which fails with:

The term "2" has type "nat" while it is expected to have type "t".

Basically, I have a Module Type with a parametrized Type and a Module that instantiates it. The Module is a specific implementation of the Module Type for naturals (hence t:=nat), so when I'm trying to use the module in a third-party module I want to talk about naturals using this instance.

In my real scenario, I have some coercions I want to get working. I know that if I use Nats in Module B the definitions from A would work fine, but what happens is that I obtain values of type t and need to treat them as type nat.

Is there any chance to "expose" the type equality from the module? I tried something like an identity function: t -> nat in a but it doesn't work.

Is it even possible?

Answer 1

Instead of Module a : A., which seals the module (and thus hides the definition of t), write Module a <: A., which keeps a's definition visible.