-{-

-specRhs :: SpecEnv -> [InVar] -> InExpr -> [OutExpr]

-        -> SpecM (OutExpr, UsageDetails)

-

-specRhs env bndrs body []  -- Like specExpr (Lam bndrs body)

-  = specLam env' bndrs' body

-  where

-    (env', bndrs') = substBndrs env bndrs

-

-specRhs _env [] body args

-  = -- The caller should have ensured that there are no more

-    -- args than we have binders on the RHS

-    pprPanic "specRhs:too many args" (ppr args $$ ppr body)

-

-specRhs env@(SE { se_subst = subst }) (bndr:bndrs) body (arg:args)

-  | exprIsTrivial arg

-  , let env' = env { se_subst = Core.extendSubst subst bndr arg }

-  = specRhs env' bndrs body args

-

-

-  | otherwise  -- Non-trivial argument; it must be a dictionary

-  = do { fresh_id <- newIdBndr "dx" (exprType arg)

-       ; let fresh_id' = fresh_id `addDictUnfolding` arg

-             dict_bind = mkDB (NonRec fresh_id' arg)

-             env' = env { se_subst = Core.extendSubst subst bndr (Var fresh_id')

-                                      `Core.extendSubstInScope` fresh_id' }

-                                      -- Ensure the new unfolding is in the in-scope set

-       ; (body', uds) <- specRhs env' bndrs body args

-       ; return (body', dict_bind `consDictBind` uds) }

-

-consDictBind :: DictBind -> UsageDetails -> UsageDetails

-consDictBind db uds@MkUD{ud_binds=FDB{fdb_binds = binds, fdb_bndrs = bs}}

-  = uds { ud_binds = FDB{ fdb_binds = db `consOL` binds

-                        , fdb_bndrs = bs `extendVarSetList` bindersOfDictBind db } }

-

--}

-

-  , let (subst1, bndr') = Core.substBndr subst bndr

-solveForAll ev tvs theta body_pred fuel =

-  case ev of

-    CtGiven {} ->

-      -- See Note [Solving a Given forall-constraint]

-      do { addInertForAll qci

-         ; stopWith ev "Given forall-constraint" }

-    CtWanted wtd ->

-      -- See Note [Solving a Wanted forall-constraint]

-      runSolverStage $

-      do { tryInertQCs qci

-         ; Stage $ solveWantedForAll wtd tvs theta body_pred }

---

-solveWantedForAll :: WantedCtEvidence -> [TcTyVar] -> TcThetaType -> PredType

-                         -> TcS (StopOrContinue Void)

-solveWantedForAll wtd@(WantedCt { ctev_dest = dest, ctev_loc = loc

-                                , ctev_rewriters = rewriters })

-  = -- We are about to do something irreversible (turning a quantified constraint

-    -- into an implication), so wrap the inner call in solveCompletelyIfRequired

-    -- to ensure we can roll back if we can't solve the implication fully.

-    -- See Note [TcSSpecPrag] in GHC.Tc.Solver.Monad.

-    do { mode <- getTcSMode

-       ; case mode of

-           TcSSpecPrag

-             -> do { traceTcS "solveWantedForAll {" (ppr wtd)

-                   ; fully_solved <- tryTcS (setTcSMode TcSVanilla $

-                                             solveSimpleWanteds (unitBag ct))

-                   ; if fully_solved

-                     then do { traceTcS "solveWantedForAll: fully solved }" (ppr wtd)

-                             ; return $ Stop ev (text "Fully solved:" <+> ppr wtd) }

-                     else do { traceTcS "solveWantedForAll: fully solved }" (ppr wtd)

-                             ; updInertIrreds (IrredCt ev IrredShapeReason)

-                                 -- Stash the unsolved quantified constraint in the irreds

-                             ; return $ Stop ev (text "Not fully solved:" <+> ppr wtd) } }

-

-           _ -> do { solve_by_emitting_implic

-                   ; stopWith ev "Wanted forall-constraint (implication)" } }

-    ev    = CtWanted wtd

-    ct    = mkNonCanonical ev

-    -- This setSrcSpan is important: the emitImplicationTcS uses that

-    -- TcLclEnv for the implication, and that in turn sets the location

-    -- for the Givens when solving the constraint (#21006)

-    solve_by_emitting_implic

-       = TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $

-         do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]

-              --           in GHC.Tc.Utils.TcType

-              -- Very like the code in tcSkolDFunType

-              rec { skol_info <- mkSkolemInfo skol_info_anon

-            ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs

-            ; let inst_pred  = substTy    subst body_pred

-                  inst_theta = substTheta subst theta

-                  skol_info_anon = InstSkol is_qc (get_size inst_pred) }

-

-             ; given_ev_vars <- mapM newEvVar inst_theta

-             ; (lvl, (w_id, wanteds))

-                   <- pushLevelNoWorkList (ppr skol_info) $

-                      do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc)

-                               -- Set the thing to prove to have a ScOrigin, so we are

-                               -- careful about its termination checks.

-                               -- See (QC-INV) in Note [Solving a Wanted forall-constraint]

-                         ; wanted_ev <- newWantedNC loc' rewriters inst_pred

-                               -- NB: inst_pred can be an equality

-                         ; return ( wantedCtEvEvId wanted_ev

-                                  , unitBag (mkNonCanonical $ CtWanted wanted_ev)) }

-

-            ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id)

-            ; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds

-

-            ; setWantedEvTerm dest EvCanonical $

-              EvFun { et_tvs = skol_tvs, et_given = given_ev_vars

-                    , et_binds = ev_binds, et_body = w_id }

-            }

-

-  do { (new_val_bind, new_exports) <- mfix $ \ ~(new_val_binds, _) ->

-       runZonkBndrT (extendIdZonkEnvRec $ collectHsBindsBinders CollNoDictBinders new_val_binds) $ \ _ ->