casting bug when double-annotating function parameters

[disconcision]

casting bug when double-annotating function parameters

[disconcision]

This is the problematic elaboration which causes the exception. I also tried disabling fixed point elaboration to make sure it wasn't fixed point casting related, ie it still occurs given this elaboration:

[disconcision]

Here's my analysis of what's going on. First, three similar but ultimately unproblematic scenarios for context, followed by the one above:

SCENARIO 1: if there's no annotation on the fn, but an annotation on the arg b:

let f = fun b:? {b[?->Bool] && true} in f(true[Bool->?])
=> (fun b:? {b[?->Bool] && true})(true[Bool->?])
=> (true[Bool->?])[?->Bool] && true
=> true[Bool->Bool] && true
=> true && true
=> true

SCENARIO 2: if there is an ? -> ? annotation on the fn, and an annotation on the arg b:

let f:?->? = fun b:? {(b[?->Bool] && true)[Bool->?]} in f(true[Bool->?])
=> (fun b:? {(b[?->Bool] && true)[Bool->?]})(true[Bool->?])
=> ((true[Bool->?])[?->Bool] && true)[Bool->?]
=> (true[Bool->Bool] && true)[Bool->?]
=> (true && true)[Bool->?]
=> true[Bool->?]
=> true

SCENARIO 3: if there is an Bool -> ? annotation on the fn, but no annotation on the arg b:

let f:Bool->? = fun b: Bool {(b && true)[Bool->?]} in f(true)
=> (fun b: Bool {(b && true)[Bool->?]})(true)
=> (true && true)[Bool->?]
=> true[Bool->?]
=> true

SCENARIO 4 (PROBLEM): if there is an Bool -> ? annotation on the fn AND an:

let f:Bool->? = fun b: Bool {(b[?->Bool] && true)[Bool->?]} in f(true)
=> (fun b: Bool {(b[?->Bool] && true)[Bool->?]})(true)
=> (true[?->Bool] && true)[Bool->?]
=> CastBVHoleGround

The inconsistency arises because the cast on the use of the parameter 'b' is determined by the annotation on the function parameter, but the cast on the function argument is determined by the annotation on the function. Thus in the case where these annotations are consistent, but the parameter annotation is less specific than the function annotation, we are left with an unresolved cast from a Hole to a Ground type.

Not obvious to me how to resolve this...

[disconcision]

One way would be to change the statics of type annotations and say that in analytic mode, the pattern of an annotation should be analytic against the joint type of the analytic type and the annotation type (if consistent). that addresses the immediate issue but seems to trigger other casting exceptions in other code (can't really be specific without more work to minimize them)

[disconcision]

@cyrus so the change we discussed isn't working because in the above scenario (4), the self-type of the function literal "fun b:? -> b && true" is Bool->Bool. So the function literal just gets cast from Bool->Bool to Bool->?, so after distribution the argument just gets cast Bool->Bool i.e. no-op.

The reason the self-type of the function literal "fun b:? -> b && true" is Bool->Bool is because the self-type of composite things are generally based on the fixed types of their components. So in this case, because the function literal is in analytic against Bool->?, the pattern ends up in analytic against Bool, so although the pattern has a self-type of ?, its fixed type is Bool.

Not quite sure how to proceed here...

[disconcision]

I guess i could special-case the casting for function literals to use the self-type of the pattern + body instead of the self-type of the function literal, but not sure what the principle is exactly