Open ohad opened 4 years ago
Hmm, it's probably just not propagating the multiplicity to the local definition properly. You probably at least noticed that you can work around this for now with an explicit annotation on q
. (Also that your last bar
should be baz
:))
Assuming that let (omega q : Bool) = foo True in q
should be equivalent to (\omega q : Bool => q) (foo True)
, this should typecheck because the result of the lambda is used zero times.
So I don't think the annotation on q
is inferred wrong. I think that the type checker should accept an omega
there; is that right?
@ziman : This is a local definition, and not a let-binding. See the README
Oh, I see, thanks!
I thought we discussed/reported this at some point, but I can't find the report/fix.
Steps to Reproduce
Expected Behavior
Observed Behavior