b -> Bool> = (:*:) (x::a) (y::b

) @-} {-@ measure pfst :: (PairS a b) -> a pfst ((:*:) x y) = x @-} {-@ measure psnd :: (PairS a b) -> b psnd ((:*:) x y) = y @-} {-@ type FooS a = PairS <{\z v -> v <= (psnd z)}> (PairS a Int) Int @-} {-@ moo :: a -> Int -> (FooS a) @-} moo :: a -> Int -> PairS (PairS a Int) Int moo x n = (x :*: n :*: m) -- moo x n = (x :*: 1 :*: 100) -- ALAS, also reported "SAFE" where m = n + 1