\forall x vs. \forall robust x

[davidweichiang]

This does not cause an error (even with -O0):

define double = \x. (x, x);
let f = double (\y. y) in ()

However, these do:

let f = (\x. (x, x)) (\y. y) in ()

data BoxT b = Box b;
let z = (case Box (\x. x) of Box y -> (y, y)) in ()

[davidweichiang]

Definitely a bug:

define double = \x. (x, x);
let (f, g) = double (\y. y) in f ()

-z gives [0.0], which is not right.

[davidweichiang]

I think the problem is that when a function definition is typechecked, we need to record whether each \forall-quantified type variable needs to be constrained to be Robust. Then when infer' instantiates a \forall-quantified type variable to a fresh one, it needs to add a Robust constraint if needed. This information can be stored in a few possible places:

1. Add yet another parameter to SProgFun and DefGlobal.
2. The list of constraints already records this information, and I believe it is never cleared, so infer' could search the constraints to see if the \forall-quantified variable had a Robust constraint on it.
3. After Var is split up into different types (#103), there will presumably be a newtype TypeVar = String; this could become data TypeVar = TvAny | TvRobust.

[davidweichiang]

4. infer' can generate a constraint like RobustIf x y where x is the \forall-quantified type variable and y is the fresh one. The meaning is if there is a constraint Robust x then y must also be robust. Then solvedWell can make two passes through the list of constraints, first collecting all the Robust constraints, then checking the RobustIf constraints.

[davidweichiang]

I don't think 2 or 4 will work, since the constraints are not retained across SCCs. So maybe 3? @ccshan, are you trying to split Var into multiple types?

[davidweichiang]

5. If infer' had access to the function definitions, it could just check whether the definition uses each parameter twice.