Nominal types

theory MyModuleType := sig end
theory YourModuleType := sig end

def bad (x : MyModuleType) : YourModuleType := x

\[\begin{align*} &\ms{Energy} := \{k,p\} \\ &\ms{Ty}_{-} \colon \ms{Energy} \to \ms{Jdg} \\ &\ms{El}_{-} \colon \ms{Energy} \to \ms{Ty}_k \to \ms{Jdg}^+ \\ &\ms{\rightsquigarrow} \colon \{A \colon \ms{Ty}_k\} \to \ms{El}_k\,A \to \ms{El}_p\,A \to \ms{Jdg}^+ \\ &\ms{let}_p \colon \{A\,B \colon \ms{Ty}_k\} \to (a' \colon \ms{El}_p\,A) \to ((a \colon \ms{El}_k\,A) \to a \rightsquigarrow a' \to \ms{El}_k\,B) \to \ms{El}_k\,B \\ \end{align*}\]

Taken from reading the Narya source code; I believe this is original to Shulman.