Determine the types of variables in matched expressions

fun (x : Int|Bool , y : Int | Bool) : Int | Bool = 
  match (x,y) with 
   | (Int,Bool) -> if y then x+3 else x +2
   | _ -> x;;

does not type. In order to have it working we have to redefine the pattern as follows

fun (x : Int|Bool , y : Int | Bool) : Int | Bool = 
  match (x,y) with 
   | (Int,Bool)&(x,y) -> if y then x+3 else x +2
   | _ -> x;;

Idea ... in order to refine the type of variables occuring in the MATCHED expression, then whenever this expression is ALSO A PATTERN rewrite it as follows:

match p with p1 -> e1 | ... | pn-> en

into

match p with p&p1 -> e1 | ... | p&pn-> en

Unfortunately this does not work when p and pi have a variable in common. We must find a smarter solution.

Edited Oct 08, 2021 by Kim Nguyễn