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

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

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

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

For example, this solver can prove the equality between:

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

and

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

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

To use the plugin, add

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

To the header of your file.

== Treating subtraction as addition with a negated number

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

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

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

=== When it leads to unsound behaviour

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

@
(n - 1) + 1 ~ n
@

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

This would allow the following erroneous definition:

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

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

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

=== When it might be Okay

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

When you have:

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

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

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

And you want to define:

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

then the last line will give rise to the constraint:

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

because:

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

In this case it's okay to add

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

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

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

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

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE BangPatterns          #-}
{-# 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
  ( (<=<), unless )
import Control.Monad.Trans.Writer.Strict
  ( WriterT(runWriterT), runWriter )
import Data.Either
  ( rights, partitionEithers )
import Data.Foldable
import Data.List
  ( stripPrefix, partition )
import Data.Maybe
  ( mapMaybe, catMaybes, fromMaybe, isJust )
import Data.Traversable
  ( for )
import Text.Read
  ( readMaybe )

-- containers
import Data.Set
  ( Set )
import qualified Data.Set as Set
  ( elems, empty )
import Data.Map.Strict
  ( Map )
import qualified Data.Map.Strict as Map
  ( empty, insertWith, traverseWithKey )

-- ghc
import GHC.Builtin.Names
  ( knownNatClassName )
import GHC.Builtin.Types.Literals
  ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )
import GHC.Core.TyCon
  ( Injectivity (..), tyConInjectivityInfo, tyConArity )
import GHC.Utils.Misc
  ( filterByList )

-- ghc-tcplugin-api
import GHC.TcPlugin.API
import GHC.TcPlugin.API.TyConSubst
  ( TyConSubst, mkTyConSubst )
import GHC.Plugins
  ( Plugin(..), defaultPlugin, purePlugin, allVarSet, isEmptyVarSet, tyCoVarsOfType )
import GHC.Utils.Outputable

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

-- transformers
import Control.Monad.Trans.Class
  ( lift )
import Control.Monad.Trans.State.Strict
  ( StateT, evalStateT, get, modify )

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

-- | 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
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
                         return $ mkTcPlugin $ normalisePlugin 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 {k} (key :: k) 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
  tcs <- TcPluginM 'Init LookedUpTyCons
lookupTyCons
  return $
    ExtraDefs
      { tyCons = 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
    (redGivens, _) <- Bool
-> Opts
-> LookedUpTyCons
-> [Ct]
-> TcPluginM 'Solve ([Ct], Map CType CtLoc)
reduceGivens Bool
False Opts
opts LookedUpTyCons
tcs [Ct]
givens

    tcPluginTrace "decideEqualSOP Givens {" $
      vcat [ text "givens:" <+> ppr givens ]

    -- Try to find contradictory Givens, to improve pattern match warnings.
    SimplifyResult { simplifiedWanteds, contradictions, newGivens } <-
      simplifyNats opts tcs [] $
        concatMap (toNatEquality opts tcs givensTyConSubst) redGivens

    -- Only add new Givens that are genuinely new, i.e. that GHC doesn't
    -- already know.
    --
    -- For example, in #116 we had: [G] m ~ n, [G] n ~ 0. Recalling that
    -- the inert set in GHC is a /not necessarily idempotent/ terminating
    -- generalised substitution (see Note [The KickOut Criteria] in GHC.Tc.Solver.InertSet),
    -- we don't want to emit a new Given [G] m ~ 0: GHC already knows this, and
    -- if we repeatedly emit this Given we will cause a typechecker loop (as in #116).
    let
      isSolvedGiven Subst
subst Ct
ct =
        case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (Ct -> Type
ctPred Ct
ct) of
          EqPred EqRel
_rel Type
t1 Type
t2 -> Type
t1 Type -> Type -> Bool
`eqType` Type
t2
          Pred
_ -> Bool
False
      tyEqLit Ct
ct =
        case Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct) of
          EqPred EqRel
NomEq Type
t1 Type
t2 -> Type -> Bool
isTyVarTy Type
t1 Bool -> Bool -> Bool
&& Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe Integer
isNumLitTy Type
t2)
          Pred
_ -> Bool
False
      givensSubst = [Ct] -> Subst
ctsSubst [Ct]
givens -- Computes the idempotent substitution from the Givens
      actuallyNewGivens =
        (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (\ Ct
ct ->
            Ct -> Bool
tyEqLit Ct
ct
              -- For now, only admit improved Givens in the form of `n ~ L`,
              -- where `n` is a type variable and `L` is a numeric literal.
              Bool -> Bool -> Bool
&&
            Bool -> Bool
not (Subst -> Ct -> Bool
isSolvedGiven Subst
givensSubst Ct
ct)
              -- Ensure this Given is genuinely new information to GHC, to
              -- avoid repeatedly emitting facts that GHC already knows,
              -- which can cause the typechecker to loop (#116).
          )
          [Ct]
newGivens

    tcPluginTrace "decideEqualSOP Givens }" $
      vcat [ text "givens:" <+> ppr givens
           , text "simpls:" <+> ppr simplifiedWanteds
           , text "contra:" <+> ppr contradictions
           , text "new:" <+> ppr actuallyNewGivens
           ]
    return $
      mkTcPluginSolveResult
#if MIN_VERSION_ghc(9,14,0)
        ( map fromNatEquality contradictions )
#else
        []
#endif
        [] -- no solved Givens
        actuallyNewGivens

-- 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
    deriveds <- TcPluginM 'Solve [Ct]
askDeriveds
    let 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 = [Ct] -> TyConSubst
mkTyConSubst [Ct]
givens
        unit_wanteds0 = (Ct -> [NatCt]) -> [Ct] -> [NatCt]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]
toNatEquality Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst) [Ct]
wanteds
        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

    (redGivens, negWanteds) <- reduceGivens True opts tcs givens
    reducible_wanteds
      <- catMaybes <$> 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
<$>
                                    [Ct]
-> Ct -> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr [Ct]
redGivens Ct
ct)
                            nonEqs

    tcPluginTrace "decideEqualSOP Wanteds {" $
       vcat [ text "givens:" <+> ppr givens
            , text "new reduced givens:" <+> ppr redGivens
            , text $ replicate 80 '-'
            , text "wanteds:" <+> ppr wanteds
            , text "unit_wanteds:" <+> ppr unit_wanteds0
            , text "reducible_wanteds:" <+> ppr reducible_wanteds
            ]
    if null unit_wanteds0 && null reducible_wanteds
    then return $ 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.
        let mkNegWanted ( CType Type
wtdPred ) CtLoc
loc = CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> f CtEvidence -> f Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> f CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc Type
wtdPred
        ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds
        let unit_givens = (Ct -> [NatCt]) -> [Ct] -> [NatCt]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]
toNatEquality Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst) [Ct]
redGivens
            unit_wanteds = [NatCt]
unit_wanteds0 [NatCt] -> [NatCt] -> [NatCt]
forall a. [a] -> [a] -> [a]
++ (Ct -> [NatCt]) -> Map CType Ct -> [NatCt]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]
toNatEquality Opts
opts LookedUpTyCons
tcs TyConSubst
givensTyConSubst) Map CType Ct
ineqForRedWants
        sr@SimplifyResult{simplifiedWanteds, contradictions} <-
          simplifyNats opts tcs unit_givens unit_wanteds
        tcPluginTrace "normalised" (ppr sr)
        reds <- for reducible_wanteds $ \(Ct
origCt,(EvTerm
term, [(Type, Type)]
ws, [Ct]
wDicts)) -> do
          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
          return ((term, origCt), wDicts ++ wants)
        let -- Only solve a Derived when there are Wanteds in play
            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])]
simplifiedWanteds [((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])]
simplifiedWanteds
            (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds)

        tcPluginTrace "decideEqualSOP Wanteds }" $
           vcat [ text "givens:" <+> ppr givens
                , text "new reduced givens:" <+> ppr redGivens
                , text "unit givens:" <+> ppr unit_givens
                , text $ replicate 80 '-'
                , text "wanteds:" <+> ppr wanteds
                , text "ineqForRedWants:" <+> ppr ineqForRedWants
                , text "unit_wanteds:" <+> ppr unit_wanteds
                , text "reducible_wanteds:" <+> ppr reducible_wanteds
                , text $ replicate 80 '='
                , text "solved:" <+> ppr solved
                , text "newWanteds:" <+> ppr newWanteds
                ]
        return $
          mkTcPluginSolveResult
            (map fromNatEquality contradictions)
            solved
            newWanteds

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

reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds
             -> Opts -> LookedUpTyCons
             -> [Ct]
             -> TcPluginM Solve ([Ct], Map CType CtLoc)
reduceGivens :: Bool
-> Opts
-> LookedUpTyCons
-> [Ct]
-> TcPluginM 'Solve ([Ct], Map CType CtLoc)
reduceGivens Bool
gen_wanteds Opts
opts LookedUpTyCons
tcs [Ct]
origGivens = [Ct]
-> Map CType CtLoc
-> [Ct]
-> TcPluginM 'Solve ([Ct], Map CType CtLoc)
go [] Map CType CtLoc
forall k a. Map k a
Map.empty [Ct]
origGivens
  where
    go :: [Ct]
-> Map CType CtLoc
-> [Ct]
-> TcPluginM 'Solve ([Ct], Map CType CtLoc)
go [Ct]
rev_acc_gs Map CType CtLoc
acc_ws [] = ([Ct], Map CType CtLoc) -> TcPluginM 'Solve ([Ct], Map CType CtLoc)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Ct] -> [Ct]
forall a. [a] -> [a]
reverse [Ct]
rev_acc_gs, Map CType CtLoc
acc_ws )
    go [Ct]
rev_acc_gs Map CType CtLoc
acc_ws (Ct
g:[Ct]
gs) =
      case Opts
-> LookedUpTyCons -> [Ct] -> Ct -> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts LookedUpTyCons
tcs [Ct]
origGivens Ct
g of
        Just ( Type
pred', EvTerm
evExpr, [Type]
ws )
          | Bool
gen_wanteds Bool -> Bool -> Bool
|| [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ws Bool -> Bool -> Bool
|| Opts -> Bool
negNumbers Opts
opts
          -> do
            let loc :: CtLoc
loc = Ct -> CtLoc
ctLoc Ct
g
            g' <- 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 CtLoc
loc Type
pred' EvTerm
evExpr
            let !acc' = (Map CType CtLoc -> Type -> Map CType CtLoc)
-> Map CType CtLoc -> [Type] -> Map CType CtLoc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc
insertWanted CtLoc
loc) Map CType CtLoc
acc_ws [Type]
ws
            go ( g' : rev_acc_gs ) acc' gs
        Maybe (Type, EvTerm, [Type])
_ ->
          [Ct]
-> Map CType CtLoc
-> [Ct]
-> TcPluginM 'Solve ([Ct], Map CType CtLoc)
go ( Ct
g Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
rev_acc_gs ) Map CType CtLoc
acc_ws [Ct]
gs

    insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc
    insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc
insertWanted CtLoc
loc Map CType CtLoc
acc Type
w =
      (CtLoc -> CtLoc -> CtLoc)
-> CType -> CtLoc -> Map CType CtLoc -> Map CType CtLoc
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\ CtLoc
_new CtLoc
old -> CtLoc
old) (Type -> CType
CType Type
w) CtLoc
loc Map CType CtLoc
acc

tryReduceGiven
  :: Opts -> LookedUpTyCons
  -> [Ct] -> Ct
  -> Maybe (PredType, EvTerm, [PredType])
tryReduceGiven :: Opts
-> LookedUpTyCons -> [Ct] -> Ct -> Maybe (Type, EvTerm, [Type])
tryReduceGiven Opts
opts LookedUpTyCons
tcs [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
$ Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
normaliseNatEverywhere (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)
    (pred', deps) <- Maybe (Type, [Coercion])
mans
    case classifyPredType pred' of
      EqPred EqRel
_ Type
l Type
r
        | Type
l Type -> Type -> Bool
`eqType` Type
r
        -> Maybe (Type, EvTerm, [Type])
forall a. Maybe a
Nothing
      Pred
_ -> (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 NatEquality NatInEquality -> Ct
fromNatEquality (Left  (Ct
ct, CoreSOP
_, CoreSOP
_)) = Ct
ct
fromNatEquality (Right (Ct
ct, (CoreSOP, CoreSOP, Bool)
_))    = Ct
ct

reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr :: [Ct]
-> Ct -> TcPluginM 'Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
reduceNatConstr [Ct]
givens Ct
ct = do
  let pred0 :: Type
pred0 = CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct
      (Maybe (Type, [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
$ Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
normaliseNatEverywhere 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
          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 = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-natnormalise"
                       Role
Representational
                       [Coercion]
deps'
                       Type
pred' Type
pred0
              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.
          return (Just (EvExpr ev, tests, [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
  = SimplifyResult
     { SimplifyResult -> [((EvTerm, Ct), [Ct])]
simplifiedWanteds :: [((EvTerm,Ct),[Ct])]
     -- ^ List of:
     --   * Tuple of:
     --     * Evidence for:
     --     * The solved Wanted
     --   * Preconditions (in the for of new Wanteds)
     , SimplifyResult -> [Either NatEquality NatInEquality]
contradictions :: [Either NatEquality NatInEquality]
     -- ^ List of contradictions
     , SimplifyResult -> [Ct]
newGivens :: [Ct]
     -- ^ Givens derived in the improve givens stage
     }

instance Outputable SimplifyResult where
  ppr :: SimplifyResult -> SDoc
ppr (SimplifyResult { [((EvTerm, Ct), [Ct])]
simplifiedWanteds :: SimplifyResult -> [((EvTerm, Ct), [Ct])]
simplifiedWanteds :: [((EvTerm, Ct), [Ct])]
simplifiedWanteds, [Either NatEquality NatInEquality]
contradictions :: SimplifyResult -> [Either NatEquality NatInEquality]
contradictions :: [Either NatEquality NatInEquality]
contradictions, [Ct]
newGivens :: SimplifyResult -> [Ct]
newGivens :: [Ct]
newGivens }) =
    CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"SimplifyResult { simplified =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [((EvTerm, Ct), [Ct])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [((EvTerm, Ct), [Ct])]
simplifiedWanteds
               SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
", impossible =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Either NatEquality NatInEquality] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Either NatEquality NatInEquality]
contradictions
               SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
", new_givens =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
newGivens SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"}"

data NatCt
  = NatCt
  { NatCt -> Either NatEquality NatInEquality
predicate :: Either NatEquality NatInEquality
  -- ^ Predicate: either an equality or inequality
  , NatCt -> [Type]
preconds :: [PredType]
  -- ^ Preconditions (in the form of inequalities encoded as PredTypes)
  , NatCt -> [Coercion]
ctDeps :: [Coercion]
  -- ^ Coercion(s) from which the predicate is derived, needed so that evidence
  -- doesn't float above the coercions from which it is derived.
  }

instance Outputable NatCt where
  ppr :: NatCt -> SDoc
ppr (NatCt {Either NatEquality NatInEquality
predicate :: NatCt -> Either NatEquality NatInEquality
predicate :: Either NatEquality NatInEquality
predicate, [Type]
preconds :: NatCt -> [Type]
preconds :: [Type]
preconds, [Coercion]
ctDeps :: NatCt -> [Coercion]
ctDeps :: [Coercion]
ctDeps}) =
    CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"NatCt { predicate = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Either NatEquality NatInEquality -> SDoc
forall a. Outputable a => a -> SDoc
ppr Either NatEquality NatInEquality
predicate
      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
", preconditions = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
preconds
      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
", dependencies = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
ctDeps SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"}"

data SimplifyState
  = SimplifyState
  { SimplifyState -> [Coercion]
stDeps :: [Coercion]
    -- ^ Coercions on which the simplified evidence depends, this needs to be
    -- kept around because sometimes we solving one constraint (which has a
    -- depedency) is used to solve another constraint
  , SimplifyState -> [CoreUnify]
subst :: [CoreUnify]
    -- ^ Derived simplifications (i.e. b ~ c derived from (a + b) ~ (a + c)),
    -- and substitutions (i.e. n := 0 derived from y ^ n ~ 1)
  , SimplifyState -> [((EvTerm, Ct), [Ct])]
evs :: [((EvTerm,Ct),[Ct])]
    -- ^ Collected evidence
  , SimplifyState -> [(CoreSOP, CoreSOP, Bool)]
leqsG :: [(CoreSOP,CoreSOP,Bool)]
    -- ^ Given inequalities
  , SimplifyState -> [NatCt]
unsolved :: [NatCt]
    -- ^ Tried, but unsolved predicates. We keep them around in case we solve a
    -- new predicate which could lead to a substitution that enables a solve.
  , SimplifyState -> [Ct]
derivedGivens :: [Ct]
    -- ^ Unifiers derived from Givens. E.g. when we have /[G] x ^ n ~ 1/, this
    -- field will hold a derived /[G] n ~ 0/.
  }

emptySimplifyState :: SimplifyState
emptySimplifyState :: SimplifyState
emptySimplifyState
  = SimplifyState
  { stDeps :: [Coercion]
stDeps = []
  , subst :: [CoreUnify]
subst = []
  , evs :: [((EvTerm, Ct), [Ct])]
evs = []
  , leqsG :: [(CoreSOP, CoreSOP, Bool)]
leqsG = []
  , unsolved :: [NatCt]
unsolved = []
  , derivedGivens :: [Ct]
derivedGivens = []
  }

simplifyNats
  :: Opts
  -- ^ Allow negated numbers (potentially unsound!)
  -> LookedUpTyCons
  -> [NatCt]
  -- ^ Given constraints
  -> [NatCt]
  -- ^ Wanted constraints
  -> TcPluginM Solve SimplifyResult
simplifyNats :: Opts
-> LookedUpTyCons
-> [NatCt]
-> [NatCt]
-> TcPluginM 'Solve SimplifyResult
simplifyNats Opts{Word
depth :: Opts -> Word
depth :: Word
depth} LookedUpTyCons
tcs [NatCt]
eqsG [NatCt]
eqsW = do
    let eqsG1 :: [NatCt]
eqsG1 = (NatCt -> NatCt) -> [NatCt] -> [NatCt]
forall a b. (a -> b) -> [a] -> [b]
map (\NatCt
nCt -> NatCt
nCt{preconds = []}) [NatCt]
eqsG
        ([NatCt]
varEqs, [NatCt]
otherEqs) = (NatCt -> Bool) -> [NatCt] -> ([NatCt], [NatCt])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either NatEquality NatInEquality -> Bool
forall {a} {v} {c} {v} {c} {b}.
Either (a, SOP v c, SOP v c) b -> Bool
isVarEqs (Either NatEquality NatInEquality -> Bool)
-> (NatCt -> Either NatEquality NatInEquality) -> NatCt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatCt -> Either NatEquality NatInEquality
predicate) [NatCt]
eqsG1
        fancyGivens :: [[NatCt]]
fancyGivens = (NatCt -> [[NatCt]]) -> [NatCt] -> [[NatCt]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([NatCt] -> NatCt -> [[NatCt]]
makeGivensSet [NatCt]
otherEqs) [NatCt]
varEqs
    case [NatCt]
varEqs of
      [] -> do
        let eqs :: [NatCt]
eqs = [NatCt]
otherEqs [NatCt] -> [NatCt] -> [NatCt]
forall a. [a] -> [a] -> [a]
++ [NatCt]
eqsW
        CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"simplifyNats" ([NatCt] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [NatCt]
eqs)
        StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
-> SimplifyState -> TcPluginM 'Solve SimplifyResult
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs) SimplifyState
emptySimplifyState
      [NatCt]
_  -> 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 ([[NatCt]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[NatCt]]
fancyGivens) CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
")")
                      ([NatCt] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [NatCt]
varEqs)

        allSimplified <- [[NatCt]]
-> ([NatCt] -> TcPluginM 'Solve SimplifyResult)
-> TcPluginM 'Solve [SimplifyResult]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [[NatCt]]
fancyGivens (([NatCt] -> TcPluginM 'Solve SimplifyResult)
 -> TcPluginM 'Solve [SimplifyResult])
-> ([NatCt] -> TcPluginM 'Solve SimplifyResult)
-> TcPluginM 'Solve [SimplifyResult]
forall a b. (a -> b) -> a -> b
$ \[NatCt]
v -> do
          let eqs :: [NatCt]
eqs = [NatCt]
v [NatCt] -> [NatCt] -> [NatCt]
forall a. [a] -> [a] -> [a]
++ [NatCt]
eqsW
          CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"simplifyNats" ([NatCt] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [NatCt]
eqs)
          StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
-> SimplifyState -> TcPluginM 'Solve SimplifyResult
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs) SimplifyState
emptySimplifyState

        pure (foldr findFirstSimpliedWanted (SimplifyResult [] [] []) allSimplified)
  where
    simples ::
      [NatCt] ->
      StateT SimplifyState (TcPluginM Solve) SimplifyResult
    simples :: [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [] = do
      SimplifyState{evs, derivedGivens} <- StateT SimplifyState (TcPluginM 'Solve) SimplifyState
forall (m :: * -> *) s. Monad m => StateT s m s
get
      return SimplifyResult { simplifiedWanteds = evs
                            , contradictions = []
                            , newGivens = derivedGivens
                            }
    simples (eq :: NatCt
eq@NatCt{predicate :: NatCt -> Either NatEquality NatInEquality
predicate=(Left (Ct
ct,CoreSOP
u,CoreSOP
v)), [Type]
preconds :: NatCt -> [Type]
preconds :: [Type]
preconds, [Coercion]
ctDeps :: NatCt -> [Coercion]
ctDeps :: [Coercion]
ctDeps}:[NatCt]
eqs) = do
      SimplifyState{stDeps, subst, evs, leqsG, unsolved, derivedGivens} <- StateT SimplifyState (TcPluginM 'Solve) SimplifyState
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let allDeps = [Coercion]
stDeps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
ctDeps

      let 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' = [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
      ur <- lift (unifyNats ct u' v')
      lift (tcPluginTrace "unifyNats result" (ppr ur))
      case ur of
        UnifyResult
Win -> do
          -- Do note record "new" evidence for given constraints.
          Bool
-> StateT SimplifyState (TcPluginM 'Solve) ()
-> StateT SimplifyState (TcPluginM 'Solve) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct)) (StateT SimplifyState (TcPluginM 'Solve) ()
 -> StateT SimplifyState (TcPluginM 'Solve) ())
-> StateT SimplifyState (TcPluginM 'Solve) ()
-> StateT SimplifyState (TcPluginM 'Solve) ()
forall a b. (a -> b) -> a -> b
$ do
            -- Only recorde evidence for wanted contstraints
            evM <- TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> StateT
     SimplifyState (TcPluginM 'Solve) (Maybe ((EvTerm, Ct), [Ct]))
forall (m :: * -> *) a. Monad m => m a -> StateT SimplifyState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
allDeps Set CType
forall a. Monoid a => a
mempty [Type]
preconds)
            lift $ tcPluginTrace "unifyNats Win" $
              vcat [ text "evM:" <+> ppr evM
                   , text "ct:" <+> ppr ct
                   ]
            modify (\SimplifyState
s -> SimplifyState
s {evs = maybe evs (:evs) evM})
          [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs
        UnifyResult
Lose ->
          Either NatEquality NatInEquality
-> SimplifyResult -> SimplifyResult
addContra (NatCt -> Either NatEquality NatInEquality
predicate NatCt
eq) (SimplifyResult -> SimplifyResult)
-> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
-> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs
        Draw [] -> do
          -- No progress made, add it to the "unsolved" list, in the hope we
          -- can make progress when we later find a new substitution
          (SimplifyState -> SimplifyState)
-> StateT SimplifyState (TcPluginM 'Solve) ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (\SimplifyState
s -> SimplifyState
s {unsolved = eq:unsolved})
          [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs
        Draw [CoreUnify]
unifications -> do -- We made some progress in the form of a unifier

          -- As the derived unifiers we record here can lead to solving another
          -- equation, we add it and its dependencies to the list of global
          -- dependencies which we use when creating new evidence
          let stDeps1 :: [Coercion]
stDeps1 = HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion (Ct -> CtEvidence
ctEvidence Ct
ct)Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
allDeps
          -- We add apply the derived unification in the existing set of
          -- unification, and also add the derived unificaiton to the global
          -- state; to be used in solving later equations.
          let subst1 :: [CoreUnify]
subst1 = [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]
unifications [CoreUnify]
subst [CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall a. [a] -> [a] -> [a]
++ [CoreUnify]
unifications
          if CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) then do
            if [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
preconds then do
              -- We only record the unification derived from a given constraint
              -- when it has no preconditions in order for this unification to
              -- hold. The reason for that is that we can currently not record
              -- new Wanteds to be emitted at the end of the solve.
              givensU <- TcPluginM 'Solve [Ct]
-> StateT SimplifyState (TcPluginM 'Solve) [Ct]
forall (m :: * -> *) a. Monad m => m a -> StateT SimplifyState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((CoreUnify -> TcPluginM 'Solve Ct)
-> [CoreUnify] -> 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 -> [Coercion] -> CoreUnify -> TcPluginM 'Solve Ct
unifyItemToGiven (Ct -> CtLoc
ctLoc Ct
ct) [Coercion]
allDeps) [CoreUnify]
unifications)
              modify (\SimplifyState
s -> SimplifyState
s { stDeps = stDeps1
                              , subst = subst1
                              , leqsG = eqToLeq u' v' ++ leqsG
                              , unsolved = []
                              , derivedGivens = givensU ++ derivedGivens
                              })
              simples (unsolved ++ eqs)
            else
              [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs
          else do
            let allPreconds :: [Type]
allPreconds = (CoreUnify -> Type) -> [CoreUnify] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> Type
unifyItemToPredType [CoreUnify]
unifications [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
preconds
            evM <- TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> StateT
     SimplifyState (TcPluginM 'Solve) (Maybe ((EvTerm, Ct), [Ct]))
forall (m :: * -> *) a. Monad m => m a -> StateT SimplifyState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
allDeps Set CType
forall a. Set a
Set.empty [Type]
allPreconds)
            case evM of
              Maybe ((EvTerm, Ct), [Ct])
Nothing ->
                [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs
              Just ((EvTerm, Ct), [Ct])
ev -> do
                -- We only record the unification derived from a wanted constraint
                -- when we can actually record evidence for a succesful solve.
                (SimplifyState -> SimplifyState)
-> StateT SimplifyState (TcPluginM 'Solve) ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (\SimplifyState
s -> SimplifyState
s { stDeps = stDeps1
                                , subst = subst1
                                , evs = ev:evs
                                , unsolved = []
                                })
                [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples ([NatCt]
unsolved [NatCt] -> [NatCt] -> [NatCt]
forall a. [a] -> [a] -> [a]
++ [NatCt]
eqs)

    simples (eq :: NatCt
eq@NatCt{predicate :: NatCt -> Either NatEquality NatInEquality
predicate=Right (Ct
ct,u :: (CoreSOP, CoreSOP, Bool)
u@(CoreSOP
x,CoreSOP
y,Bool
b)), [Type]
preconds :: NatCt -> [Type]
preconds :: [Type]
preconds, [Coercion]
ctDeps :: NatCt -> [Coercion]
ctDeps :: [Coercion]
ctDeps}:[NatCt]
eqs) = do
      SimplifyState{stDeps, subst, evs, leqsG, unsolved} <- StateT SimplifyState (TcPluginM 'Solve) SimplifyState
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let 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'    = [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'    = [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
x',CoreSOP
y',Bool
b)
          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)]] -> [(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 NatEquality NatInEquality] -> [NatInEquality]
forall a b. [Either a b] -> [b]
rights ((NatCt -> Either NatEquality NatInEquality)
-> [NatCt] -> [Either NatEquality NatInEquality]
forall a b. (a -> b) -> [a] -> [b]
map NatCt -> Either NatEquality NatInEquality
predicate [NatCt]
eqsG))
                         ]
          allDeps = [Coercion]
stDeps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
ctDeps
      lift (tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)))
      case runWriterT (isNatural u') of
        Just (Bool
True,Set CType
knW)  -> do
          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])])
-> StateT
     SimplifyState (TcPluginM 'Solve) (Maybe ((EvTerm, Ct), [Ct]))
-> StateT SimplifyState (TcPluginM 'Solve) [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> StateT
     SimplifyState (TcPluginM 'Solve) (Maybe ((EvTerm, Ct), [Ct]))
forall (m :: * -> *) a. Monad m => m a -> StateT SimplifyState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
allDeps Set CType
knW [Type]
preconds)
          modify (\SimplifyState
s -> SimplifyState
s {evs = evs', leqsG = leqsG'})
          simples eqs

        Just (Bool
False,Set CType
_) | [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
preconds ->
          Either NatEquality NatInEquality
-> SimplifyResult -> SimplifyResult
addContra (NatCt -> Either NatEquality NatInEquality
predicate NatCt
eq) (SimplifyResult -> SimplifyResult)
-> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
-> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
eqs
        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
              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])])
-> StateT
     SimplifyState (TcPluginM 'Solve) (Maybe ((EvTerm, Ct), [Ct]))
-> StateT SimplifyState (TcPluginM 'Solve) [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
-> StateT
     SimplifyState (TcPluginM 'Solve) (Maybe ((EvTerm, Ct), [Ct]))
forall (m :: * -> *) a. Monad m => m a -> StateT SimplifyState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LookedUpTyCons
-> Ct
-> [Coercion]
-> Set CType
-> [Type]
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
allDeps Set CType
kW [Type]
preconds)
              modify (\SimplifyState
s -> SimplifyState
s { stDeps = allDeps
                              , evs = evs'
                              , leqsG = leqsG'
                              })
              simples eqs
            (Bool, Set CType)
_ -> do
              (SimplifyState -> SimplifyState)
-> StateT SimplifyState (TcPluginM 'Solve) ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (\SimplifyState
s -> SimplifyState
s {unsolved = eq:unsolved})
              [NatCt] -> StateT SimplifyState (TcPluginM 'Solve) SimplifyResult
simples [NatCt]
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 -> Bool
isVarEqs (Left (a
_,S [P [V v
_]], S [P [V v
_]])) = Bool
True
    isVarEqs Either (a, SOP v c, SOP v c) b
_ = Bool
False

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

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

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

    findFirstSimpliedWanted :: SimplifyResult -> SimplifyResult -> SimplifyResult
findFirstSimpliedWanted s1 :: SimplifyResult
s1@(SimplifyResult {[((EvTerm, Ct), [Ct])]
simplifiedWanteds :: SimplifyResult -> [((EvTerm, Ct), [Ct])]
simplifiedWanteds :: [((EvTerm, Ct), [Ct])]
simplifiedWanteds, [Either NatEquality NatInEquality]
contradictions :: SimplifyResult -> [Either NatEquality NatInEquality]
contradictions :: [Either NatEquality NatInEquality]
contradictions}) SimplifyResult
s2
      |  Bool -> Bool
not ([Either NatEquality NatInEquality] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Either NatEquality NatInEquality]
contradictions)
      Bool -> Bool -> Bool
|| (((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])]
simplifiedWanteds
      = SimplifyResult
s1
      | Bool
otherwise
      = SimplifyResult
s2

addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult
addContra :: Either NatEquality NatInEquality
-> SimplifyResult -> SimplifyResult
addContra Either NatEquality NatInEquality
contra SimplifyResult
sr = SimplifyResult
sr { contradictions = contra : contradictions sr }

-- 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 :: Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]
toNatEquality :: Opts -> LookedUpTyCons -> TyConSubst -> Ct -> [NatCt]
toNatEquality Opts
opts 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 (Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat 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 (Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat Type
y)
      preds :: [Type]
preds = Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs ([(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
        [Either NatEquality NatInEquality -> [Type] -> [Coercion] -> NatCt
NatCt (NatEquality -> Either NatEquality NatInEquality
forall a b. a -> Either a b
Left (Ct
ct0, CoreSOP
x', CoreSOP
y')) [Type]
preds ([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
        [Either NatEquality NatInEquality -> [Type] -> [Coercion] -> NatCt
NatCt (NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct0, (CoreSOP
x', CoreSOP
y', Bool
b))) [Type]
preds ([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 -> [NatCt]
goNomEq Type
t1 Type
t2
      ClassPred Class
kn [Type
x]
        -- From [G] KnownNat blah, also produce [G] 0 <= blah
        -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94.
        | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct0)
        , Class -> Name
className Class
kn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
knownNatClassName
        , let ((CoreSOP
x', [Coercion]
cos0), [(Type, Type)]
ks) = Writer [(Type, Type)] (CoreSOP, [Coercion])
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat Type
x)
        , let preds :: [Type]
preds = Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs [(Type, Type)]
ks
        -> [Either NatEquality NatInEquality -> [Type] -> [Coercion] -> NatCt
NatCt (NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct0, ([Product TyVar CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [], CoreSOP
x', Bool
True))) [Type]
preds [Coercion]
cos0]
      Pred
_ -> []
  where
    pred0 :: Type
pred0 = Ct -> Type
ctPred Ct
ct0
    -- x ~ y
    goNomEq :: Type -> Type -> [NatCt]
    goNomEq :: Type -> Type -> [NatCt]
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 (TyCon
tc , [Type]
xs) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
lhs
      , Just (TyCon
tc', [Type]
ys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs
      , TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc'
      , 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 xys :: [(Type, Type)]
xys = [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
xs [Type]
ys
      -- Make sure not to recur into non-injective positions of type families,
      -- e.g. if we know 'F n ~ F m' that doesn't mean 'n ~ m'.
            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)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$
                case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc of
                  Injective [Bool]
inj ->
                    [Bool] -> [(Type, Type)] -> [(Type, Type)]
forall a. [Bool] -> [a] -> [a]
filterByList ([Bool]
inj [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True) [(Type, Type)]
xys
                  Injectivity
_ ->
                    -- However, it is okay to recur in the following specific
                    -- exception:
                    let ([(Type, Type)]
tcArgs,[(Type, Type)]
rest) = Int -> [(Type, Type)] -> ([(Type, Type)], [(Type, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [(Type, Type)]
xys
                        diffs :: [(Type, Type)]
diffs = ((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)]
tcArgs
                     in case [(Type, Type)]
diffs of
                            -- 1. The types only differ in one argument position
                          [(Type
x,Type
y)]
                            | let xFVs :: TyCoVarSet
xFVs = Type -> TyCoVarSet
tyCoVarsOfType Type
x
                            , let yFVs :: TyCoVarSet
yFVs = Type -> TyCoVarSet
tyCoVarsOfType Type
y
                            -- 2. The argument must have variables, and they must
                            -- all be skolem variables.
                            , Bool -> Bool
not (TyCoVarSet -> Bool
isEmptyVarSet TyCoVarSet
xFVs)
                            , (TyVar -> Bool) -> TyCoVarSet -> Bool
allVarSet TyVar -> Bool
isSkolemTyVar TyCoVarSet
xFVs
                            -- 3. The variables in both argument postions must
                            -- be the same.
                            , TyCoVarSet
xFVs TyCoVarSet -> TyCoVarSet -> Bool
forall a. Eq a => a -> a -> Bool
== TyCoVarSet
yFVs
                            -> (Type
x,Type
y)(Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
:[(Type, Type)]
rest
                          [(Type, Type)]
_ -> [(Type, Type)]
rest
      = case ((Type, Type) -> [NatCt]) -> [(Type, Type)] -> [NatCt]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Type -> Type -> [NatCt]) -> (Type, Type) -> [NatCt]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> [NatCt]
rewrite) [(Type, Type)]
subs of
          [] -> []
          [NatCt
rw] -> [NatCt
rw]
          [NatCt]
rws ->
            -- For Given Cts, it's fine to extract multiple (in)equalities. However,
            -- for Wanted Cts we should not claim to solve the entire Ct when we
            -- only solve a part of the Ct. So when we can extra two or more inequalities
            -- from a Wanted Ct, we conservatively choose not to solve any of them.
            if CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct0) then
              [NatCt]
rws
            else
              []
      | Bool
otherwise
      = Type -> Type -> [NatCt]
rewrite Type
lhs Type
rhs

    rewrite :: Type -> Type -> [NatCt]
    rewrite :: Type -> Type -> [NatCt]
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 (Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat 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 (Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat Type
y)
      , let preds :: [Type]
preds = Opts -> LookedUpTyCons -> [(Type, Type)] -> [Type]
subToPred Opts
opts LookedUpTyCons
tcs ([(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
      = [Either NatEquality NatInEquality -> [Type] -> [Coercion] -> NatCt
NatCt (NatEquality -> Either NatEquality NatInEquality
forall a b. a -> Either a b
Left (Ct
ct0,CoreSOP
x',CoreSOP
y')) [Type]
preds ([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


unifyItemToGiven :: CtLoc -> [Coercion] -> CoreUnify -> TcPluginM Solve Ct
unifyItemToGiven :: CtLoc -> [Coercion] -> CoreUnify -> TcPluginM 'Solve Ct
unifyItemToGiven CtLoc
loc [Coercion]
deps CoreUnify
ui = 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 CtLoc
loc Type
pty (EvExpr -> EvTerm
EvExpr (Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
co))
  where
    ty1 :: Type
ty1 = case CoreUnify
ui of
            SubstItem {TyVar
CoreSOP
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
siVar :: TyVar
siSOP :: CoreSOP
..} -> TyVar -> Type
mkTyVarTy TyVar
siVar
            UnifyItem {CoreSOP
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: CoreSOP
siRHS :: CoreSOP
..} -> 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

    pty :: Type
pty = Role -> Type -> Type -> Type
mkEqPredRole Role
Nominal Type
ty1 Type
ty2
    co :: Coercion
co = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-natnormalise" Role
Nominal [Coercion]
deps Type
ty1 Type
ty2

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 ::
  -- | Known TyCon environment
  LookedUpTyCons ->
  -- | Constraint for which we are creating evidence
  Ct ->
  -- | Coercions in which the evidence depends
  [Coercion] ->
  -- | Types that we should be known to be a Natural
  Set CType ->
  -- | Inequalities that should hold
  [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
  holeWanteds <- CtLoc -> [Type] -> TcPluginM 'Solve [Ct]
evSubtPreds (Ct -> CtLoc
ctLoc Ct
ct) [Type]
preds
  knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW)
  let newWant = [Ct]
knWanted [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
holeWanteds
  case classifyPredType $ ctEvPred $ ctEvidence 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
  kc_clas <- Name -> TcPluginM 'Solve Class
forall (m :: * -> *). MonadTcPlugin m => Name -> m Class
tcLookupClass Name
knownNatClassName
  let kn_pred = Class -> [Type] -> Type
mkClassPred Class
kc_clas [Type
ty]
  wantedCtEv <- newWanted loc kn_pred
  return $ mkNonCanonical wantedCtEv