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