Type test yields error for union test-expression

Question

My question relates to the following programme.

open System

// Types
type Car (brand: string) =
    member _.Brand = brand
type BMW () =
    inherit Car "BMW"
type Pet =
    | Cat
    | Dog

[<EntryPoint>]
let main argv =
    // Match subtype of test-expression type: ok
    let car = Car "Mercedes"
    let carResult =
        match car with
        | :? BMW -> 1
        | _ -> 0
    // Match type of test-expression: "will always hold" warning
    let bmw = BMW ()
    let bmwResult =
        match bmw with
        | :? BMW -> 1
        | _ -> 0
    // Catch any exception: "will always hold" warning
    let exceptionResult =
        try
            1/0
        with
            | :? Exception -> 2
    // Match type of test-expression (union type): "The type 'Pet' does not have any proper subtypes" error
    let cat = Cat // this has type Pet
    let catResult =
        match cat with
        | :? Pet -> 1
        | _ -> 0
    0

In the first test, the test-expression is of type Car, of which the type in the type test pattern, BMW, is a subtype, and there are no warnings or errors. In the second and third tests, the type in the type test pattern is the same as the type of the test-expression, and a warning is raised, understandably, because when the programmer is testing whether a BMW is really a BMW, or an Exception is really an Exception, it is likely a logical error.

The last test has the same form as tests two and three: the test-expression is of type Pet, and the type test pattern is also Pet. So why in this case does it generate an error? The error says The type 'Pet' does not have any proper subtypes.... But BMW doesn't have any subtypes, and doesn't yield this error. Moreover, the Pattern Matching page (under "Type Test Pattern") says that "If the input type is a match to (or a derived type of) the type specified in the pattern, the match succeeds." Pet is a match to Pet, ergo, etc.. Why is the union type treated differently?

Answer 1

Perhaps the error message is phrased a bit too vaguely. It's not that the type Pet doesn't have subtypes, it's that it can't have subtypes.

Because BMW is a class, it may have a subtype coming from a different assembly, which was compiled after the one where BMW itself is defined.

But for Pet this cannot happen, because sum types cannot have subtypes, and so inheritance-matching for these types is prohibited.

Note also that the source of the error is the type of the variable being matched, not the type of the pattern. So, for example, this will compile without errors:

let n : obj = null

match n with
| :? Pet -> "is a pet"
| _ -> "no idea"

This works, because n is of type obj, which does have subtypes, of which Pet is one (this is .NET after all, everything is an object). But matching on your variable cat doesn't work, because that variable is of an inherently subtype-less type.