Issue https://github.com/CakeML/pure/issues/27 ensures that most dead code still gets type-checked. However there are still problems with multiple declarations of the same name due to the letrec distinctness pass. Also, the parser must still check for closed expressions, even though type inference already does this.
As discussed in a meeting, this issue suggests:
moving distinct declaration checking to parsing: remove the existing pass and reject programs with multiple declarations of the same name
removing the parser closedness check, relying on this result to lift type inference checks upwards
Unfortunately it is not enough to check top-level declarations only, as demand analysis proofs require letrec_distinct.
Rejection of programs with multiple declarations of the same name is in line with GHC. However, if we support function-clause pattern-matching in the future, we must be careful to align with GHC's behaviour in warning on overlapping patterns rather than rejecting programs when appropriate.
Issue https://github.com/CakeML/pure/issues/27 ensures that most dead code still gets type-checked. However there are still problems with multiple declarations of the same name due to the
letrecdistinctness pass. Also, the parser must still check for closed expressions, even though type inference already does this.As discussed in a meeting, this issue suggests:
Unfortunately it is not enough to check top-level declarations only, as demand analysis proofs require
letrec_distinct.Rejection of programs with multiple declarations of the same name is in line with GHC. However, if we support function-clause pattern-matching in the future, we must be careful to align with GHC's behaviour in warning on overlapping patterns rather than rejecting programs when appropriate.