```{-|
Copyright  :  (C) 2015-2016, University of Twente,
2017     , QBayLogic B.V.
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.

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

== 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

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

module GHC.TypeLits.Normalise
( plugin )
where

-- external
import Control.Arrow       (second)
#if !MIN_VERSION_ghc(8,4,1)
#endif
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)
import qualified GHC.TcPluginM.Extra as TcPluginM
#if MIN_VERSION_ghc(8,4,0)
import GHC.TcPluginM.Extra (flattenGivens)
#endif

-- GHC API
#if MIN_VERSION_ghc(9,0,0)
import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)
import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon, typeNatKind)
import GHC.Builtin.Types.Literals
typeNatSubTyCon)
import GHC.Core (Expr (..))
import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo)
import GHC.Core.Predicate
(EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,
mkPrimEqPred, isEqPred, isEqPrimPred)
import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))
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)
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)
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  (eqTyConKey, heqTyConKey)
import TcEvidence (EvTerm (..))
#if MIN_VERSION_ghc(8,6,0)
import TcEvidence (evCast)
#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 TcPluginM  (newCoercionHole, tcLookupClass)
import TcRnTypes  (TcPlugin (..), TcPluginResult(..))
import TyCoRep    (UnivCoProvenance (..))
import TcType     (isEqPred)
import TyCoRep    (Type (..))
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)
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, getEqPredTys, mkClassPred,
mkPrimEqPred)
#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)
#else
#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(8,10,0)
isEqPrimPred :: PredType -> Bool
isEqPrimPred = isEqPred
#endif

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

-- | To use the plugin, add
--
-- @
-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}
-- @
--
plugin :: Plugin
plugin :: Plugin
plugin
= Plugin
defaultPlugin
{ tcPlugin :: TcPlugin
tcPlugin = ([Opts -> Opts] -> TcPlugin)
-> Maybe [Opts -> Opts] -> Maybe TcPlugin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Opts -> TcPlugin
normalisePlugin (Opts -> TcPlugin)
-> ([Opts -> Opts] -> Opts) -> [Opts -> Opts] -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Opts -> Opts) -> Opts -> Opts) -> Opts -> [Opts -> Opts] -> Opts
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Opts -> Opts) -> Opts -> Opts
forall a. a -> a
id Opts
defaultOpts) (Maybe [Opts -> Opts] -> Maybe TcPlugin)
-> ([[Char]] -> Maybe [Opts -> Opts]) -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Maybe (Opts -> Opts))
-> [[Char]] -> Maybe [Opts -> Opts]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse [Char] -> Maybe (Opts -> Opts)
parseArgument
#if MIN_VERSION_ghc(8,6,0)
, pluginRecompile :: [[Char]] -> IO PluginRecompile
pluginRecompile = [[Char]] -> IO PluginRecompile
purePlugin
#endif
}
where
parseArgument :: [Char] -> Maybe (Opts -> Opts)
parseArgument [Char]
"allow-negated-numbers" = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { negNumbers :: Bool
negNumbers = Bool
True })
parseArgument ([Char] -> Maybe Word
forall a. Read a => [Char] -> Maybe a
-> ([Char] -> Maybe [Char]) -> [Char] -> Maybe Word
forall (m :: * -> *) b c a.
(b -> m c) -> (a -> m b) -> a -> m c
<=< [Char] -> [Char] -> Maybe [Char]
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix [Char]
"depth=" -> Just Word
depth) = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { Word
depth :: Word
depth :: Word
depth })
parseArgument [Char]
_ = Maybe (Opts -> Opts)
forall a. Maybe a
Nothing
defaultOpts :: Opts
defaultOpts = Opts :: Bool -> Word -> Opts
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 = [Char] -> TcPlugin -> TcPlugin
tracePlugin [Char]
"ghc-typelits-natnormalise"
TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin { tcPluginInit :: TcPluginM (IORef (Set CType))
tcPluginInit  = IO (IORef (Set CType)) -> TcPluginM (IORef (Set CType))
forall a. IO a -> TcPluginM a
tcPluginIO (IO (IORef (Set CType)) -> TcPluginM (IORef (Set CType)))
-> IO (IORef (Set CType)) -> TcPluginM (IORef (Set CType))
forall a b. (a -> b) -> a -> b
\$ Set CType -> IO (IORef (Set CType))
forall a. a -> IO (IORef a)
newIORef Set CType
forall a. Set a
empty
, tcPluginSolve :: IORef (Set CType) -> TcPluginSolver
tcPluginSolve = Opts -> IORef (Set CType) -> TcPluginSolver
decideEqualSOP Opts
opts
, tcPluginStop :: IORef (Set CType) -> TcPluginM ()
tcPluginStop  = TcPluginM () -> IORef (Set CType) -> TcPluginM ()
forall a b. a -> b -> a
const (() -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
}
newtype OrigCt = OrigCt { OrigCt -> Ct
runOrigCt :: Ct }

decideEqualSOP
:: Opts
-> IORef (Set CType)
-- ^ Givens that is already generated.
--   We have to generate new givens at most once;
--   otherwise GHC will loop indefinitely.
-> [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 -> IORef (Set CType) -> TcPluginSolver
decideEqualSOP Opts
opts IORef (Set CType)
gen'd [Ct]
givens [Ct]
_deriveds [] = 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
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, (PredType, EvTerm, [PredType]))]
reds =
((Ct, (PredType, EvTerm, [PredType])) -> Bool)
-> [(Ct, (PredType, EvTerm, [PredType]))]
-> [(Ct, (PredType, EvTerm, [PredType]))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ct
_,(PredType
_,EvTerm
_,[PredType]
v)) -> [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PredType]
v Bool -> Bool -> Bool
|| Opts -> Bool
negNumbers Opts
opts) ([(Ct, (PredType, EvTerm, [PredType]))]
-> [(Ct, (PredType, EvTerm, [PredType]))])
-> [(Ct, (PredType, EvTerm, [PredType]))]
-> [(Ct, (PredType, EvTerm, [PredType]))]
forall a b. (a -> b) -> a -> b
\$
Opts -> Set CType -> [Ct] -> [(Ct, (PredType, EvTerm, [PredType]))]
reduceGivens Opts
opts Set CType
done [Ct]
simplGivens
newlyDone :: [CType]
newlyDone = ((Ct, (PredType, EvTerm, [PredType])) -> CType)
-> [(Ct, (PredType, EvTerm, [PredType]))] -> [CType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(PredType
prd, EvTerm
_,[PredType]
_)) -> PredType -> CType
CType PredType
prd) [(Ct, (PredType, EvTerm, [PredType]))]
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, (PredType, EvTerm, [PredType]))]
-> ((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM Ct)
-> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
t a -> (a -> m b) -> m (t b)
forM [(Ct, (PredType, EvTerm, [PredType]))]
reds (((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM Ct)
-> TcPluginM [Ct])
-> ((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM Ct)
-> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
\$ \(Ct
origCt, (PredType
pred', EvTerm
evTerm, [PredType]
_)) ->
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
<\$> CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) PredType
pred' EvTerm
evTerm
TcPluginResult -> TcPluginM TcPluginResult
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 [Ct]
givens  [Ct]
_deriveds [Ct]
wanteds = do
-- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
#if MIN_VERSION_ghc(8,4,0)
let simplGivens :: [Ct]
simplGivens = [Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct] -> [Ct]
flattenGivens [Ct]
givens
subst :: [(TcTyVar, PredType)]
subst = ([(TcTyVar, PredType)], [Ct]) -> [(TcTyVar, PredType)]
forall a b. (a, b) -> a
fst (([(TcTyVar, PredType)], [Ct]) -> [(TcTyVar, PredType)])
-> ([(TcTyVar, PredType)], [Ct]) -> [(TcTyVar, PredType)]
forall a b. (a -> b) -> a -> b
\$ [((TcTyVar, PredType), Ct)] -> ([(TcTyVar, PredType)], [Ct])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((TcTyVar, PredType), Ct)] -> ([(TcTyVar, PredType)], [Ct]))
-> [((TcTyVar, PredType), Ct)] -> ([(TcTyVar, PredType)], [Ct])
forall a b. (a -> b) -> a -> b
\$ [Ct] -> [((TcTyVar, PredType), Ct)]
TcPluginM.mkSubst' [Ct]
givens
wanteds0 :: [(OrigCt, Ct)]
wanteds0 = (Ct -> (OrigCt, Ct)) -> [Ct] -> [(OrigCt, Ct)]
forall a b. (a -> b) -> [a] -> [b]
map (\Ct
ct -> (Ct -> OrigCt
OrigCt Ct
ct,
[(TcTyVar, PredType)] -> Ct -> Ct
TcPluginM.substCt [(TcTyVar, PredType)]
subst Ct
ct
)
) [Ct]
wanteds
#else
let wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds
simplGivens <- mapM zonkCt givens
#endif
let wanteds' :: [Ct]
wanteds' = (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool) -> (Ct -> CtEvidence) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
wanteds
unit_wanteds :: [(Either NatEquality NatInEquality, [(PredType, PredType)])]
unit_wanteds = (Ct
-> Maybe
(Either NatEquality NatInEquality, [(PredType, PredType)]))
-> [Ct]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
toNatEquality [Ct]
wanteds'
nonEqs :: [(OrigCt, Ct)]
nonEqs = ((OrigCt, Ct) -> Bool) -> [(OrigCt, Ct)] -> [(OrigCt, Ct)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((OrigCt, Ct) -> Bool) -> (OrigCt, Ct) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\PredType
p -> PredType -> Bool
isEqPred PredType
p Bool -> Bool -> Bool
|| PredType -> Bool
isEqPrimPred PredType
p) (PredType -> Bool)
-> ((OrigCt, Ct) -> PredType) -> (OrigCt, Ct) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType)
-> ((OrigCt, Ct) -> CtEvidence) -> (OrigCt, Ct) -> PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence(Ct -> CtEvidence)
-> ((OrigCt, Ct) -> Ct) -> (OrigCt, Ct) -> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OrigCt, Ct) -> Ct
forall a b. (a, b) -> b
snd)
([(OrigCt, Ct)] -> [(OrigCt, Ct)])
-> [(OrigCt, Ct)] -> [(OrigCt, Ct)]
forall a b. (a -> b) -> a -> b
\$ ((OrigCt, Ct) -> Bool) -> [(OrigCt, Ct)] -> [(OrigCt, Ct)]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted(CtEvidence -> Bool)
-> ((OrigCt, Ct) -> CtEvidence) -> (OrigCt, Ct) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence(Ct -> CtEvidence)
-> ((OrigCt, Ct) -> Ct) -> (OrigCt, Ct) -> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(OrigCt, Ct) -> Ct
forall a b. (a, b) -> b
snd) [(OrigCt, Ct)]
wanteds0
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
gen'd
let redGs :: [(Ct, (PredType, EvTerm, [PredType]))]
redGs = Opts -> Set CType -> [Ct] -> [(Ct, (PredType, EvTerm, [PredType]))]
reduceGivens Opts
opts Set CType
done [Ct]
simplGivens
newlyDone :: [CType]
newlyDone = ((Ct, (PredType, EvTerm, [PredType])) -> CType)
-> [(Ct, (PredType, EvTerm, [PredType]))] -> [CType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(PredType
prd, EvTerm
_,[PredType]
_)) -> PredType -> CType
CType PredType
prd) [(Ct, (PredType, EvTerm, [PredType]))]
redGs
[Ct]
redGivens <- [(Ct, (PredType, EvTerm, [PredType]))]
-> ((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM Ct)
-> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
t a -> (a -> m b) -> m (t b)
forM [(Ct, (PredType, EvTerm, [PredType]))]
redGs (((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM Ct)
-> TcPluginM [Ct])
-> ((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM Ct)
-> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
\$ \(Ct
origCt, (PredType
pred', EvTerm
evTerm, [PredType]
_)) ->
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
<\$> CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) PredType
pred' EvTerm
evTerm
[(Ct, (EvTerm, [(PredType, PredType)]))]
reducible_wanteds
<- [Maybe (Ct, (EvTerm, [(PredType, PredType)]))]
-> [(Ct, (EvTerm, [(PredType, PredType)]))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Ct, (EvTerm, [(PredType, PredType)]))]
-> [(Ct, (EvTerm, [(PredType, PredType)]))])
-> TcPluginM [Maybe (Ct, (EvTerm, [(PredType, PredType)]))]
-> TcPluginM [(Ct, (EvTerm, [(PredType, PredType)]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$>
((OrigCt, Ct)
-> TcPluginM (Maybe (Ct, (EvTerm, [(PredType, PredType)]))))
-> [(OrigCt, Ct)]
-> TcPluginM [Maybe (Ct, (EvTerm, [(PredType, PredType)]))]
forall (t :: * -> *) (m :: * -> *) a b.
(a -> m b) -> t a -> m (t b)
mapM
(\(OrigCt
origCt, Ct
ct) -> ((EvTerm, [(PredType, PredType)])
-> (Ct, (EvTerm, [(PredType, PredType)])))
-> Maybe (EvTerm, [(PredType, PredType)])
-> Maybe (Ct, (EvTerm, [(PredType, PredType)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OrigCt -> Ct
runOrigCt OrigCt
origCt,) (Maybe (EvTerm, [(PredType, PredType)])
-> Maybe (Ct, (EvTerm, [(PredType, PredType)])))
-> TcPluginM (Maybe (EvTerm, [(PredType, PredType)]))
-> TcPluginM (Maybe (Ct, (EvTerm, [(PredType, PredType)])))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$>
[Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(PredType, PredType)]))
reduceNatConstr ([Ct]
simplGivens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
redGivens) Ct
ct
)
[(OrigCt, Ct)]
nonEqs
if [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either NatEquality NatInEquality, [(PredType, PredType)])]
unit_wanteds Bool -> Bool -> Bool
&& [(Ct, (EvTerm, [(PredType, PredType)]))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Ct, (EvTerm, [(PredType, PredType)]))]
reducible_wanteds
then TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
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 <- ([[Ct]] -> [Ct]) -> TcPluginM [[Ct]] -> TcPluginM [Ct]
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, (PredType, EvTerm, [PredType]))]
-> ((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]]
forall (t :: * -> *) (m :: * -> *) a b.
t a -> (a -> m b) -> m (t b)
forM [(Ct, (PredType, EvTerm, [PredType]))]
redGs (((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]])
-> ((Ct, (PredType, EvTerm, [PredType])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]]
forall a b. (a -> b) -> a -> b
\$ \(Ct
ct, (PredType
_,EvTerm
_, [PredType]
ws)) -> [PredType] -> (PredType -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
t a -> (a -> m b) -> m (t b)
forM [PredType]
ws ((PredType -> TcPluginM Ct) -> TcPluginM [Ct])
-> (PredType -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
\$
(CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
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)
-> (PredType -> TcPluginM CtEvidence) -> PredType -> TcPluginM Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> PredType -> 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 NatEquality NatInEquality, [(PredType, PredType)])]
unit_givens = (Ct
-> Maybe
(Either NatEquality NatInEquality, [(PredType, PredType)]))
-> [Ct]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
toNatEquality [Ct]
simplGivens
SimplifyResult
sr <- Opts
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simplifyNats Opts
opts [(Either NatEquality NatInEquality, [(PredType, PredType)])]
unit_givens [(Either NatEquality NatInEquality, [(PredType, PredType)])]
unit_wanteds
[Char] -> SDoc -> TcPluginM ()
tcPluginTrace [Char]
"normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
[((EvTerm, Ct), [Ct])]
reds <- [(Ct, (EvTerm, [(PredType, PredType)]))]
-> ((Ct, (EvTerm, [(PredType, PredType)]))
-> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
t a -> (a -> m b) -> m (t b)
forM [(Ct, (EvTerm, [(PredType, PredType)]))]
reducible_wanteds (((Ct, (EvTerm, [(PredType, PredType)]))
-> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])])
-> ((Ct, (EvTerm, [(PredType, PredType)]))
-> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall a b. (a -> b) -> a -> b
\$ \(Ct
origCt,(EvTerm
term, [(PredType, PredType)]
ws)) -> do
[Ct]
wants <- Ct -> [(PredType, PredType)] -> TcPluginM [Ct]
evSubtPreds Ct
origCt ([(PredType, PredType)] -> TcPluginM [Ct])
-> [(PredType, PredType)] -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
\$ Opts -> [(PredType, PredType)] -> [(PredType, PredType)]
subToPred Opts
opts [(PredType, PredType)]
ws
((EvTerm, Ct), [Ct]) -> TcPluginM ((EvTerm, Ct), [Ct])
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm
term, Ct
origCt), [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 (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)]
solved',[Ct]
newWanteds) = ([[Ct]] -> [Ct])
-> ([(EvTerm, Ct)], [[Ct]]) -> ([(EvTerm, Ct)], [Ct])
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])]
simpld [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds)
TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [(EvTerm, Ct)]
solved' ([Ct] -> TcPluginResult) -> [Ct] -> TcPluginResult
forall a b. (a -> b) -> a -> b
\$ [Ct]
newWanteds [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
ineqForRedWants)
Impossible Either NatEquality NatInEquality
eq -> TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginResult
TcPluginContradiction [Either NatEquality NatInEquality -> Ct
fromNatEquality Either NatEquality NatInEquality
eq])

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

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

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

fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality :: Either NatEquality 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)]))
reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(PredType, PredType)]))
reduceNatConstr [Ct]
givens Ct
ct =  do
let pred0 :: PredType
pred0 = CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType) -> CtEvidence -> PredType
forall a b. (a -> b) -> a -> b
\$ Ct -> CtEvidence
ctEvidence Ct
ct
(Maybe PredType
mans, [(PredType, PredType)]
tests) = Writer [(PredType, PredType)] (Maybe PredType)
-> (Maybe PredType, [(PredType, PredType)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(PredType, PredType)] (Maybe PredType)
-> (Maybe PredType, [(PredType, PredType)]))
-> Writer [(PredType, PredType)] (Maybe PredType)
-> (Maybe PredType, [(PredType, PredType)])
forall a b. (a -> b) -> a -> b
\$ PredType -> Writer [(PredType, PredType)] (Maybe PredType)
normaliseNatEverywhere PredType
pred0
case Maybe PredType
mans of
Maybe PredType
Nothing -> Maybe (EvTerm, [(PredType, PredType)])
-> TcPluginM (Maybe (EvTerm, [(PredType, PredType)]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(PredType, PredType)])
forall a. Maybe a
Nothing
Just PredType
pred' -> do
case (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((PredType -> PredType -> Bool
`eqType` PredType
pred') (PredType -> Bool) -> (Ct -> PredType) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType) -> (Ct -> CtEvidence) -> Ct -> PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
givens of
Maybe Ct
Nothing -> Maybe (EvTerm, [(PredType, PredType)])
-> TcPluginM (Maybe (EvTerm, [(PredType, PredType)]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(PredType, PredType)])
forall a. Maybe a
Nothing
Just Ct
c  -> Maybe (EvTerm, [(PredType, PredType)])
-> TcPluginM (Maybe (EvTerm, [(PredType, PredType)]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(PredType, PredType)])
-> Maybe (EvTerm, [(PredType, PredType)])
forall a. a -> Maybe a
Just (CtEvidence -> PredType -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
c) PredType
pred0, [(PredType, PredType)]
tests))

toReducedDict :: CtEvidence -> PredType -> EvTerm
toReducedDict :: CtEvidence -> PredType -> EvTerm
toReducedDict CtEvidence
ct PredType
pred' =
let pred0 :: PredType
pred0 = CtEvidence -> PredType
ctEvPred CtEvidence
ct
evCo :: Coercion
evCo = UnivCoProvenance -> Role -> PredType -> PredType -> Coercion
mkUnivCo ([Char] -> UnivCoProvenance
PluginProv [Char]
"ghc-typelits-natnormalise")
Role
Representational
PredType
pred0 PredType
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) = [Char] -> SDoc
text [Char]
"Simplified" SDoc -> SDoc -> SDoc
\$\$ [((EvTerm, Ct), [Ct])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [((EvTerm, Ct), [Ct])]
evs
ppr (Impossible Either NatEquality NatInEquality
eq)  = [Char] -> SDoc
text [Char]
"Impossible" SDoc -> SDoc -> SDoc
<+> Either NatEquality NatInEquality -> SDoc
forall a. Outputable a => a -> SDoc
ppr Either NatEquality NatInEquality
eq

simplifyNats
:: Opts
-- ^ Allow negated numbers (potentially unsound!)
-> [(Either NatEquality NatInEquality,[(Type,Type)])]
-- ^ Given constraints
-> [(Either NatEquality NatInEquality,[(Type,Type)])]
-- ^ Wanted constraints
-> TcPluginM SimplifyResult
simplifyNats :: Opts
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simplifyNats opts :: Opts
opts@Opts {Bool
Word
depth :: Word
negNumbers :: Bool
depth :: Opts -> Word
negNumbers :: Opts -> Bool
..} [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsG [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsW = do
let eqsG1 :: [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsG1 = ((Either NatEquality NatInEquality, [(PredType, PredType)])
-> (Either NatEquality NatInEquality, [(PredType, PredType)]))
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a b. (a -> b) -> [a] -> [b]
map (([(PredType, PredType)] -> [(PredType, PredType)])
-> (Either NatEquality NatInEquality, [(PredType, PredType)])
-> (Either NatEquality NatInEquality, [(PredType, PredType)])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([(PredType, PredType)]
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a b. a -> b -> a
const ([] :: [(Type,Type)]))) [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsG
([(Either NatEquality NatInEquality, [(PredType, PredType)])]
varEqs,[(Either NatEquality NatInEquality, [(PredType, PredType)])]
otherEqs) = ((Either NatEquality NatInEquality, [(PredType, PredType)])
-> Bool)
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> ([(Either NatEquality NatInEquality, [(PredType, PredType)])],
[(Either NatEquality NatInEquality, [(PredType, PredType)])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either NatEquality NatInEquality, [(PredType, PredType)]) -> Bool
forall a v c v c b b. (Either (a, SOP v c, SOP v c) b, b) -> Bool
isVarEqs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsG1
fancyGivens :: [[(Either NatEquality NatInEquality, [(PredType, PredType)])]]
fancyGivens = ((Either NatEquality NatInEquality, [(PredType, PredType)])
-> [[(Either NatEquality NatInEquality, [(PredType, PredType)])]])
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [[(Either NatEquality NatInEquality, [(PredType, PredType)])]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> (Either NatEquality NatInEquality, [(PredType, PredType)])
-> [[(Either NatEquality NatInEquality, [(PredType, PredType)])]]
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 NatEquality NatInEquality, [(PredType, PredType)])]
otherEqs) [(Either NatEquality NatInEquality, [(PredType, PredType)])]
varEqs
case [(Either NatEquality NatInEquality, [(PredType, PredType)])]
varEqs of
[] -> do
let eqs :: [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs = [(Either NatEquality NatInEquality, [(PredType, PredType)])]
otherEqs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a. [a] -> [a] -> [a]
++ [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsW
[Char] -> SDoc -> TcPluginM ()
tcPluginTrace [Char]
"simplifyNats" ([(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs)
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [] [] [] [] [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs
[(Either NatEquality NatInEquality, [(PredType, PredType)])]
_  -> do
[Char] -> SDoc -> TcPluginM ()
tcPluginTrace ([Char]
"simplifyNats(backtrack: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([[(Either NatEquality NatInEquality, [(PredType, PredType)])]]
-> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Either NatEquality NatInEquality, [(PredType, PredType)])]]
fancyGivens) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")")
([(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either NatEquality NatInEquality, [(PredType, PredType)])]
varEqs)

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

SimplifyResult -> TcPluginM SimplifyResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SimplifyResult -> SimplifyResult -> SimplifyResult)
-> SimplifyResult -> [SimplifyResult] -> SimplifyResult
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 NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
_subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
_leqsG [(Either NatEquality NatInEquality, [(PredType, PredType)])]
_xs [] = SimplifyResult -> TcPluginM SimplifyResult
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 NatEquality NatInEquality, [(PredType, PredType)])]
xs (eq :: (Either NatEquality NatInEquality, [(PredType, PredType)])
eq@(Left (Ct
ct,CoreSOP
u,CoreSOP
v),[(PredType, PredType)]
k):[(Either NatEquality NatInEquality, [(PredType, PredType)])]
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'
[Char] -> SDoc -> TcPluginM ()
tcPluginTrace [Char]
"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
-> [(PredType, PredType)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty (Opts -> [(PredType, PredType)] -> [(PredType, PredType)]
subToPred Opts
opts [(PredType, PredType)]
k)
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG [] ([(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a. [a] -> [a] -> [a]
++ [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs')
UnifyResult
Lose -> if [((EvTerm, Ct), [Ct])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((EvTerm, Ct), [Ct])]
evs Bool -> Bool -> Bool
&& [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs'
then SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NatEquality NatInEquality -> SimplifyResult
Impossible ((Either NatEquality NatInEquality, [(PredType, PredType)])
-> Either NatEquality NatInEquality
forall a b. (a, b) -> a
fst (Either NatEquality NatInEquality, [(PredType, PredType)])
eq))
else [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs'
Draw [] -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [] ((Either NatEquality NatInEquality, [(PredType, PredType)])
eq(Either NatEquality NatInEquality, [(PredType, PredType)])
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a. a -> [a] -> [a]
:[(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs) [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs'
Draw [CoreUnify]
subst' -> do
Maybe ((EvTerm, Ct), [Ct])
evM <- Ct
-> Set CType
-> [(PredType, PredType)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty ((CoreUnify -> (PredType, PredType))
-> [CoreUnify] -> [(PredType, PredType)]
forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> (PredType, PredType)
unifyItemToPredType [CoreUnify]
subst' [(PredType, PredType)]
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a. [a] -> [a] -> [a]
++
Opts -> [(PredType, PredType)] -> [(PredType, PredType)]
subToPred Opts
opts [(PredType, PredType)]
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 NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs'
Just ((EvTerm, Ct), [Ct])
ev ->
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> 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 NatEquality NatInEquality, [(PredType, PredType)])]
xs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a. [a] -> [a] -> [a]
++ [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs')
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs (eq :: (Either NatEquality NatInEquality, [(PredType, PredType)])
eq@(Right (Ct
ct,u :: (CoreSOP, CoreSOP, Bool)
u@(CoreSOP
x,CoreSOP
y,Bool
b)),[(PredType, PredType)]
k):[(Either NatEquality NatInEquality, [(PredType, PredType)])]
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 NatEquality NatInEquality] -> [NatInEquality]
forall a b. [Either a b] -> [b]
rights (((Either NatEquality NatInEquality, [(PredType, PredType)])
-> Either NatEquality NatInEquality)
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [Either NatEquality NatInEquality]
forall a b. (a -> b) -> [a] -> [b]
map (Either NatEquality NatInEquality, [(PredType, PredType)])
-> Either NatEquality NatInEquality
forall a b. (a, b) -> a
fst [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqsG))
]
[Char] -> SDoc -> TcPluginM ()
tcPluginTrace [Char]
"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
-> [(PredType, PredType)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW (Opts -> [(PredType, PredType)] -> [(PredType, PredType)]
subToPred Opts
opts [(PredType, PredType)]
k)
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs'

Just (Bool
False,Set CType
_) | [(PredType, PredType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(PredType, PredType)]
k -> SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NatEquality NatInEquality -> SimplifyResult
Impossible ((Either NatEquality NatInEquality, [(PredType, PredType)])
-> Either NatEquality NatInEquality
forall a b. (a, b) -> a
fst (Either NatEquality NatInEquality, [(PredType, PredType)])
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]
:
-- 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
-> [(PredType, PredType)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
kW (Opts -> [(PredType, PredType)] -> [(PredType, PredType)]
subToPred Opts
opts [(PredType, PredType)]
k)
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs [(Either NatEquality NatInEquality, [(PredType, PredType)])]
eqs'
(Bool, Set CType)
_ -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG ((Either NatEquality NatInEquality, [(PredType, PredType)])
eq(Either NatEquality NatInEquality, [(PredType, PredType)])
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
-> [(Either NatEquality NatInEquality, [(PredType, PredType)])]
forall a. a -> [a] -> [a]
:[(Either NatEquality NatInEquality, [(PredType, PredType)])]
xs) [(Either NatEquality NatInEquality, [(PredType, PredType)])]
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)
_ = [Char]
-> 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 => [Char] -> a
error [Char]
"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)
_ = [Char] -> (Either (a, SOP v c, SOP v c) b, b)
forall a. HasCallStack => [Char] -> a
error [Char]
"internal error"

findFirstSimpliedWanted :: SimplifyResult -> SimplifyResult -> SimplifyResult
findFirstSimpliedWanted (Impossible Either NatEquality NatInEquality
e)   SimplifyResult
_  = Either NatEquality NatInEquality -> SimplifyResult
Impossible Either NatEquality 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 -> [(Type, Type)] -> [(PredType, Kind)]
subToPred :: Opts -> [(PredType, PredType)] -> [(PredType, PredType)]
subToPred Opts{Bool
Word
depth :: Word
negNumbers :: Bool
depth :: Opts -> Word
negNumbers :: Opts -> Bool
..}
| Bool
negNumbers = [(PredType, PredType)]
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a b. a -> b -> a
const []
| Bool
otherwise  = ((PredType, PredType) -> (PredType, PredType))
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a b. (a -> b) -> [a] -> [b]
map (PredType, PredType) -> (PredType, PredType)
subtractionToPred

-- Extract the Nat equality constraints
toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
toNatEquality :: Ct
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
toNatEquality Ct
ct = case PredType -> Pred
classifyPredType (PredType -> Pred) -> PredType -> Pred
forall a b. (a -> b) -> a -> b
\$ CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType) -> CtEvidence -> PredType
forall a b. (a -> b) -> a -> b
\$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq PredType
t1 PredType
t2
-> PredType
-> PredType
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
go PredType
t1 PredType
t2
Pred
_ -> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
forall a. Maybe a
Nothing
where
go :: PredType
-> PredType
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
go (TyConApp TyCon
tc [PredType]
xs) (TyConApp TyCon
tc' [PredType]
ys)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc'
, [TyCon] -> 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
typeNatSubTyCon
,TyCon
typeNatMulTyCon,TyCon
typeNatExpTyCon])
= case ((PredType, PredType) -> Bool)
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((PredType, PredType) -> Bool) -> (PredType, PredType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PredType -> PredType -> Bool) -> (PredType, PredType) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry PredType -> PredType -> Bool
eqType) ([PredType] -> [PredType] -> [(PredType, PredType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PredType]
xs [PredType]
ys) of
[(PredType
x,PredType
y)]
| PredType -> Bool
isNatKind (HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
x)
, PredType -> Bool
isNatKind (HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
y)
, let (CoreSOP
x',[(PredType, PredType)]
k1) = Writer [(PredType, PredType)] CoreSOP
-> (CoreSOP, [(PredType, PredType)])
forall w a. Writer w a -> (a, w)
runWriter (PredType -> Writer [(PredType, PredType)] CoreSOP
normaliseNat PredType
x)
, let (CoreSOP
y',[(PredType, PredType)]
k2) = Writer [(PredType, PredType)] CoreSOP
-> (CoreSOP, [(PredType, PredType)])
forall w a. Writer w a -> (a, w)
runWriter (PredType -> Writer [(PredType, PredType)] CoreSOP
normaliseNat PredType
y)
-> (Either NatEquality NatInEquality, [(PredType, PredType)])
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
forall a. a -> Maybe a
Just (NatEquality -> Either NatEquality NatInEquality
forall a b. a -> Either a b
Left (Ct
ct, CoreSOP
x', CoreSOP
y'),[(PredType, PredType)]
k1 [(PredType, PredType)]
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a. [a] -> [a] -> [a]
++ [(PredType, PredType)]
k2)
[(PredType, PredType)]
_ -> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
forall a. Maybe a
Nothing
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatLeqTyCon
, [PredType
x,PredType
y] <- [PredType]
xs
, let (CoreSOP
x',[(PredType, PredType)]
k1) = Writer [(PredType, PredType)] CoreSOP
-> (CoreSOP, [(PredType, PredType)])
forall w a. Writer w a -> (a, w)
runWriter (PredType -> Writer [(PredType, PredType)] CoreSOP
normaliseNat PredType
x)
, let (CoreSOP
y',[(PredType, PredType)]
k2) = Writer [(PredType, PredType)] CoreSOP
-> (CoreSOP, [(PredType, PredType)])
forall w a. Writer w a -> (a, w)
runWriter (PredType -> Writer [(PredType, PredType)] CoreSOP
normaliseNat PredType
y)
, let ks :: [(PredType, PredType)]
ks      = [(PredType, PredType)]
k1 [(PredType, PredType)]
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall a. [a] -> [a] -> [a]
++ [(PredType, PredType)]
k2
= case TyCon
tc' of
TyCon
_ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
-> (Either NatEquality NatInEquality, [(PredType, PredType)])
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
forall a. a -> Maybe a
Just (NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
True)), [(PredType, PredType)]
ks)
TyCon
_ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
-> (Either NatEquality NatInEquality, [(PredType, PredType)])
-> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
forall a. a -> Maybe a
Just (NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
False)), [(PredType, PredType)]
ks)
TyCon
_ -> Maybe (Either NatEquality NatInEquality, [(PredType, PredType)])
forall a. Maybe a
Nothing

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

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

unifyItemToPredType :: CoreUnify -> (PredType,Kind)
unifyItemToPredType :: CoreUnify -> (PredType, PredType)
unifyItemToPredType CoreUnify
ui =
(PredType -> PredType -> PredType
mkPrimEqPred PredType
ty1 PredType
ty2,PredType
typeNatKind)
where
ty1 :: PredType
ty1 = case CoreUnify
ui of
SubstItem {TcTyVar
CoreSOP
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
siSOP :: CoreSOP
siVar :: TcTyVar
..} -> TcTyVar -> PredType
mkTyVarTy TcTyVar
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 -> PredType
reifySOP CoreSOP
siLHS
ty2 :: PredType
ty2 = case CoreUnify
ui of
SubstItem {TcTyVar
CoreSOP
siSOP :: CoreSOP
siVar :: TcTyVar
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
..} -> CoreSOP -> PredType
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 -> PredType
reifySOP CoreSOP
siRHS

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

evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic :: Ct
-> Set CType
-> [(PredType, PredType)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW [(PredType, PredType)]
preds = case PredType -> Pred
classifyPredType (PredType -> Pred) -> PredType -> Pred
forall a b. (a -> b) -> a -> b
\$ CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType) -> CtEvidence -> PredType
forall a b. (a -> b) -> a -> b
\$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq PredType
t1 PredType
t2 -> do
[Ct]
holeWanteds <- Ct -> [(PredType, PredType)] -> TcPluginM [Ct]
evSubtPreds Ct
ct [(PredType, PredType)]
preds
[Ct]
knWanted <- (CType -> TcPluginM Ct) -> [CType] -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(a -> m b) -> t a -> m (t b)
mapM (Ct -> CType -> TcPluginM Ct
mkKnWanted 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
ctEv :: Coercion
ctEv    = UnivCoProvenance -> Role -> PredType -> PredType -> Coercion
mkUnivCo ([Char] -> UnivCoProvenance
PluginProv [Char]
"ghc-typelits-natnormalise") Role
Nominal PredType
t1 PredType
t2
#if MIN_VERSION_ghc(8,5,0)
Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
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))
#else
return (Just ((EvCoercion ctEv, ct),newWant))
#endif
Pred
_ -> Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
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 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 PredType
ty) = do
Class
kc_clas <- Name -> TcPluginM Class
tcLookupClass Name
knownNatClassName
let kn_pred :: PredType
kn_pred = Class -> [PredType] -> PredType
mkClassPred Class
kc_clas [PredType
ty]
CtEvidence
wantedCtEv <- CtLoc -> PredType -> TcPluginM CtEvidence
TcPluginM.newWanted (Ct -> CtLoc
ctLoc Ct
ct) PredType
kn_pred
let wanted' :: Ct
wanted' = CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
ct) CtEvidence
wantedCtEv
Ct -> TcPluginM Ct
forall (m :: * -> *) a. Monad m => a -> m a
return Ct
wanted'

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