    module Agda.TypeChecking.SizedTypes.Utils where

    import Data.IORef
    import qualified Debug.Trace as Debug
    import System.IO.Unsafe

    import Agda.Utils.Function

    {-# NOINLINE debug #-}
    debug :: IORef Bool
    debug :: IORef Bool
    debug = IO (IORef Bool) -> IORef Bool
    forall a. IO a -> a
    unsafePerformIO (IO (IORef Bool) -> IORef Bool) -> IO (IORef Bool) -> IORef Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO (IORef Bool)
    forall a. a -> IO (IORef a)
    newIORef Bool
    False

    setDebugging :: Bool -> IO ()
    setDebugging :: Bool -> IO ()
    setDebugging = IORef Bool -> Bool -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef Bool
    debug

    trace :: String -> a -> a
    trace :: forall a. String -> a -> a
    trace String
    s = Bool -> (a -> a) -> a -> a
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (IO Bool -> Bool
    forall a. IO a -> a
    unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ IORef Bool -> IO Bool
    forall a. IORef a -> IO a
    readIORef IORef Bool
    debug) ((a -> a) -> a -> a) -> (a -> a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ String -> a -> a
    forall a. String -> a -> a
    Debug.trace String
    s

    traceM :: Applicative f => String -> f ()
    traceM :: forall (f :: * -> *). Applicative f => String -> f ()
    traceM String
    s = String -> f () -> f ()
    forall a. String -> a -> a
    trace String
    s (f () -> f ()) -> f () -> f ()
    forall a b. (a -> b) -> a -> b
    $ () -> f ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    class Eq a => Top a where
      top   :: a
      isTop :: a -> Bool
      isTop = (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    ==a
    forall a. Top a => a
    top)

    class Plus a b c where
      plus :: a -> b -> c

    instance Plus Int Int Int where
      plus :: Int -> Int -> Int
    plus = Int -> Int -> Int
    forall a. Num a => a -> a -> a
    (+)

    class MeetSemiLattice a where
      meet :: a -> a -> a

    -- | Semiring with idempotent '+' == dioid
    class (MeetSemiLattice a, Top a) => Dioid a where
      compose     :: a -> a -> a  -- ^ E.g. +
      unitCompose :: a            -- ^ neutral element of @compose@, e.g. zero