Subtyping on pairs

[ngrimm]

I had a problem with subtyping in pairs and I reduced it to this program:

module Pairs

val test1 : (x:int{x>0} * unit)
let test1 = 2, ()

val test2 : (x:int * unit)
let test2 = test1 

It fails with:

pairs.fst(7,12-7,17): Subtyping check failed; expected type (Tuple2 int unit); got type (Tuple2 x:int{(x > 0)} unit)

[catalin-hritcu]

AFAIK this is a known limitation. Adding polarities would solve this, but for now you can build explicit coercion functions:

val coerce : (nat * unit) -> (int * unit)
let coerce p = let (x1,x2) = p in (x1,x2)

val test2' : (x:int * unit)
let test2' = coerce test1

[catalin-hritcu]

There is already an issue about this #65, closing as duplicate.