    {-|
    Copyright  :  (C) 2015-2016, University of Twente,
                      2017     , QBayLogic B.V.
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
    -}

    {-# LANGUAGE CPP #-}

    module GHC.TypeLits.Extra.Solver.Unify
      ( ExtraDefs (..)
      , UnifyResult (..)
      , NormaliseResult
      , normaliseNat
      , unifyExtra
      )
    where

    -- external
    import Control.Monad.Trans.Class    (lift)
    import Control.Monad.Trans.Maybe    (MaybeT (..))
    import Data.Maybe                   (catMaybes)
    import Data.Function                (on)
    import GHC.TypeLits.Normalise.Unify (CType (..))

    -- GHC API
    #if MIN_VERSION_ghc(9,0,0)
    import GHC.Builtin.Types.Literals (typeNatExpTyCon)
    import GHC.Core.TyCo.Rep (Type (..), TyLit (..))
    import GHC.Core.Type (TyVar, coreView)
    import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)
    import GHC.Tc.Types.Constraint (Ct)
    import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
    import GHC.Utils.Outputable (Outputable (..), ($$), text)
    #else
    import Outputable (Outputable (..), ($$), text)
    import TcPluginM  (TcPluginM, tcPluginTrace)
    import TcTypeNats (typeNatExpTyCon)
    import Type       (TyVar, coreView)
    import TyCoRep    (Type (..), TyLit (..))
    import UniqSet    (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
    #if MIN_VERSION_ghc(8,10,0)
    import Constraint (Ct)
    #else
    import TcRnMonad  (Ct)
    #endif
    #endif

    -- internal
    import GHC.TypeLits.Extra.Solver.Operations

    mergeNormResWith
      :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
      -> MaybeT TcPluginM NormaliseResult
      -> MaybeT TcPluginM NormaliseResult
      -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult
    f MaybeT TcPluginM NormaliseResult
    x MaybeT TcPluginM NormaliseResult
    y = do
      (x', n1) <- MaybeT TcPluginM NormaliseResult
    x
      (y', n2) <- y
      (res, n3) <- f x' y'
      pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3)

    normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    ty | Just Type
    ty1 <- Type -> Maybe Type
    coreView Type
    ty = ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    ty1
    normaliseNat ExtraDefs
    _ (TyVarTy TyVar
    v)          = NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TyVar -> ExtraOp
    V TyVar
    v, Normalised
    Untouched)
    normaliseNat ExtraDefs
    _ (LitTy (NumTyLit Integer
    i)) = NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> ExtraOp
    I Integer
    i, Normalised
    Untouched)
    normaliseNat ExtraDefs
    defs (TyConApp TyCon
    tc [Type
    x,Type
    y])
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    maxTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
    mergeMax ExtraDefs
    defs ExtraOp
    x' ExtraOp
    y'))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    minTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
    mergeMin ExtraDefs
    defs ExtraOp
    x' ExtraOp
    y'))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    divTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> TcPluginM (Maybe NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeDiv ExtraOp
    x' ExtraOp
    y')))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    modTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> TcPluginM (Maybe NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeMod ExtraOp
    x' ExtraOp
    y')))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    flogTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> TcPluginM (Maybe NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeFLog ExtraOp
    x' ExtraOp
    y')))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    clogTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> TcPluginM (Maybe NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeCLog ExtraOp
    x' ExtraOp
    y')))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    logTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> TcPluginM (Maybe NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeLog ExtraOp
    x' ExtraOp
    y')))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    gcdTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> NormaliseResult
    mergeGCD ExtraOp
    x' ExtraOp
    y'))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    lcmTyCon ExtraDefs
    defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> NormaliseResult
    mergeLCM ExtraOp
    x' ExtraOp
    y'))
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                               (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)
      | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    typeNatExpTyCon = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    -> MaybeT TcPluginM NormaliseResult
    mergeNormResWith (\ExtraOp
    x' ExtraOp
    y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> NormaliseResult
    mergeExp ExtraOp
    x' ExtraOp
    y'))
                                                 (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    x)
                                                 (ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs Type
    y)

    normaliseNat ExtraDefs
    defs (TyConApp TyCon
    tc [Type]
    tys) = do
      let mergeExtraOp :: [(Maybe NormaliseResult, Type)] -> [Type]
    mergeExtraOp [] = []
          mergeExtraOp ((Just (ExtraOp
    op, Normalised
    Normalised), Type
    _):[(Maybe NormaliseResult, Type)]
    xs) = ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    opType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[(Maybe NormaliseResult, Type)] -> [Type]
    mergeExtraOp [(Maybe NormaliseResult, Type)]
    xs
          mergeExtraOp ((Maybe NormaliseResult
    _, Type
    ty):[(Maybe NormaliseResult, Type)]
    xs) = Type
    tyType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[(Maybe NormaliseResult, Type)] -> [Type]
    mergeExtraOp [(Maybe NormaliseResult, Type)]
    xs

      normResults <- TcPluginM [Maybe NormaliseResult]
    -> MaybeT TcPluginM [Maybe NormaliseResult]
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ([TcPluginM (Maybe NormaliseResult)]
    -> TcPluginM [Maybe NormaliseResult]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence (MaybeT TcPluginM NormaliseResult
    -> TcPluginM (Maybe NormaliseResult)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT TcPluginM NormaliseResult
     -> TcPluginM (Maybe NormaliseResult))
    -> (Type -> MaybeT TcPluginM NormaliseResult)
    -> Type
    -> TcPluginM (Maybe NormaliseResult)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
    normaliseNat ExtraDefs
    defs (Type -> TcPluginM (Maybe NormaliseResult))
    -> [Type] -> [TcPluginM (Maybe NormaliseResult)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Type]
    tys))
      let anyNormalised = (Normalised -> Normalised -> Normalised)
    -> Normalised -> [Normalised] -> Normalised
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Normalised -> Normalised -> Normalised
    mergeNormalised Normalised
    Untouched (NormaliseResult -> Normalised
    forall a b. (a, b) -> b
    snd (NormaliseResult -> Normalised)
    -> [NormaliseResult] -> [Normalised]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Maybe NormaliseResult] -> [NormaliseResult]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe NormaliseResult]
    normResults)
      let tys' = [(Maybe NormaliseResult, Type)] -> [Type]
    mergeExtraOp ([Maybe NormaliseResult]
    -> [Type] -> [(Maybe NormaliseResult, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Maybe NormaliseResult]
    normResults [Type]
    tys)
      pure (C (CType (TyConApp tc tys')), anyNormalised)

    normaliseNat ExtraDefs
    _ Type
    t = NormaliseResult -> MaybeT TcPluginM NormaliseResult
    forall a. a -> MaybeT TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CType -> ExtraOp
    C (Type -> CType
    CType Type
    t), Normalised
    Untouched)

    -- | Result of comparing two 'SOP' terms, returning a potential substitution
    -- list under which the two terms are equal.
    data UnifyResult
      = Win  -- ^ Two terms are equal
      | Lose -- ^ Two terms are /not/ equal
      | Draw -- ^ We don't know if the two terms are equal

    instance Outputable UnifyResult where
      ppr :: UnifyResult -> SDoc
    ppr UnifyResult
    Win  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Win"
      ppr UnifyResult
    Lose = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Lose"
      ppr UnifyResult
    Draw = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Draw"

    unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
    unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
    unifyExtra Ct
    ct ExtraOp
    u ExtraOp
    v = do
      String -> SDoc -> TcPluginM ()
    tcPluginTrace String
    "unifyExtra" (Ct -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Ct
    ct SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    u SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    v)
      UnifyResult -> TcPluginM UnifyResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtraOp -> ExtraOp -> UnifyResult
    unifyExtra' ExtraOp
    u ExtraOp
    v)

    unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult
    unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult
    unifyExtra' ExtraOp
    u ExtraOp
    v
      | ExtraOp -> ExtraOp -> Bool
    eqFV ExtraOp
    u ExtraOp
    v
      = ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    u ExtraOp
    v
      | Bool
    otherwise
      = UnifyResult
    Draw
      where
        go :: ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    a ExtraOp
    b | ExtraOp
    a ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    b = UnifyResult
    Win
        -- The following operations commute
        go (Max ExtraOp
    a ExtraOp
    b) (Max ExtraOp
    x ExtraOp
    y) = UnifyResult -> UnifyResult -> UnifyResult
    commuteResult (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    a ExtraOp
    y) (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    b ExtraOp
    x)
        go (Min ExtraOp
    a ExtraOp
    b) (Min ExtraOp
    x ExtraOp
    y) = UnifyResult -> UnifyResult -> UnifyResult
    commuteResult (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    a ExtraOp
    y) (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    b ExtraOp
    x)
        go (GCD ExtraOp
    a ExtraOp
    b) (GCD ExtraOp
    x ExtraOp
    y) = UnifyResult -> UnifyResult -> UnifyResult
    commuteResult (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    a ExtraOp
    y) (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    b ExtraOp
    x)
        go (LCM ExtraOp
    a ExtraOp
    b) (LCM ExtraOp
    x ExtraOp
    y) = UnifyResult -> UnifyResult -> UnifyResult
    commuteResult (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    a ExtraOp
    y) (ExtraOp -> ExtraOp -> UnifyResult
    go ExtraOp
    b ExtraOp
    x)
        -- If there are operations contained in the type which this solver does
        -- not understand, then the result is a Draw
        go ExtraOp
    a ExtraOp
    b = if ExtraOp -> Bool
    containsConstants ExtraOp
    a Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    b then UnifyResult
    Draw else UnifyResult
    Lose

        commuteResult :: UnifyResult -> UnifyResult -> UnifyResult
    commuteResult UnifyResult
    Win  UnifyResult
    Win  = UnifyResult
    Win
        commuteResult UnifyResult
    Lose UnifyResult
    _    = UnifyResult
    Lose
        commuteResult UnifyResult
    _    UnifyResult
    Lose = UnifyResult
    Lose
        commuteResult UnifyResult
    _    UnifyResult
    _    = UnifyResult
    Draw

    fvOP :: ExtraOp -> UniqSet TyVar
    fvOP :: ExtraOp -> UniqSet TyVar
    fvOP (I Integer
    _)      = UniqSet TyVar
    forall a. UniqSet a
    emptyUniqSet
    fvOP (V TyVar
    v)      = TyVar -> UniqSet TyVar
    forall a. Uniquable a => a -> UniqSet a
    unitUniqSet TyVar
    v
    fvOP (C CType
    _)      = UniqSet TyVar
    forall a. UniqSet a
    emptyUniqSet
    fvOP (Max ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (Min ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (Div ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (Mod ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (FLog ExtraOp
    x ExtraOp
    y) = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (CLog ExtraOp
    x ExtraOp
    y) = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (Log ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (GCD ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (LCM ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y
    fvOP (Exp ExtraOp
    x ExtraOp
    y)  = ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    x UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` ExtraOp -> UniqSet TyVar
    fvOP ExtraOp
    y

    eqFV :: ExtraOp -> ExtraOp -> Bool
    eqFV :: ExtraOp -> ExtraOp -> Bool
    eqFV = UniqSet TyVar -> UniqSet TyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (UniqSet TyVar -> UniqSet TyVar -> Bool)
    -> (ExtraOp -> UniqSet TyVar) -> ExtraOp -> ExtraOp -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` ExtraOp -> UniqSet TyVar
    fvOP

    containsConstants :: ExtraOp -> Bool
    containsConstants :: ExtraOp -> Bool
    containsConstants (I Integer
    _) = Bool
    False
    containsConstants (V TyVar
    _) = Bool
    False
    containsConstants (C CType
    _) = Bool
    True
    containsConstants (Max ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (Min ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (Div ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (Mod ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (FLog ExtraOp
    x ExtraOp
    y) = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (CLog ExtraOp
    x ExtraOp
    y) = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (Log ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (GCD ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (LCM ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y
    containsConstants (Exp ExtraOp
    x ExtraOp
    y)  = ExtraOp -> Bool
    containsConstants ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp -> Bool
    containsConstants ExtraOp
    y