[ #13 ] Level for Sigma/Pi/Sum

oraluben commented 5 years ago

So far WIP, merge to fix CI error

ice1000 commented 5 years ago

I still feel like there's some problem with this implementation, but caching the Level information into Expression and Value does not sound like a problem to me.

ice1000 commented 5 years ago

I don't see any reason to have MaybeLevel instead of using Option<Level>. I'm replacing it with Option<Level>. Tell me if there's special reason.

ice1000 commented 5 years ago

Here's a (sub)list of problems I've encountered during refactoring this code:

Value::Sum has a Level, but how do you decide to calculate recursive sums' levels?
What's the point of having suc_level when you have level_safe().unwrap_or(0)?
Wrong error message: it's expecting a type whose level is 1 (as specified by Type1, but it's actually 2 (Type1, Type1 : Type 2): https://github.com/owo-lang/minitt-rs/blob/e9314140c5355e08b22efe745f4b612d8c40970c/samples/negative/level_fail.out#L2
How do you calculate the value of a generated value? https://github.com/owo-lang/minitt-rs/blob/e9314140c5355e08b22efe745f4b612d8c40970c/src/check/expr.rs#L203
Inferring the level of Sigma or Pi requires you to instantiate Sigma's second type or Pi's output type, which requires you to generate a value, instantiate the closure. Do you think it's worthwhile?

owo-lang / minitt-rs

[ #13 ] Level for Sigma/Pi/Sum #19