Add let generalization

[TimWhiting]

Currently Koka instantiates at lets, this causes issues with using a function at multiple different effects.

Making that small change would solve the following issues.

401

402

Daan has been concerned whether this will cause other issues, due to some issues mentioned in this paper: Let should not be generalized

We should investigate whether Koka has the problems listed in the paper, and if not, let generalize, which would make the effect system a lot nicer.

[TimWhiting]

Reading through the paper again, their main argument is related to problems with constraint based type systems. Koka uses something closer to simple Hindley Milner so it does not have that problem. Additionally they state that generalization is not used much and so only in a very slim number of cases do you need it. In contrast I believe that the effect system of Koka makes this a much bigger issue here.

Let's take for example one of their examples of the issue:

data S a where
  MkS :: Show a => a -> S a

fs :: a -> S a -> Bool
fs x y = let h z = show x
  in case y of
    MkS v -> show v ++ h ()

This does not type check in Haskell, but with let generalization it would (since the function h would be generalized to include a Show constraint).

Koka does not have the same problem, show instances do not get populated in datatypes and implicitly destructured, additionally generalizing lambdas does not add implicit arguments. Instead this function would require a show instance, and be captured as a free variable in the lambda instead of propagated via constraints, and if you do want to add a show instance to a datatype it will be an explicit lambda that you would have to access from the datatype.