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

    To use the plugin, add the

    @
    {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
    @

    pragma to the header of your file

    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE TemplateHaskellQuotes #-}

    {-# OPTIONS_HADDOCK show-extensions #-}

    module GHC.TypeLits.Extra.Solver
      ( plugin )
    where

    -- external
    import Control.Monad.Trans.Maybe (MaybeT (..))
    import Data.Maybe (catMaybes)
    import GHC.TcPluginM.Extra (evByFiat, tracePlugin, newWanted)
    import qualified Data.Type.Ord
    import qualified GHC.TypeError

    -- GHC API
    import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique)
    import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)
    import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon)
    import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon)
    import GHC.Core.Coercion (mkUnivCo)
    import GHC.Core.DataCon (dataConWrapId)
    import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType)
    import GHC.Core.Reduction (Reduction(..))
    import GHC.Core.TyCon (TyCon)
    import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))
    import GHC.Core.Type (Kind, mkTyConApp, splitTyConApp_maybe, typeKind)
    #if MIN_VERSION_ghc(9,6,0)
    import GHC.Core.TyCo.Compare (eqType)
    #else
    import GHC.Core.Type (eqType)
    #endif
    import GHC.Data.IOEnv (getEnv)
    import GHC.Driver.Env (hsc_NC)
    import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
    import GHC.Plugins (thNameToGhcNameIO)
    import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM)
    import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..), Env (env_top))
    import GHC.Tc.Types.Constraint
      (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt)
    #if MIN_VERSION_ghc(9,8,0)
    import GHC.Tc.Types.Constraint (Ct (..), DictCt(..), EqCt(..), IrredCt(..), qci_ev)
    #else
    import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev, cc_ev)
    #endif
    import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId)
    import GHC.Types.Unique.FM (UniqFM, listToUFM)
    import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
    import GHC (Name)

    -- template-haskell
    import qualified Language.Haskell.TH as TH

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

    -- | A solver implement as a type-checker plugin for:
    --
    --     * 'Div': type-level 'div'
    --
    --     * 'Mod': type-level 'mod'
    --
    --     * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
    --       .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
    --
    --     * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
    --       .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"
    --
    --     * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
    --        where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"
    --
    --     * 'GCD': a type-level 'gcd'
    --
    --     * 'LCM': a type-level 'lcm'
    --
    -- To use the plugin, add
    --
    -- @
    -- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
    -- @
    --
    -- To the header of your file.
    plugin :: Plugin
    plugin :: Plugin
    plugin
      = Plugin
    defaultPlugin
      { tcPlugin = const $ Just normalisePlugin
      , pluginRecompile = purePlugin
      }

    normalisePlugin :: TcPlugin
    normalisePlugin :: TcPlugin
    normalisePlugin = CommandLineOption -> TcPlugin -> TcPlugin
    tracePlugin CommandLineOption
    "ghc-typelits-extra"
      TcPlugin { tcPluginInit :: TcPluginM ExtraDefs
    tcPluginInit    = TcPluginM ExtraDefs
    lookupExtraDefs
               , tcPluginSolve :: ExtraDefs -> TcPluginSolver
    tcPluginSolve   = ExtraDefs -> TcPluginSolver
    decideEqualSOP
               , tcPluginRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
    tcPluginRewrite = ExtraDefs -> UniqFM TyCon TcPluginRewriter
    extraRewrite
               , tcPluginStop :: ExtraDefs -> TcPluginM ()
    tcPluginStop    = TcPluginM () -> ExtraDefs -> TcPluginM ()
    forall a b. a -> b -> a
    const (() -> TcPluginM ()
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
               }

    extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
    extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
    extraRewrite ExtraDefs
    defs = [(TyCon, TcPluginRewriter)] -> UniqFM TyCon TcPluginRewriter
    forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
    listToUFM
      [ (ExtraDefs -> TyCon
    gcdTyCon ExtraDefs
    defs, TcPluginRewriter
    forall {f :: * -> *} {p} {p}.
    Applicative f =>
    p -> p -> [Type] -> f TcPluginRewriteResult
    gcdRewrite)
      , (ExtraDefs -> TyCon
    lcmTyCon ExtraDefs
    defs, TcPluginRewriter
    forall {f :: * -> *} {p} {p}.
    Applicative f =>
    p -> p -> [Type] -> f TcPluginRewriteResult
    lcmRewrite)
      ]
      where
        gcdRewrite :: p -> p -> [Type] -> f TcPluginRewriteResult
    gcdRewrite p
    _ p
    _ args :: [Type]
    args@[LitTy (NumTyLit Integer
    i), LitTy (NumTyLit Integer
    j)] = TcPluginRewriteResult -> f TcPluginRewriteResult
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TcPluginRewriteResult -> f TcPluginRewriteResult)
    -> TcPluginRewriteResult -> f TcPluginRewriteResult
    forall a b. (a -> b) -> a -> b
    $
          Reduction -> [Ct] -> TcPluginRewriteResult
    TcPluginRewriteTo (TyCon -> [Type] -> Type -> Reduction
    reduce (ExtraDefs -> TyCon
    gcdTyCon ExtraDefs
    defs) [Type]
    args (TyLit -> Type
    LitTy (Integer -> TyLit
    NumTyLit (Integer
    i Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `gcd` Integer
    j)))) []
        gcdRewrite p
    _ p
    _ [Type]
    _ = TcPluginRewriteResult -> f TcPluginRewriteResult
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TcPluginRewriteResult
    TcPluginNoRewrite

        lcmRewrite :: p -> p -> [Type] -> f TcPluginRewriteResult
    lcmRewrite p
    _ p
    _ args :: [Type]
    args@[LitTy (NumTyLit Integer
    i), LitTy (NumTyLit Integer
    j)] = TcPluginRewriteResult -> f TcPluginRewriteResult
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TcPluginRewriteResult -> f TcPluginRewriteResult)
    -> TcPluginRewriteResult -> f TcPluginRewriteResult
    forall a b. (a -> b) -> a -> b
    $
          Reduction -> [Ct] -> TcPluginRewriteResult
    TcPluginRewriteTo (TyCon -> [Type] -> Type -> Reduction
    reduce (ExtraDefs -> TyCon
    lcmTyCon ExtraDefs
    defs) [Type]
    args (TyLit -> Type
    LitTy (Integer -> TyLit
    NumTyLit (Integer
    i Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `lcm` Integer
    j)))) []
        lcmRewrite p
    _ p
    _ [Type]
    _ = TcPluginRewriteResult -> f TcPluginRewriteResult
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TcPluginRewriteResult
    TcPluginNoRewrite

        reduce :: TyCon -> [Type] -> Type -> Reduction
    reduce TyCon
    tc [Type]
    args Type
    res = Coercion -> Type -> Reduction
    Reduction Coercion
    co Type
    res
         where
          co :: Coercion
    co = UnivCoProvenance -> Role -> Type -> Type -> Coercion
    mkUnivCo (CommandLineOption -> UnivCoProvenance
    PluginProv CommandLineOption
    "ghc-typelits-extra") Role
    Nominal
                 (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc [Type]
    args) Type
    res

    decideEqualSOP :: ExtraDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
    decideEqualSOP :: ExtraDefs -> TcPluginSolver
    decideEqualSOP ExtraDefs
    _    EvBindsVar
    _ [Ct]
    _givens []      = TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
    TcPluginOk [] [])
    decideEqualSOP ExtraDefs
    defs EvBindsVar
    _ [Ct]
    givens  [Ct]
    wanteds = do
      unit_wanteds <- [Maybe SolverConstraint] -> [SolverConstraint]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe SolverConstraint] -> [SolverConstraint])
    -> TcPluginM [Maybe SolverConstraint]
    -> TcPluginM [SolverConstraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Ct -> TcPluginM (Maybe SolverConstraint))
    -> [Ct] -> TcPluginM [Maybe SolverConstraint]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (MaybeT TcPluginM SolverConstraint
    -> TcPluginM (Maybe SolverConstraint)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT TcPluginM SolverConstraint
     -> TcPluginM (Maybe SolverConstraint))
    -> (Ct -> MaybeT TcPluginM SolverConstraint)
    -> Ct
    -> TcPluginM (Maybe SolverConstraint)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint
    toSolverConstraint ExtraDefs
    defs) [Ct]
    wanteds
      case unit_wanteds of
        [] -> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
    TcPluginOk [] [])
        [SolverConstraint]
    _  -> do
          unit_givens <- [Maybe SolverConstraint] -> [SolverConstraint]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe SolverConstraint] -> [SolverConstraint])
    -> TcPluginM [Maybe SolverConstraint]
    -> TcPluginM [SolverConstraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Ct -> TcPluginM (Maybe SolverConstraint))
    -> [Ct] -> TcPluginM [Maybe SolverConstraint]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (MaybeT TcPluginM SolverConstraint
    -> TcPluginM (Maybe SolverConstraint)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT TcPluginM SolverConstraint
     -> TcPluginM (Maybe SolverConstraint))
    -> (Ct -> MaybeT TcPluginM SolverConstraint)
    -> Ct
    -> TcPluginM (Maybe SolverConstraint)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint
    toSolverConstraint ExtraDefs
    defs) [Ct]
    givens
          sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)
          tcPluginTrace "normalised" (ppr sr)
          case sr of
            Simplified [(EvTerm, Ct)]
    evs [Ct]
    new -> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
    TcPluginOk (((EvTerm, Ct) -> Bool) -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Ct -> Bool
    isWantedCt (Ct -> Bool) -> ((EvTerm, Ct) -> Ct) -> (EvTerm, Ct) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (EvTerm, Ct) -> Ct
    forall a b. (a, b) -> b
    snd) [(EvTerm, Ct)]
    evs) [Ct]
    new)
            Impossible SolverConstraint
    eq  -> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Ct] -> TcPluginSolveResult
    TcPluginContradiction [SolverConstraint -> Ct
    fromSolverConstraint SolverConstraint
    eq])

    data SolverConstraint
       = NatEquality Ct ExtraOp ExtraOp Normalised
       | NatInequality Ct ExtraOp ExtraOp Bool Normalised

    instance Outputable SolverConstraint where
      ppr :: SolverConstraint -> SDoc
    ppr (NatEquality Ct
    ct ExtraOp
    op1 ExtraOp
    op2 Normalised
    norm) = CommandLineOption -> SDoc
    forall doc. IsLine doc => CommandLineOption -> doc
    text CommandLineOption
    "NatEquality" SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ 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
    op1 SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    op2 SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Normalised -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Normalised
    norm
      ppr (NatInequality Ct
    _ ExtraOp
    op1 ExtraOp
    op2 Bool
    b Normalised
    norm) = CommandLineOption -> SDoc
    forall doc. IsLine doc => CommandLineOption -> doc
    text CommandLineOption
    "NatInequality" SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    op1 SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    op2 SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Bool -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Bool
    b SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Normalised -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Normalised
    norm

    data SimplifyResult
      = Simplified [(EvTerm,Ct)] [Ct]
      | Impossible SolverConstraint

    instance Outputable SimplifyResult where
      ppr :: SimplifyResult -> SDoc
    ppr (Simplified [(EvTerm, Ct)]
    evs [Ct]
    new) = CommandLineOption -> SDoc
    forall doc. IsLine doc => CommandLineOption -> doc
    text CommandLineOption
    "Simplified" SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ CommandLineOption -> SDoc
    forall doc. IsLine doc => CommandLineOption -> doc
    text CommandLineOption
    "Solved:" SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ [(EvTerm, Ct)] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [(EvTerm, Ct)]
    evs SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ CommandLineOption -> SDoc
    forall doc. IsLine doc => CommandLineOption -> doc
    text CommandLineOption
    "New:" SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ [Ct] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Ct]
    new
      ppr (Impossible SolverConstraint
    sct)  = CommandLineOption -> SDoc
    forall doc. IsLine doc => CommandLineOption -> doc
    text CommandLineOption
    "Impossible" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SolverConstraint -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr SolverConstraint
    sct

    simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult
    simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult
    simplifyExtra ExtraDefs
    defs [SolverConstraint]
    eqs = CommandLineOption -> SDoc -> TcPluginM ()
    tcPluginTrace CommandLineOption
    "simplifyExtra" ([SolverConstraint] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [SolverConstraint]
    eqs) TcPluginM ()
    -> TcPluginM SimplifyResult -> TcPluginM SimplifyResult
    forall a b. TcPluginM a -> TcPluginM b -> TcPluginM b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [] [] [SolverConstraint]
    eqs
      where
        simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
        simples :: [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news [] = SimplifyResult -> TcPluginM SimplifyResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> SimplifyResult
    Simplified ([Maybe (EvTerm, Ct)] -> [(EvTerm, Ct)]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe (EvTerm, Ct)]
    evs) [Ct]
    news)
        simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news (eq :: SolverConstraint
    eq@(NatEquality Ct
    ct ExtraOp
    u ExtraOp
    v Normalised
    norm):[SolverConstraint]
    eqs') = do
          ur <- Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
    unifyExtra Ct
    ct ExtraOp
    u ExtraOp
    v
          tcPluginTrace "unifyExtra result" (ppr ur)
          case ur of
            UnifyResult
    Win                          -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples (((,) (EvTerm -> Ct -> (EvTerm, Ct))
    -> Maybe EvTerm -> Maybe (Ct -> (EvTerm, Ct))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Ct -> Maybe EvTerm
    evMagic Ct
    ct Maybe (Ct -> (EvTerm, Ct)) -> Maybe Ct -> Maybe (EvTerm, Ct)
    forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Ct -> Maybe Ct
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ct
    ct)Maybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
    forall a. a -> [a] -> [a]
    :[Maybe (EvTerm, Ct)]
    evs) [Ct]
    news [SolverConstraint]
    eqs'
            UnifyResult
    Lose | [Maybe (EvTerm, Ct)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Maybe (EvTerm, Ct)]
    evs Bool -> Bool -> Bool
    && [SolverConstraint] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SolverConstraint]
    eqs' -> SimplifyResult -> TcPluginM SimplifyResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SolverConstraint -> SimplifyResult
    Impossible SolverConstraint
    eq)
            UnifyResult
    _ | Normalised
    norm Normalised -> Normalised -> Bool
    forall a. Eq a => a -> a -> Bool
    == Normalised
    Normalised Bool -> Bool -> Bool
    && Ct -> Bool
    isWantedCt Ct
    ct -> do
              newCt <- ExtraDefs -> SolverConstraint -> TcPluginM Ct
    createWantedFromNormalised ExtraDefs
    defs SolverConstraint
    eq
              simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'
            UnifyResult
    Lose -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news [SolverConstraint]
    eqs'
            UnifyResult
    Draw -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news [SolverConstraint]
    eqs'
        simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news (eq :: SolverConstraint
    eq@(NatInequality Ct
    ct ExtraOp
    u ExtraOp
    v Bool
    b Normalised
    norm):[SolverConstraint]
    eqs') = do
          CommandLineOption -> SDoc -> TcPluginM ()
    tcPluginTrace CommandLineOption
    "unifyExtra leq result" ((ExtraOp, ExtraOp, Bool) -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (ExtraOp
    u,ExtraOp
    v,Bool
    b))
          case (ExtraOp
    u,ExtraOp
    v) of
            (I Integer
    i,I Integer
    j)
              | (Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    j) Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    b -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples (((,) (EvTerm -> Ct -> (EvTerm, Ct))
    -> Maybe EvTerm -> Maybe (Ct -> (EvTerm, Ct))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Ct -> Maybe EvTerm
    evMagic Ct
    ct Maybe (Ct -> (EvTerm, Ct)) -> Maybe Ct -> Maybe (EvTerm, Ct)
    forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Ct -> Maybe Ct
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ct
    ct)Maybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
    forall a. a -> [a] -> [a]
    :[Maybe (EvTerm, Ct)]
    evs) [Ct]
    news [SolverConstraint]
    eqs'
              | Bool
    otherwise     -> SimplifyResult -> TcPluginM SimplifyResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return  (SolverConstraint -> SimplifyResult
    Impossible SolverConstraint
    eq)
            (ExtraOp
    p, Max ExtraOp
    x ExtraOp
    y)
              | Bool
    b Bool -> Bool -> Bool
    && (ExtraOp
    p ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    x Bool -> Bool -> Bool
    || ExtraOp
    p ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    y) -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples (((,) (EvTerm -> Ct -> (EvTerm, Ct))
    -> Maybe EvTerm -> Maybe (Ct -> (EvTerm, Ct))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Ct -> Maybe EvTerm
    evMagic Ct
    ct Maybe (Ct -> (EvTerm, Ct)) -> Maybe Ct -> Maybe (EvTerm, Ct)
    forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Ct -> Maybe Ct
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ct
    ct)Maybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
    forall a. a -> [a] -> [a]
    :[Maybe (EvTerm, Ct)]
    evs) [Ct]
    news [SolverConstraint]
    eqs'

            -- transform:  q ~ Max x y => (p <=? q ~ True)
            -- to:         (p <=? Max x y) ~ True
            -- and try to solve that along with the rest of the eqs'
            (ExtraOp
    p, q :: ExtraOp
    q@(V TyVar
    _))
              | Bool
    b -> case ExtraOp -> [SolverConstraint] -> Maybe ExtraOp
    findMax ExtraOp
    q [SolverConstraint]
    eqs of
                       Just ExtraOp
    m  -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news (Ct -> ExtraOp -> ExtraOp -> Bool -> Normalised -> SolverConstraint
    NatInequality Ct
    ct ExtraOp
    p ExtraOp
    m Bool
    b Normalised
    normSolverConstraint -> [SolverConstraint] -> [SolverConstraint]
    forall a. a -> [a] -> [a]
    :[SolverConstraint]
    eqs')
                       Maybe ExtraOp
    Nothing -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news [SolverConstraint]
    eqs'
            (ExtraOp, ExtraOp)
    _ | Normalised
    norm Normalised -> Normalised -> Bool
    forall a. Eq a => a -> a -> Bool
    == Normalised
    Normalised Bool -> Bool -> Bool
    && Ct -> Bool
    isWantedCt Ct
    ct -> do
              newCt <- ExtraDefs -> SolverConstraint -> TcPluginM Ct
    createWantedFromNormalised ExtraDefs
    defs SolverConstraint
    eq
              simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'
            (ExtraOp, ExtraOp)
    _ -> [Maybe (EvTerm, Ct)]
    -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult
    simples [Maybe (EvTerm, Ct)]
    evs [Ct]
    news [SolverConstraint]
    eqs'

        -- look for given constraint with the form: c ~ Max x y
        findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp
        findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp
    findMax ExtraOp
    c = [SolverConstraint] -> Maybe ExtraOp
    go
          where
            go :: [SolverConstraint] -> Maybe ExtraOp
    go [] = Maybe ExtraOp
    forall a. Maybe a
    Nothing
            go ((NatEquality Ct
    ct ExtraOp
    a b :: ExtraOp
    b@(Max ExtraOp
    _ ExtraOp
    _) Normalised
    _) :[SolverConstraint]
    _)
              | ExtraOp
    c ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    a Bool -> Bool -> Bool
    && Bool -> Bool
    not (Ct -> Bool
    isWantedCt Ct
    ct)
                = ExtraOp -> Maybe ExtraOp
    forall a. a -> Maybe a
    Just ExtraOp
    b
            go ((NatEquality Ct
    ct a :: ExtraOp
    a@(Max ExtraOp
    _ ExtraOp
    _) ExtraOp
    b Normalised
    _) :[SolverConstraint]
    _)
              | ExtraOp
    c ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    b Bool -> Bool -> Bool
    && Bool -> Bool
    not (Ct -> Bool
    isWantedCt Ct
    ct)
                = ExtraOp -> Maybe ExtraOp
    forall a. a -> Maybe a
    Just ExtraOp
    a
            go (SolverConstraint
    _:[SolverConstraint]
    rest) = [SolverConstraint] -> Maybe ExtraOp
    go [SolverConstraint]
    rest

    -- Extract the Nat equality constraints
    toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint
    toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint
    toSolverConstraint ExtraDefs
    defs Ct
    ct = case Type -> Pred
    classifyPredType (Type -> Pred) -> Type -> Pred
    forall a b. (a -> b) -> a -> b
    $ CtEvidence -> Type
    ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
    forall a b. (a -> b) -> a -> b
    $ Ct -> CtEvidence
    ctEvidence Ct
    ct of
        EqPred EqRel
    NomEq Type
    t1 Type
    t2
          | Type -> Bool
    isNatKind (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    t1) Bool -> Bool -> Bool
    || Type -> Bool
    isNatKind (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    t2)
          -> do
             (t1', n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
    normaliseNat ExtraDefs
    defs Type
    t1
             (t2', n2) <- normaliseNat defs t2
             pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))
          | TyConApp TyCon
    tc [Type
    _,Type
    cmpNat,TyConApp TyCon
    tt1 [],TyConApp TyCon
    tt2 [],TyConApp TyCon
    ff1 []] <- Type
    t1
          , TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    ordTyCon ExtraDefs
    defs
          , TyConApp TyCon
    cmpNatTc [Type
    x,Type
    y] <- Type
    cmpNat
          , TyCon
    cmpNatTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    typeNatCmpTyCon
          , TyCon
    tt1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
          , TyCon
    tt2 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
          , TyCon
    ff1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedFalseDataCon
          , TyConApp TyCon
    tc' [] <- Type
    t2
          -> do
              (x', n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
    normaliseNat ExtraDefs
    defs Type
    x
              (y', n2) <- normaliseNat defs y
              let res | TyCon
    tc' TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon  = SolverConstraint -> MaybeT TcPluginM SolverConstraint
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Ct -> ExtraOp -> ExtraOp -> Bool -> Normalised -> SolverConstraint
    NatInequality Ct
    ct ExtraOp
    x' ExtraOp
    y' Bool
    True  (Normalised -> Normalised -> Normalised
    mergeNormalised Normalised
    n1 Normalised
    n2))
                      | TyCon
    tc' TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedFalseDataCon = SolverConstraint -> MaybeT TcPluginM SolverConstraint
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Ct -> ExtraOp -> ExtraOp -> Bool -> Normalised -> SolverConstraint
    NatInequality Ct
    ct ExtraOp
    x' ExtraOp
    y' Bool
    False (Normalised -> Normalised -> Normalised
    mergeNormalised Normalised
    n1 Normalised
    n2))
                      | Bool
    otherwise                   = CommandLineOption -> MaybeT TcPluginM SolverConstraint
    forall a. CommandLineOption -> MaybeT TcPluginM a
    forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
    fail CommandLineOption
    "Nothing"
              res
          | TyConApp TyCon
    tc [TyConApp TyCon
    ordCondTc [Type]
    zs, Type
    _] <- Type
    t1
          , TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    assertTC ExtraDefs
    defs
          , TyConApp TyCon
    tc' [] <- Type
    t2
          , TyCon
    tc' TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == Arity -> TyCon
    cTupleTyCon Arity
    0
          , TyCon
    ordCondTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    ordTyCon ExtraDefs
    defs
          , [Type
    _,Type
    cmp,Type
    lt,Type
    eq,Type
    gt] <- [Type]
    zs
          , TyConApp TyCon
    tcCmpNat [Type
    x,Type
    y] <- Type
    cmp
          , TyCon
    tcCmpNat TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    typeNatCmpTyCon
          , TyConApp TyCon
    ltTc [] <- Type
    lt
          , TyCon
    ltTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
          , TyConApp TyCon
    eqTc [] <- Type
    eq
          , TyCon
    eqTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
          , TyConApp TyCon
    gtTc [] <- Type
    gt
          , TyCon
    gtTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedFalseDataCon
          -> do
              (x', n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
    normaliseNat ExtraDefs
    defs Type
    x
              (y', n2) <- normaliseNat defs y
              pure (NatInequality ct x' y' True  (mergeNormalised n1 n2))
        IrredPred (TyConApp TyCon
    tc [TyConApp TyCon
    ordCondTc [Type]
    zs, Type
    _])
          | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    assertTC ExtraDefs
    defs
          , TyCon
    ordCondTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraDefs -> TyCon
    ordTyCon ExtraDefs
    defs
          , [Type
    _,Type
    cmp,Type
    lt,Type
    eq,Type
    gt] <- [Type]
    zs
          , TyConApp TyCon
    tcCmpNat [Type
    x,Type
    y] <- Type
    cmp
          , TyCon
    tcCmpNat TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    typeNatCmpTyCon
          , TyConApp TyCon
    ltTc [] <- Type
    lt
          , TyCon
    ltTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
          , TyConApp TyCon
    eqTc [] <- Type
    eq
          , TyCon
    eqTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
          , TyConApp TyCon
    gtTc [] <- Type
    gt
          , TyCon
    gtTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedFalseDataCon
          -> do
              (x', n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
    normaliseNat ExtraDefs
    defs Type
    x
              (y', n2) <- normaliseNat defs y
              pure (NatInequality ct x' y' True  (mergeNormalised n1 n2))
        Pred
    _ -> CommandLineOption -> MaybeT TcPluginM SolverConstraint
    forall a. CommandLineOption -> MaybeT TcPluginM a
    forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
    fail CommandLineOption
    "Nothing"
      where
        isNatKind :: Kind -> Bool
        isNatKind :: Type -> Bool
    isNatKind = (Type -> Type -> Bool
    `eqType` Type
    naturalTy)

    createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct
    createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct
    createWantedFromNormalised ExtraDefs
    defs SolverConstraint
    sct = do
      let extractCtSides :: SolverConstraint -> (Ct, Type, Type)
    extractCtSides (NatEquality Ct
    ct ExtraOp
    t1 ExtraOp
    t2 Normalised
    _)   = (Ct
    ct, ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    t1, ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    t2)
          extractCtSides (NatInequality Ct
    ct ExtraOp
    x ExtraOp
    y Bool
    b Normalised
    _) =
            let tc :: TyCon
    tc = if Bool
    b then TyCon
    promotedTrueDataCon else TyCon
    promotedFalseDataCon
                t1 :: Type
    t1 = TyCon -> [Type] -> Type
    TyConApp (ExtraDefs -> TyCon
    ordTyCon ExtraDefs
    defs)
                        [ Type
    boolTy
                        , TyCon -> [Type] -> Type
    TyConApp TyCon
    typeNatCmpTyCon [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x, ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
                        , TyCon -> [Type] -> Type
    TyConApp TyCon
    promotedTrueDataCon []
                        , TyCon -> [Type] -> Type
    TyConApp TyCon
    promotedTrueDataCon []
                        , TyCon -> [Type] -> Type
    TyConApp TyCon
    promotedFalseDataCon []
                        ]
                t2 :: Type
    t2 = TyCon -> [Type] -> Type
    TyConApp TyCon
    tc []
              in (Ct
    ct, Type
    t1, Type
    t2)
      let (Ct
    ct, Type
    t1, Type
    t2) = SolverConstraint -> (Ct, Type, Type)
    extractCtSides SolverConstraint
    sct
      newPredTy <- case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
    forall a b. (a -> b) -> a -> b
    $ CtEvidence -> Type
    ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
    forall a b. (a -> b) -> a -> b
    $ Ct -> CtEvidence
    ctEvidence Ct
    ct of
        Just (TyCon
    tc, [Type
    a, Type
    b, Type
    _, Type
    _]) | TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqPrimTyConKey -> Type -> TcPluginM Type
    forall a. a -> TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc [Type
    a, Type
    b, Type
    t1, Type
    t2])
        Just (TyCon
    tc, [Type
    _, Type
    b]) | TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` TyCon -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique (ExtraDefs -> TyCon
    assertTC ExtraDefs
    defs) -> Type -> TcPluginM Type
    forall a. a -> TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc [Type
    t1,Type
    b])
        Maybe (TyCon, [Type])
    _ -> CommandLineOption -> TcPluginM Type
    forall a. HasCallStack => CommandLineOption -> a
    error CommandLineOption
    "Impossible: neither (<=?) nor Assert"
      ev <- newWanted (ctLoc ct) newPredTy
      let ctN = case Ct
    ct of
                  CQuantCan QCInst
    qc -> QCInst -> Ct
    CQuantCan (QCInst
    qc { qci_ev = ev})
    #if MIN_VERSION_ghc(9,8,0)
                  CDictCan DictCt
    di     -> DictCt -> Ct
    CDictCan (DictCt
    di { di_ev = ev})
                  CIrredCan IrredCt
    ir    -> IrredCt -> Ct
    CIrredCan (IrredCt
    ir { ir_ev = ev})
                  CEqCan EqCt
    eq       -> EqCt -> Ct
    CEqCan (EqCt
    eq { eq_ev = ev})
                  CNonCanonical CtEvidence
    _ -> CtEvidence -> Ct
    CNonCanonical CtEvidence
    ev
    #else
                  ctX -> ctX { cc_ev = ev }
    #endif
      return ctN

    fromSolverConstraint :: SolverConstraint -> Ct
    fromSolverConstraint :: SolverConstraint -> Ct
    fromSolverConstraint (NatEquality Ct
    ct ExtraOp
    _ ExtraOp
    _ Normalised
    _)  = Ct
    ct
    fromSolverConstraint (NatInequality Ct
    ct ExtraOp
    _ ExtraOp
    _ Bool
    _ Normalised
    _) = Ct
    ct

    lookupExtraDefs :: TcPluginM ExtraDefs
    lookupExtraDefs :: TcPluginM ExtraDefs
    lookupExtraDefs = do
        TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> TyCon
    -> ExtraDefs
    ExtraDefs (TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> TyCon
     -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM
         (TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> ExtraDefs)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.Max
                  TcPluginM
      (TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM
         (TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.Min
                  TcPluginM
      (TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM
         (TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> TyCon
          -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TyCon -> TcPluginM TyCon
    forall a. a -> TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TyCon
    typeNatDivTyCon
                  TcPluginM
      (TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> TyCon
       -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM
         (TyCon
          -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TyCon -> TcPluginM TyCon
    forall a. a -> TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TyCon
    typeNatModTyCon
                  TcPluginM
      (TyCon
       -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM
         (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.FLog
                  TcPluginM
      (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM
         (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.CLog
                  TcPluginM (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM (TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.Log
                  TcPluginM (TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
    -> TcPluginM TyCon
    -> TcPluginM (TyCon -> TyCon -> TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.GCD
                  TcPluginM (TyCon -> TyCon -> TyCon -> ExtraDefs)
    -> TcPluginM TyCon -> TcPluginM (TyCon -> TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeLits.Extra.LCM
                  TcPluginM (TyCon -> TyCon -> ExtraDefs)
    -> TcPluginM TyCon -> TcPluginM (TyCon -> ExtraDefs)
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''Data.Type.Ord.OrdCond
                  TcPluginM (TyCon -> ExtraDefs)
    -> TcPluginM TyCon -> TcPluginM ExtraDefs
    forall a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Name -> TcPluginM TyCon
    look ''GHC.TypeError.Assert
      where
        look :: Name -> TcPluginM TyCon
    look Name
    nm = Name -> TcPluginM TyCon
    tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Name -> TcPluginM Name
    lookupTHName Name
    nm

    lookupTHName :: TH.Name -> TcPluginM Name
    lookupTHName :: Name -> TcPluginM Name
    lookupTHName Name
    th = do
        nc <- TcM NameCache -> TcPluginM NameCache
    forall a. TcM a -> TcPluginM a
    unsafeTcPluginTcM (HscEnv -> NameCache
    hsc_NC (HscEnv -> NameCache)
    -> (Env TcGblEnv TcLclEnv -> HscEnv)
    -> Env TcGblEnv TcLclEnv
    -> NameCache
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Env TcGblEnv TcLclEnv -> HscEnv
    forall gbl lcl. Env gbl lcl -> HscEnv
    env_top (Env TcGblEnv TcLclEnv -> NameCache)
    -> IOEnv (Env TcGblEnv TcLclEnv) (Env TcGblEnv TcLclEnv)
    -> TcM NameCache
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IOEnv (Env TcGblEnv TcLclEnv) (Env TcGblEnv TcLclEnv)
    forall env. IOEnv env env
    getEnv)
        res <- tcPluginIO $ thNameToGhcNameIO nc th
        maybe (fail $ "Failed to lookup " ++ show th) return res

    -- Utils
    evMagic :: Ct -> Maybe EvTerm
    evMagic :: Ct -> Maybe EvTerm
    evMagic Ct
    ct = case Type -> Pred
    classifyPredType (Type -> Pred) -> Type -> Pred
    forall a b. (a -> b) -> a -> b
    $ CtEvidence -> Type
    ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
    forall a b. (a -> b) -> a -> b
    $ Ct -> CtEvidence
    ctEvidence Ct
    ct of
        EqPred EqRel
    NomEq Type
    t1 Type
    t2 -> EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just (CommandLineOption -> Type -> Type -> EvTerm
    evByFiat CommandLineOption
    "ghc-typelits-extra" Type
    t1 Type
    t2)
        IrredPred Type
    p ->
          let t1 :: Type
    t1 = TyCon -> [Type] -> Type
    mkTyConApp (Arity -> TyCon
    cTupleTyCon Arity
    0) []
              co :: Coercion
    co = UnivCoProvenance -> Role -> Type -> Type -> Coercion
    mkUnivCo (CommandLineOption -> UnivCoProvenance
    PluginProv CommandLineOption
    "ghc-typelits-extra") Role
    Representational Type
    t1 Type
    p
              dcApp :: EvExpr
    dcApp = TyVar -> EvExpr
    evId (DataCon -> TyVar
    dataConWrapId (Arity -> DataCon
    cTupleDataCon Arity
    0))
           in EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just (EvExpr -> Coercion -> EvTerm
    evCast EvExpr
    dcApp Coercion
    co)
        Pred
    _ -> Maybe EvTerm
    forall a. Maybe a
    Nothing