Using include ignores refinement predicates

[jpolitz]

... but import doesn't!

provide-integer.arr:

provide *
provide-types *

type Integer = Number%(num-is-integer)

importer.arr:

include file("provide-integer.arr")

fun foo(n :: Integer):
  n
end

foo(10.5)

⤇ make importer.jarr
node -max-old-space-size=8192 build/phaseA/pyret.jarr --outfile importer.jarr \
                      --build-runnable importer.arr \
                      --builtin-js-dir src/js/trove/ \
                      --builtin-arr-dir src/arr/trove/ \
                      --compiled-dir compiled/ \
                      -no-check-mode \
                      --require-config src/scripts/standalone-configA.json
26/26 modules compiled (importer.arr)
Cleaning up and generating standalone...
~/s/pyret-lang (horizon|…71)
⤇ node importer.jarr
21/2The program didn't define any tests.

But! If you change to:

import file("provide-integer.arr") as F

fun foo(n :: F.Integer):
  n
end

print(foo(10.5))

You get:

⤇ make importer.jarr
node -max-old-space-size=8192 build/phaseA/pyret.jarr --outfile importer.jarr \
                      --build-runnable importer.arr \
                      --builtin-js-dir src/js/trove/ \
                      --builtin-arr-dir src/arr/trove/ \
                      --compiled-dir compiled/ \
                      -no-check-mode \
                      --require-config src/scripts/standalone-configA.json
26/26 modules compiled (importer.arr)
Cleaning up and generating standalone...
~/s/pyret-lang (horizon|…71)
⤇ node importer.jarr
The run ended in error:
The predicate`num-is-integer`in the annotation atfile:///Users/joe/src/pyret-lang/importer.arr:3:13-3:22returned false for this value: 21/2
Pyret stack:
  file:///Users/joe/src/pyret-lang/importer.arr: line 7, column 6

So something in the include desugaring is probably doing a direct alias to Number that's mistakenly skipping the new annotation on the imported module that has the predicate.

[shriram]

Please credit this bug observation to Dylan Hu.

[jpolitz]

To further narrow this down, this only happens on types that are written as SomeName%(predicate), then provided, then included. 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.