{-# LANGUAGE FlexibleInstances #-}

module Instances where

class OptEq a where
  (==.) :: a -> a -> a

instance OptEq a where
{-@ instance OptEq a where
  ==. :: x:a -> y:{a| x == y} -> a
  @-}
  (==.) x _ = x



class OptEq2 a where
  cmp :: a -> a -> a

instance OptEq2 a where
{-@ instance OptEq2 a where
  cmp :: x:a -> y:{a| x == y} -> a
  @-}
  cmp x _ = x


-- This is unsoundly UNSAFE 
unsound x y = x ==. y 
ok      x y = x `cmp` y