fix: const primitive directionality

[brprice]

Since const x y is synthesisable but x is checkable, the reduction rule is const x y ~> x : Bool (rather than const x y ~> x). Note that const is restricted to type Bool -> Int -> Bool, and that this reduction matches that of obvious analogue where const is replaced by the non-primitive (λx y. x) : Bool -> Int -> Bool.

[brprice]

Note that this bug can manifest in a slightly odd test failure, where the type preservation test fails with CaseOfHoleNeedsEmptyBranches, because the initial term case (const ? t) of True -> ...; False -> ... is well-typed (recall const : Bool -> Int -> Bool), but it reduces to case ? of True -> ...; False -> ....

I suspect it can also fail with a could not synthesise type error because of case (const True t) of ... reducing to case True of ..., and our approach of (ADT) constructors not being synthesisable (even for easy cases like Bool): the scrutinee needs its type to be synthesised, but we cannot synthesise the type of True. (However I have not actually observed this, presumably for lack of looking. EDIT: I have now observed this, but only when turning off shrinking.)

[brprice]

(whoops, forgot to update a test. force-pushed)

[dhess]

Note that this bug can manifest in a slightly odd test failure, where the type preservation test fails with CaseOfHoleNeedsEmptyBranches, because the initial term case (const ? t) of True -> ...; False -> ... is well-typed (recall const : Bool -> Int -> Bool), but it reduces to case ? of True -> ...; False -> ....

I suspect it can also fail with a could not synthesise type error because of case (const True t) of ... reducing to case True of ..., and our approach of (ADT) constructors not being synthesisable (even for easy cases like Bool): the scrutinee needs its type to be synthesised, but we cannot synthesise the type of True. (However I have not actually observed this, presumably for lack of looking.)

I assume that by "can manifest" and "can also fail," you mean before this fix, and that once this fix is in, these failures will no longer manifest?

[brprice]

Note that this bug can manifest in a slightly odd test failure...
I suspect it can also fail with a could not synthesise type error...

I assume that by "can manifest" and "can also fail," you mean before this fix, and that once this fix is in, these failures will no longer manifest?

Yes, that is what I meant.