content: {-# language DefaultSignatures #-}
  {-# language FlexibleContexts #-}
  {-# language MonoLocalBinds #-}
  {-# language TypeApplications #-}
  
  module Termination.Class
    ( Termination(..)
    , Termination1(..)
    ) where
  
  import Termination.Test
  import Data.Functor.Contravariant.Generic
  import Data.Proxy
  import Numeric.Natural
  
  class Termination a where
    wqo :: Test a
    default wqo :: Deciding Termination a => Test a
    wqo = deciding (Proxy @Termination) wqo
  
  instance Termination ()
  instance Termination a => Termination [a]
  instance Termination a => Termination (Maybe a)
  instance (Termination a, Termination b) => Termination (Either a b)
  instance (Termination a, Termination b) => Termination (a, b)
  instance Termination Int where wqo = ord
  instance Termination Word where wqo = ord
  instance Termination Natural where wqo = ord
  
  class Termination1 f where
    wqo1 :: Test a -> Test (f a)
    default wqo1 :: Deciding1 Termination f => Test a -> Test (f a)
    wqo1 = deciding1 (Proxy @Termination) wqo
  
  instance Termination1 []
  instance Termination1 Maybe
  instance Termination e => Termination1 ((,) e)
  instance Termination e => Termination1 (Either e)
  