{-@ plus :: x:a -> y:a -> {v:a | v = x} @-}
plus :: a -> a -> a
plus = undefined