    -- | Extract all names from things.

    module Agda.Syntax.Internal.Names where

    import Data.List.NonEmpty (NonEmpty(..))
    import Data.Map (Map)
    import Data.Set (Set)

    import Agda.Syntax.Common
    import Agda.Syntax.Literal
    import Agda.Syntax.Internal
    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Abstract as A

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.CompiledClause

    import Agda.Utils.Singleton
    import Agda.Utils.Impossible

    namesIn :: (NamesIn a, Collection QName m) => a -> m
    namesIn :: forall a m. (NamesIn a, Collection QName m) => a -> m
    namesIn = (QName -> m) -> a -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton

    class NamesIn a where
      namesIn' :: Monoid m => (QName -> m) -> a -> m

      default namesIn' :: (Monoid m, Foldable f, NamesIn b, f b ~ a) => (QName -> m) -> a -> m
      namesIn' = (b -> m) -> f b -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> m) -> f b -> m)
    -> ((QName -> m) -> b -> m) -> (QName -> m) -> f b -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> m) -> b -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn'

    -- Generic collections
    instance NamesIn a => NamesIn (Maybe a)
    instance NamesIn a => NamesIn [a]
    instance NamesIn a => NamesIn (NonEmpty a)
    instance NamesIn a => NamesIn (Set a)
    instance NamesIn a => NamesIn (Map k a)

    -- Decorations
    instance NamesIn a => NamesIn (Arg a)
    instance NamesIn a => NamesIn (Dom a)
    instance NamesIn a => NamesIn (Named n a)
    instance NamesIn a => NamesIn (Abs a)
    instance NamesIn a => NamesIn (WithArity a)
    instance NamesIn a => NamesIn (Open a)
    instance NamesIn a => NamesIn (C.FieldAssignment' a)

    -- Specific collections
    instance NamesIn a => NamesIn (Tele a)

    -- Tuples

    instance (NamesIn a, NamesIn b) => NamesIn (a, b) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> (a, b) -> m
    namesIn' QName -> m
    sg (a
    x, b
    y) = m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend ((QName -> m) -> a -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg a
    x) ((QName -> m) -> b -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg b
    y)

    instance (NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> (a, b, c) -> m
    namesIn' QName -> m
    sg (a
    x, b
    y, c
    z) = (QName -> m) -> (a, (b, c)) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (a
    x, (b
    y, c
    z))

    instance (NamesIn a, NamesIn b, NamesIn c, NamesIn d) => NamesIn (a, b, c, d) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> (a, b, c, d) -> m
    namesIn' QName -> m
    sg (a
    x, b
    y, c
    z, d
    u) = (QName -> m) -> ((a, b), (c, d)) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg ((a
    x, b
    y), (c
    z, d
    u))

    instance NamesIn CompKit where
      namesIn' :: forall m. Monoid m => (QName -> m) -> CompKit -> m
    namesIn' QName -> m
    sg (CompKit Maybe QName
    a Maybe QName
    b) = (QName -> m) -> (Maybe QName, Maybe QName) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Maybe QName
    a,Maybe QName
    b)

    -- Base case

    instance NamesIn QName where
      namesIn' :: forall m. Monoid m => (QName -> m) -> QName -> m
    namesIn' QName -> m
    sg QName
    x = QName -> m
    sg QName
    x  -- interesting case!

    instance NamesIn ConHead where
      namesIn' :: forall m. Monoid m => (QName -> m) -> ConHead -> m
    namesIn' QName -> m
    sg ConHead
    h = (QName -> m) -> QName -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (ConHead -> QName
    conName ConHead
    h)

    -- Andreas, 2017-07-27
    -- In the following clauses, the choice of fields is not obvious
    -- to the reader.  Please comment on the choices.
    --
    -- Also, this would be more robust if these were constructor-style
    -- matches instead of record-style matches.
    -- If someone adds a field containing names, this would go unnoticed.

    instance NamesIn Definition where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Definition -> m
    namesIn' QName -> m
    sg Definition
    def = (QName -> m) -> (Type, Defn, [LocalDisplayForm]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Definition -> Type
    defType Definition
    def, Definition -> Defn
    theDef Definition
    def, Definition -> [LocalDisplayForm]
    defDisplay Definition
    def)

    instance NamesIn Defn where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Defn -> m
    namesIn' QName -> m
    sg = \case
        Axiom Bool
    _            -> m
    forall a. Monoid a => a
    mempty
        DataOrRecSig{}     -> m
    forall a. Monoid a => a
    mempty
        GeneralizableVar{} -> m
    forall a. Monoid a => a
    mempty
        PrimitiveSort{}    -> m
    forall a. Monoid a => a
    mempty
        AbstractDefn{}     -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- Andreas 2017-07-27, Q: which names can be in @cc@ which are not already in @cl@?
        Function    { funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cl, funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc }
          -> (QName -> m) -> ([Clause], Maybe CompiledClauses) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg ([Clause]
    cl, Maybe CompiledClauses
    cc)
        Datatype    { dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    cl, dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs, dataSort :: Defn -> Sort
    dataSort = Sort
    s }
          -> (QName -> m) -> (Maybe Clause, [QName], Sort) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Maybe Clause
    cl, [QName]
    cs, Sort
    s)
        Record      { recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    cl, recConHead :: Defn -> ConHead
    recConHead = ConHead
    c, recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    fs, recComp :: Defn -> CompKit
    recComp = CompKit
    comp }
          -> (QName -> m) -> (Maybe Clause, ConHead, [Dom QName], CompKit) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Maybe Clause
    cl, ConHead
    c, [Dom QName]
    fs, CompKit
    comp)
          -- Don't need recTel since those will be reachable from the constructor
        Constructor { conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c, conData :: Defn -> QName
    conData = QName
    d, conComp :: Defn -> CompKit
    conComp = CompKit
    kit, conProj :: Defn -> Maybe [QName]
    conProj = Maybe [QName]
    fs }
          -> (QName -> m) -> (ConHead, QName, CompKit, Maybe [QName]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (ConHead
    c, QName
    d, CompKit
    kit, Maybe [QName]
    fs)
        Primitive   { primClauses :: Defn -> [Clause]
    primClauses = [Clause]
    cl, primCompiled :: Defn -> Maybe CompiledClauses
    primCompiled = Maybe CompiledClauses
    cc }
          -> (QName -> m) -> ([Clause], Maybe CompiledClauses) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg ([Clause]
    cl, Maybe CompiledClauses
    cc)

    instance NamesIn Clause where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Clause -> m
    namesIn' QName -> m
    sg Clause{ clauseTel :: Clause -> Telescope
    clauseTel = Telescope
    tel, namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps, clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    b, clauseType :: Clause -> Maybe (Arg Type)
    clauseType = Maybe (Arg Type)
    t } =
        (QName -> m)
    -> (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Telescope
    tel, NAPs
    ps, Maybe Term
    b, Maybe (Arg Type)
    t)

    instance NamesIn CompiledClauses where
      namesIn' :: forall m. Monoid m => (QName -> m) -> CompiledClauses -> m
    namesIn' QName -> m
    sg (Case Arg Int
    _ Case CompiledClauses
    c) = (QName -> m) -> Case CompiledClauses -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Case CompiledClauses
    c
      namesIn' QName -> m
    sg (Done [Arg ArgName]
    _ Term
    v) = (QName -> m) -> Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Term
    v
      namesIn' QName -> m
    sg Fail{}     = m
    forall a. Monoid a => a
    mempty

    -- Andreas, 2017-07-27
    -- Why ignoring the litBranches?
    instance NamesIn a => NamesIn (Case a) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Case a -> m
    namesIn' QName -> m
    sg Branches{ conBranches :: forall c. Case c -> Map QName (WithArity c)
    conBranches = Map QName (WithArity a)
    bs, catchAllBranch :: forall c. Case c -> Maybe c
    catchAllBranch = Maybe a
    c } =
        (QName -> m) -> (Map QName (WithArity a), Maybe a) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Map QName (WithArity a)
    bs, Maybe a
    c)

    instance NamesIn (Pattern' a) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Pattern' a -> m
    namesIn' QName -> m
    sg = \case
        VarP{}          -> m
    forall a. Monoid a => a
    mempty
        LitP PatternInfo
    _ Literal
    l        -> (QName -> m) -> Literal -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Literal
    l
        DotP PatternInfo
    _ Term
    v        -> (QName -> m) -> Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Term
    v
        ConP ConHead
    c ConPatternInfo
    _ [NamedArg (Pattern' a)]
    args   -> (QName -> m) -> (ConHead, [NamedArg (Pattern' a)]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (ConHead
    c, [NamedArg (Pattern' a)]
    args)
        DefP PatternInfo
    o QName
    q [NamedArg (Pattern' a)]
    args   -> (QName -> m) -> (QName, [NamedArg (Pattern' a)]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (QName
    q, [NamedArg (Pattern' a)]
    args)
        ProjP ProjOrigin
    _ QName
    f       -> (QName -> m) -> QName -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg QName
    f
        IApplyP PatternInfo
    _ Term
    t Term
    u a
    _ -> (QName -> m) -> (Term, Term) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Term
    t, Term
    u)

    instance NamesIn a => NamesIn (Type' a) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Type' a -> m
    namesIn' QName -> m
    sg (El Sort
    s a
    t) = (QName -> m) -> (Sort, a) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Sort
    s, a
    t)

    instance NamesIn Sort where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Sort -> m
    namesIn' QName -> m
    sg = \case
        Type Level' Term
    l      -> (QName -> m) -> Level' Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Level' Term
    l
        Prop Level' Term
    l      -> (QName -> m) -> Level' Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Level' Term
    l
        Inf IsFibrant
    _ Integer
    _     -> m
    forall a. Monoid a => a
    mempty
        SSet Level' Term
    l      -> (QName -> m) -> Level' Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Level' Term
    l
        Sort
    SizeUniv    -> m
    forall a. Monoid a => a
    mempty
        Sort
    LockUniv    -> m
    forall a. Monoid a => a
    mempty
        PiSort Dom' Term Term
    a Sort
    b Abs Sort
    c  -> (QName -> m) -> (Dom' Term Term, Sort, Abs Sort) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Dom' Term Term
    a, Sort
    b, Abs Sort
    c)
        FunSort Sort
    a Sort
    b -> (QName -> m) -> (Sort, Sort) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Sort
    a, Sort
    b)
        UnivSort Sort
    a  -> (QName -> m) -> Sort -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Sort
    a
        MetaS MetaId
    _ [Elim' Term]
    es  -> (QName -> m) -> [Elim' Term] -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg [Elim' Term]
    es
        DefS QName
    d [Elim' Term]
    es   -> (QName -> m) -> (QName, [Elim' Term]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (QName
    d, [Elim' Term]
    es)
        DummyS{}    -> m
    forall a. Monoid a => a
    mempty

    instance NamesIn Term where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Term -> m
    namesIn' QName -> m
    sg = \case
        Var Int
    _ [Elim' Term]
    args   -> (QName -> m) -> [Elim' Term] -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg [Elim' Term]
    args
        Lam ArgInfo
    _ Abs Term
    b      -> (QName -> m) -> Abs Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Abs Term
    b
        Lit Literal
    l        -> (QName -> m) -> Literal -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Literal
    l
        Def QName
    f [Elim' Term]
    args   -> (QName -> m) -> (QName, [Elim' Term]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (QName
    f, [Elim' Term]
    args)
        Con ConHead
    c ConInfo
    _ [Elim' Term]
    args -> (QName -> m) -> (ConHead, [Elim' Term]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (ConHead
    c, [Elim' Term]
    args)
        Pi Dom' Term Type
    a Abs Type
    b       -> (QName -> m) -> (Dom' Term Type, Abs Type) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (Dom' Term Type
    a, Abs Type
    b)
        Sort Sort
    s       -> (QName -> m) -> Sort -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Sort
    s
        Level Level' Term
    l      -> (QName -> m) -> Level' Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Level' Term
    l
        MetaV MetaId
    _ [Elim' Term]
    args -> (QName -> m) -> [Elim' Term] -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg [Elim' Term]
    args
        DontCare Term
    v   -> (QName -> m) -> Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Term
    v
        Dummy{}      -> m
    forall a. Monoid a => a
    mempty

    instance NamesIn Level where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Level' Term -> m
    namesIn' QName -> m
    sg (Max Integer
    _ [PlusLevel' Term]
    ls) = (QName -> m) -> [PlusLevel' Term] -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg [PlusLevel' Term]
    ls

    instance NamesIn PlusLevel where
      namesIn' :: forall m. Monoid m => (QName -> m) -> PlusLevel' Term -> m
    namesIn' QName -> m
    sg (Plus Integer
    _ Term
    l) = (QName -> m) -> Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Term
    l

    -- For QName literals!
    instance NamesIn Literal where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Literal -> m
    namesIn' QName -> m
    sg = \case
        LitNat{}      -> m
    forall a. Monoid a => a
    mempty
        LitWord64{}   -> m
    forall a. Monoid a => a
    mempty
        LitString{}   -> m
    forall a. Monoid a => a
    mempty
        LitChar{}     -> m
    forall a. Monoid a => a
    mempty
        LitFloat{}    -> m
    forall a. Monoid a => a
    mempty
        LitQName    QName
    x -> (QName -> m) -> QName -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg QName
    x
        LitMeta{}     -> m
    forall a. Monoid a => a
    mempty

    instance NamesIn a => NamesIn (Elim' a) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Elim' a -> m
    namesIn' QName -> m
    sg (Apply Arg a
    arg)      = (QName -> m) -> Arg a -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Arg a
    arg
      namesIn' QName -> m
    sg (Proj ProjOrigin
    _ QName
    f)       = (QName -> m) -> QName -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg QName
    f
      namesIn' QName -> m
    sg (IApply a
    x a
    y a
    arg) = (QName -> m) -> (a, a, a) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (a
    x, a
    y, a
    arg)

    instance NamesIn DisplayForm where
      namesIn' :: forall m. Monoid m => (QName -> m) -> DisplayForm -> m
    namesIn' QName -> m
    sg (Display Int
    _ [Elim' Term]
    ps DisplayTerm
    v) = (QName -> m) -> ([Elim' Term], DisplayTerm) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg ([Elim' Term]
    ps, DisplayTerm
    v)

    instance NamesIn DisplayTerm where
      namesIn' :: forall m. Monoid m => (QName -> m) -> DisplayTerm -> m
    namesIn' QName -> m
    sg = \case
        DWithApp DisplayTerm
    v [DisplayTerm]
    us [Elim' Term]
    es -> (QName -> m) -> (DisplayTerm, [DisplayTerm], [Elim' Term]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (DisplayTerm
    v, [DisplayTerm]
    us, [Elim' Term]
    es)
        DCon ConHead
    c ConInfo
    _ [Arg DisplayTerm]
    vs      -> (QName -> m) -> (ConHead, [Arg DisplayTerm]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (ConHead
    c, [Arg DisplayTerm]
    vs)
        DDef QName
    f [Elim' DisplayTerm]
    es        -> (QName -> m) -> (QName, [Elim' DisplayTerm]) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (QName
    f, [Elim' DisplayTerm]
    es)
        DDot Term
    v           -> (QName -> m) -> Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Term
    v
        DTerm Term
    v          -> (QName -> m) -> Term -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Term
    v

    -- Pattern synonym stuff --

    newtype PSyn = PSyn A.PatternSynDefn
    instance NamesIn PSyn where
      namesIn' :: forall m. Monoid m => (QName -> m) -> PSyn -> m
    namesIn' QName -> m
    sg (PSyn ([Arg Name]
    _args, Pattern' Void
    p)) = (QName -> m) -> Pattern' Void -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Pattern' Void
    p

    instance NamesIn (A.Pattern' a) where
      namesIn' :: forall m. Monoid m => (QName -> m) -> Pattern' a -> m
    namesIn' QName -> m
    sg = \case
        A.VarP{}               -> m
    forall a. Monoid a => a
    mempty
        A.ConP ConPatInfo
    _ AmbiguousQName
    c NAPs a
    args        -> (QName -> m) -> (AmbiguousQName, NAPs a) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (AmbiguousQName
    c, NAPs a
    args)
        A.ProjP PatInfo
    _ ProjOrigin
    _ AmbiguousQName
    d          -> (QName -> m) -> AmbiguousQName -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg AmbiguousQName
    d
        A.DefP PatInfo
    _ AmbiguousQName
    f NAPs a
    args        -> (QName -> m) -> (AmbiguousQName, NAPs a) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (AmbiguousQName
    f, NAPs a
    args)
        A.WildP{}              -> m
    forall a. Monoid a => a
    mempty
        A.AsP PatInfo
    _ BindName
    _ Pattern' a
    p            -> (QName -> m) -> Pattern' a -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Pattern' a
    p
        A.AbsurdP{}            -> m
    forall a. Monoid a => a
    mempty
        A.LitP PatInfo
    _ Literal
    l             -> (QName -> m) -> Literal -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Literal
    l
        A.PatternSynP PatInfo
    _ AmbiguousQName
    c NAPs a
    args -> (QName -> m) -> (AmbiguousQName, NAPs a) -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg (AmbiguousQName
    c, NAPs a
    args)
        A.RecP PatInfo
    _ [FieldAssignment' (Pattern' a)]
    fs            -> (QName -> m) -> [FieldAssignment' (Pattern' a)] -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg [FieldAssignment' (Pattern' a)]
    fs
        A.DotP{}               -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__    -- Dot patterns are not allowed in pattern synonyms
        A.EqualP{}             -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__    -- Andrea: should we allow these in pattern synonyms?
        A.WithP PatInfo
    _ Pattern' a
    p            -> (QName -> m) -> Pattern' a -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg Pattern' a
    p
        A.AnnP PatInfo
    _ a
    a Pattern' a
    p           -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__    -- Type annotations are not (yet) allowed in pattern synonyms

    instance NamesIn AmbiguousQName where
      namesIn' :: forall m. Monoid m => (QName -> m) -> AmbiguousQName -> m
    namesIn' QName -> m
    sg (AmbQ List1 QName
    cs) = (QName -> m) -> List1 QName -> m
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    sg List1 QName
    cs