{-# LANGUAGE DeriveDataTypeable #-}

 {-# OPTIONS_HADDOCK not-home #-}

         CoercionN, CoercionR, CoercionP, KindCoercion,

         MCoercion(..), MCoercionR, MCoercionN, KindMCoercion,

         -- * Functions over types

         mkNakedTyConTy, mkTyVarTy, mkTyVarTys,

         mkTyCoVarTy, mkTyCoVarTys,

 -- friends:

 import GHC.Types.Var

 import GHC.Types.Var.Set( elemVarSet )

 import GHC.Core.TyCon

 import GHC.Core.Coercion.Axiom

 -- libraries

 import qualified Data.Data as Data hiding ( TyCon )

 import Data.IORef ( IORef )   -- for CoercionHole

 import Control.DeepSeq

 {- **********************************************************************

 %*                                                                      *

 %*                                                                      *

 %********************************************************************* -}

   = CoercionHole { ch_co_var  :: CoVar

                        -- See Note [CoercionHoles and coercion free variables]

                  }

 coHoleCoVar :: CoercionHole -> CoVar

 instance Uniquable CoercionHole where

   getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv

 {- Note [Coercion holes]

 ~~~~~~~~~~~~~~~~~~~~~~~~

 During typechecking, constraint solving for type classes works by

 Here co2 is a CoercionHole. But we /must/ know that it is free in

 co1, because that's all that stops it floating outside the

 implication.

 -}

              -> do { -- See Note [Deferred errors for coercion holes]

                      let co_var = coHoleCoVar hole

                    ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var EvNonCanonical err_tm

 addDeferredBinding _ _ _ _ _ = return ()    -- Do not set any evidence for Given

 mkSolverErrorTerm :: CtLoc -> Type  -- of the error term

          do { ev_id <- newEvVar pred

             ; fillCoercionHole hole (mkCoVarCo ev_id)

             ; return ev_id }

     hole. Much easier just to side-step the issue entirely by not quantifying over

     equalities.

     go_simple ct = case ctEvidence ct of

       CtWanted (WantedCt { ctev_pred = pty, ctev_dest = dest })

         -> do { ev_expr <- unsatisfiableEvExpr unsat_given pty

       _ -> return ()

 -- | Create an evidence expression for an arbitrary constraint using

        ; co <- wrapUnifierAndEmit ev role $ \uenv ->

                uType uenv t1 t2

          -- Set  d :: (t1~t2) = Eq# co

          evDictApp cls tys [Coercion co]

        ; stopWith ev "Solved wanted lifted equality" }

 -- See Note [Solving forall equalities]

 can_eq_nc_forall ev eq_rel s1 s2

  = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2

             flags1 = binderFlags bndrs1

             flags2 = binderFlags bndrs2

                       , ic_wanted = emptyWC { wc_simple = wanteds } }

       ; if solved

                 ; stopWith ev "Polytype equality: solved" }

         else canEqSoftFailure IrredShapeReason ev s1 s2 } }

 -- to an irreducible constraint; see typecheck/should_compile/T10494

 -- See Note [Decomposing AppTy equalities]

 can_eq_app ev s1 t1 s2 t2

   = do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1

                                      , text "s2:" <+> ppr s2, text "t2:" <+> ppr t2

                                      , text "vis:" <+> ppr (isNextArgVisible s1) ])

                ; co_t <- uType arg_env t1 t2

                ; co_s <- uType uenv s1 s2

                ; return (mkAppCo co_s co_t) }

        ; stopWith ev "Decomposed [W] AppTy" }

     -- If there is a ForAll/(->) mismatch, the use of the Left coercion

     do { traceTcS "canDecomposableTyConAppOK"

                   (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2)

        ; case ev of

              -- new_locs and tc_roles are both infinite, so we are

              -- guaranteed that cos has the same length as tys1 and tys2

              -- See Note [Fast path when decomposing TyConApps]

                         do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2

                                     -- zipWith4M: see Note [Work-list ordering]

                            ; return (mkTyConAppCo role tc cos) }

            CtGiven (GivenCt { ctev_evar = evar })

              | let pred_ty = mkEqPred eq_rel ty1 ty2

   = do { traceTcS "canDecomposableFunTy"

                   (ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2)

        ; case ev of

              -> do { co <- wrapUnifierAndEmit ev Nominal $ \ uenv ->

                         do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc InvisibleMultiplicity

                                                  `setUEnvRole` funRole role SelMult

                            ; arg  <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2

                            ; res  <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2

                            ; return (mkNakedFunCo role af mult arg res) }

            CtGiven (GivenCt { ctev_evar = evar })

              | let pred_ty = mkEqPred eq_rel ty1 ty2

        ; (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRewriteRole old_ev) nlhs nrhs

        ; let co = maybeSymCo swapped $

                   lhs_co `mkTransCo` hole_co `mkTransCo` mkSymCo rhs_co

        ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev

                                             , ppr nlhs

                                             , ppr nrhs

     newWantedNC, newWantedEvVarNC,

     newBoundEvVarId,

     unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications,

     setWantedEvTerm, setEvBindIfWanted,

     newEvVar, newGivenEv, emitNewGivens,

     emitChildEqs, checkReductionDepth,

        ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked)

        ; return n_kicked }

 -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty]

 -- in GHC.Tc.Solver.Equality

 --

 -- It's possible that this could just go ahead and unify, but could there

 -- be occurs-check problems? Seems simpler just to kick out.

   = do { ics <- getInertCans

              n_kicked           = length kicked_out

        ; unless (n_kicked == 0) $

        ; setInertCans ics' }

   where

       = (eqs_to_kick, ics { inert_eqs = eqs_to_keep })

       where

       | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev

       , TyVarLHS tv <- lhs

       , isMetaTyVar tv

   = do { ev_binds_var <- getTcEvBindsVar

        ; wrapTcS (TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)) }

   = do { addUsedCoercion co

   | Just co <- evTermCoercion_maybe tm

   = do { addUsedCoercion co

   | otherwise

   = -- See Note [Yukky eq_sel for a HoleDest]

     do { let co_var = coHoleCoVar hole

        ; setEvBind (mkWantedEvBind co_var EvCanonical tm)

 {- Note [Yukky eq_sel for a HoleDest]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 Yuk!

 -}

 setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()

 setEvBindIfWanted ev canonical tm

   = case ev of

 newTcEvBinds :: TcS EvBindsVar

 newTcEvBinds = wrapTcS TcM.newTcEvBinds

               -- NB: even if it is fully solved we must return it, because it is

               --     carrying a record of which evidence variables are used

               --     See Note [Free vars of EvFun] in GHC.Tc.Types.Evidence

                   EvFun { et_tvs = skol_tvs, et_given = given_ev_vars

                         , et_binds = TcEvBinds ev_binds_var

                         , et_body = wantedCtEvEvId wanted_ev }

              ev_rw_role = ctEvRewriteRole ev

        ; mb_new_ev <- newWanted loc rewriters' new_pred

        ; massert (coercionRole co == ev_rw_role)

          evCast (getEvExpr mb_new_ev)     $

          downgradeRole Representational ev_rw_role (mkSymCo co)

        ; case mb_new_ev of

   where

     setEv :: (EvTerm,Ct) -> TcS ()

     setEv (ev,ct) = case ctEvidence ct of

            -- TODO: plugins should be able to signal non-canonicity

       _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"

         -- RewriterSet

         --   RewriterSet(..) is exported concretely only for zonkRewriterSet

         RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, elemRewriterSet,

         wrapType,

 import GHC.Builtin.Names

 import GHC.Types.Var.Set

 import GHC.Types.Name.Reader

 import GHC.Utils.FV

 import GHC.Data.Bag

 import Control.Monad ( when )

 import Data.List  ( intersperse )

 import Data.Maybe ( mapMaybe, isJust )

 import GHC.Data.Maybe ( firstJust, firstJusts )

 setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence

 setWantedCtEvRewriters ev rs = ev { ctev_rewriters = rs }

 ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr

 ctEvExpr (CtWanted ev@(WantedCt { ctev_dest = HoleDest _ }))

             = Coercion $ ctEvCoercion (CtWanted ev)

 isGiven (CtGiven {})  = True

 isGiven _ = False

 {-

 ************************************************************************

 *                                                                      *

        ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }

 -- | Put a value in a coercion hole

 {- **********************************************************************

 *

     go_co dv (HoleCo hole)

       = do m_co <- liftZonkM (unpackCoercionHole_maybe hole)

            case m_co of

     go_co dv (CoVarCo cv) = go_cv dv cv

     -- * Coercion holes

   , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe

     -- * Tidying

   , tcInitTidyEnv, tcInitOpenTidyEnv

         hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })

           = do { contents <- readTcRef ref

                ; case contents of

                    Nothing -> do { cv' <- zonkCoVar cv

                                  ; return $ HoleCo (hole { ch_co_var = cv' }) } }

     go :: CoercionHole -> UnfilledCoercionHoleMonoid -> UnfilledCoercionHoleMonoid

     go hole m_acc = freeHolesOfHole hole `mappend` m_acc

 freeHolesOfHole :: CoercionHole -> UnfilledCoercionHoleMonoid

 freeHolesOfHole hole

   = UCHM $ do { m_co <- unpackCoercionHole_maybe hole

               ; case m_co of

                    Nothing -> return (unitRewriterSet hole)  -- Not filled

 newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet }

 unpackCoercionHole hole

   = do { contents <- unpackCoercionHole_maybe hole

        ; case contents of

            Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }

 -- | Retrieve the contents of a coercion hole, if it is filled

 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref

 zonkCoHole hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })

   = do { contents <- readTcRef ref

        ; case contents of

               -- This next case should happen only in the presence of

               -- (undeferred) type errors. Originally, I put in a panic