F# pattern matching with generic types. Possible?

I have the following code:

[<AbstractClass>]
type Effect<'a>() =
    class end

type Input<'a>(chan : Channel<'a>, cont : 'a -> Effect<'a>) = 
    inherit Effect<'a>()
    member this.Chan = chan
    member this.Cont = cont

type Output<'a>(value : 'a, chan : Channel<'a>, cont : unit -> Effect<'a>) =
    inherit Effect<'a>()
    member this.Value = value
    member this.Chan = chan
    member this.Cont = cont

type Parallel<'a, 'b>(eff1 : Effect<'a>, eff2 : Effect<'b>) =
    inherit Effect<'a * 'b>()
    member this.Eff1 = eff1
    member this.Eff2 = eff2

type Return<'a>(value : 'a) =
    inherit Effect<'a>()
    member this.Value = value

let Send(value, chan, cont) = Output(value, chan, cont)
let Receive(chan, cont) = Input(chan, cont)

let rec NaiveEval (eff : Effect<'a>) =
    match eff with 
    | :? Input<'a> as input           -> ()
    | :? Output<'a> as output         -> ()
    | :? Parallel<'a, 'b> as par      -> () // ERROR: FS0193: Type constraint mismatch. The type 'Parallel<'a,'b> is not compatible with type 'Effect<'a>'.
    | :? Return<'a> as ret            -> ()
    | _                               -> failwith "Unsupported effect!"

I want to be able to pattern match in some way on the different subclasses of Effect as seen in the NaiveEval function. The pattern match on Parallel<'a, 'b> gives the following error:

FS0193: Type constraint mismatch. The type 'Parallel<'a,'b> is not compatible with type 'Effect<'a>'.

I would assume that in this case 'a would be inferred to be 'a * 'b but I guess that is not what's happening.

Any help is appreciated. Thanks.

EDIT to Mark's answer:

So as far as I understand, what I am trying to do is not possible. I started out with a discriminated union, but I thought the type hierarchy would fix my issue. I guess not.

I used this union before:

type Effect<'a> =
     | Input of Channel<'a> * ('a -> Effect<'a>)
     | Output of 'a * Channel<'a> * (unit -> Effect<'a>)
     | Parallel of Effect<'a> * Effect<'a>
     | Return of 'a

I used to use this type, but I wanted to parallel to be: Parallel of Effect<'a> * Effect<'b> and not just both 'a. I assume this is not possible either?

Solution 1:

This is because the type parameter in Parallel is defined as corresponding to 'a * 'b. In other words, the single type parameter of Effect<'a> is here 'a * 'b.

Perhaps it's easier to understand how these correspond if you rename the type variables to 'b and 'c:

type Parallel<'b, 'c>(eff1 : Effect<'b>, eff2 : Effect<'c>) =
    inherit Effect<'b * 'c>()
    member this.Eff1 = eff1
    member this.Eff2 = eff2

Now you have that in the Parallel case, 'a = 'b * 'c.

The compiler error is exactly because you're trying to redefine what 'a is. Essentially, you're trying to insist that 'a = 'a * 'b. This doesn't work because you have 'a on both sides of the equals sign.

(We could imagine a more sophisticated type system that would allow this. This would essentially be like saying that x = x + y, which is only possible if y = 0. In the world of algebraic data types, this would imply that 'b would be () (unit)... but the F# type system can't infer that, and in any case it's probably not what you want.)

You can exchange the error for a compiler warning by explicitly using the renamed type arguments:

let rec NaiveEval (eff : Effect<'a>) =
    match eff with 
    | :? Input<'a> as input           -> ()
    | :? Output<'a> as output         -> ()
    | :? Parallel<'b, 'c> as par      -> () // Warning FS0064
    | :? Return<'a> as ret            -> ()
    | _                               -> failwith "Unsupported effect!"

The warning, however, is:

This construct causes code to be less generic than indicated by the type annotations. The type variable 'a has been constrained to be type ''b * 'c'.

In other words, the NaiveEval function can only evaluate Effect<'b * 'c> - probably still not what you want..?

This may still be a little difficult to accept, but imagine that you'd want to do something with par in the Parallel case. This, for example, doesn't compile because, once again, the types don't line up:

| :? Parallel<'b, 'c> as par      ->
    NaiveEval (par.Eff2)

Here, par.Eff2 has the type 'c, but you're currently 'inside' a function of the type Effect<'b * 'c> -> unit. You can't recurse into it, and compiler tells you so:

Error FS0001 The types ''c' and ''b * 'c' cannot be unified.

BTW, have you considered defining a discriminated union instead of a type hierarchy?