Open jpolitz opened 3 years ago
Please credit this bug observation to Dylan Hu.
To further narrow this down, this only happens on types that are written as SomeName%(predicate)
, then provided, then include
d. For a record type, for instance, like {x :: Number}%(x-is-integer)
, this example would have the expected behavior.
The issue is that, for good semantic reasons, the compiler tries to collapse aliases to the same underlying type when resolving imports. This makes it so if you include the same name from the same underlying module through various means, they can be compared for (static) equality and not cause a shadowing error. In addition, this makes it so from the type-checker's point of view, all refined Number
annotations are equal.
Unfortunately, in this case since the static information strips the predicate, and the static information is used by include
to resolve these aliases, it's doing the wrong thing and treating Integer
as a direct alias to Number
. The dynamic predicate type Integer
is still there, it's just skipped over in the dynamic lookup that populates the environment and Integer
in importer.arr
is bound to the same value as Number
.
So we need a little more information on bind-origin
data structures so that we can use one module origin for the static definition of the type, and another module origin for where to look it up dynamically.
... but import doesn't!
provide-integer.arr
:importer.arr
:But! If you change to:
You get:
So something in the
include
desugaring is probably doing a direct alias toNumber
that's mistakenly skipping the new annotation on the imported module that has the predicate.