GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Type synonyms of newtypes in functors not getting instantiated #1590

Closed qsctr closed 11 months ago

qsctr commented 12 months ago
module Main where

submodule F where
  parameter
    x : Bit
  newtype T = { bit : Bit }
  type U = T

submodule M = submodule F where x = False

import submodule M

foo : U
foo = T { bit = True }
[error] at Main.cry:14:7--14:8:
  Type mismatch:
    Expected type: Main::F::T
    Inferred type: Main::M::T
    Context: _ -> ERROR
    When checking function call

It seems like we are not properly instantiating U and M::U still points to F::T instead of M::T.