content: 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 (Eq, Ord, Outputable)
  
  initialSubGoalDepth :: SubGoalDepth
  initialSubGoalDepth = SubGoalDepth 0
  
  bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
  bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
  
  maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
  maxSubGoalDepth (SubGoalDepth n) (SubGoalDepth m) = SubGoalDepth (n `max` m)
  
  subGoalDepthExceeded :: IntWithInf -> SubGoalDepth -> Bool
  subGoalDepthExceeded reductionDepth (SubGoalDepth d)
    = mkIntWithInf d > 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 { ctl_origin   :: CtOrigin
                     , ctl_env      :: CtLocEnv -- Everything we need to know about
                                                -- the context this Ct arose in.
                     , ctl_t_or_k   :: Maybe TypeOrKind  -- OK if we're not sure
                     , ctl_depth    :: !SubGoalDepth }
  
  mkKindEqLoc :: TcType -> TcType   -- original *types* being compared
              -> CtLoc -> CtLoc
  mkKindEqLoc s1 s2 ctloc
    | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- 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 tc_bndr loc
    = adjustCtLoc mb_invis_kind is_kind loc
    where
      mb_invis_kind =
        if isVisibleTyConBinder tc_bndr
        then Nothing
        else Just InvisibleKind
      is_kind = isNamedTyConBinder tc_bndr
  
  adjustCtLoc :: Maybe InvisibleBit
              -> Bool    -- True <=> A kind argument
              -> CtLoc -> CtLoc
  -- Adjust the CtLoc when decomposing a type constructor, application, etc
  adjustCtLoc mb_invis is_kind loc
    = loc2
    where
      loc1 | is_kind   = toKindLoc loc
           | otherwise = loc
      loc2 =
        case mb_invis of
          Nothing    -> loc1
          Just invis -> toInvisibleLoc invis loc1
  
  -- | Take a CtLoc and moves it to the kind level
  toKindLoc :: CtLoc -> CtLoc
  toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
  
  toInvisibleLoc :: InvisibleBit -> CtLoc -> CtLoc
  toInvisibleLoc invis loc = updateCtLocOrigin loc (toInvisibleOrigin invis)
  
  mkGivenLoc :: TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
  mkGivenLoc tclvl skol_info env
    = CtLoc { ctl_origin   = GivenOrigin skol_info
            , ctl_env      = setCtLocEnvLvl env tclvl
            , ctl_t_or_k   = Nothing    -- this only matters for error msgs
            , ctl_depth    = initialSubGoalDepth }
  
  ctLocEnv :: CtLoc -> CtLocEnv
  ctLocEnv = ctl_env
  
  ctLocLevel :: CtLoc -> TcLevel
  ctLocLevel loc = getCtLocEnvLvl (ctLocEnv loc)
  
  ctLocDepth :: CtLoc -> SubGoalDepth
  ctLocDepth = ctl_depth
  
  ctLocOrigin :: CtLoc -> CtOrigin
  ctLocOrigin = ctl_origin
  
  ctLocSpan :: CtLoc -> RealSrcSpan
  ctLocSpan (CtLoc { ctl_env = lcl}) = getCtLocEnvLoc lcl
  
  ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
  ctLocTypeOrKind_maybe = ctl_t_or_k
  
  setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
  setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (setCtLocRealLoc lcl loc)
  
  bumpCtLocDepth :: CtLoc -> CtLoc
  bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }
  
  setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
  setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
  
  updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
  updateCtLocOrigin ctl@(CtLoc { ctl_origin = orig }) upd
    = ctl { ctl_origin = upd orig }
  
  setCtLocEnv :: CtLoc -> CtLocEnv -> CtLoc
  setCtLocEnv ctl env = ctl { ctl_env = env }
  
  isGivenLoc :: CtLoc -> Bool
  isGivenLoc loc = isGivenOrigin (ctLocOrigin loc)
  
  pprCtLoc :: CtLoc -> SDoc
  -- "arising from ... at ..."
  -- Not an instance of Outputable because of the "arising from" prefix
  pprCtLoc (CtLoc { ctl_origin = o, ctl_env = lcl})
    = sep [ pprCtOrigin o
          , text "at" <+> ppr (getCtLocEnvLoc 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 { ctl_ctxt :: ![ErrCtxt]
                           , ctl_loc :: !RealSrcSpan
                           , ctl_bndrs :: !TcBinderStack
                           , ctl_tclvl :: !TcLevel
                           , ctl_in_gen_code :: !Bool
                           , ctl_rdr :: !LocalRdrEnv }
  
  getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan
  getCtLocEnvLoc = ctl_loc
  
  getCtLocEnvLvl :: CtLocEnv -> TcLevel
  getCtLocEnvLvl = ctl_tclvl
  
  setCtLocEnvLvl :: CtLocEnv -> TcLevel -> CtLocEnv
  setCtLocEnvLvl env lvl = env { ctl_tclvl = lvl }
  
  setCtLocRealLoc :: CtLocEnv -> RealSrcSpan -> CtLocEnv
  setCtLocRealLoc env ss = env { ctl_loc = ss }
  
  setCtLocEnvLoc :: CtLocEnv -> SrcSpan -> CtLocEnv
  -- See Note [Error contexts in generated code]
  -- for the ctl_in_gen_code manipulation
  setCtLocEnvLoc env (RealSrcSpan loc _)
    = env { ctl_loc = loc, ctl_in_gen_code = False }
  
  setCtLocEnvLoc env loc@(UnhelpfulSpan _)
    | isGeneratedSrcSpan loc
    = env { ctl_in_gen_code = True }
    | otherwise
    = env
  
  ctLocEnvInGeneratedCode :: CtLocEnv -> Bool
  ctLocEnvInGeneratedCode = ctl_in_gen_code
  