--

 -- It's better to read it as: "if we know these, then we're going to know these"

 module GHC.Tc.Instance.FunDeps

    , pprEquation

    , improveFromInstEnv

    , improveFromAnother

 for generating a single equality. For instance:

      class C a b | a -> b

 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha

 However notice that a functional dependency may have more than one variable

 in the RHS which will create more than one pair of types in fd_eqs. Example:

      class C a b c | a -> b c

      [Wanted] C Int alpha alpha

      [Wanted] C Int Bool beta

 Will generate:

 INVARIANT: Corresponding types aren't already equal

 That is, there exists at least one non-identity equality in FDEqs.

    instance C Int Bool

    [W] C Int ty

 describing an equality (Bool ~ ty).  To do this we /match/ the instance head

 against the [W], using just the LHS of the fundep; if we match, we return

     Note that although the `Int` parts match, that does not fix what `x` is.

     So we just make up a fresh unification variable (a meta_tv), to give the

     Note that the fd_qtvs can be free in the /first/ component of the Pair,

     but not in the second (which comes from the [W] constraint).

        instance D Int x (Maybe x)

        [W] D Int Bool ty

        FDEqn { fd_qtvs = [x0], fd_eqs = [ x0 ~ Bool, Maybe x0 ~ ty] }

     which generates one fresh unification variable x0

     with two FDEqns, generating two separate unification variables.

 (IMP3) improveFromInstEnv doesn't return any equations that already hold.

     Reason: just an optimisation; the caller does the same thing, but

     with a bit more ceremony.

 -}

                                  --   to fresh unification vars,

                                  -- See (IMP2) in Note [Improving against instances]

                                    -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be

                                    -- free in ty1 but not in ty2.  See Wrinkle (1) of

                                    -- Note [Improving against instances]

   ppr = pprEquation

   = vcat [text "forall" <+> braces (pprWithCommas ppr qtvs),

           nest 2 (vcat [ ppr t1 <+> text "~" <+> ppr t2

                        | Pair t1 t2 <- pairs])]

 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 improveFromAnother :: PredType -- Template item (usually given, or inert)

                    -> PredType -- Workitem [that can be improved]

 -- Post: FDEqs always oriented from the other to the workitem

 --       Equations have empty quantified variables

 improveFromAnother pred1 pred2

   | Just (cls1, tys1) <- getClassPredTys_maybe pred1

   , Just (cls2, tys2) <- getClassPredTys_maybe pred2

   , cls1 == cls2

     | let (cls_tvs, cls_fds) = classTvsFds cls1

     , fd <- cls_fds

     , let (ltys1, rs1) = instFD fd cls_tvs tys1

 improveFromInstEnv :: InstEnvs

                    -> Class -> [Type]

 -- See Note [Improving against instances]

 -- Post: Equations oriented from the template (matching instance) to the workitem!

 improveFromInstEnv inst_env cls tys

     | fd <- cls_fds             -- Iterate through the fundeps first,

                                 -- because there often are none!

     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs

 Here is our plan for dealing with functional dependencies

 * When we have failed to solve a Wanted constraint, do this

   3. If any unifications happened, send the constraint back to the

      start of the pipeline

        - tryDictFunDeps: for class constraints (C t1 .. tn)

          we look at top-level instances and inert Givens

        - tryEqFunDeps: for type-family equalities (F t1 .. tn ~ ty)

          we look at top-level family instances

                     and inert Given family equalities

   solver.  Key property:

       The ONLY effect of `solveFunDeps` is possibly to perform unifications:

 (some unification has happened), and hence go round again; but actually all we

 have done is to replace `alpha` with `gamma1`.

 For example

       class C a b | a -> b

       instance .. => C Int [x]

 If we see

       [W] C Int alpha

 we'll generate a fundep-equality   [W] alpha ~ [beta1]

 This problem shows up in several guises; see (at the bottom)

   * Historical Note [Improvement orientation]

 The solution is super-simple:

     lists the "fresh variables"

     gives the new unification variables a level one deeper than the current

     level.

     Note [Deeper level on the left].  That ensures that the fresh `gamma1`

     will be eliminated in favour of `alpha`. Hooray.

     It uses `reportUnifications` to see if any unification happened at this

     level or outside -- that is, it does NOT report unifications to the fresh

     unification variables.  So `solveFunDeps` returns True only if it

        ; traceTcS "tryDictFunDepsLocal {" (ppr dict_ct)

              eqns = foldr ((++) . do_interaction) [] $

                     findDictsByClass (inert_dicts inerts) cls

        ; imp <- solveFunDeps work_ev eqns

     work_pred     = ctEvPred work_ev

     work_is_given = isGiven work_ev

     do_interaction (DictCt { di_ev = inert_ev }) -- This can be Given or Wanted

       | work_is_given && isGiven inert_ev

         -- Do not create FDs from Given/Given interactions

     do { inst_envs <- getInstEnvs

        ; traceTcS "tryDictFunDepsTop {" (ppr dict_ct)

              eqns = improveFromInstEnv inst_envs cls xis

        ; imp <- solveFunDeps ev eqns

        ; traceTcS "tryDictFunDepsTop }" (text "imp =" <+> ppr imp)

   | otherwise

   = nopStage ()

 tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eqns

   = Stage $

     do { fd_eqns <- mk_fd_eqns

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

 --  User-defined type families

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

 -- Implements (INJFAM:Wanted/top)

 mkTopUserFamEqFDs fam_tc inj_flags work_args work_rhs

   = do { fam_envs <- getFamInstEnvs

       | otherwise

       = []

     do_one branch@(CoAxBranch { cab_tvs = branch_tvs

                               , cab_lhs = branch_lhs_tys

                               , cab_rhs = branch_rhs })

                                    !(subst', tvs') = trim_qtvs subst1 tvs

                                in (subst', tv':tvs')

 mkLocalUserFamEqFDs fam_tc inj_flags work_args work_rhs

   = do { fun_eqs_for_me <- getInertFamEqsFor fam_tc

        ; return (eqns_from_inerts ++ eqns_from_self) }

   where

     do_one (EqCt { eq_lhs = TyFamLHS _ inert_args, eq_rhs = inert_rhs })

       | work_rhs `tcEqType` inert_rhs = Just (mk_eqn inert_args)

       | otherwise                     = Nothing

     do_one _ = return ()

 mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs

 mkLocalBuiltinFamEqFDs fam_tc ops work_args work_rhs

   = do { fun_eqs_for_me <- getInertFamEqsFor fam_tc

              do_one (EqCt { eq_lhs = TyFamLHS _ inert_args, eq_rhs = inert_rhs })

                | inert_rhs `tcEqType` work_rhs = [mk_eqn inert_args]

                | otherwise                     = []

              do_one _ = pprPanic "interactFunEq 1" (ppr fam_tc) -- TyVarLHS

                                                                      work_args iargs }

        ; let eqns_from_inerts = concatMap do_one fun_eqs_for_me

 mkInjectivityFDEqn :: [Bool]       -- Injectivity flags

                    -> [TcTyVar]    -- Quantify these

                    -> [TcType] -> [TcType]  -- Make these equal

 -- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True]

 -- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are

 mkInjectivityFDEqn inj_args qtvs lhs_args rhs_args

   where

     eqs = [ Pair lhs_arg rhs_arg

           | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]

 * (INJFAM:Wanted/Self) see `mkLocalUserFamEqFDs`

     work item: [W] F s1 s2 ~ F t1 t2

 * (INJFAM:Wanted/other) see `mkLocalUserFamEqFDs`

     work item: [W]   F s1 s2 ~ rhs   -- Wanted

     inert:     [G/W] F t2 t2 ~ rhs   -- Same `rhs`, Given or Wanted

 * (INJFAM:Wanted/top) see `mkTopUserFamEqFDs`

     work item: [W] F s1 s2 ~ rhs

     type instance forall a b c. F t1 t2 ~ top_rhs

   and we can /match/ the LHS, so that

      S(top_rhs) = rhs

   But see wrinkle (TIF1), (TIF2)

 For /built-in/ type families, it's pretty similar, except that

      [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa))

   we match (Proxy @kappa delta) against the template (Proxy k a), succeeding

     FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] }

   Notice that

       we will generate a fresh unfication variable in `instantiateFunDepEqn`.

     * we must substitute `k:->kappa` in the kind of `b`.

   This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in

 ********************************************************************* -}

 solveFunDeps :: CtEvidence  -- The work item

              -> TcS Bool

 -- Solve a bunch of type-equality equations, generated by functional dependencies

 -- By "solve" we mean: (only) do unifications.  We do not generate evidence, and

     do_fundeps :: UnifyEnv -> TcM ()

     do_fundeps env = mapM_ (do_one env) fd_eqns

     do_one uenv eqn = do { eqs <- instantiateFunDepEqn eqn

                          ; uPairsTcM uenv eqs }

   | null tvs

   = return rev_eqs

   | otherwise

     TcM.pushTcLevelM_  $

          -- pushTcLevelTcM: increase the level so that unification variables

          -- allocated by the fundep-creation itself don't count as useful unifications

     do { inerts <- TcM.readTcRef inerts_var

        ; let nest_inerts = resetInertCans inerts

        ; new_inert_var <- TcM.newTcRef nest_inerts

        ; new_wl_var    <- TcM.newTcRef emptyWorkList

        ; let nest_env = env { tcs_inerts   = new_inert_var