{-|
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
  [SolverConstraint]
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 [SolverConstraint]
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
      [SolverConstraint]
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
      SimplifyResult
sr <- ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult
simplifyExtra ExtraDefs
defs ([SolverConstraint]
unit_givens [SolverConstraint] -> [SolverConstraint] -> [SolverConstraint]
forall a. [a] -> [a] -> [a]
++ [SolverConstraint]
unit_wanteds)
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
      case SimplifyResult
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
      UnifyResult
ur <- Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
unifyExtra Ct
ct ExtraOp
u ExtraOp
v
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"unifyExtra result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      case UnifyResult
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
          Ct
newCt <- ExtraDefs -> SolverConstraint -> TcPluginM Ct
createWantedFromNormalised ExtraDefs
defs SolverConstraint
eq
          [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
newCtCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
news) [SolverConstraint]
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
          Ct
newCt <- ExtraDefs -> SolverConstraint -> TcPluginM Ct
createWantedFromNormalised ExtraDefs
defs SolverConstraint
eq
          [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
newCtCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
news) [SolverConstraint]
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 ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
t1) Bool -> Bool -> Bool
|| Type -> Bool
isNatKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
t2)
      -> do
         (ExtraOp
t1', Normalised
n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
t1
         (ExtraOp
t2', Normalised
n2) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
t2
         SolverConstraint -> MaybeT TcPluginM SolverConstraint
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ct -> ExtraOp -> ExtraOp -> Normalised -> SolverConstraint
NatEquality Ct
ct ExtraOp
t1' ExtraOp
t2' (Normalised -> Normalised -> Normalised
mergeNormalised Normalised
n1 Normalised
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
          (ExtraOp
x', Normalised
n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
x
          (ExtraOp
y', Normalised
n2) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
y
          let res :: MaybeT TcPluginM SolverConstraint
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"
          MaybeT TcPluginM SolverConstraint
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
          (ExtraOp
x', Normalised
n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
x
          (ExtraOp
y', Normalised
n2) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
y
          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))
    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
          (ExtraOp
x', Normalised
n1) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
x
          (ExtraOp
y', Normalised
n2) <- ExtraDefs -> Type -> MaybeT TcPluginM (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
y
          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))
    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
  Type
newPredTy <- case (() :: Constraint) => 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"
  CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct) Type
newPredTy
  let ctN :: Ct
ctN = case Ct
ct of
              CQuantCan QCInst
qc -> QCInst -> Ct
CQuantCan (QCInst
qc { qci_ev = ev})
#if MIN_VERSION_ghc(9,8,0)
              CDictCan di     -> CDictCan (di { di_ev = ev})
              CIrredCan ir    -> CIrredCan (ir { ir_ev = ev})
              CEqCan eq       -> CEqCan (eq { eq_ev = ev})
              CNonCanonical _ -> CNonCanonical ev
#else
              Ct
ctX -> Ct
ctX { cc_ev = ev }
#endif
  Ct -> TcPluginM Ct
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Ct
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
    NameCache
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)
    Maybe Name
res <- IO (Maybe Name) -> TcPluginM (Maybe Name)
forall a. IO a -> TcPluginM a
tcPluginIO (IO (Maybe Name) -> TcPluginM (Maybe Name))
-> IO (Maybe Name) -> TcPluginM (Maybe Name)
forall a b. (a -> b) -> a -> b
$ NameCache -> Name -> IO (Maybe Name)
thNameToGhcNameIO NameCache
nc Name
th
    TcPluginM Name
-> (Name -> TcPluginM Name) -> Maybe Name -> TcPluginM Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CommandLineOption -> TcPluginM Name
forall a. CommandLineOption -> TcPluginM a
forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
fail (CommandLineOption -> TcPluginM Name)
-> CommandLineOption -> TcPluginM Name
forall a b. (a -> b) -> a -> b
$ CommandLineOption
"Failed to lookup " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ Name -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show Name
th) Name -> TcPluginM Name
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
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