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

A type checker plugin for GHC that can solve /equalities/ of types of kind
'GHC.TypeLits.Nat', where these types are either:

* Type-level naturals
* Type variables
* Applications of the arithmetic expressions @(+,-,*,^)@.

It solves these equalities by normalising them to /sort-of/
'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a
simple syntactic equality.

For example, this solver can prove the equality between:

@
(x + 2)^(y + 2)
@

and

@
4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
@

Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form
of the former.

To use the plugin, add

@
{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}
@

To the header of your file.

== Treating subtraction as addition with a negated number

If you are absolutely sure that your subtractions can /never/ lead to (a locally)
negative number, you can ask the plugin to treat subtraction as addition with
a negated operand by additionally adding:

@
{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}
@

to the header of your file, thereby allowing to use associativity and
commutativity rules when proving constraints involving subtractions. Note that
this option can lead to unsound behaviour and should be handled with extreme
care.

=== When it leads to unsound behaviour

For example, enabling the /allow-negated-numbers/ feature would allow
you to prove:

@
(n - 1) + 1 ~ n
@

/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the
subtraction @n-1@ would be locally negative and hence not be a natural number.

This would allow the following erroneous definition:

@
data Fin (n :: Nat) where
  FZ :: Fin (n + 1)
  FS :: Fin n -> Fin (n + 1)

f :: forall n . Natural -> Fin n
f n = case of
  0 -> FZ
  x -> FS (f \@(n-1) (x - 1))

fs :: [Fin 0]
fs = f \<$\> [0..]
@

=== When it might be Okay

This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>
library.

When you have:

@
-- | Singleton type for the number of repetitions of an element.
data Times (n :: Nat) where
    T :: Times n

-- | An element of a "run-length encoded" vector, containing the value and
-- the number of repetitions
data Elem :: Type -> Nat -> Type where
    (:*) :: t -> Times n -> Elem t n

-- | A length-indexed vector, optimised for repetitions.
data OptVector :: Type -> Nat -> Type where
    End  :: OptVector t 0
    (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n
@

And you want to define:

@
-- | Append two optimised vectors.
type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where
    ys        ++ End = ys
    End       ++ ys = ys
    (x :- xs) ++ ys = x :- (xs ++ ys)
@

then the last line will give rise to the constraint:

@
(n-l)+m ~ (n+m)-l
@

because:

@
x  :: Elem t l
xs :: OptVector t (n-l)
ys :: OptVector t m
@

In this case it's okay to add

@
{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}
@

if you can convince yourself you will never be able to construct a:

@
xs :: OptVector t (n-l)
@

where /n-l/ is a negative number.
-}

{-# LANGUAGE CPP             #-}
{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE NamedFieldPuns  #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections   #-}
{-# LANGUAGE ViewPatterns    #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module GHC.TypeLits.Normalise
  ( plugin )
where

-- external

import Control.Arrow (second)
import Control.Monad ((<=<), forM)
import Control.Monad.Trans.Writer.Strict
import Data.Either (partitionEithers, rights)
import Data.IORef
import Data.List (intersect, partition, stripPrefix, find)
import Data.Maybe (mapMaybe, catMaybes)
import Data.Set (Set, empty, toList, notMember, fromList, union)
import Text.Read (readMaybe)
import qualified Data.Type.Ord
import qualified GHC.TypeError

import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)

-- GHC API

import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)
import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)
import GHC.Builtin.Types.Literals
  (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)
import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon)
import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
import GHC.Core (Expr (..))
import GHC.Core.Class (className)
import GHC.Core.Coercion (Role (..), mkUnivCo)
import GHC.Core.DataCon (dataConWrapId)
import GHC.Core.Predicate
  (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred,
   mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)
import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))
import GHC.Core.TyCon (TyCon)
#if MIN_VERSION_ghc(9,6,0)
import GHC.Core.Type
  (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)
import GHC.Core.TyCo.Compare
  (eqType)
#else
import GHC.Core.Type
  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)
#endif
import GHC.Data.IOEnv (getEnv)
import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC))
import GHC.Tc.Plugin
  (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)
import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)
import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))
import GHC.Tc.Types.Constraint
  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence,
   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLocSpan,
   isWantedCt, ctEvLoc, ctEvPred, ctEvExpr, emptyRewriterSet, setCtEvLoc)
import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId)
import GHC.Types.Unique.FM (emptyUFM)
import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
import GHC (Name)

-- template-haskell

import qualified Language.Haskell.TH as TH

-- internal

import GHC.TypeLits.Normalise.SOP
import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred)

isEqPredClass :: PredType -> Bool
isEqPredClass :: Type -> Bool
isEqPredClass Type
ty = case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
  Just TyCon
tc -> TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
  Maybe TyCon
_ -> Bool
False

-- | To use the plugin, add

--

-- @

-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}

-- @

--

-- To the header of your file.

plugin :: Plugin
plugin :: Plugin
plugin
  = Plugin
defaultPlugin
  { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument
  , pluginRecompile = purePlugin
  }
 where
  parseArgument :: CommandLineOption -> Maybe (Opts -> Opts)
parseArgument CommandLineOption
"allow-negated-numbers" = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { negNumbers = True })
  parseArgument (CommandLineOption -> Maybe Word
forall a. Read a => CommandLineOption -> Maybe a
readMaybe (CommandLineOption -> Maybe Word)
-> (CommandLineOption -> Maybe CommandLineOption)
-> CommandLineOption
-> Maybe Word
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< CommandLineOption -> CommandLineOption -> Maybe CommandLineOption
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix CommandLineOption
"depth=" -> Just Word
depth) = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { depth })
  parseArgument CommandLineOption
_ = Maybe (Opts -> Opts)
forall a. Maybe a
Nothing
  defaultOpts :: Opts
defaultOpts = Opts { negNumbers :: Bool
negNumbers = Bool
False, depth :: Word
depth = Word
5 }

data Opts = Opts { Opts -> Bool
negNumbers :: Bool, Opts -> Word
depth :: Word }

normalisePlugin :: Opts -> TcPlugin
normalisePlugin :: Opts -> TcPlugin
normalisePlugin Opts
opts = CommandLineOption -> TcPlugin -> TcPlugin
tracePlugin CommandLineOption
"ghc-typelits-natnormalise"
  TcPlugin { tcPluginInit :: TcPluginM ExtraDefs
tcPluginInit    = TcPluginM ExtraDefs
lookupExtraDefs
           , tcPluginSolve :: ExtraDefs -> TcPluginSolver
tcPluginSolve   = Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts
           , tcPluginRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite = UniqFM TyCon TcPluginRewriter
-> ExtraDefs -> UniqFM TyCon TcPluginRewriter
forall a b. a -> b -> a
const UniqFM TyCon TcPluginRewriter
forall key elt. UniqFM key elt
emptyUFM
           , 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 ())
           }

type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon))

lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs = do
    IORef (Set CType)
ref <- IO (IORef (Set CType)) -> TcPluginM (IORef (Set CType))
forall a. IO a -> TcPluginM a
tcPluginIO (Set CType -> IO (IORef (Set CType))
forall a. a -> IO (IORef a)
newIORef Set CType
forall a. Set a
empty)
    TyCon
ordCond <- Name -> TcPluginM Name
lookupTHName ''Data.Type.Ord.OrdCond TcPluginM Name -> (Name -> TcPluginM TyCon) -> TcPluginM TyCon
forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM TyCon
tcLookupTyCon
    TyCon
leqT <- Name -> TcPluginM Name
lookupTHName ''(Data.Type.Ord.<=) TcPluginM Name -> (Name -> TcPluginM TyCon) -> TcPluginM TyCon
forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM TyCon
tcLookupTyCon
    TyCon
assertT <- Name -> TcPluginM Name
lookupTHName ''GHC.TypeError.Assert TcPluginM Name -> (Name -> TcPluginM TyCon) -> TcPluginM TyCon
forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM TyCon
tcLookupTyCon
    ExtraDefs -> TcPluginM ExtraDefs
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef (Set CType)
ref, (TyCon
leqT,TyCon
assertT,TyCon
ordCond))

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

decideEqualSOP
  :: Opts
  -> ExtraDefs
      -- ^ 1. Givens that is already generated.

      --   We have to generate new givens at most once;

      --   otherwise GHC will loop indefinitely.

      --

      --

      --   2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond

      --      For older: TyCon of GHC.TypeLits.<=?

  -> EvBindsVar
  -> [Ct]
  -> [Ct]
  -> TcPluginM TcPluginSolveResult

-- Simplification phase: Derives /simplified/ givens;

-- we can reduce given constraints like @Show (Foo (n + 2))@

-- to its normal form @Show (Foo (2 + n))@, which is eventually

-- useful in solving phase.

--

-- This helps us to solve /indirect/ constraints;

-- without this phase, we cannot derive, e.g.,

-- @IsVector UVector (Fin (n + 1))@ from

-- @Unbox (1 + n)@!

decideEqualSOP :: Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts (IORef (Set CType)
gen'd,(TyCon
leqT,TyCon
_,TyCon
_)) EvBindsVar
ev [Ct]
givens [] = do
    Set CType
done <- IO (Set CType) -> TcPluginM (Set CType)
forall a. IO a -> TcPluginM a
tcPluginIO (IO (Set CType) -> TcPluginM (Set CType))
-> IO (Set CType) -> TcPluginM (Set CType)
forall a b. (a -> b) -> a -> b
$ IORef (Set CType) -> IO (Set CType)
forall a. IORef a -> IO a
readIORef IORef (Set CType)
gen'd
    let reds :: [(Ct, (Type, EvTerm, [Type]))]
reds =
          ((Ct, (Type, EvTerm, [Type])) -> Bool)
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ct
_,(Type
_,EvTerm
_,[Type]
v)) -> [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
v Bool -> Bool -> Bool
|| Opts -> Bool
negNumbers Opts
opts) ([(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))])
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> b) -> a -> b
$
          Opts
-> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts TyCon
leqT Set CType
done [Ct]
givens
        newlyDone :: [CType]
newlyDone = ((Ct, (Type, EvTerm, [Type])) -> CType)
-> [(Ct, (Type, EvTerm, [Type]))] -> [CType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(Type
prd, EvTerm
_,[Type]
_)) -> Type -> CType
CType Type
prd) [(Ct, (Type, EvTerm, [Type]))]
reds
    IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$
      IORef (Set CType) -> (Set CType -> Set CType) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Set CType)
gen'd ((Set CType -> Set CType) -> IO ())
-> (Set CType -> Set CType) -> IO ()
forall a b. (a -> b) -> a -> b
$ Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
union ([CType] -> Set CType
forall a. Ord a => [a] -> Set a
fromList [CType]
newlyDone)
    [Ct]
newGivens <- [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
reds (((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
      CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
origCt) (CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvBindsVar -> CtLoc -> Type -> EvTerm -> TcPluginM CtEvidence
newGiven EvBindsVar
ev (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
    TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] [Ct]
newGivens)

-- Solving phase.

-- Solves in/equalities on Nats and simplifiable constraints

-- containing naturals.

decideEqualSOP Opts
opts (IORef (Set CType)
gen'd,tcs :: (TyCon, TyCon, TyCon)
tcs@(TyCon
leqT,TyCon
_,TyCon
_)) EvBindsVar
ev [Ct]
givens [Ct]
wanteds = do
    let unit_wanteds :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds = (Ct
 -> Maybe
      (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)]))
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((TyCon, TyCon, TyCon)
-> Ct
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality (TyCon, TyCon, TyCon)
tcs) [Ct]
wanteds
        nonEqs :: [Ct]
nonEqs = (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter ( Bool -> Bool
not
                        (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Type
p -> Type -> Bool
isEqPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqPrimPred Type
p)
                        (Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred
                        (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence )
                 [Ct]
wanteds
    Set CType
done <- IO (Set CType) -> TcPluginM (Set CType)
forall a. IO a -> TcPluginM a
tcPluginIO (IO (Set CType) -> TcPluginM (Set CType))
-> IO (Set CType) -> TcPluginM (Set CType)
forall a b. (a -> b) -> a -> b
$ IORef (Set CType) -> IO (Set CType)
forall a. IORef a -> IO a
readIORef IORef (Set CType)
gen'd
    let redGs :: [(Ct, (Type, EvTerm, [Type]))]
redGs = Opts
-> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts TyCon
leqT Set CType
done [Ct]
givens
        newlyDone :: [CType]
newlyDone = ((Ct, (Type, EvTerm, [Type])) -> CType)
-> [(Ct, (Type, EvTerm, [Type]))] -> [CType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(Type
prd, EvTerm
_,[Type]
_)) -> Type -> CType
CType Type
prd) [(Ct, (Type, EvTerm, [Type]))]
redGs
    [Ct]
redGivens <- [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
redGs (((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
      CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
origCt) (CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvBindsVar -> CtLoc -> Type -> EvTerm -> TcPluginM CtEvidence
newGiven EvBindsVar
ev (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
    [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
      <- [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
 -> [(Ct, (EvTerm, [(Type, Type)], [Ct]))])
-> TcPluginM [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> TcPluginM [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM (Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))))
-> [Ct] -> TcPluginM [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
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 (\Ct
ct -> ((EvTerm, [(Type, Type)], [Ct])
 -> (Ct, (EvTerm, [(Type, Type)], [Ct])))
-> Maybe (EvTerm, [(Type, Type)], [Ct])
-> Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ct
ct,) (Maybe (EvTerm, [(Type, Type)], [Ct])
 -> Maybe (Ct, (EvTerm, [(Type, Type)], [Ct])))
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
-> TcPluginM (Maybe (Ct, (EvTerm, [(Type, Type)], [Ct])))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                    [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr ([Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
redGivens) Ct
ct)
                            [Ct]
nonEqs
    if [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds Bool -> Bool -> Bool
&& [(Ct, (EvTerm, [(Type, Type)], [Ct]))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
    then TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] []
    else do
        -- Since reducible wanteds also can have some negation/subtraction

        -- subterms, we have to make sure appropriate inequalities to hold.

        -- Here, we generate such additional inequalities for reduction

        -- that is to be added to new [W]anteds.

        [Ct]
ineqForRedWants <- ([[Ct]] -> [Ct]) -> TcPluginM [[Ct]] -> TcPluginM [Ct]
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (TcPluginM [[Ct]] -> TcPluginM [Ct])
-> TcPluginM [[Ct]] -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
redGs (((Ct, (Type, EvTerm, [Type])) -> TcPluginM [Ct])
 -> TcPluginM [[Ct]])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]]
forall a b. (a -> b) -> a -> b
$ \(Ct
ct, (Type
_,EvTerm
_, [Type]
ws)) -> [Type] -> (Type -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
ws ((Type -> TcPluginM Ct) -> TcPluginM [Ct])
-> (Type -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$
          (CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
ct)) (TcPluginM CtEvidence -> TcPluginM Ct)
-> (Type -> TcPluginM CtEvidence) -> Type -> TcPluginM Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> Type -> TcPluginM CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct)
        IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$
          IORef (Set CType) -> (Set CType -> Set CType) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Set CType)
gen'd ((Set CType -> Set CType) -> IO ())
-> (Set CType -> Set CType) -> IO ()
forall a b. (a -> b) -> a -> b
$ Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
union ([CType] -> Set CType
forall a. Ord a => [a] -> Set a
fromList [CType]
newlyDone)
        let unit_givens :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_givens = (Ct
 -> Maybe
      (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)]))
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
                            ((TyCon, TyCon, TyCon)
-> Ct
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality (TyCon, TyCon, TyCon)
tcs)
                            [Ct]
givens
        SimplifyResult
sr <- Opts
-> TyCon
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simplifyNats Opts
opts TyCon
leqT [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_givens [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
        [((EvTerm, Ct), [Ct])]
reds <- [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> ((Ct, (EvTerm, [(Type, Type)], [Ct]))
    -> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds (((Ct, (EvTerm, [(Type, Type)], [Ct]))
  -> TcPluginM ((EvTerm, Ct), [Ct]))
 -> TcPluginM [((EvTerm, Ct), [Ct])])
-> ((Ct, (EvTerm, [(Type, Type)], [Ct]))
    -> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt,(EvTerm
term, [(Type, Type)]
ws, [Ct]
wDicts)) -> do
          [Ct]
wants <- CtLoc -> [Type] -> TcPluginM [Ct]
evSubtPreds (Ct -> CtLoc
ctLoc Ct
origCt) ([Type] -> TcPluginM [Ct]) -> [Type] -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts
opts TyCon
leqT [(Type, Type)]
ws
          ((EvTerm, Ct), [Ct]) -> TcPluginM ((EvTerm, Ct), [Ct])
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm
term, Ct
origCt), [Ct]
wDicts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
wants)
        case SimplifyResult
sr of
          Simplified [((EvTerm, Ct), [Ct])]
evs -> do
            let simpld :: [((EvTerm, Ct), [Ct])]
simpld = (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (((EvTerm, Ct), [Ct]) -> Bool) -> ((EvTerm, Ct), [Ct]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Bool
isGiven (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs
                -- Only solve derived when we solved a wanted

                simpld1 :: [((EvTerm, Ct), [Ct])]
simpld1 = case (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds of
                            [] -> []
                            [((EvTerm, Ct), [Ct])]
_  -> [((EvTerm, Ct), [Ct])]
simpld
                ([(EvTerm, Ct)]
solved',[Ct]
newWanteds) = ([[Ct]] -> [Ct])
-> ([(EvTerm, Ct)], [[Ct]]) -> ([(EvTerm, Ct)], [Ct])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]]))
-> [((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [((EvTerm, Ct), [Ct])]
simpld1 [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds)
            TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [(EvTerm, Ct)]
solved' ([Ct] -> TcPluginSolveResult) -> [Ct] -> TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [Ct]
newWanteds [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
ineqForRedWants)
          Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq -> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginSolveResult
TcPluginContradiction [Either (Ct, CoreSOP, CoreSOP) NatInEquality -> Ct
fromNatEquality Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq])

type NatEquality   = (Ct,CoreSOP,CoreSOP)
type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))

reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]
reduceGivens :: Opts
-> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts TyCon
leqT Set CType
done [Ct]
givens =
  let nonEqs :: [Ct]
nonEqs =
        [ Ct
ct
        | Ct
ct <- [Ct]
givens
        , let ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
              prd :: Type
prd = CtEvidence -> Type
ctEvPred CtEvidence
ev
        , CtEvidence -> Bool
isGiven CtEvidence
ev
        , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (\Type
p -> Type -> Bool
isEqPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqPrimPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqPredClass Type
p) Type
prd
        ]
  in ((Ct, (Type, EvTerm, [Type])) -> Bool)
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (\(Ct
_, (Type
prd, EvTerm
_, [Type]
_)) ->
        CType -> Set CType -> Bool
forall a. Ord a => a -> Set a -> Bool
notMember (Type -> CType
CType Type
prd) Set CType
done
      )
    ([(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))])
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> b) -> a -> b
$ (Ct -> Maybe (Ct, (Type, EvTerm, [Type])))
-> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
      (\Ct
ct -> (Ct
ct,) ((Type, EvTerm, [Type]) -> (Ct, (Type, EvTerm, [Type])))
-> Maybe (Type, EvTerm, [Type])
-> Maybe (Ct, (Type, EvTerm, [Type]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Opts -> TyCon -> [Ct] -> Ct -> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts TyCon
leqT [Ct]
givens Ct
ct)
      [Ct]
nonEqs

tryReduceGiven
  :: Opts -> TyCon -> [Ct] -> Ct
  -> Maybe (PredType, EvTerm, [PredType])
tryReduceGiven :: Opts -> TyCon -> [Ct] -> Ct -> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts TyCon
leqT [Ct]
simplGivens Ct
ct = do
    let (Maybe Type
mans, [(Type, Type)]
ws) =
          Writer [(Type, Type)] (Maybe Type) -> (Maybe Type, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (Maybe Type)
 -> (Maybe Type, [(Type, Type)]))
-> Writer [(Type, Type)] (Maybe Type)
-> (Maybe Type, [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere (Type -> Writer [(Type, Type)] (Maybe Type))
-> Type -> Writer [(Type, Type)] (Maybe 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
        ws' :: [Type]
ws' = [ Type
p
              | Type
p <- Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts
opts TyCon
leqT [(Type, Type)]
ws
              , (Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Bool
`eqType` Type
p)(Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
simplGivens
              ]
    Type
pred' <- Maybe Type
mans
    (Type, EvTerm, [Type]) -> Maybe (Type, EvTerm, [Type])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
pred', CtEvidence -> Type -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
ct) Type
pred', [Type]
ws')

fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality :: Either (Ct, CoreSOP, CoreSOP) NatInEquality -> Ct
fromNatEquality (Left  (Ct
ct, CoreSOP
_, CoreSOP
_)) = Ct
ct
fromNatEquality (Right (Ct
ct, (CoreSOP, CoreSOP, Bool)
_))    = Ct
ct

reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr [Ct]
givens Ct
ct =  do
  let pred0 :: Type
pred0 = CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
      (Maybe Type
mans, [(Type, Type)]
tests) = Writer [(Type, Type)] (Maybe Type) -> (Maybe Type, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (Maybe Type)
 -> (Maybe Type, [(Type, Type)]))
-> Writer [(Type, Type)] (Maybe Type)
-> (Maybe Type, [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere Type
pred0
  case Maybe Type
mans of
    Maybe Type
Nothing -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. Maybe a
Nothing
    Just Type
pred' -> do
      case (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Type -> Type -> Bool
`eqType` Type
pred') (Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
givens of
        -- No existing evidence found

        Maybe Ct
Nothing -> case Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred' of
          -- Are we trying to solve a class instance?

          Just (Class
cls,[Type]
_) | Class -> Name
className Class
cls Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
knownNatClassName -> do
            -- Create new evidence binding for normalized class constraint

            TyVar
evVar <- Type -> TcPluginM TyVar
newEvVar Type
pred'
            -- Bind the evidence to a new wanted normalized class constraint

            let wDict :: Ct
wDict = CtEvidence -> Ct
mkNonCanonical
                          (Type -> TcEvDest -> CtLoc -> RewriterSet -> CtEvidence
CtWanted Type
pred' (TyVar -> TcEvDest
EvVarDest TyVar
evVar) (Ct -> CtLoc
ctLoc Ct
ct) RewriterSet
emptyRewriterSet)
            -- Evidence for current wanted is simply the coerced binding for

            -- the new binding

                evCo :: Coercion
evCo = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
"ghc-typelits-natnormalise")
                         Role
Representational
                         Type
pred' Type
pred0
                ev :: EvTerm
ev = TyVar -> EvExpr
evId TyVar
evVar EvExpr -> Coercion -> EvTerm
`evCast` Coercion
evCo
            -- Use newly created coerced wanted as evidence, and emit the

            -- normalized wanted as a new constraint to solve.

            Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(Type, Type)], [Ct])
-> Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. a -> Maybe a
Just (EvTerm
ev, [(Type, Type)]
tests, [Ct
wDict]))
          Maybe (Class, [Type])
_ -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. Maybe a
Nothing
        -- Use existing evidence

        Just Ct
c  -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(Type, Type)], [Ct])
-> Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. a -> Maybe a
Just (CtEvidence -> Type -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
c) Type
pred0, [(Type, Type)]
tests, []))

toReducedDict :: CtEvidence -> PredType -> EvTerm
toReducedDict :: CtEvidence -> Type -> EvTerm
toReducedDict CtEvidence
ct Type
pred' =
  let pred0 :: Type
pred0 = CtEvidence -> Type
ctEvPred CtEvidence
ct
      evCo :: Coercion
evCo = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
"ghc-typelits-natnormalise")
              Role
Representational
              Type
pred0 Type
pred'
      ev :: EvTerm
ev = (() :: Constraint) => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ct
             EvExpr -> Coercion -> EvTerm
`evCast` Coercion
evCo
  in EvTerm
ev

data SimplifyResult
  = Simplified [((EvTerm,Ct),[Ct])]
  | Impossible (Either NatEquality NatInEquality)

instance Outputable SimplifyResult where
  ppr :: SimplifyResult -> SDoc
ppr (Simplified [((EvTerm, Ct), [Ct])]
evs) = CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"Simplified" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [((EvTerm, Ct), [Ct])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [((EvTerm, Ct), [Ct])]
evs
  ppr (Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq)  = CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"Impossible" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SDoc
forall a. Outputable a => a -> SDoc
ppr Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq

simplifyNats
  :: Opts
  -- ^ Allow negated numbers (potentially unsound!)

  -> TyCon
  -- * TyCon of Data.Type.Ord.<=

  -> [(Either NatEquality NatInEquality,[(Type,Type)])]
  -- ^ Given constraints

  -> [(Either NatEquality NatInEquality,[(Type,Type)])]
  -- ^ Wanted constraints

  -> TcPluginM SimplifyResult
simplifyNats :: Opts
-> TyCon
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simplifyNats opts :: Opts
opts@Opts {Bool
Word
negNumbers :: Opts -> Bool
depth :: Opts -> Word
negNumbers :: Bool
depth :: Word
..} TyCon
leqT [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW = do
    let eqsG1 :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG1 = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
 -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)]))
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a b. (a -> b) -> [a] -> [b]
map (([(Type, Type)] -> [(Type, Type)])
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a b. a -> b -> a
const ([] :: [(Type,Type)]))) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG
        ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs,[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
otherEqs) = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
 -> Bool)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
      [(Type, Type)])],
    [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Bool
forall {a} {v} {c} {v} {c} {b} {b}.
(Either (a, SOP v c, SOP v c) b, b) -> Bool
isVarEqs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG1
        fancyGivens :: [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
 -> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
       [(Type, Type)])]])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
      [(Type, Type)])]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
      [(Type, Type)])]]
forall {v} {a} {c} {c} {a} {c} {c} {c} {b}.
Eq v =>
[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
makeGivensSet [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
otherEqs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs
    case [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs of
      [] -> do
        let eqs :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs = [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
otherEqs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"simplifyNats" ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs)
        [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [] [] [] [] [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs
      [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
_  -> do
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace (CommandLineOption
"simplifyNats(backtrack: " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ Int -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show ([[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
-> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens) CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
")")
                      ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs)

        [SimplifyResult]
allSimplified <- [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
    -> TcPluginM SimplifyResult)
-> TcPluginM [SimplifyResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens (([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
  -> TcPluginM SimplifyResult)
 -> TcPluginM [SimplifyResult])
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
    -> TcPluginM SimplifyResult)
-> TcPluginM [SimplifyResult]
forall a b. (a -> b) -> a -> b
$ \[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
v -> do
          let eqs :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs = [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
v [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW
          CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"simplifyNats" ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs)
          [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [] [] [] [] [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs

        SimplifyResult -> TcPluginM SimplifyResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SimplifyResult -> SimplifyResult -> SimplifyResult)
-> SimplifyResult -> [SimplifyResult] -> SimplifyResult
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SimplifyResult -> SimplifyResult -> SimplifyResult
findFirstSimpliedWanted ([((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified []) [SimplifyResult]
allSimplified)
  where
    simples :: [CoreUnify]
            -> [((EvTerm, Ct), [Ct])]
            -> [(CoreSOP,CoreSOP,Bool)]
            -> [(Either NatEquality NatInEquality,[(Type,Type)])]
            -> [(Either NatEquality NatInEquality,[(Type,Type)])]
            -> TcPluginM SimplifyResult
    simples :: [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
_subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
_leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
_xs [] = SimplifyResult -> TcPluginM SimplifyResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified [((EvTerm, Ct), [Ct])]
evs)
    simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs (eq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq@(Left (Ct
ct,CoreSOP
u,CoreSOP
v),[(Type, Type)]
k):[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs') = do
      let u' :: CoreSOP
u' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
u
          v' :: CoreSOP
v' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
v
      UnifyResult
ur <- Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
unifyNats Ct
ct CoreSOP
u' CoreSOP
v'
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"unifyNats result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      case UnifyResult
ur of
        UnifyResult
Win -> do
          [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Set CType -> [Type] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty (Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts
opts TyCon
leqT [(Type, Type)]
k)
          [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs')
        UnifyResult
Lose -> if [((EvTerm, Ct), [Ct])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((EvTerm, Ct), [Ct])]
evs Bool -> Bool -> Bool
&& [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
                   then SimplifyResult -> TcPluginM SimplifyResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. (a, b) -> a
fst (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq))
                   else [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
        Draw [] -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [] ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. a -> [a] -> [a]
:[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
        Draw [CoreUnify]
subst' -> do
          Maybe ((EvTerm, Ct), [Ct])
evM <- Ct -> Set CType -> [Type] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty ((CoreUnify -> Type) -> [CoreUnify] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> Type
unifyItemToPredType [CoreUnify]
subst' [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++
                                   Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts
opts TyCon
leqT [(Type, Type)]
k)
          let leqsG' :: [(CoreSOP, CoreSOP, Bool)]
leqsG' | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = CoreSOP -> CoreSOP -> [(CoreSOP, CoreSOP, Bool)]
forall {a}. a -> a -> [(a, a, Bool)]
eqToLeq CoreSOP
u' CoreSOP
v' [(CoreSOP, CoreSOP, Bool)]
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a. [a] -> [a] -> [a]
++ [(CoreSOP, CoreSOP, Bool)]
leqsG
                     | Bool
otherwise  = [(CoreSOP, CoreSOP, Bool)]
leqsG
          case Maybe ((EvTerm, Ct), [Ct])
evM of
            Maybe ((EvTerm, Ct), [Ct])
Nothing -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
            Just ((EvTerm, Ct), [Ct])
ev ->
              [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples ([CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall v c.
(Ord v, Ord c) =>
[UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst [CoreUnify]
subst' [CoreUnify]
subst [CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall a. [a] -> [a] -> [a]
++ [CoreUnify]
subst')
                      (((EvTerm, Ct), [Ct])
ev((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) [(CoreSOP, CoreSOP, Bool)]
leqsG' [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs')
    simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs (eq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq@(Right (Ct
ct,u :: (CoreSOP, CoreSOP, Bool)
u@(CoreSOP
x,CoreSOP
y,Bool
b)),[(Type, Type)]
k):[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs') = do
      let u' :: CoreSOP
u'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst ((CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP, CoreSOP, Bool)
u)
          x' :: CoreSOP
x'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
x
          y' :: CoreSOP
y'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
y
          uS :: (CoreSOP, CoreSOP, Bool)
uS    = (CoreSOP
x',CoreSOP
y',Bool
b)
          leqsG' :: [(CoreSOP, CoreSOP, Bool)]
leqsG' | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = (CoreSOP
x',CoreSOP
y',Bool
b)(CoreSOP, CoreSOP, Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a. a -> [a] -> [a]
:[(CoreSOP, CoreSOP, Bool)]
leqsG
                 | Bool
otherwise               = [(CoreSOP, CoreSOP, Bool)]
leqsG
          ineqs :: [(CoreSOP, CoreSOP, Bool)]
ineqs = [[(CoreSOP, CoreSOP, Bool)]] -> [(CoreSOP, CoreSOP, Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(CoreSOP, CoreSOP, Bool)]
leqsG
                         , ((CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool))
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ([CoreUnify] -> (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool)
forall {v} {c} {c}.
(Ord v, Ord c) =>
[UnifyItem v c] -> (SOP v c, SOP v c, c) -> (SOP v c, SOP v c, c)
substLeq [CoreUnify]
subst) [(CoreSOP, CoreSOP, Bool)]
leqsG
                         , (NatInEquality -> (CoreSOP, CoreSOP, Bool))
-> [NatInEquality] -> [(CoreSOP, CoreSOP, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map NatInEquality -> (CoreSOP, CoreSOP, Bool)
forall a b. (a, b) -> b
snd ([Either (Ct, CoreSOP, CoreSOP) NatInEquality] -> [NatInEquality]
forall a b. [Either a b] -> [b]
rights (((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
 -> Either (Ct, CoreSOP, CoreSOP) NatInEquality)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [Either (Ct, CoreSOP, CoreSOP) NatInEquality]
forall a b. (a -> b) -> [a] -> [b]
map (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. (a, b) -> a
fst [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG))
                         ]
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"unifyNats(ineq) results" ((Ct, (CoreSOP, CoreSOP, Bool), CoreSOP, [(CoreSOP, CoreSOP, Bool)])
-> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct
ct,(CoreSOP, CoreSOP, Bool)
u,CoreSOP
u',[(CoreSOP, CoreSOP, Bool)]
ineqs))
      case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
u') of
        Just (Bool
True,Set CType
knW)  -> do
          [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Set CType -> [Type] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW (Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts
opts TyCon
leqT [(Type, Type)]
k)
          [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'

        Just (Bool
False,Set CType
_) | [(Type, Type)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Type)]
k -> SimplifyResult -> TcPluginM SimplifyResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. (a, b) -> a
fst (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq))
        Maybe (Bool, Set CType)
_ -> do
          let solvedIneq :: [(Bool, Set CType)]
solvedIneq = (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType))
-> [WriterT (Set CType) Maybe Bool] -> [(Bool, Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
                 -- it is an inequality that can be instantly solved, such as

                 -- `1 <= x^y`

                 -- OR

                (Word -> (CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool
instantSolveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uWriterT (Set CType) Maybe Bool
-> [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
forall a. a -> [a] -> [a]
:
                Word -> (CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool
instantSolveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uSWriterT (Set CType) Maybe Bool
-> [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
forall a. a -> [a] -> [a]
:
                -- This inequality is either a given constraint, or it is a wanted

                -- constraint, which in normal form is equal to another given

                -- constraint, hence it can be solved.

                -- OR

                ((CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [WriterT (Set CType) Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
u) [(CoreSOP, CoreSOP, Bool)]
ineqs [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
forall a. [a] -> [a] -> [a]
++
                -- The above, but with valid substitutions applied to the wanted.

                ((CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [WriterT (Set CType) Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uS) [(CoreSOP, CoreSOP, Bool)]
ineqs)
              smallest :: (Bool, Set CType)
smallest = [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint [(Bool, Set CType)]
solvedIneq
          case (Bool, Set CType)
smallest of
            (Bool
True,Set CType
kW) -> do
              [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Set CType -> [Type] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
kW (Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts
opts TyCon
leqT [(Type, Type)]
k)
              [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
            (Bool, Set CType)
_ -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. a -> [a] -> [a]
:[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'

    eqToLeq :: a -> a -> [(a, a, Bool)]
eqToLeq a
x a
y = [(a
x,a
y,Bool
True),(a
y,a
x,Bool
True)]
    substLeq :: [UnifyItem v c] -> (SOP v c, SOP v c, c) -> (SOP v c, SOP v c, c)
substLeq [UnifyItem v c]
s (SOP v c
x,SOP v c
y,c
b) = ([UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
x, [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
y, c
b)

    isVarEqs :: (Either (a, SOP v c, SOP v c) b, b) -> Bool
isVarEqs (Left (a
_,S [P [V v
_]], S [P [V v
_]]), b
_) = Bool
True
    isVarEqs (Either (a, SOP v c, SOP v c) b, b)
_ = Bool
False

    makeGivensSet :: [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
makeGivensSet [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
otherEqs (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq
      = let ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV,[Either
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsV)   = [Either
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
   (Either
      (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
      (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b))]
-> ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)],
    [Either
       (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
       (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers
                                          (((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
 -> Either
      (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
      (Either
         (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
         (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)))
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [Either
      (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
      (Either
         (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
         (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b))]
forall a b. (a -> b) -> [a] -> [b]
map ((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> Either
     (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
     (Either
        (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
        (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b))
forall {a} {a} {c} {c} {b} {b} {a} {c} {c} {a} {c} {c} {c} {b}.
Eq a =>
(Either (a, SOP a c, SOP a c) b, b)
-> (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
matchesVarEq (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq) [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
otherEqs)
            ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS,[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS) = [Either
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)],
    [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsV
            vS :: (Either (a, SOP v c, SOP v c) b, b)
vS = (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> (Either (a, SOP v c, SOP v c) b, b)
forall {a} {v} {c} {v} {c} {b} {b} {c} {c} {b}.
(Either (a, SOP v c, SOP v c) b, b)
-> (Either (a, SOP v c, SOP v c) b, b)
swapVar (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq
            givensLHS :: [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensLHS = case [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS of
              [] -> []
              [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
_  -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ (((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. a -> [a] -> [a]
:[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS) [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV)]
            givensRHS :: [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensRHS = case [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS of
              [] -> []
              [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
_  -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ ((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
forall {c} {c} {b}. (Either (a, SOP v c, SOP v c) b, b)
vS(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. a -> [a] -> [a]
:[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV)]
        in  case [Either
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsV of
              [] -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV]
              [Either
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
   (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
_  -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensLHS [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
forall a. [a] -> [a] -> [a]
++ [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensRHS

    matchesVarEq :: (Either (a, SOP a c, SOP a c) b, b)
-> (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
matchesVarEq (Left (a
_, S [P [V a
v1]], S [P [V a
v2]]),b
_) (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r = case (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r of
      (Left (a
_,S [P [V a
v3]],SOP a c
_),b
_)
        | a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
        | a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
      (Left (a
_,SOP a c
_,S [P [V a
v3]]),b
_)
        | a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
        | a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
      (Right (a
_,(S [P [V a
v3]],SOP a c
_,c
_)),b
_)
        | a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
        | a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
      (Right (a
_,(SOP a c
_,S [P [V a
v3]],c
_)),b
_)
        | a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
        | a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
  (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
      (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
_ -> (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r
    matchesVarEq (Either (a, SOP a c, SOP a c) b, b)
_ (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
_ = CommandLineOption
-> Either
     (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
     (Either
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
        (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a. HasCallStack => CommandLineOption -> a
error CommandLineOption
"internal error"

    swapVar :: (Either (a, SOP v c, SOP v c) b, b)
-> (Either (a, SOP v c, SOP v c) b, b)
swapVar (Left (a
ct,S [P [V v
v1]], S [P [V v
v2]]),b
ps) =
      ((a, SOP v c, SOP v c) -> Either (a, SOP v c, SOP v c) b
forall a b. a -> Either a b
Left (a
ct,[Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [v -> Symbol v c
forall v c. v -> Symbol v c
V v
v2]], [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [v -> Symbol v c
forall v c. v -> Symbol v c
V v
v1]]),b
ps)
    swapVar (Either (a, SOP v c, SOP v c) b, b)
_ = CommandLineOption -> (Either (a, SOP v c, SOP v c) b, b)
forall a. HasCallStack => CommandLineOption -> a
error CommandLineOption
"internal error"

    findFirstSimpliedWanted :: SimplifyResult -> SimplifyResult -> SimplifyResult
findFirstSimpliedWanted (Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
e)   SimplifyResult
_  = Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
e
    findFirstSimpliedWanted (Simplified [((EvTerm, Ct), [Ct])]
evs) SimplifyResult
s2
      | (((EvTerm, Ct), [Ct]) -> Bool) -> [((EvTerm, Ct), [Ct])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ct -> Bool
isWantedCt (Ct -> Bool)
-> (((EvTerm, Ct), [Ct]) -> Ct) -> ((EvTerm, Ct), [Ct]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EvTerm, Ct) -> Ct
forall a b. (a, b) -> b
snd ((EvTerm, Ct) -> Ct)
-> (((EvTerm, Ct), [Ct]) -> (EvTerm, Ct))
-> ((EvTerm, Ct), [Ct])
-> Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((EvTerm, Ct), [Ct]) -> (EvTerm, Ct)
forall a b. (a, b) -> a
fst) [((EvTerm, Ct), [Ct])]
evs
      = [((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified [((EvTerm, Ct), [Ct])]
evs
      | Bool
otherwise
      = SimplifyResult
s2

-- If we allow negated numbers we simply do not emit the inequalities

-- derived from the subtractions that are converted to additions with a

-- negated operand

subToPred :: Opts -> TyCon -> [(Type, Type)] -> [PredType]
subToPred :: Opts -> TyCon -> [(Type, Type)] -> [Type]
subToPred Opts{Bool
Word
negNumbers :: Opts -> Bool
depth :: Opts -> Word
negNumbers :: Bool
depth :: Word
..} TyCon
leqT
  | Bool
negNumbers = [Type] -> [(Type, Type)] -> [Type]
forall a b. a -> b -> a
const []
  | Bool
otherwise  = ((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
leq
  where
    leq :: (Type, Type) -> Type
leq (Type
a,Type
b) =
      let lhs :: Type
lhs = TyCon -> [Type] -> Type
TyConApp TyCon
leqT [Type
naturalTy,Type
b,Type
a]
          rhs :: Type
rhs = TyCon -> [Type] -> Type
TyConApp (Int -> TyCon
cTupleTyCon Int
0) []
       in Type -> Type -> Type
mkPrimEqPred Type
lhs Type
rhs

-- Extract the Nat equality constraints

toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
toNatEquality :: (TyCon, TyCon, TyCon)
-> Ct
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality (TyCon
_,TyCon
assertT,TyCon
ordCond) 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
-> Type
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
go Type
t1 Type
t2
    IrredPred Type
p
      -> Type
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall {a}. Type -> Maybe (Either a NatInEquality, [(Type, Type)])
go2 Type
p
    Pred
_ -> Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
  where
    go :: Type
-> Type
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
go (TyConApp TyCon
tc [Type]
xs) (TyConApp TyCon
tc' [Type]
ys)
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc'
      , [TyCon] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyCon
tc,TyCon
tc'] [TyCon] -> [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [TyCon
typeNatAddTyCon,TyCon
typeNatSubTyCon
                                   ,TyCon
typeNatMulTyCon,TyCon
typeNatExpTyCon])
      = case ((Type, Type) -> Bool) -> [(Type, Type)] -> [(Type, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Type, Type) -> Bool) -> (Type, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Bool) -> (Type, Type) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
eqType) ([Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
xs [Type]
ys) of
          [(Type
x,Type
y)]
            | Type -> Bool
isNatKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
x)
            , Type -> Bool
isNatKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
y)
            , let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
            , let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
            -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just ((Ct, CoreSOP, CoreSOP)
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. a -> Either a b
Left (Ct
ct, CoreSOP
x', CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
          [(Type, Type)]
_ -> Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
ordCond
      , [Type
_,Type
cmp,Type
lt,Type
eq,Type
gt] <- [Type]
xs
      , 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
      , let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
      , let ks :: [(Type, Type)]
ks      = [(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
      = case TyCon
tc' of
         TyCon
_ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
           -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
True)), [(Type, Type)]
ks)
         TyCon
_ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
           -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
False)), [(Type, Type)]
ks)
         TyCon
_ -> Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
assertT
      , TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== (Int -> TyCon
cTupleTyCon Int
0)
      , [] <- [Type]
ys
      , [TyConApp TyCon
ordCondTc [Type]
zs, Type
_] <- [Type]
xs
      , TyCon
ordCondTc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
ordCond
      , [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
      , let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
      , let ks :: [(Type, Type)]
ks      = [(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
      = (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
True)), [(Type, Type)]
ks)

    go Type
x Type
y
      | Type -> Bool
isNatKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
x)
      , Type -> Bool
isNatKind ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
y)
      , let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
      = (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just ((Ct, CoreSOP, CoreSOP)
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. a -> Either a b
Left (Ct
ct,CoreSOP
x',CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
      | Bool
otherwise
      = Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing

    go2 :: Type -> Maybe (Either a NatInEquality, [(Type, Type)])
go2 (TyConApp TyCon
tc [Type]
ys)
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
assertT
      , [TyConApp TyCon
ordCondTc [Type]
xs, Type
_] <- [Type]
ys
      , TyCon
ordCondTc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
ordCond
      , [Type
_,Type
cmp,Type
lt,Type
eq,Type
gt] <- [Type]
xs
      , 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
      , let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
      , let ks :: [(Type, Type)]
ks      = [(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
      = (Either a NatInEquality, [(Type, Type)])
-> Maybe (Either a NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either a NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
True)), [(Type, Type)]
ks)

    go2 Type
_ = Maybe (Either a NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing

    isNatKind :: Kind -> Bool
    isNatKind :: Type -> Bool
isNatKind = (Type -> Type -> Bool
`eqType` Type
naturalTy)

unifyItemToPredType :: CoreUnify -> PredType
unifyItemToPredType :: CoreUnify -> Type
unifyItemToPredType CoreUnify
ui = Type -> Type -> Type
mkPrimEqPred Type
ty1 Type
ty2
  where
    ty1 :: Type
ty1 = case CoreUnify
ui of
            SubstItem {TyVar
CoreSOP
siVar :: TyVar
siSOP :: CoreSOP
siVar :: forall v c. UnifyItem v c -> v
siSOP :: forall v c. UnifyItem v c -> SOP v c
..} -> TyVar -> Type
mkTyVarTy TyVar
siVar
            UnifyItem {CoreSOP
siLHS :: CoreSOP
siRHS :: CoreSOP
siLHS :: forall v c. UnifyItem v c -> SOP v c
siRHS :: forall v c. UnifyItem v c -> SOP v c
..} -> CoreSOP -> Type
reifySOP CoreSOP
siLHS
    ty2 :: Type
ty2 = case CoreUnify
ui of
            SubstItem {TyVar
CoreSOP
siVar :: forall v c. UnifyItem v c -> v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: TyVar
siSOP :: CoreSOP
..} -> CoreSOP -> Type
reifySOP CoreSOP
siSOP
            UnifyItem {CoreSOP
siLHS :: forall v c. UnifyItem v c -> SOP v c
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: CoreSOP
siRHS :: CoreSOP
..} -> CoreSOP -> Type
reifySOP CoreSOP
siRHS

evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]
evSubtPreds :: CtLoc -> [Type] -> TcPluginM [Ct]
evSubtPreds CtLoc
loc = (Type -> TcPluginM Ct) -> [Type] -> TcPluginM [Ct]
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 ((CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CtEvidence -> Ct
mkNonCanonical (TcPluginM CtEvidence -> TcPluginM Ct)
-> (Type -> TcPluginM CtEvidence) -> Type -> TcPluginM Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc)

evMagic :: Ct -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic :: Ct -> Set CType -> [Type] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW [Type]
preds = do
  [Ct]
holeWanteds <- CtLoc -> [Type] -> TcPluginM [Ct]
evSubtPreds (Ct -> CtLoc
ctLoc Ct
ct) [Type]
preds
  [Ct]
knWanted <- (CType -> TcPluginM Ct) -> [CType] -> TcPluginM [Ct]
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 (CtLoc -> CType -> TcPluginM Ct
mkKnWanted (Ct -> CtLoc
ctLoc Ct
ct)) (Set CType -> [CType]
forall a. Set a -> [a]
toList Set CType
knW)
  let newWant :: [Ct]
newWant = [Ct]
knWanted [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
holeWanteds
  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 ->
      let ctEv :: Coercion
ctEv = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
"ghc-typelits-natnormalise") Role
Nominal Type
t1 Type
t2
      in Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (((EvTerm, Ct), [Ct]) -> Maybe ((EvTerm, Ct), [Ct])
forall a. a -> Maybe a
Just ((EvExpr -> EvTerm
EvExpr (Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
ctEv), Ct
ct),[Ct]
newWant))
    IrredPred Type
p ->
      let t1 :: Type
t1 = TyCon -> [Type] -> Type
mkTyConApp (Int -> TyCon
cTupleTyCon Int
0) []
          co :: Coercion
co = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
"ghc-typelits-natnormalise") Role
Representational Type
t1 Type
p
          dcApp :: EvExpr
dcApp = TyVar -> EvExpr
evId (DataCon -> TyVar
dataConWrapId (Int -> DataCon
cTupleDataCon Int
0))
       in Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (((EvTerm, Ct), [Ct]) -> Maybe ((EvTerm, Ct), [Ct])
forall a. a -> Maybe a
Just ((EvExpr -> Coercion -> EvTerm
evCast EvExpr
dcApp Coercion
co, Ct
ct),[Ct]
newWant))
    Pred
_ -> Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ((EvTerm, Ct), [Ct])
forall a. Maybe a
Nothing

mkNonCanonical' :: CtLoc -> CtEvidence -> Ct
mkNonCanonical' :: CtLoc -> CtEvidence -> Ct
mkNonCanonical' CtLoc
origCtl CtEvidence
ev =
  let ct_ls :: RealSrcSpan
ct_ls   = CtLoc -> RealSrcSpan
ctLocSpan CtLoc
origCtl
      ctl :: CtLoc
ctl     = CtEvidence -> CtLoc
ctEvLoc  CtEvidence
ev
  in CtEvidence -> Ct
mkNonCanonical (CtEvidence -> CtLoc -> CtEvidence
setCtEvLoc CtEvidence
ev (CtLoc -> RealSrcSpan -> CtLoc
setCtLocSpan CtLoc
ctl RealSrcSpan
ct_ls))

mkKnWanted
  :: CtLoc
  -> CType
  -> TcPluginM Ct
mkKnWanted :: CtLoc -> CType -> TcPluginM Ct
mkKnWanted CtLoc
loc (CType Type
ty) = do
  Class
kc_clas <- Name -> TcPluginM Class
tcLookupClass Name
knownNatClassName
  let kn_pred :: Type
kn_pred = Class -> [Type] -> Type
mkClassPred Class
kc_clas [Type
ty]
  CtEvidence
wantedCtEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc Type
kn_pred
  let wanted' :: Ct
wanted' = CtLoc -> CtEvidence -> Ct
mkNonCanonical' CtLoc
loc CtEvidence
wantedCtEv
  Ct -> TcPluginM Ct
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Ct
wanted'