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

Apply functor instantiation map to types #1592

Merged
merged 4 commits into from
Dec 8, 2023
Merged

Apply functor instantiation map to types #1592

merged 4 commits into from
Dec 8, 2023

Conversation

qsctr
Copy link
Contributor

@qsctr qsctr commented 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 referred 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". I have renamed them to better reflect this.

Fixes #1590.

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 qsctr added the parameterized modules Related to Cryptol's parameterized modules label Nov 29, 2023
@qsctr qsctr requested a review from yav November 29, 2023 05:13
@qsctr qsctr self-assigned this Nov 29, 2023
@qsctr qsctr removed the request for review from yav November 29, 2023 05:13
@qsctr qsctr requested a review from yav December 5, 2023 04:02
@qsctr qsctr marked this pull request as ready for review December 5, 2023 04:02
@qsctr qsctr merged commit d23add7 into master Dec 8, 2023
43 checks passed
@qsctr qsctr deleted the T1590 branch December 8, 2023 19:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Type synonyms of newtypes in functors not getting instantiated
2 participants