Variance.hs

module Variance where

{-@ data variance Foo invariant bivariant covariant contravariant @-}
data Foo a b c d



{-@ check_covariant :: Foo a b {v:Int | v = 1} c -> Foo a b {v:Int | v > 0} c @-}
check_covariant :: Foo a b Int c -> Foo a b Int c
check_covariant r = r


{-@ check_contravariant0 :: Foo a b c {v:Int | v > 0} -> Foo a b c {v:Int | v = 1} @-}
check_contravariant0 :: Foo a b c Int-> Foo a b c Int
check_contravariant0 r = r

{-@ check_contravariant :: ((Foo a b c {v:Int | v = 1}) -> ()) -> (Foo a b c {v:Int | v > 0}) -> () @-}
check_contravariant :: ((Foo a b c Int) -> ()) -> Foo a b c Int -> ()
check_contravariant r = r

{-@ check_bivariant :: Foo a {v: Int | v = 1} c d -> Foo a {v:Int | ((v > 0) && (v < 2))} c d @-}
check_bivariant :: Foo a Int c d -> Foo a Int c d
check_bivariant r = r


{-@ check_invariant :: Foo {v: Int | v = 1} b c d -> Foo {v:Int | ((v > 0) && (v < 2))} b c d @-}
check_invariant :: Foo Int b c d -> Foo Int b c d
check_invariant r = r