    {-# LANGUAGE CPP                   #-}
    {-# LANGUAGE DeriveDataTypeable    #-}
    {-# LANGUAGE TemplateHaskell       #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}

    {-| The abstract syntax. This is what you get after desugaring and scope
        analysis of the concrete syntax. The type checker works on abstract syntax,
        producing internal syntax ("Agda.Syntax.Internal").
    -}
    module Agda.Syntax.Abstract
        ( module Agda.Syntax.Abstract
        , module Agda.Syntax.Abstract.Name
        ) where

    import Prelude
    import Control.Arrow (first, second, (***))

    import Data.Foldable (Foldable)
    import qualified Data.Foldable as Fold
    import Data.Function (on)
    import Data.Map (Map)
    import Data.Maybe
    import Data.Sequence (Seq, (<|), (><))
    import qualified Data.Sequence as Seq
    import qualified Data.Set as Set
    import Data.Set (Set)
    import Data.Traversable
    import Data.Void

    import Data.Data (Data)
    import Data.Monoid (mappend)

    import Agda.Syntax.Concrete.Name (NumHoles(..))
    import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA, HoleContent'(..))
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Pretty ()

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Abstract.Name as A (QNamed)

    import qualified Agda.Syntax.Internal as I

    import Agda.Syntax.Common
    import Agda.Syntax.Info
    import Agda.Syntax.Fixity ( Fixity' )
    import Agda.Syntax.Literal
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base

    import Agda.TypeChecking.Positivity.Occurrence

    import Agda.Utils.Functor
    import Agda.Utils.Geniplate
    import Agda.Utils.Lens
    import Agda.Utils.NonemptyList
    import Agda.Utils.Pretty

    #include "undefined.h"
    import Agda.Utils.Impossible

    -- | A name in a binding position: we also compare the nameConcrete
    -- when comparing the binders for equality.
    --
    -- With @--caching@ on we compare abstract syntax to determine if we can
    -- reuse previous typechecking results: during that comparison two
    -- names can have the same nameId but be semantically different,
    -- e.g. in @{_ : A} -> ..@ vs. @{r : A} -> ..@.

    newtype BindName = BindName { unBind :: Name }
      deriving (Show, Data, HasRange, SetRange, KillRange)

    instance Eq BindName where
      (BindName n) == (BindName m)
        = ((==) `on` nameId) n m
          && ((==) `on` nameConcrete) n m

    instance Ord BindName where
      (BindName n) `compare` (BindName m)
        = (compare `on` nameId) n m
          `mappend` (compare `on` nameConcrete) n m

    type Args = [NamedArg Expr]

    -- | Expressions after scope checking (operators parsed, names resolved).
    data Expr
      = Var  Name                          -- ^ Bound variable.
      | Def  QName                         -- ^ Constant: axiom, function, data or record type.
      | Proj ProjOrigin AmbiguousQName     -- ^ Projection (overloaded).
      | Con  AmbiguousQName                -- ^ Constructor (overloaded).
      | PatternSyn AmbiguousQName          -- ^ Pattern synonym.
      | Macro QName                        -- ^ Macro.
      | Lit Literal                        -- ^ Literal.
      | QuestionMark MetaInfo InteractionId
        -- ^ Meta variable for interaction.
        --   The 'InteractionId' is usually identical with the
        --   'metaNumber' of 'MetaInfo'.
        --   However, if you want to print an interaction meta as
        --   just @?@ instead of @?n@, you should set the
        --   'metaNumber' to 'Nothing' while keeping the 'InteractionId'.
      | Underscore   MetaInfo
        -- ^ Meta variable for hidden argument (must be inferred locally).
      | Dot ExprInfo Expr                  -- ^ @.e@, for postfix projection.
      | App  AppInfo Expr (NamedArg Expr)  -- ^ Ordinary (binary) application.
      | WithApp ExprInfo Expr [Expr]       -- ^ With application.
      | Lam  ExprInfo LamBinding Expr      -- ^ @λ bs → e@.
      | AbsurdLam ExprInfo Hiding          -- ^ @λ()@ or @λ{}@.
      | ExtendedLam ExprInfo DefInfo QName [Clause]
      | Pi   ExprInfo Telescope Expr       -- ^ Dependent function space @Γ → A@.
      | Generalized (Set.Set QName) Expr   -- ^ Like a Pi, but the ordering is not known
      | Fun  ExprInfo (Arg Expr) Expr      -- ^ Non-dependent function space.
      | Set  ExprInfo Integer              -- ^ @Set@, @Set1@, @Set2@, ...
      | Prop ExprInfo Integer              -- ^ @Prop@, @Prop1@, @Prop2@, ...
      | Let  ExprInfo [LetBinding] Expr    -- ^ @let bs in e@.
      | ETel Telescope                     -- ^ Only used when printing telescopes.
      | Rec  ExprInfo RecordAssigns        -- ^ Record construction.
      | RecUpdate ExprInfo Expr Assigns    -- ^ Record update.
      | ScopedExpr ScopeInfo Expr          -- ^ Scope annotation.
      | QuoteGoal ExprInfo Name Expr       -- ^ Binds @Name@ to current type in @Expr@.
      | QuoteContext ExprInfo              -- ^ Returns the current context.
      | Quote ExprInfo                     -- ^ Quote an identifier 'QName'.
      | QuoteTerm ExprInfo                 -- ^ Quote a term.
      | Unquote ExprInfo                   -- ^ The splicing construct: unquote ...
      | Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]
                                           -- ^ @tactic e x1 .. xn | y1 | .. | yn@
      | DontCare Expr                      -- ^ For printing @DontCare@ from @Syntax.Internal@.
      deriving (Data, Show)

    -- | Smart constructor for Generalized
    generalized :: Set.Set QName -> Expr -> Expr
    generalized s e
        | Set.null s = e
        | otherwise = Generalized s e

    -- | Record field assignment @f = e@.
    type Assign  = FieldAssignment' Expr
    type Assigns = [Assign]
    type RecordAssign  = Either Assign ModuleName
    type RecordAssigns = [RecordAssign]

    -- | Is a type signature a `postulate' or a function signature?
    data Axiom
      = FunSig    -- ^ A function signature.
      | NoFunSig  -- ^ Not a function signature, i.e., a postulate (in user input)
                  --   or another (e.g. data/record) type signature (internally).
      deriving (Data, Eq, Ord, Show)

    -- | Renaming (generic).
    type Ren a = [(a, a)]

    data ScopeCopyInfo = ScopeCopyInfo
      { renModules :: Ren ModuleName
      , renNames   :: Ren QName }
      deriving (Eq, Show, Data)

    initCopyInfo :: ScopeCopyInfo
    initCopyInfo = ScopeCopyInfo
      { renModules = []
      , renNames   = []
      }

    instance Pretty ScopeCopyInfo where
      pretty i = vcat [ prRen "renModules =" (renModules i)
                      , prRen "renNames   =" (renNames i) ]
        where
          prRen s r = sep [ text s, nest 2 $ vcat (map pr r) ]
          pr (x, y) = pretty x <+> "->" <+> pretty y

    data Declaration
      = Axiom      Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr
        -- ^ Type signature (can be irrelevant, but not hidden).
        --
        -- The fourth argument contains an optional assignment of
        -- polarities to arguments.
      | Generalize (Set.Set QName) DefInfo ArgInfo QName Expr
        -- ^ First argument is set of generalizable variables used in the type.
      | Field      DefInfo QName (Arg Expr)              -- ^ record field
      | Primitive  DefInfo QName Expr                    -- ^ primitive function
      | Mutual     MutualInfo [Declaration]              -- ^ a bunch of mutually recursive definitions
      | Section    ModuleInfo ModuleName GeneralizeTelescope [Declaration]
      | Apply      ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
        -- ^ The @ImportDirective@ is for highlighting purposes.
      | Import     ModuleInfo ModuleName ImportDirective
        -- ^ The @ImportDirective@ is for highlighting purposes.
      | Pragma     Range      Pragma
      | Open       ModuleInfo ModuleName ImportDirective
        -- ^ only retained for highlighting purposes
      | FunDef     DefInfo QName Delayed [Clause] -- ^ sequence of function clauses
      | DataSig    DefInfo QName GeneralizeTelescope Expr -- ^ lone data signature
      | DataDef    DefInfo QName UniverseCheck DataDefParams [Constructor]
          -- ^ the 'LamBinding's are 'DomainFree' and bind the parameters of the datatype.
      | RecSig     DefInfo QName GeneralizeTelescope Expr -- ^ lone record signature
      | RecDef     DefInfo QName UniverseCheck (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) DataDefParams Expr [Declaration]
          -- ^ The 'LamBinding's are 'DomainFree' and bind the parameters of the datatype.
          --   The 'Expr' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Prop@,
          --   and the optional name is the constructor's name.
      | PatternSynDef QName [Arg Name] (Pattern' Void)
          -- ^ Only for highlighting purposes
      | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
      | UnquoteDef  [DefInfo] [QName] Expr
      | ScopedDecl ScopeInfo [Declaration]  -- ^ scope annotation
      deriving (Data, Show)

    class GetDefInfo a where
      getDefInfo :: a -> Maybe DefInfo

    instance GetDefInfo Declaration where
      getDefInfo (Axiom _ i _ _ _ _)    = Just i
      getDefInfo (Generalize _ i _ _ _) = Just i
      getDefInfo (Field i _ _)          = Just i
      getDefInfo (Primitive i _ _)      = Just i
      getDefInfo (ScopedDecl _ (d:_))   = getDefInfo d
      getDefInfo (FunDef i _ _ _)       = Just i
      getDefInfo (DataSig i _ _ _)      = Just i
      getDefInfo (DataDef i _ _ _ _)    = Just i
      getDefInfo (RecSig i _ _ _)       = Just i
      getDefInfo (RecDef i _ _ _ _ _ _ _ _) = Just i
      getDefInfo _ = Nothing

    type ImportDirective = ImportDirective' QName ModuleName
    type Renaming        = Renaming'        QName ModuleName
    type ImportedName    = ImportedName'    QName ModuleName

    data ModuleApplication
        = SectionApp Telescope ModuleName [NamedArg Expr]
          -- ^ @tel. M args@:  applies @M@ to @args@ and abstracts @tel@.
        | RecordModuleInstance ModuleName
          -- ^ @M {{...}}@
      deriving (Data, Show, Eq)

    data Pragma
      = OptionsPragma [String]
      | BuiltinPragma String ResolvedName
        -- ^ 'ResolvedName' is not 'UnknownName'.
        --   Name can be ambiguous e.g. for built-in constructors.
      | BuiltinNoDefPragma String QName
        -- ^ Builtins that do not come with a definition,
        --   but declare a name for an Agda concept.
      | RewritePragma QName
      | CompilePragma String QName String
      | StaticPragma QName
      | EtaPragma QName
        -- ^ For coinductive records, use pragma instead of regular
        --   @eta-equality@ definition (as it is might make Agda loop).
      | InjectivePragma QName
      | InlinePragma Bool QName -- INLINE or NOINLINE
      | DisplayPragma QName [NamedArg Pattern] Expr
      deriving (Data, Show, Eq)

    -- | Bindings that are valid in a @let@.
    data LetBinding
      = LetBind LetInfo ArgInfo BindName Expr Expr
        -- ^ @LetBind info rel name type defn@
      | LetPatBind LetInfo Pattern Expr
        -- ^ Irrefutable pattern binding.
      | LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
        -- ^ @LetApply mi newM (oldM args) renamings dir@.
        -- The @ImportDirective@ is for highlighting purposes.
      | LetOpen ModuleInfo ModuleName ImportDirective
        -- ^ only for highlighting and abstractToConcrete
      | LetDeclaredVariable BindName
        -- ^ Only used for highlighting. Refers to the first occurrence of
        -- @x@ in @let x : A; x = e@.
    --  | LetGeneralize DefInfo ArgInfo Expr
      deriving (Data, Show, Eq)

    -- | Only 'Axiom's.
    type TypeSignature  = Declaration
    type Constructor    = TypeSignature
    type Field          = TypeSignature

    -- | A lambda binding is either domain free or typed.
    data LamBinding
      = DomainFree (NamedArg BindName)  -- ^ . @x@ or @{x}@ or @.x@ or @{x = y}@
      | DomainFull TypedBinding         -- ^ . @(xs:e)@ or @{xs:e}@ or @(let Ds)@
      deriving (Data, Show, Eq)

    -- | A typed binding.  Appears in dependent function spaces, typed lambdas, and
    --   telescopes.  It might be tempting to simplify this to only bind a single
    --   name at a time, and translate, say, @(x y : A)@ to @(x : A)(y : A)@
    --   before type-checking.  However, this would be slightly problematic:
    --
    --     1. We would have to typecheck the type @A@ several times.
    --
    --     2. If @A@ contains a meta variable or hole, it would be duplicated
    --        by such a translation.
    --
    --   While 1. is only slightly inefficient, 2. would be an outright bug.
    --   Duplicating @A@ could not be done naively, we would have to make sure
    --   that the metas of the copy are aliases of the metas of the original.

    data TypedBinding
      = TBind Range [NamedArg BindName] Expr
        -- ^ As in telescope @(x y z : A)@ or type @(x y z : A) -> B@.
      | TLet Range [LetBinding]
        -- ^ E.g. @(let x = e)@ or @(let open M)@.
      deriving (Data, Show, Eq)

    type Telescope  = [TypedBinding]

    data GeneralizeTelescope = GeneralizeTel
      { generalizeTelVars :: Map QName Name
        -- ^ Maps generalize variables to the corresponding bound variable (to be
        --   introduced by the generalisation).
      , generalizeTel     :: Telescope }
      deriving (Data, Show, Eq)

    data DataDefParams = DataDefParams
      { dataDefGeneralizedParams :: Set Name
        -- ^ We don't yet know the position of generalized parameters from the data
        --   sig, so we keep these in a set on the side.
      , dataDefParams :: [LamBinding]
      }
      deriving (Data, Show, Eq)

    noDataDefParams :: DataDefParams
    noDataDefParams = DataDefParams Set.empty []

    -- | A user pattern together with an internal term that it should be equal to
    --   after splitting is complete.
    --   Special cases:
    --    * User pattern is a variable but internal term isn't:
    --      this will be turned into an as pattern.
    --    * User pattern is a dot pattern:
    --      this pattern won't trigger any splitting but will be checked
    --      for equality after all splitting is complete and as patterns have
    --      been bound.
    --    * User pattern is an absurd pattern:
    --      emptiness of the type will be checked after splitting is complete.
    data ProblemEq = ProblemEq
      { problemInPat :: Pattern
      , problemInst  :: I.Term
      , problemType  :: Dom I.Type
      } deriving (Data, Show)

    -- These are not relevant for caching purposes
    instance Eq ProblemEq where _ == _ = True

    -- | We could throw away @where@ clauses at this point and translate them to
    --   @let@. It's not obvious how to remember that the @let@ was really a
    --   @where@ clause though, so for the time being we keep it here.
    data Clause' lhs = Clause
      { clauseLHS        :: lhs
      , clauseStrippedPats :: [ProblemEq]
          -- ^ Only in with-clauses where we inherit some already checked patterns from the parent.
          --   These live in the context of the parent clause left-hand side.
      , clauseRHS        :: RHS
      , clauseWhereDecls :: WhereDeclarations
      , clauseCatchall   :: Bool
      } deriving (Data, Show, Functor, Foldable, Traversable, Eq)

    data WhereDeclarations = WhereDecls
      { whereModule :: Maybe ModuleName
      , whereDecls  :: [Declaration]
      } deriving (Data, Show, Eq)

    noWhereDecls :: WhereDeclarations
    noWhereDecls = WhereDecls Nothing []

    type Clause = Clause' LHS
    type SpineClause = Clause' SpineLHS

    data RHS
      = RHS
        { rhsExpr     :: Expr
        , rhsConcrete :: Maybe C.Expr
          -- ^ We store the original concrete expression in case
          --   we have to reproduce it during interactive case splitting.
          --   'Nothing' for internally generated rhss.
        }
      | AbsurdRHS
      | WithRHS QName [Expr] [Clause]
          -- ^ The 'QName' is the name of the with function.
      | RewriteRHS
        { rewriteExprs      :: [(QName, Expr)]
          -- ^ The 'QName's are the names of the generated with functions,
          --   one for each 'Expr'.
        , rewriteStrippedPats :: [ProblemEq]
          -- ^ The patterns stripped by with-desugaring. These are only present
          --   if this rewrite follows a with.
        , rewriteRHS        :: RHS
          -- ^ The RHS should not be another @RewriteRHS@.
        , rewriteWhereDecls :: WhereDeclarations
          -- ^ The where clauses are attached to the @RewriteRHS@ by
          ---  the scope checker (instead of to the clause).
        }
      deriving (Data, Show)

    -- | Ignore 'rhsConcrete' when comparing 'RHS's.
    instance Eq RHS where
      RHS e _          == RHS e' _            = e == e'
      AbsurdRHS        == AbsurdRHS           = True
      WithRHS a b c    == WithRHS a' b' c'    = and [ a == a', b == b', c == c' ]
      RewriteRHS a b c d == RewriteRHS a' b' c' d' = and [ a == a', b == b', c == c' , d == d' ]
      _                == _                   = False

    -- | The lhs of a clause in spine view (inside-out).
    --   Projection patterns are contained in @spLhsPats@,
    --   represented as @ProjP d@.
    data SpineLHS = SpineLHS
      { spLhsInfo     :: LHSInfo             -- ^ Range.
      , spLhsDefName  :: QName               -- ^ Name of function we are defining.
      , spLhsPats     :: [NamedArg Pattern]  -- ^ Elimination by pattern, projections, with-patterns.
      }
      deriving (Data, Show, Eq)

    -- | Ignore 'Range' when comparing 'LHS's.
    instance Eq LHS where
      LHS _ core == LHS _ core' = core == core'

    -- | The lhs of a clause in focused (projection-application) view (outside-in).
    --   Projection patters are represented as 'LHSProj's.
    data LHS = LHS
      { lhsInfo     :: LHSInfo               -- ^ Range.
      , lhsCore     :: LHSCore               -- ^ Copatterns.
      }
      deriving (Data, Show)

    -- | The lhs in projection-application and with-pattern view.
    --   Parameterised over the type @e@ of dot patterns.
    data LHSCore' e
        -- | The head applied to ordinary patterns.
      = LHSHead  { lhsDefName  :: QName
                     -- ^ Head @f@.
                 , lhsPats     :: [NamedArg (Pattern' e)]
                     -- ^ Applied to patterns @ps@.
                 }
        -- | Projection.
      | LHSProj  { lhsDestructor :: AmbiguousQName
                     -- ^ Record projection identifier.
                 , lhsFocus      :: NamedArg (LHSCore' e)
                     -- ^ Main argument of projection.
                 , lhsPats       :: [NamedArg (Pattern' e)]
                     -- ^ Further applied to patterns.
                 }
        -- | With patterns.
      | LHSWith  { lhsHead         :: LHSCore' e
                     -- ^ E.g. the 'LHSHead'.
                 , lhsWithPatterns :: [Pattern' e]
                     -- ^ Applied to with patterns @| p1 | ... | pn@.
                     --   These patterns are not prefixed with @WithP@!
                 , lhsPats         :: [NamedArg (Pattern' e)]
                     -- ^ Further applied to patterns.
                 }
      deriving (Data, Show, Functor, Foldable, Traversable, Eq)

    type LHSCore = LHSCore' Expr

    ---------------------------------------------------------------------------
    -- * Patterns
    ---------------------------------------------------------------------------

    -- | Parameterised over the type of dot patterns.
    data Pattern' e
      = VarP BindName
      | ConP ConPatInfo AmbiguousQName (NAPs e)
      | ProjP PatInfo ProjOrigin AmbiguousQName
        -- ^ Destructor pattern @d@.
      | DefP PatInfo AmbiguousQName (NAPs e)
        -- ^ Defined pattern: function definition @f ps@.
        --   It is also abused to convert destructor patterns into concrete syntax
        --   thus, we put AmbiguousQName here as well.
      | WildP PatInfo
        -- ^ Underscore pattern entered by user.
        --   Or generated at type checking for implicit arguments.
      | AsP PatInfo BindName (Pattern' e)
      | DotP PatInfo e
        -- ^ Dot pattern @.e@
      | AbsurdP PatInfo
      | LitP Literal
      | PatternSynP PatInfo AmbiguousQName (NAPs e)
      | RecP PatInfo [FieldAssignment' (Pattern' e)]
      | EqualP PatInfo [(e, e)]
      | WithP PatInfo (Pattern' e)  -- ^ @| p@, for with-patterns.
      deriving (Data, Show, Functor, Foldable, Traversable, Eq)

    type NAPs e   = [NamedArg (Pattern' e)]
    type Pattern  = Pattern' Expr
    type Patterns = [NamedArg Pattern]

    instance IsProjP (Pattern' e) where
      -- Andreas, 2018-06-19, issue #3130
      -- Do not interpret things like .(p) as projection pattern any more.
      -- maybePostfixProjP (DotP _ e)    = isProjP e <&> \ (_o, d) -> (ProjPostfix, d)
      isProjP (ProjP _ o d) = Just (o, d)
      isProjP _ = Nothing

    instance IsProjP Expr where
      isProjP (Proj o ds)      = Just (o, ds)
      isProjP (ScopedExpr _ e) = isProjP e
      isProjP _ = Nothing

    {--------------------------------------------------------------------------
        Things we parse but are not part of the Agda file syntax
     --------------------------------------------------------------------------}

    type HoleContent = C.HoleContent' Expr

    {--------------------------------------------------------------------------
        Instances
     --------------------------------------------------------------------------}

    -- | Does not compare 'ScopeInfo' fields.
    --   Does not distinguish between prefix and postfix projections.

    instance Eq Expr where
      ScopedExpr _ a1         == ScopedExpr _ a2         = a1 == a2

      Var a1                  == Var a2                  = a1 == a2
      Def a1                  == Def a2                  = a1 == a2
      Proj _ a1               == Proj _ a2               = a1 == a2
      Con a1                  == Con a2                  = a1 == a2
      PatternSyn a1           == PatternSyn a2           = a1 == a2
      Macro a1                == Macro a2                = a1 == a2
      Lit a1                  == Lit a2                  = a1 == a2
      QuestionMark a1 b1      == QuestionMark a2 b2      = (a1, b1) == (a2, b2)
      Underscore a1           == Underscore a2           = a1 == a2
      Dot r1 e1               == Dot r2 e2               = (r1, e1) == (r2, e2)
      App a1 b1 c1            == App a2 b2 c2            = (a1, b1, c1) == (a2, b2, c2)
      WithApp a1 b1 c1        == WithApp a2 b2 c2        = (a1, b1, c1) == (a2, b2, c2)
      Lam a1 b1 c1            == Lam a2 b2 c2            = (a1, b1, c1) == (a2, b2, c2)
      AbsurdLam a1 b1         == AbsurdLam a2 b2         = (a1, b1) == (a2, b2)
      ExtendedLam a1 b1 c1 d1 == ExtendedLam a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      Pi a1 b1 c1             == Pi a2 b2 c2             = (a1, b1, c1) == (a2, b2, c2)
      Generalized a1 b1       == Generalized a2 b2       = (a1, b1) == (a2, b2)
      Fun a1 b1 c1            == Fun a2 b2 c2            = (a1, b1, c1) == (a2, b2, c2)
      Set a1 b1               == Set a2 b2               = (a1, b1) == (a2, b2)
      Prop a1 b1              == Prop a2 b2              = (a1, b1) == (a2, b2)
      Let a1 b1 c1            == Let a2 b2 c2            = (a1, b1, c1) == (a2, b2, c2)
      ETel a1                 == ETel a2                 = a1 == a2
      Rec a1 b1               == Rec a2 b2               = (a1, b1) == (a2, b2)
      RecUpdate a1 b1 c1      == RecUpdate a2 b2 c2      = (a1, b1, c1) == (a2, b2, c2)
      QuoteGoal a1 b1 c1      == QuoteGoal a2 b2 c2      = (a1, b1, c1) == (a2, b2, c2)
      QuoteContext a1         == QuoteContext a2         = a1 == a2
      Quote a1                == Quote a2                = a1 == a2
      QuoteTerm a1            == QuoteTerm a2            = a1 == a2
      Unquote a1              == Unquote a2              = a1 == a2
      Tactic a1 b1 c1 d1      == Tactic a2 b2 c2 d2      = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      DontCare a1             == DontCare a2             = a1 == a2

      _                       == _                       = False

    -- | Does not compare 'ScopeInfo' fields.

    instance Eq Declaration where
      ScopedDecl _ a1                == ScopedDecl _ a2                = a1 == a2

      Axiom a1 b1 c1 d1 e1 f1        == Axiom a2 b2 c2 d2 e2 f2        = (a1, b1, c1, d1, e1, f1) == (a2, b2, c2, d2, e2, f2)
      Generalize a1 b1 c1 d1 e1      == Generalize a2 b2 c2 d2 e2      = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
      Field a1 b1 c1                 == Field a2 b2 c2                 = (a1, b1, c1) == (a2, b2, c2)
      Primitive a1 b1 c1             == Primitive a2 b2 c2             = (a1, b1, c1) == (a2, b2, c2)
      Mutual a1 b1                   == Mutual a2 b2                   = (a1, b1) == (a2, b2)
      Section a1 b1 c1 d1            == Section a2 b2 c2 d2            = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      Apply a1 b1 c1 d1 e1           == Apply a2 b2 c2 d2 e2           = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
      Import a1 b1 c1                == Import a2 b2 c2                = (a1, b1, c1) == (a2, b2, c2)
      Pragma a1 b1                   == Pragma a2 b2                   = (a1, b1) == (a2, b2)
      Open a1 b1 c1                  == Open a2 b2 c2                  = (a1, b1, c1) == (a2, b2, c2)
      FunDef a1 b1 c1 d1             == FunDef a2 b2 c2 d2             = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      DataSig a1 b1 c1 d1            == DataSig a2 b2 c2 d2            = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      DataDef a1 b1 c1 d1 e1         == DataDef a2 b2 c2 d2 e2         = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
      RecSig a1 b1 c1 d1             == RecSig a2 b2 c2 d2             = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      RecDef a1 b1 c1 d1 e1 f1 g1 h1 i1 == RecDef a2 b2 c2 d2 e2 f2 g2 h2 i2 = (a1, b1, c1, d1, e1, f1, g1, h1, i1) == (a2, b2, c2, d2, e2, f2, g2, h2, i2)
      PatternSynDef a1 b1 c1         == PatternSynDef a2 b2 c2         = (a1, b1, c1) == (a2, b2, c2)
      UnquoteDecl a1 b1 c1 d1        == UnquoteDecl a2 b2 c2 d2        = (a1, b1, c1, d1) == (a2, b2, c2, d2)
      UnquoteDef a1 b1 c1            == UnquoteDef a2 b2 c2            = (a1, b1, c1) == (a2, b2, c2)

      _                              == _                              = False

    instance Underscore Expr where
      underscore   = Underscore emptyMetaInfo
      isUnderscore = __IMPOSSIBLE__

    instance LensHiding LamBinding where
      getHiding   (DomainFree x)  = getHiding x
      getHiding   (DomainFull tb) = getHiding tb
      mapHiding f (DomainFree x)  = DomainFree $ mapHiding f x
      mapHiding f (DomainFull tb) = DomainFull $ mapHiding f tb

    instance LensHiding TypedBinding where
      getHiding (TBind _ (x : _) _) = getHiding x   -- Slightly dubious
      getHiding (TBind _ [] _)      = __IMPOSSIBLE__
      getHiding TLet{}              = mempty
      mapHiding f (TBind r xs e) = TBind r ((map . mapHiding) f xs) e
      mapHiding f b@TLet{}       = b

    instance HasRange LamBinding where
        getRange (DomainFree x) = getRange x
        getRange (DomainFull b) = getRange b

    instance HasRange TypedBinding where
        getRange (TBind r _ _) = r
        getRange (TLet r _)    = r

    instance HasRange Expr where
        getRange (Var x)               = getRange x
        getRange (Def x)               = getRange x
        getRange (Proj _ x)            = getRange x
        getRange (Con x)               = getRange x
        getRange (Lit l)               = getRange l
        getRange (QuestionMark i _)    = getRange i
        getRange (Underscore  i)       = getRange i
        getRange (Dot i _)             = getRange i
        getRange (App i _ _)           = getRange i
        getRange (WithApp i _ _)       = getRange i
        getRange (Lam i _ _)           = getRange i
        getRange (AbsurdLam i _)       = getRange i
        getRange (ExtendedLam i _ _ _) = getRange i
        getRange (Pi i _ _)            = getRange i
        getRange (Generalized _ x)     = getRange x
        getRange (Fun i _ _)           = getRange i
        getRange (Set i _)             = getRange i
        getRange (Prop i _)            = getRange i
        getRange (Let i _ _)           = getRange i
        getRange (Rec i _)             = getRange i
        getRange (RecUpdate i _ _)     = getRange i
        getRange (ETel tel)            = getRange tel
        getRange (ScopedExpr _ e)      = getRange e
        getRange (QuoteGoal _ _ e)     = getRange e
        getRange (QuoteContext i)      = getRange i
        getRange (Quote i)             = getRange i
        getRange (QuoteTerm i)         = getRange i
        getRange (Unquote i)           = getRange i
        getRange (Tactic i _ _ _)      = getRange i
        getRange (DontCare{})          = noRange
        getRange (PatternSyn x)        = getRange x
        getRange (Macro x)             = getRange x

    instance HasRange Declaration where
        getRange (Axiom    _ i _ _ _ _  ) = getRange i
        getRange (Generalize _ i _ _ _)   = getRange i
        getRange (Field      i _ _      ) = getRange i
        getRange (Mutual     i _        ) = getRange i
        getRange (Section    i _ _ _    ) = getRange i
        getRange (Apply      i _ _ _ _)   = getRange i
        getRange (Import     i _ _      ) = getRange i
        getRange (Primitive  i _ _      ) = getRange i
        getRange (Pragma     i _        ) = getRange i
        getRange (Open       i _ _      ) = getRange i
        getRange (ScopedDecl _ d        ) = getRange d
        getRange (FunDef     i _ _ _    ) = getRange i
        getRange (DataSig    i _ _ _    ) = getRange i
        getRange (DataDef    i _ _ _ _  ) = getRange i
        getRange (RecSig     i _ _ _    ) = getRange i
        getRange (RecDef i _ _ _ _ _ _ _ _) = getRange i
        getRange (PatternSynDef x _ _   ) = getRange x
        getRange (UnquoteDecl _ i _ _)    = getRange i
        getRange (UnquoteDef i _ _)       = getRange i

    instance HasRange (Pattern' e) where
        getRange (VarP x)           = getRange x
        getRange (ConP i _ _)        = getRange i
        getRange (ProjP i _ _)       = getRange i
        getRange (DefP i _ _)        = getRange i
        getRange (WildP i)           = getRange i
        getRange (AsP i _ _)         = getRange i
        getRange (DotP i _)          = getRange i
        getRange (AbsurdP i)         = getRange i
        getRange (LitP l)            = getRange l
        getRange (PatternSynP i _ _) = getRange i
        getRange (RecP i _)          = getRange i
        getRange (EqualP i _)        = getRange i
        getRange (WithP i _)         = getRange i

    instance HasRange SpineLHS where
        getRange (SpineLHS i _ _)  = getRange i

    instance HasRange LHS where
        getRange (LHS i _)   = getRange i

    instance HasRange (LHSCore' e) where
        getRange (LHSHead f ps)         = fuseRange f ps
        getRange (LHSProj d lhscore ps) = d `fuseRange` lhscore `fuseRange` ps
        getRange (LHSWith h wps ps)     = h `fuseRange` wps `fuseRange` ps

    instance HasRange a => HasRange (Clause' a) where
        getRange (Clause lhs _ rhs ds catchall) = getRange (lhs, rhs, ds)

    instance HasRange RHS where
        getRange AbsurdRHS                = noRange
        getRange (RHS e _)                = getRange e
        getRange (WithRHS _ e cs)         = fuseRange e cs
        getRange (RewriteRHS xes _ rhs wh) = getRange (map snd xes, rhs, wh)

    instance HasRange WhereDeclarations where
      getRange (WhereDecls _ ds) = getRange ds

    instance HasRange LetBinding where
        getRange (LetBind i _ _ _ _     ) = getRange i
        getRange (LetPatBind  i _ _      ) = getRange i
        getRange (LetApply i _ _ _ _     ) = getRange i
        getRange (LetOpen  i _ _         ) = getRange i
        getRange (LetDeclaredVariable x)  = getRange x

    -- setRange for patterns applies the range to the outermost pattern constructor
    instance SetRange (Pattern' a) where
        setRange r (VarP x)            = VarP (setRange r x)
        setRange r (ConP i ns as)       = ConP (setRange r i) ns as
        setRange r (ProjP _ o ns)       = ProjP (PatRange r) o ns
        setRange r (DefP _ ns as)       = DefP (PatRange r) ns as -- (setRange r n) as
        setRange r (WildP _)            = WildP (PatRange r)
        setRange r (AsP _ n p)          = AsP (PatRange r) (setRange r n) p
        setRange r (DotP _ e)           = DotP (PatRange r) e
        setRange r (AbsurdP _)          = AbsurdP (PatRange r)
        setRange r (LitP l)             = LitP (setRange r l)
        setRange r (PatternSynP _ n as) = PatternSynP (PatRange r) n as
        setRange r (RecP i as)          = RecP (PatRange r) as
        setRange r (EqualP _ es)        = EqualP (PatRange r) es
        setRange r (WithP i p)          = WithP (setRange r i) p

    instance KillRange LamBinding where
      killRange (DomainFree x) = killRange1 DomainFree x
      killRange (DomainFull b) = killRange1 DomainFull b

    instance KillRange GeneralizeTelescope where
      killRange (GeneralizeTel s tel) = GeneralizeTel s (killRange tel)

    instance KillRange DataDefParams where
      killRange (DataDefParams s tel) = DataDefParams s (killRange tel)

    instance KillRange TypedBinding where
      killRange (TBind r xs e) = killRange3 TBind r xs e
      killRange (TLet r lbs)   = killRange2 TLet r lbs

    instance KillRange Expr where
      killRange (Var x)                = killRange1 Var x
      killRange (Def x)                = killRange1 Def x
      killRange (Proj o x)             = killRange1 (Proj o) x
      killRange (Con x)                = killRange1 Con x
      killRange (Lit l)                = killRange1 Lit l
      killRange (QuestionMark i ii)    = killRange2 QuestionMark i ii
      killRange (Underscore  i)        = killRange1 Underscore i
      killRange (Dot i e)              = killRange2 Dot i e
      killRange (App i e1 e2)          = killRange3 App i e1 e2
      killRange (WithApp i e es)       = killRange3 WithApp i e es
      killRange (Lam i b e)            = killRange3 Lam i b e
      killRange (AbsurdLam i h)        = killRange2 AbsurdLam i h
      killRange (ExtendedLam i n d ps) = killRange4 ExtendedLam i n d ps
      killRange (Pi i a b)             = killRange3 Pi i a b
      killRange (Generalized s x)      = killRange1 (Generalized s) x
      killRange (Fun i a b)            = killRange3 Fun i a b
      killRange (Set i n)              = killRange2 Set i n
      killRange (Prop i n)             = killRange2 Prop i n
      killRange (Let i ds e)           = killRange3 Let i ds e
      killRange (Rec i fs)             = killRange2 Rec i fs
      killRange (RecUpdate i e fs)     = killRange3 RecUpdate i e fs
      killRange (ETel tel)             = killRange1 ETel tel
      killRange (ScopedExpr s e)       = killRange1 (ScopedExpr s) e
      killRange (QuoteGoal i x e)      = killRange3 QuoteGoal i x e
      killRange (QuoteContext i)       = killRange1 QuoteContext i
      killRange (Quote i)              = killRange1 Quote i
      killRange (QuoteTerm i)          = killRange1 QuoteTerm i
      killRange (Unquote i)            = killRange1 Unquote i
      killRange (Tactic i e xs ys)     = killRange4 Tactic i e xs ys
      killRange (DontCare e)           = killRange1 DontCare e
      killRange (PatternSyn x)         = killRange1 PatternSyn x
      killRange (Macro x)              = killRange1 Macro x

    instance KillRange Declaration where
      killRange (Axiom    p i a b c d     ) = killRange4 (\i a c d -> Axiom p i a b c d) i a c d
      killRange (Generalize s i j x e     ) = killRange4 (Generalize s) i j x e
      killRange (Field      i a b         ) = killRange3 Field      i a b
      killRange (Mutual     i a           ) = killRange2 Mutual     i a
      killRange (Section    i a b c       ) = killRange4 Section    i a b c
      killRange (Apply      i a b c d     ) = killRange5 Apply      i a b c d
      killRange (Import     i a b         ) = killRange3 Import     i a b
      killRange (Primitive  i a b         ) = killRange3 Primitive  i a b
      killRange (Pragma     i a           ) = Pragma (killRange i) a
      killRange (Open       i x dir       ) = killRange3 Open       i x dir
      killRange (ScopedDecl a d           ) = killRange1 (ScopedDecl a) d
      killRange (FunDef  i a b c          ) = killRange4 FunDef  i a b c
      killRange (DataSig i a b c          ) = killRange4 DataSig i a b c
      killRange (DataDef i a b c d        ) = killRange5 DataDef i a b c d
      killRange (RecSig  i a b c          ) = killRange4 RecSig  i a b c
      killRange (RecDef  i a b c d e f g h) = killRange9 RecDef  i a b c d e f g h
      killRange (PatternSynDef x xs p     ) = killRange3 PatternSynDef x xs p
      killRange (UnquoteDecl mi i x e     ) = killRange4 UnquoteDecl mi i x e
      killRange (UnquoteDef i x e         ) = killRange3 UnquoteDef i x e

    instance KillRange ModuleApplication where
      killRange (SectionApp a b c  ) = killRange3 SectionApp a b c
      killRange (RecordModuleInstance a) = killRange1 RecordModuleInstance a

    instance KillRange ScopeCopyInfo where
      killRange (ScopeCopyInfo a b) = killRange2 ScopeCopyInfo a b

    instance KillRange e => KillRange (Pattern' e) where
      killRange (VarP x)           = killRange1 VarP x
      killRange (ConP i a b)        = killRange3 ConP i a b
      killRange (ProjP i o a)       = killRange3 ProjP i o a
      killRange (DefP i a b)        = killRange3 DefP i a b
      killRange (WildP i)           = killRange1 WildP i
      killRange (AsP i a b)         = killRange3 AsP i a b
      killRange (DotP i a)          = killRange2 DotP i a
      killRange (AbsurdP i)         = killRange1 AbsurdP i
      killRange (LitP l)            = killRange1 LitP l
      killRange (PatternSynP i a p) = killRange3 PatternSynP i a p
      killRange (RecP i as)         = killRange2 RecP i as
      killRange (EqualP i es)       = killRange2 EqualP i es
      killRange (WithP i p)         = killRange2 WithP i p

    instance KillRange SpineLHS where
      killRange (SpineLHS i a b)  = killRange3 SpineLHS i a b

    instance KillRange LHS where
      killRange (LHS i a)   = killRange2 LHS i a

    instance KillRange e => KillRange (LHSCore' e) where
      killRange (LHSHead a b)   = killRange2 LHSHead a b
      killRange (LHSProj a b c) = killRange3 LHSProj a b c
      killRange (LHSWith a b c) = killRange3 LHSWith a b c

    instance KillRange a => KillRange (Clause' a) where
      killRange (Clause lhs spats rhs ds catchall) = killRange5 Clause lhs spats rhs ds catchall

    instance KillRange ProblemEq where
      killRange (ProblemEq p v a) = killRange3 ProblemEq p v a

    instance KillRange RHS where
      killRange AbsurdRHS                = AbsurdRHS
      killRange (RHS e c)                = killRange2 RHS e c
      killRange (WithRHS q e cs)         = killRange3 WithRHS q e cs
      killRange (RewriteRHS xes spats rhs wh) = killRange4 RewriteRHS xes spats rhs wh

    instance KillRange WhereDeclarations where
      killRange (WhereDecls a b) = killRange2 WhereDecls a b

    instance KillRange LetBinding where
      killRange (LetBind   i info a b c) = killRange5 LetBind i info a b c
      killRange (LetPatBind i a b       ) = killRange3 LetPatBind i a b
      killRange (LetApply   i a b c d   ) = killRange5 LetApply i a b c d
      killRange (LetOpen    i x dir     ) = killRange3 LetOpen  i x dir
      killRange (LetDeclaredVariable x)  = killRange1 LetDeclaredVariable x

    -- See Agda.Utils.GeniPlate:
    -- Does not descend into ScopeInfo and renaming maps, for instance.

    instanceUniverseBiT' [] [t| (Declaration, QName)          |]
    instanceUniverseBiT' [] [t| (Declaration, AmbiguousQName) |]
    instanceUniverseBiT' [] [t| (Declaration, Expr)           |]
    instanceUniverseBiT' [] [t| (Declaration, LetBinding)     |]
    instanceUniverseBiT' [] [t| (Declaration, LamBinding)     |]
    instanceUniverseBiT' [] [t| (Declaration, TypedBinding)   |]
    instanceUniverseBiT' [] [t| (Declaration, Pattern)        |]
    instanceUniverseBiT' [] [t| (Declaration, Pattern' Void)  |]
    instanceUniverseBiT' [] [t| (Declaration, Declaration)    |]
    instanceUniverseBiT' [] [t| (Declaration, ModuleName)     |]
    instanceUniverseBiT' [] [t| (Declaration, ModuleInfo)     |]
    instanceUniverseBiT' [] [t| (Declaration, NamedArg LHSCore)  |]
    instanceUniverseBiT' [] [t| (Declaration, NamedArg BindName) |]
    instanceUniverseBiT' [] [t| (Declaration, NamedArg Expr)     |]
    instanceUniverseBiT' [] [t| (Declaration, NamedArg Pattern)  |]

    ------------------------------------------------------------------------
    -- Queries
    ------------------------------------------------------------------------

    -- | Extracts all the names which are declared in a 'Declaration'.
    -- This does not include open public or let expressions, but it does
    -- include local modules, where clauses and the names of extended
    -- lambdas.

    class AllNames a where
      allNames :: a -> Seq QName

    instance AllNames a => AllNames [a] where
      allNames = Fold.foldMap allNames

    instance AllNames a => AllNames (Maybe a) where
      allNames = Fold.foldMap allNames

    instance AllNames a => AllNames (Arg a) where
      allNames = Fold.foldMap allNames

    instance AllNames a => AllNames (Named name a) where
      allNames = Fold.foldMap allNames

    instance (AllNames a, AllNames b) => AllNames (a,b) where
      allNames (a,b) = allNames a >< allNames b

    instance AllNames QName where
      allNames q = Seq.singleton q

    instance AllNames Declaration where
      allNames (Axiom   _ _ _ _ q _)      = Seq.singleton q
      allNames (Generalize _ _ _ q _)     = Seq.singleton q
      allNames (Field     _   q _)        = Seq.singleton q
      allNames (Primitive _   q _)        = Seq.singleton q
      allNames (Mutual     _ defs)        = allNames defs
      allNames (DataSig _ q _ _)          = Seq.singleton q
      allNames (DataDef _ q _ _ decls)    = q <| allNames decls
      allNames (RecSig _ q _ _)           = Seq.singleton q
      allNames (RecDef _ q _ _ _ c _ _ decls) = q <| allNames c >< allNames decls
      allNames (PatternSynDef q _ _)      = Seq.singleton q
      allNames (UnquoteDecl _ _ qs _)     = Seq.fromList qs
      allNames (UnquoteDef _ qs _)        = Seq.fromList qs
      allNames (FunDef _ q _ cls)         = q <| allNames cls
      allNames (Section _ _ _ decls)      = allNames decls
      allNames Apply{}                    = Seq.empty
      allNames Import{}                   = Seq.empty
      allNames Pragma{}                   = Seq.empty
      allNames Open{}                     = Seq.empty
      allNames (ScopedDecl _ decls)       = allNames decls

    instance AllNames Clause where
      allNames cl = allNames (clauseRHS cl, clauseWhereDecls cl)

    instance AllNames RHS where
      allNames (RHS e _)                 = allNames e
      allNames AbsurdRHS{}               = Seq.empty
      allNames (WithRHS q _ cls)         = q <| allNames cls
      allNames (RewriteRHS qes _ rhs cls) = Seq.fromList (map fst qes) >< allNames rhs >< allNames cls

    instance AllNames WhereDeclarations where
      allNames (WhereDecls _ ds) = allNames ds

    instance AllNames Expr where
      allNames Var{}                   = Seq.empty
      allNames Def{}                   = Seq.empty
      allNames Proj{}                  = Seq.empty
      allNames Con{}                   = Seq.empty
      allNames Lit{}                   = Seq.empty
      allNames QuestionMark{}          = Seq.empty
      allNames Underscore{}            = Seq.empty
      allNames (Dot _ e)               = allNames e
      allNames (App _ e1 e2)           = allNames e1 >< allNames e2
      allNames (WithApp _ e es)        = allNames e >< allNames es
      allNames (Lam _ b e)             = allNames b >< allNames e
      allNames AbsurdLam{}             = Seq.empty
      allNames (ExtendedLam _ _ q cls) = q <| allNames cls
      allNames (Pi _ tel e)            = allNames tel >< allNames e
      allNames (Generalized s e)       = Seq.fromList (Set.toList s) >< allNames e  -- TODO: or just (allNames e)?
      allNames (Fun _ e1 e2)           = allNames e1 >< allNames e2
      allNames Set{}                   = Seq.empty
      allNames Prop{}                  = Seq.empty
      allNames (Let _ lbs e)           = allNames lbs >< allNames e
      allNames ETel{}                  = __IMPOSSIBLE__
      allNames (Rec _ fields)          = allNames [ a ^. exprFieldA | Left a <- fields ]
      allNames (RecUpdate _ e fs)      = allNames e >< allNames (map (view exprFieldA) fs)
      allNames (ScopedExpr _ e)        = allNames e
      allNames (QuoteGoal _ _ e)       = allNames e
      allNames (QuoteContext _)        = Seq.empty
      allNames Quote{}                 = Seq.empty
      allNames QuoteTerm{}             = Seq.empty
      allNames Unquote{}               = Seq.empty
      allNames (Tactic _ e xs ys)      = allNames e >< allNames xs >< allNames ys
      allNames DontCare{}              = Seq.empty
      allNames PatternSyn{}            = Seq.empty
      allNames Macro{}                 = Seq.empty

    instance AllNames LamBinding where
      allNames DomainFree{}       = Seq.empty
      allNames (DomainFull binds) = allNames binds

    instance AllNames TypedBinding where
      allNames (TBind _ _ e) = allNames e
      allNames (TLet _ lbs)  = allNames lbs

    instance AllNames LetBinding where
      allNames (LetBind _ _ _ e1 e2)  = allNames e1 >< allNames e2
      allNames (LetPatBind _ _ e)      = allNames e
      allNames (LetApply _ _ app _ _)  = allNames app
      allNames LetOpen{}               = Seq.empty
      allNames (LetDeclaredVariable _) = Seq.empty

    instance AllNames ModuleApplication where
      allNames (SectionApp bindss _ es) = allNames bindss >< allNames es
      allNames RecordModuleInstance{}   = Seq.empty

    -- | The name defined by the given axiom.
    --
    -- Precondition: The declaration has to be a (scoped) 'Axiom'.

    axiomName :: Declaration -> QName
    axiomName (Axiom _ _ _ _ q _)  = q
    axiomName (ScopedDecl _ (d:_)) = axiomName d
    axiomName _                    = __IMPOSSIBLE__

    -- | Are we in an abstract block?
    --
    --   In that case some definition is abstract.
    class AnyAbstract a where
      anyAbstract :: a -> Bool

    instance AnyAbstract a => AnyAbstract [a] where
      anyAbstract = Fold.any anyAbstract

    instance AnyAbstract Declaration where
      anyAbstract (Axiom _ i _ _ _ _)    = defAbstract i == AbstractDef
      anyAbstract (Field i _ _)          = defAbstract i == AbstractDef
      anyAbstract (Mutual     _ ds)      = anyAbstract ds
      anyAbstract (ScopedDecl _ ds)      = anyAbstract ds
      anyAbstract (Section _ _ _ ds)     = anyAbstract ds
      anyAbstract (FunDef i _ _ _)       = defAbstract i == AbstractDef
      anyAbstract (DataDef i _ _ _ _)    = defAbstract i == AbstractDef
      anyAbstract (RecDef i _ _ _ _ _ _ _ _) = defAbstract i == AbstractDef
      anyAbstract (DataSig i _ _ _)      = defAbstract i == AbstractDef
      anyAbstract (RecSig i _ _ _)       = defAbstract i == AbstractDef
      anyAbstract _                      = __IMPOSSIBLE__

    class NameToExpr a where
      nameExpr :: a -> Expr

    -- | Turn an 'AbstractName' to an expression.
    instance NameToExpr AbstractName where
      nameExpr d = mk (anameKind d) $ anameName d
        where
        mk DefName        x = Def x
        mk GeneralizeName x = Def x
        mk DisallowedGeneralizeName x = Def x
        mk FldName        x = Proj ProjSystem $ unambiguous x
        mk ConName        x = Con $ unambiguous x
        mk PatternSynName x = PatternSyn $ unambiguous x
        mk MacroName      x = Macro x
        mk QuotableName   x = App (defaultAppInfo r) (Quote i) (defaultNamedArg $ Def x)
          where i = ExprRange r
                r = getRange x

    -- | Assumes name is not 'UnknownName'.
    instance NameToExpr ResolvedName where
      nameExpr = \case
        VarName x _          -> Var x
        DefinedName _ x      -> nameExpr x  -- Can be 'DefName', 'MacroName', 'QuotableName'.
        FieldName xs         -> Proj ProjSystem . AmbQ . fmap anameName $ xs
        ConstructorName xs   -> Con . AmbQ . fmap anameName $ xs
        PatternSynResName xs -> PatternSyn . AmbQ . fmap anameName $ xs
        UnknownName          -> __IMPOSSIBLE__

    app :: Expr -> [NamedArg Expr] -> Expr
    app = foldl (App defaultAppInfo_)

    mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
    mkLet i [] e = e
    mkLet i ds e = Let i ds e

    patternToExpr :: Pattern -> Expr
    patternToExpr (VarP x)           = Var (unBind x)
    patternToExpr (ConP _ c ps)       =
      Con c `app` map (fmap (fmap patternToExpr)) ps
    patternToExpr (ProjP _ o ds)      = Proj o ds
    patternToExpr (DefP _ fs ps) =
      Def (headAmbQ fs) `app` map (fmap (fmap patternToExpr)) ps
    patternToExpr (WildP _)           = Underscore emptyMetaInfo
    patternToExpr (AsP _ _ p)         = patternToExpr p
    patternToExpr (DotP _ e)          = e
    patternToExpr (AbsurdP _)         = Underscore emptyMetaInfo  -- TODO: could this happen?
    patternToExpr (LitP l)            = Lit l
    patternToExpr (PatternSynP _ c ps) = PatternSyn c `app` (map . fmap . fmap) patternToExpr ps
    patternToExpr (RecP _ as)         = Rec exprNoRange $ map (Left . fmap patternToExpr) as
    patternToExpr EqualP{}            = __IMPOSSIBLE__  -- Andrea TODO: where is this used?
    patternToExpr (WithP r p)         = __IMPOSSIBLE__

    type PatternSynDefn = ([Arg Name], Pattern' Void)
    type PatternSynDefns = Map QName PatternSynDefn

    lambdaLiftExpr :: [Name] -> Expr -> Expr
    lambdaLiftExpr []     e = e
    lambdaLiftExpr (n:ns) e = Lam exprNoRange (DomainFree $ defaultNamedArg $ BindName n) $
                                lambdaLiftExpr ns e

    class SubstExpr a where
      substExpr :: [(Name, Expr)] -> a -> a

    instance SubstExpr a => SubstExpr [a] where
      substExpr = fmap . substExpr

    instance SubstExpr a => SubstExpr (Arg a) where
      substExpr = fmap . substExpr

    instance SubstExpr a => SubstExpr (Named name a) where
      substExpr = fmap . substExpr

    instance (SubstExpr a, SubstExpr b) => SubstExpr (a, b) where
      substExpr s (x, y) = (substExpr s x, substExpr s y)

    instance (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) where
      substExpr s (Left x)  = Left (substExpr s x)
      substExpr s (Right y) = Right (substExpr s y)

    instance SubstExpr C.Name where
      substExpr _ = id

    instance SubstExpr ModuleName where
      substExpr _ = id

    instance SubstExpr Assign where
      substExpr s (FieldAssignment n x) = FieldAssignment n (substExpr s x)

    instance SubstExpr Expr where
      substExpr s e = case e of
        Var n                 -> fromMaybe e (lookup n s)
        Def _                 -> e
        Proj{}                -> e
        Con _                 -> e
        Lit _                 -> e
        QuestionMark{}        -> e
        Underscore   _        -> e
        Dot i e               -> Dot i (substExpr s e)
        App  i e e'           -> App i (substExpr s e) (substExpr s e')
        WithApp i e es        -> WithApp i (substExpr s e) (substExpr s es)
        Lam  i lb e           -> Lam i lb (substExpr s e)
        AbsurdLam i h         -> e
        ExtendedLam i di n cs -> __IMPOSSIBLE__   -- Maybe later...
        Pi   i t e            -> Pi i (substExpr s t) (substExpr s e)
        Generalized ns e      -> Generalized ns (substExpr s e)
        Fun  i ae e           -> Fun i (substExpr s ae) (substExpr s e)
        Set  i n              -> e
        Prop i n              -> e
        Let  i ls e           -> Let i (substExpr s ls) (substExpr s e)
        ETel t                -> e
        Rec  i nes            -> Rec i (substExpr s nes)
        RecUpdate i e nes     -> RecUpdate i (substExpr s e) (substExpr s nes)
        -- XXX: Do we need to do more with ScopedExprs?
        ScopedExpr si e       -> ScopedExpr si (substExpr s e)
        QuoteGoal i n e       -> QuoteGoal i n (substExpr s e)
        QuoteContext i        -> e
        Quote i               -> e
        QuoteTerm i           -> e
        Unquote i             -> e
        Tactic i e xs ys      -> Tactic i (substExpr s e) (substExpr s xs) (substExpr s ys)
        DontCare e            -> DontCare (substExpr s e)
        PatternSyn{}          -> e
        Macro{}               -> e

    instance SubstExpr LetBinding where
      substExpr s lb = case lb of
        LetBind i r n e e' -> LetBind i r n (substExpr s e) (substExpr s e')
        LetPatBind i p e   -> LetPatBind i p (substExpr s e) -- Andreas, 2012-06-04: what about the pattern p
        _                  -> lb -- Nicolas, 2013-11-11: what about "LetApply" there is experessions in there

    instance SubstExpr TypedBinding where
      substExpr s tb = case tb of
        TBind r ns e -> TBind r ns $ substExpr s e
        TLet r lbs   -> TLet r $ substExpr s lbs

    -- TODO: more informative failure
    insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] ->
                                Maybe ([(Name, a)], [Arg Name])
    insertImplicitPatSynArgs wild r ns as = matchArgs r ns as
      where
        matchNextArg r n as@(~(a : as'))
          | matchNext n as = return (namedArg a, as')
          | visible n      = Nothing
          | otherwise      = return (wild r, as)

        matchNext _ [] = False
        matchNext n (a:as) = sameHiding n a && matchName
          where
            x = unranged $ C.nameToRawName $ nameConcrete $ unArg n
            matchName = maybe True (== x) (nameOf $ unArg a)

        matchArgs r [] []     = return ([], [])
        matchArgs r [] as     = Nothing
        matchArgs r (n:ns) [] | visible n = return ([], n : ns)    -- under-applied
        matchArgs r (n:ns) as = do
          (p, as) <- matchNextArg r n as
          first ((unArg n, p) :) <$> matchArgs (getRange p) ns as