data Bool = tt | ff

f (b:: Bool)
  :: Bool
  = case b of {
      (tt) -> ff;
      (ff) -> tt;}


test :: Type
     = {!f tt  !}


data False = 

g (x:: False)
  :: Bool
  = case x of { }