The following example passes the type checking and I think should not. In the pattern of the first equation, the argument of the function (which is a channel) is used to receive a label that is then checked if it is A, c is then bound to the channel continuation. In the pattern of the second equation, the argument of the function is bound to c. This two equations are not compatible and should not be allowed in the same function.
type T: 1S
type T = &{A: Close, B: Wait}
f : T -> ()
f (&A c) = close c
f c = case c of
&A c1 -> close c1
&B c1 -> wait c1
The following example passes the type checking and I think should not. In the pattern of the first equation, the argument of the function (which is a channel) is used to receive a label that is then checked if it is A, c is then bound to the channel continuation. In the pattern of the second equation, the argument of the function is bound to c. This two equations are not compatible and should not be allowed in the same function.