Skip to content

Type synonyms with same name in distinct interface imports getting confused when instantiating functors #1561

@qsctr

Description

@qsctr

If we have

interface module I where
type n : #
type m = 2 * n
module F where
import interface I as J
import interface I as K
module M where
type n = 2
module N where
type n = 3
module Inst = F { J = M, K = N }

then F correctly defines F::J::m = 4 and F::K::m = 6, but in Inst we have Inst::J::m = 6 and Inst::K::m = 6.

Furthermore, if we instead have

module F where
import interface I
import interface I as K
module Inst = F { I = M, K = N }

then in Inst we only have Inst::m = 6.

Metadata

Metadata

Assignees

Labels

bugSomething not working correctlyparameterized modulesRelated to Cryptol's parameterized modules

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions