{-# 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, extendWorkListEq,
    appendWorkList, extendWorkListImplic,
    workListSize,
    selectWorkItem,

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

    noMatchableGivenDicts,
    noGivenIrreds,
    mightEqualLater,
    prohibitedSuperClassSolve,

    -- * Inert equalities
    foldTyEqs, delEq, findEq,
    partitionInertEqs, partitionFunEqs,

    -- * Kick-out
    kickOutRewritableLHS,

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

  ) where

import GHC.Prelude

import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Solver.Types
import GHC.Tc.Utils.TcType

import GHC.Types.Var
import GHC.Types.Var.Env

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.Unify

import GHC.Data.Bag
import GHC.Utils.Misc       ( partitionWith )
import GHC.Utils.Outputable
import GHC.Utils.Panic

import Data.List          ( partition )
import Data.List.NonEmpty ( NonEmpty(..), (<|) )
import qualified Data.List.NonEmpty as NE
import GHC.Utils.Panic.Plain
import GHC.Data.Maybe
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 /first/:

* (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.

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     :: [Ct]  -- CEqCan, CDictCan, CIrredCan
                             -- Given and Wanted
                       -- 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_rest    :: [Ct]

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

appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
    (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs1, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest1
        , wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics1 })
    (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs2, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2
        , wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
   = WL { wl_eqs :: [Ct]
wl_eqs     = [Ct]
eqs1     [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
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 -> Int
workListSize (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  = [Ct] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
eqs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Ct] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
rest

extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl = WorkList
wl { wl_eqs = ct : wl_eqs wl }

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
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
 = case TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct) of
     EqPred {}
       -> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl

     ClassPred Class
cls [TcType]
_  -- See Note [Prioritise class equalities]
       |  Class -> Bool
isEqPredClass Class
cls
       -> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl

     Pred
_ -> Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl

extendWorkListCts :: [Ct] -> WorkList -> WorkList
-- Agnostic
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts [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

isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, 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 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 :: [Ct]
wl_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 :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  | Ct
ct:[Ct]
cts <- [Ct]
eqs  = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_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 :: WorkList -> [Ct]
wl_eqs = [Ct]
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) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"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]
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 [(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.Canonical
   -- Why store the outer implications? For the use in mightEqualLater (only)

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 CtEvidence
inert_solved_dicts   :: DictMap CtEvidence
              -- All Wanteds, of form ev :: C t1 .. tn
              -- 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 CtEvidence
inert_solved_dicts = DictMap CtEvidence
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 ([CtEvidence] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
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 ((CtEvidence -> SDoc) -> [CtEvidence] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
dicts) ]
         where
           dicts :: [CtEvidence]
dicts = Bag CtEvidence -> [CtEvidence]
forall a. Bag a -> [a]
bagToList (DictMap CtEvidence -> Bag CtEvidence
forall a. DictMap a -> Bag a
dictsToBag DictMap CtEvidence
solved_dicts)

emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
  = IC { inert_eqs :: InertEqs
inert_eqs          = InertEqs
forall a. DVarEnv a
emptyDVarEnv
       , inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
topTcLevel
       , inert_given_eqs :: Bool
inert_given_eqs    = Bool
False
       , inert_dicts :: DictMap Ct
inert_dicts        = DictMap Ct
forall a. DictMap a
emptyDictMap
       , inert_safehask :: DictMap Ct
inert_safehask     = DictMap Ct
forall a. DictMap a
emptyDictMap
       , inert_funeqs :: FunEqMap [Ct]
inert_funeqs       = FunEqMap [Ct]
forall a. DictMap a
emptyFunEqs
       , inert_insts :: [QCInst]
inert_insts        = []
       , inert_irreds :: Cts
inert_irreds       = Cts
emptyCts }

emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
  = IS { inert_cans :: InertCans
inert_cans           = InertCans
emptyInertCans
       , inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = [] [(TcTyVar, TcType)]
-> [[(TcTyVar, TcType)]] -> CycleBreakerVarStack
forall a. a -> [a] -> NonEmpty a
:| []
       , inert_famapp_cache :: FunEqMap Reduction
inert_famapp_cache   = FunEqMap Reduction
forall a. DictMap a
emptyFunEqs
       , inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts   = DictMap CtEvidence
forall a. DictMap 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.Interact.doTopReactDict

  - 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 updateGivenEqs.

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?

* We do /not/ need to worry about let-bound skolems, such ast
     forall[2] a. a ~ [b] => blah
  See Note [Let-bound skolems]

* 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).

 * 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, updateGivenEqs conservatively
   treats it as a potential equality, and updates inert_give_eq_lvl

 * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?

   That Given cannot affect the Wanted, because the Given is entirely
   *local*: it mentions only skolems bound in the very same
   implication. Such equalities need not make alpha untouchable. (Test
   case typecheck/should_compile/LocalGivenEqs has a real-life
   motivating example, with some detailed commentary.)
   Hence the 'mentionsOuterVar' test in updateGivenEqs.

   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 to set the ic_given_eqs field to LocalGivenEqs;
   see the function getHasGivenEqs.

   Here is a simpler case that triggers this behaviour:

     data T where
       MkT :: F a ~ G b => a -> b -> T

     f (MkT _ _) = True

   Because of this behaviour around local equality givens, we can infer the
   type of f. This is typecheck/should_compile/LocalGivenEqs2.

 * We need 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.

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.

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

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.

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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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

Definition [Applying a generalised substitution]
If S is a generalised substitution
   S(f,t0) = t,  if (t0 -fs-> t) in S, and fs >= f
           = apply S to components of t0, otherwise
See also Note [Flavours with roles].

Theorem: 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)

Notation: repeated application.
  S^0(f,t)     = t
  S^(n+1)(f,t) = S(f, S^n(t))

Definition: terminating generalised substitution
A generalised substitution S is *terminating* iff

  (IG1) there is an n such that
        for every f,t, 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.

-----------------------------------------------------------------------------
Our main invariant:
   the CEqCans in inert_eqs should be a terminating generalised substitution
-----------------------------------------------------------------------------

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]
~~~~~~~~~~~~~~~~~
This Note defines what it means for a type variable or type family application
(that is, a CanEqLHS) to be rewritable in a type. This definition is used
by the anyRewritableXXX family of functions and is meant to model the actual
behaviour in GHC.Tc.Solver.Rewrite.

Ignoring roles (for now): 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.

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.

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.

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.Canonical.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.

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.

Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main Theorem [Stability under extension]
   Suppose we have a "work item"
       lhs -fw-> t
   and a terminating generalised substitution S,
   THEN the extended substitution T = S+(lhs -fw-> t)
        is a terminating generalised substitution
   PROVIDED
      (T1) S(fw,lhs) = lhs   -- LHS of work-item is a fixpoint of S(fw,_)
      (T2) S(fw,t)   = t     -- RHS of work-item is a fixpoint of S(fw,_)
      (T3) lhs not in t      -- No occurs check in the work item
          -- If lhs is a type family application, we require only that
          -- lhs is not *rewritable* in t. See Note [Rewritable] and
          -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.

      AND, for every (lhs1 -fs-> s) in S:
           (K0) not (fw >= fs)
                Reason: suppose we kick out (lhs1 -fs-> s),
                        and add (lhs -fw-> t) to the inert set.
                        The latter can't rewrite the former,
                        so the kick-out achieved nothing

              -- From here, we can assume fw >= fs
           OR (K4) lhs1 is a tyvar AND fs >= fw

           OR { (K1) lhs is not rewritable in lhs1. See Note [Rewritable].
                     Reason: if fw >= fs, WF1 says we can't have both
                             lhs0 -fw-> t  and  F lhs0 -fs-> s

                AND (K2): guarantees termination of the new substitution
                    {  (K2a) not (fs >= fs)
                    OR (K2b) lhs not in s }

                AND (K3) See Note [K3: completeness of solving]
                    { (K3a) If the role of fs is nominal: s /= lhs
                      (K3b) If the role of fs is representational:
                            s is not of form (lhs t1 .. tn) } }


Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable

The idea is that
* 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 [CEqCan occurs check] in GHC.Tc.Types.Constraint.

* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
  "keep" criteria.) If the current inert S contains a triple that does
  not satisfy (K1-3), then we remove it from S by "kicking it out",
  and re-processing it.

* Note that kicking out is a Bad Thing, because it means we have to
  re-process a constraint.  The less we kick out, the better.
  TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
  this but haven't done the empirical study to check.

* Assume we have  G>=G, G>=W and that's all.  Then, when performing
  a unification we add a new given  a -G-> ty.  But doing so does NOT require
  us to kick out an inert wanted that mentions a, because of (K2a).  This
  is a common case, hence good not to kick out. See also (K2a) below.

* Lemma (L1): The conditions of the Main Theorem imply that there is no
              (lhs -fs-> t) in S, s.t.  (fs >= fw).
  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
  S(fw,lhs)=lhs.  But since fs>=fw, S(fw,lhs) = t, hence t=lhs.  But now we
  have (lhs -fs-> lhs) in S, which contradicts (WF2).

* The extended substitution satisfies (WF1) and (WF2)
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
  - (T3) guarantees (WF2).

* (K2) and (K4) are about termination.  Intuitively, any infinite chain S^0(f,t),
  S^1(f,t), S^2(f,t).... must pass through the new work item infinitely
  often, since the substitution without the work item is terminating; and must
  pass through at least one of the triples in S infinitely often.

  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f)
    (this is Lemma (L0)), and hence this triple never plays a role in application S(f,t).
    It is always safe to extend S with such a triple.

    (NB: we could strengthen K1) in this way too, but see K3.

  - (K2b): if lhs not in s, we have no further opportunity to apply the
    work item

  - (K4): See Note [K4]

* Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
  if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
  Proof. K4 holds; thus, we keep.

Key lemma to make it watertight.
  Under the conditions of the Main Theorem,
  forall f st fw >= f, a is not in S^k(f,t), for any k

Also, consider roles more carefully. See Note [Flavours with roles]

Note [K4]
~~~~~~~~~
K4 is a "keep" condition of Note [Extending the inert equalities].
Here is the scenario:

* We are considering adding (lhs -fw-> t) to the inert set S.
* S already has (lhs1 -fs-> s).
* We know S(fw, lhs) = lhs, S(fw, t) = t, and lhs is not rewritable in t.
  See Note [Rewritable]. These are (T1), (T2), and (T3).
* We further know fw >= fs. (If not, then we short-circuit via (K0).)

K4 says that we may keep lhs1 -fs-> s in S if:
  lhs1 is a tyvar AND fs >= fw

Why K4 guarantees termination:
  * If fs >= fw, we know a is not rewritable in t, because of (T2).
  * We further know lhs /= a, because of (T1).
  * Accordingly, a use of the new inert item lhs -fw-> t cannot create the conditions
    for a use of a -fs-> s (precisely because t does not mention a), and hence,
    the extended substitution (with lhs -fw-> t in it) is a terminating
    generalised substitution.

Recall that the termination generalised substitution includes only mappings that
pass an occurs check. This is (T3). At one point, we worried that the
argument here would fail if s mentioned a, but (T3) rules out this possibility.
Put another way: the terminating generalised substitution considers only the inert_eqs,
not other parts of the inert set (such as the irreds).

Can we liberalise K4? No.

Why we cannot drop the (fs >= fw) condition:
  * Suppose not (fs >= fw). It might be the case that t mentions a, and this
    can cause a loop. Example:

      Work:  [G] b ~ a
      Inert: [W] a ~ b

    (where G >= G, G >= W, and W >= W)
    If we don't kick out the inert, then we get a loop on e.g. [W] a ~ Int.

  * Note that the above example is different if the inert is a Given G, because
    (T1) won't hold.

Why we cannot drop the tyvar condition:
  * Presume fs >= fw. Thus, F tys is not rewritable in t, because of (T2).
  * Can the use of lhs -fw-> t create the conditions for a use of F tys -fs-> s?
    Yes! This can happen if t appears within tys.

    Here is an example:

      Work:  [G] a ~ Int
      Inert: [G] F Int ~ F a

    Now, if we have [W] F a ~ Bool, we will rewrite ad infinitum on the left-hand
    side. The key reason why K2b works in the tyvar case is that tyvars are atomic:
    if the right-hand side of an equality does not mention a variable a, then it
    cannot allow an equality with an LHS of a to fire. This is not the case for
    type family applications.

Bottom line: K4 can keep only inerts with tyvars on the left. Put differently,
K4 will never prevent an inert with a type family on the left from being kicked
out.

Consequence: We never kick out a Given/Nominal equality with a tyvar on the left.
This is Lemma (L3) of Note [Extending the inert equalities]. It is good because
it means we can effectively model the mutable filling of metavariables with
Given/Nominal equalities. That is: it should be the case that we could rewrite
our solver never to fill in a metavariable; instead, it would "solve" a wanted
like alpha ~ Int by turning it into a Given, allowing it to be used in rewriting.
We would want the solver to behave the same whether it uses metavariables or
Givens. And (L3) says that no Given/Nominals over tyvars are ever kicked out,
just like we never unfill a metavariable. Nice.

Getting this wrong (that is, allowing K4 to apply to situations with the type
family on the left) led to #19042. (At that point, K4 was known as K2b.)

Originally, this condition was part of K2, but #17672 suggests it should be
a top-level K condition.

Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
to be terminating.  In fact K1 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 to the kick-out criteria

Another way to understand (K3) 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.

When considering roles, we also need the second clause (K3b). 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 (K3a), 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
is_can_eq_lhs_head. This is encoded in (K3b).

Beware: if we make this test succeed too often, we kick out too much,
and the solver might loop.  Consider (#14363)
  work item:   [G] a ~R f b
  inert item:  [G] b ~R f a
In GHC 8.2 the completeness tests more aggressive, and kicked out
the inert item; but no rewriting happened and there was an infinite
loop.  All we need is to have the tyvar at the head.

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 CEqCans with a TyVarLHS; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified

       , InertCans -> FunEqMap [Ct]
inert_funeqs :: FunEqMap EqualCtList
              -- All CEqCans 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 Ct
inert_dicts :: DictMap Ct
              -- Dictionaries only
              -- All fully rewritten (modulo flavour constraints)
              --     wrt inert_eqs

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

       , InertCans -> DictMap Ct
inert_safehask :: DictMap Ct
              -- 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 -> Cts
inert_irreds :: Cts
              -- 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

instance Outputable InertCans where
  ppr :: InertCans -> SDoc
ppr (IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs
          , inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
funeqs
          , inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts
          , inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask
          , inert_irreds :: InertCans -> Cts
inert_irreds = Cts
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
<+> Cts -> SDoc
pprCts (([Ct] -> Cts -> Cts) -> Cts -> InertEqs -> Cts
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv [Ct] -> Cts -> Cts
folder Cts
emptyCts InertEqs
eqs)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (FunEqMap [Ct] -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap [Ct]
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
<+> Cts -> SDoc
pprCts (([Ct] -> Cts -> Cts) -> FunEqMap [Ct] -> Cts -> Cts
forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs [Ct] -> Cts -> Cts
folder FunEqMap [Ct]
funeqs Cts
emptyCts)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (DictMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
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
<+> Cts -> SDoc
pprCts (DictMap Ct -> Cts
forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
dicts)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (DictMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
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
<+> Cts -> SDoc
pprCts (DictMap Ct -> Cts
forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
safehask)
      , Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (Cts -> Bool
isEmptyCts Cts
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
<+> Cts -> SDoc
pprCts Cts
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
      ]
    where
      folder :: [Ct] -> Cts -> Cts
folder [Ct]
eqs Cts
rest = [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
eqs Cts -> Cts -> Cts
`andCts` Cts
rest

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

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

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

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

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

delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq InertCans
ic CanEqLHS
lhs TcType
rhs = case CanEqLHS
lhs of
    TyVarLHS TcTyVar
tv
      -> InertCans
ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
    TyFamLHS TyCon
tf [TcType]
args
      -> InertCans
ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
  where
    isThisOne :: Ct -> Bool
    isThisOne :: Ct -> Bool
isThisOne (CEqCan { cc_rhs :: Ct -> TcType
cc_rhs = TcType
t1 }) = TcType -> TcType -> Bool
tcEqTypeNoKindCheck TcType
rhs TcType
t1
    isThisOne Ct
other = String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"delEq" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ic SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
other)

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

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

{-# INLINE partition_eqs_container #-}
partition_eqs_container
  :: forall container
   . container    -- empty container
  -> (forall b. (EqualCtList -> b -> b) -> b -> container -> b) -- folder
  -> (container -> CanEqLHS -> EqualCtList -> container)  -- extender
  -> (Ct -> Bool)
  -> container
  -> ([Ct], container)
partition_eqs_container :: forall container.
container
-> (forall b. ([Ct] -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> [Ct] -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container container
empty_container forall b. ([Ct] -> b -> b) -> b -> container -> b
fold_container container -> CanEqLHS -> [Ct] -> container
extend_container Ct -> Bool
pred container
orig_inerts
  = ([Ct] -> ([Ct], container) -> ([Ct], container))
-> ([Ct], container) -> container -> ([Ct], container)
forall b. ([Ct] -> b -> b) -> b -> container -> b
fold_container [Ct] -> ([Ct], container) -> ([Ct], container)
folder ([], container
empty_container) container
orig_inerts
  where
    folder :: EqualCtList -> ([Ct], container) -> ([Ct], container)
    folder :: [Ct] -> ([Ct], container) -> ([Ct], container)
folder [Ct]
eqs ([Ct]
acc_true, container
acc_false)
      = ([Ct]
eqs_true [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
acc_true, container
acc_false')
      where
        ([Ct]
eqs_true, [Ct]
eqs_false) = (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Ct -> Bool
pred [Ct]
eqs

        acc_false' :: container
acc_false'
          | CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs } : [Ct]
_ <- [Ct]
eqs_false
          = container -> CanEqLHS -> [Ct] -> container
extend_container container
acc_false CanEqLHS
lhs [Ct]
eqs_false
          | Bool
otherwise
          = container
acc_false

partitionInertEqs :: (Ct -> Bool)   -- Ct will always be a CEqCan with a TyVarLHS
                  -> InertEqs
                  -> ([Ct], InertEqs)
partitionInertEqs :: (Ct -> Bool) -> InertEqs -> ([Ct], InertEqs)
partitionInertEqs = InertEqs
-> (forall b. ([Ct] -> b -> b) -> b -> InertEqs -> b)
-> (InertEqs -> CanEqLHS -> [Ct] -> InertEqs)
-> (Ct -> Bool)
-> InertEqs
-> ([Ct], InertEqs)
forall container.
container
-> (forall b. ([Ct] -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> [Ct] -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container InertEqs
forall a. DVarEnv a
emptyDVarEnv ([Ct] -> b -> b) -> b -> InertEqs -> b
forall b. ([Ct] -> b -> b) -> b -> InertEqs -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv InertEqs -> CanEqLHS -> [Ct] -> InertEqs
extendInertEqs

-- precondition: CanEqLHS is a TyVarLHS
extendInertEqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extendInertEqs :: InertEqs -> CanEqLHS -> [Ct] -> InertEqs
extendInertEqs InertEqs
eqs (TyVarLHS TcTyVar
tv) [Ct]
new_eqs = InertEqs -> TcTyVar -> [Ct] -> InertEqs
forall a. DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv InertEqs
eqs TcTyVar
tv [Ct]
new_eqs
extendInertEqs InertEqs
_ CanEqLHS
other [Ct]
_ = String -> SDoc -> InertEqs
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendInertEqs" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)

partitionFunEqs :: (Ct -> Bool)    -- Ct will always be a CEqCan with a TyFamLHS
                -> FunEqMap EqualCtList
                -> ([Ct], FunEqMap EqualCtList)
partitionFunEqs :: (Ct -> Bool) -> FunEqMap [Ct] -> ([Ct], FunEqMap [Ct])
partitionFunEqs
  = FunEqMap [Ct]
-> (forall b. ([Ct] -> b -> b) -> b -> FunEqMap [Ct] -> b)
-> (FunEqMap [Ct] -> CanEqLHS -> [Ct] -> FunEqMap [Ct])
-> (Ct -> Bool)
-> FunEqMap [Ct]
-> ([Ct], FunEqMap [Ct])
forall container.
container
-> (forall b. ([Ct] -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> [Ct] -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container FunEqMap [Ct]
forall a. DictMap a
emptyFunEqs (\ [Ct] -> b -> b
f b
z FunEqMap [Ct]
eqs -> ([Ct] -> b -> b) -> FunEqMap [Ct] -> b -> b
forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs [Ct] -> b -> b
f FunEqMap [Ct]
eqs b
z) FunEqMap [Ct] -> CanEqLHS -> [Ct] -> FunEqMap [Ct]
extendFunEqs

-- precondition: CanEqLHS is a TyFamLHS
extendFunEqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList
extendFunEqs :: FunEqMap [Ct] -> CanEqLHS -> [Ct] -> FunEqMap [Ct]
extendFunEqs FunEqMap [Ct]
eqs (TyFamLHS TyCon
tf [TcType]
args) [Ct]
new_eqs = FunEqMap [Ct] -> TyCon -> [TcType] -> [Ct] -> FunEqMap [Ct]
forall a. TcAppMap a -> TyCon -> [TcType] -> a -> TcAppMap a
insertTcApp FunEqMap [Ct]
eqs TyCon
tf [TcType]
args [Ct]
new_eqs
extendFunEqs FunEqMap [Ct]
_ CanEqLHS
other [Ct]
_ = String -> SDoc -> FunEqMap [Ct]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendFunEqs" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)

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

addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
addInertItem TcLevel
tc_lvl
             ics :: InertCans
ics@(IC { inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
funeqs, inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
             item :: Ct
item@(CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs })
  = TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
    case CanEqLHS
lhs of
       TyFamLHS TyCon
tc [TcType]
tys -> InertCans
ics { inert_funeqs = addCanFunEq funeqs tc tys item }
       TyVarLHS TcTyVar
tv     -> InertCans
ics { inert_eqs    = addTyEq eqs tv item }

addInertItem TcLevel
tc_lvl ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds }) item :: Ct
item@(CIrredCan {})
  = TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$   -- An Irred might turn out to be an
                                 -- equality, so we play safe
    InertCans
ics { inert_irreds = irreds `snocBag` item }

addInertItem TcLevel
_ InertCans
ics item :: Ct
item@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [TcType]
cc_tyargs = [TcType]
tys })
  = InertCans
ics { inert_dicts = addDict (inert_dicts ics) cls tys item }

addInertItem TcLevel
_ InertCans
_ Ct
item
  = String -> SDoc -> InertCans
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"upd_inert set: can't happen! Inserting " (SDoc -> InertCans) -> SDoc -> InertCans
forall a b. (a -> b) -> a -> b
$
    Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
item   -- Can't be CNonCanonical because they only land in inert_irreds

updateGivenEqs :: 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]
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tclvl Ct
ct inerts :: InertCans
inerts@(IC { inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl })
  | Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct) = InertCans
inerts
  | Ct -> Bool
not_equality Ct
ct    = InertCans
inerts -- See Note [Let-bound skolems]
  | Bool
otherwise          = InertCans
inerts { inert_given_eq_lvl = ge_lvl'
                                , inert_given_eqs    = True }
  where
    ge_lvl' :: TcLevel
ge_lvl' | TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl (Ct -> CtEvidence
ctEvidence Ct
ct)
              -- Includes things like (c a), which *might* be an equality
            = TcLevel
tclvl
            | Bool
otherwise
            = TcLevel
ge_lvl

    not_equality :: Ct -> Bool
    -- True <=> definitely not an equality of any kind
    --          except for a let-bound skolem, which doesn't count
    --          See Note [Let-bound skolems]
    -- NB: no need to spot the boxed CDictCan (a ~ b) because its
    --     superclass (a ~# b) will be a CEqCan
    not_equality :: Ct -> Bool
not_equality (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv }) = Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
    not_equality (CDictCan {})                     = Bool
True
    not_equality Ct
_                                 = Bool
False

kickOutRewritableLHS :: CtFlavourRole  -- Flavour/role of the equality that
                                       -- is being added to the inert set
                     -> CanEqLHS       -- The new equality is lhs ~ ty
                     -> InertCans
                     -> (WorkList, InertCans)
-- See Note [kickOutRewritable]
kickOutRewritableLHS :: CtFlavourRole -> CanEqLHS -> InertCans -> (WorkList, InertCans)
kickOutRewritableLHS CtFlavourRole
new_fr CanEqLHS
new_lhs
                     ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs      = InertEqs
tv_eqs
                             , inert_dicts :: InertCans -> DictMap Ct
inert_dicts    = DictMap Ct
dictmap
                             , inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs   = FunEqMap [Ct]
funeqmap
                             , inert_irreds :: InertCans -> Cts
inert_irreds   = Cts
irreds
                             , inert_insts :: InertCans -> [QCInst]
inert_insts    = [QCInst]
old_insts })
  = (WorkList
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 :: WorkList
    -- NB: use extendWorkList to ensure that kicked-out equalities get priority
    -- See Note [Prioritise equalities] (Kick-out).
    -- The irreds may include non-canonical (hetero-kinded) equality
    -- constraints, which perhaps may have become soluble after new_lhs
    -- is substituted; ditto the dictionaries, which may include (a~b)
    -- or (a~~b) constraints.
    kicked_out :: WorkList
kicked_out = (Ct -> WorkList -> WorkList) -> WorkList -> Cts -> 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
emptyWorkList { wl_eqs = tv_eqs_out ++ feqs_out })
                          ((Cts
dicts_out Cts -> Cts -> Cts
`andCts` Cts
irs_out)
                            Cts -> [Ct] -> Cts
`extendCtsList` [Ct]
insts_out)

    ([Ct]
tv_eqs_out, InertEqs
tv_eqs_in) = (Ct -> Bool) -> InertEqs -> ([Ct], InertEqs)
partitionInertEqs Ct -> Bool
kick_out_eq InertEqs
tv_eqs
    ([Ct]
feqs_out,   FunEqMap [Ct]
feqs_in)   = (Ct -> Bool) -> FunEqMap [Ct] -> ([Ct], FunEqMap [Ct])
partitionFunEqs   Ct -> Bool
kick_out_eq FunEqMap [Ct]
funeqmap
    (Cts
dicts_out,  DictMap Ct
dicts_in)  = (Ct -> Bool) -> DictMap Ct -> (Cts, DictMap Ct)
partitionDicts    Ct -> Bool
kick_out_ct DictMap Ct
dictmap
    (Cts
irs_out,    Cts
irs_in)    = (Ct -> Bool) -> Cts -> (Cts, Cts)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag      Ct -> Bool
kick_out_ct Cts
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.Canonical
    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
      , EqRel -> TcType -> Bool
fr_can_rewrite_ty EqRel
NomEq (CtEvidence -> TcType
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

    (CtFlavour
_, EqRel
new_role) = CtFlavourRole
new_fr

    fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
    fr_tv_can_rewrite_ty :: TcTyVar -> EqRel -> TcType -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role TcType
ty
      = EqRel -> (EqRel -> TcTyVar -> Bool) -> TcType -> Bool
anyRewritableTyVar EqRel
role EqRel -> TcTyVar -> Bool
can_rewrite TcType
ty
      where
        can_rewrite :: EqRel -> TyVar -> Bool
        can_rewrite :: EqRel -> TcTyVar -> Bool
can_rewrite EqRel
old_role TcTyVar
tv = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&& TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
new_tv

    fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
    fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> TcType -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [TcType]
new_tf_args EqRel
role TcType
ty
      = EqRel -> (EqRel -> TyCon -> [TcType] -> Bool) -> TcType -> Bool
anyRewritableTyFamApp EqRel
role EqRel -> TyCon -> [TcType] -> Bool
can_rewrite TcType
ty
      where
        can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
        can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
can_rewrite EqRel
old_role TyCon
old_tf [TcType]
old_tf_args
          = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&&
            TyCon -> [TcType] -> TyCon -> [TcType] -> Bool
tcEqTyConApps TyCon
new_tf [TcType]
new_tf_args TyCon
old_tf [TcType]
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.

    {-# INLINE fr_can_rewrite_ty #-}   -- perform the check here only once
    fr_can_rewrite_ty :: EqRel -> Type -> Bool
    fr_can_rewrite_ty :: EqRel -> TcType -> Bool
fr_can_rewrite_ty = case CanEqLHS
new_lhs of
      TyVarLHS TcTyVar
new_tv             -> TcTyVar -> EqRel -> TcType -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv
      TyFamLHS TyCon
new_tf [TcType]
new_tf_args -> TyCon -> [TcType] -> EqRel -> TcType -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [TcType]
new_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?

    {-# INLINE kick_out_ct #-}   -- perform case on new_lhs here only once
    kick_out_ct :: Ct -> Bool
    -- Kick it out if the new CEqCan can rewrite the inert one
    -- See Note [kickOutRewritable]
    kick_out_ct :: Ct -> Bool
kick_out_ct = case CanEqLHS
new_lhs of
      TyVarLHS TcTyVar
new_tv -> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_,EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
                                CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
                             Bool -> Bool -> Bool
&& TcTyVar -> EqRel -> TcType -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role (Ct -> TcType
ctPred Ct
ct)
      TyFamLHS TyCon
new_tf [TcType]
new_tf_args
        -> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_, EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
                  CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
               Bool -> Bool -> Bool
&& TyCon -> [TcType] -> EqRel -> TcType -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [TcType]
new_tf_args EqRel
role (Ct -> TcType
ctPred Ct
ct)

    -- Implements criteria K1-K3 in Note [Extending the inert equalities]
    kick_out_eq :: Ct -> Bool
    kick_out_eq :: Ct -> Bool
kick_out_eq (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_rhs :: Ct -> TcType
cc_rhs = TcType
rhs_ty
                        , cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
      | Bool -> Bool
not (CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs)
      = Bool
False  -- (K0) Keep it in the inert set if the new thing can't rewrite it

      -- Below here (fr_may_rewrite fs) is True

      | TyVarLHS TcTyVar
_ <- CanEqLHS
lhs
      , CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
new_fr
      = Bool
False  -- (K4) Keep it in the inert set if the LHS is a tyvar and
               -- it can rewrite the work item. See Note [K4]

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

      | Bool
kick_out_for_inertness    = Bool
True   -- (K2)
      | Bool
kick_out_for_completeness = Bool
True   -- (K3)
      | Bool
otherwise                 = Bool
False

      where
        fs :: CtFlavourRole
fs = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
        kick_out_for_inertness :: Bool
kick_out_for_inertness
          =    (CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fs)           -- (K2a)
            Bool -> Bool -> Bool
&& EqRel -> TcType -> Bool
fr_can_rewrite_ty EqRel
eq_rel TcType
rhs_ty    -- (K2b)

        kick_out_for_completeness :: Bool
kick_out_for_completeness  -- (K3) and Note [K3: completeness of solving]
          = case EqRel
eq_rel of
              EqRel
NomEq  -> TcType
rhs_ty TcType -> TcType -> Bool
`eqType` CanEqLHS -> TcType
canEqLHSType CanEqLHS
new_lhs -- (K3a)
              EqRel
ReprEq -> CanEqLHS -> TcType -> Bool
is_can_eq_lhs_head CanEqLHS
new_lhs TcType
rhs_ty    -- (K3b)

    kick_out_eq Ct
ct = String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"kick_out_eq" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

    is_can_eq_lhs_head :: CanEqLHS -> TcType -> Bool
is_can_eq_lhs_head (TyVarLHS TcTyVar
tv) = TcType -> Bool
go
      where
        go :: TcType -> Bool
go (Rep.TyVarTy TcTyVar
tv')   = TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv'
        go (Rep.AppTy TcType
fun TcType
_)   = TcType -> Bool
go TcType
fun
        go (Rep.CastTy TcType
ty KindCoercion
_)   = TcType -> Bool
go TcType
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
    is_can_eq_lhs_head (TyFamLHS TyCon
fun_tc [TcType]
fun_args) = TcType -> Bool
go
      where
        go :: TcType -> Bool
go (Rep.TyVarTy {})       = Bool
False
        go (Rep.AppTy {})         = Bool
False  -- no TyConApp to the left of an AppTy
        go (Rep.CastTy TcType
ty KindCoercion
_)      = TcType -> Bool
go TcType
ty
        go (Rep.TyConApp TyCon
tc [TcType]
args) = TyCon -> [TcType] -> TyCon -> [TcType] -> Bool
tcEqTyConApps TyCon
fun_tc [TcType]
fun_args TyCon
tc [TcType]
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.Canonical.
   See Note [Make sure that insolubles are fully rewritten]
   in GHC.Tc.Solver.Canonical.
-}

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

mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl CtEvidence
ev
  = (TcTyVar -> Bool) -> TcType -> Bool
anyFreeVarsOfType (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl) (TcType -> Bool) -> TcType -> Bool
forall a b. (a -> b) -> a -> b
$
    CtEvidence -> TcType
ctEvPred CtEvidence
ev

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

noGivenIrreds :: InertSet -> Bool
noGivenIrreds :: InertSet -> Bool
noGivenIrreds (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans })
  = Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag (InertCans -> Cts
inert_irreds InertCans
inert_cans)

-- | Returns True iff there are no Given constraints that might,
-- potentially, match the given class consraint. 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.Interact"
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
noMatchableGivenDicts inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans }) CtLoc
loc_w Class
clas [TcType]
tys
  = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Ct -> Bool) -> Cts -> Bool
forall a. (a -> Bool) -> Bag a -> Bool
anyBag Ct -> Bool
matchable_given (Cts -> Bool) -> Cts -> Bool
forall a b. (a -> b) -> a -> b
$
    DictMap Ct -> Class -> Cts
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap Ct
inert_dicts InertCans
inert_cans) Class
clas
  where
    pred_w :: TcType
pred_w = Class -> [TcType] -> TcType
mkClassPred Class
clas [TcType]
tys

    matchable_given :: Ct -> Bool
    matchable_given :: Ct -> Bool
matchable_given Ct
ct
      | CtGiven { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: CtEvidence -> TcType
ctev_pred = TcType
pred_g } <- Ct -> CtEvidence
ctEvidence Ct
ct
      = Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ InertSet -> TcType -> CtLoc -> TcType -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts TcType
pred_g CtLoc
loc_g TcType
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.Interact
mightEqualLater :: InertSet -> TcType -> CtLoc -> TcType -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inert_set TcType
given_pred CtLoc
given_loc TcType
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 -> [TcType] -> [TcType] -> UnifyResult
tcUnifyTysFG BindFun
bind_fun [TcType
flattened_given] [TcType
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  = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [TcType] -> VarSet
tyCoVarsOfTypes [TcType
given_pred, TcType
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.
    ([TcType
flattened_given, TcType
flattened_wanted], TyVarEnv (TyCon, [TcType])
var_mapping)
      = InScopeSet -> [TcType] -> ([TcType], TyVarEnv (TyCon, [TcType]))
flattenTysX InScopeSet
in_scope [TcType
given_pred, TcType
wanted_pred]

    bind_fun :: BindFun
    bind_fun :: BindFun
bind_fun TcTyVar
tv TcType
rhs_ty
      | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
      , TcTyVar -> MetaInfo -> TcType -> Bool
can_unify TcTyVar
tv (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv) TcType
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, [TcType]
fam_args) <- TyVarEnv (TyCon, [TcType]) -> TcTyVar -> Maybe (TyCon, [TcType])
forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv TyVarEnv (TyCon, [TcType])
var_mapping TcTyVar
tv
      , (TcTyVar -> Bool) -> [TcType] -> Bool
anyFreeVarsOfTypes TcTyVar -> Bool
mentions_meta_ty_var [TcType]
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) -> TcType -> Bool
anyFreeVarsOfType TcTyVar -> Bool
mentions_meta_ty_var
                 (TcTyVar -> InertSet -> TcType
lookupCycleBreakerVar TcTyVar
tv InertSet
inert_set)
          MetaInfo
_ -> Bool
True
      | Bool
otherwise
      = Bool
False

    -- like startSolvingByUnification, but allows cbv variables to unify
    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
    can_unify :: TcTyVar -> MetaInfo -> TcType -> Bool
can_unify TcTyVar
_lhs_tv MetaInfo
TyVarTv TcType
rhs_ty  -- see Example 3 from the Note
      | Just TcTyVar
rhs_tv <- TcType -> Maybe TcTyVar
getTyVar_maybe TcType
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 TcType
_rhs_ty = TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
lhs_tv

prohibitedSuperClassSolve :: CtLoc    -- ^ is it loopy to use this one ...
                          -> CtLoc    -- ^ ... to solve this one?
                          -> Bool     -- ^ True ==> don't solve it
-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2)
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
  | GivenSCOrigin SkolemInfoAnon
_ Int
_ 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.Canonical.
   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 -> TcType
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 TcType
tyfam_app <- Bool -> Maybe TcType -> Maybe TcType
forall a. HasCallStack => Bool -> a -> a
assert (TcTyVar -> Bool
isCycleBreakerTyVar TcTyVar
cbv) (Maybe TcType -> Maybe TcType) -> Maybe TcType -> Maybe TcType
forall a b. (a -> b) -> a -> b
$
                      NonEmpty (Maybe TcType) -> Maybe TcType
forall (f :: * -> *) a. Foldable f => f (Maybe a) -> Maybe a
firstJusts (([(TcTyVar, TcType)] -> Maybe TcType)
-> CycleBreakerVarStack -> NonEmpty (Maybe TcType)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (TcTyVar -> [(TcTyVar, TcType)] -> Maybe TcType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TcTyVar
cbv) CycleBreakerVarStack
cbvs_stack)
  = TcType
tyfam_app
  | Bool
otherwise
  = String -> SDoc -> TcType
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 = ([] [(TcTyVar, TcType)] -> CycleBreakerVarStack -> CycleBreakerVarStack
forall a. a -> NonEmpty a -> NonEmpty a
<|)

-- | Add a new cycle-breaker binding to the top environment on the stack.
insertCycleBreakerBinding :: TcTyVar   -- ^ cbv, must be a CycleBreakerTv
                          -> TcType    -- ^ cbv's expansion
                          -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding :: TcTyVar -> TcType -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding TcTyVar
cbv TcType
expansion ([(TcTyVar, TcType)]
top_env :| [[(TcTyVar, TcType)]]
rest_envs)
  = Bool -> CycleBreakerVarStack -> CycleBreakerVarStack
forall a. HasCallStack => Bool -> a -> a
assert (TcTyVar -> Bool
isCycleBreakerTyVar TcTyVar
cbv) (CycleBreakerVarStack -> CycleBreakerVarStack)
-> CycleBreakerVarStack -> CycleBreakerVarStack
forall a b. (a -> b) -> a -> b
$
    ((TcTyVar
cbv, TcType
expansion) (TcTyVar, TcType) -> [(TcTyVar, TcType)] -> [(TcTyVar, TcType)]
forall a. a -> [a] -> [a]
: [(TcTyVar, TcType)]
top_env) [(TcTyVar, TcType)]
-> [[(TcTyVar, TcType)]] -> CycleBreakerVarStack
forall a. a -> [a] -> NonEmpty a
:| [[(TcTyVar, TcType)]]
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 -> TcType -> m ()) -> m ()
forAllCycleBreakerBindings_ ([(TcTyVar, TcType)]
top_env :| [[(TcTyVar, TcType)]]
_rest_envs) TcTyVar -> TcType -> m ()
action
  = [(TcTyVar, TcType)] -> ((TcTyVar, TcType) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(TcTyVar, TcType)]
top_env ((TcTyVar -> TcType -> m ()) -> (TcTyVar, TcType) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TcTyVar -> TcType -> m ()
action)
{-# INLINABLE forAllCycleBreakerBindings_ #-}  -- to allow SPECIALISE later