Estou tentando usar Módulos no meu projeto e fiz este pequeno exemplo para mostrar o que estou enfrentando.
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.
O que falha com:
O termo "2" possui o tipo "nat", embora seja esperado que tenha o tipo "t".
Basicamente, tenho um Module Type com um Type parametrizado e um Module que o instancia. O Módulo é uma implementação específica do Tipo de Módulo para naturais (portanto, t:=nat), portanto, quando estou tentando usar o módulo em um módulo de terceiros, quero falar sobre naturais usando esta instância.
No meu cenário real, tenho algumas coerções que quero que funcionem. Eu sei que se eu usar Nats no Módulo B as definições de A funcionariam bem, mas o que acontece é que obtenho valores de type te preciso tratá-los como type nat.
Existe alguma chance de "expor" a igualdade de tipo do módulo? Eu tentei algo como uma função de identidade: t -> natin amas não funciona.
É mesmo possível?