Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type synonyms of newtypes in functors not getting instantiated #1590

Closed
qsctr opened this issue Nov 24, 2023 · 0 comments · Fixed by #1592
Closed

Type synonyms of newtypes in functors not getting instantiated #1590

qsctr opened this issue Nov 24, 2023 · 0 comments · Fixed by #1592
Assignees
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules

Comments

@qsctr
Copy link
Contributor

qsctr commented Nov 24, 2023

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.

@qsctr qsctr added bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules labels Nov 24, 2023
@qsctr qsctr self-assigned this Nov 29, 2023
qsctr added a commit that referenced this issue Nov 29, 2023
If a functor contains both a newtype and a type synonym referring to the
newtype, then during instantiation we must apply the instantiation map
to the types in the functor, so that the type synonym now refers to the
instantiated newtype instead. Previously, we only applied type
substitutions to the types in the functor, which would replace type
variables with concrete types defined in the functor arguments, but
would not replace any actual names. (Confusingly, the code refers to the
instantiation map as "value substitutions" even though it can contain
names in the type namespace. The "type substitutions" and "value
substitutions" are better thought of as "TVar -> Type mappings" and
"Name -> Name mappings".)

Fixes #1590.
qsctr added a commit that referenced this issue Dec 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant