{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module GHC.TypeLits.Normalise
( plugin )
where
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)
#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
import GHC.TypeLits.Normalise.SOP
import GHC.TypeLits.Normalise.Unify
#if MIN_VERSION_ghc(9,2,0)
typeNatKind :: Type
typeNatKind = 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 TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
Maybe TyCon
_ -> Bool
False
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)
-> ([String] -> Maybe [Opts -> Opts]) -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe (Opts -> Opts))
-> [String] -> Maybe [Opts -> Opts]
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" = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { negNumbers :: Bool
negNumbers = Bool
True })
parseArgument (String -> Maybe Word
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe Word)
-> (String -> Maybe String) -> String -> Maybe Word
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
"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 String
_ = 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 = String -> TcPlugin -> TcPlugin
tracePlugin String
"ghc-typelits-natnormalise"
TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin { tcPluginInit :: TcPluginM ExtraDefs
tcPluginInit = TcPluginM ExtraDefs
lookupExtraDefs
, tcPluginSolve :: ExtraDefs -> TcPluginSolver
tcPluginSolve = Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts
, tcPluginStop :: ExtraDefs -> TcPluginM ()
tcPluginStop = TcPluginM () -> ExtraDefs -> 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 }
type = (IORef (Set CType), TyCon)
lookupExtraDefs :: TcPluginM ExtraDefs
= do
IORef (Set CType)
ref <- IO (IORef (Set CType)) -> TcPluginM (IORef (Set CType))
forall a. IO a -> TcPluginM a
tcPluginIO (Set CType -> IO (IORef (Set CType))
forall a. a -> IO (IORef a)
newIORef Set CType
forall a. Set a
empty)
#if !MIN_VERSION_ghc(9,2,0)
ExtraDefs -> TcPluginM ExtraDefs
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef (Set CType)
ref, TyCon
typeNatLeqTyCon)
#else
md <- lookupModule myModule myPackage
ordCond <- look md "OrdCond"
return (ref, ordCond)
where
look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
myModule = mkModuleName "Data.Type.Ord"
myPackage = fsLit "base"
#endif
decideEqualSOP
:: Opts
-> ExtraDefs
-> [Ct]
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginResult
decideEqualSOP :: Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts (IORef (Set CType)
gen'd,TyCon
ordCond) [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
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 =
((Ct, (Type, EvTerm, [Type])) -> Bool)
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ct
_,(Type
_,EvTerm
_,[Type]
v)) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
v Bool -> Bool -> Bool
|| Opts -> Bool
negNumbers Opts
opts) ([(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))])
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> b) -> a -> b
$
Opts
-> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts TyCon
ordCond Set CType
done [Ct]
simplGivens
newlyDone :: [CType]
newlyDone = ((Ct, (Type, EvTerm, [Type])) -> CType)
-> [(Ct, (Type, EvTerm, [Type]))] -> [CType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(Type
prd, EvTerm
_,[Type]
_)) -> Type -> CType
CType Type
prd) [(Ct, (Type, EvTerm, [Type]))]
reds
IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$
IORef (Set CType) -> (Set CType -> Set CType) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Set CType)
gen'd ((Set CType -> Set CType) -> IO ())
-> (Set CType -> Set CType) -> IO ()
forall a b. (a -> b) -> a -> b
$ Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
union ([CType] -> Set CType
forall a. Ord a => [a] -> Set a
fromList [CType]
newlyDone)
[Ct]
newGivens <- [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
reds (((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
origCt) (CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> EvTerm -> TcPluginM CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [Ct]
newGivens)
decideEqualSOP Opts
opts (IORef (Set CType)
gen'd,TyCon
ordCond) [Ct]
givens [Ct]
deriveds [Ct]
wanteds = do
#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 :: [(TyVar, Type)]
subst = ([(TyVar, Type)], [Ct]) -> [(TyVar, Type)]
forall a b. (a, b) -> a
fst (([(TyVar, Type)], [Ct]) -> [(TyVar, Type)])
-> ([(TyVar, Type)], [Ct]) -> [(TyVar, Type)]
forall a b. (a -> b) -> a -> b
$ [((TyVar, Type), Ct)] -> ([(TyVar, Type)], [Ct])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((TyVar, Type), Ct)] -> ([(TyVar, Type)], [Ct]))
-> [((TyVar, Type), Ct)] -> ([(TyVar, Type)], [Ct])
forall a b. (a -> b) -> a -> b
$ [Ct] -> [((TyVar, Type), 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,
[(TyVar, Type)] -> Ct -> Ct
TcPluginM.substCt [(TyVar, Type)]
subst Ct
ct
)
) [Ct]
wanteds
#else
let wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds
simplGivens <- mapM zonkCt givens
#endif
let wanteds1 :: [Ct]
wanteds1 = (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
wanteds2 :: [Ct]
wanteds2 = case [Ct]
wanteds1 of
[] -> []
[Ct]
w -> [Ct]
w [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
deriveds
unit_wanteds :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds = (Ct
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)]))
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyCon
-> Ct
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality TyCon
ordCond) [Ct]
wanteds2
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
. (\Type
p -> Type -> Bool
isEqPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqPrimPred Type
p) (Type -> Bool) -> ((OrigCt, Ct) -> Type) -> (OrigCt, Ct) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred (CtEvidence -> Type)
-> ((OrigCt, Ct) -> CtEvidence) -> (OrigCt, Ct) -> Type
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
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 = ((Ct, (Type, EvTerm, [Type])) -> CType)
-> [(Ct, (Type, EvTerm, [Type]))] -> [CType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ct
_,(Type
prd, EvTerm
_,[Type]
_)) -> Type -> CType
CType Type
prd) [(Ct, (Type, EvTerm, [Type]))]
redGs
[Ct]
redGivens <- [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
redGs (((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
origCt) (CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> EvTerm -> TcPluginM CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
[(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
<- [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> [(Ct, (EvTerm, [(Type, Type)], [Ct]))])
-> TcPluginM [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> TcPluginM [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
((OrigCt, Ct)
-> TcPluginM (Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))))
-> [(OrigCt, Ct)]
-> TcPluginM [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
(\(OrigCt
origCt, Ct
ct) -> ((EvTerm, [(Type, Type)], [Ct])
-> (Ct, (EvTerm, [(Type, Type)], [Ct])))
-> Maybe (EvTerm, [(Type, Type)], [Ct])
-> Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OrigCt -> Ct
runOrigCt OrigCt
origCt,) (Maybe (EvTerm, [(Type, Type)], [Ct])
-> Maybe (Ct, (EvTerm, [(Type, Type)], [Ct])))
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
-> TcPluginM (Maybe (Ct, (EvTerm, [(Type, Type)], [Ct])))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
[Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr ([Ct]
simplGivens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
redGivens) Ct
ct
)
[(OrigCt, Ct)]
nonEqs
if [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_wanteds Bool -> Bool -> Bool
&& [(Ct, (EvTerm, [(Type, Type)], [Ct]))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
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
[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, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (Type, EvTerm, [Type]))]
redGs (((Ct, (Type, EvTerm, [Type])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM [Ct])
-> TcPluginM [[Ct]]
forall a b. (a -> b) -> a -> b
$ \(Ct
ct, (Type
_,EvTerm
_, [Type]
ws)) -> [Type] -> (Type -> TcPluginM Ct) -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
ws ((Type -> TcPluginM Ct) -> TcPluginM [Ct])
-> (Type -> TcPluginM Ct) -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$
(CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CtLoc -> CtEvidence -> Ct
mkNonCanonical' (Ct -> CtLoc
ctLoc Ct
ct)) (TcPluginM CtEvidence -> TcPluginM Ct)
-> (Type -> TcPluginM CtEvidence) -> Type -> TcPluginM Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> Type -> TcPluginM CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct)
IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$
IORef (Set CType) -> (Set CType -> Set CType) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Set CType)
gen'd ((Set CType -> Set CType) -> IO ())
-> (Set CType -> Set CType) -> IO ()
forall a b. (a -> b) -> a -> b
$ Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
union ([CType] -> Set CType
forall a. Ord a => [a] -> Set a
fromList [CType]
newlyDone)
let unit_givens :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
unit_givens = (Ct
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)]))
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyCon
-> Ct
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality TyCon
ordCond) [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" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
[((EvTerm, Ct), [Ct])]
reds <- [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> ((Ct, (EvTerm, [(Type, Type)], [Ct]))
-> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds (((Ct, (EvTerm, [(Type, Type)], [Ct]))
-> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])])
-> ((Ct, (EvTerm, [(Type, Type)], [Ct]))
-> TcPluginM ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt,(EvTerm
term, [(Type, Type)]
ws, [Ct]
wDicts)) -> do
[Ct]
wants <- Ct -> [(Type, Type)] -> TcPluginM [Ct]
evSubtPreds Ct
origCt ([(Type, Type)] -> TcPluginM [Ct])
-> [(Type, Type)] -> TcPluginM [Ct]
forall a b. (a -> b) -> a -> b
$ Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(Type, Type)]
ws
((EvTerm, Ct), [Ct]) -> TcPluginM ((EvTerm, Ct), [Ct])
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm
term, Ct
origCt), [Ct]
wDicts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
wants)
case SimplifyResult
sr of
Simplified [((EvTerm, Ct), [Ct])]
evs -> do
let simpld :: [((EvTerm, Ct), [Ct])]
simpld = (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (((EvTerm, Ct), [Ct]) -> Bool) -> ((EvTerm, Ct), [Ct]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Bool
isGiven (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs
simpld1 :: [((EvTerm, Ct), [Ct])]
simpld1 = case (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds of
[] -> []
[((EvTerm, Ct), [Ct])]
_ -> [((EvTerm, Ct), [Ct])]
simpld
([(EvTerm, Ct)]
solved',[Ct]
newWanteds) = ([[Ct]] -> [Ct])
-> ([(EvTerm, Ct)], [[Ct]]) -> ([(EvTerm, Ct)], [Ct])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]]))
-> [((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [((EvTerm, Ct), [Ct])]
simpld1 [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds)
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 (Ct, CoreSOP, CoreSOP) NatInEquality
eq -> TcPluginResult -> TcPluginM TcPluginResult
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (\Type
p -> Type -> Bool
isEqPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqPrimPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqPredClass Type
p) Type
prd
]
in ((Ct, (Type, EvTerm, [Type])) -> Bool)
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a. (a -> Bool) -> [a] -> [a]
filter
(\(Ct
_, (Type
prd, EvTerm
_, [Type]
_)) ->
CType -> Set CType -> Bool
forall a. Ord a => a -> Set a -> Bool
notMember (Type -> CType
CType Type
prd) Set CType
done
)
([(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))])
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> b) -> a -> b
$ (Ct -> Maybe (Ct, (Type, EvTerm, [Type])))
-> [Ct] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
(\Ct
ct -> (Ct
ct,) ((Type, EvTerm, [Type]) -> (Ct, (Type, EvTerm, [Type])))
-> Maybe (Type, EvTerm, [Type])
-> Maybe (Ct, (Type, EvTerm, [Type]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Opts -> TyCon -> [Ct] -> Ct -> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts TyCon
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) =
Writer [(Type, Type)] (Maybe Type) -> (Maybe Type, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (Maybe Type)
-> (Maybe Type, [(Type, Type)]))
-> Writer [(Type, Type)] (Maybe Type)
-> (Maybe Type, [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere (Type -> Writer [(Type, Type)] (Maybe Type))
-> Type -> Writer [(Type, Type)] (Maybe Type)
forall a b. (a -> b) -> a -> b
$
CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
ws' :: [Type]
ws' = [ Type
p
| (Type
p, Type
_) <- Opts -> TyCon -> [(Type, Type)] -> [(Type, Type)]
subToPred Opts
opts TyCon
ordCond [(Type, Type)]
ws
, (Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Bool
`eqType` Type
p)(Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
simplGivens
]
Type
pred' <- Maybe Type
mans
(Type, EvTerm, [Type]) -> Maybe (Type, EvTerm, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
pred', CtEvidence -> Type -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
ct) Type
pred', [Type]
ws')
fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality :: Either (Ct, CoreSOP, CoreSOP) NatInEquality -> Ct
fromNatEquality (Left (Ct
ct, CoreSOP
_, CoreSOP
_)) = Ct
ct
fromNatEquality (Right (Ct
ct, (CoreSOP, CoreSOP, Bool)
_)) = Ct
ct
reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr [Ct]
givens Ct
ct = do
let pred0 :: Type
pred0 = CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
(Maybe Type
mans, [(Type, Type)]
tests) = Writer [(Type, Type)] (Maybe Type) -> (Maybe Type, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (Maybe Type)
-> (Maybe Type, [(Type, Type)]))
-> Writer [(Type, Type)] (Maybe Type)
-> (Maybe Type, [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere Type
pred0
case Maybe Type
mans of
Maybe Type
Nothing -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. Maybe a
Nothing
Just Type
pred' -> do
case (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Type -> Type -> Bool
`eqType` Type
pred') (Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
givens of
Maybe Ct
Nothing -> case Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred' of
Just (Class
cls,[Type]
_) | Class -> Name
className Class
cls Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
knownNatClassName -> do
TyVar
evVar <- Type -> TcPluginM TyVar
newEvVar Type
pred'
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))
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
Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(Type, Type)], [Ct])
-> Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. a -> Maybe a
Just (EvTerm
ev, [(Type, Type)]
tests, [Ct
wDict]))
Maybe (Class, [Type])
_ -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. Maybe a
Nothing
Just Ct
c -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(Type, Type)], [Ct])
-> Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. a -> Maybe a
Just (CtEvidence -> Type -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
c) Type
pred0, [(Type, Type)]
tests, []))
toReducedDict :: CtEvidence -> PredType -> EvTerm
toReducedDict :: CtEvidence -> Type -> EvTerm
toReducedDict CtEvidence
ct Type
pred' =
let pred0 :: Type
pred0 = CtEvidence -> Type
ctEvPred CtEvidence
ct
evCo :: Coercion
evCo = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (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
$$ [((EvTerm, Ct), [Ct])] -> 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
<+> Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SDoc
forall a. Outputable a => a -> SDoc
ppr Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq
simplifyNats
:: Opts
-> TyCon
-> [(Either NatEquality NatInEquality,[(Type,Type)])]
-> [(Either NatEquality NatInEquality,[(Type,Type)])]
-> 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 = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)]))
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a b. (a -> b) -> [a] -> [b]
map (([(Type, Type)] -> [(Type, Type)])
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a b. a -> b -> a
const ([] :: [(Type,Type)]))) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG
([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs,[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
otherEqs) = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Bool)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
[(Type, Type)])],
[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Bool
forall {a} {v} {c} {v} {c} {b} {b}.
(Either (a, SOP v c, SOP v c) b, b) -> Bool
isVarEqs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG1
fancyGivens :: [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
[(Type, Type)])]])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
[(Type, Type)])]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality,
[(Type, Type)])]]
forall {v} {a} {c} {c} {a} {c} {c} {c} {b}.
Eq v =>
[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
makeGivensSet [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
otherEqs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs
case [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs of
[] -> do
let eqs :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs = [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
otherEqs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"simplifyNats" ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs)
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [] [] [] [] [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs
[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
_ -> do
String -> SDoc -> TcPluginM ()
tcPluginTrace (String
"simplifyNats(backtrack: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
-> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")
([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
varEqs)
[SimplifyResult]
allSimplified <- [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult)
-> TcPluginM [SimplifyResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]]
fancyGivens (([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult)
-> TcPluginM [SimplifyResult])
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult)
-> TcPluginM [SimplifyResult]
forall a b. (a -> b) -> a -> b
$ \[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
v -> do
let eqs :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs = [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
v [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsW
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"simplifyNats" ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs)
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [] [] [] [] [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs
SimplifyResult -> TcPluginM SimplifyResult
forall (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 (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
_subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
_leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
_xs [] = SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified [((EvTerm, Ct), [Ct])]
evs)
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs (eq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq@(Left (Ct
ct,CoreSOP
u,CoreSOP
v),[(Type, Type)]
k):[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs') = do
let u' :: CoreSOP
u' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
u
v' :: CoreSOP
v' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
v
UnifyResult
ur <- Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
unifyNats Ct
ct CoreSOP
u' CoreSOP
v'
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"unifyNats result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
case UnifyResult
ur of
UnifyResult
Win -> do
[((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
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 [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs')
UnifyResult
Lose -> if [((EvTerm, Ct), [Ct])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((EvTerm, Ct), [Ct])]
evs Bool -> Bool -> Bool
&& [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
then SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. (a, b) -> a
fst (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq))
else [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
Draw [] -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [] ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. a -> [a] -> [a]
:[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
Draw [CoreUnify]
subst' -> do
Maybe ((EvTerm, Ct), [Ct])
evM <- Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty ((CoreUnify -> (Type, Type)) -> [CoreUnify] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> (Type, Type)
unifyItemToPredType [CoreUnify]
subst' [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
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) = CoreSOP -> CoreSOP -> [(CoreSOP, CoreSOP, Bool)]
forall {a}. a -> a -> [(a, a, Bool)]
eqToLeq CoreSOP
u' CoreSOP
v' [(CoreSOP, CoreSOP, Bool)]
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a. [a] -> [a] -> [a]
++ [(CoreSOP, CoreSOP, Bool)]
leqsG
| Bool
otherwise = [(CoreSOP, CoreSOP, Bool)]
leqsG
case Maybe ((EvTerm, Ct), [Ct])
evM of
Maybe ((EvTerm, Ct), [Ct])
Nothing -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
Just ((EvTerm, Ct), [Ct])
ev ->
[CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples ([CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall v c.
(Ord v, Ord c) =>
[UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst [CoreUnify]
subst' [CoreUnify]
subst [CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall a. [a] -> [a] -> [a]
++ [CoreUnify]
subst')
(((EvTerm, Ct), [Ct])
ev((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) [(CoreSOP, CoreSOP, Bool)]
leqsG' [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs')
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs (eq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq@(Right (Ct
ct,u :: (CoreSOP, CoreSOP, Bool)
u@(CoreSOP
x,CoreSOP
y,Bool
b)),[(Type, Type)]
k):[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs') = do
let u' :: CoreSOP
u' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst ((CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP, CoreSOP, Bool)
u)
x' :: CoreSOP
x' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
x
y' :: CoreSOP
y' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
y
uS :: (CoreSOP, CoreSOP, Bool)
uS = (CoreSOP
x',CoreSOP
y',Bool
b)
leqsG' :: [(CoreSOP, CoreSOP, Bool)]
leqsG' | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = (CoreSOP
x',CoreSOP
y',Bool
b)(CoreSOP, CoreSOP, Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a. a -> [a] -> [a]
:[(CoreSOP, CoreSOP, Bool)]
leqsG
| Bool
otherwise = [(CoreSOP, CoreSOP, Bool)]
leqsG
ineqs :: [(CoreSOP, CoreSOP, Bool)]
ineqs = [[(CoreSOP, CoreSOP, Bool)]] -> [(CoreSOP, CoreSOP, Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(CoreSOP, CoreSOP, Bool)]
leqsG
, ((CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool))
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ([CoreUnify] -> (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool)
forall {v} {c} {c}.
(Ord v, Ord c) =>
[UnifyItem v c] -> (SOP v c, SOP v c, c) -> (SOP v c, SOP v c, c)
substLeq [CoreUnify]
subst) [(CoreSOP, CoreSOP, Bool)]
leqsG
, (NatInEquality -> (CoreSOP, CoreSOP, Bool))
-> [NatInEquality] -> [(CoreSOP, CoreSOP, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map NatInEquality -> (CoreSOP, CoreSOP, Bool)
forall a b. (a, b) -> b
snd ([Either (Ct, CoreSOP, CoreSOP) NatInEquality] -> [NatInEquality]
forall a b. [Either a b] -> [b]
rights (((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [Either (Ct, CoreSOP, CoreSOP) NatInEquality]
forall a b. (a -> b) -> [a] -> [b]
map (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. (a, b) -> a
fst [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqsG))
]
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"unifyNats(ineq) results" ((Ct, (CoreSOP, CoreSOP, Bool), CoreSOP, [(CoreSOP, CoreSOP, Bool)])
-> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct
ct,(CoreSOP, CoreSOP, Bool)
u,CoreSOP
u',[(CoreSOP, CoreSOP, Bool)]
ineqs))
case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
u') of
Just (Bool
True,Set CType
knW) -> do
[((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, 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
_) | [(Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Type)]
k -> SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. (a, b) -> a
fst (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
eq))
Maybe (Bool, Set CType)
_ -> do
let solvedIneq :: [(Bool, Set CType)]
solvedIneq = (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType))
-> [WriterT (Set CType) Maybe Bool] -> [(Bool, Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
(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]
:
((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]
++
((CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [WriterT (Set CType) Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uS) [(CoreSOP, CoreSOP, Bool)]
ineqs)
smallest :: (Bool, Set CType)
smallest = [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint [(Bool, Set CType)]
solvedIneq
case (Bool, Set CType)
smallest of
(Bool
True,Set CType
kW) -> do
[((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, 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)])
eq(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
forall a. a -> [a] -> [a]
:[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
xs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])]
eqs'
eqToLeq :: a -> a -> [(a, a, Bool)]
eqToLeq a
x a
y = [(a
x,a
y,Bool
True),(a
y,a
x,Bool
True)]
substLeq :: [UnifyItem v c] -> (SOP v c, SOP v c, c) -> (SOP v c, SOP v c, c)
substLeq [UnifyItem v c]
s (SOP v c
x,SOP v c
y,c
b) = ([UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
x, [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
y, c
b)
isVarEqs :: (Either (a, SOP v c, SOP v c) b, b) -> Bool
isVarEqs (Left (a
_,S [P [V v
_]], S [P [V v
_]]), b
_) = Bool
True
isVarEqs (Either (a, SOP v c, SOP v c) b, b)
_ = Bool
False
makeGivensSet :: [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
makeGivensSet [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
otherEqs (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq
= let ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV,[Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsV) = [Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b))]
-> ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)],
[Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers
(((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)))
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b))]
forall a b. (a -> b) -> [a] -> [b]
map ((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b))
forall {a} {a} {c} {c} {b} {b} {a} {c} {c} {a} {c} {c} {c} {b}.
Eq a =>
(Either (a, SOP a c, SOP a c) b, b)
-> (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
matchesVarEq (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq) [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
otherEqs)
([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS,[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS) = [Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> ([(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)],
[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsV
vS :: (Either (a, SOP v c, SOP v c) b, b)
vS = (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> (Either (a, SOP v c, SOP v c) b, b)
forall {a} {v} {c} {v} {c} {b} {b} {c} {c} {b}.
(Either (a, SOP v c, SOP v c) b, b)
-> (Either (a, SOP v c, SOP v c) b, b)
swapVar (Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq
givensLHS :: [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensLHS = case [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS of
[] -> []
[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
_ -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ (((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
varEq(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. a -> [a] -> [a]
:[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS) [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV)]
givensRHS :: [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensRHS = case [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS of
[] -> []
[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
_ -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsRHS [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ ((Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
forall {c} {c} {b}. (Either (a, SOP v c, SOP v c) b, b)
vS(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. a -> [a] -> [a]
:[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsLHS [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
-> [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
forall a. [a] -> [a] -> [a]
++ [(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV)]
in case [Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
mentionsV of
[] -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
noMentionsV]
[Either
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)
(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]
_ -> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensLHS [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
-> [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
forall a. [a] -> [a] -> [a]
++ [[(Either (a, SOP v c, SOP v c) (a, (SOP v c, SOP v c, c)), b)]]
givensRHS
matchesVarEq :: (Either (a, SOP a c, SOP a c) b, b)
-> (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
matchesVarEq (Left (a
_, S [P [V a
v1]], S [P [V a
v2]]),b
_) (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r = case (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r of
(Left (a
_,S [P [V a
v3]],SOP a c
_),b
_)
| a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
| a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
(Left (a
_,SOP a c
_,S [P [V a
v3]]),b
_)
| a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
| a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
(Right (a
_,(S [P [V a
v3]],SOP a c
_,c
_)),b
_)
| a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
| a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
(Right (a
_,(SOP a c
_,S [P [V a
v3]],c
_)),b
_)
| a
v1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
| a
v2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v3 -> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. b -> Either a b
Right ((Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
forall a b. b -> Either a b
Right (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
_ -> (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
-> Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
(Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b))
forall a b. a -> Either a b
Left (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
r
matchesVarEq (Either (a, SOP a c, SOP a c) b, b)
_ (Either (a, SOP a c, SOP a c) (a, (SOP a c, SOP a c, c)), b)
_ = String
-> 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 => 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) =
((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)
_ = String -> (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
| (((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
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 = [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a b. a -> b -> a
const []
| Bool
otherwise = ((Type, Type) -> (Type, Type)) -> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> (Type, Type) -> (Type, Type)
subtractionToPred TyCon
ordCond)
toNatEquality :: TyCon -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
toNatEquality :: TyCon
-> Ct
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
toNatEquality TyCon
ordCond Ct
ct = case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq Type
t1 Type
t2
-> Type
-> Type
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
go Type
t1 Type
t2
Pred
_ -> Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
where
go :: Type
-> Type
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
go (TyConApp TyCon
tc [Type]
xs) (TyConApp TyCon
tc' [Type]
ys)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc'
, [TyCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyCon
tc,TyCon
tc'] [TyCon] -> [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [TyCon
typeNatAddTyCon,TyCon
typeNatSubTyCon
,TyCon
typeNatMulTyCon,TyCon
typeNatExpTyCon])
= case ((Type, Type) -> Bool) -> [(Type, Type)] -> [(Type, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Type, Type) -> Bool) -> (Type, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Bool) -> (Type, Type) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
eqType) ([Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
xs [Type]
ys) of
[(Type
x,Type
y)]
| Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
x)
, Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
y)
, let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
, let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just ((Ct, CoreSOP, CoreSOP)
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. a -> Either a b
Left (Ct
ct, CoreSOP
x', CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
[(Type, Type)]
_ -> Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
#if MIN_VERSION_ghc(9,2,0)
| tc == ordCond
, [_,cmp,lt,eq,gt] <- xs
, TyConApp tcCmpNat [x,y] <- cmp
, tcCmpNat == typeNatCmpTyCon
, TyConApp ltTc [] <- lt
, ltTc == promotedTrueDataCon
, TyConApp eqTc [] <- eq
, eqTc == promotedTrueDataCon
, TyConApp gtTc [] <- gt
, gtTc == promotedFalseDataCon
, let (x',k1) = runWriter (normaliseNat x)
, let (y',k2) = runWriter (normaliseNat y)
, let ks = k1 ++ k2
= case tc' of
_ | tc' == promotedTrueDataCon
-> Just (Right (ct, (x', y', True)), ks)
_ | tc' == promotedFalseDataCon
-> Just (Right (ct, (x', y', False)), ks)
_ -> Nothing
#else
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
ordCond
, [Type
x,Type
y] <- [Type]
xs
, let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
, let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
, let ks :: [(Type, Type)]
ks = [(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
= case TyCon
tc' of
TyCon
_ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
True)), [(Type, Type)]
ks)
TyCon
_ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
False)), [(Type, Type)]
ks)
TyCon
_ -> Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
#endif
go Type
x Type
y
| Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
x)
, Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
y)
, let (CoreSOP
x',[(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
, let (CoreSOP
y',[(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
= (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
-> Maybe
(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just ((Ct, CoreSOP, CoreSOP)
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. a -> Either a b
Left (Ct
ct,CoreSOP
x',CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
| Bool
otherwise
= Maybe (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
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 = ((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> a
fst [(Type, Type)]
preds
#if MIN_VERSION_ghc(8,4,1)
[CoercionHole]
holes <- (Type -> TcPluginM CoercionHole)
-> [Type] -> TcPluginM [CoercionHole]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> TcPluginM CoercionHole
newCoercionHole (Type -> TcPluginM CoercionHole)
-> (Type -> Type) -> Type -> TcPluginM CoercionHole
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Type) -> (Type, Type) -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Type
mkPrimEqPred ((Type, Type) -> Type) -> (Type -> (Type, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, Type)
getEqPredTys) [Type]
predTypes
#else
holes <- replicateM (length preds) newCoercionHole
#endif
[Ct] -> TcPluginM [Ct]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type -> CoercionHole -> Ct) -> [Type] -> [CoercionHole] -> [Ct]
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 (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq Type
t1 Type
t2 -> do
[Ct]
holeWanteds <- Ct -> [(Type, Type)] -> TcPluginM [Ct]
evSubtPreds Ct
ct [(Type, Type)]
preds
[Ct]
knWanted <- (CType -> TcPluginM Ct) -> [CType] -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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 -> Type -> Type -> Coercion
mkUnivCo (String -> UnivCoProvenance
PluginProv String
"ghc-typelits-natnormalise") Role
Nominal Type
t1 Type
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 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
Ct -> TcPluginM Ct
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)