Sam Tobin-Hochstadt
Sam Tobin-Hochstadt
I think `Refinement` needs the function to already be typechecked before the use of `Refinement`. The best way to do this is to use a separate module.
We should give it a simpler one then, even though that will be somewhat unsatisfying.
Typed Racket has some tricks to try to make some things like this typecheck, and could do more (obviously we could just inline that function and then typecheck) but it...
Yes, I think so.
For 1, that portion of the type just shouldn't be printed at all (and when it is printed, it should print in the way you can write it). It isn't...
Yes, anything that can appear printed should be legal to write.
This is probably failing to figure out that `f` is defined "locally" and thus needs a contract.
That would work, and seems easy enough.
I think this is a doc bug -- that case is allowed.
Right, but case-> is a type constructor and case-lambda, which this report is about, is a term constructor.