    module GHC.Tc.Types.CtLoc (

      -- * CtLoc
      CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
      ctLocTypeOrKind_maybe, toInvisibleLoc,
      ctLocDepth, bumpCtLocDepth, isGivenLoc, mkGivenLoc, mkKindEqLoc,
      setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
      pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder,

      -- * CtLocEnv
      CtLocEnv(..),
      getCtLocEnvLoc, setCtLocEnvLoc, setCtLocRealLoc,
      getCtLocEnvLvl, setCtLocEnvLvl,
      ctLocEnvInGeneratedCode,

      -- * SubGoalDepth
      SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
      bumpSubGoalDepth, subGoalDepthExceeded

      ) where

    import GHC.Prelude

    import GHC.Tc.Types.BasicTypes
    import GHC.Tc.Types.ErrCtxt
    import GHC.Tc.Types.Origin

    import GHC.Tc.Utils.TcType

    import GHC.Types.SrcLoc
    import GHC.Types.Name.Reader
    import GHC.Types.Basic( IntWithInf, mkIntWithInf, TypeOrKind(..) )

    import GHC.Core.TyCon( TyConBinder, isVisibleTyConBinder, isNamedTyConBinder )

    import GHC.Utils.Outputable

    {- *********************************************************************
    *                                                                      *
                SubGoalDepth
    *                                                                      *
    ********************************************************************* -}

    {- Note [SubGoalDepth]
    ~~~~~~~~~~~~~~~~~~~~~~
    The 'SubGoalDepth' takes care of stopping the constraint solver from looping.

    The counter starts at zero and increases. It includes dictionary constraints,
    equality simplification, and type family reduction. (Why combine these? Because
    it's actually quite easy to mistake one for another, in sufficiently involved
    scenarios, like ConstraintKinds.)

    The flag -freduction-depth=n fixes the maximum level.

    * The counter includes the depth of type class instance declarations.  Example:
         [W] d{7} : Eq [Int]
      That is d's dictionary-constraint depth is 7.  If we use the instance
         $dfEqList :: Eq a => Eq [a]
      to simplify it, we get
         d{7} = $dfEqList d'{8}
      where d'{8} : Eq Int, and d' has depth 8.

      For civilised (decidable) instance declarations, each increase of
      depth removes a type constructor from the type, so the depth never
      gets big; i.e. is bounded by the structural depth of the type.

    * The counter also increments when resolving
    equalities involving type functions. Example:
      Assume we have a wanted at depth 7:
        [W] d{7} : F () ~ a
      If there is a type function equation "F () = Int", this would be rewritten to
        [W] d{8} : Int ~ a
      and remembered as having depth 8.

      Again, without UndecidableInstances, this counter is bounded, but without it
      can resolve things ad infinitum. Hence there is a maximum level.

    * Lastly, every time an equality is rewritten, the counter increases. Again,
      rewriting an equality constraint normally makes progress, but it's possible
      the "progress" is just the reduction of an infinitely-reducing type family.
      Hence we need to track the rewrites.

    When compiling a program requires a greater depth, then GHC recommends turning
    off this check entirely by setting -freduction-depth=0. This is because the
    exact number that works is highly variable, and is likely to change even between
    minor releases. Because this check is solely to prevent infinite compilation
    times, it seems safe to disable it when a user has ascertained that their program
    doesn't loop at the type level.

    -}

    -- | See Note [SubGoalDepth]
    newtype SubGoalDepth = SubGoalDepth Int
      deriving (SubGoalDepth -> SubGoalDepth -> Bool
    (SubGoalDepth -> SubGoalDepth -> Bool)
    -> (SubGoalDepth -> SubGoalDepth -> Bool) -> Eq SubGoalDepth
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SubGoalDepth -> SubGoalDepth -> Bool
    == :: SubGoalDepth -> SubGoalDepth -> Bool
    $c/= :: SubGoalDepth -> SubGoalDepth -> Bool
    /= :: SubGoalDepth -> SubGoalDepth -> Bool
    Eq, Eq SubGoalDepth
    Eq SubGoalDepth =>
    (SubGoalDepth -> SubGoalDepth -> Ordering)
    -> (SubGoalDepth -> SubGoalDepth -> Bool)
    -> (SubGoalDepth -> SubGoalDepth -> Bool)
    -> (SubGoalDepth -> SubGoalDepth -> Bool)
    -> (SubGoalDepth -> SubGoalDepth -> Bool)
    -> (SubGoalDepth -> SubGoalDepth -> SubGoalDepth)
    -> (SubGoalDepth -> SubGoalDepth -> SubGoalDepth)
    -> Ord SubGoalDepth
    SubGoalDepth -> SubGoalDepth -> Bool
    SubGoalDepth -> SubGoalDepth -> Ordering
    SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SubGoalDepth -> SubGoalDepth -> Ordering
    compare :: SubGoalDepth -> SubGoalDepth -> Ordering
    $c< :: SubGoalDepth -> SubGoalDepth -> Bool
    < :: SubGoalDepth -> SubGoalDepth -> Bool
    $c<= :: SubGoalDepth -> SubGoalDepth -> Bool
    <= :: SubGoalDepth -> SubGoalDepth -> Bool
    $c> :: SubGoalDepth -> SubGoalDepth -> Bool
    > :: SubGoalDepth -> SubGoalDepth -> Bool
    $c>= :: SubGoalDepth -> SubGoalDepth -> Bool
    >= :: SubGoalDepth -> SubGoalDepth -> Bool
    $cmax :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    max :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    $cmin :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    min :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    Ord, SubGoalDepth -> SDoc
    (SubGoalDepth -> SDoc) -> Outputable SubGoalDepth
    forall a. (a -> SDoc) -> Outputable a
    $cppr :: SubGoalDepth -> SDoc
    ppr :: SubGoalDepth -> SDoc
    Outputable)

    initialSubGoalDepth :: SubGoalDepth
    initialSubGoalDepth :: SubGoalDepth
    initialSubGoalDepth = Int -> SubGoalDepth
    SubGoalDepth Int
    0

    bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
    bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
    bumpSubGoalDepth (SubGoalDepth Int
    n) = Int -> SubGoalDepth
    SubGoalDepth (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)

    maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
    maxSubGoalDepth (SubGoalDepth Int
    n) (SubGoalDepth Int
    m) = Int -> SubGoalDepth
    SubGoalDepth (Int
    n Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` Int
    m)

    subGoalDepthExceeded :: IntWithInf -> SubGoalDepth -> Bool
    subGoalDepthExceeded :: IntWithInf -> SubGoalDepth -> Bool
    subGoalDepthExceeded IntWithInf
    reductionDepth (SubGoalDepth Int
    d)
      = Int -> IntWithInf
    mkIntWithInf Int
    d IntWithInf -> IntWithInf -> Bool
    forall a. Ord a => a -> a -> Bool
    > IntWithInf
    reductionDepth

    {- *********************************************************************
    *                                                                      *
                CtLoc
    *                                                                      *
    ************************************************************************

    The 'CtLoc' gives information about where a constraint came from.
    This is important for decent error message reporting because
    dictionaries don't appear in the original source code.

    -}

    data CtLoc = CtLoc { CtLoc -> CtOrigin
    ctl_origin   :: CtOrigin
                       , CtLoc -> CtLocEnv
    ctl_env      :: CtLocEnv -- Everything we need to know about
                                                  -- the context this Ct arose in.
                       , CtLoc -> Maybe TypeOrKind
    ctl_t_or_k   :: Maybe TypeOrKind  -- OK if we're not sure
                       , CtLoc -> SubGoalDepth
    ctl_depth    :: !SubGoalDepth }

    mkKindEqLoc :: TcType -> TcType   -- original *types* being compared
                -> CtLoc -> CtLoc
    mkKindEqLoc :: TcType -> TcType -> CtLoc -> CtLoc
    mkKindEqLoc TcType
    s1 TcType
    s2 CtLoc
    ctloc
      | CtLoc { ctl_t_or_k :: CtLoc -> Maybe TypeOrKind
    ctl_t_or_k = Maybe TypeOrKind
    t_or_k, ctl_origin :: CtLoc -> CtOrigin
    ctl_origin = CtOrigin
    origin } <- CtLoc
    ctloc
      = CtLoc
    ctloc { ctl_origin = KindEqOrigin s1 s2 origin t_or_k
              , ctl_t_or_k = Just KindLevel }

    adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc
    -- Adjust the CtLoc when decomposing a type constructor
    adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc
    adjustCtLocTyConBinder TyConBinder
    tc_bndr CtLoc
    loc
      = Bool -> Bool -> CtLoc -> CtLoc
    adjustCtLoc Bool
    is_vis Bool
    is_kind CtLoc
    loc
      where
        is_vis :: Bool
    is_vis  = TyConBinder -> Bool
    forall tv. VarBndr tv TyConBndrVis -> Bool
    isVisibleTyConBinder TyConBinder
    tc_bndr
        is_kind :: Bool
    is_kind = TyConBinder -> Bool
    isNamedTyConBinder TyConBinder
    tc_bndr

    adjustCtLoc :: Bool    -- True <=> A visible argument
                -> Bool    -- True <=> A kind argument
                -> CtLoc -> CtLoc
    -- Adjust the CtLoc when decomposing a type constructor, application, etc
    adjustCtLoc :: Bool -> Bool -> CtLoc -> CtLoc
    adjustCtLoc Bool
    is_vis Bool
    is_kind CtLoc
    loc
      = CtLoc
    loc2
      where
        loc1 :: CtLoc
    loc1 | Bool
    is_kind   = CtLoc -> CtLoc
    toKindLoc CtLoc
    loc
             | Bool
    otherwise = CtLoc
    loc
        loc2 :: CtLoc
    loc2 | Bool
    is_vis    = CtLoc
    loc1
             | Bool
    otherwise = CtLoc -> CtLoc
    toInvisibleLoc CtLoc
    loc1

    -- | Take a CtLoc and moves it to the kind level
    toKindLoc :: CtLoc -> CtLoc
    toKindLoc :: CtLoc -> CtLoc
    toKindLoc CtLoc
    loc = CtLoc
    loc { ctl_t_or_k = Just KindLevel }

    toInvisibleLoc :: CtLoc -> CtLoc
    toInvisibleLoc :: CtLoc -> CtLoc
    toInvisibleLoc CtLoc
    loc = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
    updateCtLocOrigin CtLoc
    loc CtOrigin -> CtOrigin
    toInvisibleOrigin

    mkGivenLoc :: TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
    mkGivenLoc :: TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
    mkGivenLoc TcLevel
    tclvl SkolemInfoAnon
    skol_info CtLocEnv
    env
      = CtLoc { ctl_origin :: CtOrigin
    ctl_origin   = SkolemInfoAnon -> CtOrigin
    GivenOrigin SkolemInfoAnon
    skol_info
              , ctl_env :: CtLocEnv
    ctl_env      = CtLocEnv -> TcLevel -> CtLocEnv
    setCtLocEnvLvl CtLocEnv
    env TcLevel
    tclvl
              , ctl_t_or_k :: Maybe TypeOrKind
    ctl_t_or_k   = Maybe TypeOrKind
    forall a. Maybe a
    Nothing    -- this only matters for error msgs
              , ctl_depth :: SubGoalDepth
    ctl_depth    = SubGoalDepth
    initialSubGoalDepth }

    ctLocEnv :: CtLoc -> CtLocEnv
    ctLocEnv :: CtLoc -> CtLocEnv
    ctLocEnv = CtLoc -> CtLocEnv
    ctl_env

    ctLocLevel :: CtLoc -> TcLevel
    ctLocLevel :: CtLoc -> TcLevel
    ctLocLevel CtLoc
    loc = CtLocEnv -> TcLevel
    getCtLocEnvLvl (CtLoc -> CtLocEnv
    ctLocEnv CtLoc
    loc)

    ctLocDepth :: CtLoc -> SubGoalDepth
    ctLocDepth :: CtLoc -> SubGoalDepth
    ctLocDepth = CtLoc -> SubGoalDepth
    ctl_depth

    ctLocOrigin :: CtLoc -> CtOrigin
    ctLocOrigin :: CtLoc -> CtOrigin
    ctLocOrigin = CtLoc -> CtOrigin
    ctl_origin

    ctLocSpan :: CtLoc -> RealSrcSpan
    ctLocSpan :: CtLoc -> RealSrcSpan
    ctLocSpan (CtLoc { ctl_env :: CtLoc -> CtLocEnv
    ctl_env = CtLocEnv
    lcl}) = CtLocEnv -> RealSrcSpan
    getCtLocEnvLoc CtLocEnv
    lcl

    ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
    ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
    ctLocTypeOrKind_maybe = CtLoc -> Maybe TypeOrKind
    ctl_t_or_k

    setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
    setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
    setCtLocSpan ctl :: CtLoc
    ctl@(CtLoc { ctl_env :: CtLoc -> CtLocEnv
    ctl_env = CtLocEnv
    lcl }) RealSrcSpan
    loc = CtLoc -> CtLocEnv -> CtLoc
    setCtLocEnv CtLoc
    ctl (CtLocEnv -> RealSrcSpan -> CtLocEnv
    setCtLocRealLoc CtLocEnv
    lcl RealSrcSpan
    loc)

    bumpCtLocDepth :: CtLoc -> CtLoc
    bumpCtLocDepth :: CtLoc -> CtLoc
    bumpCtLocDepth loc :: CtLoc
    loc@(CtLoc { ctl_depth :: CtLoc -> SubGoalDepth
    ctl_depth = SubGoalDepth
    d }) = CtLoc
    loc { ctl_depth = bumpSubGoalDepth d }

    setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
    setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
    setCtLocOrigin CtLoc
    ctl CtOrigin
    orig = CtLoc
    ctl { ctl_origin = orig }

    updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
    updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
    updateCtLocOrigin ctl :: CtLoc
    ctl@(CtLoc { ctl_origin :: CtLoc -> CtOrigin
    ctl_origin = CtOrigin
    orig }) CtOrigin -> CtOrigin
    upd
      = CtLoc
    ctl { ctl_origin = upd orig }

    setCtLocEnv :: CtLoc -> CtLocEnv -> CtLoc
    setCtLocEnv :: CtLoc -> CtLocEnv -> CtLoc
    setCtLocEnv CtLoc
    ctl CtLocEnv
    env = CtLoc
    ctl { ctl_env = env }

    isGivenLoc :: CtLoc -> Bool
    isGivenLoc :: CtLoc -> Bool
    isGivenLoc CtLoc
    loc = CtOrigin -> Bool
    isGivenOrigin (CtLoc -> CtOrigin
    ctLocOrigin CtLoc
    loc)

    pprCtLoc :: CtLoc -> SDoc
    -- "arising from ... at ..."
    -- Not an instance of Outputable because of the "arising from" prefix
    pprCtLoc :: CtLoc -> SDoc
    pprCtLoc (CtLoc { ctl_origin :: CtLoc -> CtOrigin
    ctl_origin = CtOrigin
    o, ctl_env :: CtLoc -> CtLocEnv
    ctl_env = CtLocEnv
    lcl})
      = [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [ CtOrigin -> SDoc
    pprCtOrigin CtOrigin
    o
            , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "at" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> RealSrcSpan -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (CtLocEnv -> RealSrcSpan
    getCtLocEnvLoc CtLocEnv
    lcl)]

    {- *********************************************************************
    *                                                                      *
                CtLocEnv
    *                                                                      *
    ********************************************************************* -}

    -- | Local typechecker environment for a constraint.
    --
    -- Used to restore the environment of a constraint
    -- when reporting errors, see `setCtLocM`.
    --
    -- See also 'TcLclCtxt'.
    data CtLocEnv = CtLocEnv { CtLocEnv -> [ErrCtxt]
    ctl_ctxt :: ![ErrCtxt]
                             , CtLocEnv -> RealSrcSpan
    ctl_loc :: !RealSrcSpan
                             , CtLocEnv -> TcBinderStack
    ctl_bndrs :: !TcBinderStack
                             , CtLocEnv -> TcLevel
    ctl_tclvl :: !TcLevel
                             , CtLocEnv -> Bool
    ctl_in_gen_code :: !Bool
                             , CtLocEnv -> LocalRdrEnv
    ctl_rdr :: !LocalRdrEnv }

    getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan
    getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan
    getCtLocEnvLoc = CtLocEnv -> RealSrcSpan
    ctl_loc

    getCtLocEnvLvl :: CtLocEnv -> TcLevel
    getCtLocEnvLvl :: CtLocEnv -> TcLevel
    getCtLocEnvLvl = CtLocEnv -> TcLevel
    ctl_tclvl

    setCtLocEnvLvl :: CtLocEnv -> TcLevel -> CtLocEnv
    setCtLocEnvLvl :: CtLocEnv -> TcLevel -> CtLocEnv
    setCtLocEnvLvl CtLocEnv
    env TcLevel
    lvl = CtLocEnv
    env { ctl_tclvl = lvl }

    setCtLocRealLoc :: CtLocEnv -> RealSrcSpan -> CtLocEnv
    setCtLocRealLoc :: CtLocEnv -> RealSrcSpan -> CtLocEnv
    setCtLocRealLoc CtLocEnv
    env RealSrcSpan
    ss = CtLocEnv
    env { ctl_loc = ss }

    setCtLocEnvLoc :: CtLocEnv -> SrcSpan -> CtLocEnv
    -- See Note [Error contexts in generated code]
    -- for the ctl_in_gen_code manipulation
    setCtLocEnvLoc :: CtLocEnv -> SrcSpan -> CtLocEnv
    setCtLocEnvLoc CtLocEnv
    env (RealSrcSpan RealSrcSpan
    loc Maybe BufSpan
    _)
      = CtLocEnv
    env { ctl_loc = loc, ctl_in_gen_code = False }

    setCtLocEnvLoc CtLocEnv
    env loc :: SrcSpan
    loc@(UnhelpfulSpan UnhelpfulSpanReason
    _)
      | SrcSpan -> Bool
    isGeneratedSrcSpan SrcSpan
    loc
      = CtLocEnv
    env { ctl_in_gen_code = True }
      | Bool
    otherwise
      = CtLocEnv
    env

    ctLocEnvInGeneratedCode :: CtLocEnv -> Bool
    ctLocEnvInGeneratedCode :: CtLocEnv -> Bool
    ctLocEnvInGeneratedCode = CtLocEnv -> Bool
    ctl_in_gen_code