{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module GHC.Tc.Solver.InertSet (
    -- * The work list
    WorkList(..), isEmptyWorkList, emptyWorkList,
    extendWorkListNonEq, extendWorkListCt,
    extendWorkListCts, extendWorkListCtList,
    extendWorkListEq, extendWorkListEqs,
    appendWorkList, extendWorkListImplic,
    workListSize,
    selectWorkItem,

    -- * The inert set
    InertSet(..),
    InertCans(..),
    emptyInert,

    noMatchableGivenDicts,
    noGivenNewtypeReprEqs, updGivenEqs,
    mightEqualLater,
    prohibitedSuperClassSolve,

    -- * Inert equalities
    InertEqs,
    foldTyEqs, delEq, findEq,
    partitionInertEqs, partitionFunEqs,
    foldFunEqs, addEqToCans,

    -- * Inert Dicts
    updDicts, delDict, addDict, filterDicts, partitionDicts,
    addSolvedDict,

    -- * Inert Irreds
    InertIrreds, delIrred, addIrreds, addIrred, foldIrreds,
    findMatchingIrreds, updIrreds, addIrredToCans,

    -- * Kick-out
    KickOutSpec(..), kickOutRewritableLHS,

    -- * Cycle breaker vars
    CycleBreakerVarStack,
    pushCycleBreakerVarStack,
    addCycleBreakerBindings,
    forAllCycleBreakerBindings_,

    -- * Solving one from another
    InteractResult(..), solveOneFromTheOther

  ) where

import GHC.Prelude

import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin, ctLocSpan, ctLocLevel )
import GHC.Tc.Solver.Types
import GHC.Tc.Utils.TcType

import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique( hasKey )
import GHC.Types.Basic( SwapFlag(..) )

import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.TyCo.FVs
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.Class( Class )
import GHC.Core.TyCon
import GHC.Core.Class( classTyCon )
import GHC.Core.Unify
import GHC.Builtin.Names( eqPrimTyConKey, heqTyConKey, eqTyConKey )
import GHC.Utils.Misc       ( partitionWith )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.Maybe
import GHC.Data.Bag

import Data.List.NonEmpty ( NonEmpty(..), (<|) )
import qualified Data.List.NonEmpty as NE
import Data.Function ( on )

import Control.Monad      ( forM_ )

{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************

Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavours).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.

As a simple form of priority queue, our worklist separates out

* equalities (wl_eqs); see Note [Prioritise equalities]
* all the rest (wl_rest)

Note [Prioritise equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's very important to process equalities over class constraints:

* (Efficiency)  The general reason to do so is that if we process a
  class constraint first, we may end up putting it into the inert set
  and then kicking it out later.  That's extra work compared to just
  doing the equality first.

* (Avoiding fundep iteration) As #14723 showed, it's possible to
  get non-termination if we
      - Emit the fundep equalities for a class constraint,
        generating some fresh unification variables.
      - That leads to some unification
      - Which kicks out the class constraint
      - Which isn't solved (because there are still some more
        equalities in the work-list), but generates yet more fundeps
  Solution: prioritise equalities over class constraints

* (Class equalities) We need to prioritise equalities even if they
  are hidden inside a class constraint; see Note [Prioritise class equalities]

* (Kick-out) We want to apply this priority scheme to kicked-out
  constraints too (see the call to extendWorkListCt in kick_out_rewritable)
  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
  homo-kinded when kicked out, and hence we want to prioritise it.

Further refinements:

* Among the equalities we prioritise ones with an empty rewriter set;
  see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1).

* Among equalities with an empty rewriter set, we prioritise nominal equalities.
   * They have more rewriting power, so doing them first is better.
   * Prioritising them ameliorates the incompleteness of newtype
     solving: see (Ex2) in Note [Decomposing newtype equalities] in
     GHC.Tc.Solver.Equality.

Note [Prioritise class equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prioritise equalities in the solver (see selectWorkItem). But class
constraints like (a ~ b) and (a ~~ b) are actually equalities too;
see Note [The equality types story] in GHC.Builtin.Types.Prim.

Failing to prioritise these is inefficient (more kick-outs etc).
But, worse, it can prevent us spotting a "recursive knot" among
Wanted constraints.  See comment:10 of #12734 for a worked-out
example.

So we arrange to put these particular class constraints in the wl_eqs.

  NB: since we do not currently apply the substitution to the
  inert_solved_dicts, the knot-tying still seems a bit fragile.
  But this makes it better.

Note [Residual implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The wl_implics in the WorkList are the residual implication
constraints that are generated while solving or canonicalising the
current worklist.  Specifically, when canonicalising
   (forall a. t1 ~ forall a. t2)
from which we get the implication
   (forall a. t1 ~ t2)
See GHC.Tc.Solver.Monad.deferTcSForAllEq

-}

-- See Note [WorkList priorities]
data WorkList
  = WL { WorkList -> [Ct]
wl_eqs_N :: [Ct]  -- /Nominal/ equalities (s ~#N t), (s ~ t), (s ~~ t)
                           -- with empty rewriter set
       , WorkList -> [Ct]
wl_eqs_X :: [Ct]  -- CEqCan, CDictCan, CIrredCan
                           -- with empty rewriter set
           -- All other equalities: contains both equality constraints and
           -- their class-level variants (a~b) and (a~~b);
           -- See Note [Prioritise equalities]
           -- See Note [Prioritise class equalities]

       , WorkList -> [Ct]
wl_rw_eqs  :: [Ct]  -- Like wl_eqs, but ones that have a non-empty
                             -- rewriter set; or, more precisely, did when
                             -- added to the WorkList
         -- We prioritise wl_eqs over wl_rw_eqs;
         -- see Note [Prioritise Wanteds with empty RewriterSet]
         -- in GHC.Tc.Types.Constraint for more details.

       , WorkList -> [Ct]
wl_rest :: [Ct]

       , WorkList -> Bag Implication
wl_implics :: Bag Implication  -- See Note [Residual implications]
    }

isNominalEqualityCt :: Ct -> Bool
-- A nominal equality, primitive or not,
--                     canonical or not
--     (s ~# t), (s ~ t), or (s ~~ t)
isNominalEqualityCt :: Ct -> Bool
isNominalEqualityCt Ct
ct
  | Just TyCon
tc <- Type -> Maybe TyCon
tcTyConAppTyCon_maybe (Ct -> Type
ctPred Ct
ct)
  = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
  | Bool
otherwise
  = Bool
False

appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
    (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs1_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs1_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs1
        , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest1, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics1 })
    (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs2_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs2_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs2
        , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
   = WL { wl_eqs_N :: [Ct]
wl_eqs_N   = [Ct]
eqs1_N   [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2_N
        , wl_eqs_X :: [Ct]
wl_eqs_X   = [Ct]
eqs1_X   [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2_X
        , wl_rw_eqs :: [Ct]
wl_rw_eqs  = [Ct]
rw_eqs1  [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rw_eqs2
        , wl_rest :: [Ct]
wl_rest    = [Ct]
rest1    [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rest2
        , wl_implics :: Bag Implication
wl_implics = Bag Implication
implics1 Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags`   Bag Implication
implics2 }

workListSize :: WorkList -> Int
workListSize :: WorkList -> ScDepth
workListSize (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  = [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
eqs_N ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
eqs_X ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
rw_eqs ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
rest

extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq RewriterSet
rewriters Ct
ct
    wl :: WorkList
wl@(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs })
  | RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters      -- A wanted that has not been rewritten
    -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]
    --                         in GHC.Tc.Types.Constraint
  = if Ct -> Bool
isNominalEqualityCt Ct
ct
    then WorkList
wl { wl_eqs_N = ct : eqs_N }
    else WorkList
wl { wl_eqs_X = ct : eqs_X }

  | Bool
otherwise
  = WorkList
wl { wl_rw_eqs = ct : rw_eqs }

extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList
-- Add [eq1,...,eqn] to the work-list
-- They all have the same rewriter set
-- The constraints will be solved in left-to-right order:
--   see Note [Work-list ordering] in GHC.Tc.Solver.Equality
--
-- Precondition: new_eqs is non-empty
extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList
extendWorkListEqs RewriterSet
rewriters Bag Ct
new_eqs
    wl :: WorkList
wl@(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs })
  | RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters
    -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]
    --                         in GHC.Tc.Types.Constraint
  = case (Ct -> Bool) -> Bag Ct -> (Bag Ct, Bag Ct)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag Ct -> Bool
isNominalEqualityCt Bag Ct
new_eqs of
       (Bag Ct
new_eqs_N, Bag Ct
new_eqs_X)
          | Bag Ct -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Ct
new_eqs_N -> WorkList
wl { wl_eqs_X = new_eqs_X `push_on_front` eqs_X }
          | Bag Ct -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Ct
new_eqs_X -> WorkList
wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N }
          | Bool
otherwise            -> WorkList
wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N
                                       , wl_eqs_X = new_eqs_X `push_on_front` eqs_X }
          -- These isEmptyBag tests are just trying
          -- to avoid creating unnecessary thunks

  | Bool
otherwise
  = WorkList
wl { wl_rw_eqs = new_eqs `push_on_front` rw_eqs }
  where
    push_on_front :: Bag Ct -> [Ct] -> [Ct]
    -- push_on_front puts the new equlities on the front of the queue
    push_on_front :: Bag Ct -> [Ct] -> [Ct]
push_on_front Bag Ct
new_eqs [Ct]
eqs = (Ct -> [Ct] -> [Ct]) -> [Ct] -> Bag Ct -> [Ct]
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (:) [Ct]
eqs Bag Ct
new_eqs

extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl = WorkList
wl { wl_rest = ct : wl_rest wl }

extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic Implication
implic WorkList
wl = WorkList
wl { wl_implics = implic `consBag` wl_implics wl }

extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic about what kind of constraint
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
 = case Type -> Pred
classifyPredType (CtEvidence -> Type
ctEvPred CtEvidence
ev) of
     EqPred {}
       -> RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq RewriterSet
rewriters Ct
ct WorkList
wl

     ClassPred Class
cls [Type]
_  -- See Note [Prioritise class equalities]
       |  Class -> Bool
isEqualityClass Class
cls
       -> RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq RewriterSet
rewriters Ct
ct WorkList
wl

     Pred
_ -> Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl
  where
    ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
    rewriters :: RewriterSet
rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev

extendWorkListCtList :: [Ct] -> WorkList -> WorkList
extendWorkListCtList :: [Ct] -> WorkList -> WorkList
extendWorkListCtList [Ct]
cts WorkList
wl = (Ct -> WorkList -> WorkList) -> WorkList -> [Ct] -> WorkList
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl [Ct]
cts

extendWorkListCts :: Cts -> WorkList -> WorkList
extendWorkListCts :: Bag Ct -> WorkList -> WorkList
extendWorkListCts Bag Ct
cts WorkList
wl = (Ct -> WorkList -> WorkList) -> WorkList -> Bag Ct -> WorkList
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl Bag Ct
cts

isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X
                    , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
  = [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_N Bool -> Bool -> Bool
&& [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_X Bool -> Bool -> Bool
&& [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest Bool -> Bool -> Bool
&& Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics

emptyWorkList :: WorkList
emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs_N :: [Ct]
wl_eqs_N = [], wl_eqs_X :: [Ct]
wl_eqs_X = []
                   , wl_rw_eqs :: [Ct]
wl_rw_eqs = [], wl_rest :: [Ct]
wl_rest = [], wl_implics :: Bag Implication
wl_implics = Bag Implication
forall a. Bag a
emptyBag }

selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
-- See Note [Prioritise equalities]
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectWorkItem wl :: WorkList
wl@(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X
                      , wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  | Ct
ct:[Ct]
cts <- [Ct]
eqs_N  = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs_N  = cts })
  | Ct
ct:[Ct]
cts <- [Ct]
eqs_X  = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs_X  = cts })
  | Ct
ct:[Ct]
cts <- [Ct]
rw_eqs = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rw_eqs = cts })
  | Ct
ct:[Ct]
cts <- [Ct]
rest   = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rest   = cts })
  | Bool
otherwise        = Maybe (Ct, WorkList)
forall a. Maybe a
Nothing

-- Pretty printing
instance Outputable WorkList where
  ppr :: WorkList -> SDoc
ppr (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs
          , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
   = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"WL" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
     [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_N) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Eqs_N =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs_N)
          , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_X) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Eqs_X =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs_X)
          , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rw_eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"RwEqs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
rw_eqs)
          , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Non-eqs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
rest)
          , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            SDoc -> SDoc -> SDoc
forall doc. IsOutput doc => doc -> doc -> doc
ifPprDebug (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Implics =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Implication -> SDoc) -> [Implication] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Bag Implication -> [Implication]
forall a. Bag a -> [a]
bagToList Bag Implication
implics)))
                       (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(Implics omitted)")
          ])

{- *********************************************************************
*                                                                      *
                InertSet: the inert set
*                                                                      *
*                                                                      *
********************************************************************* -}

type CycleBreakerVarStack = NonEmpty (Bag (TcTyVar, TcType))
   -- ^ a stack of (CycleBreakerTv, original family applications) lists
   -- first element in the stack corresponds to current implication;
   --   later elements correspond to outer implications
   -- used to undo the cycle-breaking needed to handle
   -- Note [Type equality cycles] in GHC.Tc.Solver.Equality
   -- Why store the outer implications? For the use in mightEqualLater (only)
   --
   -- Why NonEmpty? So there is always a top element to add to

data InertSet
  = IS { InertSet -> InertCans
inert_cans :: InertCans
              -- Canonical Given, Wanted
              -- Sometimes called "the inert set"

       , InertSet -> CycleBreakerVarStack
inert_cycle_breakers :: CycleBreakerVarStack

       , InertSet -> FunEqMap Reduction
inert_famapp_cache :: FunEqMap Reduction
              -- Just a hash-cons cache for use when reducing family applications
              -- only
              --
              -- If    F tys :-> (co, rhs, flav),
              -- then  co :: F tys ~N rhs
              -- all evidence is from instances or Givens; no coercion holes here
              -- (We have no way of "kicking out" from the cache, so putting
              --  wanteds here means we can end up solving a Wanted with itself. Bad)

       , InertSet -> DictMap DictCt
inert_solved_dicts :: DictMap DictCt
              -- All Wanteds, of form (C t1 .. tn)
              -- Always a dictionary solved by an instance decl; never an implict parameter
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }

instance Outputable InertSet where
  ppr :: InertSet -> SDoc
ppr (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics
          , inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
solved_dicts })
      = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics
             , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([DictCt] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DictCt]
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Solved dicts =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((DictCt -> SDoc) -> [DictCt] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DictCt]
dicts) ]
         where
           dicts :: [DictCt]
dicts = Bag DictCt -> [DictCt]
forall a. Bag a -> [a]
bagToList (DictMap DictCt -> Bag DictCt
forall a. DictMap a -> Bag a
dictsToBag DictMap DictCt
solved_dicts)

emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
  = IC { inert_eqs :: InertEqs
inert_eqs          = InertEqs
emptyTyEqs
       , inert_funeqs :: InertFunEqs
inert_funeqs       = InertFunEqs
forall a. TcAppMap a
emptyFunEqs
       , inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
topTcLevel
       , inert_given_eqs :: Bool
inert_given_eqs    = Bool
False
       , inert_dicts :: DictMap DictCt
inert_dicts        = DictMap DictCt
forall a. TcAppMap a
emptyDictMap
       , inert_safehask :: DictMap DictCt
inert_safehask     = DictMap DictCt
forall a. TcAppMap a
emptyDictMap
       , inert_insts :: [QCInst]
inert_insts        = []
       , inert_irreds :: InertIrreds
inert_irreds       = InertIrreds
forall a. Bag a
emptyBag }

emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
  = IS { inert_cans :: InertCans
inert_cans           = InertCans
emptyInertCans
       , inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = Bag (TcTyVar, Type)
forall a. Bag a
emptyBag Bag (TcTyVar, Type)
-> [Bag (TcTyVar, Type)] -> CycleBreakerVarStack
forall a. a -> [a] -> NonEmpty a
:| []
       , inert_famapp_cache :: FunEqMap Reduction
inert_famapp_cache   = FunEqMap Reduction
forall a. TcAppMap a
emptyFunEqs
       , inert_solved_dicts :: DictMap DictCt
inert_solved_dicts   = DictMap DictCt
forall a. TcAppMap a
emptyDictMap }


{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we apply a top-level instance declaration, we add the "solved"
dictionary to the inert_solved_dicts.  In general, we use it to avoid
creating a new EvVar when we have a new goal that we have solved in
the past.

But in particular, we can use it to create *recursive* dictionaries.
The simplest, degenerate case is
    instance C [a] => C [a] where ...
If we have
    [W] d1 :: C [x]
then we can apply the instance to get
    d1 = $dfCList d
    [W] d2 :: C [x]
Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
    d1 = $dfCList d
    d2 = d1

See Note [Example of recursive dictionaries]

VERY IMPORTANT INVARIANT:

 (Solved Dictionary Invariant)
    Every member of the inert_solved_dicts is the result
    of applying an instance declaration that "takes a step"

    An instance "takes a step" if it has the form
        dfunDList d1 d2 = MkD (...) (...) (...)
    That is, the dfun is lazy in its arguments, and guarantees to
    immediately return a dictionary constructor.  NB: all dictionary
    data constructors are lazy in their arguments.

    This property is crucial to ensure that all dictionaries are
    non-bottom, which in turn ensures that the whole "recursive
    dictionary" idea works at all, even if we get something like
        rec { d = dfunDList d dx }
    See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.

 Reason:
   - All instances, except two exceptions listed below, "take a step"
     in the above sense

   - Exception 1: local quantified constraints have no such guarantee;
     indeed, adding a "solved dictionary" when applying a quantified
     constraint led to the ability to define unsafeCoerce
     in #17267.

   - Exception 2: the magic built-in instance for (~) has no
     such guarantee.  It behaves as if we had
         class    (a ~# b) => (a ~ b) where {}
         instance (a ~# b) => (a ~ b) where {}
     The "dfun" for the instance is strict in the coercion.
     Anyway there's no point in recording a "solved dict" for
     (t1 ~ t2); it's not going to allow a recursive dictionary
     to be constructed.  Ditto (~~) and Coercible.

THEREFORE we only add a "solved dictionary"
  - when applying an instance declaration
  - subject to Exceptions 1 and 2 above

In implementation terms
  - GHC.Tc.Solver.Monad.addSolvedDict adds a new solved dictionary,
    conditional on the kind of instance

  - It is only called when applying an instance decl,
    in GHC.Tc.Solver.Dict.tryInstances

  - ClsInst.InstanceWhat says what kind of instance was
    used to solve the constraint.  In particular
      * LocalInstance identifies quantified constraints
      * BuiltinEqInstance identifies the strange built-in
        instances for equality.

  - ClsInst.instanceReturnsDictCon says which kind of
    instance guarantees to return a dictionary constructor

Other notes about solved dictionaries

* See also Note [Do not add superclasses of solved dictionaries]

* The inert_solved_dicts field is not rewritten by equalities,
  so it may get out of date.

* The inert_solved_dicts are all Wanteds, never givens

* We only cache dictionaries from top-level instances, not from
  local quantified constraints.  Reason: if we cached the latter
  we'd need to purge the cache when bringing new quantified
  constraints into scope, because quantified constraints "shadow"
  top-level instances.

Note [Do not add superclasses of solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Every member of inert_solved_dicts is the result of applying a
dictionary function, NOT of applying superclass selection to anything.
Consider

        class Ord a => C a where
        instance Ord [a] => C [a] where ...

Suppose we are trying to solve
  [G] d1 : Ord a
  [W] d2 : C [a]

Then we'll use the instance decl to give

  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
  [W] d3 : Ord [a]

We must not add d4 : Ord [a] to the 'solved' set (by taking the
superclass of d2), otherwise we'll use it to solve d3, without ever
using d1, which would be a catastrophe.

Solution: when extending the solved dictionaries, do not add superclasses.
That's why each element of the inert_solved_dicts is the result of applying
a dictionary function.

Note [Example of recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- Example 1

    data D r = ZeroD | SuccD (r (D r));

    instance (Eq (r (D r))) => Eq (D r) where
        ZeroD     == ZeroD     = True
        (SuccD a) == (SuccD b) = a == b
        _         == _         = False;

    equalDC :: D [] -> D [] -> Bool;
    equalDC = (==);

We need to prove (Eq (D [])). Here's how we go:

   [W] d1 : Eq (D [])
By instance decl of Eq (D r):
   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
By instance decl of Eq [a]:
   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
                                   d1 = dfEqD d2
Now this wanted can interact with our "solved" d1 to get:
    d3 = d1

-- Example 2:
This code arises in the context of "Scrap Your Boilerplate with Class"

    class Sat a
    class Data ctx a
    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2

    class Data Maybe a => Foo a

    instance Foo t => Sat (Maybe t)                             -- dfunSat

    instance Data Maybe a => Foo a                              -- dfunFoo1
    instance Foo a        => Foo [a]                            -- dfunFoo2
    instance                 Foo [Char]                         -- dfunFoo3

Consider generating the superclasses of the instance declaration
         instance Foo a => Foo [a]

So our problem is this
    [G] d0 : Foo t
    [W] d1 : Data Maybe [t]   -- Desired superclass

We may add the given in the inert set, along with its superclasses
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  WorkList
    [W] d1 : Data Maybe [t]

Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
  WorkList:
    [W] d2 : Sat (Maybe [t])
    [W] d3 : Data Maybe t

Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
  WorkList:
    [W] d3 : Data Maybe t
    [W] d4 : Foo [t]

Now, we can just solve d3 from d01; d3 := d01
  Inert
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
  WorkList
    [W] d4 : Foo [t]

Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
  Inert
    [G] d0  : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
        d4 : Foo [t]
  WorkList:
    [W] d5 : Foo t

Now, d5 can be solved! d5 := d0

Result
   d1 := dfunData2 d2 d3
   d2 := dfunSat d4
   d3 := d01
   d4 := dfunFoo2 d5
   d5 := d0
-}

{- *********************************************************************
*                                                                      *
                InertCans: the canonical inerts
*                                                                      *
*                                                                      *
********************************************************************* -}

{- Note [Tracking Given equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify
Note [Unification preconditions], we can't unify
   alpha[2] ~ Int
under a level-4 implication if there are any Given equalities
bound by the implications at level 3 of 4.  To that end, the
InertCans tracks

  inert_given_eq_lvl :: TcLevel
     -- The TcLevel of the innermost implication that has a Given
     -- equality of the sort that make a unification variable untouchable
     -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).

We update inert_given_eq_lvl whenever we add a Given to the
inert set, in updGivenEqs.

Then a unification variable alpha[n] is untouchable iff
    n < inert_given_eq_lvl
that is, if the unification variable was born outside an
enclosing Given equality.

Exactly which constraints should trigger (UNTOUCHABLE), and hence
should update inert_given_eq_lvl?

(TGE1) We do /not/ need to worry about let-bound skolems, such as
     forall[2] a. a ~ [b] => blah
  See Note [Let-bound skolems] and the isOuterTyVar tests in `updGivenEqs`

(TGE2) However, solely to support better error messages (see Note [HasGivenEqs] in
   GHC.Tc.Types.Constraint) we also track these "local" equalities in the
   boolean inert_given_eqs field.  This field is used only subsequntly (see
   `getHasGivenEqs`), to set the ic_given_eqs field to LocalGivenEqs.

(TGE3) Consider an implication
      forall[2]. beta[1] => alpha[1] ~ Int
  where beta is a unification variable that has already been unified
  to () in an outer scope.  Then alpha[1] is perfectly touchable and
  we can unify alpha := Int. So when deciding whether the givens contain
  an equality, we should canonicalise first, rather than just looking at
  the /original/ givens (#8644).

(TGE4) However, we must take account of *potential* equalities. Consider the
   same example again, but this time we have /not/ yet unified beta:
      forall[2] beta[1] => ...blah...

   Because beta might turn into an equality, updGivenEqs conservatively
   treats it as a potential equality, and updates inert_give_eq_lvl

(TGE5) We should not look at the equality relation involved (nominal vs
   representational), because representational equalities can still
   imply nominal ones. For example, if (G a ~R G b) and G's argument's
   role is nominal, then we can deduce a ~N b.

Historical note: prior to #24938 we also ignored Given equalities that
did not mention an "outer" type variable.  But that is wrong, as #24938
showed. Another example is immortalised in test LocalGivenEqs2
   data T where
      MkT :: F a ~ G b => a -> b -> T
   f (MkT _ _) = True
We should not infer the type for `f`; let-bound-skolems does not apply.

Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If   * the inert set contains a canonical Given CEqCan (a ~ ty)
and  * 'a' is a skolem bound in this very implication,

then:
   a) The Given is pretty much a let-binding, like
         f :: (a ~ b->c) => a -> a
      Here the equality constraint is like saying
         let a = b->c in ...
      It is not adding any new, local equality  information,
      and hence can be ignored by has_given_eqs

   b) 'a' will have been completely substituted out in the inert set,
      so we can safely discard it.

For an example, see #9211.

The actual test is in `isLetBoundSkolemCt`

Wrinkles:

(LBS1) See GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
       that the correct variable is on the left of the equality when both are
       tyvars.

(LBS2) We also want this to work for
            forall a. [G] F b ~ a   (CEqCt with TyFamLHS)
   Here the Given will have a TyFamLHS, with the skolem-bound tyvar on the RHS.
   See tests T24938a, and LocalGivenEqs.

(LBS3) Happily (LBS2) also makes cycle-breakers work. Suppose we have
            forall a. [G] (F a) Int ~ a
  where F has arity 1, and `a` is the locally-bound skolem.  Then, as
  Note [Type equality cycles] explains, we split into
           [G] F a ~ cbv, [G] cbv Int ~ a
  where `cbv` is the cycle breaker variable.  But cbv has the same level
  as `a`, so `isOuterTyVar` (called in `isLetBoundSkolemCt`) will return False.

  This actually matters occasionally: see test LocalGivenEqs.

You might wonder whether the skolem really needs to be bound "in the
very same implication" as the equality constraint.
Consider this (c.f. #15009):

  data S a where
    MkS :: (a ~ Int) => S a

  g :: forall a. S a -> a -> blah
  g x y = let h = \z. ( z :: Int
                      , case x of
                           MkS -> [y,z])
          in ...

From the type signature for `g`, we get `y::a` .  Then when we
encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
body of the lambda we'll get

  [W] alpha[1] ~ Int                             -- From z::Int
  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]

Now, unify alpha := a.  Now we are stuck with an unsolved alpha~Int!
So we must treat alpha as untouchable under the forall[2] implication.

Possible future improvements.  The current test just looks to see whether one
side of an equality is a locally-bound skolem.  But actually we could, in
theory, do better: if one side (or both sides, actually) of an equality
ineluctably mentions a local skolem, then the equality cannot possibly impact
types outside of the implication (because doing to would cause those types to be
ill-scoped). The problem is the "ineluctably": this means that no expansion,
other solving, etc., could possibly get rid of the variable. This is hard,
perhaps impossible, to know for sure, especially when we think about type family
interactions. (And it's a user-visible property so we don't want it to be hard
to predict.) So we keep the existing check, looking for one lone variable,
because we're sure that variable isn't going anywhere.

Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:

  * All canonical

  * No two dictionaries with the same head
  * No two CIrreds with the same type

  * Family equations inert wrt top-level family axioms

  * Dictionaries have no matching top-level instance

  * Given family or dictionary constraints don't mention touchable
    unification variables

  * Non-CEqCan constraints are fully rewritten with respect
    to the CEqCan equalities (modulo eqCanRewrite of course;
    eg a wanted cannot rewrite a given)

  * CEqCan equalities: see Note [inert_eqs: the inert equalities]
    Also see documentation in Constraint.Ct for a list of invariants

Note [inert_eqs: the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Our main invariant:
   the EqCts in inert_eqs should be a
        terminating generalised substitution

-------------- Definition [Can-rewrite relation] --------------
A "can-rewrite" relation between flavours, written f1 >= f2, is a
binary relation with the following properties

  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
       then either f1 >= f2 or f2 >= f1
  (See Note [Why R2?].)

Lemma (L0). If f1 >= f then f1 >= f1
Proof.      By property (R2), with f1=f2

--------- Definition [Generalised substitution] ---------------
A "generalised substitution" S is a set of triples (lhs -f-> t), where
  - lhs is a type variable or an exactly-saturated type family application
                  (that is, lhs is a CanEqLHS)
  - t is a type
  - f is a flavour

such that

  (WF1) if (lhs1 -f1-> t1) in S
           (lhs2 -f2-> t2) in S
        then (f1 >= f2) implies that lhs1 does not appear within lhs2

  (WF2) if (lhs -f-> t) is in S, then t /= lhs

  (WF3) No LHS in S is rewritable in an RHS in S,
        in the argument of a type family application (F ty1..tyn)
        where F heads a LHS in S

--------- Definition [Applying a generalised substitution] ----------
If S is a generalised substitution
   S(f,lhs)      = rhs,             if (lhs -fs-> rhs) in S, and fs >= f
   S(f,T t1..tn) = T S(f1,t1)..S(fn,tn)
   S(f,t1 t2)    = S(f,t1) S(f_N,t2)
   S(f,t)        = t
Here f1..fn are obtained from f and T using the roles of T, and f_N is
the nominal version of f.  See Note [Flavours with roles].

Notation: repeated application.
  S^0(f,t)     = t
  S^(n+1)(f,t) = S(f, S^n(t))
  S*(f,t) is the result of applying S until you reach a fixpoint

---------  Definition [Terminating generalised substitution] ---------
A generalised substitution S is *terminating* iff

  (IG1) for every f,t, there is an n such that
             S^n(f,t) = S^(n+1)(f,t)

By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.
--------- End of definitions ------------------------------------


Rationale for (WF1)-(WF3)
-------------------------
* (WF1) guarantees that S is well-defined /as a function/;
  see Theorem (S is a function)

   Theorem (S is a function): S(f,t0) is well defined as a function.
   Proof: Suppose (lhs -f1-> t1) and (lhs -f2-> t2) are both in S,
               and  f1 >= f and f2 >= f
          Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
   Note: this argument isn't quite right.  WF1 ensures that lhs1 does
   not appear inside lhs2, and that guarantees confluence. But I can't quite
   see how to make that argument precise.

* (WF2) is a bit trivial.  It means that if S is terminating, so that
  S^(n+1)(f,t) = S^n(f,t), then there is no LHS of S in S^n(f,t).  We
  never get a silly infinite sequence a -> a -> a -> a  .... which is
  technically a fixed point but would still go on for ever.

* (WF3) is need for the termination proof.

Note that termination is not the same as idempotence.  To apply S to a
type, you may have to apply it recursively.  But termination does
guarantee that this recursive use will terminate.

Note [Why R2?]
~~~~~~~~~~~~~~
R2 states that, if we have f1 >= f and f2 >= f, then either f1 >= f2 or f2 >=
f1. If we do not have R2, we will easily fall into a loop.

To see why, imagine we have f1 >= f, f2 >= f, and that's it. Then, let our
inert set S = {a -f1-> b, b -f2-> a}. Computing S(f,a) does not terminate. And
yet, we have a hard time noticing an occurs-check problem when building S, as
the two equalities cannot rewrite one another.

R2 actually restricts our ability to accept user-written programs. See
Note [Avoiding rewriting cycles] in GHC.Tc.Types.Constraint for an example.

Note [Rewritable]
~~~~~~~~~~~~~~~~~
Definition. A CanEqLHS lhs is *rewritable* in a type t if the
lhs tree appears as a subtree within t without traversing any of the following
components of t:
  * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
  * kinds of variable occurrences
The check for rewritability *does* look in kinds of the bound variable of a
ForAllTy.

The reason for this definition is that the rewriter does not rewrite in coercions
or variables' kinds. In turn, the rewriter does not need to rewrite there because
those places are never used for controlling the behaviour of the solver: these
places are not used in matching instances or in decomposing equalities.

This definition is used by the anyRewritableXXX family of functions and is meant
to model the actual behaviour in GHC.Tc.Solver.Rewrite.

Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
for all f.

Wrinkles

* Taking roles into account: we must consider a rewrite at a given role. That is,
  a rewrite arises from some equality, and that equality has a role associated
  with it. As we traverse a type, we track what role we are allowed to rewrite with.

  For example, suppose we have an inert [G] b ~R# Int. Then b is rewritable in
  Maybe b but not in F b, where F is a type function. This role-aware logic is
  present in both the anyRewritableXXX functions and in the rewriter.
  See also Note [anyRewritableTyVar must be role-aware] in GHC.Tc.Utils.TcType.

* There is one exception to the claim that non-rewritable parts of the tree do
  not affect the solver: we sometimes do an occurs-check to decide e.g. how to
  orient an equality. (See the comments on GHC.Tc.Solver.Equality.canEqTyVarFunEq.)
  Accordingly, the presence of a variable in a kind or coercion just might
  influence the solver. Here is an example:

    type family Const x y where
      Const x y = x

    AxConst :: forall x y. Const x y ~# x

    alpha :: Const Type Nat
    [W] alpha ~ Int |> (sym (AxConst Type alpha) ;;
                        AxConst Type alpha ;;
                        sym (AxConst Type Nat))

  The cast is clearly ludicrous (it ties together a cast and its symmetric
  version), but we can't quite rule it out. (See (EQ1) from Note [Respecting
  definitional equality] in GHC.Core.TyCo.Rep to see why we need the Const Type
  Nat bit.) And yet this cast will (quite rightly) prevent alpha from unifying
  with the RHS. I (Richard E) don't have an example of where this problem can
  arise from a Haskell program, but we don't have an air-tight argument for why
  the definition of *rewritable* given here is correct.

Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main Theorem [Stability under extension]
   GIVEN a "work item" [lhs_w -fw-> rhs_w]
         and a terminating generalised substitution S,

   SUCH THAT
      (T1) S(fw,lhs_w) = lhs_w   -- LHS of work-item is a fixpoint of S(fw,_)
      (T2) S(fw,rhs_w) = rhs_w   -- RHS of work-item is a fixpoint of S(fw,_)
      (T3) lhs_w not in rhs_w    -- No occurs check in the work item
             -- If lhs is a type family application, we require only that
             -- lhs is not *rewritable* in rhs_w. See Note [Rewritable] and
             -- Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
      (T4) no [lhs_s -fs-> rhs_s] in S meets [The KickOut Criteria]
           (i.e. we already kicked any such items out!)

   THEN the extended substitution T = S+(lhs_w -fw-> rhs_w)
        is a terminating generalised substitution

How do we establish these conditions?

  * (T1) and (T2) are guaranteed by exhaustively rewriting the work-item
    with S(fw,_).

  * (T3) is guaranteed by an occurs-check on the work item.
    This is done during canonicalisation, in checkTypeEq; invariant
    (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint.

  * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable.  If the inert
    set contains a triple that meets the KickOut Criteria, we kick it out and
    add it to the work list for later re-examination.  See
    Note [The KickOut Criteria]

Theorem: T (defined in "THEN" above) is a generalised substitution;
  that is, it satisfies (WF1)-(WF3)
Proof:
  (WF1) Suppose we are adding [lhs_w -fw-> rhs_w], and [lhs_s -fs-> rhs_s] is in S.
        Then:
          - by (T1)  if fs>=fw, lhs_s does not occur within lhs_w.
          - by (KK1) if fw>=fs, lhs_w is not rewritable in lhs_s, or we'd have
            kicked out the stable constraint.

  (WF2) is directly guaranteed by (T3)

  (WF3) No lhs_s in S is rewritable in rhs_w at all, because of (T2)
        And (KK2) guarantees that lhs_w is not rewritable under a type
        family in rhs_s

Note [The KickOut Criteria]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kicking out is a Bad Thing:
* It means we have to re-process a constraint.  The less we kick out, the better.
* In the limit, kicking can lead to non-termination: imagine that we /always/
  kick out the entire inert set!
* Because (mid 2024) we don't support sharing in constraints, excessive kicking out
  can lead to exponentially big constraints (#24984).

So we seek to do as little kicking out as possible.  For example, consider this,
which happens a lot:

   Inert:  g1: a ~ Maybe b
   Work:   g2: b ~ Int

We do /not/ kick out g1 when adding g2.  The new substitution S' = {g1,g2} is still
/terminating/ but it is not /idmempotent/.  To apply S' to, say, (Tree a), we may
need to apply it twice:  Tree a --> Tree (Maybe b) --> Tree (Maybe Int)

Here are the KickOut Criteria:

    When adding [lhs_w -fw-> rhs_w] to a well-formed terminating substitution S,
    element [lhs_s -fs-> rhs_s] in S meets the KickOut Criteria if:

    (KK0) fw >= fs    AND   any of (KK1), (KK2) or (KK3) hold

    * (KK1: satisfy WF1) `lhs_w` is rewritable in `lhs_s`.

    * (KK2: termination) `lhs_w` is rewritable in `rhs_s` in these positions:
        If not(fs>=fw)
        then (KK2a) anywhere
        else (KK2b) look only in the argument of type family applications,
                    whose type family heads some LHS in `S`

    * (KK3: completeness)
      If not(fs >= fw)   -- If fs can rewrite fw, kick-out is redundant/harmful
      * (KK3a) If the role of `fs` is Nominal:
           kick out if `rhs_s = lhs_w`
      * (KK3b) If the role of `fs` is Representational:
           kick out if `rhs_s` is of form `(lhs_w t1 .. tn)`

Rationale

* (KK0) kick out only if `fw` can rewrite `fs`.
  Reason: suppose we kick out (lhs1 -fs-> s), and add (lhs -fw-> t) to the ineart
  set. The latter can't rewrite the former, so the kick-out achieved nothing

* (KK1) `lhs_w` is rewritable in `lhs_s`.
  Reason: needed to guarantee (WF1).  See Theorem: T is well formed

* (KK2) see Note [KK2: termination of the extended substitution]

* (KK3) see Note [KK3: completeness of solving]

The above story is a bit vague wrt roles, but the code is not.
See Note [Flavours with roles]

Note [KK2: termination of the extended substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Proving termination of the extended substitution T is surprisingly tricky.

* Reason for (KK2a).  Consider
      Work:  [G] b ~ a
      Inert: [W] a ~ b
  If we don't kick out the inert, then we get a loop on e.g. [W] a ~ Int.
  But if both were Wanted we really should not kick out (the substitution does not
  have to be idempotent). So we only look everywhere for the `lhs_w` if
  not (fs>=fw), that is the inert item cannot rewrite the work item.  So in the
  above example we will kick out; but if both were Wanted we won't.

* Reason for (KK2b).  Consider the case where (fs >= fw)
      Work:  [G] a ~ Int
      Inert: [G] F Int ~ F a
  If we just added the work item, the substitution would loop on type (F Int).
  So we must kick out the inert item, even though (fs>=fw). (KK2b) does this
  by looking for lhs_w under type family applications in rhs_s.

  (KK2b) makes kick-out less aggressive by looking only under type-family applications,
  in the case where (fs >= fw), and that made a /huge/ difference to #24944.

Tricky examples in: #19042, #17672, #24984. The last (#24984) is particular subtle:

  Inert:   [W] g1: F a0 ~ F a1
           [W] g2: F a2 ~ F a1
           [W] g3: F a3 ~ F a1

Now we add [W] g4: F a1 ~ F a7.  Should we kick out g1,g2,g3?  No!  The
substitution doesn't need to be idempotent, merely terminating.  And in #24984
it turned out that we kept adding one new constraint and kicking out all the
previous inert ones (and that rewriting led to exponentially big constraints due
to lack of contraint sharing.)  So we only want to look /under/ type family applications.

The proof is hard. We start by ignoring flavours. Suppose that:
* We are adding [lhs_w -fw-> rhs_w] to a well-formed, terminating substitution S.
* None of the constraints in S meet the KickOut Criteria.
* Define T = S+[lhs_w -fw-> rhs_w]
* `f` is an arbitrary flavour

Lemma 1: for any lhs_s in S, T*(f,lhs_s) terminates.
  Proof.
  * We know that r1 = S*(f,lhs_s) terminates.
  * Moreover, we know there are no occurrences of lhs_w under a type family (which
    is the head of a LHS) in r1 (KK2)+(WF3).  We need (WF3) because you might wonder
    what if rhs_s is (F a), and [a --> lhs_w] was in S.  But (WF3) prevents that.
  * Define r2 = r1{rhs_w/lhs_w}.  We know that rhs_w has no occurrences of any lhs in S,
    nor of lhs_w.
  * Since any occurrence of lhs_w does not occur under a type family, the substitution
    won't make any F t1..tn ~ s in S match.
  * So r2 is a fixed point of T.

Lemma 2: T*(f,lhs_w) teminates.
  Proof: no occurrences of any LHS in rhs_w.

Theorem. For any type r, T*(r) terminates.
  Proof:
  1. Consider any sub-term of r, which is a LHS of T.
     - Rewrite it with T*; this terminates (Lemma 1).
     - Do this simultaneously to all sub-terms that match a LHS of T, yielding r1.
  2. Could this new r1 have a sub-term that is an LHS of T?  Yes, but only if r has a
     sub-term F w, and w rewrote in Step 1 to w' and F w' matches a LHS in T.
  3. Very well: apply step 1 again, but note that /doing so consumes one of the family
     applications in the original r/.
  4. After Step 1 either we have reached a fixed point, or we repeat Step 1 consuming at
     least one family application of r.
  5. There are only a finite number of family applications in r, so this process terminates.

Example:

Inert set:   gs : F Int ~ b
Work item:   gw : b ~ Int

F (F (F b)) --[gw]--> F (F (F Int)) --[gs]--> F (F b)
            --[gw]--> F (F Int)     --[gs]--> F b
            --[gw]--> F Int         --[gs]--> b
            --[gw]--> Int

Notice that each iteration of Step 1 strips off one of the layers of F, all
of which were in the original r.

The argument is even more tricky when flavours are involved, and we have not
fleshed it out in detail.

Note [KK3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(KK3) is not necessary for the extended substitution
to be terminating.  In fact (KK0) could be made stronger by saying
   ... then (not (fw >= fs) or not (fs >= fs))
But it's not enough for S to be /terminating/; we also want /completeness/.
That is, we want to be able to solve all soluble wanted equalities.
Suppose we have
   work-item   b -G-> a
   inert-item  a -W-> b
Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
so we could extend the inerts, thus:
   inert-items   b -G-> a
                 a -W-> b
But if we kicked-out the inert item, we'd get
   work-item     a -W-> b
   inert-item    b -G-> a

Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
So we add one more clause (KK3) to the kick-out criteria:

    * (KK3: completeness)
      If not(fs >= fw)   (KK3a)
      * (KK3b) If the role of `fs` is Nominal:
           kick out if `rhs_s = lhs_w`
      * (KK3c) If the role of `fs` is Representational:
           kick out if `rhs_s` is of form `(lhs_w t1 .. tn)`

Wrinkles:

* (KK3a) All this can only happen if the work-item can rewrite the inert
  one, /but not vice versa/; that is not(fs >= fw).  It is useless to kick
  out if (fs >= fw) becuase then the work-item is already fully rewritten
  by the inert item.  And too much kick-out is positively harmful.
  (Historical example #14363.)

* (KK3b) addresses teh main example above for KK3. Another way to understand
  (KK3b) is that we treat an inert item
        a -f-> b
  in the same way as
        b -f-> a
  So if we kick out one, we should kick out the other.  The orientation
  is somewhat accidental.

* (KK3c) When considering roles, we also need the second clause (KK3b). Consider
      work-item    c -G/N-> a
      inert-item   a -W/R-> b c
  The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
  But we don't kick out the inert item because not (W/R >= W/R).  So we just
  add the work item. But then, consider if we hit the following:
      work-item    b -G/N-> Id
      inert-items  a -W/R-> b c
                 c -G/N-> a
    where
      newtype Id x = Id x

  For similar reasons, if we only had (KK3a), we wouldn't kick the
  representational inert out. And then, we'd miss solving the inert, which now
  reduced to reflexivity.

  The solution here is to kick out representational inerts whenever the lhs of a
  work item is "exposed", where exposed means being at the head of the top-level
  application chain (lhs t1 .. tn).  See head_is_new_lhs. This is encoded in
  (KK3c)).


Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
set of flavours. In GHC, flavours have two components: the flavour proper,
taken from {Wanted, Given} and the equality relation (often called
role), taken from {NomEq, ReprEq}.
When substituting w.r.t. the inert set,
as described in Note [inert_eqs: the inert equalities],
we must be careful to respect all components of a flavour.
For example, if we have

  inert set: a -G/R-> Int
             b -G/R-> Bool

  type role T nominal representational

and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
T Int Bool. The reason is that T's first parameter has a nominal role, and
thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
substitution means that the proof in Note [inert_eqs: the inert equalities] may
need to be revisited, but we don't think that the end conclusion is wrong.
-}

data InertCans   -- See Note [Detailed InertCans Invariants] for more
  = IC { InertCans -> InertEqs
inert_eqs :: InertEqs
              -- See Note [inert_eqs: the inert equalities]
              -- All EqCt with a TyVarLHS; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified

       , InertCans -> InertFunEqs
inert_funeqs :: InertFunEqs
              -- All EqCt with a TyFamLHS; index is the whole family head type.
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
              --     wrt inert_eqs
              -- Can include both [G] and [W]

       , InertCans -> DictMap DictCt
inert_dicts :: DictMap DictCt
              -- Dictionaries only
              -- All fully rewritten (modulo flavour constraints)
              --     wrt inert_eqs

       , InertCans -> [QCInst]
inert_insts :: [QCInst]

       , InertCans -> DictMap DictCt
inert_safehask :: DictMap DictCt
              -- Failed dictionary resolution due to Safe Haskell overlapping
              -- instances restriction. We keep this separate from inert_dicts
              -- as it doesn't cause compilation failure, just safe inference
              -- failure.
              --
              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
              -- in GHC.Tc.Solver

       , InertCans -> InertIrreds
inert_irreds :: InertIrreds
              -- Irreducible predicates that cannot be made canonical,
              --     and which don't interact with others (e.g.  (c a))
              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])

       , InertCans -> TcLevel
inert_given_eq_lvl :: TcLevel
              -- The TcLevel of the innermost implication that has a Given
              -- equality of the sort that make a unification variable untouchable
              -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
              -- See Note [Tracking Given equalities]

       , InertCans -> Bool
inert_given_eqs :: Bool
              -- True <=> The inert Givens *at this level* (tcl_tclvl)
              --          could includes at least one equality /other than/ a
              --          let-bound skolem equality.
              -- Reason: report these givens when reporting a failed equality
              -- See Note [Tracking Given equalities]
       }

type InertEqs    = DTyVarEnv EqualCtList
type InertFunEqs = FunEqMap  EqualCtList
type InertIrreds = Bag IrredCt

instance Outputable InertCans where
  ppr :: InertCans -> SDoc
ppr (IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs
          , inert_funeqs :: InertCans -> InertFunEqs
inert_funeqs = InertFunEqs
funeqs
          , inert_dicts :: InertCans -> DictMap DictCt
inert_dicts = DictMap DictCt
dicts
          , inert_safehask :: InertCans -> DictMap DictCt
inert_safehask = DictMap DictCt
safehask
          , inert_irreds :: InertCans -> InertIrreds
inert_irreds = InertIrreds
irreds
          , inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl
          , inert_given_eqs :: InertCans -> Bool
inert_given_eqs = Bool
given_eqs
          , inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })

    = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
      [ Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (InertEqs -> Bool
forall a. DVarEnv a -> Bool
isEmptyDVarEnv InertEqs
eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Equalities ="
          SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag EqCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag ((EqCt -> Bag EqCt -> Bag EqCt) -> InertEqs -> Bag EqCt -> Bag EqCt
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs EqCt -> Bag EqCt -> Bag EqCt
forall a. a -> Bag a -> Bag a
consBag InertEqs
eqs Bag EqCt
forall a. Bag a
emptyBag)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (InertFunEqs -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap InertFunEqs
funeqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type-function equalities ="
          SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag EqCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag ((EqCt -> Bag EqCt -> Bag EqCt)
-> InertFunEqs -> Bag EqCt -> Bag EqCt
forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b
foldFunEqs EqCt -> Bag EqCt -> Bag EqCt
forall a. a -> Bag a -> Bag a
consBag InertFunEqs
funeqs Bag EqCt
forall a. Bag a
emptyBag)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (DictMap DictCt -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap DictCt
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Dictionaries =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag DictCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag (DictMap DictCt -> Bag DictCt
forall a. DictMap a -> Bag a
dictsToBag DictMap DictCt
dicts)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (DictMap DictCt -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap DictCt
safehask) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag DictCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag (DictMap DictCt -> Bag DictCt
forall a. DictMap a -> Bag a
dictsToBag DictMap DictCt
safehask)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (InertIrreds -> Bool
forall a. Bag a -> Bool
isEmptyBag InertIrreds
irreds) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Irreds =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertIrreds -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag InertIrreds
irreds
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([QCInst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QCInst]
insts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Given instances =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((QCInst -> SDoc) -> [QCInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr [QCInst]
insts)
      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Innermost given equalities =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
      , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Given eqs at this level =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
      ]


{- *********************************************************************
*                                                                      *
                   Inert equalities
*                                                                      *
********************************************************************* -}

emptyTyEqs :: InertEqs
emptyTyEqs :: InertEqs
emptyTyEqs = InertEqs
forall a. DVarEnv a
emptyDVarEnv

addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans
addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans
addEqToCans TcLevel
tc_lvl eq_ct :: EqCt
eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs })
            ics :: InertCans
ics@(IC { inert_funeqs :: InertCans -> InertFunEqs
inert_funeqs = InertFunEqs
funeqs, inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
  = TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs TcLevel
tc_lvl (EqCt -> Ct
CEqCan EqCt
eq_ct) (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
    case CanEqLHS
lhs of
       TyFamLHS TyCon
tc [Type]
tys -> InertCans
ics { inert_funeqs = addCanFunEq funeqs tc tys eq_ct }
       TyVarLHS TcTyVar
tv     -> InertCans
ics { inert_eqs    = addTyEq eqs tv eq_ct }

addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq InertEqs
old_eqs TcTyVar
tv EqCt
ct
  = (EqualCtList -> EqualCtList -> EqualCtList)
-> InertEqs -> TcTyVar -> EqualCtList -> InertEqs
forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv_C EqualCtList -> EqualCtList -> EqualCtList
add_eq InertEqs
old_eqs TcTyVar
tv [EqCt
ct]
  where
    add_eq :: EqualCtList -> EqualCtList -> EqualCtList
add_eq EqualCtList
old_eqs EqualCtList
_ = EqCt -> EqualCtList -> EqualCtList
addToEqualCtList EqCt
ct EqualCtList
old_eqs

foldTyEqs :: (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs :: forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs EqCt -> b -> b
k InertEqs
eqs b
z
  = (EqualCtList -> b -> b) -> b -> InertEqs -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (\EqualCtList
cts b
z -> (EqCt -> b -> b) -> b -> EqualCtList -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr EqCt -> b -> b
k b
z EqualCtList
cts) b
z InertEqs
eqs

findTyEqs :: InertCans -> TyVar -> [EqCt]
findTyEqs :: InertCans -> TcTyVar -> EqualCtList
findTyEqs InertCans
icans TcTyVar
tv = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat @Maybe (InertEqs -> TcTyVar -> Maybe EqualCtList
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv (InertCans -> InertEqs
inert_eqs InertCans
icans) TcTyVar
tv)

delEq :: EqCt -> InertCans -> InertCans
delEq :: EqCt -> InertCans -> InertCans
delEq (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs }) InertCans
ic = case CanEqLHS
lhs of
    TyVarLHS TcTyVar
tv
      -> InertCans
ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
    TyFamLHS TyCon
tf [Type]
args
      -> InertCans
ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
  where
    isThisOne :: EqCt -> Bool
    isThisOne :: EqCt -> Bool
isThisOne (EqCt { eq_rhs :: EqCt -> Type
eq_rhs = Type
t1 }) = Type -> Type -> Bool
tcEqTypeNoKindCheck Type
rhs Type
t1

    upd :: Maybe EqualCtList -> Maybe EqualCtList
    upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
eq_ct_list) = (EqCt -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList (Bool -> Bool
not (Bool -> Bool) -> (EqCt -> Bool) -> EqCt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> Bool
isThisOne) EqualCtList
eq_ct_list
    upd Maybe EqualCtList
Nothing           = Maybe EqualCtList
forall a. Maybe a
Nothing

findEq :: InertCans -> CanEqLHS -> [EqCt]
findEq :: InertCans -> CanEqLHS -> EqualCtList
findEq InertCans
icans (TyVarLHS TcTyVar
tv) = InertCans -> TcTyVar -> EqualCtList
findTyEqs InertCans
icans TcTyVar
tv
findEq InertCans
icans (TyFamLHS TyCon
fun_tc [Type]
fun_args)
  = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat @Maybe (InertFunEqs -> TyCon -> [Type] -> Maybe EqualCtList
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq (InertCans -> InertFunEqs
inert_funeqs InertCans
icans) TyCon
fun_tc [Type]
fun_args)

{-# INLINE partition_eqs_container #-}
partition_eqs_container
  :: forall container
   . container    -- empty container
  -> (forall b. (EqCt -> b -> b) ->  container -> b -> b) -- folder
  -> (EqCt -> container -> container)  -- extender
  -> (EqCt -> Bool)
  -> container
  -> ([EqCt], container)
partition_eqs_container :: forall container.
container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> (EqualCtList, container)
partition_eqs_container container
empty_container forall b. (EqCt -> b -> b) -> container -> b -> b
fold_container EqCt -> container -> container
extend_container EqCt -> Bool
pred container
orig_inerts
  = (EqCt -> (EqualCtList, container) -> (EqualCtList, container))
-> container
-> (EqualCtList, container)
-> (EqualCtList, container)
forall b. (EqCt -> b -> b) -> container -> b -> b
fold_container EqCt -> (EqualCtList, container) -> (EqualCtList, container)
folder container
orig_inerts ([], container
empty_container)
  where
    folder :: EqCt -> ([EqCt], container) -> ([EqCt], container)
    folder :: EqCt -> (EqualCtList, container) -> (EqualCtList, container)
folder EqCt
eq_ct (EqualCtList
acc_true, container
acc_false)
      | EqCt -> Bool
pred EqCt
eq_ct = (EqCt
eq_ct EqCt -> EqualCtList -> EqualCtList
forall a. a -> [a] -> [a]
: EqualCtList
acc_true, container
acc_false)
      | Bool
otherwise  = (EqualCtList
acc_true,         EqCt -> container -> container
extend_container EqCt
eq_ct container
acc_false)

partitionInertEqs :: (EqCt -> Bool)   -- EqCt will always have a TyVarLHS
                  -> InertEqs
                  -> ([EqCt], InertEqs)
partitionInertEqs :: (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs)
partitionInertEqs = InertEqs
-> (forall b. (EqCt -> b -> b) -> InertEqs -> b -> b)
-> (EqCt -> InertEqs -> InertEqs)
-> (EqCt -> Bool)
-> InertEqs
-> (EqualCtList, InertEqs)
forall container.
container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> (EqualCtList, container)
partition_eqs_container InertEqs
emptyTyEqs (EqCt -> b -> b) -> InertEqs -> b -> b
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs EqCt -> InertEqs -> InertEqs
addInertEqs

addInertEqs :: EqCt -> InertEqs -> InertEqs
-- Precondition: CanEqLHS is a TyVarLHS
addInertEqs :: EqCt -> InertEqs -> InertEqs
addInertEqs eq_ct :: EqCt
eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyVarLHS TcTyVar
tv }) InertEqs
eqs = InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq InertEqs
eqs TcTyVar
tv EqCt
eq_ct
addInertEqs EqCt
other InertEqs
_ = String -> SDoc -> InertEqs
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendInertEqs" (EqCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqCt
other)

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

addCanFunEq :: InertFunEqs -> TyCon -> [TcType] -> EqCt -> InertFunEqs
addCanFunEq :: InertFunEqs -> TyCon -> [Type] -> EqCt -> InertFunEqs
addCanFunEq InertFunEqs
old_eqs TyCon
fun_tc [Type]
fun_args EqCt
ct
  = InertFunEqs
-> TyCon
-> [Type]
-> (Maybe EqualCtList -> Maybe EqualCtList)
-> InertFunEqs
forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp InertFunEqs
old_eqs TyCon
fun_tc [Type]
fun_args Maybe EqualCtList -> Maybe EqualCtList
upd
  where
    upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
old_equal_ct_list) = EqualCtList -> Maybe EqualCtList
forall a. a -> Maybe a
Just (EqualCtList -> Maybe EqualCtList)
-> EqualCtList -> Maybe EqualCtList
forall a b. (a -> b) -> a -> b
$ EqCt -> EqualCtList -> EqualCtList
addToEqualCtList EqCt
ct EqualCtList
old_equal_ct_list
    upd Maybe EqualCtList
Nothing                  = EqualCtList -> Maybe EqualCtList
forall a. a -> Maybe a
Just [EqCt
ct]

foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs :: forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b
foldFunEqs EqCt -> b -> b
k InertFunEqs
fun_eqs b
z = (EqualCtList -> b -> b) -> InertFunEqs -> b -> b
forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap (\EqualCtList
eqs b
z -> (EqCt -> b -> b) -> b -> EqualCtList -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr EqCt -> b -> b
k b
z EqualCtList
eqs) InertFunEqs
fun_eqs b
z

partitionFunEqs :: (EqCt -> Bool)    -- EqCt will have a TyFamLHS
                -> InertFunEqs
                -> ([EqCt], InertFunEqs)
partitionFunEqs :: (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs)
partitionFunEqs = InertFunEqs
-> (forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b)
-> (EqCt -> InertFunEqs -> InertFunEqs)
-> (EqCt -> Bool)
-> InertFunEqs
-> (EqualCtList, InertFunEqs)
forall container.
container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> (EqualCtList, container)
partition_eqs_container InertFunEqs
forall a. TcAppMap a
emptyFunEqs (EqCt -> b -> b) -> InertFunEqs -> b -> b
forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b
foldFunEqs EqCt -> InertFunEqs -> InertFunEqs
addFunEqs

addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs
-- Precondition: EqCt is a TyFamLHS
addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs
addFunEqs eq_ct :: EqCt
eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyFamLHS TyCon
tc [Type]
args }) InertFunEqs
fun_eqs
  = InertFunEqs -> TyCon -> [Type] -> EqCt -> InertFunEqs
addCanFunEq InertFunEqs
fun_eqs TyCon
tc [Type]
args EqCt
eq_ct
addFunEqs EqCt
other InertFunEqs
_ = String -> SDoc -> InertFunEqs
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendFunEqs" (EqCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqCt
other)



{- *********************************************************************
*                                                                      *
                   Inert Dicts
*                                                                      *
********************************************************************* -}

updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts DictMap DictCt -> DictMap DictCt
upd InertCans
ics = InertCans
ics { inert_dicts = upd (inert_dicts ics) }

delDict :: DictCt -> DictMap a -> DictMap a
delDict :: forall a. DictCt -> DictMap a -> DictMap a
delDict (DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys }) DictMap a
m
  = DictMap a -> TyCon -> [Type] -> DictMap a
forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys

addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addDict item :: DictCt
item@(DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys }) DictMap DictCt
dm
  = DictMap DictCt -> TyCon -> [Type] -> DictCt -> DictMap DictCt
forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp DictMap DictCt
dm (Class -> TyCon
classTyCon Class
cls) [Type]
tys DictCt
item

addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addSolvedDict item :: DictCt
item@(DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys }) DictMap DictCt
dm
  = DictMap DictCt -> TyCon -> [Type] -> DictCt -> DictMap DictCt
forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp DictMap DictCt
dm (Class -> TyCon
classTyCon Class
cls) [Type]
tys DictCt
item

filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
filterDicts DictCt -> Bool
f DictMap DictCt
m = (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap DictCt -> Bool
f DictMap DictCt
m

partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts DictCt -> Bool
f DictMap DictCt
m = (DictCt
 -> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt))
-> DictMap DictCt
-> (Bag DictCt, DictMap DictCt)
-> (Bag DictCt, DictMap DictCt)
forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap DictCt
-> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt)
k DictMap DictCt
m (Bag DictCt
forall a. Bag a
emptyBag, DictMap DictCt
forall a. TcAppMap a
emptyDictMap)
  where
    k :: DictCt
-> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt)
k DictCt
ct (Bag DictCt
yeses, DictMap DictCt
noes) | DictCt -> Bool
f DictCt
ct      = (DictCt
ct DictCt -> Bag DictCt -> Bag DictCt
forall a. a -> Bag a -> Bag a
`consBag` Bag DictCt
yeses, DictMap DictCt
noes)
                       | Bool
otherwise = (Bag DictCt
yeses,              DictCt -> DictMap DictCt -> DictMap DictCt
addDict DictCt
ct DictMap DictCt
noes)


{- *********************************************************************
*                                                                      *
                   Inert Irreds
*                                                                      *
********************************************************************* -}

addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans
addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans
addIrredToCans TcLevel
tc_lvl IrredCt
irred InertCans
ics
  = TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs TcLevel
tc_lvl (IrredCt -> Ct
CIrredCan IrredCt
irred) (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
    (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds (IrredCt -> InertIrreds -> InertIrreds
addIrred IrredCt
irred) InertCans
ics

addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
addIrreds [IrredCt]
extras InertIrreds
irreds
  | [IrredCt] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IrredCt]
extras = InertIrreds
irreds
  | Bool
otherwise   = InertIrreds
irreds InertIrreds -> InertIrreds -> InertIrreds
forall a. Bag a -> Bag a -> Bag a
`unionBags` [IrredCt] -> InertIrreds
forall a. [a] -> Bag a
listToBag [IrredCt]
extras

addIrred :: IrredCt -> InertIrreds -> InertIrreds
addIrred :: IrredCt -> InertIrreds -> InertIrreds
addIrred IrredCt
extra InertIrreds
irreds = InertIrreds
irreds InertIrreds -> IrredCt -> InertIrreds
forall a. Bag a -> a -> Bag a
`snocBag` IrredCt
extra

updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds InertIrreds -> InertIrreds
upd InertCans
ics = InertCans
ics { inert_irreds = upd (inert_irreds ics) }

delIrred :: IrredCt -> InertCans -> InertCans
-- Remove a particular (Given) Irred, on the instructions of a plugin
-- For some reason this is done vis the evidence Id, not the type
-- Compare delEq.  I have not idea why
delIrred :: IrredCt -> InertCans -> InertCans
delIrred (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev }) InertCans
ics
  = (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds ((IrredCt -> Bool) -> InertIrreds -> InertIrreds
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag IrredCt -> Bool
keep) InertCans
ics
  where
    ev_id :: TcTyVar
ev_id = CtEvidence -> TcTyVar
ctEvEvId CtEvidence
ev
    keep :: IrredCt -> Bool
keep (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev' }) = TcTyVar
ev_id TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
/= CtEvidence -> TcTyVar
ctEvEvId CtEvidence
ev'

foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b
foldIrreds :: forall b. (IrredCt -> b -> b) -> InertIrreds -> b -> b
foldIrreds IrredCt -> b -> b
k InertIrreds
irreds b
z = (IrredCt -> b -> b) -> b -> InertIrreds -> b
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr IrredCt -> b -> b
k b
z InertIrreds
irreds

findMatchingIrreds :: InertIrreds -> CtEvidence
                   -> (Bag (IrredCt, SwapFlag), InertIrreds)
findMatchingIrreds :: InertIrreds -> CtEvidence -> (Bag (IrredCt, SwapFlag), InertIrreds)
findMatchingIrreds InertIrreds
irreds CtEvidence
ev
  | EqPred EqRel
eq_rel1 Type
lty1 Type
rty1 <- Type -> Pred
classifyPredType Type
pred
    -- See Note [Solving irreducible equalities]
  = (IrredCt -> Either (IrredCt, SwapFlag) IrredCt)
-> InertIrreds -> (Bag (IrredCt, SwapFlag), InertIrreds)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith (EqRel
-> Type -> Type -> IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_eq EqRel
eq_rel1 Type
lty1 Type
rty1) InertIrreds
irreds
  | Bool
otherwise
  = (IrredCt -> Either (IrredCt, SwapFlag) IrredCt)
-> InertIrreds -> (Bag (IrredCt, SwapFlag), InertIrreds)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_non_eq InertIrreds
irreds
  where
    pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
    match_non_eq :: IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_non_eq IrredCt
irred
      | IrredCt -> Type
irredCtPred IrredCt
irred HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
pred = (IrredCt, SwapFlag) -> Either (IrredCt, SwapFlag) IrredCt
forall a b. a -> Either a b
Left (IrredCt
irred, SwapFlag
NotSwapped)
      | Bool
otherwise                         = IrredCt -> Either (IrredCt, SwapFlag) IrredCt
forall a b. b -> Either a b
Right IrredCt
irred

    match_eq :: EqRel
-> Type -> Type -> IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_eq EqRel
eq_rel1 Type
lty1 Type
rty1 IrredCt
irred
      | EqPred EqRel
eq_rel2 Type
lty2 Type
rty2 <- Type -> Pred
classifyPredType (IrredCt -> Type
irredCtPred IrredCt
irred)
      , EqRel
eq_rel1 EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
eq_rel2
      , Just SwapFlag
swap <- Type -> Type -> Type -> Type -> Maybe SwapFlag
match_eq_help Type
lty1 Type
rty1 Type
lty2 Type
rty2
      = (IrredCt, SwapFlag) -> Either (IrredCt, SwapFlag) IrredCt
forall a b. a -> Either a b
Left (IrredCt
irred, SwapFlag
swap)
      | Bool
otherwise
      = IrredCt -> Either (IrredCt, SwapFlag) IrredCt
forall a b. b -> Either a b
Right IrredCt
irred

    match_eq_help :: Type -> Type -> Type -> Type -> Maybe SwapFlag
match_eq_help Type
lty1 Type
rty1 Type
lty2 Type
rty2
      | Type
lty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
lty2, Type
rty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
rty2
      = SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
NotSwapped
      | Type
lty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
rty2, Type
rty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
lty2
      = SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
IsSwapped
      | Bool
otherwise
      = Maybe SwapFlag
forall a. Maybe a
Nothing

{- Note [Solving irreducible equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#14333)
  [G] a b ~R# c d
  [W] c d ~R# a b
Clearly we should be able to solve this! Even though the constraints are
not decomposable. We solve this when looking up the work-item in the
irreducible constraints to look for an identical one.  When doing this
lookup, findMatchingIrreds spots the equality case, and matches either
way around. It has to return a swap-flag so we can generate evidence
that is the right way round too.
-}

{- *********************************************************************
*                                                                      *
                Adding to and removing from the inert set
*                                                                      *
*                                                                      *
********************************************************************* -}

updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
-- Set the inert_given_eq_level to the current level (tclvl)
-- if the constraint is a given equality that should prevent
-- filling in an outer unification variable.
-- See Note [Tracking Given equalities]
--
-- Precondition: Ct is either CEqCan or CIrredCan
updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs TcLevel
tclvl Ct
ct InertCans
inerts
  | Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct) = InertCans
inerts

  -- See Note [Let-bound skolems]
  | TcLevel -> Ct -> Bool
isLetBoundSkolemCt TcLevel
tclvl Ct
ct = InertCans
inerts { inert_given_eqs = True }

  -- At this point we are left with a constraint that either
  -- is an equality (F a ~ ty), or /might/ be, like (c a)
  | Bool
otherwise = InertCans
inerts { inert_given_eq_lvl = tclvl
                       , inert_given_eqs    = True }

isLetBoundSkolemCt :: TcLevel -> Ct -> Bool
-- See Note [Let-bound skolems]
isLetBoundSkolemCt :: TcLevel -> Ct -> Bool
isLetBoundSkolemCt TcLevel
tclvl (CEqCan (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs }))
  = case CanEqLHS
lhs of
      TyVarLHS TcTyVar
tv -> Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
      TyFamLHS {} -> case Type -> Maybe TcTyVar
getTyVar_maybe Type
rhs of
                       Just TcTyVar
tv -> Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
                       Maybe TcTyVar
Nothing -> Bool
False
isLetBoundSkolemCt TcLevel
_ Ct
_ = Bool
False

data KickOutSpec -- See Note [KickOutSpec]
  = KOAfterUnify  TcTyVarSet   -- We have unified these tyvars
  | KOAfterAdding CanEqLHS     -- We are adding to the inert set a canonical equality
                               -- constraint with this LHS

instance Outputable KickOutSpec where
  ppr :: KickOutSpec -> SDoc
ppr (KOAfterUnify TcTyVarSet
tvs)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"KOAfterUnify" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> TcTyVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVarSet
tvs
  ppr (KOAfterAdding CanEqLHS
lhs) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"KOAfterAdding" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs)

{- Note [KickOutSpec]
~~~~~~~~~~~~~~~~~~~~~~
KickOutSpec explains why we are kicking out.

Important property:
  KOAfterAdding (TyVarLHS tv) should behave exactly like
  KOAfterUnifying (unitVarSet tv)

The main reasons for treating the two separately are
* More efficient in the single-tyvar case
* The code is far more perspicuous
-}

data WhereToLook = LookEverywhere | LookOnlyUnderFamApps
                   deriving( WhereToLook -> WhereToLook -> Bool
(WhereToLook -> WhereToLook -> Bool)
-> (WhereToLook -> WhereToLook -> Bool) -> Eq WhereToLook
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WhereToLook -> WhereToLook -> Bool
== :: WhereToLook -> WhereToLook -> Bool
$c/= :: WhereToLook -> WhereToLook -> Bool
/= :: WhereToLook -> WhereToLook -> Bool
Eq )

kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Cts, InertCans)
-- See Note [kickOutRewritable]
kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Bag Ct, InertCans)
kickOutRewritableLHS KickOutSpec
ko_spec new_fr :: CtFlavourRole
new_fr@(CtFlavour
_, EqRel
new_role)
                     ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs      = InertEqs
tv_eqs
                             , inert_dicts :: InertCans -> DictMap DictCt
inert_dicts    = DictMap DictCt
dictmap
                             , inert_funeqs :: InertCans -> InertFunEqs
inert_funeqs   = InertFunEqs
funeqmap
                             , inert_irreds :: InertCans -> InertIrreds
inert_irreds   = InertIrreds
irreds
                             , inert_insts :: InertCans -> [QCInst]
inert_insts    = [QCInst]
old_insts })
  = (Bag Ct
kicked_out, InertCans
inert_cans_in)
  where
    -- inert_safehask stays unchanged; is that right?
    inert_cans_in :: InertCans
inert_cans_in = InertCans
ics { inert_eqs      = tv_eqs_in
                        , inert_dicts    = dicts_in
                        , inert_funeqs   = feqs_in
                        , inert_irreds   = irs_in
                        , inert_insts    = insts_in }

    kicked_out :: Cts
    kicked_out :: Bag Ct
kicked_out = ((DictCt -> Ct) -> Bag DictCt -> Bag Ct
forall a b. (a -> b) -> Bag a -> Bag b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictCt -> Ct
CDictCan Bag DictCt
dicts_out Bag Ct -> Bag Ct -> Bag Ct
`andCts` (IrredCt -> Ct) -> InertIrreds -> Bag Ct
forall a b. (a -> b) -> Bag a -> Bag b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IrredCt -> Ct
CIrredCan InertIrreds
irs_out)
                  Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` [Ct]
insts_out
                  Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` (EqCt -> Ct) -> EqualCtList -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map EqCt -> Ct
CEqCan EqualCtList
tv_eqs_out
                  Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` (EqCt -> Ct) -> EqualCtList -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map EqCt -> Ct
CEqCan EqualCtList
feqs_out

    (EqualCtList
tv_eqs_out, InertEqs
tv_eqs_in) = (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs)
partitionInertEqs EqCt -> Bool
kick_out_eq InertEqs
tv_eqs
    (EqualCtList
feqs_out,   InertFunEqs
feqs_in)   = (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs)
partitionFunEqs   EqCt -> Bool
kick_out_eq InertFunEqs
funeqmap
    (Bag DictCt
dicts_out,  DictMap DictCt
dicts_in)  = (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts    DictCt -> Bool
kick_out_dict DictMap DictCt
dictmap
    (InertIrreds
irs_out,    InertIrreds
irs_in)    = (IrredCt -> Bool) -> InertIrreds -> (InertIrreds, InertIrreds)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag      IrredCt -> Bool
kick_out_irred InertIrreds
irreds
      -- Kick out even insolubles: See Note [Rewrite insolubles]
      -- Of course we must kick out irreducibles like (c a), in case
      -- we can rewrite 'c' to something more useful

    -- Kick-out for inert instances
    -- See Note [Quantified constraints] in GHC.Tc.Solver.Solve
    insts_out :: [Ct]
    insts_in  :: [QCInst]
    ([Ct]
insts_out, [QCInst]
insts_in)
       | CtFlavourRole -> Bool
fr_may_rewrite (CtFlavour
Given, EqRel
NomEq)  -- All the insts are Givens
       = (QCInst -> Either Ct QCInst) -> [QCInst] -> ([Ct], [QCInst])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith QCInst -> Either Ct QCInst
kick_out_qci [QCInst]
old_insts
       | Bool
otherwise
       = ([], [QCInst]
old_insts)
    kick_out_qci :: QCInst -> Either Ct QCInst
kick_out_qci QCInst
qci
      | let ev :: CtEvidence
ev = QCInst -> CtEvidence
qci_ev QCInst
qci
      , WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
NomEq (CtEvidence -> Type
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
qci))
      = Ct -> Either Ct QCInst
forall a b. a -> Either a b
Left (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)
      | Bool
otherwise
      = QCInst -> Either Ct QCInst
forall a b. b -> Either a b
Right QCInst
qci

    fr_tv_can_rewrite_ty :: WhereToLook -> (TyVar -> Bool) -> EqRel -> Type -> Bool
    fr_tv_can_rewrite_ty :: WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty WhereToLook
where_to_look TcTyVar -> Bool
check_tv EqRel
role Type
ty
      = EqRel -> (Bool -> EqRel -> TcTyVar -> Bool) -> Type -> Bool
anyRewritableTyVar EqRel
role Bool -> EqRel -> TcTyVar -> Bool
can_rewrite Type
ty
      where
        can_rewrite :: UnderFam -> EqRel -> TyVar -> Bool
        can_rewrite :: Bool -> EqRel -> TcTyVar -> Bool
can_rewrite Bool
is_under_famapp EqRel
old_role TcTyVar
tv
           = (WhereToLook
where_to_look WhereToLook -> WhereToLook -> Bool
forall a. Eq a => a -> a -> Bool
== WhereToLook
LookEverywhere Bool -> Bool -> Bool
|| Bool
is_under_famapp) Bool -> Bool -> Bool
&&
             EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&& TcTyVar -> Bool
check_tv TcTyVar
tv

    fr_tf_can_rewrite_ty :: WhereToLook -> TyCon -> [TcType] -> EqRel -> Type -> Bool
    fr_tf_can_rewrite_ty :: WhereToLook -> TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty WhereToLook
where_to_look TyCon
new_tf [Type]
new_tf_args EqRel
role Type
ty
      = EqRel -> (Bool -> EqRel -> TyCon -> [Type] -> Bool) -> Type -> Bool
anyRewritableTyFamApp EqRel
role Bool -> EqRel -> TyCon -> [Type] -> Bool
can_rewrite Type
ty
      where
        can_rewrite :: UnderFam -> EqRel -> TyCon -> [TcType] -> Bool
        can_rewrite :: Bool -> EqRel -> TyCon -> [Type] -> Bool
can_rewrite Bool
is_under_famapp EqRel
old_role TyCon
old_tf [Type]
old_tf_args
          = (WhereToLook
where_to_look WhereToLook -> WhereToLook -> Bool
forall a. Eq a => a -> a -> Bool
== WhereToLook
LookEverywhere Bool -> Bool -> Bool
|| Bool
is_under_famapp) Bool -> Bool -> Bool
&&
            EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&&
            TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
new_tf [Type]
new_tf_args TyCon
old_tf [Type]
old_tf_args
              -- it's possible for old_tf_args to have too many. This is fine;
              -- we'll only check what we need to.


    fr_can_rewrite_ty :: WhereToLook -> EqRel -> Type -> Bool
    -- UnderFam = True <=> look only under type-family applications
    fr_can_rewrite_ty :: WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
uf = case KickOutSpec
ko_spec of  -- See Note [KickOutSpec]
      KOAfterUnify TcTyVarSet
tvs                    -> WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty WhereToLook
uf (TcTyVar -> TcTyVarSet -> Bool
`elemVarSet` TcTyVarSet
tvs)
      KOAfterAdding (TyVarLHS TcTyVar
tv)         -> WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty WhereToLook
uf (TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv)
      KOAfterAdding (TyFamLHS TyCon
tf [Type]
tf_args) -> WhereToLook -> TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty WhereToLook
uf TyCon
tf [Type]
tf_args

    fr_may_rewrite :: CtFlavourRole -> Bool
    fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs = CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fs
        -- Can the new item rewrite the inert item?

    kick_out_dict :: DictCt -> Bool
    -- Kick it out if the new CEqCan can rewrite the inert one
    -- See Note [kickOutRewritable]
    kick_out_dict :: DictCt -> Bool
kick_out_dict (DictCt { di_tys :: DictCt -> [Type]
di_tys = [Type]
tys, di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
      =  CtFlavourRole -> Bool
fr_may_rewrite (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
NomEq)
      Bool -> Bool -> Bool
&& (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
NomEq) [Type]
tys

    kick_out_irred :: IrredCt -> Bool
    kick_out_irred :: IrredCt -> Bool
kick_out_irred (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev })
      =  CtFlavourRole -> Bool
fr_may_rewrite (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
      Bool -> Bool -> Bool
&& WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
eq_rel Type
pred
      where
       pred :: Type
pred   = CtEvidence -> Type
ctEvPred CtEvidence
ev
       eq_rel :: EqRel
eq_rel = Type -> EqRel
predTypeEqRel Type
pred

    -- Implements criteria K1-K3 in Note [Extending the inert equalities]
    kick_out_eq :: EqCt -> Bool
    kick_out_eq :: EqCt -> Bool
kick_out_eq (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs_ty
                      , eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel })

      -- (KK0) Keep it in the inert set if the new thing can't rewrite it
      | Bool -> Bool
not (CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs)
      = Bool
False

      -- Below here (fr_may_rewrite fs) is True

      -- (KK1)
      | WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
eq_rel (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs)
      = Bool
True   -- (KK1)
         -- The above check redundantly checks the role & flavour,
         -- but it's very convenient

      -- (KK2)
      | let where_to_look :: WhereToLook
where_to_look | Bool
fs_can_rewrite_fr = WhereToLook
LookOnlyUnderFamApps
                          | Bool
otherwise         = WhereToLook
LookEverywhere
      , WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
where_to_look EqRel
eq_rel Type
rhs_ty
      = Bool
True

      -- (KK3)
      | Bool -> Bool
not Bool
fs_can_rewrite_fr                    -- (KK3a)
      , case EqRel
eq_rel of
              EqRel
NomEq  -> Type -> Bool
is_new_lhs      Type
rhs_ty   -- (KK3b)
              EqRel
ReprEq -> Type -> Bool
head_is_new_lhs Type
rhs_ty   -- (KK3c)
      = Bool
True

      | Bool
otherwise = Bool
False

      where
        fs_can_rewrite_fr :: Bool
fs_can_rewrite_fr = CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
new_fr
        fs :: CtFlavourRole
fs = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)

    is_new_lhs :: Type -> Bool
    is_new_lhs :: Type -> Bool
is_new_lhs = case KickOutSpec
ko_spec of   -- See Note [KickOutSpec]
          KOAfterUnify TcTyVarSet
tvs  -> TcTyVarSet -> Type -> Bool
is_tyvar_ty_for TcTyVarSet
tvs
          KOAfterAdding CanEqLHS
lhs -> (HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs)

    is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool
    -- True if the type is equal to one of the tyvars
    is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool
is_tyvar_ty_for TcTyVarSet
tvs Type
ty
      = case Type -> Maybe TcTyVar
getTyVar_maybe Type
ty of
          Maybe TcTyVar
Nothing -> Bool
False
          Just TcTyVar
tv -> TcTyVar
tv TcTyVar -> TcTyVarSet -> Bool
`elemVarSet` TcTyVarSet
tvs

    head_is_new_lhs :: Type -> Bool
    head_is_new_lhs :: Type -> Bool
head_is_new_lhs = case KickOutSpec
ko_spec of   -- See Note [KickOutSpec]
          KOAfterUnify TcTyVarSet
tvs                    -> (TcTyVar -> Bool) -> Type -> Bool
tv_at_head (TcTyVar -> TcTyVarSet -> Bool
`elemVarSet` TcTyVarSet
tvs)
          KOAfterAdding (TyVarLHS TcTyVar
tv)         -> (TcTyVar -> Bool) -> Type -> Bool
tv_at_head (TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv)
          KOAfterAdding (TyFamLHS TyCon
tf [Type]
tf_args) -> TyCon -> [Type] -> Type -> Bool
fam_at_head TyCon
tf [Type]
tf_args

    tv_at_head :: (TyVar -> Bool) -> Type -> Bool
    tv_at_head :: (TcTyVar -> Bool) -> Type -> Bool
tv_at_head TcTyVar -> Bool
is_tv = Type -> Bool
go
      where
        go :: Type -> Bool
go (Rep.TyVarTy TcTyVar
tv)    = TcTyVar -> Bool
is_tv TcTyVar
tv
        go (Rep.AppTy Type
fun Type
_)   = Type -> Bool
go Type
fun
        go (Rep.CastTy Type
ty KindCoercion
_)   = Type -> Bool
go Type
ty
        go (Rep.TyConApp {})   = Bool
False
        go (Rep.LitTy {})      = Bool
False
        go (Rep.ForAllTy {})   = Bool
False
        go (Rep.FunTy {})      = Bool
False
        go (Rep.CoercionTy {}) = Bool
False

    fam_at_head :: TyCon -> [Type] -> Type -> Bool
    fam_at_head :: TyCon -> [Type] -> Type -> Bool
fam_at_head TyCon
fun_tc [Type]
fun_args = Type -> Bool
go
      where
        go :: Type -> Bool
go (Rep.TyVarTy {})       = Bool
False
        go (Rep.AppTy {})         = Bool
False  -- no TyConApp to the left of an AppTy
        go (Rep.CastTy Type
ty KindCoercion
_)      = Type -> Bool
go Type
ty
        go (Rep.TyConApp TyCon
tc [Type]
args) = TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
fun_tc [Type]
fun_args TyCon
tc [Type]
args
        go (Rep.LitTy {})         = Bool
False
        go (Rep.ForAllTy {})      = Bool
False
        go (Rep.FunTy {})         = Bool
False
        go (Rep.CoercionTy {})    = Bool
False

{- Note [kickOutRewritable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
See also Note [inert_eqs: the inert equalities].

When we add a new inert equality (lhs ~N ty) to the inert set,
we must kick out any inert items that could be rewritten by the
new equality, to maintain the inert-set invariants.

  - We want to kick out an existing inert constraint if
    a) the new constraint can rewrite the inert one
    b) 'lhs' is free in the inert constraint (so that it *will*)
       rewrite it if we kick it out.

    For (b) we use anyRewritableCanLHS, which examines the types /and
    kinds/ that are directly visible in the type. Hence
    we will have exposed all the rewriting we care about to make the
    most precise kinds visible for matching classes etc. No need to
    kick out constraints that mention type variables whose kinds
    contain this LHS!

  - We don't kick out constraints from inert_solved_dicts, and
    inert_solved_funeqs optimistically. But when we lookup we have to
    take the substitution into account

NB: we could in principle avoid kick-out:
  a) When unifying a meta-tyvar from an outer level, because
     then the entire implication will be iterated; see
     Note [The Unification Level Flag] in GHC.Tc.Solver.Monad.

  b) For Givens, after a unification.  By (GivenInv) in GHC.Tc.Utils.TcType
     Note [TcLevel invariants], a Given can't include a meta-tyvar from
     its own level, so it falls under (a).  Of course, we must still
     kick out Givens when adding a new non-unification Given.

But kicking out more vigorously may lead to earlier unification and fewer
iterations, so we don't take advantage of these possibilities.

Note [Rewrite insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an insoluble alpha ~ [alpha], which is insoluble
because an occurs check.  And then we unify alpha := [Int].  Then we
really want to rewrite the insoluble to [Int] ~ [[Int]].  Now it can
be decomposed.  Otherwise we end up with a "Can't match [Int] ~
[[Int]]" which is true, but a bit confusing because the outer type
constructors match.

Hence:
 * In the main simplifier loops in GHC.Tc.Solver (solveWanteds,
   simpl_loop), we feed the insolubles in solveSimpleWanteds,
   so that they get rewritten (albeit not solved).

 * We kick insolubles out of the inert set, if they can be
   rewritten (see GHC.Tc.Solver.Monad.kick_out_rewritable)

 * We rewrite those insolubles in GHC.Tc.Solver.Equality
   See Note [Make sure that insolubles are fully rewritten]
   in GHC.Tc.Solver.Equality
-}

{- *********************************************************************
*                                                                      *
                 Queries
*                                                                      *
*                                                                      *
********************************************************************* -}

isOuterTyVar :: TcLevel -> TyCoVar -> Bool
-- True of a type variable that comes from a
-- shallower level than the ambient level (tclvl)
isOuterTyVar :: TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv
  | TcTyVar -> Bool
isTyVar TcTyVar
tv = Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl TcTyVar
tv)) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
                 TcLevel
tclvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv
    -- ASSERT: we are dealing with Givens here, and invariant (GivenInv) from
    -- Note Note [TcLevel invariants] in GHC.Tc.Utils.TcType ensures that there can't
    -- be a touchable meta tyvar.   If this wasn't true, you might worry that,
    -- at level 3, a meta-tv alpha[3] gets unified with skolem b[2], and thereby
    -- becomes "outer" even though its level numbers says it isn't.
  | Bool
otherwise  = Bool
False  -- Coercion variables; doesn't much matter

noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool
-- True <=> there is no Irred looking like (N tys1 ~ N tys2)
-- See Note [Decomposing newtype equalities] (EX2) in GHC.Tc.Solver.Equality
--     This is the only call site.
noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool
noGivenNewtypeReprEqs TyCon
tc InertSet
inerts
  = Bool -> Bool
not ((IrredCt -> Bool) -> InertIrreds -> Bool
forall a. (a -> Bool) -> Bag a -> Bool
anyBag IrredCt -> Bool
might_help (InertCans -> InertIrreds
inert_irreds (InertSet -> InertCans
inert_cans InertSet
inerts)))
  where
    might_help :: IrredCt -> Bool
might_help IrredCt
irred
      = case Type -> Pred
classifyPredType (CtEvidence -> Type
ctEvPred (IrredCt -> CtEvidence
irredCtEvidence IrredCt
irred)) of
          EqPred EqRel
ReprEq Type
t1 Type
t2
             | Just (TyCon
tc1,[Type]
_) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
t1
             , TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc1
             , Just (TyCon
tc2,[Type]
_) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
t2
             , TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
             -> Bool
True
          Pred
_  -> Bool
False

-- | Returns True iff there are no Given constraints that might,
-- potentially, match the given class constraint. This is used when checking to see if a
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in GHC.Tc.Solver.Dict
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [Type] -> Bool
noMatchableGivenDicts inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans }) CtLoc
loc_w Class
clas [Type]
tys
  = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (DictCt -> Bool) -> Bag DictCt -> Bool
forall a. (a -> Bool) -> Bag a -> Bool
anyBag DictCt -> Bool
matchable_given (Bag DictCt -> Bool) -> Bag DictCt -> Bool
forall a b. (a -> b) -> a -> b
$
    DictMap DictCt -> Class -> Bag DictCt
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap DictCt
inert_dicts InertCans
inert_cans) Class
clas
  where
    pred_w :: Type
pred_w = Class -> [Type] -> Type
mkClassPred Class
clas [Type]
tys

    matchable_given :: DictCt -> Bool
    matchable_given :: DictCt -> Bool
matchable_given (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
      | CtGiven { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: CtEvidence -> Type
ctev_pred = Type
pred_g } <- CtEvidence
ev
      = Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts Type
pred_g CtLoc
loc_g Type
pred_w CtLoc
loc_w

      | Bool
otherwise
      = Bool
False

mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst
-- See Note [What might equal later?]
-- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Dict
mightEqualLater :: InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inert_set Type
given_pred CtLoc
given_loc Type
wanted_pred CtLoc
wanted_loc
  | CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
  = Maybe Subst
forall a. Maybe a
Nothing

  | Bool
otherwise
  = case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fun [Type
flattened_given] [Type
flattened_wanted] of
      Unifiable Subst
subst
        -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
subst
      MaybeApart MaybeApartReason
reason Subst
subst
        | MaybeApartReason
MARInfinite <- MaybeApartReason
reason -- see Example 7 in the Note.
        -> Maybe Subst
forall a. Maybe a
Nothing
        | Bool
otherwise
        -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
subst
      UnifyResult
SurelyApart -> Maybe Subst
forall a. Maybe a
Nothing

  where
    in_scope :: InScopeSet
in_scope  = TcTyVarSet -> InScopeSet
mkInScopeSet (TcTyVarSet -> InScopeSet) -> TcTyVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> TcTyVarSet
tyCoVarsOfTypes [Type
given_pred, Type
wanted_pred]

    -- NB: flatten both at the same time, so that we can share mappings
    -- from type family applications to variables, and also to guarantee
    -- that the fresh variables are really fresh between the given and
    -- the wanted. Flattening both at the same time is needed to get
    -- Example 10 from the Note.
    ([Type
flattened_given, Type
flattened_wanted], TyVarEnv (TyCon, [Type])
var_mapping)
      = InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type
given_pred, Type
wanted_pred]

    bind_fun :: BindFun
    bind_fun :: BindFun
bind_fun TcTyVar
tv Type
rhs_ty
      | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
      , TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
tv (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv) Type
rhs_ty
         -- this checks for CycleBreakerTvs and TyVarTvs; forgetting
         -- the latter was #19106.
      = BindFlag
BindMe

         -- See Examples 4, 5, and 6 from the Note
      | Just (TyCon
_fam_tc, [Type]
fam_args) <- TyVarEnv (TyCon, [Type]) -> TcTyVar -> Maybe (TyCon, [Type])
forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv TyVarEnv (TyCon, [Type])
var_mapping TcTyVar
tv
      , (TcTyVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes TcTyVar -> Bool
mentions_meta_ty_var [Type]
fam_args
      = BindFlag
BindMe

      | Bool
otherwise
      = BindFlag
Apart

    -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
    -- (as they can be unified)
    -- and also for CycleBreakerTvs that mentions meta-tyvars
    mentions_meta_ty_var :: TyVar -> Bool
    mentions_meta_ty_var :: TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
tv
      | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
      = case TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv of
          -- See Examples 8 and 9 in the Note
          MetaInfo
CycleBreakerTv
            -> (TcTyVar -> Bool) -> Type -> Bool
anyFreeVarsOfType TcTyVar -> Bool
mentions_meta_ty_var
                 (TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
tv InertSet
inert_set)
          MetaInfo
_ -> Bool
True
      | Bool
otherwise
      = Bool
False

    -- Like checkTopShape, but allows cbv variables to unify
    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
_lhs_tv MetaInfo
TyVarTv Type
rhs_ty  -- see Example 3 from the Note
      | Just TcTyVar
rhs_tv <- Type -> Maybe TcTyVar
getTyVar_maybe Type
rhs_ty
      = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
rhs_tv of
          MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
TyVarTv } -> Bool
True
          MetaTv {}                     -> Bool
False  -- Could unify with anything
          SkolemTv {}                   -> Bool
True
          TcTyVarDetails
RuntimeUnk                    -> Bool
True
      | Bool
otherwise  -- not a var on the RHS
      = Bool
False
    can_unify TcTyVar
lhs_tv MetaInfo
_other Type
_rhs_ty = TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
lhs_tv

-- | Is it (potentially) loopy to use the first @ct1@ to solve @ct2@?
--
-- Necessary (but not sufficient) conditions for this function to return @True@:
--
--   - @ct1@ and @ct2@ both arise from superclass expansion,
--   - @ct1@ is a Given and @ct2@ is a Wanted.
--
-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2).
prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ...
                          -> CtLoc -- ^ ... to solve this one?
                          -> Bool  -- ^ True ==> don't solve it
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
  | GivenSCOrigin SkolemInfoAnon
_ ScDepth
_ Bool
blocked <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
given_loc
  , Bool
blocked
  , ScOrigin ClsInstOrQC
_ NakedScFlag
NakedSc <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
wanted_loc
  = Bool
True    -- Prohibited if the Wanted is a superclass
            -- and the Given has come via a superclass selection from
            -- a predicate bigger than the head
  | Bool
otherwise
  = Bool
False

{- Note [What might equal later?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We must determine whether a Given might later equal a Wanted. We
definitely need to account for the possibility that any metavariable
might be arbitrarily instantiated. Yet we do *not* want
to allow skolems in to be instantiated, as we've already rewritten
with respect to any Givens. (We're solving a Wanted here, and so
all Givens have already been processed.)

This is best understood by example.

1. C alpha  ~?  C Int

   That given certainly might match later.

2. C a  ~?  C Int

   No. No new givens are going to arise that will get the `a` to rewrite
   to Int.

3. C alpha[tv]   ~?  C Int

   That alpha[tv] is a TyVarTv, unifiable only with other type variables.
   It cannot equal later.

4. C (F alpha)   ~?   C Int

   Sure -- that can equal later, if we learn something useful about alpha.

5. C (F alpha[tv])  ~?  C Int

   This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
   Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
   and F x x = Int. Remember: returning True doesn't commit ourselves to
   anything.

6. C (F a)  ~?  C a

   No, this won't match later. If we could rewrite (F a) or a, we would
   have by now. But see also Red Herring below.

7. C (Maybe alpha)  ~?  C alpha

   We say this cannot equal later, because it would require
   alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
   we choose not to worry about it. See Note [Infinitary substitution in lookup]
   in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in
   typecheck/should_compile/T19107.

8. C cbv   ~?  C Int
   where cbv = F a

   The cbv is a cycle-breaker var which stands for F a. See
   Note [Type equality cycles] in GHC.Tc.Solver.Equality
   This is just like case 6, and we say "no". Saying "no" here is
   essential in getting the parser to type-check, with its use of DisambECP.

9. C cbv   ~?   C Int
   where cbv = F alpha

   Here, we might indeed equal later. Distinguishing between
   this case and Example 8 is why we need the InertSet in mightEqualLater.

10. C (F alpha, Int)  ~?  C (Bool, F alpha)

   This cannot equal later, because F a would have to equal both Bool and
   Int.

To deal with type family applications, we use the Core flattener. See
Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
The Core flattener replaces all type family applications with
fresh variables. The next question: should we allow these fresh
variables in the domain of a unifying substitution?

A type family application that mentions only skolems (example 6) is settled:
any skolems would have been rewritten w.r.t. Givens by now. These type family
applications match only themselves. A type family application that mentions
metavariables, on the other hand, can match anything. So, if the original type
family application contains a metavariable, we use BindMe to tell the unifier
to allow it in the substitution. On the other hand, a type family application
with only skolems is considered rigid.

This treatment fixes #18910 and is tested in
typecheck/should_compile/InstanceGivenOverlap{,2}

Red Herring
~~~~~~~~~~~
In #21208, we have this scenario:

instance forall b. C b
[G] C a[sk]
[W] C (F a[sk])

What should we do with that wanted? According to the logic above, the Given
cannot match later (this is example 6), and so we use the global instance.
But wait, you say: What if we learn later (say by a future type instance F a = a)
that F a unifies with a? That looks like the Given might really match later!

This mechanism described in this Note is *not* about this kind of situation, however.
It is all asking whether a Given might match the Wanted *in this run of the solver*.
It is *not* about whether a variable might be instantiated so that the Given matches,
or whether a type instance introduced in a downstream module might make the Given match.
The reason we care about what might match later is only about avoiding order-dependence.
That is, we don't want to commit to a course of action that depends on seeing constraints
in a certain order. But an instantiation of a variable and a later type instance
don't introduce order dependency in this way, and so mightMatchLater is right to ignore
these possibilities.

Here is an example, with no type families, that is perhaps clearer:

instance forall b. C (Maybe b)
[G] C (Maybe Int)
[W] C (Maybe a)

What to do? We *might* say that the Given could match later and should thus block
us from using the global instance. But we don't do this. Instead, we rely on class
coherence to say that choosing the global instance is just fine, even if later we
call a function with (a := Int). After all, in this run of the solver, [G] C (Maybe Int)
will definitely never match [W] C (Maybe a). (Recall that we process Givens before
Wanteds, so there is no [G] a ~ Int hanging about unseen.)

Interestingly, in the first case (from #21208), the behavior changed between
GHC 8.10.7 and GHC 9.2, with the latter behaving correctly and the former
reporting overlapping instances.

Test case: typecheck/should_compile/T21208.

-}

{- *********************************************************************
*                                                                      *
    Cycle breakers
*                                                                      *
********************************************************************* -}

-- | Return the type family application a CycleBreakerTv maps to.
lookupCycleBreakerVar :: TcTyVar    -- ^ cbv, must be a CycleBreakerTv
                      -> InertSet
                      -> TcType     -- ^ type family application the cbv maps to
lookupCycleBreakerVar :: TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
cbv (IS { inert_cycle_breakers :: InertSet -> CycleBreakerVarStack
inert_cycle_breakers = CycleBreakerVarStack
cbvs_stack })
-- This function looks at every environment in the stack. This is necessary
-- to avoid #20231. This function (and its one usage site) is the only reason
-- that we store a stack instead of just the top environment.
  | Just Type
tyfam_app <- Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert (TcTyVar -> Bool
isCycleBreakerTyVar TcTyVar
cbv) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$
                      NonEmpty (Maybe Type) -> Maybe Type
forall (f :: * -> *) a. Foldable f => f (Maybe a) -> Maybe a
firstJusts ((Bag (TcTyVar, Type) -> Maybe Type)
-> CycleBreakerVarStack -> NonEmpty (Maybe Type)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (TcTyVar -> Bag (TcTyVar, Type) -> Maybe Type
forall a b. Eq a => a -> Bag (a, b) -> Maybe b
lookupBag TcTyVar
cbv) CycleBreakerVarStack
cbvs_stack)
  = Type
tyfam_app
  | Bool
otherwise
  = String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lookupCycleBreakerVar found an unbound cycle breaker" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
cbv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CycleBreakerVarStack -> SDoc
forall a. Outputable a => a -> SDoc
ppr CycleBreakerVarStack
cbvs_stack)

-- | Push a fresh environment onto the cycle-breaker var stack. Useful
-- when entering a nested implication.
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack = (Bag (TcTyVar, Type)
forall a. Bag a
emptyBag Bag (TcTyVar, Type) -> CycleBreakerVarStack -> CycleBreakerVarStack
forall a. a -> NonEmpty a -> NonEmpty a
<|)

-- | Add a new cycle-breaker binding to the top environment on the stack.
addCycleBreakerBindings :: Bag (TcTyVar, Type)   -- ^ (cbv,expansion) pairs
                        -> InertSet -> InertSet
addCycleBreakerBindings :: Bag (TcTyVar, Type) -> InertSet -> InertSet
addCycleBreakerBindings Bag (TcTyVar, Type)
prs InertSet
ics
  = Bool -> SDoc -> InertSet -> InertSet
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (((TcTyVar, Type) -> Bool) -> Bag (TcTyVar, Type) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Bool
isCycleBreakerTyVar (TcTyVar -> Bool)
-> ((TcTyVar, Type) -> TcTyVar) -> (TcTyVar, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TcTyVar, Type) -> TcTyVar
forall a b. (a, b) -> a
fst) Bag (TcTyVar, Type)
prs) (Bag (TcTyVar, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag (TcTyVar, Type)
prs) (InertSet -> InertSet) -> InertSet -> InertSet
forall a b. (a -> b) -> a -> b
$
    InertSet
ics { inert_cycle_breakers = add_to (inert_cycle_breakers ics) }
  where
    add_to :: CycleBreakerVarStack -> CycleBreakerVarStack
add_to (Bag (TcTyVar, Type)
top_env :| [Bag (TcTyVar, Type)]
rest_envs) = (Bag (TcTyVar, Type)
prs Bag (TcTyVar, Type) -> Bag (TcTyVar, Type) -> Bag (TcTyVar, Type)
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag (TcTyVar, Type)
top_env) Bag (TcTyVar, Type)
-> [Bag (TcTyVar, Type)] -> CycleBreakerVarStack
forall a. a -> [a] -> NonEmpty a
:| [Bag (TcTyVar, Type)]
rest_envs

-- | Perform a monadic operation on all pairs in the top environment
-- in the stack.
forAllCycleBreakerBindings_ :: Monad m
                            => CycleBreakerVarStack
                            -> (TcTyVar -> TcType -> m ()) -> m ()
forAllCycleBreakerBindings_ :: forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ (Bag (TcTyVar, Type)
top_env :| [Bag (TcTyVar, Type)]
_rest_envs) TcTyVar -> Type -> m ()
action
  = Bag (TcTyVar, Type) -> ((TcTyVar, Type) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Bag (TcTyVar, Type)
top_env ((TcTyVar -> Type -> m ()) -> (TcTyVar, Type) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TcTyVar -> Type -> m ()
action)
{-# INLINABLE forAllCycleBreakerBindings_ #-}  -- to allow SPECIALISE later


{- *********************************************************************
*                                                                      *
         Solving one from another
*                                                                      *
********************************************************************* -}

data InteractResult
   = KeepInert   -- Keep the inert item, and solve the work item from it
                 -- (if the latter is Wanted; just discard it if not)
   | KeepWork    -- Keep the work item, and solve the inert item from it

instance Outputable InteractResult where
  ppr :: InteractResult -> SDoc
ppr InteractResult
KeepInert = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"keep inert"
  ppr InteractResult
KeepWork  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"keep work-item"

solveOneFromTheOther :: Ct  -- Inert    (Dict or Irred)
                     -> Ct  -- WorkItem (same predicate as inert)
                     -> InteractResult
-- Precondition:
-- * inert and work item represent evidence for the /same/ predicate
-- * Both are CDictCan or CIrredCan
--
-- We can always solve one from the other: even if both are wanted,
-- although we don't rewrite wanteds with wanteds, we can combine
-- two wanteds into one by solving one from the other

solveOneFromTheOther :: Ct -> Ct -> InteractResult
solveOneFromTheOther Ct
ct_i Ct
ct_w
  | CtWanted { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_w } <- CtEvidence
ev_w
  , CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
loc_i CtLoc
loc_w
  -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
  = -- Inert must be Given
    InteractResult
KeepWork

  | CtWanted {} <- CtEvidence
ev_w
  = -- Inert is Given or Wanted
    case CtEvidence
ev_i of
      CtGiven {} -> InteractResult
KeepInert
        -- work is Wanted; inert is Given: easy choice.

      CtWanted {} -- Both are Wanted
        -- If only one has no pending superclasses, use it
        -- Otherwise we can get infinite superclass expansion (#22516)
        -- in silly cases like   class C T b => C a b where ...
        | Bool -> Bool
not Bool
is_psc_i, Bool
is_psc_w     -> InteractResult
KeepInert
        | Bool
is_psc_i,     Bool -> Bool
not Bool
is_psc_w -> InteractResult
KeepWork

        -- If only one is a WantedSuperclassOrigin (arising from expanding
        -- a Wanted class constraint), keep the other: wanted superclasses
        -- may be unexpected by users
        | Bool -> Bool
not Bool
is_wsc_orig_i, Bool
is_wsc_orig_w     -> InteractResult
KeepInert
        | Bool
is_wsc_orig_i,     Bool -> Bool
not Bool
is_wsc_orig_w -> InteractResult
KeepWork

        -- otherwise, just choose the lower span
        -- reason: if we have something like (abs 1) (where the
        -- Num constraint cannot be satisfied), it's better to
        -- get an error about abs than about 1.
        -- This test might become more elaborate if we see an
        -- opportunity to improve the error messages
        | (RealSrcSpan -> RealSrcSpan -> Bool
forall a. Ord a => a -> a -> Bool
(<) (RealSrcSpan -> RealSrcSpan -> Bool)
-> (CtLoc -> RealSrcSpan) -> CtLoc -> CtLoc -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CtLoc -> RealSrcSpan
ctLocSpan) CtLoc
loc_i CtLoc
loc_w -> InteractResult
KeepInert
        | Bool
otherwise                        -> InteractResult
KeepWork

  -- From here on the work-item is Given

  | CtWanted { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_i } <- CtEvidence
ev_i
  , CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
loc_w CtLoc
loc_i
  = InteractResult
KeepInert   -- Just discard the un-usable Given
                -- This never actually happens because
                -- Givens get processed first

  | CtWanted {} <- CtEvidence
ev_i
  = InteractResult
KeepWork

  -- From here on both are Given
  -- See Note [Replacement vs keeping]

  | TcLevel
lvl_i TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
lvl_w
  = InteractResult
same_level_strategy

  | Bool
otherwise   -- Both are Given, levels differ
  = InteractResult
different_level_strategy
  where
     ev_i :: CtEvidence
ev_i  = Ct -> CtEvidence
ctEvidence Ct
ct_i
     ev_w :: CtEvidence
ev_w  = Ct -> CtEvidence
ctEvidence Ct
ct_w

     pred :: Type
pred  = CtEvidence -> Type
ctEvPred CtEvidence
ev_i

     loc_i :: CtLoc
loc_i  = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i
     loc_w :: CtLoc
loc_w  = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
     orig_i :: CtOrigin
orig_i = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc_i
     orig_w :: CtOrigin
orig_w = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc_w
     lvl_i :: TcLevel
lvl_i  = CtLoc -> TcLevel
ctLocLevel CtLoc
loc_i
     lvl_w :: TcLevel
lvl_w  = CtLoc -> TcLevel
ctLocLevel CtLoc
loc_w

     is_psc_w :: Bool
is_psc_w = Ct -> Bool
isPendingScDict Ct
ct_w
     is_psc_i :: Bool
is_psc_i = Ct -> Bool
isPendingScDict Ct
ct_i

     is_wsc_orig_i :: Bool
is_wsc_orig_i = CtOrigin -> Bool
isWantedSuperclassOrigin CtOrigin
orig_i
     is_wsc_orig_w :: Bool
is_wsc_orig_w = CtOrigin -> Bool
isWantedSuperclassOrigin CtOrigin
orig_w

     different_level_strategy :: InteractResult
different_level_strategy  -- Both Given
       | Type -> Bool
isIPLikePred Type
pred = if TcLevel
lvl_w TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl_i then InteractResult
KeepWork  else InteractResult
KeepInert
       | Bool
otherwise         = if TcLevel
lvl_w TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl_i then InteractResult
KeepInert else InteractResult
KeepWork
       -- See Note [Replacement vs keeping] part (1)
       -- For the isIPLikePred case see Note [Shadowing of implicit parameters]
       --                               in GHC.Tc.Solver.Dict

     same_level_strategy :: InteractResult
same_level_strategy -- Both Given
       = case (CtOrigin
orig_i, CtOrigin
orig_w) of

           (GivenSCOrigin SkolemInfoAnon
_ ScDepth
depth_i Bool
blocked_i, GivenSCOrigin SkolemInfoAnon
_ ScDepth
depth_w Bool
blocked_w)
             | Bool
blocked_i, Bool -> Bool
not Bool
blocked_w -> InteractResult
KeepWork  -- Case 2(a) from
             | Bool -> Bool
not Bool
blocked_i, Bool
blocked_w -> InteractResult
KeepInert -- Note [Replacement vs keeping]

             -- Both blocked or both not blocked

             | ScDepth
depth_w ScDepth -> ScDepth -> Bool
forall a. Ord a => a -> a -> Bool
< ScDepth
depth_i -> InteractResult
KeepWork   -- Case 2(c) from
             | Bool
otherwise         -> InteractResult
KeepInert  -- Note [Replacement vs keeping]

           (GivenSCOrigin {}, CtOrigin
_) -> InteractResult
KeepWork  -- Case 2(b) from Note [Replacement vs keeping]

           (CtOrigin, CtOrigin)
_ -> InteractResult
KeepInert  -- Case 2(d) from Note [Replacement vs keeping]

{-
Note [Replacement vs keeping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have two Given constraints both of type (C tys), say, which should
we keep?  More subtle than you might think! This is all implemented in
solveOneFromTheOther.

  1) Constraints come from different levels (different_level_strategy)

      - For implicit parameters we want to keep the innermost (deepest)
        one, so that it overrides the outer one.
        See Note [Shadowing of implicit parameters] in GHC.Tc.Solver.Dict

      - For everything else, we want to keep the outermost one.  Reason: that
        makes it more likely that the inner one will turn out to be unused,
        and can be reported as redundant.  See Note [Tracking redundant constraints]
        in GHC.Tc.Solver.

        It transpires that using the outermost one is responsible for an
        8% performance improvement in nofib cryptarithm2, compared to
        just rolling the dice.  I didn't investigate why.

  2) Constraints coming from the same level (i.e. same implication)

       (a) If both are GivenSCOrigin, choose the one that is unblocked if possible
           according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.

       (b) Prefer constraints that are not superclass selections. Example:

             f :: (Eq a, Ord a) => a -> Bool
             f x = x == x

           Eager superclass expansion gives us two [G] Eq a constraints. We
           want to keep the one from the user-written Eq a, not the superclass
           selection. This means we report the Ord a as redundant with
           -Wredundant-constraints, not the Eq a.

           Getting this wrong was #20602. See also
           Note [Tracking redundant constraints] in GHC.Tc.Solver.

       (c) If both are GivenSCOrigin, chooose the one with the shallower
           superclass-selection depth, in the hope of identifying more correct
           redundant constraints. This is really a generalization of point (b),
           because the superclass depth of a non-superclass constraint is 0.

           (If the levels differ, we definitely won't have both with GivenSCOrigin.)

       (d) Finally, when there is still a choice, use KeepInert rather than
           KeepWork, for two reasons:
             - to avoid unnecessary munging of the inert set.
             - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Dict

Doing the level-check for implicit parameters, rather than making the work item
always override, is important.  Consider

    data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }

    f :: (?x::a) => T a -> Int
    f T1 = ?x
    f T2 = 3

We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
two new givens in the work-list:  [G] (?x::Int)
                                  [G] (a ~ Int)
Now consider these steps
  - process a~Int, kicking out (?x::a)
  - process (?x::Int), the inner given, adding to inert set
  - process (?x::a), the outer given, overriding the inner given
Wrong!  The level-check ensures that the inner implicit parameter wins.
(Actually I think that the order in which the work-list is processed means
that this chain of events won't happen, but that's very fragile.)
-}