module GHC.Tc.Types.CtLoc (

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

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

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

  -- * Explanations
  CtExplanations(..), ctLocExplanations, updCtLocExplanations,
  outOfScopeNT, stuckDataFamApp, nullCtExplanations,

  -- * RoleExplanation
  RoleExplanation(..),
  tyConAppRoleExplanation, appTyRoleExplanation

  ) 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.Basic( IntWithInf, mkIntWithInf, TypeOrKind(..) )
import GHC.Types.SrcLoc
import GHC.Types.Name.Reader
import GHC.Types.Unique.Map ( UniqMap, emptyUniqMap, plusUniqMap_C, unitUniqMap, isNullUniqMap )
import GHC.Types.Unique.Set ( UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet, isEmptyUniqSet )

import GHC.Core.DataCon ( DataCon )
import GHC.Core.TyCon
  ( Role(..), TyCon, TyConBinder
  , isVisibleTyConBinder, isNamedTyConBinder
  )
import GHC.Utils.Outputable

import qualified Data.Semigroup as S
import qualified GHC.Data.List.NonEmpty as NE

{- *********************************************************************
*                                                                      *
            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.

-}


-- | '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.
--
-- See Note [CtLoc].
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 -> CtExplanations
ctl_expln    :: CtExplanations
                      -- ^ Explanations we can display to the user if
                      -- the constraint goes unsolved; see Note [CtExplanations]
                   , CtLoc -> SubGoalDepth
ctl_depth    :: !SubGoalDepth
                   }

{- Note [CtLoc]
~~~~~~~~~~~~~~~
When we report an unsolved constraint to the user, we report several pieces of
information to the user for additional context:

  - `CtOrigin` describes the place in the source code where the constraint
    originated; the same `CtOrigin` is inherited by its sub-goals.
    For example, starting with `Maybe t1 ~# Maybe t2` we may decompose to
    `t1 ~# t2`, but the latter inherits the same `CtOrigin`.
  - `CtLocEnv` provides further context, e.g. a source code line number, as
    well as e.g. in-scope bindings so that they can be suggested for an
    out-of-scope error.
  - `CtExplanations` contain additional information that explain why we ended
    up with this sub-goal. They pertain to work the solver has done to process
    the original constraint. See See Note [CtExplanations].

Note [CtExplanations]
~~~~~~~~~~~~~~~~~~~~~
The CtExplanations type records information about steps the solver has taken
when processing a constraint, in particular when the solver had to make a choice.

For example, starting with a representational equality `T a ~R# T b`, the solver
may proceed in two different ways:

  (Unwrap)
    If T is a newtype whose constructor is in scope, we may unwrap it, resulting
    in the constraint `a ~R# b`.
  (Decompose)
    If T is a not a newtype or its constructor isn't in scope, we decompose
    according to the role of `T`. If `T` has nominal role, this means we end
    up with `a ~# b`.

It's helpful to report some additional explanations if we end up with `a ~# b`
starting from `T a ~R# T b`: the user might wonder why the role went from
representational to nominal:

  (NTScope)
    If `T` is a newtype whose constructor is out-of-scope, inform the user:

      NB: The data constructor ‘MkT’ of newtype ‘T’ is not in scope.

  (Role)
    If moreover `T` has nominal role, also report that to the user.

      NB: ‘T’ has nominal role in its first argument.

This is especially important as `T` may otherwise not appear in the error
message at all (as indeed is the case if we end up with `a ~# b`), so it can be
jolly confusing: #15850, #20289, #23731, #26137.

CRUCIAL POINT: we store the out-of-scope newtype constructor precisely at the
point in the typechecker in which we perform the in-scope test. That is, in
the ReprEq case of GHC.Tc.Solver.Equality.can_eq_nc, where we call
tcTopNormaliseNewTypeTF_maybe.
This ensures that the explanations are in sync with the source of truth.

For the time being, CtExplanations records only information relating to
representational equalities, as described above. In the future, one could
imagine adding explanations relating to instance resolution, e.g.

  - Store the result of instance lookup, e.g. "no instances" or
    "overlapping instances", to avoid needing to perform a second instance
    lookup in GHC.Tc.Errors.mkDictErr.
  - When GHC holds off from using a quantified constraint because there is no
    single "best match" (#22216).
-}

-- | Explanations that can be presented to the user about why the solver
-- might have failed to solve a constraint. See Note [CtExplanations].
--
-- For example: couldn't solve a representational equality because a newtype
-- constructor was out of scope.
data CtExplanations
  -- NB: there might be several explanations associated with a single constraint.
  -- Example: T23731b, where the error "Couldn't match type ‘Int’ with ‘Sum Int’"
  -- comes with the explanations
  --
  --    The type constructor ‘Foo’ has nominal role in its first argument.
  --    The data constructor ‘MkFoo’ of newtype ‘Foo’ is not in scope.
  = CtExplanations
    { CtExplanations -> [RoleExplanation]
ctexpl_roleExplanations :: [RoleExplanation]
      -- ^ Explanations to the user that involve roles,
      -- e.g. remarking that a 'TyCon' has nominal role in one of its arguments.
    , CtExplanations -> UniqSet DataCon
ctexpl_outOfScopeNTs :: UniqSet DataCon
      -- ^ Newtypes that could not be unwrapped because their constructors
      -- were not in scope.
      --
      -- NB: store the 'DataCon' rather than the 'TyCon', as this avoids
      -- any issues with internal representation 'TyCon's for data families,
      -- as in 'data family D a; newtype instance D Int = MkDInt Bool'.

    , CtExplanations -> UniqMap TyCon (NonEmpty [Type])
ctexpl_stuckDataFamApps :: UniqMap TyCon (NE.NonEmpty [Type])
      -- ^ Data family applications that could not be reduced.
    }

outOfScopeNT :: DataCon -> CtExplanations
outOfScopeNT :: DataCon -> CtExplanations
outOfScopeNT DataCon
nt =
  CtExplanations
forall a. Monoid a => a
mempty { ctexpl_outOfScopeNTs = unitUniqSet nt }

stuckDataFamApp :: TyCon -> [Type] -> CtExplanations
stuckDataFamApp :: TyCon -> [Type] -> CtExplanations
stuckDataFamApp TyCon
tc [Type]
tys =
  CtExplanations
forall a. Monoid a => a
mempty { ctexpl_stuckDataFamApps = unitUniqMap tc (NE.singleton tys) }

nullCtExplanations :: CtExplanations -> Bool
nullCtExplanations :: CtExplanations -> Bool
nullCtExplanations (CtExplanations [RoleExplanation]
a UniqSet DataCon
b UniqMap TyCon (NonEmpty [Type])
c) =
  [RoleExplanation] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RoleExplanation]
a Bool -> Bool -> Bool
&& UniqSet DataCon -> Bool
forall a. UniqSet a -> Bool
isEmptyUniqSet UniqSet DataCon
b Bool -> Bool -> Bool
&& UniqMap TyCon (NonEmpty [Type]) -> Bool
forall k a. UniqMap k a -> Bool
isNullUniqMap UniqMap TyCon (NonEmpty [Type])
c

instance Outputable CtExplanations where
  ppr :: CtExplanations -> SDoc
ppr (CtExplanations [RoleExplanation]
ns UniqSet DataCon
cs UniqMap TyCon (NonEmpty [Type])
dfs) =
    SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"CtExplanations")
      Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
            [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"nominal reasons:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [RoleExplanation] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [RoleExplanation]
ns
            , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"out of scope newtype constructors:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> UniqSet DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr UniqSet DataCon
cs
            , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"stuck data-fam apps:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> UniqMap TyCon (NonEmpty [Type]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr UniqMap TyCon (NonEmpty [Type])
dfs
            ]
instance Semigroup CtExplanations where
  CtExplanations [RoleExplanation]
n1 UniqSet DataCon
c1 UniqMap TyCon (NonEmpty [Type])
dfs1 <> :: CtExplanations -> CtExplanations -> CtExplanations
<> CtExplanations [RoleExplanation]
n2 UniqSet DataCon
c2 UniqMap TyCon (NonEmpty [Type])
dfs2 =
    [RoleExplanation]
-> UniqSet DataCon
-> UniqMap TyCon (NonEmpty [Type])
-> CtExplanations
CtExplanations
      ([RoleExplanation]
n1 [RoleExplanation] -> [RoleExplanation] -> [RoleExplanation]
forall a. [a] -> [a] -> [a]
++ [RoleExplanation]
n2)
      (UniqSet DataCon
c1 UniqSet DataCon -> UniqSet DataCon -> UniqSet DataCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` UniqSet DataCon
c2)
      ((NonEmpty [Type] -> NonEmpty [Type] -> NonEmpty [Type])
-> UniqMap TyCon (NonEmpty [Type])
-> UniqMap TyCon (NonEmpty [Type])
-> UniqMap TyCon (NonEmpty [Type])
forall a k.
(a -> a -> a) -> UniqMap k a -> UniqMap k a -> UniqMap k a
plusUniqMap_C NonEmpty [Type] -> NonEmpty [Type] -> NonEmpty [Type]
forall a. Semigroup a => a -> a -> a
(S.<>) UniqMap TyCon (NonEmpty [Type])
dfs1 UniqMap TyCon (NonEmpty [Type])
dfs2)

instance Monoid CtExplanations where
  mempty :: CtExplanations
mempty = [RoleExplanation]
-> UniqSet DataCon
-> UniqMap TyCon (NonEmpty [Type])
-> CtExplanations
CtExplanations [] UniqSet DataCon
forall a. UniqSet a
emptyUniqSet UniqMap TyCon (NonEmpty [Type])
forall k a. UniqMap k a
emptyUniqMap

-- | Information about why a representational equality gave rise to
-- a nominal equality.
data RoleExplanation
  -- | The 'TyCon' has the given role this argument.
  = TyConArg
      TyCon
      Int -- ^ argument position (starting from 1); may be greater than the
          -- arity of the 'TyCon' in the case of an over-saturated application
      Role
  -- | The role of the argument in an 'AppTy' is nominal.
  --
  -- Store the function type in the 'AppTy'.
  | NominalAppTy Type
instance Outputable RoleExplanation where
  ppr :: RoleExplanation -> SDoc
ppr = \case
    TyConArg TyCon
tc Int
i Role
r ->
      String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NominalTyConArg" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
i SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r
    NominalAppTy Type
f ->
      String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NominalAppTy" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
f

addRoleExplanation :: RoleExplanation -> CtExplanations -> CtExplanations
addRoleExplanation :: RoleExplanation -> CtExplanations -> CtExplanations
addRoleExplanation RoleExplanation
rea CtExplanations
expln =
  CtExplanations
expln { ctexpl_roleExplanations = rea : ctexpl_roleExplanations expln }

mkKindEqLoc :: TcType -> TcType   -- original *types* being compared
            -> CtLoc -> CtLoc
mkKindEqLoc :: Type -> Type -> CtLoc -> CtLoc
mkKindEqLoc Type
s1 Type
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 :: Maybe TyConBinder -> Maybe RoleExplanation -> CtLoc -> CtLoc
-- Adjust the CtLoc when decomposing a type constructor
adjustCtLocTyConBinder :: Maybe TyConBinder -> Maybe RoleExplanation -> CtLoc -> CtLoc
adjustCtLocTyConBinder Maybe TyConBinder
mb_tc_bndr Maybe RoleExplanation
mb_repr CtLoc
loc
  = Maybe InvisibleBit
-> Bool -> Maybe RoleExplanation -> CtLoc -> CtLoc
adjustCtLoc Maybe InvisibleBit
mb_invis_kind Bool
is_kind Maybe RoleExplanation
mb_repr CtLoc
loc
  where
    mb_invis_kind :: Maybe InvisibleBit
mb_invis_kind
      | Just TyConBinder
tc_bndr <- Maybe TyConBinder
mb_tc_bndr
      , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyConBinder -> Bool
forall tv. VarBndr tv TyConBndrVis -> Bool
isVisibleTyConBinder TyConBinder
tc_bndr
      = InvisibleBit -> Maybe InvisibleBit
forall a. a -> Maybe a
Just InvisibleBit
InvisibleKind
      | Bool
otherwise
      = Maybe InvisibleBit
forall a. Maybe a
Nothing
    is_kind :: Bool
is_kind = Bool -> (TyConBinder -> Bool) -> Maybe TyConBinder -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False TyConBinder -> Bool
isNamedTyConBinder Maybe TyConBinder
mb_tc_bndr

-- | Add a role explanation when decomposing 'T a ~r1 T b' for some role 'r1'
-- into 'a ~r2 b' with stronger role 'r2' (e.g. turning a representational
-- equality into a nominal equality).
tyConAppRoleExplanation :: Role -> TyCon -> (Int, Role) -> Maybe RoleExplanation
tyConAppRoleExplanation :: Role -> TyCon -> (Int, Role) -> Maybe RoleExplanation
tyConAppRoleExplanation Role
role TyCon
tc (Int
arg_no, Role
arg_role) =
  if Role
arg_role Role -> Role -> Bool
forall a. Ord a => a -> a -> Bool
< Role
role -- finer notion of equality
  then RoleExplanation -> Maybe RoleExplanation
RoleExplanation -> Maybe RoleExplanation
forall a. a -> Maybe a
Just (RoleExplanation -> Maybe RoleExplanation)
-> RoleExplanation -> Maybe RoleExplanation
forall a b. (a -> b) -> a -> b
$ TyCon -> Int -> Role -> RoleExplanation
TyConArg TyCon
tc Int
arg_no Role
arg_role
  else Maybe RoleExplanation
forall a. Maybe a
Nothing

appTyRoleExplanation :: Type -> CtOrigin -> Maybe RoleExplanation
appTyRoleExplanation :: Type -> CtOrigin -> Maybe RoleExplanation
appTyRoleExplanation Type
s CtOrigin
orig
  | (CtOrigin, (Type, Type))
_ : [(CtOrigin, (Type, Type))]
_ <- CtOrigin -> [(CtOrigin, (Type, Type))]
defaultReprEqOrigins CtOrigin
orig
  = RoleExplanation -> Maybe RoleExplanation
RoleExplanation -> Maybe RoleExplanation
forall a. a -> Maybe a
Just (RoleExplanation -> Maybe RoleExplanation)
-> RoleExplanation -> Maybe RoleExplanation
forall a b. (a -> b) -> a -> b
$ Type -> RoleExplanation
NominalAppTy Type
s
  | Bool
otherwise
  = Maybe RoleExplanation
forall a. Maybe a
Nothing

adjustCtLoc :: Maybe InvisibleBit
            -> Bool    -- True <=> A kind argument
            -> Maybe RoleExplanation
            -> CtLoc -> CtLoc
-- Adjust the CtLoc when decomposing a type constructor, application, etc
adjustCtLoc :: Maybe InvisibleBit
-> Bool -> Maybe RoleExplanation -> CtLoc -> CtLoc
adjustCtLoc Maybe InvisibleBit
mb_invis Bool
is_kind Maybe RoleExplanation
mb_repr CtLoc
loc
  = CtLoc
loc3
  where
    loc1 :: CtLoc
loc1 | Bool
is_kind   = CtLoc -> CtLoc
toKindLoc CtLoc
loc
         | Bool
otherwise = CtLoc
loc
    loc2 :: CtLoc
loc2 =
      case Maybe InvisibleBit
mb_invis of
        Maybe InvisibleBit
Nothing    -> CtLoc
loc1
        Just InvisibleBit
invis -> InvisibleBit -> CtLoc -> CtLoc
toInvisibleLoc InvisibleBit
invis CtLoc
loc1
    loc3 :: CtLoc
loc3 | Just RoleExplanation
repr_loc <- Maybe RoleExplanation
mb_repr
         = (CtExplanations -> CtExplanations) -> CtLoc -> CtLoc
updCtLocExplanations (RoleExplanation -> CtExplanations -> CtExplanations
addRoleExplanation RoleExplanation
repr_loc) CtLoc
loc2
         | Bool
otherwise
         = CtLoc
loc2

-- | 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 :: InvisibleBit -> CtLoc -> CtLoc
toInvisibleLoc :: InvisibleBit -> CtLoc -> CtLoc
toInvisibleLoc InvisibleBit
invis CtLoc
loc = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin CtLoc
loc (InvisibleBit -> CtOrigin -> CtOrigin
toInvisibleOrigin InvisibleBit
invis)

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    -- these only matter
          , ctl_expln :: CtExplanations
ctl_expln    = CtExplanations
forall a. Monoid a => a
mempty     -- for error messages
          , 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

ctLocExplanations :: CtLoc -> CtExplanations
ctLocExplanations :: CtLoc -> CtExplanations
ctLocExplanations = CtLoc -> CtExplanations
ctl_expln

updCtLocExplanations :: (CtExplanations -> CtExplanations) -> CtLoc -> CtLoc
updCtLocExplanations :: (CtExplanations -> CtExplanations) -> CtLoc -> CtLoc
updCtLocExplanations CtExplanations -> CtExplanations
f CtLoc
loc = CtLoc
loc { ctl_expln = f $ ctl_expln loc }

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 }

resetCtLocDepth :: CtLoc -> CtLoc
resetCtLocDepth :: CtLoc -> CtLoc
resetCtLocDepth CtLoc
loc = CtLoc
loc { ctl_depth = initialSubGoalDepth }

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