brownplt / pyret-lang

The Pyret language.
Other
1.07k stars 111 forks source link

cannot use REPL after putting refinements (aka predicate annotations) on type declarations #1663

Open pnkfelix opened 2 years ago

pnkfelix commented 2 years ago

Consider the following code:

WIDTH = 3

fun in-bounds(x :: Number) -> Boolean:
  (0 <= x) and (x < WIDTH)
end

data PlaceV0: place-d-v0(x :: Number % (in-bounds), y :: Number % (in-bounds)) end

fun place-t-v0(x :: Number % (in-bounds), y :: Number % (in-bounds)) -> {Number % (in-bounds); Number % (in-bounds)}:
  {x; y} 
end

# type Coord = Number % (in-bounds)

# data Place: place-d-v1(x :: Coord, y :: Coord) end

# fun place-t-v1(x :: Coord, y :: Coord) -> {Coord; Coord}: {x; y} end

It runs, and you can do things like place-d-v0(2, 2) in the REPL, and you get values you expect.

But, as you might have predicted, I wanted to avoid the repeating the refinement annotation, So I tried to make a type, Coord.

As soon as you uncomment type Coord = Number % (in-bounds) above, then the repl complains in response to any interactions , saying: "Could not find type Coord on module definitions://"

pnkfelix commented 2 years ago

or actually, maybe this is an instance of a more general problem with type declarations? See e.g. #1623

asolove commented 1 year ago

The refined named type works correctly if you switch from untyped to typed run mode in CPO, so I think this is the same as #1677.