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

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

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

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

For example, this solver can prove the equality between:

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

and

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

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

To use the plugin, add

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

To the header of your file.

== Treating subtraction as addition with a negated number

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

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

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

=== When it leads to unsound behaviour

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

@
(n - 1) + 1 ~ n
@

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

This would allow the following erroneous definition:

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

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

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

=== When it might be Okay

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

When you have:

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

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

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

And you want to define:

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

then the last line will give rise to the constraint:

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

because:

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

In this case it's okay to add

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

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

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

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

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE ExplicitNamespaces    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE ViewPatterns          #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# OPTIONS_HADDOCK show-extensions #-}

module GHC.TypeLits.Normalise
  ( plugin )
where

-- base
import Control.Arrow
  ( second )
import Control.Monad
  ( (<=<) )
import Control.Monad.Trans.Writer.Strict
  ( WriterT(runWriterT), runWriter )
import Data.Either
  ( rights, partitionEithers )
import Data.List
  ( stripPrefix, find, partition )
import qualified Data.List.NonEmpty as NE
import Data.Maybe
  ( mapMaybe, catMaybes, fromMaybe )
import Data.Traversable
  ( for )
import Text.Read
  ( readMaybe )

-- containers
import Data.Set
  ( Set )
import qualified Data.Set as Set
  ( elems, empty )

-- ghc
import GHC.Builtin.Names
  ( knownNatClassName )
import GHC.Builtin.Types.Literals
  ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )

-- ghc-tcplugin-api
import GHC.TcPlugin.API
import GHC.TcPlugin.API.TyConSubst
  ( TyConSubst, mkTyConSubst, splitTyConApp_upTo )
import GHC.Plugins
  ( Plugin(..), defaultPlugin, purePlugin )
import GHC.Utils.Outputable
  ( ($$), (<+>), text, vcat )

-- ghc-typelits-natnormalise
import GHC.TypeLits.Normalise.Compat
import GHC.TypeLits.Normalise.SOP
  ( SOP(S), Product(P), Symbol(V) )
import GHC.TypeLits.Normalise.Unify

--------------------------------------------------------------------------------

-- | To use the plugin, add
--
-- @
-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}
-- @
--
-- To the header of your file.
plugin :: Plugin
plugin :: Plugin
plugin
  = Plugin
defaultPlugin
  { tcPlugin = \ [CommandLineOption]
p -> do Opts
opts <- ((Opts -> Opts) -> Opts -> Opts) -> Opts -> [Opts -> Opts] -> Opts
forall a b. (a -> b -> b) -> b -> [a] -> b
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 ([Opts -> Opts] -> Opts) -> Maybe [Opts -> Opts] -> Maybe Opts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CommandLineOption -> Maybe (Opts -> Opts))
-> [CommandLineOption] -> Maybe [Opts -> Opts]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse CommandLineOption -> Maybe (Opts -> Opts)
parseArgument [CommandLineOption]
p
                         TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPlugin -> Maybe TcPlugin) -> TcPlugin -> Maybe TcPlugin
forall a b. (a -> b) -> a -> b
$ TcPlugin -> TcPlugin
mkTcPlugin (TcPlugin -> TcPlugin) -> TcPlugin -> TcPlugin
forall a b. (a -> b) -> a -> b
$ Opts -> TcPlugin
normalisePlugin Opts
opts
  , pluginRecompile = purePlugin
  }
 where
  parseArgument :: CommandLineOption -> Maybe (Opts -> Opts)
parseArgument CommandLineOption
"allow-negated-numbers" = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { negNumbers = True })
  parseArgument (CommandLineOption -> Maybe Word
forall a. Read a => CommandLineOption -> Maybe a
readMaybe (CommandLineOption -> Maybe Word)
-> (CommandLineOption -> Maybe CommandLineOption)
-> CommandLineOption
-> Maybe Word
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< CommandLineOption -> CommandLineOption -> Maybe CommandLineOption
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix CommandLineOption
"depth=" -> Just Word
depth) = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ Opts
opts -> Opts
opts { depth })
  parseArgument CommandLineOption
_ = Maybe (Opts -> Opts)
forall a. Maybe a
Nothing
  defaultOpts :: Opts
defaultOpts = Opts { negNumbers :: Bool
negNumbers = Bool
False, depth :: Word
depth = Word
5 }

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

normalisePlugin :: Opts -> TcPlugin
normalisePlugin :: Opts -> TcPlugin
normalisePlugin Opts
opts =
  TcPlugin { tcPluginInit :: TcPluginM 'Init ExtraDefs
tcPluginInit    = TcPluginM 'Init ExtraDefs
lookupExtraDefs
           , tcPluginSolve :: ExtraDefs -> TcPluginSolver
tcPluginSolve   = Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts
           , tcPluginRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite = UniqFM TyCon TcPluginRewriter
-> ExtraDefs -> UniqFM TyCon TcPluginRewriter
forall a b. a -> b -> a
const UniqFM TyCon TcPluginRewriter
forall key elt. UniqFM key elt
emptyUFM
           , tcPluginStop :: ExtraDefs -> TcPluginM 'Stop ()
tcPluginStop    = TcPluginM 'Stop () -> ExtraDefs -> TcPluginM 'Stop ()
forall a b. a -> b -> a
const (() -> TcPluginM 'Stop ()
forall a. a -> TcPluginM 'Stop a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           }

data ExtraDefs
  = ExtraDefs
    { ExtraDefs -> LookedUpTyCons
tyCons :: LookedUpTyCons }

lookupExtraDefs :: TcPluginM Init ExtraDefs
lookupExtraDefs :: TcPluginM 'Init ExtraDefs
lookupExtraDefs = do
  LookedUpTyCons
tcs <- TcPluginM 'Init LookedUpTyCons
lookupTyCons
  ExtraDefs -> TcPluginM 'Init ExtraDefs
forall a. a -> TcPluginM 'Init a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraDefs -> TcPluginM 'Init ExtraDefs)
-> ExtraDefs -> TcPluginM 'Init ExtraDefs
forall a b. (a -> b) -> a -> b
$
    ExtraDefs
      { tyCons :: LookedUpTyCons
tyCons = LookedUpTyCons
tcs }

decideEqualSOP
  :: Opts
  -> ExtraDefs
      -- ^ 1. Givens that is already generated.
      --   We have to generate new givens at most once;
      --   otherwise GHC will loop indefinitely.
      --
      --
      --   2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond
      --      For older: TyCon of GHC.TypeLits.<=?
  -> [Ct]
  -> [Ct]
  -> TcPluginM Solve TcPluginSolveResult
-- Simplification phase: Derives /simplified/ givens;
-- we can reduce given constraints like @Show (Foo (n + 2))@
-- to its normal form @Show (Foo (2 + n))@, which is eventually
-- useful in solving phase.
--
-- This helps us to solve /indirect/ constraints;
-- without this phase, we cannot derive, e.g.,
-- @IsVector UVector (Fin (n + 1))@ from
-- @Unbox (1 + n)@!
decideEqualSOP :: Opts -> ExtraDefs -> TcPluginSolver
decideEqualSOP Opts
opts (ExtraDefs { tyCons :: ExtraDefs -> LookedUpTyCons
tyCons = LookedUpTyCons
tcs }) [Ct]
givens [] =
   do
    let givensTyConSubst :: TyConSubst
givensTyConSubst = [Ct] -> TyConSubst
mkTyConSubst [Ct]
givens
        reds :: [(Ct, (Type, EvTerm, [Type]))]
reds =
          ((Ct, (Type, EvTerm, [Type])) -> Bool)
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a. (a -> Bool) -> [a] -> [a]
filter
            (\(Ct
_,(Type
_,EvTerm
_,[Type]
v)) -> [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
v Bool -> Bool -> Bool
|| Opts -> Bool
negNumbers Opts
opts) ([(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))])
-> [(Ct, (Type, EvTerm, [Type]))] -> [(Ct, (Type, EvTerm, [Type]))]
forall a b. (a -> b) -> a -> b
$
              Opts
-> LookedUpTyCons
-> TyConSubst
-> [Ct]
-> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts LookedUpTyCons
tcs ([Ct] -> TyConSubst
mkTyConSubst [Ct]
givens) [Ct]
givens

    CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"decideEqualSOP Givens {" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
      [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens ]

    [Ct]
newGivens <- [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve Ct)
-> TcPluginM 'Solve [Ct]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Ct, (Type, EvTerm, [Type]))]
reds (((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve Ct)
 -> TcPluginM 'Solve [Ct])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve Ct)
-> TcPluginM 'Solve [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evTerm, [Type]
_)) ->
      CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct)
-> TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> EvTerm -> TcPluginM 'Solve CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evTerm
    -- Try to find contradictory Givens, to improve pattern match warnings.
    SimplifyResult
sr <- Opts
-> LookedUpTyCons
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simplifyNats Opts
opts LookedUpTyCons
tcs [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])]
 -> TcPluginM 'Solve SimplifyResult)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
forall a b. (a -> b) -> a -> b
$ (Ct
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (LookedUpTyCons
-> TyConSubst
-> Ct
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
toNatEquality LookedUpTyCons
tcs TyConSubst
givensTyConSubst) ([Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
newGivens)
    case SimplifyResult
sr of
      Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq -> do
        let contra :: Ct
contra = Either (Ct, CoreSOP, CoreSOP) NatInEquality -> Ct
fromNatEquality Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq
        CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"decideEqualSOP Givens (FAIL) }" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
          [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens
               , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"contra:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
contra  ]
        TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginSolveResult
TcPluginContradiction [Ct
contra]
      Simplified {} -> do
        CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"decideEqualSOP Givens (OK) }" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
          [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens ]
        TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] []

-- Solving phase.
-- Solves in/equalities on Nats and simplifiable constraints
-- containing naturals.
decideEqualSOP Opts
opts (ExtraDefs { tyCons :: ExtraDefs -> LookedUpTyCons
tyCons = LookedUpTyCons
tcs }) [Ct]
givens [Ct]
wanteds0 = do
    [Ct]
deriveds <- TcPluginM 'Solve [Ct]
askDeriveds
    let wanteds :: [Ct]
wanteds = if [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
wanteds0
                  then []
                  else [Ct]
wanteds0 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
deriveds
        givensTyConSubst :: TyConSubst
givensTyConSubst = [Ct] -> TyConSubst
mkTyConSubst [Ct]
givens
        unit_wanteds0 :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds0 = (Ct
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (LookedUpTyCons
-> TyConSubst
-> Ct
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
toNatEquality LookedUpTyCons
tcs TyConSubst
givensTyConSubst) [Ct]
wanteds
        nonEqs :: [Ct]
nonEqs = (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter ( Bool -> Bool
not
                        (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Type
p -> Type -> Bool
isEqPred Type
p Bool -> Bool -> Bool
|| Type -> Bool
isEqClassPred Type
p)
                        (Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred
                        (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence )
                 [Ct]
wanteds
    let newRedGs :: [(Ct, (Type, EvTerm, [Type]))]
newRedGs = Opts
-> LookedUpTyCons
-> TyConSubst
-> [Ct]
-> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst [Ct]
givens
    [Ct]
redGivens <- [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve Ct)
-> TcPluginM 'Solve [Ct]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Ct, (Type, EvTerm, [Type]))]
newRedGs (((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve Ct)
 -> TcPluginM 'Solve [Ct])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve Ct)
-> TcPluginM 'Solve [Ct]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt, (Type
pred', EvTerm
evExpr, [Type]
_)) ->
      CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct)
-> TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> EvTerm -> TcPluginM 'Solve CtEvidence
newGiven (Ct -> CtLoc
ctLoc Ct
origCt) Type
pred' EvTerm
evExpr
    [(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 'Solve [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> TcPluginM 'Solve [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct
 -> TcPluginM 'Solve (Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))))
-> [Ct]
-> TcPluginM 'Solve [Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Ct
ct -> ((EvTerm, [(Type, Type)], [Ct])
 -> (Ct, (EvTerm, [(Type, Type)], [Ct])))
-> Maybe (EvTerm, [(Type, Type)], [Ct])
-> Maybe (Ct, (EvTerm, [(Type, Type)], [Ct]))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ct
ct,) (Maybe (EvTerm, [(Type, Type)], [Ct])
 -> Maybe (Ct, (EvTerm, [(Type, Type)], [Ct])))
-> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
-> TcPluginM 'Solve (Maybe (Ct, (EvTerm, [(Type, Type)], [Ct])))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                    TyConSubst
-> [Ct]
-> Ct
-> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr TyConSubst
givensTyConSubst ([Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
redGivens) Ct
ct)
                            [Ct]
nonEqs

    CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"decideEqualSOP Wanteds {" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
       [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens
            , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"new reduced givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
redGivens
            , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"newRedGs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Ct, (Type, EvTerm, [Type]))] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Ct, (Type, EvTerm, [Type]))]
newRedGs
            , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> Char -> CommandLineOption
forall a. Int -> a -> [a]
replicate Int
80 Char
'-'
            , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
wanteds
            , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"unit_wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds0
            , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"reducible_wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Ct, (EvTerm, [(Type, Type)], [Ct]))] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
            ]
    if [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds0 Bool -> Bool -> Bool
&& [(Ct, (EvTerm, [(Type, Type)], [Ct]))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
    then TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] []
    else do
        -- Since reducible Wanteds also can have some negation/subtraction
        -- subterms, we have to make sure appropriate inequalities to hold.
        -- Here, we generate such additional inequalities for reduction
        -- that is to be added to new [W]anteds.
        [Ct]
ineqForRedWants <- ([[Ct]] -> [Ct])
-> TcPluginM 'Solve [[Ct]] -> TcPluginM 'Solve [Ct]
forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (TcPluginM 'Solve [[Ct]] -> TcPluginM 'Solve [Ct])
-> TcPluginM 'Solve [[Ct]] -> TcPluginM 'Solve [Ct]
forall a b. (a -> b) -> a -> b
$ [(Ct, (Type, EvTerm, [Type]))]
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve [Ct])
-> TcPluginM 'Solve [[Ct]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Ct, (Type, EvTerm, [Type]))]
newRedGs (((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve [Ct])
 -> TcPluginM 'Solve [[Ct]])
-> ((Ct, (Type, EvTerm, [Type])) -> TcPluginM 'Solve [Ct])
-> TcPluginM 'Solve [[Ct]]
forall a b. (a -> b) -> a -> b
$ \(Ct
ct, (Type
_,EvTerm
_, [Type]
ws)) -> [Type] -> (Type -> TcPluginM 'Solve Ct) -> TcPluginM 'Solve [Ct]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Type]
ws ((Type -> TcPluginM 'Solve Ct) -> TcPluginM 'Solve [Ct])
-> (Type -> TcPluginM 'Solve Ct) -> TcPluginM 'Solve [Ct]
forall a b. (a -> b) -> a -> b
$
          (CtEvidence -> Ct)
-> TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct
forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CtEvidence -> Ct
mkNonCanonical (TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct)
-> (Type -> TcPluginM 'Solve CtEvidence)
-> Type
-> TcPluginM 'Solve Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct)
        let unit_givens :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_givens = (Ct
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (LookedUpTyCons
-> TyConSubst
-> Ct
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
toNatEquality LookedUpTyCons
tcs TyConSubst
givensTyConSubst) [Ct]
givens
            unit_wanteds :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds = [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds0 [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a. [a] -> [a] -> [a]
++ (Ct
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> [Ct]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (LookedUpTyCons
-> TyConSubst
-> Ct
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
toNatEquality LookedUpTyCons
tcs TyConSubst
givensTyConSubst) [Ct]
ineqForRedWants
        SimplifyResult
sr <- Opts
-> LookedUpTyCons
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simplifyNats Opts
opts LookedUpTyCons
tcs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_givens [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds
        CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
        [((EvTerm, Ct), [Ct])]
reds <- [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
-> ((Ct, (EvTerm, [(Type, Type)], [Ct]))
    -> TcPluginM 'Solve ((EvTerm, Ct), [Ct]))
-> TcPluginM 'Solve [((EvTerm, Ct), [Ct])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds (((Ct, (EvTerm, [(Type, Type)], [Ct]))
  -> TcPluginM 'Solve ((EvTerm, Ct), [Ct]))
 -> TcPluginM 'Solve [((EvTerm, Ct), [Ct])])
-> ((Ct, (EvTerm, [(Type, Type)], [Ct]))
    -> TcPluginM 'Solve ((EvTerm, Ct), [Ct]))
-> TcPluginM 'Solve [((EvTerm, Ct), [Ct])]
forall a b. (a -> b) -> a -> b
$ \(Ct
origCt,(EvTerm
term, [(Type, Type)]
ws, [Ct]
wDicts)) -> do
          [Ct]
wants <- CtLoc -> [Type] -> TcPluginM 'Solve [Ct]
evSubtPreds (Ct -> CtLoc
ctLoc Ct
origCt) ([Type] -> TcPluginM 'Solve [Ct])
-> [Type] -> TcPluginM 'Solve [Ct]
forall a b. (a -> b) -> a -> b
$ Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(Type, Type)]
ws
          ((EvTerm, Ct), [Ct]) -> TcPluginM 'Solve ((EvTerm, Ct), [Ct])
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm
term, Ct
origCt), [Ct]
wDicts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
wants)
        case SimplifyResult
sr of
          Simplified [((EvTerm, Ct), [Ct])]
evs -> do
            let simpld :: [((EvTerm, Ct), [Ct])]
simpld = (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (((EvTerm, Ct), [Ct]) -> Bool) -> ((EvTerm, Ct), [Ct]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Bool
isGiven (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs
                -- Only solve a Derived when there are Wanteds in play
                simpld1 :: [((EvTerm, Ct), [Ct])]
simpld1 = case (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((EvTerm
_,Ct
x),[Ct]
_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds of
                            [] -> []
                            [((EvTerm, Ct), [Ct])]
_  -> [((EvTerm, Ct), [Ct])]
simpld
                ([(EvTerm, Ct)]
solved,[Ct]
newWanteds) = ([[Ct]] -> [Ct])
-> ([(EvTerm, Ct)], [[Ct]]) -> ([(EvTerm, Ct)], [Ct])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]]))
-> [((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [((EvTerm, Ct), [Ct])]
simpld1 [((EvTerm, Ct), [Ct])]
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. [a] -> [a] -> [a]
++ [((EvTerm, Ct), [Ct])]
reds)

            CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"decideEqualSOP Wanteds }" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
               [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"new reduced givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
redGivens
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"newRedGs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Ct, (Type, EvTerm, [Type]))] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Ct, (Type, EvTerm, [Type]))]
newRedGs
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> Char -> CommandLineOption
forall a. Int -> a -> [a]
replicate Int
80 Char
'-'
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
wanteds
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"ineqForRedWants:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
ineqForRedWants
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"unit_wanteds0:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])]]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr ((Ct
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> [Ct]
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])]]
forall a b. (a -> b) -> [a] -> [b]
map (LookedUpTyCons
-> TyConSubst
-> Ct
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
toNatEquality LookedUpTyCons
tcs TyConSubst
givensTyConSubst) [Ct]
wanteds)
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"unit_wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
unit_wanteds
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"reducible_wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Ct, (EvTerm, [(Type, Type)], [Ct]))] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Ct, (EvTerm, [(Type, Type)], [Ct]))]
reducible_wanteds
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> Char -> CommandLineOption
forall a. Int -> a -> [a]
replicate Int
80 Char
'='
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"solved:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(EvTerm, Ct)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(EvTerm, Ct)]
solved
                    , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"newWanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
newWanteds
                    ]

            TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [(EvTerm, Ct)]
solved ([Ct] -> TcPluginSolveResult) -> [Ct] -> TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [Ct]
newWanteds)
          Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq -> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginSolveResult
TcPluginContradiction [Either (Ct, CoreSOP, CoreSOP) NatInEquality -> Ct
fromNatEquality Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq])

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

reduceGivens :: Opts -> LookedUpTyCons
             -> TyConSubst
             -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]
reduceGivens :: Opts
-> LookedUpTyCons
-> TyConSubst
-> [Ct]
-> [(Ct, (Type, EvTerm, [Type]))]
reduceGivens Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst [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
isEqClassPred Type
p ) Type
prd
        ]
  in (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
-> LookedUpTyCons
-> TyConSubst
-> [Ct]
-> Ct
-> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst [Ct]
givens Ct
ct)
      [Ct]
nonEqs

tryReduceGiven
  :: Opts -> LookedUpTyCons
  -> TyConSubst
  -> [Ct] -> Ct
  -> Maybe (PredType, EvTerm, [PredType])
tryReduceGiven :: Opts
-> LookedUpTyCons
-> TyConSubst
-> [Ct]
-> Ct
-> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst [Ct]
simplGivens Ct
ct = do
    let (Maybe (Type, [Coercion])
mans, [(Type, Type)]
ws) =
          Writer [(Type, Type)] (Maybe (Type, [Coercion]))
-> (Maybe (Type, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (Maybe (Type, [Coercion]))
 -> (Maybe (Type, [Coercion]), [(Type, Type)]))
-> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
-> (Maybe (Type, [Coercion]), [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ TyConSubst
-> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
normaliseNatEverywhere TyConSubst
givensTyConSubst (Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion])))
-> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
forall a b. (a -> b) -> a -> b
$
          CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
        ws' :: [Type]
ws' = [ Type
p
              | Type
p <- Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(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
              ]
        -- deps = unitDVarSet (ctEvId ct)
    (Type
pred', [Coercion]
deps) <- Maybe (Type, [Coercion])
mans
    (Type, EvTerm, [Type]) -> Maybe (Type, EvTerm, [Type])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
pred', CtEvidence -> Type -> [Coercion] -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
ct) Type
pred' [Coercion]
deps, [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 :: TyConSubst -> [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr :: TyConSubst
-> [Ct]
-> Ct
-> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr TyConSubst
givensTyConSubst [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, [Coercion])
mans, [(Type, Type)]
tests) = Writer [(Type, Type)] (Maybe (Type, [Coercion]))
-> (Maybe (Type, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (Maybe (Type, [Coercion]))
 -> (Maybe (Type, [Coercion]), [(Type, Type)]))
-> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
-> (Maybe (Type, [Coercion]), [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ TyConSubst
-> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
normaliseNatEverywhere TyConSubst
givensTyConSubst Type
pred0

      -- Even if we didn't rewrite the Wanted,
      -- we may still be able to solve it from a (rewritten) Given.
      (Type
pred', [Coercion]
deps') = (Type, [Coercion])
-> Maybe (Type, [Coercion]) -> (Type, [Coercion])
forall a. a -> Maybe a -> a
fromMaybe (Type
pred0, []) Maybe (Type, [Coercion])
mans
  case (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Type -> Type -> Bool
`eqType` Type
pred') (Type -> Bool) -> (Ct -> Type) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
givens of
    -- No existing evidence found
    Maybe Ct
Nothing
      | ClassPred Class
cls [Type]
_ <- Type -> Pred
classifyPredType Type
pred'
      , Class -> Name
className Class
cls Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
knownNatClassName

      -- We actually did do some rewriting/normalisation.
      , Just {} <- Maybe (Type, [Coercion])
mans
      -> do
          -- Create new evidence binding for normalized class constraint
          Ct
wtdDictCt <- CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct)
-> TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct) Type
pred'
          -- Evidence for current wanted is simply the coerced binding for
          -- the new binding
          let evCo :: Coercion
evCo = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-natnormalise"
                       Role
Representational
                       [Coercion]
deps'
                       Type
pred' Type
pred0
              ev :: EvExpr
ev = EvExpr -> Coercion -> EvExpr
evCast (TyVar -> EvExpr
evId (TyVar -> EvExpr) -> TyVar -> EvExpr
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Ct -> TyVar
Ct -> TyVar
ctEvId Ct
wtdDictCt) Coercion
evCo
          -- Use newly created coerced wanted as evidence, and emit the
          -- normalized wanted as a new constraint to solve.
          Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(Type, Type)], [Ct])
-> Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. a -> Maybe a
Just (EvExpr -> EvTerm
EvExpr EvExpr
ev, [(Type, Type)]
tests, [Ct
wtdDictCt]))
      | Bool
otherwise
      -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. Maybe a
Nothing
    -- Use existing evidence
    Just Ct
c  -> Maybe (EvTerm, [(Type, Type)], [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [(Type, Type)], [Ct])
-> Maybe (EvTerm, [(Type, Type)], [Ct])
forall a. a -> Maybe a
Just (CtEvidence -> Type -> [Coercion] -> EvTerm
toReducedDict (Ct -> CtEvidence
ctEvidence Ct
c) Type
pred0 [Coercion]
deps', [(Type, Type)]
tests, []))

toReducedDict :: CtEvidence -> PredType -> [Coercion] -> EvTerm
toReducedDict :: CtEvidence -> Type -> [Coercion] -> EvTerm
toReducedDict CtEvidence
ct Type
pred' [Coercion]
deps' =
  let pred0 :: Type
pred0 = CtEvidence -> Type
ctEvPred CtEvidence
ct
      evCo :: Coercion
evCo = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-natnormalise"
              Role
Representational
              [Coercion]
deps'
              Type
pred0 Type
pred'
      ev :: EvExpr
ev = EvExpr -> Coercion -> EvExpr
evCast (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ct) Coercion
evCo
  in EvExpr -> EvTerm
EvExpr EvExpr
ev

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

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

type NatCt = (Either NatEquality NatInEquality, [(Type,Type)], [Coercion])

simplifyNats
  :: Opts
  -- ^ Allow negated numbers (potentially unsound!)
  -> LookedUpTyCons
  -> [NatCt]
  -- ^ Given constraints
  -> [NatCt]
  -- ^ Wanted constraints
  -> TcPluginM Solve SimplifyResult
simplifyNats :: Opts
-> LookedUpTyCons
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simplifyNats opts :: Opts
opts@Opts {Bool
Word
negNumbers :: Opts -> Bool
depth :: Opts -> Word
negNumbers :: Bool
depth :: Word
..} LookedUpTyCons
tcs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsW = do
    let eqsG1 :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsG1 = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])
 -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion]))
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq, [(Type, Type)]
_, [Coercion]
deps) -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq, [] :: [(Type, Type)], [Coercion]
deps)) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsG
        ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
varEqs, [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
otherEqs) = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])
 -> Bool)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])],
    [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Bool
forall {a} {v} {c} {v} {c} {b} {b} {c}.
(Either (a, SOP v c, SOP v c) b, b, c) -> Bool
isVarEqs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsG1
        fancyGivens :: [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])]]
fancyGivens = ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])
 -> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
       [Coercion])]])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
    [Coercion])
-> [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])]]
makeGivensSet [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
otherEqs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
varEqs
    case [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
varEqs of
      [] -> do
        let eqs :: [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs = [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
otherEqs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsW
        CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"simplifyNats" ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs)
        [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [] [] [] [] [] [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs
      [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
_  -> do
        CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace (CommandLineOption
"simplifyNats(backtrack: " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ Int -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show ([[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])]]
-> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])]]
fancyGivens) CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
")")
                      ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
varEqs)

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

        SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SimplifyResult -> SimplifyResult -> SimplifyResult)
-> SimplifyResult -> [SimplifyResult] -> SimplifyResult
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SimplifyResult -> SimplifyResult -> SimplifyResult
findFirstSimpliedWanted ([((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified []) [SimplifyResult]
allSimplified)
  where
    simples :: [Coercion]
            -> [CoreUnify]
            -> [((EvTerm, Ct), [Ct])]
            -> [(CoreSOP,CoreSOP,Bool)]
            -> [NatCt]
            -> [NatCt]
            -> TcPluginM Solve SimplifyResult
    simples :: [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
_ [CoreUnify]
_subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
_leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
_xs [] = SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified [((EvTerm, Ct), [Ct])]
evs)
    simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs (eq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
eq@(lr :: Either (Ct, CoreSOP, CoreSOP) NatInEquality
lr@(Left (Ct
ct,CoreSOP
u,CoreSOP
v)),[(Type, Type)]
k,[Coercion]
deps2):[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs') = do
      let u' :: CoreSOP
u' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c.
(Outputable v, Outputable 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.
(Outputable v, Outputable 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 'Solve UnifyResult
unifyNats Ct
ct CoreSOP
u' CoreSOP
v'
      CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"unifyNats result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      case UnifyResult
ur of
        UnifyResult
Win -> do
          [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM 'Solve [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct ([Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps2) Set CType
forall a. Set a
Set.empty (Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(Type, Type)]
k)
          [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs')
        UnifyResult
Lose -> if [((EvTerm, Ct), [Ct])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((EvTerm, Ct), [Ct])]
evs Bool -> Bool -> Bool
&& [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs'
                   then SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
lr)
                   else [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs'
        Draw [] -> [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [] ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
eq(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a. a -> [a] -> [a]
:[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs'
        Draw [CoreUnify]
subst' -> do
          Maybe ((EvTerm, Ct), [Ct])
evM <- LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
deps Set CType
forall a. Set a
Set.empty ((CoreUnify -> Type) -> [CoreUnify] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> Type
unifyItemToPredType [CoreUnify]
subst' [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++
                                                Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(Type, Type)]
k)

          CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"unifyNats: Draw (non-empty subst)" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
             [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"subst':" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [CoreUnify] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CoreUnify]
subst'
                  , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"evM:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe ((EvTerm, Ct), [Ct]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe ((EvTerm, Ct), [Ct])
evM ]

          let ([(CoreSOP, CoreSOP, Bool)]
leqsG1, [Coercion]
deps1)
                | 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
                                            , HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion (Ct -> CtEvidence
ctEvidence Ct
ct)Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
deps)
                | Bool
otherwise               = ([(CoreSOP, CoreSOP, Bool)]
leqsG, [Coercion]
deps)
          case Maybe ((EvTerm, Ct), [Ct])
evM of
            Maybe ((EvTerm, Ct), [Ct])
Nothing -> [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps1 [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG1 [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs'
            Just ((EvTerm, Ct), [Ct])
ev ->
              [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion (Ct -> CtEvidence
ctEvidence Ct
ct)Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps2)
                      ([CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall v c.
(Outputable v, Outputable 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)]
leqsG1 [] ([(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a. [a] -> [a] -> [a]
++ [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs')
    simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs (eq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
eq@(lr :: Either (Ct, CoreSOP, CoreSOP) NatInEquality
lr@(Right (Ct
ct,u :: (CoreSOP, CoreSOP, Bool)
u@(CoreSOP
x,CoreSOP
y,Bool
b))),[(Type, Type)]
k,[Coercion]
deps2):[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs') = do
      let u' :: CoreSOP
u'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c.
(Outputable v, Outputable 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.
(Outputable v, Outputable 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.
(Outputable v, Outputable 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}.
(Outputable v, Outputable 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)],
  [Coercion])
 -> Either (Ct, CoreSOP, CoreSOP) NatInEquality)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [Either (Ct, CoreSOP, CoreSOP) NatInEquality]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Either (Ct, CoreSOP, CoreSOP) NatInEquality
lr', [(Type, Type)]
_, [Coercion]
_) -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
lr') [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqsG))
                         ]
      CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"unifyNats(ineq) results" ((Ct, (CoreSOP, CoreSOP, Bool), CoreSOP, [(CoreSOP, CoreSOP, Bool)])
-> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct
ct,(CoreSOP, CoreSOP, Bool)
u,CoreSOP
u',[(CoreSOP, CoreSOP, Bool)]
ineqs))
      case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
u') of
        Just (Bool
True,Set CType
knW)  -> do
          [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM 'Solve [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
deps Set CType
knW (Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(Type, Type)]
k)
          [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs'

        Just (Bool
False,Set CType
_) | [(Type, Type)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Type)]
k -> SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
lr)
        Maybe (Bool, Set CType)
_ -> do
          let solvedIneq :: [(Bool, Set CType)]
solvedIneq = (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType))
-> [WriterT (Set CType) Maybe Bool] -> [(Bool, Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
                 -- it is an inequality that can be instantly solved, such as
                 -- `1 <= x^y`
                 -- OR
                (Word -> (CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool
instantSolveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uWriterT (Set CType) Maybe Bool
-> [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
forall a. a -> [a] -> [a]
:
                Word -> (CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool
instantSolveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uSWriterT (Set CType) Maybe Bool
-> [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
forall a. a -> [a] -> [a]
:
                -- This inequality is either a given constraint, or it is a wanted
                -- constraint, which in normal form is equal to another given
                -- constraint, hence it can be solved.
                -- OR
                ((CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [WriterT (Set CType) Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
u) [(CoreSOP, CoreSOP, Bool)]
ineqs [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
-> [WriterT (Set CType) Maybe Bool]
forall a. [a] -> [a] -> [a]
++
                -- The above, but with valid substitutions applied to the wanted.
                ((CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [WriterT (Set CType) Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uS) [(CoreSOP, CoreSOP, Bool)]
ineqs)
              smallest :: (Bool, Set CType)
smallest = [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint [(Bool, Set CType)]
solvedIneq
          case (Bool, Set CType)
smallest of
            (Bool
True,Set CType
kW) -> do
              let deps' :: [Coercion]
deps' = [Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps2
              [((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 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM 'Solve [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
deps' Set CType
kW (Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(Type, Type)]
k)
              [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps' [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
eqs'
            (Bool, Set CType)
_ -> [Coercion]
-> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> TcPluginM 'Solve SimplifyResult
simples [Coercion]
deps [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
eq(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a. a -> [a] -> [a]
:[(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
xs) [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])]
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.
(Outputable v, Outputable 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.
(Outputable v, Outputable 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, c) -> Bool
isVarEqs (Left (a
_,S [P [V v
_]], S [P [V v
_]]), b
_, c
_) = Bool
True
    isVarEqs (Either (a, SOP v c, SOP v c) b, b, c)
_ = Bool
False

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

    matchesVarEq :: NatCt
                 -> NatCt
                 -> Either NatCt (Either NatCt NatCt)
    matchesVarEq :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
    [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
matchesVarEq (Left (Ct
_, S [P [V TyVar
v1]], S [P [V TyVar
v2]]), [(Type, Type)]
_, [Coercion]
_) r :: (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r@(Either (Ct, CoreSOP, CoreSOP) NatInEquality
e, [(Type, Type)]
_, [Coercion]
_) =
      case Either (Ct, CoreSOP, CoreSOP) NatInEquality
e of
        Left (Ct
_,S [P [V TyVar
v3]],CoreSOP
_)
          | TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. a -> Either a b
Left (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
          | TyVar
v2 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. b -> Either a b
Right (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
        Left (Ct
_,CoreSOP
_,S [P [V TyVar
v3]])
          | TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. a -> Either a b
Left (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
          | TyVar
v2 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. b -> Either a b
Right (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
        Right (Ct
_,(S [P [V TyVar
v3]],CoreSOP
_,Bool
_))
          | TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. a -> Either a b
Left (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
          | TyVar
v2 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. b -> Either a b
Right (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
        Right (Ct
_,(CoreSOP
_,S [P [V TyVar
v3]],Bool
_))
          | TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. a -> Either a b
Left (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
          | TyVar
v2 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v3 -> Either
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
  (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
   [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. b -> Either a b
Right ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
forall a b. b -> Either a b
Right (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r)
        Either (Ct, CoreSOP, CoreSOP) NatInEquality
_ -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a b. a -> Either a b
Left (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
r
    matchesVarEq (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
_ (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
 [Coercion])
_ = CommandLineOption
-> Either
     (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])
     (Either
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion])
        (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
         [Coercion]))
forall a. HasCallStack => CommandLineOption -> a
error CommandLineOption
"internal error"

    swapVar :: (Either (a, SOP v c, SOP v c) b, b, c)
-> (Either (a, SOP v c, SOP v c) b, b, c)
swapVar (Left (a
ct,S [P [V v
v1]], S [P [V v
v2]]), b
ps, c
deps) =
      ((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, c
deps)
    swapVar (Either (a, SOP v c, SOP v c) b, b, c)
_ = CommandLineOption -> (Either (a, SOP v c, SOP v c) b, b, c)
forall a. HasCallStack => CommandLineOption -> a
error CommandLineOption
"internal error"

    findFirstSimpliedWanted :: SimplifyResult -> SimplifyResult -> SimplifyResult
findFirstSimpliedWanted (Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
e)   SimplifyResult
_  = Either (Ct, CoreSOP, CoreSOP) NatInEquality -> SimplifyResult
Impossible Either (Ct, CoreSOP, CoreSOP) NatInEquality
e
    findFirstSimpliedWanted (Simplified [((EvTerm, Ct), [Ct])]
evs) SimplifyResult
s2
      | (((EvTerm, Ct), [Ct]) -> Bool) -> [((EvTerm, Ct), [Ct])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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) -> 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 -> LookedUpTyCons -> [(Type, Type)] -> [PredType]
subToPred :: Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts{Bool
Word
negNumbers :: Opts -> Bool
depth :: Opts -> Word
negNumbers :: Bool
depth :: Word
..} LookedUpTyCons
tcs
  | Bool
negNumbers = [Type] -> [(Type, Type)] -> [Type]
forall a b. a -> b -> a
const []
  | Bool
otherwise  =
    -- Given 'a - b', require 'b <= a'.
    ((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Type
a, Type
b) -> LookedUpTyCons -> Type -> Type -> Type
mkLEqNat LookedUpTyCons
tcs Type
b Type
a)

-- | Extract all Nat equality and inequality constraints from another constraint.
toNatEquality :: LookedUpTyCons -> TyConSubst -> Ct -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]
toNatEquality :: LookedUpTyCons
-> TyConSubst
-> Ct
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
toNatEquality LookedUpTyCons
tcs TyConSubst
givensTyConSubst Ct
ct0
  | Just (((Type
x,Type
y), Maybe Bool
mbLTE), [Coercion]
cos0) <- LookedUpTyCons
-> TyConSubst -> Type -> Maybe (Relation, [Coercion])
isNatRel LookedUpTyCons
tcs TyConSubst
givensTyConSubst Type
pred0
  , let
      ((CoreSOP
x', [Coercion]
cos1),[(Type, Type)]
k1) = Writer [(Type, Type)] (CoreSOP, [Coercion])
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (TyConSubst -> Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat TyConSubst
givensTyConSubst Type
x)
      ((CoreSOP
y', [Coercion]
cos2),[(Type, Type)]
k2) = Writer [(Type, Type)] (CoreSOP, [Coercion])
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (TyConSubst -> Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat TyConSubst
givensTyConSubst Type
y)
      ks :: [(Type, Type)]
ks      = [(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
  = case Maybe Bool
mbLTE of
      Maybe Bool
Nothing ->
        -- Equality constraint: x ~ y
        [((Ct, CoreSOP, CoreSOP)
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. a -> Either a b
Left (Ct
ct0, CoreSOP
x', CoreSOP
y'), [(Type, Type)]
ks, [Coercion]
cos0 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos2)]
      Just Bool
b ->
        -- Inequality constraint: (x <=? y) ~ b
        [(NatInEquality -> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. b -> Either a b
Right (Ct
ct0, (CoreSOP
x', CoreSOP
y', Bool
b)), [(Type, Type)]
ks, [Coercion]
cos0 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos2)]
  | Bool
otherwise
  = case Type -> Pred
classifyPredType Type
pred0 of
      EqPred EqRel
NomEq Type
t1 Type
t2
        -> Type
-> Type
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
goNomEq Type
t1 Type
t2
      Pred
_ -> []
  where
    pred0 :: Type
pred0 = Ct -> Type
ctPred Ct
ct0
    -- x ~ y
    goNomEq :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]
    goNomEq :: Type
-> Type
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
goNomEq Type
lhs Type
rhs
      -- Recur into a TyCon application for TyCons that we **do not** rewrite,
      -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'.
      | Just NonEmpty (TyCon, [Type], [Coercion])
tcApps1 <- TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
splitTyConApp_upTo TyConSubst
givensTyConSubst Type
lhs
      , Just NonEmpty (TyCon, [Type], [Coercion])
tcApps2 <- TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
splitTyConApp_upTo TyConSubst
givensTyConSubst Type
rhs
      , let tcAppsMap1 :: UniqMap TyCon ([Type], [Coercion])
tcAppsMap1 = [(TyCon, ([Type], [Coercion]))]
-> UniqMap TyCon ([Type], [Coercion])
forall k a. Uniquable k => [(k, a)] -> UniqMap k a
listToUniqMap ([(TyCon, ([Type], [Coercion]))]
 -> UniqMap TyCon ([Type], [Coercion]))
-> [(TyCon, ([Type], [Coercion]))]
-> UniqMap TyCon ([Type], [Coercion])
forall a b. (a -> b) -> a -> b
$ ((TyCon, [Type], [Coercion]) -> (TyCon, ([Type], [Coercion])))
-> [(TyCon, [Type], [Coercion])] -> [(TyCon, ([Type], [Coercion]))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TyCon
tc, [Type]
tys, [Coercion]
deps) -> (TyCon
tc, ([Type]
tys, [Coercion]
deps))) ([(TyCon, [Type], [Coercion])] -> [(TyCon, ([Type], [Coercion]))])
-> [(TyCon, [Type], [Coercion])] -> [(TyCon, ([Type], [Coercion]))]
forall a b. (a -> b) -> a -> b
$ NonEmpty (TyCon, [Type], [Coercion])
-> [(TyCon, [Type], [Coercion])]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (TyCon, [Type], [Coercion])
tcApps1
            tcAppsMap2 :: UniqMap TyCon ([Type], [Coercion])
tcAppsMap2 = [(TyCon, ([Type], [Coercion]))]
-> UniqMap TyCon ([Type], [Coercion])
forall k a. Uniquable k => [(k, a)] -> UniqMap k a
listToUniqMap ([(TyCon, ([Type], [Coercion]))]
 -> UniqMap TyCon ([Type], [Coercion]))
-> [(TyCon, ([Type], [Coercion]))]
-> UniqMap TyCon ([Type], [Coercion])
forall a b. (a -> b) -> a -> b
$ ((TyCon, [Type], [Coercion]) -> (TyCon, ([Type], [Coercion])))
-> [(TyCon, [Type], [Coercion])] -> [(TyCon, ([Type], [Coercion]))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TyCon
tc, [Type]
tys, [Coercion]
deps) -> (TyCon
tc, ([Type]
tys, [Coercion]
deps))) ([(TyCon, [Type], [Coercion])] -> [(TyCon, ([Type], [Coercion]))])
-> [(TyCon, [Type], [Coercion])] -> [(TyCon, ([Type], [Coercion]))]
forall a b. (a -> b) -> a -> b
$ NonEmpty (TyCon, [Type], [Coercion])
-> [(TyCon, [Type], [Coercion])]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (TyCon, [Type], [Coercion])
tcApps2
            tcAppPairs :: UniqMap TyCon (([Type], [Coercion]), ([Type], [Coercion]))
tcAppPairs = (([Type], [Coercion])
 -> ([Type], [Coercion])
 -> (([Type], [Coercion]), ([Type], [Coercion])))
-> UniqMap TyCon ([Type], [Coercion])
-> UniqMap TyCon ([Type], [Coercion])
-> UniqMap TyCon (([Type], [Coercion]), ([Type], [Coercion]))
forall a b c k.
(a -> b -> c) -> UniqMap k a -> UniqMap k b -> UniqMap k c
intersectUniqMap_C (,) UniqMap TyCon ([Type], [Coercion])
tcAppsMap1 UniqMap TyCon ([Type], [Coercion])
tcAppsMap2
      , (TyCon
tc, (([Type]
xs, [Coercion]
cos1), ([Type]
ys, [Coercion]
cos2))):[(TyCon, (([Type], [Coercion]), ([Type], [Coercion])))]
_ <- UniqMap TyCon (([Type], [Coercion]), ([Type], [Coercion]))
-> [(TyCon, (([Type], [Coercion]), ([Type], [Coercion])))]
forall k a. UniqMap k a -> [(k, a)]
nonDetUniqMapToList UniqMap TyCon (([Type], [Coercion]), ([Type], [Coercion]))
tcAppPairs
      , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon
tc TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCon
typeNatAddTyCon, TyCon
typeNatSubTyCon, TyCon
typeNatMulTyCon, TyCon
typeNatExpTyCon]
      , let subs :: [(Type, Type)]
subs = ((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)
      = (\ (Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq, [(Type, Type)]
ws, [Coercion]
deps) -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality
eq, [(Type, Type)]
ws, [Coercion]
cos1 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos2 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps)) ((Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
  [Coercion])
 -> (Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion]))
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          ((Type, Type)
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> [(Type, Type)]
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Type
 -> Type
 -> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
      [Coercion])])
-> (Type, Type)
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type
-> Type
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
rewrite) [(Type, Type)]
subs
      | Bool
otherwise
      = Type
-> Type
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
rewrite Type
lhs Type
rhs

    rewrite :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]
    rewrite :: Type
-> Type
-> [(Either (Ct, CoreSOP, CoreSOP) NatInEquality, [(Type, Type)],
     [Coercion])]
rewrite 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', [Coercion]
cos1),[(Type, Type)]
k1) = Writer [(Type, Type)] (CoreSOP, [Coercion])
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (TyConSubst -> Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat TyConSubst
givensTyConSubst Type
x)
      , let ((CoreSOP
y', [Coercion]
cos2),[(Type, Type)]
k2) = Writer [(Type, Type)] (CoreSOP, [Coercion])
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (TyConSubst -> Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat TyConSubst
givensTyConSubst Type
y)
      = [((Ct, CoreSOP, CoreSOP)
-> Either (Ct, CoreSOP, CoreSOP) NatInEquality
forall a b. a -> Either a b
Left (Ct
ct0,CoreSOP
x',CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2, [Coercion]
cos1 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos2)]
      | Bool
otherwise
      = []

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

unifyItemToPredType :: CoreUnify -> PredType
unifyItemToPredType :: CoreUnify -> Type
unifyItemToPredType CoreUnify
ui = Role -> Type -> Type -> Type
mkEqPredRole Role
Nominal Type
ty1 Type
ty2
  where
    ty1 :: Type
ty1 = case CoreUnify
ui of
            SubstItem {TyVar
CoreSOP
siVar :: TyVar
siSOP :: CoreSOP
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
..} -> TyVar -> Type
mkTyVarTy TyVar
siVar
            UnifyItem {CoreSOP
siLHS :: CoreSOP
siRHS :: 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
siLHS
    ty2 :: Type
ty2 = 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
siVar :: TyVar
siSOP :: CoreSOP
..} -> CoreSOP -> Type
reifySOP CoreSOP
siSOP
            UnifyItem {CoreSOP
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: CoreSOP
siRHS :: CoreSOP
..} -> CoreSOP -> Type
reifySOP CoreSOP
siRHS

evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct]
evSubtPreds :: CtLoc -> [Type] -> TcPluginM 'Solve [Ct]
evSubtPreds CtLoc
loc = (Type -> TcPluginM 'Solve Ct) -> [Type] -> TcPluginM 'Solve [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((CtEvidence -> Ct)
-> TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct
forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CtEvidence -> Ct
mkNonCanonical (TcPluginM 'Solve CtEvidence -> TcPluginM 'Solve Ct)
-> (Type -> TcPluginM 'Solve CtEvidence)
-> Type
-> TcPluginM 'Solve Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc)

evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic :: LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
deps Set CType
knW [Type]
preds = do
  [Ct]
holeWanteds <- CtLoc -> [Type] -> TcPluginM 'Solve [Ct]
evSubtPreds (Ct -> CtLoc
ctLoc Ct
ct) [Type]
preds
  [Ct]
knWanted <- (CType -> TcPluginM 'Solve Ct) -> [CType] -> TcPluginM 'Solve [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtLoc -> CType -> TcPluginM 'Solve Ct
mkKnWanted (Ct -> CtLoc
ctLoc Ct
ct)) (Set CType -> [CType]
forall a. Set a -> [a]
Set.elems Set CType
knW)
  let newWant :: [Ct]
newWant = [Ct]
knWanted [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
holeWanteds
  case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
    EqPred EqRel
NomEq Type
t1 Type
t2 ->
      let ctEv :: Coercion
ctEv = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-natnormalise" Role
Nominal [Coercion]
deps Type
t1 Type
t2
      in Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (((EvTerm, Ct), [Ct]) -> Maybe ((EvTerm, Ct), [Ct])
forall a. a -> Maybe a
Just ((EvExpr -> EvTerm
EvExpr (Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
ctEv), Ct
ct),[Ct]
newWant))
    IrredPred Type
p ->
      let t1 :: Type
t1 = TyCon -> [Type] -> Type
mkTyConApp (LookedUpTyCons -> TyCon
c0TyCon LookedUpTyCons
tcs) []
          co :: Coercion
co = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-natnormalise" Role
Representational [Coercion]
deps Type
t1 Type
p
          dcApp :: EvExpr
dcApp = DataCon -> [Type] -> [EvExpr] -> EvExpr
evDataConApp (LookedUpTyCons -> DataCon
c0DataCon LookedUpTyCons
tcs) [] []
       in Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (((EvTerm, Ct), [Ct]) -> Maybe ((EvTerm, Ct), [Ct])
forall a. a -> Maybe a
Just ((EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> Coercion -> EvExpr
evCast EvExpr
dcApp Coercion
co, Ct
ct),[Ct]
newWant))
    Pred
_ -> Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ((EvTerm, Ct), [Ct])
forall a. Maybe a
Nothing

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