{-|
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    #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module GHC.TypeLits.Normalise
  ( plugin )
where

-- external
import Control.Arrow       (second)
import Control.Monad       ((<=<), forM)
#if !MIN_VERSION_ghc(8,4,1)
import Control.Monad       (replicateM)
#endif
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 GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)
#if MIN_VERSION_ghc(9,2,0)
import GHC.TcPluginM.Extra (lookupModule, lookupName)
#endif
import qualified GHC.TcPluginM.Extra as TcPluginM
#if MIN_VERSION_ghc(8,4,0)
import GHC.TcPluginM.Extra (flattenGivens)
#endif
import Text.Read           (readMaybe)

-- GHC API
#if MIN_VERSION_ghc(9,0,0)
import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)
import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)
import GHC.Builtin.Types.Literals
  (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Builtin.Types (naturalTy)
import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
#else
import GHC.Builtin.Types (typeNatKind)
import GHC.Builtin.Types.Literals (typeNatLeqTyCon)
#endif
import GHC.Core (Expr (..))
import GHC.Core.Class (className)
import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo)
import GHC.Core.Predicate
  (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,
   mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)
import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))
import GHC.Core.TyCon (TyCon)
import GHC.Core.Type
  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind)
import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
import GHC.Tc.Plugin
  (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO,
   newEvVar)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Tc.Plugin (tcLookupTyCon)
#endif
import GHC.Tc.Types (TcPlugin (..), TcPluginResult (..))
import GHC.Tc.Types.Constraint
  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ShadowInfo (WDeriv), ctEvidence,
   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,
   isWantedCt, ctEvLoc, ctEvPred, ctEvExpr)
import GHC.Tc.Types.Evidence (EvTerm (..), evCast, evId)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Data.FastString (fsLit)
import GHC.Types.Name.Occurrence (mkTcOcc)
import GHC.Unit.Module (mkModuleName)
#endif
import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
#else
#if MIN_VERSION_ghc(8,5,0)
import CoreSyn    (Expr (..))
#endif
import Outputable (Outputable (..), (<+>), ($$), text)
import Plugins    (Plugin (..), defaultPlugin)
#if MIN_VERSION_ghc(8,6,0)
import Plugins    (purePlugin)
#endif
import PrelNames  (hasKey, knownNatClassName)
import PrelNames  (eqTyConKey, heqTyConKey)
import TcEvidence (EvTerm (..))
#if MIN_VERSION_ghc(8,6,0)
import TcEvidence (evCast, evId)
#endif
#if !MIN_VERSION_ghc(8,4,0)
import TcPluginM  (zonkCt)
#endif
import TcPluginM  (TcPluginM, tcPluginTrace, tcPluginIO)
import Type
  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe)
import TysWiredIn (typeNatKind)

import Coercion   (CoercionHole, Role (..), mkUnivCo)
import Class      (className)
import TcPluginM  (newCoercionHole, tcLookupClass, newEvVar)
import TcRnTypes  (TcPlugin (..), TcPluginResult(..))
import TyCoRep    (UnivCoProvenance (..))
import TcType     (isEqPred)
import TyCon      (TyCon)
import TyCoRep    (Type (..))
import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
                   typeNatSubTyCon)

import TcTypeNats (typeNatLeqTyCon)
import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)

#if MIN_VERSION_ghc(8,10,0)
import Constraint
  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred,
   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,
   isWantedCt)
import Predicate
  (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,
   mkPrimEqPred, getClassPredTys_maybe)
import Type (typeKind)
#else
import TcRnTypes
  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred,
   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,
   isWantedCt)
import TcType (typeKind)
import Type
  (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkClassPred, mkPrimEqPred,
   getClassPredTys_maybe)
#if MIN_VERSION_ghc(8,4,0)
import Type (getEqPredTys)
#endif
#endif

#if MIN_VERSION_ghc(8,10,0)
import Constraint (ctEvExpr)
#elif MIN_VERSION_ghc(8,6,0)
import TcRnTypes  (ctEvExpr)
#else
import TcRnTypes  (ctEvTerm)
#endif

#if MIN_VERSION_ghc(8,2,0)
#if MIN_VERSION_ghc(8,10,0)
import Constraint (ShadowInfo (WDeriv))
#else
import TcRnTypes  (ShadowInfo (WDeriv))
#endif
#endif

#if MIN_VERSION_ghc(8,10,0)
import TcType (isEqPrimPred)
#endif
#endif

-- internal
import GHC.TypeLits.Normalise.SOP
import GHC.TypeLits.Normalise.Unify

#if MIN_VERSION_ghc(9,2,0)
typeNatKind :: Type
typeNatKind :: Type
typeNatKind = Type
naturalTy
#endif

#if !MIN_VERSION_ghc(8,10,0)
isEqPrimPred :: PredType -> Bool
isEqPrimPred = isEqPred
#endif

isEqPredClass :: PredType -> Bool
isEqPredClass :: Type -> Bool
isEqPredClass Type
ty = case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
  Just TyCon
tc -> TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey Bool -> Bool -> Bool
|| TyCon
tc 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 :: TcPlugin
tcPlugin = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Opts -> TcPlugin
normalisePlugin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. a -> a
id Opts
defaultOpts) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse String -> Maybe (Opts -> Opts)
parseArgument
#if MIN_VERSION_ghc(8,6,0)
  , pluginRecompile :: [String] -> IO PluginRecompile
pluginRecompile = [String] -> IO PluginRecompile
purePlugin
#endif
  }
 where
  parseArgument :: String -> Maybe (Opts -> Opts)
parseArgument String
"allow-negated-numbers" = forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { negNumbers :: Bool
negNumbers = Bool
True })
  parseArgument (forall a. Read a => String -> Maybe a
readMaybe forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
"depth=" -> Just Word
depth) = forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { Word
depth :: Word
depth :: Word
depth })
  parseArgument String
_ = 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 = String -> TcPlugin -> TcPlugin
tracePlugin String
"ghc-typelits-natnormalise"
  TcPlugin { tcPluginInit :: TcPluginM ExtraDefs
tcPluginInit  = TcPluginM ExtraDefs
lookupExtraDefs
           , tcPluginSolve :: ExtraDefs -> TcPluginSolver
tcPluginSolve = Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts
           , tcPluginStop :: ExtraDefs -> TcPluginM ()
tcPluginStop  = forall a b. a -> b -> a
const (forall (m :: * -> *) a. Monad m => a -> m a
return ())
           }
newtype OrigCt = OrigCt { OrigCt -> Ct
runOrigCt :: Ct }

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

lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs = do
    IORef (Set CType)
ref <- forall a. IO a -> TcPluginM a
tcPluginIO (forall a. a -> IO (IORef a)
newIORef forall a. Set a
empty)
#if !MIN_VERSION_ghc(9,2,0)
    return (ref, typeNatLeqTyCon)
#else
    Module
md <- ModuleName -> FastString -> TcPluginM Module
lookupModule ModuleName
myModule FastString
myPackage
    TyCon
ordCond <- Module -> String -> TcPluginM TyCon
look Module
md String
"OrdCond"
    forall (m :: * -> *) a. Monad m => a -> m a
return (IORef (Set CType)
ref, TyCon
ordCond)
  where
    look :: Module -> String -> TcPluginM TyCon
look Module
md String
s = Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupName Module
md (String -> OccName
mkTcOcc String
s)
    myModule :: ModuleName
myModule  = String -> ModuleName
mkModuleName String
"Data.Type.Ord"
    myPackage :: FastString
myPackage = String -> FastString
fsLit String
"base"
#endif

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.<=?
  -> [Ct]
  -> [Ct]
  -> [Ct]
  -> TcPluginM TcPluginResult

-- 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
ordCond) [Ct]
givens [Ct]
_deriveds [] = do
    Set CType
done <- forall a. IO a -> TcPluginM a
tcPluginIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Set CType)
gen'd
#if MIN_VERSION_ghc(8,4,0)
    let simplGivens :: [Ct]
simplGivens = [Ct] -> [Ct]
flattenGivens [Ct]
givens
#else
    simplGivens <- mapM zonkCt givens
#endif
    let reds :: [(Ct, (Type, EvTerm, [Type]))]
reds =
          forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ct
_,(Type
_,EvTerm
_,[Type]
v)) -> forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
v Bool -> Bool -> Bool
|| Opts -> Bool
negNumbers Opts
opts) forall a b. (a -> b) -> a -> b
$
          Opts
-> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts TyCon
ordCond Set CType
done [Ct]
simplGivens
        newlyDone :: [CType]
newlyDone = forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(Type
prd, EvTerm
_,[Type]
_)) -> Type -> CType
CType Type
prd) [(Ct, (Type, EvTerm, [Type]))]
reds
    forall a. IO a -> TcPluginM a
tcPluginIO forall a b. (a -> b) -> a -> b
$
      forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Set CType)
gen'd forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
union (forall a. Ord a => [a] -> Set a
fromList [CType]
newlyDone)
    [Ct]
newGivens <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
reds forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
      CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
origCt) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> EvTerm -> TcPluginM CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
    forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [Ct]
newGivens)

-- Solving phase.
-- Solves in/equalities on Nats and simplifiable constraints
-- containing naturals.
decideEqualSOP Opts
opts (IORef (Set CType)
gen'd,TyCon
ordCond) [Ct]
givens [Ct]
deriveds [Ct]
wanteds = do
    -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
    let flat_wanteds0 :: [(OrigCt, Ct)]
flat_wanteds0 = forall a b. (a -> b) -> [a] -> [b]
map (\Ct
ct -> (Ct -> OrigCt
OrigCt Ct
ct, Ct
ct)) [Ct]
wanteds
#if MIN_VERSION_ghc(8,4,0)
    -- flattenGivens should actually be called unflattenGivens
    let simplGivens :: [Ct]
simplGivens = [Ct]
givens forall a. [a] -> [a] -> [a]
++ [Ct] -> [Ct]
flattenGivens [Ct]
givens
        subst :: [(TyVar, Type)]
subst = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ [Ct] -> [((TyVar, Type), Ct)]
TcPluginM.mkSubst' [Ct]
givens
        unflattenWanted :: (a, Ct) -> (a, Ct)
unflattenWanted (a
oCt, Ct
ct) = (a
oCt, [(TyVar, Type)] -> Ct -> Ct
TcPluginM.substCt [(TyVar, Type)]
subst Ct
ct)
        unflat_wanteds0 :: [(OrigCt, Ct)]
unflat_wanteds0 = forall a b. (a -> b) -> [a] -> [b]
map forall {a}. (a, Ct) -> (a, Ct)
unflattenWanted [(OrigCt, Ct)]
flat_wanteds0
#else
    let unflat_wanteds0 = flat_wanteds0
    simplGivens <- mapM zonkCt givens
#endif
    let unflat_wanteds1 :: [(OrigCt, Ct)]
unflat_wanteds1 = forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(OrigCt, Ct)]
unflat_wanteds0
        -- only return solve deriveds when there are wanteds to solve
        unflat_wanteds2 :: [(OrigCt, Ct)]
unflat_wanteds2 = case [(OrigCt, Ct)]
unflat_wanteds1 of
                     [] -> []
                     [(OrigCt, Ct)]
w  -> [(OrigCt, Ct)]
w forall a. [a] -> [a] -> [a]
++ (forall a b. (a -> b) -> [a] -> [b]
map (\Ct
a -> (Ct -> OrigCt
OrigCt Ct
a,Ct
a)) [Ct]
deriveds)
        unit_wanteds :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyCon
-> (OrigCt, Ct)
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality TyCon
ordCond) [(OrigCt, Ct)]
unflat_wanteds2
        nonEqs :: [(OrigCt, Ct)]
nonEqs = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidenceforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a b. (a, b) -> b
snd)
                 forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWantedforall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidenceforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a b. (a, b) -> b
snd) [(OrigCt, Ct)]
unflat_wanteds0
    Set CType
done <- forall a. IO a -> TcPluginM a
tcPluginIO forall a b. (a -> b) -> a -> b
$ 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
ordCond Set CType
done [Ct]
simplGivens
        newlyDone :: [CType]
newlyDone = 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
redGs forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
      CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
origCt) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> EvTerm -> TcPluginM CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
    [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
      <- forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
              (\(OrigCt
origCt, Ct
ct) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OrigCt -> Ct
runOrigCt OrigCt
origCt,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                  [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr ([Ct]
simplGivens forall a. [a] -> [a] -> [a]
++ [Ct]
redGivens) Ct
ct
              )
            [(OrigCt, Ct)]
nonEqs
    if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
    then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
redGs forall a b. (a -> b) -> a -> b
$ \(Ct
ct, (Type
_,EvTerm
_, [Type]
ws)) -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
ws forall a b. (a -> b) -> a -> b
$
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
ct)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> Type -> TcPluginM CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct)
        forall a. IO a -> TcPluginM a
tcPluginIO forall a b. (a -> b) -> a -> b
$
          forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Set CType)
gen'd forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
union (forall a. Ord a => [a] -> Set a
fromList [CType]
newlyDone)
        let unit_givens :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_givens = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
                            (TyCon
-> (OrigCt, Ct)
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality TyCon
ordCond)
                            (forall a b. (a -> b) -> [a] -> [b]
map (\Ct
a -> (Ct -> OrigCt
OrigCt Ct
a, Ct
a)) [Ct]
simplGivens)
        SimplifyResult
sr <- Opts
-> TyCon
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simplifyNats Opts
opts TyCon
ordCond [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_givens [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds
        String -> SDoc -> TcPluginM ()
tcPluginTrace String
"normalised" (forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
        [((EvTerm, Ct), [Ct])]
reds <- 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 forall a b. (a -> b) -> a -> b
$ \(Ct
origCt,(EvTerm
term, [(Type, Type)]
ws, [Ct]
wDicts)) -> do
          [Ct]
wants <- Ct -> [(Type, Type)] -> TcPluginM [Ct]
evSubtPreds Ct
origCt forall a b. (a -> b) -> a -> b
$ Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(Type, Type)]
ws
          forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm
term, Ct
origCt), [Ct]
wDicts forall a. [a] -> [a] -> [a]
++ [Ct]
wants)
        case SimplifyResult
sr of
          Simplified [((EvTerm, Ct), [Ct])]
evs -> do
            let simpld :: [((EvTerm, Ct), [Ct])]
simpld = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Bool
isGiven forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
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 forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds of
                            [] -> []
                            [((EvTerm, Ct), [Ct])]
_  -> [((EvTerm, Ct), [Ct])]
simpld
                ([(EvTerm, Ct)]
solved',[Ct]
newWanteds) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ [((EvTerm, Ct), [Ct])]
simpld1 forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds)
            forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [(EvTerm, Ct)]
solved' forall a b. (a -> b) -> a -> b
$ [Ct]
newWanteds forall a. [a] -> [a] -> [a]
++ [Ct]
ineqForRedWants)
          Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginResult
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
ordCond 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 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 forall a. (a -> Bool) -> [a] -> [a]
filter
      (\(Ct
_, (Type
prd, EvTerm
_, [Type]
_)) ->
        forall a. Ord a => a -> Set a -> Bool
notMember (Type -> CType
CType Type
prd) Set CType
done
      )
    forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
      (\Ct
ct -> (Ct
ct,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Opts -> TyCon -> [Ct] -> Ct -> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts TyCon
ordCond [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
ordCond [Ct]
simplGivens Ct
ct = do
    let (Maybe Type
mans, [(Type, Type)]
ws) =
          forall w a. Writer w a -> (a, w)
runWriter forall a b. (a -> b) -> a -> b
$ Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere forall a b. (a -> b) -> a -> b
$
          CtEvidence -> Type
ctEvPred forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
        ws' :: [Type]
ws' = [ Type
p
              | (Type
p, Type
_) <- Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(Type, Type)]
ws
              , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Bool
`eqType` Type
p)forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
simplGivens
              ]
    Type
pred' <- Maybe Type
mans
    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 forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
      (Maybe Type
mans, [(Type, Type)]
tests) = forall w a. Writer w a -> (a, w)
runWriter forall a b. (a -> b) -> a -> b
$ Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere Type
pred0
  case Maybe Type
mans of
    Maybe Type
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Just Type
pred' -> do
      case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Type -> Type -> Bool
`eqType` Type
pred') forall b c a. (b -> c) -> (a -> b) -> a -> c
.CtEvidence -> Type
ctEvPred 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 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 -> ShadowInfo -> CtLoc -> CtEvidence
CtWanted Type
pred' (TyVar -> TcEvDest
EvVarDest TyVar
evVar)
#if MIN_VERSION_ghc(8,2,0)
                          ShadowInfo
WDeriv
#endif
                          (Ct -> CtLoc
ctLoc Ct
ct))
            -- Evidence for current wanted is simply the coerced binding for
            -- the new binding
                evCo :: Coercion
evCo = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (String -> UnivCoProvenance
PluginProv String
"ghc-typelits-natnormalise")
                         Role
Representational
                         Type
pred' Type
pred0
#if MIN_VERSION_ghc(8,6,0)
                ev :: EvTerm
ev = TyVar -> EvExpr
evId TyVar
evVar EvExpr -> Coercion -> EvTerm
`evCast` Coercion
evCo
#else
                ev = EvId evVar `EvCast` evCo
#endif
            -- Use newly created coerced wanted as evidence, and emit the
            -- normalized wanted as a new constraint to solve.
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (EvTerm
ev, [(Type, Type)]
tests, [Ct
wDict]))
          Maybe (Class, [Type])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        -- Use existing evidence
        Just Ct
c  -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 (String -> UnivCoProvenance
PluginProv String
"ghc-typelits-natnormalise")
              Role
Representational
              Type
pred0 Type
pred'
#if MIN_VERSION_ghc(8,6,0)
      ev :: EvTerm
ev = CtEvidence -> EvExpr
ctEvExpr CtEvidence
ct
             EvExpr -> Coercion -> EvTerm
`evCast` Coercion
evCo
#else
      ev = ctEvTerm ct `EvCast` evCo
#endif
  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) = String -> SDoc
text String
"Simplified" SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr [((EvTerm, Ct), [Ct])]
evs
  ppr (Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq)  = String -> SDoc
text String
"Impossible" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq

simplifyNats
  :: Opts
  -- ^ Allow negated numbers (potentially unsound!)
  -> TyCon
  -- ^ For GHc 9.2: TyCon of Data.Type.Ord.OrdCond
  --   For older: TyCon of GHC.TypeLits.<=?
  -> [(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
depth :: Word
negNumbers :: Bool
depth :: Opts -> Word
negNumbers :: Opts -> Bool
..} TyCon
ordCond [(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 = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (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 forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW
        String -> SDoc -> TcPluginM ()
tcPluginTrace String
"simplifyNats" (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
        String -> SDoc -> TcPluginM ()
tcPluginTrace (String
"simplifyNats(backtrack: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens) forall a. [a] -> [a] -> [a]
++ String
")")
                      (forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs)

        [SimplifyResult]
allSimplified <- 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 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 forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW
          String -> SDoc -> TcPluginM ()
tcPluginTrace String
"simplifyNats" (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

        forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 [] = 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' = forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
u
          v' :: CoreSOP
v' = 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'
      String -> SDoc -> TcPluginM ()
tcPluginTrace String
"unifyNats result" (forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      case UnifyResult
ur of
        UnifyResult
Win -> do
          [((EvTerm, Ct), [Ct])]
evs' <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct forall a. Set a
empty (Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(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 forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs')
        UnifyResult
Lose -> if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((EvTerm, Ct), [Ct])]
evs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
                   then forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible (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)])
eqforall 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, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct forall a. Set a
empty (forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> (Type, Type)
unifyItemToPredType [CoreUnify]
subst' forall a. [a] -> [a] -> [a]
++
                                   Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(Type, Type)]
k)
          let leqsG' :: [(CoreSOP, CoreSOP, Bool)]
leqsG' | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = forall {a}. a -> a -> [(a, a, Bool)]
eqToLeq CoreSOP
u' CoreSOP
v' 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 (forall v c.
(Ord v, Ord c) =>
[UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst [CoreUnify]
subst' [CoreUnify]
subst forall a. [a] -> [a] -> [a]
++ [CoreUnify]
subst')
                      (((EvTerm, Ct), [Ct])
evforall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) [(CoreSOP, CoreSOP, Bool)]
leqsG' [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs 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'    = 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'    = forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
x
          y' :: CoreSOP
y'    = 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)forall a. a -> [a] -> [a]
:[(CoreSOP, CoreSOP, Bool)]
leqsG
                 | Bool
otherwise               = [(CoreSOP, CoreSOP, Bool)]
leqsG
          ineqs :: [(CoreSOP, CoreSOP, Bool)]
ineqs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(CoreSOP, CoreSOP, Bool)]
leqsG
                         , forall a b. (a -> b) -> [a] -> [b]
map (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
                         , forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a b. [Either a b] -> [b]
rights (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG))
                         ]
      String -> SDoc -> TcPluginM ()
tcPluginTrace String
"unifyNats(ineq) results" (forall a. Outputable a => a -> SDoc
ppr (Ct
ct,(CoreSOP, CoreSOP, Bool)
u,CoreSOP
u',[(CoreSOP, CoreSOP, Bool)]
ineqs))
      case 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' <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW (Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(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
_) | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Type)]
k -> forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible (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 = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe 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)
uforall 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
                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 forall a. [a] -> [a] -> [a]
++
                -- The above, but with valid substitutions applied to the wanted.
                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 = 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' <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
kW (Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(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)])
eqforall 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) = (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, 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)   = forall a b. [Either a b] -> ([a], [b])
partitionEithers
                                          (forall a b. (a -> b) -> [a] -> [b]
map (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) = 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 = 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 forall a. [a] -> [a] -> [a]
++ (((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEqforall a. a -> [a] -> [a]
:[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS) 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 forall a. [a] -> [a] -> [a]
++ (forall {c} {c} {b}. (Either (a, SOP v c, SOP v c) b, b)
vSforall a. a -> [a] -> [a]
:[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS 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 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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== a
v3 -> forall a b. b -> Either a b
Right (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)
_ -> 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)
_ = forall a. HasCallStack => String -> a
error String
"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) =
      (forall a b. a -> Either a b
Left (a
ct,forall v c. [Product v c] -> SOP v c
S [forall v c. [Symbol v c] -> Product v c
P [forall v c. v -> Symbol v c
V v
v2]], forall v c. [Product v c] -> SOP v c
S [forall v c. [Symbol v c] -> Product v c
P [forall v c. v -> Symbol v c
V v
v1]]),b
ps)
    swapVar (Either (a, SOP v c, SOP v c) b, b)
_ = forall a. HasCallStack => String -> a
error String
"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
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ct -> Bool
isWantedCt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, Kind)]
subToPred :: Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts{Bool
Word
depth :: Word
negNumbers :: Bool
depth :: Opts -> Word
negNumbers :: Opts -> Bool
..} TyCon
ordCond
  | Bool
negNumbers = forall a b. a -> b -> a
const []
  | Bool
otherwise  = forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> (Type, Type) -> (Type, Type)
subtractionToPred TyCon
ordCond)

-- Extract the Nat equality constraints
toNatEquality :: TyCon -> (OrigCt, Ct) -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
toNatEquality :: TyCon
-> (OrigCt, Ct)
-> Maybe
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality TyCon
ordCond (OrigCt Ct
oCt, Ct
ct) = case Type -> Pred
classifyPredType forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred 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
    Pred
_ -> 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 forall a. Eq a => a -> a -> Bool
== TyCon
tc'
      , forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyCon
tc,TyCon
tc'] forall a. Eq a => [a] -> [a] -> [a]
`intersect` [TyCon
typeNatAddTyCon,TyCon
typeNatSubTyCon
                                   ,TyCon
typeNatMulTyCon,TyCon
typeNatExpTyCon])
      = case forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
eqType) (forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
xs [Type]
ys) of
          [(Type
x,Type
y)]
            | Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
typeKind Type
x)
            , Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
typeKind Type
y)
            , let (CoreSOP
x',[(Type, Type)]
k1) = forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
            , let (CoreSOP
y',[(Type, Type)]
k2) = forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
            -> forall a. a -> Maybe a
Just (forall a b. a -> Either a b
Left (Ct
oCt, CoreSOP
x', CoreSOP
y'),[(Type, Type)]
k1 forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
          [(Type, Type)]
_ -> forall a. Maybe a
Nothing
#if MIN_VERSION_ghc(9,2,0)
      | TyCon
tc 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 forall a. Eq a => a -> a -> Bool
== TyCon
typeNatCmpTyCon
      , TyConApp TyCon
ltTc [] <- Type
lt
      , TyCon
ltTc forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
      , TyConApp TyCon
eqTc [] <- Type
eq
      , TyCon
eqTc forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
      , TyConApp TyCon
gtTc [] <- Type
gt
      , TyCon
gtTc forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
      , let (CoreSOP
x',[(Type, Type)]
k1) = forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (CoreSOP
y',[(Type, Type)]
k2) = 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 forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
      = case TyCon
tc' of
         TyCon
_ | TyCon
tc' forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
           -> forall a. a -> Maybe a
Just (forall a b. b -> Either a b
Right (Ct
oCt, (CoreSOP
x', CoreSOP
y', Bool
True)), [(Type, Type)]
ks)
         TyCon
_ | TyCon
tc' forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
           -> forall a. a -> Maybe a
Just (forall a b. b -> Either a b
Right (Ct
oCt, (CoreSOP
x', CoreSOP
y', Bool
False)), [(Type, Type)]
ks)
         TyCon
_ -> forall a. Maybe a
Nothing
#else
      | tc == ordCond
      , [x,y] <- xs
      , let (x',k1) = runWriter (normaliseNat x)
      , let (y',k2) = runWriter (normaliseNat y)
      , let ks      = k1 ++ k2
      = case tc' of
         _ | tc' == promotedTrueDataCon
           -> Just (Right (oCt, (x', y', True)), ks)
         _ | tc' == promotedFalseDataCon
           -> Just (Right (oCt, (x', y', False)), ks)
         _ -> Nothing
#endif

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

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

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

evSubtPreds :: Ct -> [(PredType,Kind)] -> TcPluginM [Ct]
evSubtPreds :: Ct -> [(Type, Type)] -> TcPluginM [Ct]
evSubtPreds Ct
ct [(Type, Type)]
preds = do
  let predTypes :: [Type]
predTypes = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Type, Type)]
preds
#if MIN_VERSION_ghc(8,4,1)
  [CoercionHole]
holes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> TcPluginM CoercionHole
newCoercionHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Type
mkPrimEqPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, Type)
getEqPredTys) [Type]
predTypes
#else
  holes <- replicateM (length preds) newCoercionHole
#endif
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (CtLoc -> Type -> CoercionHole -> Ct
unifyItemToCt (Ct -> CtLoc
ctLoc Ct
ct)) [Type]
predTypes [CoercionHole]
holes)

evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic :: Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW [(Type, Type)]
preds = case Type -> Pred
classifyPredType forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
  EqPred EqRel
NomEq Type
t1 Type
t2 -> do
    [Ct]
holeWanteds <- Ct -> [(Type, Type)] -> TcPluginM [Ct]
evSubtPreds Ct
ct [(Type, Type)]
preds
    [Ct]
knWanted <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Ct -> CType -> TcPluginM Ct
mkKnWanted Ct
ct) (forall a. Set a -> [a]
toList Set CType
knW)
    let newWant :: [Ct]
newWant = [Ct]
knWanted forall a. [a] -> [a] -> [a]
++ [Ct]
holeWanteds
        ctEv :: Coercion
ctEv    = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (String -> UnivCoProvenance
PluginProv String
"ghc-typelits-natnormalise") Role
Nominal Type
t1 Type
t2
#if MIN_VERSION_ghc(8,5,0)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just ((EvExpr -> EvTerm
EvExpr (forall b. Coercion -> Expr b
Coercion Coercion
ctEv), Ct
ct),[Ct]
newWant))
#else
    return (Just ((EvCoercion ctEv, ct),newWant))
#endif
  Pred
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 Ct -> CtLoc -> Ct
setCtLoc (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev) (CtLoc -> RealSrcSpan -> CtLoc
setCtLocSpan CtLoc
ctl RealSrcSpan
ct_ls)

mkKnWanted
  :: Ct
  -> CType
  -> TcPluginM Ct
mkKnWanted :: Ct -> CType -> TcPluginM Ct
mkKnWanted Ct
ct (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
TcPluginM.newWanted (Ct -> CtLoc
ctLoc Ct
ct) Type
kn_pred
  let wanted' :: Ct
wanted' = CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
ct) CtEvidence
wantedCtEv
  forall (m :: * -> *) a. Monad m => a -> m a
return Ct
wanted'

unifyItemToCt :: CtLoc
              -> PredType
              -> CoercionHole
              -> Ct
unifyItemToCt :: CtLoc -> Type -> CoercionHole -> Ct
unifyItemToCt CtLoc
loc Type
pred_type CoercionHole
hole =
  CtEvidence -> Ct
mkNonCanonical
    (Type -> TcEvDest -> ShadowInfo -> CtLoc -> CtEvidence
CtWanted
      Type
pred_type
      (CoercionHole -> TcEvDest
HoleDest CoercionHole
hole)
#if MIN_VERSION_ghc(8,2,0)
      ShadowInfo
WDeriv
#endif
      CtLoc
loc)