Beluga icon indicating copy to clipboard operation
Beluga copied to clipboard

Bad error message when a hole is used in the type of a let statement

Open tsani opened this issue 6 years ago • 1 comments

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.

tsani avatar May 07 '18 13:05 tsani

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.

tsani avatar Sep 26 '20 14:09 tsani