    module Agda.TypeChecking.MetaVars.Mention where

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

    class MentionsMeta t where
      mentionsMeta :: MetaId -> t -> Bool

    instance MentionsMeta Term where
      mentionsMeta x v = case v of
        Var _ args   -> mm args
        Lam _ b      -> mm b
        Lit{}        -> False
        Def _ args   -> mm args
        Con _ _ args -> mm args
        Pi a b       -> mm (a, b)
        Sort s       -> mm s
        Level l      -> mm l
        Dummy{}      -> False
        DontCare v   -> False   -- we don't have to look inside don't cares when deciding to wake constraints
        MetaV y args -> x == y || mm args   -- TODO: we really only have to look one level deep at meta args
        where
          mm v = mentionsMeta x v

    instance MentionsMeta Level where
      mentionsMeta x (Max as) = mentionsMeta x as

    instance MentionsMeta PlusLevel where
      mentionsMeta x ClosedLevel{} = False
      mentionsMeta x (Plus _ a) = mentionsMeta x a

    instance MentionsMeta LevelAtom where
      mentionsMeta x l = case l of
        MetaLevel m vs   -> x == m || mentionsMeta x vs
        BlockedLevel m _ -> x == m    -- if it's blocked on a different meta it doesn't matter if it mentions the meta somewhere else
        UnreducedLevel l -> mentionsMeta x l
        NeutralLevel _ l -> mentionsMeta x l

    instance MentionsMeta Type where
        mentionsMeta x (El s t) = mentionsMeta x (s, t)

    instance MentionsMeta Sort where
      mentionsMeta x s = case s of
        Type l     -> mentionsMeta x l
        Prop l     -> mentionsMeta x l
        Inf        -> False
        SizeUniv   -> False
        PiSort s1 s2 -> mentionsMeta x (s1, s2)
        UnivSort s -> mentionsMeta x s
        MetaS m es -> x == m || mentionsMeta x es
        DefS d es  -> mentionsMeta x es
        DummyS{}   -> False

    instance MentionsMeta t => MentionsMeta (Abs t) where
      mentionsMeta x = mentionsMeta x . unAbs

    instance MentionsMeta t => MentionsMeta (Arg t) where
      mentionsMeta x a | isIrrelevant a = False
      -- ^ we don't have to look inside irrelevant arguments when deciding to wake constraints
      mentionsMeta x a = mentionsMeta x (unArg a)

    instance MentionsMeta t => MentionsMeta (Dom t) where
      mentionsMeta x = mentionsMeta x . unDom

    instance MentionsMeta t => MentionsMeta [t] where
      mentionsMeta x = any (mentionsMeta x)

    instance MentionsMeta t => MentionsMeta (Maybe t) where
      mentionsMeta x = maybe False (mentionsMeta x)

    instance (MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) where
      mentionsMeta x (a, b) = mentionsMeta x a || mentionsMeta x b

    instance (MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) where
      mentionsMeta x (a, b, c) = mentionsMeta x a || mentionsMeta x b || mentionsMeta x c

    instance MentionsMeta a => MentionsMeta (Closure a) where
      mentionsMeta x cl = mentionsMeta x (clValue cl)

    instance MentionsMeta Elim where
      mentionsMeta x Proj{} = False
      mentionsMeta x (Apply v) = mentionsMeta x v
      mentionsMeta x (IApply y0 y1 v) = mentionsMeta x (y0,y1,v)

    instance MentionsMeta a => MentionsMeta (Tele a) where
      mentionsMeta x EmptyTel = False
      mentionsMeta x (ExtendTel a b) = mentionsMeta x (a, b)

    instance MentionsMeta ProblemConstraint where
      mentionsMeta x = mentionsMeta x . theConstraint

    instance MentionsMeta Constraint where
      mentionsMeta x c = case c of
        ValueCmp _ t u v    -> mm (t, u, v)
        ValueCmpOnFace _ p t u v    -> mm ((p,t), u, v)
        ElimCmp _ _ t v as bs -> mm ((t, v), (as, bs))
        LevelCmp _ u v      -> mm (u, v)
        TypeCmp _ a b       -> mm (a, b)
        TelCmp a b _ u v    -> mm ((a, b), (u, v))
        SortCmp _ a b       -> mm (a, b)
        Guarded{}           -> False  -- This gets woken up when the problem it's guarded by is solved
        UnBlock _           -> True   -- this might be a postponed typechecking
                                      -- problem and we don't have a handle on
                                      -- what metas it depends on
        FindInstance{}      -> True   -- this needs to be woken up for any meta
        IsEmpty r t         -> mm t
        CheckSizeLtSat t    -> mm t
        CheckFunDef{}       -> True   -- not sure what metas this depends on
        HasBiggerSort a     -> mm a
        HasPTSRule a b      -> mm (a, b)
        UnquoteTactic bl tac hole goal -> Just x == bl
        where
          mm v = mentionsMeta x v

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