    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Extract all names and meta-variables from things.

    module Agda.Syntax.Internal.Names where

    import Data.HashMap.Strict (HashMap)
    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.Syntax.Treeless

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

    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Singleton
    import Agda.Utils.Impossible

    -- | Some or all of the 'QName's that can be found in the given thing.

    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

    -- | Some or all of the 'QName's that can be found in the given thing.

    namesIn' :: (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' :: forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> m
    f = (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' ((QName -> m) -> (MetaId -> m) -> Either QName MetaId -> m
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either QName -> m
    f MetaId -> m
    forall a. Monoid a => a
    mempty)

    -- | Some or all of the meta-variables that can be found in the given
    -- thing.

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

    -- | Some or all of the meta-variables that can be found in the given
    -- thing.

    -- TODO: Does this function make
    -- Agda.Syntax.Internal.MetaVars.allMetas superfluous? Maybe not,
    -- allMetas ignores the first argument of PiSort.

    metasIn' :: (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m
    metasIn' :: forall a m. (NamesIn a, Monoid m) => (MetaId -> m) -> a -> m
    metasIn' MetaId -> m
    f = (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' ((QName -> m) -> (MetaId -> m) -> Either QName MetaId -> m
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either QName -> m
    forall a. Monoid a => a
    mempty MetaId -> m
    f)

    -- | Some or all of the names and meta-variables that can be found in
    -- the given thing.

    namesAndMetasIn ::
      (NamesIn a, Collection QName m1, Collection MetaId m2) =>
      a -> (m1, m2)
    namesAndMetasIn :: forall a m1 m2.
    (NamesIn a, Collection QName m1, Collection MetaId m2) =>
    a -> (m1, m2)
    namesAndMetasIn =
      (Either QName MetaId -> (m1, m2)) -> a -> (m1, m2)
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn'
        ((QName -> (m1, m2))
    -> (MetaId -> (m1, m2)) -> Either QName MetaId -> (m1, m2)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (\QName
    x -> (QName -> m1
    forall el coll. Singleton el coll => el -> coll
    singleton QName
    x, m2
    forall a. Monoid a => a
    mempty))
                (\MetaId
    m -> (m1
    forall a. Monoid a => a
    mempty, MetaId -> m2
    forall el coll. Singleton el coll => el -> coll
    singleton MetaId
    m)))

    class NamesIn a where
      -- | Some or all of the names and meta-variables that can be found
      -- in the given thing.
      namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> a -> m

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

    -- Generic collections
    instance NamesIn a => NamesIn (Maybe a)
    instance NamesIn a => NamesIn (Strict.Maybe a)
    instance NamesIn a => NamesIn [a]
    instance NamesIn a => NamesIn (List1 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 (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)

    instance (NamesIn a, NamesIn b) => NamesIn (Dom' a b) where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Dom' a b -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Dom ArgInfo
    _ Maybe NamedName
    _ Bool
    _ Maybe a
    t b
    e) =
        m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend ((Either QName MetaId -> m) -> Maybe a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Maybe a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Maybe a
    t) ((Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg b
    e)

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

    -- Tuples

    instance (NamesIn a, NamesIn b) => NamesIn (a, b) where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> (a, b) -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (a
    x, b
    y) =
        (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg a
    x m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg b
    y
      {-# INLINE namesAndMetasIn' #-}

    instance (NamesIn a, NamesIn b, NamesIn c) => NamesIn (a, b, c) where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> (a, b, c) -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (a
    x, b
    y, c
    z) =
        (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg a
    x m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg b
    y m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> c -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> c -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg c
    z
      {-# INLINE namesAndMetasIn' #-}

    instance (NamesIn a, NamesIn b, NamesIn c, NamesIn d) => NamesIn (a, b, c, d) where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (a, b, c, d) -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (a
    x, b
    y, c
    z, d
    u) =
        (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg a
    x m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg b
    y m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> c -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> c -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg c
    z m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> d -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> d -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg d
    u
      {-# INLINE namesAndMetasIn' #-}

    instance
      (NamesIn a, NamesIn b, NamesIn c, NamesIn d, NamesIn e) =>
      NamesIn (a, b, c, d, e) where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (a, b, c, d, e) -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (a
    x, b
    y, c
    z, d
    u, e
    v) =
        (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg a
    x m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg b
    y m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> c -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> c -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg c
    z m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> d -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> d -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg d
    u
        m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> e -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> e -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg e
    v
      {-# INLINE namesAndMetasIn' #-}

    instance
      (NamesIn a, NamesIn b, NamesIn c, NamesIn d, NamesIn e, NamesIn f) =>
      NamesIn (a, b, c, d, e, f) where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (a, b, c, d, e, f) -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (a
    x, b
    y, c
    z, d
    u, e
    v, f
    w) =
        (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg a
    x m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg b
    y m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> c -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> c -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg c
    z m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> d -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> d -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg d
    u
        m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> e -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> e -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg e
    v m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Either QName MetaId -> m) -> f -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> f -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg f
    w
      {-# INLINE namesAndMetasIn' #-}

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

    -- Base cases

    instance NamesIn QName where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg QName
    x = Either QName MetaId -> m
    sg (QName -> Either QName MetaId
    forall a b. a -> Either a b
    Left QName
    x)  -- interesting case!

    instance NamesIn MetaId where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> MetaId -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg MetaId
    x = Either QName MetaId -> m
    sg (MetaId -> Either QName MetaId
    forall a b. b -> Either a b
    Right MetaId
    x)

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

    instance NamesIn Bool where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Bool -> m
    namesAndMetasIn' Either QName MetaId -> m
    _ Bool
    _ = m
    forall a. Monoid a => a
    mempty

    -- Andreas, 2017-07-27
    -- In the following clauses, the choice of fields is not obvious
    -- to the reader.  Please comment on the choices.

    instance NamesIn Definition where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Definition -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg
        (Defn ArgInfo
    _ QName
    _ Type
    t [Polarity]
    _ [Occurrence]
    _ [Maybe Name]
    _ [LocalDisplayForm]
    disp MutualId
    _ CompiledRepresentation
    _ Maybe InstanceInfo
    _ Bool
    _ Set QName
    _ Bool
    _ Bool
    _ Bool
    _ Blocked_
    _ Language
    _ Defn
    def) =
        (Either QName MetaId -> m) -> (Type, Defn, [LocalDisplayForm]) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (Type, Defn, [LocalDisplayForm]) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Type
    t, Defn
    def, [LocalDisplayForm]
    disp)

    instance NamesIn Defn where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Defn -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        Axiom Bool
    _            -> m
    forall a. Monoid a => a
    mempty
        DataOrRecSig Int
    _     -> m
    forall a. Monoid a => a
    mempty
        GeneralizableVar NumGeneralizableArgs
    _ -> m
    forall a. Monoid a => a
    mempty
        PrimitiveSort BuiltinSort
    _ Sort
    s  -> (Either QName MetaId -> m) -> Sort -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Sort -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Sort
    s
        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 [Clause]
    cl Maybe CompiledClauses
    cc Maybe SplitTree
    _ Maybe Compiled
    _ [Clause]
    _ FunctionInverse
    _ Maybe [QName]
    _ Either ProjectionLikenessMissing Projection
    _ SmallSet FunctionFlag
    _ Maybe Bool
    _ Maybe ExtLamInfo
    el Maybe QName
    _ Maybe QName
    _ IsOpaque
    _
          -> (Either QName MetaId -> m)
    -> ([Clause], Maybe CompiledClauses, Maybe ExtLamInfo) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> ([Clause], Maybe CompiledClauses, Maybe ExtLamInfo) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg ([Clause]
    cl, Maybe CompiledClauses
    cc, Maybe ExtLamInfo
    el)
        Datatype Int
    _ Int
    _ Maybe Clause
    cl [QName]
    cs Sort
    s Maybe [QName]
    _ IsAbstract
    _ [QName]
    _ Maybe QName
    trX Maybe QName
    trD
          -> (Either QName MetaId -> m)
    -> (Maybe Clause, [QName], Sort, Maybe QName, Maybe QName) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> (Maybe Clause, [QName], Sort, Maybe QName, Maybe QName) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Maybe Clause
    cl, [QName]
    cs, Sort
    s, Maybe QName
    trX, Maybe QName
    trD)
        Record Int
    _ Maybe Clause
    cl ConHead
    c Bool
    _ [Dom QName]
    fs Telescope
    recTel Maybe [QName]
    _ EtaEquality
    _ PatternOrCopattern
    _ Maybe Induction
    _ Maybe Bool
    _ IsAbstract
    _ CompKit
    comp
          -> (Either QName MetaId -> m)
    -> (Maybe Clause, ConHead, [Dom QName], Telescope, CompKit) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> (Maybe Clause, ConHead, [Dom QName], Telescope, CompKit) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Maybe Clause
    cl, ConHead
    c, [Dom QName]
    fs, Telescope
    recTel, CompKit
    comp)
        Constructor Int
    _ Int
    _ ConHead
    c QName
    d IsAbstract
    _ CompKit
    kit Maybe [QName]
    fs [IsForced]
    _ Maybe [Bool]
    _ Bool
    _ Bool
    _
          -> (Either QName MetaId -> m)
    -> (ConHead, QName, CompKit, Maybe [QName]) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> (ConHead, QName, CompKit, Maybe [QName]) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (ConHead
    c, QName
    d, CompKit
    kit, Maybe [QName]
    fs)
        Primitive IsAbstract
    _ PrimitiveId
    _ [Clause]
    cl FunctionInverse
    _ Maybe CompiledClauses
    cc IsOpaque
    _
          -> (Either QName MetaId -> m)
    -> ([Clause], Maybe CompiledClauses) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> ([Clause], Maybe CompiledClauses) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg ([Clause]
    cl, Maybe CompiledClauses
    cc)

    instance NamesIn Clause where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Clause -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Clause Range
    _ Range
    _ Telescope
    tel NAPs
    ps Maybe Term
    b Maybe (Arg Type)
    t Catchall
    _ Maybe Bool
    _ Maybe Bool
    _ ExpandedEllipsis
    _ Maybe ModuleName
    _) =
        (Either QName MetaId -> m)
    -> (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> (Telescope, NAPs, Maybe Term, Maybe (Arg Type)) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Telescope
    tel, NAPs
    ps, Maybe Term
    b, Maybe (Arg Type)
    t)

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

    -- Andreas, 2017-07-27
    -- Why ignoring the litBranches?
    instance NamesIn a => NamesIn (Case a) where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Case a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Branches Bool
    _ Map QName (WithArity a)
    bs Maybe (ConHead, WithArity a)
    _ Map Literal a
    _ Maybe a
    c Maybe Bool
    _ Bool
    _) =
        (Either QName MetaId -> m)
    -> (Map QName (WithArity a), Maybe a) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> (Map QName (WithArity a), Maybe a) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Map QName (WithArity a)
    bs, Maybe a
    c)

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

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

    instance NamesIn Sort where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Sort -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        Univ Univ
    _ Level' Term
    l    -> (Either QName MetaId -> m) -> Level' Term -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Level' Term -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Level' Term
    l
        Inf Univ
    _ Integer
    _     -> m
    forall a. Monoid a => a
    mempty
        Sort
    SizeUniv    -> m
    forall a. Monoid a => a
    mempty
        Sort
    LockUniv    -> m
    forall a. Monoid a => a
    mempty
        Sort
    LevelUniv   -> m
    forall a. Monoid a => a
    mempty
        Sort
    IntervalUniv -> m
    forall a. Monoid a => a
    mempty
        PiSort Dom' Term Term
    a Sort
    b Abs Sort
    c  -> (Either QName MetaId -> m) -> (Dom' Term Term, Sort, Abs Sort) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (Dom' Term Term, Sort, Abs Sort) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Dom' Term Term
    a, Sort
    b, Abs Sort
    c)
        FunSort Sort
    a Sort
    b -> (Either QName MetaId -> m) -> (Sort, Sort) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (Sort, Sort) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Sort
    a, Sort
    b)
        UnivSort Sort
    a  -> (Either QName MetaId -> m) -> Sort -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Sort -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Sort
    a
        MetaS MetaId
    x [Elim' Term]
    es  -> (Either QName MetaId -> m) -> (MetaId, [Elim' Term]) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (MetaId, [Elim' Term]) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (MetaId
    x, [Elim' Term]
    es)
        DefS QName
    d [Elim' Term]
    es   -> (Either QName MetaId -> m) -> (QName, [Elim' Term]) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (QName, [Elim' Term]) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (QName
    d, [Elim' Term]
    es)
        DummyS ArgName
    _    -> m
    forall a. Monoid a => a
    mempty

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

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

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

    -- For QName and Meta literals!
    instance NamesIn Literal where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Literal -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        LitNat Integer
    _    -> m
    forall a. Monoid a => a
    mempty
        LitWord64 Word64
    _ -> m
    forall a. Monoid a => a
    mempty
        LitString Text
    _ -> m
    forall a. Monoid a => a
    mempty
        LitChar Char
    _   -> m
    forall a. Monoid a => a
    mempty
        LitFloat Double
    _  -> m
    forall a. Monoid a => a
    mempty
        LitQName QName
    x  -> (Either QName MetaId -> m) -> QName -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg QName
    x
        LitMeta TopLevelModuleName' Range
    _ MetaId
    m -> (Either QName MetaId -> m) -> MetaId -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> MetaId -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg MetaId
    m

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

    instance NamesIn a => NamesIn (Substitution' a) where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Substitution' a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        Substitution' a
    IdS              -> m
    forall a. Monoid a => a
    mempty
        EmptyS Impossible
    _         -> m
    forall a. Monoid a => a
    mempty
        a
    t :# Substitution' a
    s           -> (Either QName MetaId -> m) -> (a, Substitution' a) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (a, Substitution' a) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (a
    t, Substitution' a
    s)
        Strengthen Impossible
    _ Int
    _ Substitution' a
    s -> (Either QName MetaId -> m) -> Substitution' a -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Substitution' a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Substitution' a
    s
        Wk Int
    _ Substitution' a
    s           -> (Either QName MetaId -> m) -> Substitution' a -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Substitution' a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Substitution' a
    s
        Lift Int
    _ Substitution' a
    s         -> (Either QName MetaId -> m) -> Substitution' a -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Substitution' a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Substitution' a
    s

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

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

    instance NamesIn a => NamesIn (Builtin a) where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Builtin a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        Builtin Term
    t -> (Either QName MetaId -> m) -> Term -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Term -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Term
    t
        Prim a
    x    -> (Either QName MetaId -> m) -> a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg a
    x
        BuiltinRewriteRelations Set QName
    xs -> (Either QName MetaId -> m) -> Set QName -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Set QName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Set QName
    xs

    -- | Note that the 'primFunImplementation' is skipped.
    instance NamesIn PrimFun where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> PrimFun -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        PrimFun QName
    x Int
    _ [Occurrence]
    _ [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    _ -> (Either QName MetaId -> m) -> QName -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg QName
    x

    instance NamesIn Section where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Section -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        Section Telescope
    tel -> (Either QName MetaId -> m) -> Telescope -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Telescope -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Telescope
    tel

    instance NamesIn NLPat where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> NLPat -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        PVar Int
    _ [Arg Int]
    _      -> m
    forall a. Monoid a => a
    mempty
        PDef QName
    a PElims
    b      -> (Either QName MetaId -> m) -> (QName, PElims) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (QName, PElims) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (QName
    a, PElims
    b)
        PLam ArgInfo
    _ Abs NLPat
    a      -> (Either QName MetaId -> m) -> Abs NLPat -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Abs NLPat -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Abs NLPat
    a
        PPi Dom NLPType
    a Abs NLPType
    b       -> (Either QName MetaId -> m) -> (Dom NLPType, Abs NLPType) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (Dom NLPType, Abs NLPType) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Dom NLPType
    a, Abs NLPType
    b)
        PSort NLPSort
    a       -> (Either QName MetaId -> m) -> NLPSort -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> NLPSort -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg NLPSort
    a
        PBoundVar Int
    _ PElims
    a -> (Either QName MetaId -> m) -> PElims -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> PElims -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg PElims
    a
        PTerm Term
    a       -> (Either QName MetaId -> m) -> Term -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Term -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Term
    a

    instance NamesIn NLPType where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> NLPType -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        NLPType NLPSort
    a NLPat
    b -> (Either QName MetaId -> m) -> (NLPSort, NLPat) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (NLPSort, NLPat) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (NLPSort
    a, NLPat
    b)

    instance NamesIn NLPSort where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> NLPSort -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        PUniv Univ
    _ NLPat
    a     -> (Either QName MetaId -> m) -> NLPat -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> NLPat -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg NLPat
    a
        PInf Univ
    _ Integer
    _      -> m
    forall a. Monoid a => a
    mempty
        NLPSort
    PSizeUniv     -> m
    forall a. Monoid a => a
    mempty
        NLPSort
    PLockUniv     -> m
    forall a. Monoid a => a
    mempty
        NLPSort
    PLevelUniv    -> m
    forall a. Monoid a => a
    mempty
        NLPSort
    PIntervalUniv -> m
    forall a. Monoid a => a
    mempty

    instance NamesIn RewriteRule where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> RewriteRule -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        RewriteRule QName
    a Telescope
    b QName
    c PElims
    d Term
    e Type
    f Bool
    _ TopLevelModuleName' Range
    _ ->
          (Either QName MetaId -> m)
    -> (QName, Telescope, QName, PElims, Term, Type) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m)
    -> (QName, Telescope, QName, PElims, Term, Type) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (QName
    a, Telescope
    b, QName
    c, PElims
    d, Term
    e, Type
    f)

    instance (NamesIn a, NamesIn b) => NamesIn (HashMap a b) where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> HashMap a b -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg HashMap a b
    map = (b -> m) -> HashMap a b -> m
    forall m a. Monoid m => (a -> m) -> HashMap a a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((Either QName MetaId -> m) -> b -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> b -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg) HashMap a b
    map

    instance NamesIn System where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> System -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (System Telescope
    tel [(Face, Term)]
    cs) = (Either QName MetaId -> m) -> (Telescope, [(Face, Term)]) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (Telescope, [(Face, Term)]) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Telescope
    tel, [(Face, Term)]
    cs)

    instance NamesIn ExtLamInfo where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> ExtLamInfo -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (ExtLamInfo ModuleName
    _ Bool
    _ Maybe System
    s) = (Either QName MetaId -> m) -> Maybe System -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Maybe System -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Maybe System
    s

    instance NamesIn a => NamesIn (FunctionInverse' a) where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> FunctionInverse' a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        FunctionInverse' a
    NotInjective -> m
    forall a. Monoid a => a
    mempty
        Inverse InversionMap a
    m  -> (Either QName MetaId -> m) -> InversionMap a -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> InversionMap a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg InversionMap a
    m

    instance NamesIn TTerm where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        TVar Int
    _         -> m
    forall a. Monoid a => a
    mempty
        TPrim TPrim
    _        -> m
    forall a. Monoid a => a
    mempty
        TDef QName
    x         -> (Either QName MetaId -> m) -> QName -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg QName
    x
        TApp TTerm
    t Args
    xs      -> (Either QName MetaId -> m) -> (TTerm, Args) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (TTerm, Args) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (TTerm
    t, Args
    xs)
        TLam TTerm
    t         -> (Either QName MetaId -> m) -> TTerm -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg TTerm
    t
        TLit Literal
    l         -> (Either QName MetaId -> m) -> Literal -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Literal -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Literal
    l
        TCon QName
    x         -> (Either QName MetaId -> m) -> QName -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg QName
    x
        TLet TTerm
    t1 TTerm
    t2     -> (Either QName MetaId -> m) -> (TTerm, TTerm) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (TTerm, TTerm) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (TTerm
    t1, TTerm
    t2)
        TCase Int
    _ CaseInfo
    c TTerm
    t [TAlt]
    ts -> (Either QName MetaId -> m) -> (CaseInfo, TTerm, [TAlt]) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (CaseInfo, TTerm, [TAlt]) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (CaseInfo
    c, TTerm
    t, [TAlt]
    ts)
        TTerm
    TUnit          -> m
    forall a. Monoid a => a
    mempty
        TTerm
    TSort          -> m
    forall a. Monoid a => a
    mempty
        TTerm
    TErased        -> m
    forall a. Monoid a => a
    mempty
        TCoerce TTerm
    t      -> (Either QName MetaId -> m) -> TTerm -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg TTerm
    t
        TError TError
    _       -> m
    forall a. Monoid a => a
    mempty

    instance NamesIn TAlt where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> TAlt -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        TACon QName
    x Int
    _ TTerm
    t   -> (Either QName MetaId -> m) -> (QName, TTerm) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (QName, TTerm) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (QName
    x, TTerm
    t)
        TAGuard TTerm
    t1 TTerm
    t2 -> (Either QName MetaId -> m) -> (TTerm, TTerm) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (TTerm, TTerm) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (TTerm
    t1, TTerm
    t2)
        TALit Literal
    l TTerm
    t     -> (Either QName MetaId -> m) -> (Literal, TTerm) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (Literal, TTerm) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Literal
    l, TTerm
    t)

    instance NamesIn CaseType where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> CaseType -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        CTData QName
    x   -> (Either QName MetaId -> m) -> QName -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> QName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg QName
    x
        CaseType
    CTNat      -> m
    forall a. Monoid a => a
    mempty
        CaseType
    CTInt      -> m
    forall a. Monoid a => a
    mempty
        CaseType
    CTChar     -> m
    forall a. Monoid a => a
    mempty
        CaseType
    CTString   -> m
    forall a. Monoid a => a
    mempty
        CaseType
    CTFloat    -> m
    forall a. Monoid a => a
    mempty
        CaseType
    CTQName    -> m
    forall a. Monoid a => a
    mempty

    instance NamesIn CaseInfo where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> CaseInfo -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (CaseInfo Bool
    _ Erased
    _ CaseType
    t) = (Either QName MetaId -> m) -> CaseType -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> CaseType -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg CaseType
    t

    instance NamesIn Compiled where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Compiled -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (Compiled TTerm
    t Maybe [ArgUsage]
    _) = (Either QName MetaId -> m) -> TTerm -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> TTerm -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg TTerm
    t

    -- Pattern synonym stuff --

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

    instance NamesIn ConPatternInfo where
      namesAndMetasIn' :: forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> ConPatternInfo -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (ConPatternInfo PatternInfo
    _ Bool
    _ Bool
    _ Maybe (Arg Type)
    ty Bool
    _) = (Either QName MetaId -> m) -> Maybe (Arg Type) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> Maybe (Arg Type) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Maybe (Arg Type)
    ty

    instance NamesIn (A.Pattern' a) where
      namesAndMetasIn' :: forall m. Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg = \case
        A.VarP BindName
    _               -> m
    forall a. Monoid a => a
    mempty
        A.ConP ConPatInfo
    _ AmbiguousQName
    c NAPs a
    args        -> (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (AmbiguousQName
    c, NAPs a
    args)
        A.ProjP PatInfo
    _ ProjOrigin
    _ AmbiguousQName
    d          -> (Either QName MetaId -> m) -> AmbiguousQName -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> AmbiguousQName -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg AmbiguousQName
    d
        A.DefP PatInfo
    _ AmbiguousQName
    f NAPs a
    args        -> (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (AmbiguousQName
    f, NAPs a
    args)
        A.WildP PatInfo
    _              -> m
    forall a. Monoid a => a
    mempty
        A.AsP PatInfo
    _ BindName
    _ Pattern' a
    p            -> (Either QName MetaId -> m) -> Pattern' a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Pattern' a
    p
        A.AbsurdP PatInfo
    _            -> m
    forall a. Monoid a => a
    mempty
        A.LitP PatInfo
    _ Literal
    l             -> (Either QName MetaId -> m) -> Literal -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Literal -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Literal
    l
        A.PatternSynP PatInfo
    _ AmbiguousQName
    c NAPs a
    args -> (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> (AmbiguousQName, NAPs a) -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg (AmbiguousQName
    c, NAPs a
    args)
        A.RecP KwRange
    _ ConPatInfo
    _ [FieldAssignment' (Pattern' a)]
    fs          -> (Either QName MetaId -> m) -> [FieldAssignment' (Pattern' a)] -> m
    forall m.
    Monoid m =>
    (Either QName MetaId -> m) -> [FieldAssignment' (Pattern' a)] -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> 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            -> (Either QName MetaId -> m) -> Pattern' a -> m
    forall m. Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m
    forall a m.
    (NamesIn a, Monoid m) =>
    (Either QName MetaId -> m) -> a -> m
    namesAndMetasIn' Either QName MetaId -> m
    sg Pattern' a
    p

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