    module Agda.TypeChecking.MetaVars.Mention where

    import Data.HashSet (HashSet)
    import qualified Data.HashSet as HashSet
    import qualified Data.Set as Set

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad

    class MentionsMeta t where
      mentionsMetas :: HashSet MetaId -> t -> Bool

    mentionsMeta :: MentionsMeta t => MetaId -> t -> Bool
    mentionsMeta :: forall t. MentionsMeta t => MetaId -> t -> Bool
    mentionsMeta = HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas (HashSet MetaId -> t -> Bool)
    -> (MetaId -> HashSet MetaId) -> MetaId -> t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> HashSet MetaId
    forall a. Hashable a => a -> HashSet a
    HashSet.singleton

    instance MentionsMeta Term where
      mentionsMetas :: HashSet MetaId -> Term -> Bool
    mentionsMetas HashSet MetaId
    xs = \case
        Var Int
    _ Elims
    args   -> Elims -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Elims
    args
        Lam ArgInfo
    _ Abs Term
    b      -> Abs Term -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Abs Term
    b
        Lit{}        -> Bool
    False
        Def QName
    _ Elims
    args   -> Elims -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Elims
    args
        Con ConHead
    _ ConInfo
    _ Elims
    args -> Elims -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Elims
    args
        Pi Dom Type
    a Abs Type
    b       -> (Dom Type, Abs Type) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm (Dom Type
    a, Abs Type
    b)
        Sort Sort
    s       -> Sort -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Sort
    s
        Level Level
    l      -> Level -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Level
    l
        Dummy{}      -> Bool
    False
        DontCare Term
    v   -> Bool
    False   -- we don't have to look inside don't cares when deciding to wake constraints
        MetaV MetaId
    y Elims
    args -> MetaId -> HashSet MetaId -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    HashSet.member MetaId
    y HashSet MetaId
    xs Bool -> Bool -> Bool
    || Elims -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Elims
    args   -- TODO: we really only have to look one level deep at meta args
        where
          mm :: forall t. MentionsMeta t => t -> Bool
          mm :: forall t. MentionsMeta t => t -> Bool
    mm = HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs

    instance MentionsMeta Level where
      mentionsMetas :: HashSet MetaId -> Level -> Bool
    mentionsMetas HashSet MetaId
    xs (Max Integer
    _ [PlusLevel' Term]
    as) = HashSet MetaId -> [PlusLevel' Term] -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs [PlusLevel' Term]
    as

    instance MentionsMeta PlusLevel where
      mentionsMetas :: HashSet MetaId -> PlusLevel' Term -> Bool
    mentionsMetas HashSet MetaId
    xs (Plus Integer
    _ Term
    a) = HashSet MetaId -> Term -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Term
    a

    instance MentionsMeta Blocker where
      mentionsMetas :: HashSet MetaId -> Blocker -> Bool
    mentionsMetas HashSet MetaId
    xs (UnblockOnAll Set Blocker
    bs)  = HashSet MetaId -> [Blocker] -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs ([Blocker] -> Bool) -> [Blocker] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    bs
      mentionsMetas HashSet MetaId
    xs (UnblockOnAny Set Blocker
    bs)  = HashSet MetaId -> [Blocker] -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs ([Blocker] -> Bool) -> [Blocker] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    bs
      mentionsMetas HashSet MetaId
    xs (UnblockOnMeta MetaId
    x)  = MetaId -> HashSet MetaId -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    HashSet.member MetaId
    x HashSet MetaId
    xs
      mentionsMetas HashSet MetaId
    xs UnblockOnProblem{} = Bool
    False

    instance MentionsMeta Type where
        mentionsMetas :: HashSet MetaId -> Type -> Bool
    mentionsMetas HashSet MetaId
    xs (El Sort
    s Term
    t) = HashSet MetaId -> (Sort, Term) -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Sort
    s, Term
    t)

    instance MentionsMeta Sort where
      mentionsMetas :: HashSet MetaId -> Sort -> Bool
    mentionsMetas HashSet MetaId
    xs = \case
        Type Level
    l     -> HashSet MetaId -> Level -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Level
    l
        Prop Level
    l     -> HashSet MetaId -> Level -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Level
    l
        Inf IsFibrant
    _ Integer
    _    -> Bool
    False
        SSet Level
    l     -> HashSet MetaId -> Level -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Level
    l
        Sort
    SizeUniv   -> Bool
    False
        Sort
    LockUniv   -> Bool
    False
        PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> HashSet MetaId -> (Dom' Term Term, Sort, Abs Sort) -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Dom' Term Term
    a, Sort
    s1, Abs Sort
    s2)
        FunSort Sort
    s1 Sort
    s2 -> HashSet MetaId -> (Sort, Sort) -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Sort
    s1, Sort
    s2)
        UnivSort Sort
    s -> HashSet MetaId -> Sort -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Sort
    s
        MetaS MetaId
    m Elims
    es -> MetaId -> HashSet MetaId -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    HashSet.member MetaId
    m HashSet MetaId
    xs Bool -> Bool -> Bool
    || HashSet MetaId -> Elims -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Elims
    es
        DefS QName
    d Elims
    es  -> HashSet MetaId -> Elims -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Elims
    es
        DummyS{}   -> Bool
    False

    instance MentionsMeta t => MentionsMeta (Abs t) where
      mentionsMetas :: HashSet MetaId -> Abs t -> Bool
    mentionsMetas HashSet MetaId
    xs = HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (t -> Bool) -> (Abs t -> t) -> Abs t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs t -> t
    forall a. Abs a -> a
    unAbs

    instance MentionsMeta t => MentionsMeta (Arg t) where
      mentionsMetas :: HashSet MetaId -> Arg t -> Bool
    mentionsMetas HashSet MetaId
    xs Arg t
    a | Arg t -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Arg t
    a = Bool
    False
      -- we don't have to look inside irrelevant arguments when deciding to wake constraints
      mentionsMetas HashSet MetaId
    xs Arg t
    a = HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Arg t -> t
    forall e. Arg e -> e
    unArg Arg t
    a)

    instance MentionsMeta t => MentionsMeta (Dom t) where
      mentionsMetas :: HashSet MetaId -> Dom t -> Bool
    mentionsMetas HashSet MetaId
    xs = HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (t -> Bool) -> (Dom t -> t) -> Dom t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom t -> t
    forall t e. Dom' t e -> e
    unDom

    instance MentionsMeta t => MentionsMeta [t] where
      mentionsMetas :: HashSet MetaId -> [t] -> Bool
    mentionsMetas HashSet MetaId
    xs = (t -> Bool) -> [t] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs)

    instance MentionsMeta t => MentionsMeta (Maybe t) where
      mentionsMetas :: HashSet MetaId -> Maybe t -> Bool
    mentionsMetas HashSet MetaId
    xs = Bool -> (t -> Bool) -> Maybe t -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False (HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs)

    instance (MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) where
      mentionsMetas :: HashSet MetaId -> (a, b) -> Bool
    mentionsMetas HashSet MetaId
    xs (a
    a, b
    b) = HashSet MetaId -> a -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs a
    a Bool -> Bool -> Bool
    || HashSet MetaId -> b -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs b
    b

    instance (MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) where
      mentionsMetas :: HashSet MetaId -> (a, b, c) -> Bool
    mentionsMetas HashSet MetaId
    xs (a
    a, b
    b, c
    c) = HashSet MetaId -> a -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs a
    a Bool -> Bool -> Bool
    || HashSet MetaId -> b -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs b
    b Bool -> Bool -> Bool
    || HashSet MetaId -> c -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs c
    c

    instance MentionsMeta a => MentionsMeta (Closure a) where
      mentionsMetas :: HashSet MetaId -> Closure a -> Bool
    mentionsMetas HashSet MetaId
    xs Closure a
    cl = HashSet MetaId -> a -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Closure a -> a
    forall a. Closure a -> a
    clValue Closure a
    cl)

    instance MentionsMeta Elim where
      mentionsMetas :: HashSet MetaId -> Elim' Term -> Bool
    mentionsMetas HashSet MetaId
    xs Proj{} = Bool
    False
      mentionsMetas HashSet MetaId
    xs (Apply Arg Term
    v) = HashSet MetaId -> Arg Term -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Arg Term
    v
      mentionsMetas HashSet MetaId
    xs (IApply Term
    y0 Term
    y1 Term
    v) = HashSet MetaId -> (Term, Term, Term) -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Term
    y0,Term
    y1,Term
    v)

    instance MentionsMeta a => MentionsMeta (Tele a) where
      mentionsMetas :: HashSet MetaId -> Tele a -> Bool
    mentionsMetas HashSet MetaId
    xs Tele a
    EmptyTel = Bool
    False
      mentionsMetas HashSet MetaId
    xs (ExtendTel a
    a Abs (Tele a)
    b) = HashSet MetaId -> (a, Abs (Tele a)) -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (a
    a, Abs (Tele a)
    b)

    instance MentionsMeta ProblemConstraint where
      mentionsMetas :: HashSet MetaId -> ProblemConstraint -> Bool
    mentionsMetas HashSet MetaId
    xs = HashSet MetaId -> Closure Constraint -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs (Closure Constraint -> Bool)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint

    instance MentionsMeta Constraint where
      mentionsMetas :: HashSet MetaId -> Constraint -> Bool
    mentionsMetas HashSet MetaId
    xs = \case
        ValueCmp Comparison
    _ CompareAs
    t Term
    u Term
    v    -> (CompareAs, Term, Term) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm (CompareAs
    t, Term
    u, Term
    v)
        ValueCmpOnFace Comparison
    _ Term
    p Type
    t Term
    u Term
    v    -> ((Term, Type), Term, Term) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm ((Term
    p,Type
    t), Term
    u, Term
    v)
        ElimCmp [Polarity]
    _ [IsForced]
    _ Type
    t Term
    v Elims
    as Elims
    bs -> ((Type, Term), (Elims, Elims)) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm ((Type
    t, Term
    v), (Elims
    as, Elims
    bs))
        LevelCmp Comparison
    _ Level
    u Level
    v      -> (Level, Level) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm (Level
    u, Level
    v)
        SortCmp Comparison
    _ Sort
    a Sort
    b       -> (Sort, Sort) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm (Sort
    a, Sort
    b)
        UnBlock MetaId
    _           -> Bool
    True   -- this might be a postponed typechecking
                                      -- problem and we don't have a handle on
                                      -- what metas it depends on
        FindInstance{}      -> Bool
    True   -- this needs to be woken up for any meta
        IsEmpty Range
    r Type
    t         -> Type -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Type
    t
        CheckSizeLtSat Term
    t    -> Term -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Term
    t
        CheckFunDef{}       -> Bool
    True   -- not sure what metas this depends on
        HasBiggerSort Sort
    a     -> Sort -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Sort
    a
        HasPTSRule Dom Type
    a Abs Sort
    b      -> (Dom Type, Abs Sort) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm (Dom Type
    a, Abs Sort
    b)
        UnquoteTactic Term
    tac Term
    hole Type
    goal -> Bool
    False
        CheckMetaInst MetaId
    m     -> Bool
    True   -- TODO
        CheckType Type
    t         -> Type -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Type
    t
        CheckLockedVars Term
    a Type
    b Arg Term
    c Type
    d -> ((Term, Type), (Arg Term, Type)) -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm ((Term
    a, Type
    b), (Arg Term
    c, Type
    d))
        UsableAtModality Modality
    mod Term
    t -> Term -> Bool
    forall t. MentionsMeta t => t -> Bool
    mm Term
    t
        where
          mm :: forall t. MentionsMeta t => t -> Bool
          mm :: forall t. MentionsMeta t => t -> Bool
    mm = HashSet MetaId -> t -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs

    instance MentionsMeta CompareAs where
      mentionsMetas :: HashSet MetaId -> CompareAs -> Bool
    mentionsMetas HashSet MetaId
    xs = \case
        AsTermsOf Type
    a -> HashSet MetaId -> Type -> Bool
    forall t. MentionsMeta t => HashSet MetaId -> t -> Bool
    mentionsMetas HashSet MetaId
    xs Type
    a
        CompareAs
    AsSizes -> Bool
    False
        CompareAs
    AsTypes -> Bool
    False

    -- instance (Ord k, MentionsMeta e) => MentionsMeta (Map k e) where
    --   mentionsMeta = traverse mentionsMeta