Beluga
Beluga copied to clipboard
Bad error message when a hole is used in the type of a let statement
My resolution for #68 is simply to change the error into a proper user error: right now there isn't much support for holes appearing in positions other than as terms. However, that's not to say that there shouldn't be such support.
For example, it should be possible to write let x : ? = foo
and give the hole whatever the type of foo
is (and since foo
is a synthesizable expression, we can figure out its type). Presently, this declaration produces a parse error.
It should also be possible to do with with boxed types, as demonstrated in #68. let x : [ |- ? ] = [ |- foo ]
currently parses, but as of PR #86 produces an "ill-formed computation-level type" error.
Throughout the development of Harpoon, we have realized that holes in synthesizable positions is a bad idea, broadly speaking, because of uninstantiated unification variables. Instead, this issue should be about correcting the error message produced when a hole appears in a synthesizable position, and perhaps they should be forbidden during parsing.