@@ -418,17 +418,17 @@ type Implication =
418418 /// Indicates nothing in particular
419419 | Nothing
420420
421- /// Work out what one successful type test implies about a null test
421+ /// Work out what a successful type test (against tgtTy1) implies about a null test for the same input value.
422422///
423423/// Example:
424424/// match x with
425- /// | :? string -> ...
425+ /// | :? string when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
426426/// | null -> ...
427427/// For any inputs where ':? string' succeeds, 'null' will fail
428428///
429429/// Example:
430430/// match x with
431- /// | :? (int option) -> ...
431+ /// | :? (int option) when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
432432/// | null -> ...
433433/// Nothing can be learned. If ':? (int option)' succeeds, 'null' may still have to be run.
434434let computeWhatSuccessfulTypeTestImpliesAboutNullTest g tgtTy1 =
@@ -437,7 +437,7 @@ let computeWhatSuccessfulTypeTestImpliesAboutNullTest g tgtTy1 =
437437 else
438438 Implication.Fails
439439
440- /// Work out what a failing type test implies about a null test.
440+ /// Work out what a failing type test (against tgtTy1) implies about a null test for the same input value .
441441///
442442/// Example:
443443/// match x with
@@ -450,17 +450,17 @@ let computeWhatFailingTypeTestImpliesAboutNullTest g tgtTy1 =
450450 else
451451 Implication.Nothing
452452
453- /// Work out what one successful null test implies about a type test.
453+ /// Work out what one successful null test implies about a type test (against tgtTy2) for the same input value .
454454///
455455/// Example:
456456/// match x with
457- /// | null -> ...
457+ /// | null when false -> ... // note: "when false" used so null test succeeds but proceed to next type test
458458/// | :? string -> ...
459459/// For any inputs where 'null' succeeds, ':? string' will fail
460460///
461461/// Example:
462462/// match x with
463- /// | null -> ...
463+ /// | null when false -> ... // note: "when false" used so null test succeeds but proceed to next type test
464464/// | :? (int option) -> ...
465465/// For any inputs where 'null' succeeds, ':? (int option)' will succeed
466466let computeWhatSuccessfulNullTestImpliesAboutTypeTest g tgtTy2 =
@@ -469,67 +469,79 @@ let computeWhatSuccessfulNullTestImpliesAboutTypeTest g tgtTy2 =
469469 else
470470 Implication.Fails
471471
472- /// Work out what a failing null test implies about a type test. The answer is "nothing" but it's included for symmetry.
472+ /// Work out what a failing null test implies about a type test (against tgtTy2) for the same
473+ /// input balue. The answer is "nothing" but it's included for symmetry.
473474let computeWhatFailingNullTestImpliesAboutTypeTest _g _tgtTy2 =
474475 Implication.Nothing
475476
476- /// Work out what one successful type test implies about another type test
477+ /// Work out what one successful type test (against tgtTy1) implies about another type test (against tgtTy2)
478+ /// for the same input value.
477479let computeWhatSuccessfulTypeTestImpliesAboutTypeTest g amap m tgtTy1 tgtTy2 =
478480 let tgtTy1 = stripTyEqnsWrtErasure EraseAll g tgtTy1
479481 let tgtTy2 = stripTyEqnsWrtErasure EraseAll g tgtTy2
480482
481- // A successful type test on any type implies all supertypes always succeed
483+ // A successful type test of an input value against a type (tgtTy1)
484+ // implies all type tests of the same input value on equivalent or
485+ // supertypes (tgtTy2) always succeed.
482486 //
483487 // Example:
484488 // match x with
485- // | :? string -> ...
489+ // | :? string when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
486490 // | :? IComparable -> ...
487491 //
488492 // Example:
489493 // match x with
490- // | :? string -> ...
494+ // | :? string when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
491495 // | :? string -> ...
492496 //
493497 if TypeDefinitelySubsumesTypeNoCoercion 0 g amap m tgtTy2 tgtTy1 then
494498 Implication.Succeeds
495499
496- // A successful type test on a sealed type implies all non-related types fail
500+ // A successful type test of an input value against a sealed target type (tgtTy1) implies all
501+ // type tests of the same object against a unrelated target type (tgtTy2) fails.
497502 //
498503 // Example:
499504 // match x with
500- // | :? int -> ...
505+ // | :? int when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
501506 // | :? string -> ...
502507 //
503508 // For any inputs where ':? int' succeeds, ':? string' will fail
504509 //
505- // This doesn't apply to related types:
510+ //
511+ // This only applies if tgtTy2 is not potetnially related to the sealed type tgtTy1:
506512 // match x with
507- // | :? int -> ...
513+ // | :? int when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
508514 // | :? IComparable -> ...
509515 //
510- // Here IComparable neither fails nor is redundant
516+ // Here IComparable is not known to fail (NOTE: indeed it is actually known to succeed,
517+ // give ":? int" succeeded, however this is not utilised in the analysis, because it involves coercion).
518+ //
511519 //
512- // This doesn't apply to unsealed types:
520+ // This rule also doesn't apply to unsealed types:
513521 // match x with
514- // | :? SomeClass -> ...
522+ // | :? SomeUnsealedClass when false -> ... // note: "when false" used so type test succeeds but proceed to next type test
515523 // | :? SomeInterface -> ...
524+ // because the input may be some subtype of SomeUnsealedClass and that type could implement SomeInterface even if
525+ // SomeUnsealedClass doesnt.
526+ //
516527 //
517- // This doesn't apply to types with null as true value:
528+ // This rule also doesn't apply to types with null as true value:
518529 // match x with
519- // | :? (int option) -> ...
530+ // | :? (int option) when false -> ... // "when false" means type test succeeds but proceed to next type test
520531 // | :? (string option) -> ...
521532 //
522533 // Here on 'null' input the first pattern succeeds, and the second pattern will also succeed
523534 elif isSealedTy g tgtTy1 &&
524535 not ( TypeNullIsTrueValue g tgtTy1) &&
525- not ( TypeDefinitelySubsumesTypeNoCoercion 0 g amap m tgtTy2 tgtTy1) then
536+ not ( TypeFeasiblySubsumesType 0 g amap m tgtTy2 CanCoerce tgtTy1) then
526537 Implication.Fails
527538
528- // A successful type test on an unsealed class type implies type tests on unrelated non-interface types always fail
539+ // A successful type test of an input value against an unsealed class type (tgtTy1) implies
540+ // a type test of the same input value against an unrelated non-interface type (tgtTy2) always fails
529541 //
530542 // Example:
531543 // match x with
532- // | :? SomeUnsealedClass -> ...
544+ // | :? SomeUnsealedClass when false -> ... // "when false" used so type test succeeds but proceed to next type test
533545 // | :? SomeUnrelatedClass -> ...
534546 //
535547 // For any inputs where ':? SomeUnsealedClass' succeeds, ':? SomeUnrelatedClass' will fail
@@ -543,11 +555,13 @@ let computeWhatSuccessfulTypeTestImpliesAboutTypeTest g amap m tgtTy1 tgtTy2 =
543555 not ( TypeFeasiblySubsumesType 0 g amap m tgtTy2 CanCoerce tgtTy1) then
544556 Implication.Fails
545557
546- // A successful type test on an interface type refutes sealed types that do not support that interface
558+ // A successful type test of an input value against an interface type (tgtTy1) implies
559+ // a type test of the same object against a sealed types (tgtTy2) that does not support that interface
560+ // always fails.
547561 //
548562 // Example:
549563 // match x with
550- // | :? IComparable -> ...
564+ // | :? IComparable when false -> ... // "when false" used so type test succeeds but proceed to next type test
551565 // | :? SomeOtherSealedClass -> ...
552566 //
553567 // For any inputs where ':? IComparable' succeeds, ':? SomeOtherSealedClass' will fail
@@ -561,12 +575,13 @@ let computeWhatSuccessfulTypeTestImpliesAboutTypeTest g amap m tgtTy1 tgtTy2 =
561575 else
562576 Implication.Nothing
563577
564- /// Work out what one successful type test implies about another type test
578+ /// Work out what one failing type test (tgtTy1) implies about another type test (tgtTy2)
565579let computeWhatFailingTypeTestImpliesAboutTypeTest g amap m tgtTy1 tgtTy2 =
566580 let tgtTy1 = stripTyEqnsWrtErasure EraseAll g tgtTy1
567581 let tgtTy2 = stripTyEqnsWrtErasure EraseAll g tgtTy2
568582
569- // A failing type test on any type implies all subtypes fail
583+ // If testing an input value against a target type (tgtTy1) fails then
584+ // testing the same input value against an equivalent or subtype type (tgtTy2) always fails.
570585 //
571586 // Example:
572587 // match x with
0 commit comments