[merd-devel] polymorphic |-upcasting, |-downcasting, |&|-upcasting, |&|-downcasting

[Pixel <pi...@ma...>]

 | -  upcasting  !!    t    ->  t | A   # is written  t -> (t !< A) ; t
|&|-  upcasting  !! t |&| A ->    A     # is written  A -> A
|&|-  upcasting2 !! t |&| A ->    t
|&|-downcasting  !!    t    -> t |&| A
 | -downcasting  !!  A | _  ->    A
 | -downcasting2 !!  A | t  ->    t

 | -  upcasting  := x -> x
|&|-  upcasting  := x -> x
|&|-  upcasting2 := x -> x
|&|-downcasting  := x -> check_A(x) ; x
 | -downcasting  := x -> check_A(x) ; x
 | -downcasting2 := x -> check_non_A(x) ; x

I don't know if the type system will be able to achieve all this
below. The non-polymorphic versions of these are ok 
(eg: A|&|B -> A or A|B -> A)


PS:
  check_A =
      A -> ()
      _ -> raise("check_A")
  
  check_non_A =
      A -> raise("check_non_A")
      _ -> ()