content: module Singletons.Classes where
  
  import Data.Eq.Singletons
  import Data.Ord.Singletons
  import Data.Singletons.Base.TH
  import Language.Haskell.TH.Desugar
  import Prelude hiding (const)
  import Singletons.Nat
  
  $(singletons [d|
    const :: a -> b -> a
    const x _ = x
  
    class MyOrd a where
      mycompare :: a -> a -> Ordering
      (<=>) :: a -> a -> Ordering
      (<=>) = mycompare
      infix 4 <=>
  
    instance MyOrd Nat where
      Zero `mycompare` Zero = EQ
      Zero `mycompare` (Succ _) = LT
      (Succ _) `mycompare` Zero = GT
      (Succ n) `mycompare` (Succ m) = m `mycompare` n
  
      -- test eta-expansion
    instance MyOrd () where
      mycompare _ = const EQ
  
    data Foo = A | B
  
    fooCompare :: Foo -> Foo -> Ordering
    fooCompare A A = EQ
    fooCompare A B = LT
    fooCompare B B = GT
    fooCompare B A = EQ
  
    instance MyOrd Foo where
      -- test that values in instance definitions are eta-expanded
      mycompare = fooCompare
  
    data Foo2 = F | G
  
    instance Eq Foo2 where
      F == F = True
      G == G = True
      F == G = False
      G == F = False
   |])
  
  $(promote [d|
    -- instance with overlaping equations. Tests #56
    instance MyOrd Foo2 where
        F `mycompare` F = EQ
        F `mycompare` _ = LT
        _ `mycompare` _ = GT
  
    instance Ord Foo2 where
      F `compare` F = EQ
      F `compare` _ = LT
      _ `compare` _ = GT
  
    |])
  
  -- check promotion across different splices (#55)
  $(singletons [d|
    data Nat' = Zero' | Succ' Nat'
    instance MyOrd Nat' where
      Zero' `mycompare` Zero' = EQ
      Zero' `mycompare` (Succ' _) = LT
      (Succ' _) `mycompare` Zero' = GT
      (Succ' n) `mycompare` (Succ' m) = m `mycompare` n
   |])
  
  foo1a :: Proxy (Zero `Mycompare` (Succ Zero))
  foo1a = Proxy
  
  foo1b :: Proxy LT
  foo1b = foo1a
  
  foo2a :: Proxy (A `Mycompare` A)
  foo2a = Proxy
  
  foo2b :: Proxy EQ
  foo2b = foo2a
  
  foo3a :: Proxy ('() `Mycompare` '())
  foo3a = Proxy
  
  foo3b :: Proxy EQ
  foo3b = foo3a
  
  foo4a :: Proxy (Succ' Zero' <=> Zero')
  foo4a = Proxy
  
  foo4b :: Proxy GT
  foo4b = foo4a
  