Remove normalization tests for Sort?

[ocharles]

My understanding is normalisation is only defined in the context of well-typed expressions, but Sort doesn't have a type, so it's meaningless to ask for its normal form. Due to this, my test suite is currently stuck on dhall-lang/tests/normalization/success/unit/SortA.dhall, and I'm not sure how to proceed.

[Nadrieril]

I just skip it. The test alpha-normalization/success/unit/FunctionNestedBindingXXFreeA.dhall is similar: it's not well-typed but might be useful for an implementation anyways.

[Gabriella439]

My suggestion is:

• Remove the SortA.dhall test

  It doesn't add much value, in my opinion

• Make the FunctionNestedBindingXXFreeA.dhall type-correct

[Nadrieril]

FunctionNestedBindingXXFreeA.dhall cannot be made type-correct. It's point is to check for the correct handling of free variables, for implementations that support that. dhall-rust used to support that, and this was a very useful test to have.

[Gabriella439]

Oh yeah, good point. Never mind

[ocharles]

Edit: sorry, ignore this comment. It was about type-inference tests, but this issue is about normalization tests.

[ocharles]

So, just to wrap this one up, am I OK to submit a PR removing SortA.dhall? That at least solves my problem with the beta-equivalence tests.

[sjakobi]

https://github.com/dhall-lang/dhall-lang/blob/master/standard/beta-normalization.md#constants specifies how to normalize Sort. So I think the test is useful for implementations that can handle it.

If it's important to separate the ill-typed test cases, maybe we can keep them separately in normalization/success/ill-typed.

[Nadrieril]

I'd also add that the current type inference rules ensure that the resulting type is normalized. Since Sort is a possible such output, being able to normalize Sort is sensible