    {-| 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 hiding (null)

    import Control.DeepSeq

    import Data.Bifunctor
    import qualified Data.Foldable as Fold
    import Data.Function (on)
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe
    import qualified Data.Set as Set
    import Data.Set (Set)
    import Data.Void

    import GHC.Generics (Generic)

    import Agda.Syntax.Concrete (FieldAssignment'(..), TacticAttribute'(..))
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Pretty ()
    import Agda.Syntax.Abstract.Name
    import qualified Agda.Syntax.Internal as I
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Info
    import Agda.Syntax.Literal
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base

    import Agda.TypeChecking.Positivity.Occurrence

    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null
    import Agda.Utils.Set1 (Set1)
    import qualified Agda.Utils.Set1 as Set1

    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 { BindName -> Name
    unBind :: Name }
      deriving (Int -> BindName -> ShowS
    [BindName] -> ShowS
    BindName -> String
    (Int -> BindName -> ShowS)
    -> (BindName -> String) -> ([BindName] -> ShowS) -> Show BindName
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> BindName -> ShowS
    showsPrec :: Int -> BindName -> ShowS
    $cshow :: BindName -> String
    show :: BindName -> String
    $cshowList :: [BindName] -> ShowS
    showList :: [BindName] -> ShowS
    Show, BindName -> Range
    (BindName -> Range) -> HasRange BindName
    forall a. (a -> Range) -> HasRange a
    $cgetRange :: BindName -> Range
    getRange :: BindName -> Range
    HasRange, KillRangeT BindName
    KillRangeT BindName -> KillRange BindName
    forall a. KillRangeT a -> KillRange a
    $ckillRange :: KillRangeT BindName
    killRange :: KillRangeT BindName
    KillRange, HasRange BindName
    HasRange BindName =>
    (Range -> KillRangeT BindName) -> SetRange BindName
    Range -> KillRangeT BindName
    forall a. HasRange a => (Range -> a -> a) -> SetRange a
    $csetRange :: Range -> KillRangeT BindName
    setRange :: Range -> KillRangeT BindName
    SetRange, BindName -> ()
    (BindName -> ()) -> NFData BindName
    forall a. (a -> ()) -> NFData a
    $crnf :: BindName -> ()
    rnf :: BindName -> ()
    NFData)

    mkBindName :: Name -> BindName
    mkBindName :: Name -> BindName
    mkBindName Name
    x = Name -> BindName
    BindName Name
    x

    instance Eq BindName where
      BindName Name
    n == :: BindName -> BindName -> Bool
    == BindName Name
    m
        = (NameId -> NameId -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (NameId -> NameId -> Bool)
    -> (Name -> NameId) -> Name -> Name -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Name -> NameId
    nameId) Name
    n Name
    m
          Bool -> Bool -> Bool
    && (Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Name -> Name -> Bool) -> (Name -> Name) -> Name -> Name -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Name -> Name
    nameConcrete) Name
    n Name
    m

    instance Ord BindName where
      BindName Name
    n compare :: BindName -> BindName -> Ordering
    `compare` BindName Name
    m
        = (NameId -> NameId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (NameId -> NameId -> Ordering)
    -> (Name -> NameId) -> Name -> Name -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Name -> NameId
    nameId) Name
    n Name
    m
          Ordering -> Ordering -> Ordering
    forall a. Monoid a => a -> a -> a
    `mappend` (Name -> Name -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Name -> Name -> Ordering)
    -> (Name -> Name) -> Name -> Name -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Name -> Name
    nameConcrete) Name
    n Name
    m

    type Args = [NamedArg Expr]

    -- | Types are just expressions.
    -- Use this type synonym for hinting that an expression should be a type.
    type Type = Expr

    -- | Expressions after scope checking (operators parsed, names resolved).
    data Expr
      = Var  Name                          -- ^ Bound variable.
      | Def'  QName Suffix                 -- ^ Constant: axiom, function, data or record type,
                                           --   with a possible suffix.
      | Proj ProjOrigin AmbiguousQName     -- ^ Projection (overloaded).
      | Con  AmbiguousQName                -- ^ Constructor (overloaded).
      | PatternSyn AmbiguousQName          -- ^ Pattern synonym.
      | Macro QName                        -- ^ Macro.
      | Lit ExprInfo 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 (List1 Expr) -- ^ With application.
      | Lam  ExprInfo LamBinding Expr      -- ^ @λ bs → e@.
      | AbsurdLam ExprInfo Hiding          -- ^ @λ()@ or @λ{}@.
      | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
      | Pi   ExprInfo Telescope1 Type      -- ^ Dependent function space @Γ → A@.
      | Generalized (Set1 QName) Type      -- ^ Like a Pi, but the ordering is not known
      | Fun  ExprInfo (Arg Type) Type      -- ^ Non-dependent function space.
      | Let  ExprInfo (List1 LetBinding) Expr
                                           -- ^ @let bs in e@.
      | Rec  KwRange ExprInfo RecordAssigns
          -- ^ Record construction.  The 'KwRange' is for the @record@ kewyword.
      | RecUpdate KwRange ExprInfo Expr Assigns
          -- ^ Record update.  The 'KwRange' is for the @record@ kewyword.
      | ScopedExpr ScopeInfo Expr          -- ^ Scope annotation.
      | Quote ExprInfo                     -- ^ Quote an identifier 'QName'.
      | QuoteTerm ExprInfo                 -- ^ Quote a term.
      | Unquote ExprInfo                   -- ^ The splicing construct: unquote ...
      | DontCare Expr                      -- ^ For printing @DontCare@ from @Syntax.Internal@.
      deriving (Int -> Expr -> ShowS
    [Expr] -> ShowS
    Expr -> String
    (Int -> Expr -> ShowS)
    -> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Expr -> ShowS
    showsPrec :: Int -> Expr -> ShowS
    $cshow :: Expr -> String
    show :: Expr -> String
    $cshowList :: [Expr] -> ShowS
    showList :: [Expr] -> ShowS
    Show, (forall x. Expr -> Rep Expr x)
    -> (forall x. Rep Expr x -> Expr) -> Generic Expr
    forall x. Rep Expr x -> Expr
    forall x. Expr -> Rep Expr x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Expr -> Rep Expr x
    from :: forall x. Expr -> Rep Expr x
    $cto :: forall x. Rep Expr x -> Expr
    to :: forall x. Rep Expr x -> Expr
    Generic)

    -- | Pattern synonym for regular 'Def'.
    pattern Def :: QName -> Expr
    pattern $mDef :: forall {r}. Expr -> (QName -> r) -> ((# #) -> r) -> r
    $bDef :: QName -> Expr
    Def x = Def' x NoSuffix

    -- | Smart constructor for 'Generalized'.
    generalized :: Set QName -> Type -> Type
    generalized :: Set QName -> Expr -> Expr
    generalized Set QName
    s Expr
    e = Set QName -> Expr -> (Set1 QName -> Expr) -> Expr
    forall a b. Set a -> b -> (Set1 a -> b) -> b
    Set1.ifNull Set QName
    s Expr
    e \ Set1 QName
    s -> Set1 QName -> Expr -> Expr
    Generalized Set1 QName
    s Expr
    e

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

    -- | Renaming (generic).
    type Ren a = Map a (List1 a)

    data ScopeCopyInfo = ScopeCopyInfo
      { ScopeCopyInfo -> Ren ModuleName
    renModules :: Ren ModuleName
      , ScopeCopyInfo -> Ren QName
    renNames   :: Ren QName }
      deriving (ScopeCopyInfo -> ScopeCopyInfo -> Bool
    (ScopeCopyInfo -> ScopeCopyInfo -> Bool)
    -> (ScopeCopyInfo -> ScopeCopyInfo -> Bool) -> Eq ScopeCopyInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
    == :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
    $c/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
    /= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
    Eq, Int -> ScopeCopyInfo -> ShowS
    [ScopeCopyInfo] -> ShowS
    ScopeCopyInfo -> String
    (Int -> ScopeCopyInfo -> ShowS)
    -> (ScopeCopyInfo -> String)
    -> ([ScopeCopyInfo] -> ShowS)
    -> Show ScopeCopyInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ScopeCopyInfo -> ShowS
    showsPrec :: Int -> ScopeCopyInfo -> ShowS
    $cshow :: ScopeCopyInfo -> String
    show :: ScopeCopyInfo -> String
    $cshowList :: [ScopeCopyInfo] -> ShowS
    showList :: [ScopeCopyInfo] -> ShowS
    Show, (forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x)
    -> (forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo)
    -> Generic ScopeCopyInfo
    forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
    forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
    from :: forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
    $cto :: forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
    to :: forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
    Generic)

    initCopyInfo :: ScopeCopyInfo
    initCopyInfo :: ScopeCopyInfo
    initCopyInfo = ScopeCopyInfo
      { renModules :: Ren ModuleName
    renModules = Ren ModuleName
    forall a. Monoid a => a
    mempty
      , renNames :: Ren QName
    renNames   = Ren QName
    forall a. Monoid a => a
    mempty
      }

    instance Pretty ScopeCopyInfo where
      pretty :: ScopeCopyInfo -> Doc
    pretty ScopeCopyInfo
    i = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ String -> Ren ModuleName -> Doc
    forall {l} {a}.
    (IsList l, Pretty a, Pretty (Item l)) =>
    String -> Map a l -> Doc
    prRen String
    "renModules =" (ScopeCopyInfo -> Ren ModuleName
    renModules ScopeCopyInfo
    i)
                      , String -> Ren QName -> Doc
    forall {l} {a}.
    (IsList l, Pretty a, Pretty (Item l)) =>
    String -> Map a l -> Doc
    prRen String
    "renNames   =" (ScopeCopyInfo -> Ren QName
    renNames ScopeCopyInfo
    i) ]
        where
          prRen :: String -> Map a l -> Doc
    prRen String
    s Map a l
    r = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ String -> Doc
    forall a. String -> Doc a
    text String
    s, Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (((a, Item l) -> Doc) -> [(a, Item l)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (a, Item l) -> Doc
    forall {a} {a}. (Pretty a, Pretty a) => (a, a) -> Doc
    pr [(a, Item l)]
    xs) ]
            where
              xs :: [(a, Item l)]
    xs = [ (a
    k, Item l
    v) | (a
    k, l
    vs) <- Map a l -> [(a, l)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map a l
    r, Item l
    v <- l -> [Item l]
    forall l. IsList l => l -> [Item l]
    List1.toList l
    vs ]
          pr :: (a, a) -> Doc
    pr (a
    x, a
    y) = a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "->" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    y

    -- | How did we get our hands on the 'QName' for the constructor of this
    -- record?
    data RecordConName
      = NamedRecCon { RecordConName -> QName
    recordConName :: !QName }
        -- ^ The user wrote it.
      | FreshRecCon { recordConName :: !QName }
        -- ^ We made it up.
      deriving (RecordConName -> RecordConName -> Bool
    (RecordConName -> RecordConName -> Bool)
    -> (RecordConName -> RecordConName -> Bool) -> Eq RecordConName
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: RecordConName -> RecordConName -> Bool
    == :: RecordConName -> RecordConName -> Bool
    $c/= :: RecordConName -> RecordConName -> Bool
    /= :: RecordConName -> RecordConName -> Bool
    Eq, Int -> RecordConName -> ShowS
    [RecordConName] -> ShowS
    RecordConName -> String
    (Int -> RecordConName -> ShowS)
    -> (RecordConName -> String)
    -> ([RecordConName] -> ShowS)
    -> Show RecordConName
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RecordConName -> ShowS
    showsPrec :: Int -> RecordConName -> ShowS
    $cshow :: RecordConName -> String
    show :: RecordConName -> String
    $cshowList :: [RecordConName] -> ShowS
    showList :: [RecordConName] -> ShowS
    Show, (forall x. RecordConName -> Rep RecordConName x)
    -> (forall x. Rep RecordConName x -> RecordConName)
    -> Generic RecordConName
    forall x. Rep RecordConName x -> RecordConName
    forall x. RecordConName -> Rep RecordConName x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. RecordConName -> Rep RecordConName x
    from :: forall x. RecordConName -> Rep RecordConName x
    $cto :: forall x. Rep RecordConName x -> RecordConName
    to :: forall x. Rep RecordConName x -> RecordConName
    Generic)

    type RecordDirectives = RecordDirectives' RecordConName

    data Declaration
      = Axiom      KindOfName DefInfo ArgInfo (Maybe PragmaPolarities) QName Type
        -- ^ Type signature (can be irrelevant, but not hidden).
        --
        -- The fourth argument contains an optional assignment of
        -- polarities to arguments.
      | Generalize (Set QName) DefInfo ArgInfo QName Type
        -- ^ The first argument is the (possibly empty) set of generalizable variables used in the type.
      | Field      DefInfo QName (Arg Type)              -- ^ record field
      | Primitive  DefInfo QName (Arg Type)              -- ^ primitive function
      | Mutual     MutualInfo [Declaration]              -- ^ a bunch of mutually recursive definitions
      | Section    Range Erased ModuleName GeneralizeTelescope [Declaration]
      | Apply      ModuleInfo Erased 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
      | FunDef     DefInfo QName [Clause] -- ^ sequence of function clauses
      | DataSig    DefInfo Erased QName GeneralizeTelescope Type -- ^ lone data signature
      | DataDef    DefInfo QName UniverseCheck DataDefParams [Constructor]
      | RecSig     DefInfo Erased QName GeneralizeTelescope Type -- ^ lone record signature
      | RecDef     DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
          -- ^ The 'Type' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Dummy@,
          --   and the optional name is the constructor's name.
          --   The optional 'Range' is for the @pattern@ attribute.
      | PatternSynDef QName [WithHiding BindName] (Pattern' Void)
          -- ^ Only for highlighting purposes
      | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
      | UnquoteDef  [DefInfo] [QName] Expr
      | UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
      | ScopedDecl ScopeInfo [Declaration]  -- ^ scope annotation
      | UnfoldingDecl Range [QName]
        -- ^ Only for highlighting the unfolded names
      deriving (Int -> Declaration -> ShowS
    [Declaration] -> ShowS
    Declaration -> String
    (Int -> Declaration -> ShowS)
    -> (Declaration -> String)
    -> ([Declaration] -> ShowS)
    -> Show Declaration
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Declaration -> ShowS
    showsPrec :: Int -> Declaration -> ShowS
    $cshow :: Declaration -> String
    show :: Declaration -> String
    $cshowList :: [Declaration] -> ShowS
    showList :: [Declaration] -> ShowS
    Show, (forall x. Declaration -> Rep Declaration x)
    -> (forall x. Rep Declaration x -> Declaration)
    -> Generic Declaration
    forall x. Rep Declaration x -> Declaration
    forall x. Declaration -> Rep Declaration x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Declaration -> Rep Declaration x
    from :: forall x. Declaration -> Rep Declaration x
    $cto :: forall x. Rep Declaration x -> Declaration
    to :: forall x. Rep Declaration x -> Declaration
    Generic)

    type DefInfo = DefInfo' Expr

    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 (Int -> ModuleApplication -> ShowS
    [ModuleApplication] -> ShowS
    ModuleApplication -> String
    (Int -> ModuleApplication -> ShowS)
    -> (ModuleApplication -> String)
    -> ([ModuleApplication] -> ShowS)
    -> Show ModuleApplication
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ModuleApplication -> ShowS
    showsPrec :: Int -> ModuleApplication -> ShowS
    $cshow :: ModuleApplication -> String
    show :: ModuleApplication -> String
    $cshowList :: [ModuleApplication] -> ShowS
    showList :: [ModuleApplication] -> ShowS
    Show, ModuleApplication -> ModuleApplication -> Bool
    (ModuleApplication -> ModuleApplication -> Bool)
    -> (ModuleApplication -> ModuleApplication -> Bool)
    -> Eq ModuleApplication
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ModuleApplication -> ModuleApplication -> Bool
    == :: ModuleApplication -> ModuleApplication -> Bool
    $c/= :: ModuleApplication -> ModuleApplication -> Bool
    /= :: ModuleApplication -> ModuleApplication -> Bool
    Eq, (forall x. ModuleApplication -> Rep ModuleApplication x)
    -> (forall x. Rep ModuleApplication x -> ModuleApplication)
    -> Generic ModuleApplication
    forall x. Rep ModuleApplication x -> ModuleApplication
    forall x. ModuleApplication -> Rep ModuleApplication x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ModuleApplication -> Rep ModuleApplication x
    from :: forall x. ModuleApplication -> Rep ModuleApplication x
    $cto :: forall x. Rep ModuleApplication x -> ModuleApplication
    to :: forall x. Rep ModuleApplication x -> ModuleApplication
    Generic)

    data Pragma
      = OptionsPragma [String]
      | BuiltinPragma RString ResolvedName
        -- ^ 'ResolvedName' is not 'UnknownName'.
        --   Name can be ambiguous e.g. for built-in constructors.
      | BuiltinNoDefPragma RString KindOfName QName
        -- ^ Builtins that do not come with a definition,
        --   but declare a name for an Agda concept.
      | RewritePragma Range [QName]
        -- ^ Range is range of REWRITE keyword.
      | CompilePragma (Ranged BackendName) 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
      | InjectiveForInferencePragma QName
      | InlinePragma Bool QName -- INLINE or NOINLINE
      | NotProjectionLikePragma QName
        -- ^ Mark the definition as not being projection-like
      | OverlapPragma QName OverlapMode
        -- ^ If the definition is an instance, set its overlap mode.
      | DisplayPragma QName [NamedArg Pattern] Expr
      deriving (Int -> Pragma -> ShowS
    [Pragma] -> ShowS
    Pragma -> String
    (Int -> Pragma -> ShowS)
    -> (Pragma -> String) -> ([Pragma] -> ShowS) -> Show Pragma
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Pragma -> ShowS
    showsPrec :: Int -> Pragma -> ShowS
    $cshow :: Pragma -> String
    show :: Pragma -> String
    $cshowList :: [Pragma] -> ShowS
    showList :: [Pragma] -> ShowS
    Show, Pragma -> Pragma -> Bool
    (Pragma -> Pragma -> Bool)
    -> (Pragma -> Pragma -> Bool) -> Eq Pragma
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Pragma -> Pragma -> Bool
    == :: Pragma -> Pragma -> Bool
    $c/= :: Pragma -> Pragma -> Bool
    /= :: Pragma -> Pragma -> Bool
    Eq, (forall x. Pragma -> Rep Pragma x)
    -> (forall x. Rep Pragma x -> Pragma) -> Generic Pragma
    forall x. Rep Pragma x -> Pragma
    forall x. Pragma -> Rep Pragma x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Pragma -> Rep Pragma x
    from :: forall x. Pragma -> Rep Pragma x
    $cto :: forall x. Rep Pragma x -> Pragma
    to :: forall x. Rep Pragma x -> Pragma
    Generic)

    -- | Bindings that are valid in a @let@.
    data LetBinding
      = LetBind LetInfo ArgInfo BindName Type Expr
        -- ^ @LetBind info rel name type defn@
      | LetAxiom LetInfo ArgInfo BindName Type
        -- ^ Function declarations in a let with no matching body.
      | LetPatBind LetInfo Pattern Expr
        -- ^ Irrefutable pattern binding.
      | LetApply ModuleInfo Erased 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
      deriving (Int -> LetBinding -> ShowS
    [LetBinding] -> ShowS
    LetBinding -> String
    (Int -> LetBinding -> ShowS)
    -> (LetBinding -> String)
    -> ([LetBinding] -> ShowS)
    -> Show LetBinding
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> LetBinding -> ShowS
    showsPrec :: Int -> LetBinding -> ShowS
    $cshow :: LetBinding -> String
    show :: LetBinding -> String
    $cshowList :: [LetBinding] -> ShowS
    showList :: [LetBinding] -> ShowS
    Show, LetBinding -> LetBinding -> Bool
    (LetBinding -> LetBinding -> Bool)
    -> (LetBinding -> LetBinding -> Bool) -> Eq LetBinding
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LetBinding -> LetBinding -> Bool
    == :: LetBinding -> LetBinding -> Bool
    $c/= :: LetBinding -> LetBinding -> Bool
    /= :: LetBinding -> LetBinding -> Bool
    Eq, (forall x. LetBinding -> Rep LetBinding x)
    -> (forall x. Rep LetBinding x -> LetBinding) -> Generic LetBinding
    forall x. Rep LetBinding x -> LetBinding
    forall x. LetBinding -> Rep LetBinding x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LetBinding -> Rep LetBinding x
    from :: forall x. LetBinding -> Rep LetBinding x
    $cto :: forall x. Rep LetBinding x -> LetBinding
    to :: forall x. Rep LetBinding x -> LetBinding
    Generic)

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

    type TacticAttribute = TacticAttribute' Expr

    -- A Binder @x\@p@, the pattern is optional
    data Binder' a = Binder
      { forall a. Binder' a -> Maybe Pattern
    binderPattern    :: Maybe Pattern
      , forall a. Binder' a -> BinderNameOrigin
    binderNameOrigin :: BinderNameOrigin
      , forall a. Binder' a -> a
    binderName       :: a
      } deriving (Int -> Binder' a -> ShowS
    [Binder' a] -> ShowS
    Binder' a -> String
    (Int -> Binder' a -> ShowS)
    -> (Binder' a -> String)
    -> ([Binder' a] -> ShowS)
    -> Show (Binder' a)
    forall a. Show a => Int -> Binder' a -> ShowS
    forall a. Show a => [Binder' a] -> ShowS
    forall a. Show a => Binder' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> Binder' a -> ShowS
    showsPrec :: Int -> Binder' a -> ShowS
    $cshow :: forall a. Show a => Binder' a -> String
    show :: Binder' a -> String
    $cshowList :: forall a. Show a => [Binder' a] -> ShowS
    showList :: [Binder' a] -> ShowS
    Show, Binder' a -> Binder' a -> Bool
    (Binder' a -> Binder' a -> Bool)
    -> (Binder' a -> Binder' a -> Bool) -> Eq (Binder' a)
    forall a. Eq a => Binder' a -> Binder' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => Binder' a -> Binder' a -> Bool
    == :: Binder' a -> Binder' a -> Bool
    $c/= :: forall a. Eq a => Binder' a -> Binder' a -> Bool
    /= :: Binder' a -> Binder' a -> Bool
    Eq, (forall a b. (a -> b) -> Binder' a -> Binder' b)
    -> (forall a b. a -> Binder' b -> Binder' a) -> Functor Binder'
    forall a b. a -> Binder' b -> Binder' a
    forall a b. (a -> b) -> Binder' a -> Binder' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
    fmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
    $c<$ :: forall a b. a -> Binder' b -> Binder' a
    <$ :: forall a b. a -> Binder' b -> Binder' a
    Functor, (forall m. Monoid m => Binder' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Binder' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Binder' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Binder' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Binder' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Binder' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Binder' a -> b)
    -> (forall a. (a -> a -> a) -> Binder' a -> a)
    -> (forall a. (a -> a -> a) -> Binder' a -> a)
    -> (forall a. Binder' a -> [a])
    -> (forall a. Binder' a -> Bool)
    -> (forall a. Binder' a -> Int)
    -> (forall a. Eq a => a -> Binder' a -> Bool)
    -> (forall a. Ord a => Binder' a -> a)
    -> (forall a. Ord a => Binder' a -> a)
    -> (forall a. Num a => Binder' a -> a)
    -> (forall a. Num a => Binder' a -> a)
    -> Foldable Binder'
    forall a. Eq a => a -> Binder' a -> Bool
    forall a. Num a => Binder' a -> a
    forall a. Ord a => Binder' a -> a
    forall m. Monoid m => Binder' m -> m
    forall a. Binder' a -> Bool
    forall a. Binder' a -> Int
    forall a. Binder' a -> [a]
    forall a. (a -> a -> a) -> Binder' a -> a
    forall m a. Monoid m => (a -> m) -> Binder' a -> m
    forall b a. (b -> a -> b) -> b -> Binder' a -> b
    forall a b. (a -> b -> b) -> b -> Binder' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Binder' m -> m
    fold :: forall m. Monoid m => Binder' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
    $ctoList :: forall a. Binder' a -> [a]
    toList :: forall a. Binder' a -> [a]
    $cnull :: forall a. Binder' a -> Bool
    null :: forall a. Binder' a -> Bool
    $clength :: forall a. Binder' a -> Int
    length :: forall a. Binder' a -> Int
    $celem :: forall a. Eq a => a -> Binder' a -> Bool
    elem :: forall a. Eq a => a -> Binder' a -> Bool
    $cmaximum :: forall a. Ord a => Binder' a -> a
    maximum :: forall a. Ord a => Binder' a -> a
    $cminimum :: forall a. Ord a => Binder' a -> a
    minimum :: forall a. Ord a => Binder' a -> a
    $csum :: forall a. Num a => Binder' a -> a
    sum :: forall a. Num a => Binder' a -> a
    $cproduct :: forall a. Num a => Binder' a -> a
    product :: forall a. Num a => Binder' a -> a
    Foldable, Functor Binder'
    Foldable Binder'
    (Functor Binder', Foldable Binder') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Binder' a -> f (Binder' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Binder' (f a) -> f (Binder' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Binder' a -> m (Binder' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Binder' (m a) -> m (Binder' a))
    -> Traversable Binder'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Binder' (f a) -> f (Binder' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Binder' a -> m (Binder' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Binder' a -> f (Binder' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Binder' a -> f (Binder' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Binder' a -> f (Binder' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Binder' (f a) -> f (Binder' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Binder' (f a) -> f (Binder' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Binder' a -> m (Binder' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Binder' a -> m (Binder' b)
    $csequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
    sequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
    Traversable, (forall x. Binder' a -> Rep (Binder' a) x)
    -> (forall x. Rep (Binder' a) x -> Binder' a)
    -> Generic (Binder' a)
    forall x. Rep (Binder' a) x -> Binder' a
    forall x. Binder' a -> Rep (Binder' a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (Binder' a) x -> Binder' a
    forall a x. Binder' a -> Rep (Binder' a) x
    $cfrom :: forall a x. Binder' a -> Rep (Binder' a) x
    from :: forall x. Binder' a -> Rep (Binder' a) x
    $cto :: forall a x. Rep (Binder' a) x -> Binder' a
    to :: forall x. Rep (Binder' a) x -> Binder' a
    Generic)

    type Binder = Binder' BindName

    mkBinder :: a -> Binder' a
    mkBinder :: forall a. a -> Binder' a
    mkBinder = Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    forall a. Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    Binder Maybe Pattern
    forall a. Maybe a
    Nothing BinderNameOrigin
    UserBinderName

    mkBinder_ :: Name -> Binder
    mkBinder_ :: Name -> Binder
    mkBinder_ = BindName -> Binder
    forall a. a -> Binder' a
    mkBinder (BindName -> Binder) -> (Name -> BindName) -> Name -> Binder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> BindName
    mkBindName

    insertedBinder :: a -> Binder' a
    insertedBinder :: forall a. a -> Binder' a
    insertedBinder = Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    forall a. Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    Binder Maybe Pattern
    forall a. Maybe a
    Nothing BinderNameOrigin
    InsertedBinderName

    insertedBinder_ :: Name -> Binder
    insertedBinder_ :: Name -> Binder
    insertedBinder_ = BindName -> Binder
    forall a. a -> Binder' a
    insertedBinder (BindName -> Binder) -> (Name -> BindName) -> Name -> Binder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> BindName
    mkBindName

    extractPattern :: Binder' a -> Maybe (Pattern, a)
    extractPattern :: forall a. Binder' a -> Maybe (Pattern, a)
    extractPattern (Binder Maybe Pattern
    p BinderNameOrigin
    _ a
    a) = (,a
    a) (Pattern -> (Pattern, a)) -> Maybe Pattern -> Maybe (Pattern, a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Pattern
    p

    -- | A lambda binding is either domain free or typed.
    data LamBinding
      = DomainFree TacticAttribute (NamedArg Binder)
        -- ^ . @x@ or @{x}@ or @.x@ or @{x = y}@ or @x\@p@ or @(p)@
      | DomainFull TypedBinding
        -- ^ . @(xs:e)@ or @{xs:e}@ or @(let Ds)@
      deriving (Int -> LamBinding -> ShowS
    [LamBinding] -> ShowS
    LamBinding -> String
    (Int -> LamBinding -> ShowS)
    -> (LamBinding -> String)
    -> ([LamBinding] -> ShowS)
    -> Show LamBinding
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> LamBinding -> ShowS
    showsPrec :: Int -> LamBinding -> ShowS
    $cshow :: LamBinding -> String
    show :: LamBinding -> String
    $cshowList :: [LamBinding] -> ShowS
    showList :: [LamBinding] -> ShowS
    Show, LamBinding -> LamBinding -> Bool
    (LamBinding -> LamBinding -> Bool)
    -> (LamBinding -> LamBinding -> Bool) -> Eq LamBinding
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LamBinding -> LamBinding -> Bool
    == :: LamBinding -> LamBinding -> Bool
    $c/= :: LamBinding -> LamBinding -> Bool
    /= :: LamBinding -> LamBinding -> Bool
    Eq, (forall x. LamBinding -> Rep LamBinding x)
    -> (forall x. Rep LamBinding x -> LamBinding) -> Generic LamBinding
    forall x. Rep LamBinding x -> LamBinding
    forall x. LamBinding -> Rep LamBinding x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LamBinding -> Rep LamBinding x
    from :: forall x. LamBinding -> Rep LamBinding x
    $cto :: forall x. Rep LamBinding x -> LamBinding
    to :: forall x. Rep LamBinding x -> LamBinding
    Generic)

    mkDomainFree :: NamedArg Binder -> LamBinding
    mkDomainFree :: NamedArg Binder -> LamBinding
    mkDomainFree = TacticAttribute -> NamedArg Binder -> LamBinding
    DomainFree TacticAttribute
    forall a. Null a => a
    empty

    -- | Extra information that is attached to a typed binding, that plays a
    -- role during type checking but strictly speaking is not part of the
    -- @name : type@" relation which a makes up a binding.
    data TypedBindingInfo
      = TypedBindingInfo
        { TypedBindingInfo -> TacticAttribute
    tbTacticAttr :: TacticAttribute
          -- ^ Does this binding have a tactic annotation?
        , TypedBindingInfo -> Bool
    tbFinite     :: Bool
          -- ^ Does this binding correspond to a Partial binder, rather than
          -- to a Pi binder? Must be present here to be reflected into
          -- abstract syntax later (and to be printed to the user later).
        }
      deriving (Int -> TypedBindingInfo -> ShowS
    [TypedBindingInfo] -> ShowS
    TypedBindingInfo -> String
    (Int -> TypedBindingInfo -> ShowS)
    -> (TypedBindingInfo -> String)
    -> ([TypedBindingInfo] -> ShowS)
    -> Show TypedBindingInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TypedBindingInfo -> ShowS
    showsPrec :: Int -> TypedBindingInfo -> ShowS
    $cshow :: TypedBindingInfo -> String
    show :: TypedBindingInfo -> String
    $cshowList :: [TypedBindingInfo] -> ShowS
    showList :: [TypedBindingInfo] -> ShowS
    Show, TypedBindingInfo -> TypedBindingInfo -> Bool
    (TypedBindingInfo -> TypedBindingInfo -> Bool)
    -> (TypedBindingInfo -> TypedBindingInfo -> Bool)
    -> Eq TypedBindingInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TypedBindingInfo -> TypedBindingInfo -> Bool
    == :: TypedBindingInfo -> TypedBindingInfo -> Bool
    $c/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
    /= :: TypedBindingInfo -> TypedBindingInfo -> Bool
    Eq, (forall x. TypedBindingInfo -> Rep TypedBindingInfo x)
    -> (forall x. Rep TypedBindingInfo x -> TypedBindingInfo)
    -> Generic TypedBindingInfo
    forall x. Rep TypedBindingInfo x -> TypedBindingInfo
    forall x. TypedBindingInfo -> Rep TypedBindingInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TypedBindingInfo -> Rep TypedBindingInfo x
    from :: forall x. TypedBindingInfo -> Rep TypedBindingInfo x
    $cto :: forall x. Rep TypedBindingInfo x -> TypedBindingInfo
    to :: forall x. Rep TypedBindingInfo x -> TypedBindingInfo
    Generic)

    instance Null TypedBindingInfo where
      null :: TypedBindingInfo -> Bool
    null (TypedBindingInfo TacticAttribute
    tac Bool
    fin) = TacticAttribute -> Bool
    forall a. Null a => a -> Bool
    null TacticAttribute
    tac Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    fin
      empty :: TypedBindingInfo
    empty = TacticAttribute -> Bool -> TypedBindingInfo
    TypedBindingInfo TacticAttribute
    forall a. Null a => a
    empty Bool
    forall a. Null a => a
    empty

    -- | 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 TypedBindingInfo (List1 (NamedArg Binder)) Type
        -- ^ As in telescope @(x y z : A)@ or type @(x y z : A) -> B@.
      | TLet Range (List1 LetBinding)
        -- ^ E.g. @(let x = e)@ or @(let open M)@.
      deriving (Int -> TypedBinding -> ShowS
    Telescope -> ShowS
    TypedBinding -> String
    (Int -> TypedBinding -> ShowS)
    -> (TypedBinding -> String)
    -> (Telescope -> ShowS)
    -> Show TypedBinding
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TypedBinding -> ShowS
    showsPrec :: Int -> TypedBinding -> ShowS
    $cshow :: TypedBinding -> String
    show :: TypedBinding -> String
    $cshowList :: Telescope -> ShowS
    showList :: Telescope -> ShowS
    Show, TypedBinding -> TypedBinding -> Bool
    (TypedBinding -> TypedBinding -> Bool)
    -> (TypedBinding -> TypedBinding -> Bool) -> Eq TypedBinding
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TypedBinding -> TypedBinding -> Bool
    == :: TypedBinding -> TypedBinding -> Bool
    $c/= :: TypedBinding -> TypedBinding -> Bool
    /= :: TypedBinding -> TypedBinding -> Bool
    Eq, (forall x. TypedBinding -> Rep TypedBinding x)
    -> (forall x. Rep TypedBinding x -> TypedBinding)
    -> Generic TypedBinding
    forall x. Rep TypedBinding x -> TypedBinding
    forall x. TypedBinding -> Rep TypedBinding x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TypedBinding -> Rep TypedBinding x
    from :: forall x. TypedBinding -> Rep TypedBinding x
    $cto :: forall x. Rep TypedBinding x -> TypedBinding
    to :: forall x. Rep TypedBinding x -> TypedBinding
    Generic)

    mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
    mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
    mkTBind Range
    r = Range
    -> TypedBindingInfo
    -> List1 (NamedArg Binder)
    -> Expr
    -> TypedBinding
    TBind Range
    r TypedBindingInfo
    forall a. Null a => a
    empty

    mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
    mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
    mkTLet Range
    _ []     = Maybe TypedBinding
    forall a. Maybe a
    Nothing
    mkTLet Range
    r (LetBinding
    d:[LetBinding]
    ds) = TypedBinding -> Maybe TypedBinding
    forall a. a -> Maybe a
    Just (TypedBinding -> Maybe TypedBinding)
    -> TypedBinding -> Maybe TypedBinding
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 LetBinding -> TypedBinding
    TLet Range
    r (LetBinding
    d LetBinding -> [LetBinding] -> List1 LetBinding
    forall a. a -> [a] -> NonEmpty a
    :| [LetBinding]
    ds)

    type Telescope1 = List1 TypedBinding
    type Telescope  = [TypedBinding]

    mkPi :: ExprInfo -> Telescope -> Type -> Type
    mkPi :: ExprInfo -> Telescope -> Expr -> Expr
    mkPi ExprInfo
    i []     Expr
    e = Expr
    e
    mkPi ExprInfo
    i (TypedBinding
    x:Telescope
    xs) Expr
    e = ExprInfo -> Telescope1 -> Expr -> Expr
    Pi ExprInfo
    i (TypedBinding
    x TypedBinding -> Telescope -> Telescope1
    forall a. a -> [a] -> NonEmpty a
    :| Telescope
    xs) Expr
    e

    data GeneralizeTelescope = GeneralizeTel
      { GeneralizeTelescope -> Map QName Name
    generalizeTelVars :: Map QName Name
        -- ^ Maps generalize variables to the corresponding bound variable (to be
        --   introduced by the generalisation).
      , GeneralizeTelescope -> Telescope
    generalizeTel     :: Telescope }
      deriving (Int -> GeneralizeTelescope -> ShowS
    [GeneralizeTelescope] -> ShowS
    GeneralizeTelescope -> String
    (Int -> GeneralizeTelescope -> ShowS)
    -> (GeneralizeTelescope -> String)
    -> ([GeneralizeTelescope] -> ShowS)
    -> Show GeneralizeTelescope
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> GeneralizeTelescope -> ShowS
    showsPrec :: Int -> GeneralizeTelescope -> ShowS
    $cshow :: GeneralizeTelescope -> String
    show :: GeneralizeTelescope -> String
    $cshowList :: [GeneralizeTelescope] -> ShowS
    showList :: [GeneralizeTelescope] -> ShowS
    Show, GeneralizeTelescope -> GeneralizeTelescope -> Bool
    (GeneralizeTelescope -> GeneralizeTelescope -> Bool)
    -> (GeneralizeTelescope -> GeneralizeTelescope -> Bool)
    -> Eq GeneralizeTelescope
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
    == :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
    $c/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
    /= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
    Eq, (forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x)
    -> (forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope)
    -> Generic GeneralizeTelescope
    forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
    forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
    from :: forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
    $cto :: forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
    to :: forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
    Generic)

    data DataDefParams = DataDefParams
      { DataDefParams -> Set Name
    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]
    dataDefParams :: [LamBinding]
      }
      deriving (Int -> DataDefParams -> ShowS
    [DataDefParams] -> ShowS
    DataDefParams -> String
    (Int -> DataDefParams -> ShowS)
    -> (DataDefParams -> String)
    -> ([DataDefParams] -> ShowS)
    -> Show DataDefParams
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DataDefParams -> ShowS
    showsPrec :: Int -> DataDefParams -> ShowS
    $cshow :: DataDefParams -> String
    show :: DataDefParams -> String
    $cshowList :: [DataDefParams] -> ShowS
    showList :: [DataDefParams] -> ShowS
    Show, DataDefParams -> DataDefParams -> Bool
    (DataDefParams -> DataDefParams -> Bool)
    -> (DataDefParams -> DataDefParams -> Bool) -> Eq DataDefParams
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DataDefParams -> DataDefParams -> Bool
    == :: DataDefParams -> DataDefParams -> Bool
    $c/= :: DataDefParams -> DataDefParams -> Bool
    /= :: DataDefParams -> DataDefParams -> Bool
    Eq, (forall x. DataDefParams -> Rep DataDefParams x)
    -> (forall x. Rep DataDefParams x -> DataDefParams)
    -> Generic DataDefParams
    forall x. Rep DataDefParams x -> DataDefParams
    forall x. DataDefParams -> Rep DataDefParams x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DataDefParams -> Rep DataDefParams x
    from :: forall x. DataDefParams -> Rep DataDefParams x
    $cto :: forall x. Rep DataDefParams x -> DataDefParams
    to :: forall x. Rep DataDefParams x -> DataDefParams
    Generic)

    noDataDefParams :: DataDefParams
    noDataDefParams :: DataDefParams
    noDataDefParams = Set Name -> [LamBinding] -> DataDefParams
    DataDefParams Set Name
    forall a. Set a
    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.
    --    * User pattern is an annotated wildcard:
    --      type annotation will be checked after splitting is complete.
    data ProblemEq = ProblemEq
      { ProblemEq -> Pattern
    problemInPat :: Pattern
      , ProblemEq -> Term
    problemInst  :: I.Term
      , ProblemEq -> Dom Type
    problemType  :: I.Dom I.Type
      } deriving (Int -> ProblemEq -> ShowS
    [ProblemEq] -> ShowS
    ProblemEq -> String
    (Int -> ProblemEq -> ShowS)
    -> (ProblemEq -> String)
    -> ([ProblemEq] -> ShowS)
    -> Show ProblemEq
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ProblemEq -> ShowS
    showsPrec :: Int -> ProblemEq -> ShowS
    $cshow :: ProblemEq -> String
    show :: ProblemEq -> String
    $cshowList :: [ProblemEq] -> ShowS
    showList :: [ProblemEq] -> ShowS
    Show, (forall x. ProblemEq -> Rep ProblemEq x)
    -> (forall x. Rep ProblemEq x -> ProblemEq) -> Generic ProblemEq
    forall x. Rep ProblemEq x -> ProblemEq
    forall x. ProblemEq -> Rep ProblemEq x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ProblemEq -> Rep ProblemEq x
    from :: forall x. ProblemEq -> Rep ProblemEq x
    $cto :: forall x. Rep ProblemEq x -> ProblemEq
    to :: forall x. Rep ProblemEq x -> ProblemEq
    Generic)

    -- These are not relevant for caching purposes
    instance Eq ProblemEq where ProblemEq
    _ == :: ProblemEq -> ProblemEq -> Bool
    == ProblemEq
    _ = Bool
    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
      { forall lhs. Clause' lhs -> lhs
    clauseLHS        :: lhs
      , forall lhs. Clause' lhs -> [ProblemEq]
    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.
      , forall lhs. Clause' lhs -> RHS
    clauseRHS        :: RHS
      , forall lhs. Clause' lhs -> WhereDeclarations
    clauseWhereDecls :: WhereDeclarations
      , forall lhs. Clause' lhs -> Catchall
    clauseCatchall   :: Catchall
      } deriving (Int -> Clause' lhs -> ShowS
    [Clause' lhs] -> ShowS
    Clause' lhs -> String
    (Int -> Clause' lhs -> ShowS)
    -> (Clause' lhs -> String)
    -> ([Clause' lhs] -> ShowS)
    -> Show (Clause' lhs)
    forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
    forall lhs. Show lhs => [Clause' lhs] -> ShowS
    forall lhs. Show lhs => Clause' lhs -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
    showsPrec :: Int -> Clause' lhs -> ShowS
    $cshow :: forall lhs. Show lhs => Clause' lhs -> String
    show :: Clause' lhs -> String
    $cshowList :: forall lhs. Show lhs => [Clause' lhs] -> ShowS
    showList :: [Clause' lhs] -> ShowS
    Show, (forall a b. (a -> b) -> Clause' a -> Clause' b)
    -> (forall a b. a -> Clause' b -> Clause' a) -> Functor Clause'
    forall a b. a -> Clause' b -> Clause' a
    forall a b. (a -> b) -> Clause' a -> Clause' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
    fmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
    $c<$ :: forall a b. a -> Clause' b -> Clause' a
    <$ :: forall a b. a -> Clause' b -> Clause' a
    Functor, (forall m. Monoid m => Clause' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Clause' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Clause' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Clause' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Clause' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Clause' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Clause' a -> b)
    -> (forall a. (a -> a -> a) -> Clause' a -> a)
    -> (forall a. (a -> a -> a) -> Clause' a -> a)
    -> (forall a. Clause' a -> [a])
    -> (forall a. Clause' a -> Bool)
    -> (forall a. Clause' a -> Int)
    -> (forall a. Eq a => a -> Clause' a -> Bool)
    -> (forall a. Ord a => Clause' a -> a)
    -> (forall a. Ord a => Clause' a -> a)
    -> (forall a. Num a => Clause' a -> a)
    -> (forall a. Num a => Clause' a -> a)
    -> Foldable Clause'
    forall a. Eq a => a -> Clause' a -> Bool
    forall a. Num a => Clause' a -> a
    forall a. Ord a => Clause' a -> a
    forall m. Monoid m => Clause' m -> m
    forall a. Clause' a -> Bool
    forall a. Clause' a -> Int
    forall a. Clause' a -> [a]
    forall a. (a -> a -> a) -> Clause' a -> a
    forall m a. Monoid m => (a -> m) -> Clause' a -> m
    forall b a. (b -> a -> b) -> b -> Clause' a -> b
    forall a b. (a -> b -> b) -> b -> Clause' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Clause' m -> m
    fold :: forall m. Monoid m => Clause' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
    $ctoList :: forall a. Clause' a -> [a]
    toList :: forall a. Clause' a -> [a]
    $cnull :: forall a. Clause' a -> Bool
    null :: forall a. Clause' a -> Bool
    $clength :: forall a. Clause' a -> Int
    length :: forall a. Clause' a -> Int
    $celem :: forall a. Eq a => a -> Clause' a -> Bool
    elem :: forall a. Eq a => a -> Clause' a -> Bool
    $cmaximum :: forall a. Ord a => Clause' a -> a
    maximum :: forall a. Ord a => Clause' a -> a
    $cminimum :: forall a. Ord a => Clause' a -> a
    minimum :: forall a. Ord a => Clause' a -> a
    $csum :: forall a. Num a => Clause' a -> a
    sum :: forall a. Num a => Clause' a -> a
    $cproduct :: forall a. Num a => Clause' a -> a
    product :: forall a. Num a => Clause' a -> a
    Foldable, Functor Clause'
    Foldable Clause'
    (Functor Clause', Foldable Clause') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Clause' a -> f (Clause' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Clause' (f a) -> f (Clause' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Clause' a -> m (Clause' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Clause' (m a) -> m (Clause' a))
    -> Traversable Clause'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Clause' (f a) -> f (Clause' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Clause' a -> m (Clause' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Clause' a -> f (Clause' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Clause' a -> f (Clause' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Clause' a -> f (Clause' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Clause' (f a) -> f (Clause' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Clause' (f a) -> f (Clause' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Clause' a -> m (Clause' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Clause' a -> m (Clause' b)
    $csequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
    sequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
    Traversable, Clause' lhs -> Clause' lhs -> Bool
    (Clause' lhs -> Clause' lhs -> Bool)
    -> (Clause' lhs -> Clause' lhs -> Bool) -> Eq (Clause' lhs)
    forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
    == :: Clause' lhs -> Clause' lhs -> Bool
    $c/= :: forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
    /= :: Clause' lhs -> Clause' lhs -> Bool
    Eq, (forall x. Clause' lhs -> Rep (Clause' lhs) x)
    -> (forall x. Rep (Clause' lhs) x -> Clause' lhs)
    -> Generic (Clause' lhs)
    forall x. Rep (Clause' lhs) x -> Clause' lhs
    forall x. Clause' lhs -> Rep (Clause' lhs) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
    forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
    $cfrom :: forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
    from :: forall x. Clause' lhs -> Rep (Clause' lhs) x
    $cto :: forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
    to :: forall x. Rep (Clause' lhs) x -> Clause' lhs
    Generic)

    data WhereDeclarations = WhereDecls
      { WhereDeclarations -> Maybe ModuleName
    whereModule :: Maybe ModuleName
          -- #2897: we need to restrict named where modules in refined contexts,
          --        so remember whether it was named here
      , WhereDeclarations -> Bool
    whereAnywhere :: Bool
          -- ^ is it an ordinary unnamed @where@?
      , WhereDeclarations -> Maybe Declaration
    whereDecls :: Maybe Declaration
          -- ^ The declaration is a 'Section'.
      } deriving (Int -> WhereDeclarations -> ShowS
    [WhereDeclarations] -> ShowS
    WhereDeclarations -> String
    (Int -> WhereDeclarations -> ShowS)
    -> (WhereDeclarations -> String)
    -> ([WhereDeclarations] -> ShowS)
    -> Show WhereDeclarations
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> WhereDeclarations -> ShowS
    showsPrec :: Int -> WhereDeclarations -> ShowS
    $cshow :: WhereDeclarations -> String
    show :: WhereDeclarations -> String
    $cshowList :: [WhereDeclarations] -> ShowS
    showList :: [WhereDeclarations] -> ShowS
    Show, WhereDeclarations -> WhereDeclarations -> Bool
    (WhereDeclarations -> WhereDeclarations -> Bool)
    -> (WhereDeclarations -> WhereDeclarations -> Bool)
    -> Eq WhereDeclarations
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: WhereDeclarations -> WhereDeclarations -> Bool
    == :: WhereDeclarations -> WhereDeclarations -> Bool
    $c/= :: WhereDeclarations -> WhereDeclarations -> Bool
    /= :: WhereDeclarations -> WhereDeclarations -> Bool
    Eq, (forall x. WhereDeclarations -> Rep WhereDeclarations x)
    -> (forall x. Rep WhereDeclarations x -> WhereDeclarations)
    -> Generic WhereDeclarations
    forall x. Rep WhereDeclarations x -> WhereDeclarations
    forall x. WhereDeclarations -> Rep WhereDeclarations x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. WhereDeclarations -> Rep WhereDeclarations x
    from :: forall x. WhereDeclarations -> Rep WhereDeclarations x
    $cto :: forall x. Rep WhereDeclarations x -> WhereDeclarations
    to :: forall x. Rep WhereDeclarations x -> WhereDeclarations
    Generic)

    instance Null WhereDeclarations where
      empty :: WhereDeclarations
    empty = Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
    WhereDecls Maybe ModuleName
    forall a. Null a => a
    empty Bool
    False Maybe Declaration
    forall a. Null a => a
    empty

    noWhereDecls :: WhereDeclarations
    noWhereDecls :: WhereDeclarations
    noWhereDecls = WhereDeclarations
    forall a. Null a => a
    empty

    type Clause = Clause' LHS
    type SpineClause = Clause' SpineLHS
    type RewriteEqn  = RewriteEqn' QName BindName Pattern Expr
    type WithExpr' e = Named BindName (Arg e)
    type WithExpr    = WithExpr' Expr

    data RHS
      = RHS
        { RHS -> Expr
    rhsExpr     :: Expr
        , RHS -> Maybe 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 (List1 WithExpr) (List1 Clause)
          -- ^ The 'QName' is the name of the with function.
      | RewriteRHS
        { RHS -> [RewriteEqn]
    rewriteExprs      :: [RewriteEqn]
          -- ^ The 'QName's are the names of the generated with functions,
          --   one for each 'Expr'.
        , RHS -> [ProblemEq]
    rewriteStrippedPats :: [ProblemEq]
          -- ^ The patterns stripped by with-desugaring. These are only present
          --   if this rewrite follows a with.
        , RHS -> RHS
    rewriteRHS        :: RHS
          -- ^ The RHS should not be another @RewriteRHS@.
        , RHS -> WhereDeclarations
    rewriteWhereDecls :: WhereDeclarations
          -- ^ The where clauses are attached to the @RewriteRHS@ by
          ---  the scope checker (instead of to the clause).
        }
      deriving (Int -> RHS -> ShowS
    [RHS] -> ShowS
    RHS -> String
    (Int -> RHS -> ShowS)
    -> (RHS -> String) -> ([RHS] -> ShowS) -> Show RHS
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RHS -> ShowS
    showsPrec :: Int -> RHS -> ShowS
    $cshow :: RHS -> String
    show :: RHS -> String
    $cshowList :: [RHS] -> ShowS
    showList :: [RHS] -> ShowS
    Show, (forall x. RHS -> Rep RHS x)
    -> (forall x. Rep RHS x -> RHS) -> Generic RHS
    forall x. Rep RHS x -> RHS
    forall x. RHS -> Rep RHS x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. RHS -> Rep RHS x
    from :: forall x. RHS -> Rep RHS x
    $cto :: forall x. Rep RHS x -> RHS
    to :: forall x. Rep RHS x -> RHS
    Generic)

    -- | Ignore 'rhsConcrete' when comparing 'RHS's.
    instance Eq RHS where
      RHS Expr
    e Maybe Expr
    _          == :: RHS -> RHS -> Bool
    == RHS Expr
    e' Maybe Expr
    _            = Expr
    e Expr -> Expr -> Bool
    forall a. Eq a => a -> a -> Bool
    == Expr
    e'
      RHS
    AbsurdRHS        == RHS
    AbsurdRHS           = Bool
    True
      WithRHS QName
    a List1 WithExpr
    b List1 Clause
    c    == WithRHS QName
    a' List1 WithExpr
    b' List1 Clause
    c'    = (QName
    a QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    a') Bool -> Bool -> Bool
    && (List1 WithExpr
    b List1 WithExpr -> List1 WithExpr -> Bool
    forall a. Eq a => a -> a -> Bool
    == List1 WithExpr
    b') Bool -> Bool -> Bool
    && (List1 Clause
    c List1 Clause -> List1 Clause -> Bool
    forall a. Eq a => a -> a -> Bool
    == List1 Clause
    c')
      RewriteRHS [RewriteEqn]
    a [ProblemEq]
    b RHS
    c WhereDeclarations
    d == RewriteRHS [RewriteEqn]
    a' [ProblemEq]
    b' RHS
    c' WhereDeclarations
    d' = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [ [RewriteEqn]
    a [RewriteEqn] -> [RewriteEqn] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [RewriteEqn]
    a', [ProblemEq]
    b [ProblemEq] -> [ProblemEq] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [ProblemEq]
    b', RHS
    c RHS -> RHS -> Bool
    forall a. Eq a => a -> a -> Bool
    == RHS
    c' , WhereDeclarations
    d WhereDeclarations -> WhereDeclarations -> Bool
    forall a. Eq a => a -> a -> Bool
    == WhereDeclarations
    d' ]
      RHS
    _                == RHS
    _                   = Bool
    False

    -- | The lhs of a clause in spine view (inside-out).
    --   Projection patterns are contained in @spLhsPats@,
    --   represented as @ProjP d@.
    data SpineLHS = SpineLHS
      { SpineLHS -> LHSInfo
    spLhsInfo     :: LHSInfo             -- ^ Range.
      , SpineLHS -> QName
    spLhsDefName  :: QName               -- ^ Name of function we are defining.
      , SpineLHS -> [NamedArg Pattern]
    spLhsPats     :: [NamedArg Pattern]  -- ^ Elimination by pattern, projections, with-patterns.
      }
      deriving (Int -> SpineLHS -> ShowS
    [SpineLHS] -> ShowS
    SpineLHS -> String
    (Int -> SpineLHS -> ShowS)
    -> (SpineLHS -> String) -> ([SpineLHS] -> ShowS) -> Show SpineLHS
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SpineLHS -> ShowS
    showsPrec :: Int -> SpineLHS -> ShowS
    $cshow :: SpineLHS -> String
    show :: SpineLHS -> String
    $cshowList :: [SpineLHS] -> ShowS
    showList :: [SpineLHS] -> ShowS
    Show, SpineLHS -> SpineLHS -> Bool
    (SpineLHS -> SpineLHS -> Bool)
    -> (SpineLHS -> SpineLHS -> Bool) -> Eq SpineLHS
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SpineLHS -> SpineLHS -> Bool
    == :: SpineLHS -> SpineLHS -> Bool
    $c/= :: SpineLHS -> SpineLHS -> Bool
    /= :: SpineLHS -> SpineLHS -> Bool
    Eq, (forall x. SpineLHS -> Rep SpineLHS x)
    -> (forall x. Rep SpineLHS x -> SpineLHS) -> Generic SpineLHS
    forall x. Rep SpineLHS x -> SpineLHS
    forall x. SpineLHS -> Rep SpineLHS x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. SpineLHS -> Rep SpineLHS x
    from :: forall x. SpineLHS -> Rep SpineLHS x
    $cto :: forall x. Rep SpineLHS x -> SpineLHS
    to :: forall x. Rep SpineLHS x -> SpineLHS
    Generic)

    -- | Ignore 'Range' when comparing 'LHS's.
    instance Eq LHS where
      LHS LHSInfo
    _ LHSCore
    core == :: LHS -> LHS -> Bool
    == LHS LHSInfo
    _ LHSCore
    core' = LHSCore
    core LHSCore -> LHSCore -> Bool
    forall a. Eq a => a -> a -> Bool
    == LHSCore
    core'

    -- | The lhs of a clause in focused (projection-application) view (outside-in).
    --   Projection patters are represented as 'LHSProj's.
    data LHS = LHS
      { LHS -> LHSInfo
    lhsInfo     :: LHSInfo               -- ^ Range.
      , LHS -> LHSCore
    lhsCore     :: LHSCore               -- ^ Copatterns.
      }
      deriving (Int -> LHS -> ShowS
    [LHS] -> ShowS
    LHS -> String
    (Int -> LHS -> ShowS)
    -> (LHS -> String) -> ([LHS] -> ShowS) -> Show LHS
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> LHS -> ShowS
    showsPrec :: Int -> LHS -> ShowS
    $cshow :: LHS -> String
    show :: LHS -> String
    $cshowList :: [LHS] -> ShowS
    showList :: [LHS] -> ShowS
    Show, (forall x. LHS -> Rep LHS x)
    -> (forall x. Rep LHS x -> LHS) -> Generic LHS
    forall x. Rep LHS x -> LHS
    forall x. LHS -> Rep LHS x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LHS -> Rep LHS x
    from :: forall x. LHS -> Rep LHS x
    $cto :: forall x. Rep LHS x -> LHS
    to :: forall x. Rep LHS x -> LHS
    Generic)

    -- | 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  { forall e. LHSCore' e -> QName
    lhsDefName  :: QName
                     -- ^ Head @f@.
                 , forall e. LHSCore' e -> [NamedArg (Pattern' e)]
    lhsPats     :: [NamedArg (Pattern' e)]
                     -- ^ Applied to patterns @ps@.
                 }
        -- | Projection.
      | LHSProj  { forall e. LHSCore' e -> AmbiguousQName
    lhsDestructor :: AmbiguousQName
                     -- ^ Record projection identifier.
                 , forall e. LHSCore' e -> NamedArg (LHSCore' e)
    lhsFocus      :: NamedArg (LHSCore' e)
                     -- ^ Main argument of projection.
                 , lhsPats       :: [NamedArg (Pattern' e)]
                     -- ^ Further applied to patterns.
                 }
        -- | With patterns.
      | LHSWith  { forall e. LHSCore' e -> LHSCore' e
    lhsHead         :: LHSCore' e
                     -- ^ E.g. the 'LHSHead'.
                 , forall e. LHSCore' e -> List1 (Arg (Pattern' e))
    lhsWithPatterns :: List1 (Arg (Pattern' e))
                     -- ^ Applied to with patterns @| p1 | ... | pn@.
                     --   These patterns are not prefixed with @WithP@!
                 , lhsPats         :: [NamedArg (Pattern' e)]
                     -- ^ Further applied to patterns.
                 }
      deriving (Int -> LHSCore' e -> ShowS
    [LHSCore' e] -> ShowS
    LHSCore' e -> String
    (Int -> LHSCore' e -> ShowS)
    -> (LHSCore' e -> String)
    -> ([LHSCore' e] -> ShowS)
    -> Show (LHSCore' e)
    forall e. Show e => Int -> LHSCore' e -> ShowS
    forall e. Show e => [LHSCore' e] -> ShowS
    forall e. Show e => LHSCore' e -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall e. Show e => Int -> LHSCore' e -> ShowS
    showsPrec :: Int -> LHSCore' e -> ShowS
    $cshow :: forall e. Show e => LHSCore' e -> String
    show :: LHSCore' e -> String
    $cshowList :: forall e. Show e => [LHSCore' e] -> ShowS
    showList :: [LHSCore' e] -> ShowS
    Show, (forall a b. (a -> b) -> LHSCore' a -> LHSCore' b)
    -> (forall a b. a -> LHSCore' b -> LHSCore' a) -> Functor LHSCore'
    forall a b. a -> LHSCore' b -> LHSCore' a
    forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
    fmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
    $c<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
    <$ :: forall a b. a -> LHSCore' b -> LHSCore' a
    Functor, (forall m. Monoid m => LHSCore' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> LHSCore' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> LHSCore' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> LHSCore' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> LHSCore' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> LHSCore' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> LHSCore' a -> b)
    -> (forall a. (a -> a -> a) -> LHSCore' a -> a)
    -> (forall a. (a -> a -> a) -> LHSCore' a -> a)
    -> (forall a. LHSCore' a -> [a])
    -> (forall a. LHSCore' a -> Bool)
    -> (forall a. LHSCore' a -> Int)
    -> (forall a. Eq a => a -> LHSCore' a -> Bool)
    -> (forall a. Ord a => LHSCore' a -> a)
    -> (forall a. Ord a => LHSCore' a -> a)
    -> (forall a. Num a => LHSCore' a -> a)
    -> (forall a. Num a => LHSCore' a -> a)
    -> Foldable LHSCore'
    forall a. Eq a => a -> LHSCore' a -> Bool
    forall a. Num a => LHSCore' a -> a
    forall a. Ord a => LHSCore' a -> a
    forall m. Monoid m => LHSCore' m -> m
    forall a. LHSCore' a -> Bool
    forall a. LHSCore' a -> Int
    forall a. LHSCore' a -> [a]
    forall a. (a -> a -> a) -> LHSCore' a -> a
    forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
    forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
    forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => LHSCore' m -> m
    fold :: forall m. Monoid m => LHSCore' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
    foldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
    foldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
    $ctoList :: forall a. LHSCore' a -> [a]
    toList :: forall a. LHSCore' a -> [a]
    $cnull :: forall a. LHSCore' a -> Bool
    null :: forall a. LHSCore' a -> Bool
    $clength :: forall a. LHSCore' a -> Int
    length :: forall a. LHSCore' a -> Int
    $celem :: forall a. Eq a => a -> LHSCore' a -> Bool
    elem :: forall a. Eq a => a -> LHSCore' a -> Bool
    $cmaximum :: forall a. Ord a => LHSCore' a -> a
    maximum :: forall a. Ord a => LHSCore' a -> a
    $cminimum :: forall a. Ord a => LHSCore' a -> a
    minimum :: forall a. Ord a => LHSCore' a -> a
    $csum :: forall a. Num a => LHSCore' a -> a
    sum :: forall a. Num a => LHSCore' a -> a
    $cproduct :: forall a. Num a => LHSCore' a -> a
    product :: forall a. Num a => LHSCore' a -> a
    Foldable, Functor LHSCore'
    Foldable LHSCore'
    (Functor LHSCore', Foldable LHSCore') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> LHSCore' a -> f (LHSCore' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        LHSCore' (f a) -> f (LHSCore' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> LHSCore' a -> m (LHSCore' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        LHSCore' (m a) -> m (LHSCore' a))
    -> Traversable LHSCore'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
    forall (f :: * -> *) a.
    Applicative f =>
    LHSCore' (f a) -> f (LHSCore' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LHSCore' a -> m (LHSCore' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LHSCore' a -> f (LHSCore' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LHSCore' a -> f (LHSCore' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LHSCore' a -> f (LHSCore' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    LHSCore' (f a) -> f (LHSCore' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    LHSCore' (f a) -> f (LHSCore' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LHSCore' a -> m (LHSCore' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LHSCore' a -> m (LHSCore' b)
    $csequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
    sequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
    Traversable, LHSCore' e -> LHSCore' e -> Bool
    (LHSCore' e -> LHSCore' e -> Bool)
    -> (LHSCore' e -> LHSCore' e -> Bool) -> Eq (LHSCore' e)
    forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
    == :: LHSCore' e -> LHSCore' e -> Bool
    $c/= :: forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
    /= :: LHSCore' e -> LHSCore' e -> Bool
    Eq, (forall x. LHSCore' e -> Rep (LHSCore' e) x)
    -> (forall x. Rep (LHSCore' e) x -> LHSCore' e)
    -> Generic (LHSCore' e)
    forall x. Rep (LHSCore' e) x -> LHSCore' e
    forall x. LHSCore' e -> Rep (LHSCore' e) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall e x. Rep (LHSCore' e) x -> LHSCore' e
    forall e x. LHSCore' e -> Rep (LHSCore' e) x
    $cfrom :: forall e x. LHSCore' e -> Rep (LHSCore' e) x
    from :: forall x. LHSCore' e -> Rep (LHSCore' e) x
    $cto :: forall e x. Rep (LHSCore' e) x -> LHSCore' e
    to :: forall x. Rep (LHSCore' e) x -> LHSCore' e
    Generic)

    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 PatInfo Literal
      | PatternSynP PatInfo AmbiguousQName (NAPs e)
      | RecP KwRange ConPatInfo [FieldAssignment' (Pattern' e)]
      | EqualP PatInfo (List1 (e, e))
      | WithP PatInfo (Pattern' e)  -- ^ @| p@, for with-patterns.
      deriving (Int -> Pattern' e -> ShowS
    [Pattern' e] -> ShowS
    Pattern' e -> String
    (Int -> Pattern' e -> ShowS)
    -> (Pattern' e -> String)
    -> ([Pattern' e] -> ShowS)
    -> Show (Pattern' e)
    forall e. Show e => Int -> Pattern' e -> ShowS
    forall e. Show e => [Pattern' e] -> ShowS
    forall e. Show e => Pattern' e -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall e. Show e => Int -> Pattern' e -> ShowS
    showsPrec :: Int -> Pattern' e -> ShowS
    $cshow :: forall e. Show e => Pattern' e -> String
    show :: Pattern' e -> String
    $cshowList :: forall e. Show e => [Pattern' e] -> ShowS
    showList :: [Pattern' e] -> ShowS
    Show, (forall a b. (a -> b) -> Pattern' a -> Pattern' b)
    -> (forall a b. a -> Pattern' b -> Pattern' a) -> Functor Pattern'
    forall a b. a -> Pattern' b -> Pattern' a
    forall a b. (a -> b) -> Pattern' a -> Pattern' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
    fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
    $c<$ :: forall a b. a -> Pattern' b -> Pattern' a
    <$ :: forall a b. a -> Pattern' b -> Pattern' a
    Functor, (forall m. Monoid m => Pattern' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
    -> (forall a. (a -> a -> a) -> Pattern' a -> a)
    -> (forall a. (a -> a -> a) -> Pattern' a -> a)
    -> (forall a. Pattern' a -> [a])
    -> (forall a. Pattern' a -> Bool)
    -> (forall a. Pattern' a -> Int)
    -> (forall a. Eq a => a -> Pattern' a -> Bool)
    -> (forall a. Ord a => Pattern' a -> a)
    -> (forall a. Ord a => Pattern' a -> a)
    -> (forall a. Num a => Pattern' a -> a)
    -> (forall a. Num a => Pattern' a -> a)
    -> Foldable Pattern'
    forall a. Eq a => a -> Pattern' a -> Bool
    forall a. Num a => Pattern' a -> a
    forall a. Ord a => Pattern' a -> a
    forall m. Monoid m => Pattern' m -> m
    forall a. Pattern' a -> Bool
    forall a. Pattern' a -> Int
    forall a. Pattern' a -> [a]
    forall a. (a -> a -> a) -> Pattern' a -> a
    forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Pattern' m -> m
    fold :: forall m. Monoid m => Pattern' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
    $ctoList :: forall a. Pattern' a -> [a]
    toList :: forall a. Pattern' a -> [a]
    $cnull :: forall a. Pattern' a -> Bool
    null :: forall a. Pattern' a -> Bool
    $clength :: forall a. Pattern' a -> Int
    length :: forall a. Pattern' a -> Int
    $celem :: forall a. Eq a => a -> Pattern' a -> Bool
    elem :: forall a. Eq a => a -> Pattern' a -> Bool
    $cmaximum :: forall a. Ord a => Pattern' a -> a
    maximum :: forall a. Ord a => Pattern' a -> a
    $cminimum :: forall a. Ord a => Pattern' a -> a
    minimum :: forall a. Ord a => Pattern' a -> a
    $csum :: forall a. Num a => Pattern' a -> a
    sum :: forall a. Num a => Pattern' a -> a
    $cproduct :: forall a. Num a => Pattern' a -> a
    product :: forall a. Num a => Pattern' a -> a
    Foldable, Functor Pattern'
    Foldable Pattern'
    (Functor Pattern', Foldable Pattern') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Pattern' a -> f (Pattern' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Pattern' (f a) -> f (Pattern' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Pattern' a -> m (Pattern' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Pattern' (m a) -> m (Pattern' a))
    -> Traversable Pattern'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pattern' a -> f (Pattern' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pattern' a -> f (Pattern' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Pattern' a -> f (Pattern' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b)
    $csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
    sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
    Traversable, Pattern' e -> Pattern' e -> Bool
    (Pattern' e -> Pattern' e -> Bool)
    -> (Pattern' e -> Pattern' e -> Bool) -> Eq (Pattern' e)
    forall e. Eq e => Pattern' e -> Pattern' e -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall e. Eq e => Pattern' e -> Pattern' e -> Bool
    == :: Pattern' e -> Pattern' e -> Bool
    $c/= :: forall e. Eq e => Pattern' e -> Pattern' e -> Bool
    /= :: Pattern' e -> Pattern' e -> Bool
    Eq, (forall x. Pattern' e -> Rep (Pattern' e) x)
    -> (forall x. Rep (Pattern' e) x -> Pattern' e)
    -> Generic (Pattern' e)
    forall x. Rep (Pattern' e) x -> Pattern' e
    forall x. Pattern' e -> Rep (Pattern' e) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall e x. Rep (Pattern' e) x -> Pattern' e
    forall e x. Pattern' e -> Rep (Pattern' e) x
    $cfrom :: forall e x. Pattern' e -> Rep (Pattern' e) x
    from :: forall x. Pattern' e -> Rep (Pattern' e) x
    $cto :: forall e x. Rep (Pattern' e) x -> Pattern' e
    to :: forall x. Rep (Pattern' e) x -> Pattern' e
    Generic)

    type NAPs e   = [NamedArg (Pattern' e)]
    type NAPs1 e  = List1 (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 :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP (ProjP PatInfo
    _ ProjOrigin
    o AmbiguousQName
    d) = (ProjOrigin, AmbiguousQName) -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. a -> Maybe a
    Just (ProjOrigin
    o, AmbiguousQName
    d)
      isProjP Pattern' e
    _ = Maybe (ProjOrigin, AmbiguousQName)
    forall a. Maybe a
    Nothing

    instance IsProjP Expr where
      isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP (Proj ProjOrigin
    o AmbiguousQName
    ds)      = (ProjOrigin, AmbiguousQName) -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. a -> Maybe a
    Just (ProjOrigin
    o, AmbiguousQName
    ds)
      isProjP (ScopedExpr ScopeInfo
    _ Expr
    e) = Expr -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP Expr
    e
      isProjP Expr
    _ = Maybe (ProjOrigin, AmbiguousQName)
    forall a. Maybe a
    Nothing

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

    type HoleContent = C.HoleContent' () BindName Pattern Expr

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

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

    instance Eq Expr where
      ScopedExpr ScopeInfo
    _ Expr
    a1            == :: Expr -> Expr -> Bool
    == ScopedExpr ScopeInfo
    _ Expr
    a2            = Expr
    a1 Expr -> Expr -> Bool
    forall a. Eq a => a -> a -> Bool
    == Expr
    a2

      Var Name
    a1                     == Var Name
    a2                     = Name
    a1 Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    a2
      Def' QName
    a1 Suffix
    s1                 == Def' QName
    a2 Suffix
    s2                 = (QName
    a1, Suffix
    s1) (QName, Suffix) -> (QName, Suffix) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (QName
    a2, Suffix
    s2)
      Proj ProjOrigin
    _ AmbiguousQName
    a1                  == Proj ProjOrigin
    _ AmbiguousQName
    a2                  = AmbiguousQName
    a1 AmbiguousQName -> AmbiguousQName -> Bool
    forall a. Eq a => a -> a -> Bool
    == AmbiguousQName
    a2
      Con AmbiguousQName
    a1                     == Con AmbiguousQName
    a2                     = AmbiguousQName
    a1 AmbiguousQName -> AmbiguousQName -> Bool
    forall a. Eq a => a -> a -> Bool
    == AmbiguousQName
    a2
      PatternSyn AmbiguousQName
    a1              == PatternSyn AmbiguousQName
    a2              = AmbiguousQName
    a1 AmbiguousQName -> AmbiguousQName -> Bool
    forall a. Eq a => a -> a -> Bool
    == AmbiguousQName
    a2
      Macro QName
    a1                   == Macro QName
    a2                   = QName
    a1 QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    a2
      Lit ExprInfo
    r1 Literal
    a1                  == Lit ExprInfo
    r2 Literal
    a2                  = (ExprInfo
    r1, Literal
    a1) (ExprInfo, Literal) -> (ExprInfo, Literal) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    r2, Literal
    a2)
      QuestionMark MetaInfo
    a1 InteractionId
    b1         == QuestionMark MetaInfo
    a2 InteractionId
    b2         = (MetaInfo
    a1, InteractionId
    b1) (MetaInfo, InteractionId) -> (MetaInfo, InteractionId) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (MetaInfo
    a2, InteractionId
    b2)
      Underscore MetaInfo
    a1              == Underscore MetaInfo
    a2              = MetaInfo
    a1 MetaInfo -> MetaInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaInfo
    a2
      Dot ExprInfo
    r1 Expr
    e1                  == Dot ExprInfo
    r2 Expr
    e2                  = (ExprInfo
    r1, Expr
    e1) (ExprInfo, Expr) -> (ExprInfo, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    r2, Expr
    e2)
      App AppInfo
    a1 Expr
    b1 NamedArg Expr
    c1               == App AppInfo
    a2 Expr
    b2 NamedArg Expr
    c2               = (AppInfo
    a1, Expr
    b1, NamedArg Expr
    c1) (AppInfo, Expr, NamedArg Expr)
    -> (AppInfo, Expr, NamedArg Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (AppInfo
    a2, Expr
    b2, NamedArg Expr
    c2)
      WithApp ExprInfo
    a1 Expr
    b1 List1 Expr
    c1           == WithApp ExprInfo
    a2 Expr
    b2 List1 Expr
    c2           = (ExprInfo
    a1, Expr
    b1, List1 Expr
    c1) (ExprInfo, Expr, List1 Expr)
    -> (ExprInfo, Expr, List1 Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    a2, Expr
    b2, List1 Expr
    c2)
      Lam ExprInfo
    a1 LamBinding
    b1 Expr
    c1               == Lam ExprInfo
    a2 LamBinding
    b2 Expr
    c2               = (ExprInfo
    a1, LamBinding
    b1, Expr
    c1) (ExprInfo, LamBinding, Expr)
    -> (ExprInfo, LamBinding, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    a2, LamBinding
    b2, Expr
    c2)
      AbsurdLam ExprInfo
    a1 Hiding
    b1            == AbsurdLam ExprInfo
    a2 Hiding
    b2            = (ExprInfo
    a1, Hiding
    b1) (ExprInfo, Hiding) -> (ExprInfo, Hiding) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    a2, Hiding
    b2)
      ExtendedLam ExprInfo
    a1 DefInfo
    b1 Erased
    c1 QName
    d1 List1 Clause
    e1 == ExtendedLam ExprInfo
    a2 DefInfo
    b2 Erased
    c2 QName
    d2 List1 Clause
    e2 = (ExprInfo
    a1, DefInfo
    b1, Erased
    c1, QName
    d1, List1 Clause
    e1) (ExprInfo, DefInfo, Erased, QName, List1 Clause)
    -> (ExprInfo, DefInfo, Erased, QName, List1 Clause) -> Bool
    forall a. Eq a => a -> a -> Bool
    ==
                                                                 (ExprInfo
    a2, DefInfo
    b2, Erased
    c2, QName
    d2, List1 Clause
    e2)
      Pi ExprInfo
    a1 Telescope1
    b1 Expr
    c1                == Pi ExprInfo
    a2 Telescope1
    b2 Expr
    c2                = (ExprInfo
    a1, Telescope1
    b1, Expr
    c1) (ExprInfo, Telescope1, Expr)
    -> (ExprInfo, Telescope1, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    a2, Telescope1
    b2, Expr
    c2)
      Generalized Set1 QName
    a1 Expr
    b1          == Generalized Set1 QName
    a2 Expr
    b2          = (Set1 QName
    a1, Expr
    b1) (Set1 QName, Expr) -> (Set1 QName, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Set1 QName
    a2, Expr
    b2)
      Fun ExprInfo
    a1 Arg Expr
    b1 Expr
    c1               == Fun ExprInfo
    a2 Arg Expr
    b2 Expr
    c2               = (ExprInfo
    a1, Arg Expr
    b1, Expr
    c1) (ExprInfo, Arg Expr, Expr) -> (ExprInfo, Arg Expr, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    a2, Arg Expr
    b2, Expr
    c2)
      Let ExprInfo
    a1 List1 LetBinding
    b1 Expr
    c1               == Let ExprInfo
    a2 List1 LetBinding
    b2 Expr
    c2               = (ExprInfo
    a1, List1 LetBinding
    b1, Expr
    c1) (ExprInfo, List1 LetBinding, Expr)
    -> (ExprInfo, List1 LetBinding, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ExprInfo
    a2, List1 LetBinding
    b2, Expr
    c2)
      Rec KwRange
    r1 ExprInfo
    a1 RecordAssigns
    b1               == Rec KwRange
    r2 ExprInfo
    a2 RecordAssigns
    b2               = (KwRange
    r1, ExprInfo
    a1, RecordAssigns
    b1) (KwRange, ExprInfo, RecordAssigns)
    -> (KwRange, ExprInfo, RecordAssigns) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (KwRange
    r2, ExprInfo
    a2, RecordAssigns
    b2)
      RecUpdate KwRange
    r1 ExprInfo
    a1 Expr
    b1 Assigns
    c1      == RecUpdate KwRange
    r2 ExprInfo
    a2 Expr
    b2 Assigns
    c2      = (KwRange
    r1, ExprInfo
    a1, Expr
    b1, Assigns
    c1) (KwRange, ExprInfo, Expr, Assigns)
    -> (KwRange, ExprInfo, Expr, Assigns) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (KwRange
    r2, ExprInfo
    a2, Expr
    b2, Assigns
    c2)
      Quote ExprInfo
    a1                   == Quote ExprInfo
    a2                   = ExprInfo
    a1 ExprInfo -> ExprInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExprInfo
    a2
      QuoteTerm ExprInfo
    a1               == QuoteTerm ExprInfo
    a2               = ExprInfo
    a1 ExprInfo -> ExprInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExprInfo
    a2
      Unquote ExprInfo
    a1                 == Unquote ExprInfo
    a2                 = ExprInfo
    a1 ExprInfo -> ExprInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExprInfo
    a2
      DontCare Expr
    a1                == DontCare Expr
    a2                = Expr
    a1 Expr -> Expr -> Bool
    forall a. Eq a => a -> a -> Bool
    == Expr
    a2

      Expr
    _                          == Expr
    _                          = Bool
    False

    -- | Does not compare 'ScopeInfo' fields.

    instance Eq Declaration where
      ScopedDecl ScopeInfo
    _ [Declaration]
    a1                == :: Declaration -> Declaration -> Bool
    == ScopedDecl ScopeInfo
    _ [Declaration]
    a2                = [Declaration]
    a1 [Declaration] -> [Declaration] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Declaration]
    a2

      Axiom KindOfName
    a1 DefInfo
    b1 ArgInfo
    c1 Maybe PragmaPolarities
    d1 QName
    e1 Expr
    f1        == Axiom KindOfName
    a2 DefInfo
    b2 ArgInfo
    c2 Maybe PragmaPolarities
    d2 QName
    e2 Expr
    f2        = (KindOfName
    a1, DefInfo
    b1, ArgInfo
    c1, Maybe PragmaPolarities
    d1, QName
    e1, Expr
    f1) (KindOfName, DefInfo, ArgInfo, Maybe PragmaPolarities, QName, Expr)
    -> (KindOfName, DefInfo, ArgInfo, Maybe PragmaPolarities, QName,
        Expr)
    -> Bool
    forall a. Eq a => a -> a -> Bool
    == (KindOfName
    a2, DefInfo
    b2, ArgInfo
    c2, Maybe PragmaPolarities
    d2, QName
    e2, Expr
    f2)
      Generalize Set QName
    a1 DefInfo
    b1 ArgInfo
    c1 QName
    d1 Expr
    e1      == Generalize Set QName
    a2 DefInfo
    b2 ArgInfo
    c2 QName
    d2 Expr
    e2      = (Set QName
    a1, DefInfo
    b1, ArgInfo
    c1, QName
    d1, Expr
    e1) (Set QName, DefInfo, ArgInfo, QName, Expr)
    -> (Set QName, DefInfo, ArgInfo, QName, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Set QName
    a2, DefInfo
    b2, ArgInfo
    c2, QName
    d2, Expr
    e2)
      Field DefInfo
    a1 QName
    b1 Arg Expr
    c1                 == Field DefInfo
    a2 QName
    b2 Arg Expr
    c2                 = (DefInfo
    a1, QName
    b1, Arg Expr
    c1) (DefInfo, QName, Arg Expr) -> (DefInfo, QName, Arg Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, QName
    b2, Arg Expr
    c2)
      Primitive DefInfo
    a1 QName
    b1 Arg Expr
    c1             == Primitive DefInfo
    a2 QName
    b2 Arg Expr
    c2             = (DefInfo
    a1, QName
    b1, Arg Expr
    c1) (DefInfo, QName, Arg Expr) -> (DefInfo, QName, Arg Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, QName
    b2, Arg Expr
    c2)
      Mutual MutualInfo
    a1 [Declaration]
    b1                   == Mutual MutualInfo
    a2 [Declaration]
    b2                   = (MutualInfo
    a1, [Declaration]
    b1) (MutualInfo, [Declaration]) -> (MutualInfo, [Declaration]) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (MutualInfo
    a2, [Declaration]
    b2)
      Section Range
    a1 Erased
    b1 ModuleName
    c1 GeneralizeTelescope
    d1 [Declaration]
    e1         == Section Range
    a2 Erased
    b2 ModuleName
    c2 GeneralizeTelescope
    d2 [Declaration]
    e2         = (Range
    a1, Erased
    b1, ModuleName
    c1, GeneralizeTelescope
    d1, [Declaration]
    e1) (Range, Erased, ModuleName, GeneralizeTelescope, [Declaration])
    -> (Range, Erased, ModuleName, GeneralizeTelescope, [Declaration])
    -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Range
    a2, Erased
    b2, ModuleName
    c2, GeneralizeTelescope
    d2, [Declaration]
    e2)
      Apply ModuleInfo
    a1 Erased
    b1 ModuleName
    c1 ModuleApplication
    d1 ScopeCopyInfo
    e1 ImportDirective
    f1        == Apply ModuleInfo
    a2 Erased
    b2 ModuleName
    c2 ModuleApplication
    d2 ScopeCopyInfo
    e2 ImportDirective
    f2        = (ModuleInfo
    a1, Erased
    b1, ModuleName
    c1, ModuleApplication
    d1, ScopeCopyInfo
    e1, ImportDirective
    f1) (ModuleInfo, Erased, ModuleName, ModuleApplication, ScopeCopyInfo,
     ImportDirective)
    -> (ModuleInfo, Erased, ModuleName, ModuleApplication,
        ScopeCopyInfo, ImportDirective)
    -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ModuleInfo
    a2, Erased
    b2, ModuleName
    c2, ModuleApplication
    d2, ScopeCopyInfo
    e2, ImportDirective
    f2)
      Import ModuleInfo
    a1 ModuleName
    b1 ImportDirective
    c1                == Import ModuleInfo
    a2 ModuleName
    b2 ImportDirective
    c2                = (ModuleInfo
    a1, ModuleName
    b1, ImportDirective
    c1) (ModuleInfo, ModuleName, ImportDirective)
    -> (ModuleInfo, ModuleName, ImportDirective) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ModuleInfo
    a2, ModuleName
    b2, ImportDirective
    c2)
      Pragma Range
    a1 Pragma
    b1                   == Pragma Range
    a2 Pragma
    b2                   = (Range
    a1, Pragma
    b1) (Range, Pragma) -> (Range, Pragma) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Range
    a2, Pragma
    b2)
      Open ModuleInfo
    a1 ModuleName
    b1 ImportDirective
    c1                  == Open ModuleInfo
    a2 ModuleName
    b2 ImportDirective
    c2                  = (ModuleInfo
    a1, ModuleName
    b1, ImportDirective
    c1) (ModuleInfo, ModuleName, ImportDirective)
    -> (ModuleInfo, ModuleName, ImportDirective) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (ModuleInfo
    a2, ModuleName
    b2, ImportDirective
    c2)
      FunDef DefInfo
    a1 QName
    b1 [Clause]
    c1                == FunDef DefInfo
    a2 QName
    b2 [Clause]
    c2                = (DefInfo
    a1, QName
    b1, [Clause]
    c1) (DefInfo, QName, [Clause]) -> (DefInfo, QName, [Clause]) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, QName
    b2, [Clause]
    c2)
      DataSig DefInfo
    a1 Erased
    b1 QName
    c1 GeneralizeTelescope
    d1 Expr
    e1         == DataSig DefInfo
    a2 Erased
    b2 QName
    c2 GeneralizeTelescope
    d2 Expr
    e2         = (DefInfo
    a1, Erased
    b1, QName
    c1, GeneralizeTelescope
    d1, Expr
    e1) (DefInfo, Erased, QName, GeneralizeTelescope, Expr)
    -> (DefInfo, Erased, QName, GeneralizeTelescope, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, Erased
    b2, QName
    c2, GeneralizeTelescope
    d2, Expr
    e2)
      DataDef DefInfo
    a1 QName
    b1 UniverseCheck
    c1 DataDefParams
    d1 [Declaration]
    e1         == DataDef DefInfo
    a2 QName
    b2 UniverseCheck
    c2 DataDefParams
    d2 [Declaration]
    e2         = (DefInfo
    a1, QName
    b1, UniverseCheck
    c1, DataDefParams
    d1, [Declaration]
    e1) (DefInfo, QName, UniverseCheck, DataDefParams, [Declaration])
    -> (DefInfo, QName, UniverseCheck, DataDefParams, [Declaration])
    -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, QName
    b2, UniverseCheck
    c2, DataDefParams
    d2, [Declaration]
    e2)
      RecSig DefInfo
    a1 Erased
    b1 QName
    c1 GeneralizeTelescope
    d1 Expr
    e1          == RecSig DefInfo
    a2 Erased
    b2 QName
    c2 GeneralizeTelescope
    d2 Expr
    e2          = (DefInfo
    a1, Erased
    b1, QName
    c1, GeneralizeTelescope
    d1, Expr
    e1) (DefInfo, Erased, QName, GeneralizeTelescope, Expr)
    -> (DefInfo, Erased, QName, GeneralizeTelescope, Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, Erased
    b2, QName
    c2, GeneralizeTelescope
    d2, Expr
    e2)
      RecDef DefInfo
    a1 QName
    b1 UniverseCheck
    c1 RecordDirectives
    d1 DataDefParams
    e1 Expr
    f1 [Declaration]
    g1    == RecDef DefInfo
    a2 QName
    b2 UniverseCheck
    c2 RecordDirectives
    d2 DataDefParams
    e2 Expr
    f2 [Declaration]
    g2    = (DefInfo
    a1, QName
    b1, UniverseCheck
    c1, RecordDirectives
    d1, DataDefParams
    e1, Expr
    f1, [Declaration]
    g1) (DefInfo, QName, UniverseCheck, RecordDirectives, DataDefParams,
     Expr, [Declaration])
    -> (DefInfo, QName, UniverseCheck, RecordDirectives, DataDefParams,
        Expr, [Declaration])
    -> Bool
    forall a. Eq a => a -> a -> Bool
    == (DefInfo
    a2, QName
    b2, UniverseCheck
    c2, RecordDirectives
    d2, DataDefParams
    e2, Expr
    f2, [Declaration]
    g2)
      PatternSynDef QName
    a1 [WithHiding BindName]
    b1 Pattern' Void
    c1         == PatternSynDef QName
    a2 [WithHiding BindName]
    b2 Pattern' Void
    c2         = (QName
    a1, [WithHiding BindName]
    b1, Pattern' Void
    c1) (QName, [WithHiding BindName], Pattern' Void)
    -> (QName, [WithHiding BindName], Pattern' Void) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (QName
    a2, [WithHiding BindName]
    b2, Pattern' Void
    c2)
      UnquoteDecl MutualInfo
    a1 [DefInfo]
    b1 [QName]
    c1 Expr
    d1        == UnquoteDecl MutualInfo
    a2 [DefInfo]
    b2 [QName]
    c2 Expr
    d2        = (MutualInfo
    a1, [DefInfo]
    b1, [QName]
    c1, Expr
    d1) (MutualInfo, [DefInfo], [QName], Expr)
    -> (MutualInfo, [DefInfo], [QName], Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (MutualInfo
    a2, [DefInfo]
    b2, [QName]
    c2, Expr
    d2)
      UnquoteDef [DefInfo]
    a1 [QName]
    b1 Expr
    c1            == UnquoteDef [DefInfo]
    a2 [QName]
    b2 Expr
    c2            = ([DefInfo]
    a1, [QName]
    b1, Expr
    c1) ([DefInfo], [QName], Expr) -> ([DefInfo], [QName], Expr) -> Bool
    forall a. Eq a => a -> a -> Bool
    == ([DefInfo]
    a2, [QName]
    b2, Expr
    c2)
      UnfoldingDecl Range
    a1 [QName]
    b1            == UnfoldingDecl Range
    a2 [QName]
    b2            = (Range
    a1,[QName]
    b1) (Range, [QName]) -> (Range, [QName]) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Range
    a2,[QName]
    b2)

      Declaration
    _                              == Declaration
    _                              = Bool
    False

    instance Underscore Expr where
      underscore :: Expr
    underscore   = MetaInfo -> Expr
    Underscore MetaInfo
    emptyMetaInfo
      isUnderscore :: Expr -> Bool
    isUnderscore = \case
        Underscore MetaInfo
    _ -> Bool
    True
        Expr
    _ -> Bool
    False

    instance LensHiding LamBinding where
      getHiding :: LamBinding -> Hiding
    getHiding   (DomainFree TacticAttribute
    _ NamedArg Binder
    x) = NamedArg Binder -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg Binder
    x
      getHiding   (DomainFull TypedBinding
    tb)  = TypedBinding -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding TypedBinding
    tb
      mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding
    mapHiding Hiding -> Hiding
    f (DomainFree TacticAttribute
    t NamedArg Binder
    x) = TacticAttribute -> NamedArg Binder -> LamBinding
    DomainFree TacticAttribute
    t (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ (Hiding -> Hiding) -> NamedArg Binder -> NamedArg Binder
    forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
    mapHiding Hiding -> Hiding
    f NamedArg Binder
    x
      mapHiding Hiding -> Hiding
    f (DomainFull TypedBinding
    tb)  = TypedBinding -> LamBinding
    DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ (Hiding -> Hiding) -> TypedBinding -> TypedBinding
    forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
    mapHiding Hiding -> Hiding
    f TypedBinding
    tb

    instance LensHiding TypedBinding where
      getHiding :: TypedBinding -> Hiding
    getHiding (TBind Range
    _ TypedBindingInfo
    _ (NamedArg Binder
    x :| [NamedArg Binder]
    _) Expr
    _) = NamedArg Binder -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg Binder
    x   -- Slightly dubious
      getHiding TLet{}                 = Hiding
    forall a. Monoid a => a
    mempty
      mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding
    mapHiding Hiding -> Hiding
    f (TBind Range
    r TypedBindingInfo
    t List1 (NamedArg Binder)
    xs Expr
    e)     = Range
    -> TypedBindingInfo
    -> List1 (NamedArg Binder)
    -> Expr
    -> TypedBinding
    TBind Range
    r TypedBindingInfo
    t (((NamedArg Binder -> NamedArg Binder)
    -> List1 (NamedArg Binder) -> List1 (NamedArg Binder)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((NamedArg Binder -> NamedArg Binder)
     -> List1 (NamedArg Binder) -> List1 (NamedArg Binder))
    -> ((Hiding -> Hiding) -> NamedArg Binder -> NamedArg Binder)
    -> (Hiding -> Hiding)
    -> List1 (NamedArg Binder)
    -> List1 (NamedArg Binder)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Hiding -> Hiding) -> NamedArg Binder -> NamedArg Binder
    forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
    mapHiding) Hiding -> Hiding
    f List1 (NamedArg Binder)
    xs) Expr
    e
      mapHiding Hiding -> Hiding
    f b :: TypedBinding
    b@TLet{}             = TypedBinding
    b

    instance HasRange a => HasRange (Binder' a) where
      getRange :: Binder' a -> Range
    getRange (Binder Maybe Pattern
    p BinderNameOrigin
    _ a
    n) = Maybe Pattern -> a -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Maybe Pattern
    p a
    n

    instance HasRange LamBinding where
        getRange :: LamBinding -> Range
    getRange (DomainFree TacticAttribute
    _ NamedArg Binder
    x) = NamedArg Binder -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg Binder
    x
        getRange (DomainFull TypedBinding
    b)   = TypedBinding -> Range
    forall a. HasRange a => a -> Range
    getRange TypedBinding
    b

    instance HasRange TypedBinding where
        getRange :: TypedBinding -> Range
    getRange (TBind Range
    r TypedBindingInfo
    _ List1 (NamedArg Binder)
    _ Expr
    _) = Range
    r
        getRange (TLet Range
    r List1 LetBinding
    _)    = Range
    r

    instance HasRange Expr where
        getRange :: Expr -> Range
    getRange (Var Name
    x)                 = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
        getRange (Def' QName
    x Suffix
    _)              = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x
        getRange (Proj ProjOrigin
    _ AmbiguousQName
    x)              = AmbiguousQName -> Range
    forall a. HasRange a => a -> Range
    getRange AmbiguousQName
    x
        getRange (Con AmbiguousQName
    x)                 = AmbiguousQName -> Range
    forall a. HasRange a => a -> Range
    getRange AmbiguousQName
    x
        getRange (Lit ExprInfo
    i Literal
    _)               = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (QuestionMark MetaInfo
    i InteractionId
    _)      = MetaInfo -> Range
    forall a. HasRange a => a -> Range
    getRange MetaInfo
    i
        getRange (Underscore  MetaInfo
    i)         = MetaInfo -> Range
    forall a. HasRange a => a -> Range
    getRange MetaInfo
    i
        getRange (Dot ExprInfo
    i Expr
    _)               = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (App AppInfo
    i Expr
    _ NamedArg Expr
    _)             = AppInfo -> Range
    forall a. HasRange a => a -> Range
    getRange AppInfo
    i
        getRange (WithApp ExprInfo
    i Expr
    _ List1 Expr
    _)         = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (Lam ExprInfo
    i LamBinding
    _ Expr
    _)             = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (AbsurdLam ExprInfo
    i Hiding
    _)         = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (ExtendedLam ExprInfo
    i DefInfo
    _ Erased
    _ QName
    _ List1 Clause
    _) = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (Pi ExprInfo
    i Telescope1
    _ Expr
    _)              = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (Generalized Set1 QName
    _ Expr
    x)       = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    x
        getRange (Fun ExprInfo
    i Arg Expr
    _ Expr
    _)             = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (Let ExprInfo
    i List1 LetBinding
    _ Expr
    _)             = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (Rec KwRange
    _ ExprInfo
    i RecordAssigns
    _)             = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (RecUpdate KwRange
    _ ExprInfo
    i Expr
    _ Assigns
    _)     = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (ScopedExpr ScopeInfo
    _ Expr
    e)        = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e
        getRange (Quote ExprInfo
    i)               = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (QuoteTerm ExprInfo
    i)           = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (Unquote ExprInfo
    i)             = ExprInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ExprInfo
    i
        getRange (DontCare{})            = Range
    forall a. Range' a
    noRange
        getRange (PatternSyn AmbiguousQName
    x)          = AmbiguousQName -> Range
    forall a. HasRange a => a -> Range
    getRange AmbiguousQName
    x
        getRange (Macro QName
    x)               = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x

    instance HasRange Declaration where
        getRange :: Declaration -> Range
    getRange (Axiom    KindOfName
    _ DefInfo
    i ArgInfo
    _ Maybe PragmaPolarities
    _ QName
    _ Expr
    _  )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (Generalize Set QName
    _ DefInfo
    i ArgInfo
    _ QName
    _ Expr
    _)    = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (Field      DefInfo
    i QName
    _ Arg Expr
    _      )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (Mutual     MutualInfo
    i [Declaration]
    _        )  = MutualInfo -> Range
    forall a. HasRange a => a -> Range
    getRange MutualInfo
    i
        getRange (Section    Range
    i Erased
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    _  )  = Range -> Range
    forall a. HasRange a => a -> Range
    getRange Range
    i
        getRange (Apply      ModuleInfo
    i Erased
    _ ModuleName
    _ ModuleApplication
    _ ScopeCopyInfo
    _ ImportDirective
    _)  = ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i
        getRange (Import     ModuleInfo
    i ModuleName
    _ ImportDirective
    _      )  = ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i
        getRange (Primitive  DefInfo
    i QName
    _ Arg Expr
    _      )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (Pragma     Range
    i Pragma
    _        )  = Range -> Range
    forall a. HasRange a => a -> Range
    getRange Range
    i
        getRange (Open       ModuleInfo
    i ModuleName
    _ ImportDirective
    _      )  = ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i
        getRange (ScopedDecl ScopeInfo
    _ [Declaration]
    d        )  = [Declaration] -> Range
    forall a. HasRange a => a -> Range
    getRange [Declaration]
    d
        getRange (FunDef     DefInfo
    i QName
    _ [Clause]
    _      )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (DataSig    DefInfo
    i Erased
    _ QName
    _ GeneralizeTelescope
    _ Expr
    _  )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (DataDef    DefInfo
    i QName
    _ UniverseCheck
    _ DataDefParams
    _ [Declaration]
    _  )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (RecSig     DefInfo
    i Erased
    _ QName
    _ GeneralizeTelescope
    _ Expr
    _  )  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (RecDef DefInfo
    i QName
    _ UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Expr
    _ [Declaration]
    _)    = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
        getRange (PatternSynDef QName
    x [WithHiding BindName]
    _ Pattern' Void
    _   )  = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x
        getRange (UnquoteDecl MutualInfo
    _ [DefInfo]
    i [QName]
    _ Expr
    _)     = [DefInfo] -> Range
    forall a. HasRange a => a -> Range
    getRange [DefInfo]
    i
        getRange (UnquoteDef [DefInfo]
    i [QName]
    _ Expr
    _)        = [DefInfo] -> Range
    forall a. HasRange a => a -> Range
    getRange [DefInfo]
    i
        getRange (UnquoteData [DefInfo]
    i QName
    _ UniverseCheck
    _ [DefInfo]
    j [QName]
    _ Expr
    _) = ([DefInfo], [DefInfo]) -> Range
    forall a. HasRange a => a -> Range
    getRange ([DefInfo]
    i, [DefInfo]
    j)
        getRange (UnfoldingDecl Range
    r [QName]
    _)       = Range
    r

    instance HasRange (Pattern' e) where
        getRange :: Pattern' e -> Range
    getRange (VarP BindName
    x)            = BindName -> Range
    forall a. HasRange a => a -> Range
    getRange BindName
    x
        getRange (ConP ConPatInfo
    i AmbiguousQName
    _ NAPs e
    _)        = ConPatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ConPatInfo
    i
        getRange (ProjP PatInfo
    i ProjOrigin
    _ AmbiguousQName
    _)       = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (DefP PatInfo
    i AmbiguousQName
    _ NAPs e
    _)        = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (WildP PatInfo
    i)           = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (AsP PatInfo
    i BindName
    _ Pattern' e
    _)         = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (DotP PatInfo
    i e
    _)          = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (AbsurdP PatInfo
    i)         = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (LitP PatInfo
    i Literal
    l)          = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (PatternSynP PatInfo
    i AmbiguousQName
    _ NAPs e
    _) = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (RecP KwRange
    _kwr ConPatInfo
    i [FieldAssignment' (Pattern' e)]
    _)     = ConPatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ConPatInfo
    i
        getRange (EqualP PatInfo
    i List1 (e, e)
    _)        = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i
        getRange (WithP PatInfo
    i Pattern' e
    _)         = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i

    instance HasRange SpineLHS where
        getRange :: SpineLHS -> Range
    getRange (SpineLHS LHSInfo
    i QName
    _ [NamedArg Pattern]
    _)  = LHSInfo -> Range
    forall a. HasRange a => a -> Range
    getRange LHSInfo
    i

    instance HasRange LHS where
        getRange :: LHS -> Range
    getRange (LHS LHSInfo
    i LHSCore
    _)   = LHSInfo -> Range
    forall a. HasRange a => a -> Range
    getRange LHSInfo
    i

    instance HasRange (LHSCore' e) where
        getRange :: LHSCore' e -> Range
    getRange (LHSHead QName
    f [NamedArg (Pattern' e)]
    ps)         = QName -> [NamedArg (Pattern' e)] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange QName
    f [NamedArg (Pattern' e)]
    ps
        getRange (LHSProj AmbiguousQName
    d NamedArg (LHSCore' e)
    lhscore [NamedArg (Pattern' e)]
    ps) = AmbiguousQName
    d AmbiguousQName -> NamedArg (LHSCore' e) -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` NamedArg (LHSCore' e)
    lhscore Range -> [NamedArg (Pattern' e)] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [NamedArg (Pattern' e)]
    ps
        getRange (LHSWith LHSCore' e
    h List1 (Arg (Pattern' e))
    wps [NamedArg (Pattern' e)]
    ps)     = LHSCore' e
    h LHSCore' e -> List1 (Arg (Pattern' e)) -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` List1 (Arg (Pattern' e))
    wps Range -> [NamedArg (Pattern' e)] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [NamedArg (Pattern' e)]
    ps

    instance HasRange a => HasRange (Clause' a) where
        getRange :: Clause' a -> Range
    getRange (Clause a
    lhs [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    ds Catchall
    catchall) = (a, RHS, WhereDeclarations) -> Range
    forall a. HasRange a => a -> Range
    getRange (a
    lhs, RHS
    rhs, WhereDeclarations
    ds)

    instance HasRange RHS where
        getRange :: RHS -> Range
    getRange RHS
    AbsurdRHS                 = Range
    forall a. Range' a
    noRange
        getRange (RHS Expr
    e Maybe Expr
    _)                 = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e
        getRange (WithRHS QName
    _ List1 WithExpr
    e List1 Clause
    cs)          = List1 WithExpr -> List1 Clause -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange List1 WithExpr
    e List1 Clause
    cs
        getRange (RewriteRHS [RewriteEqn]
    xes [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    wh) = ([RewriteEqn], RHS, WhereDeclarations) -> Range
    forall a. HasRange a => a -> Range
    getRange ([RewriteEqn]
    xes, RHS
    rhs, WhereDeclarations
    wh)

    instance HasRange WhereDeclarations where
      getRange :: WhereDeclarations -> Range
    getRange (WhereDecls Maybe ModuleName
    _ Bool
    _ Maybe Declaration
    ds) = Maybe Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Maybe Declaration
    ds

    instance HasRange LetBinding where
      getRange :: LetBinding -> Range
    getRange (LetBind LetInfo
    i ArgInfo
    _ BindName
    _ Expr
    _ Expr
    _)     = LetInfo -> Range
    forall a. HasRange a => a -> Range
    getRange LetInfo
    i
      getRange (LetAxiom LetInfo
    i ArgInfo
    _ BindName
    _ Expr
    _)      = LetInfo -> Range
    forall a. HasRange a => a -> Range
    getRange LetInfo
    i
      getRange (LetPatBind  LetInfo
    i Pattern
    _ Expr
    _)     = LetInfo -> Range
    forall a. HasRange a => a -> Range
    getRange LetInfo
    i
      getRange (LetApply ModuleInfo
    i Erased
    _ ModuleName
    _ ModuleApplication
    _ ScopeCopyInfo
    _ ImportDirective
    _)  = ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i
      getRange (LetOpen  ModuleInfo
    i ModuleName
    _ ImportDirective
    _)        = ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i

    -- setRange for patterns applies the range to the outermost pattern constructor
    instance SetRange (Pattern' a) where
        setRange :: Range -> Pattern' a -> Pattern' a
    setRange Range
    r (VarP BindName
    x)            = BindName -> Pattern' a
    forall e. BindName -> Pattern' e
    VarP (Range -> KillRangeT BindName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r BindName
    x)
        setRange Range
    r (ConP ConPatInfo
    i AmbiguousQName
    ns NAPs a
    as)       = ConPatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    ConP (Range -> ConPatInfo -> ConPatInfo
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r ConPatInfo
    i) AmbiguousQName
    ns NAPs a
    as
        setRange Range
    r (ProjP PatInfo
    _ ProjOrigin
    o AmbiguousQName
    ns)       = PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' a
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    ProjP (Range -> PatInfo
    PatRange Range
    r) ProjOrigin
    o AmbiguousQName
    ns
        setRange Range
    r (DefP PatInfo
    _ AmbiguousQName
    ns NAPs a
    as)       = PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP (Range -> PatInfo
    PatRange Range
    r) AmbiguousQName
    ns NAPs a
    as -- (setRange r n) as
        setRange Range
    r (WildP PatInfo
    _)            = PatInfo -> Pattern' a
    forall e. PatInfo -> Pattern' e
    WildP (Range -> PatInfo
    PatRange Range
    r)
        setRange Range
    r (AsP PatInfo
    _ BindName
    n Pattern' a
    p)          = PatInfo -> BindName -> Pattern' a -> Pattern' a
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    AsP (Range -> PatInfo
    PatRange Range
    r) (Range -> KillRangeT BindName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r BindName
    n) Pattern' a
    p
        setRange Range
    r (DotP PatInfo
    _ a
    e)           = PatInfo -> a -> Pattern' a
    forall e. PatInfo -> e -> Pattern' e
    DotP (Range -> PatInfo
    PatRange Range
    r) a
    e
        setRange Range
    r (AbsurdP PatInfo
    _)          = PatInfo -> Pattern' a
    forall e. PatInfo -> Pattern' e
    AbsurdP (Range -> PatInfo
    PatRange Range
    r)
        setRange Range
    r (LitP PatInfo
    _ Literal
    l)           = PatInfo -> Literal -> Pattern' a
    forall e. PatInfo -> Literal -> Pattern' e
    LitP (Range -> PatInfo
    PatRange Range
    r) Literal
    l
        setRange Range
    r (PatternSynP PatInfo
    _ AmbiguousQName
    n NAPs a
    as) = PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    PatternSynP (Range -> PatInfo
    PatRange Range
    r) AmbiguousQName
    n NAPs a
    as
        setRange Range
    r (RecP KwRange
    _ ConPatInfo
    i [FieldAssignment' (Pattern' a)]
    as)        = KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' a)] -> Pattern' a
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    RecP KwRange
    forall a. Null a => a
    empty (Range -> ConPatInfo -> ConPatInfo
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r ConPatInfo
    i) [FieldAssignment' (Pattern' a)]
    as
        setRange Range
    r (EqualP PatInfo
    _ List1 (a, a)
    es)        = PatInfo -> List1 (a, a) -> Pattern' a
    forall e. PatInfo -> List1 (e, e) -> Pattern' e
    EqualP (Range -> PatInfo
    PatRange Range
    r) List1 (a, a)
    es
        setRange Range
    r (WithP PatInfo
    i Pattern' a
    p)          = PatInfo -> Pattern' a -> Pattern' a
    forall e. PatInfo -> Pattern' e -> Pattern' e
    WithP (Range -> PatInfo -> PatInfo
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r PatInfo
    i) Pattern' a
    p

    instance KillRange a => KillRange (Binder' a) where
      killRange :: KillRangeT (Binder' a)
    killRange (Binder Maybe Pattern
    a BinderNameOrigin
    o a
    b) = (Maybe Pattern -> BinderNameOrigin -> a -> Binder' a)
    -> Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    forall a. Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    Binder Maybe Pattern
    a BinderNameOrigin
    o a
    b

    instance KillRange LamBinding where
      killRange :: LamBinding -> LamBinding
    killRange (DomainFree TacticAttribute
    t NamedArg Binder
    x) = (TacticAttribute -> NamedArg Binder -> LamBinding)
    -> TacticAttribute -> NamedArg Binder -> LamBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN TacticAttribute -> NamedArg Binder -> LamBinding
    DomainFree TacticAttribute
    t NamedArg Binder
    x
      killRange (DomainFull TypedBinding
    b)   = (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN TypedBinding -> LamBinding
    DomainFull TypedBinding
    b

    instance KillRange GeneralizeTelescope where
      killRange :: KillRangeT GeneralizeTelescope
    killRange (GeneralizeTel Map QName Name
    s Telescope
    tel) = Map QName Name -> Telescope -> GeneralizeTelescope
    GeneralizeTel Map QName Name
    s (KillRangeT Telescope
    forall a. KillRange a => KillRangeT a
    killRange Telescope
    tel)

    instance KillRange DataDefParams where
      killRange :: KillRangeT DataDefParams
    killRange (DataDefParams Set Name
    s [LamBinding]
    tel) = Set Name -> [LamBinding] -> DataDefParams
    DataDefParams Set Name
    s (KillRangeT [LamBinding]
    forall a. KillRange a => KillRangeT a
    killRange [LamBinding]
    tel)

    instance KillRange TypedBindingInfo where
      killRange :: KillRangeT TypedBindingInfo
    killRange (TypedBindingInfo TacticAttribute
    a Bool
    b) = (TacticAttribute -> Bool -> TypedBindingInfo)
    -> TacticAttribute -> Bool -> TypedBindingInfo
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN TacticAttribute -> Bool -> TypedBindingInfo
    TypedBindingInfo TacticAttribute
    a Bool
    b

    instance KillRange TypedBinding where
      killRange :: TypedBinding -> TypedBinding
    killRange (TBind Range
    r TypedBindingInfo
    t List1 (NamedArg Binder)
    xs Expr
    e) = (Range
     -> TypedBindingInfo
     -> List1 (NamedArg Binder)
     -> Expr
     -> TypedBinding)
    -> Range
    -> TypedBindingInfo
    -> List1 (NamedArg Binder)
    -> Expr
    -> TypedBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range
    -> TypedBindingInfo
    -> List1 (NamedArg Binder)
    -> Expr
    -> TypedBinding
    TBind Range
    r TypedBindingInfo
    t List1 (NamedArg Binder)
    xs Expr
    e
      killRange (TLet Range
    r List1 LetBinding
    lbs)     = (Range -> List1 LetBinding -> TypedBinding)
    -> Range -> List1 LetBinding -> TypedBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range -> List1 LetBinding -> TypedBinding
    TLet Range
    r List1 LetBinding
    lbs

    instance KillRange Expr where
      killRange :: Expr -> Expr
    killRange (Var Name
    x)                  = (Name -> Expr) -> Name -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Name -> Expr
    Var Name
    x
      killRange (Def' QName
    x Suffix
    v)               = (QName -> Suffix -> Expr) -> QName -> Suffix -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> Suffix -> Expr
    Def' QName
    x Suffix
    v
      killRange (Proj ProjOrigin
    o AmbiguousQName
    x)               = (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (ProjOrigin -> AmbiguousQName -> Expr
    Proj ProjOrigin
    o) AmbiguousQName
    x
      killRange (Con AmbiguousQName
    x)                  = (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN AmbiguousQName -> Expr
    Con AmbiguousQName
    x
      killRange (Lit ExprInfo
    i Literal
    l)                = (ExprInfo -> Literal -> Expr) -> ExprInfo -> Literal -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Literal -> Expr
    Lit ExprInfo
    i Literal
    l
      killRange (QuestionMark MetaInfo
    i InteractionId
    ii)      = (MetaInfo -> InteractionId -> Expr)
    -> MetaInfo -> InteractionId -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN MetaInfo -> InteractionId -> Expr
    QuestionMark MetaInfo
    i InteractionId
    ii
      killRange (Underscore  MetaInfo
    i)          = (MetaInfo -> Expr) -> MetaInfo -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN MetaInfo -> Expr
    Underscore MetaInfo
    i
      killRange (Dot ExprInfo
    i Expr
    e)                = (ExprInfo -> Expr -> Expr) -> ExprInfo -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Expr -> Expr
    Dot ExprInfo
    i Expr
    e
      killRange (App AppInfo
    i Expr
    e1 NamedArg Expr
    e2)            = (AppInfo -> Expr -> NamedArg Expr -> Expr)
    -> AppInfo -> Expr -> NamedArg Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    i Expr
    e1 NamedArg Expr
    e2
      killRange (WithApp ExprInfo
    i Expr
    e List1 Expr
    es)         = (ExprInfo -> Expr -> List1 Expr -> Expr)
    -> ExprInfo -> Expr -> List1 Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Expr -> List1 Expr -> Expr
    WithApp ExprInfo
    i Expr
    e List1 Expr
    es
      killRange (Lam ExprInfo
    i LamBinding
    b Expr
    e)              = (ExprInfo -> LamBinding -> Expr -> Expr)
    -> ExprInfo -> LamBinding -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> LamBinding -> Expr -> Expr
    Lam ExprInfo
    i LamBinding
    b Expr
    e
      killRange (AbsurdLam ExprInfo
    i Hiding
    h)          = (ExprInfo -> Hiding -> Expr) -> ExprInfo -> Hiding -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Hiding -> Expr
    AbsurdLam ExprInfo
    i Hiding
    h
      killRange (ExtendedLam ExprInfo
    i DefInfo
    n Erased
    e QName
    d List1 Clause
    ps) = (ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr)
    -> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
    ExtendedLam ExprInfo
    i DefInfo
    n Erased
    e QName
    d List1 Clause
    ps
      killRange (Pi ExprInfo
    i Telescope1
    a Expr
    b)               = (ExprInfo -> Telescope1 -> Expr -> Expr)
    -> ExprInfo -> Telescope1 -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Telescope1 -> Expr -> Expr
    Pi ExprInfo
    i Telescope1
    a Expr
    b
      killRange (Generalized Set1 QName
    s Expr
    x)        = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Set1 QName -> Expr -> Expr
    Generalized Set1 QName
    s) Expr
    x
      killRange (Fun ExprInfo
    i Arg Expr
    a Expr
    b)              = (ExprInfo -> Arg Expr -> Expr -> Expr)
    -> ExprInfo -> Arg Expr -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Arg Expr -> Expr -> Expr
    Fun ExprInfo
    i Arg Expr
    a Expr
    b
      killRange (Let ExprInfo
    i List1 LetBinding
    ds Expr
    e)             = (ExprInfo -> List1 LetBinding -> Expr -> Expr)
    -> ExprInfo -> List1 LetBinding -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> List1 LetBinding -> Expr -> Expr
    Let ExprInfo
    i List1 LetBinding
    ds Expr
    e
      killRange (Rec KwRange
    kwr ExprInfo
    i RecordAssigns
    fs)           = (KwRange -> ExprInfo -> RecordAssigns -> Expr)
    -> KwRange -> ExprInfo -> RecordAssigns -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN KwRange -> ExprInfo -> RecordAssigns -> Expr
    Rec KwRange
    kwr ExprInfo
    i RecordAssigns
    fs
      killRange (RecUpdate KwRange
    kwr ExprInfo
    i Expr
    e Assigns
    fs)   = (KwRange -> ExprInfo -> Expr -> Assigns -> Expr)
    -> KwRange -> ExprInfo -> Expr -> Assigns -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN KwRange -> ExprInfo -> Expr -> Assigns -> Expr
    RecUpdate KwRange
    kwr ExprInfo
    i Expr
    e Assigns
    fs
      killRange (ScopedExpr ScopeInfo
    s Expr
    e)         = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (ScopeInfo -> Expr -> Expr
    ScopedExpr ScopeInfo
    s) Expr
    e
      killRange (Quote ExprInfo
    i)                = (ExprInfo -> Expr) -> ExprInfo -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Expr
    Quote ExprInfo
    i
      killRange (QuoteTerm ExprInfo
    i)            = (ExprInfo -> Expr) -> ExprInfo -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Expr
    QuoteTerm ExprInfo
    i
      killRange (Unquote ExprInfo
    i)              = (ExprInfo -> Expr) -> ExprInfo -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ExprInfo -> Expr
    Unquote ExprInfo
    i
      killRange (DontCare Expr
    e)             = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Expr -> Expr
    DontCare Expr
    e
      killRange (PatternSyn AmbiguousQName
    x)           = (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN AmbiguousQName -> Expr
    PatternSyn AmbiguousQName
    x
      killRange (Macro QName
    x)                = (QName -> Expr) -> QName -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> Expr
    Macro QName
    x

    instance KillRange Suffix where
      killRange :: KillRangeT Suffix
    killRange = KillRangeT Suffix
    forall a. a -> a
    id

    instance KillRange Declaration where
      killRange :: KillRangeT Declaration
    killRange (Axiom    KindOfName
    p DefInfo
    i ArgInfo
    a Maybe PragmaPolarities
    b QName
    c Expr
    d     ) = (DefInfo -> ArgInfo -> QName -> Expr -> Declaration)
    -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (\DefInfo
    i ArgInfo
    a QName
    c Expr
    d -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> Declaration
    Axiom KindOfName
    p DefInfo
    i ArgInfo
    a Maybe PragmaPolarities
    b QName
    c Expr
    d) DefInfo
    i ArgInfo
    a QName
    c Expr
    d
      killRange (Generalize Set QName
    s DefInfo
    i ArgInfo
    j QName
    x Expr
    e     ) = (DefInfo -> ArgInfo -> QName -> Expr -> Declaration)
    -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
    Generalize Set QName
    s) DefInfo
    i ArgInfo
    j QName
    x Expr
    e
      killRange (Field      DefInfo
    i QName
    a Arg Expr
    b         ) = (DefInfo -> QName -> Arg Expr -> Declaration)
    -> DefInfo -> QName -> Arg Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo -> QName -> Arg Expr -> Declaration
    Field      DefInfo
    i QName
    a Arg Expr
    b
      killRange (Mutual     MutualInfo
    i [Declaration]
    a           ) = (MutualInfo -> [Declaration] -> Declaration)
    -> MutualInfo -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN MutualInfo -> [Declaration] -> Declaration
    Mutual     MutualInfo
    i [Declaration]
    a
      killRange (Section    Range
    i Erased
    a ModuleName
    b GeneralizeTelescope
    c [Declaration]
    d     ) = (Range
     -> Erased
     -> ModuleName
     -> GeneralizeTelescope
     -> [Declaration]
     -> Declaration)
    -> Range
    -> Erased
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range
    -> Erased
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    Section    Range
    i Erased
    a ModuleName
    b GeneralizeTelescope
    c [Declaration]
    d
      killRange (Apply      ModuleInfo
    i Erased
    a ModuleName
    b ModuleApplication
    c ScopeCopyInfo
    d ImportDirective
    e   ) = (ModuleInfo
     -> Erased
     -> ModuleName
     -> ModuleApplication
     -> ScopeCopyInfo
     -> ImportDirective
     -> Declaration)
    -> ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> Declaration
    Apply      ModuleInfo
    i Erased
    a ModuleName
    b ModuleApplication
    c ScopeCopyInfo
    d ImportDirective
    e
      killRange (Import     ModuleInfo
    i ModuleName
    a ImportDirective
    b         ) = (ModuleInfo -> ModuleName -> ImportDirective -> Declaration)
    -> ModuleInfo -> ModuleName -> ImportDirective -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ModuleInfo -> ModuleName -> ImportDirective -> Declaration
    Import     ModuleInfo
    i ModuleName
    a ImportDirective
    b
      killRange (Primitive  DefInfo
    i QName
    a Arg Expr
    b         ) = (DefInfo -> QName -> Arg Expr -> Declaration)
    -> DefInfo -> QName -> Arg Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo -> QName -> Arg Expr -> Declaration
    Primitive  DefInfo
    i QName
    a Arg Expr
    b
      killRange (Pragma     Range
    i Pragma
    a           ) = Range -> Pragma -> Declaration
    Pragma (Range -> Range
    forall a. KillRange a => KillRangeT a
    killRange Range
    i) Pragma
    a
      killRange (Open       ModuleInfo
    i ModuleName
    x ImportDirective
    dir       ) = (ModuleInfo -> ModuleName -> ImportDirective -> Declaration)
    -> ModuleInfo -> ModuleName -> ImportDirective -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ModuleInfo -> ModuleName -> ImportDirective -> Declaration
    Open       ModuleInfo
    i ModuleName
    x ImportDirective
    dir
      killRange (ScopedDecl ScopeInfo
    a [Declaration]
    d           ) = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (ScopeInfo -> [Declaration] -> Declaration
    ScopedDecl ScopeInfo
    a) [Declaration]
    d
      killRange (FunDef  DefInfo
    i QName
    a [Clause]
    b            ) = (DefInfo -> QName -> [Clause] -> Declaration)
    -> DefInfo -> QName -> [Clause] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo -> QName -> [Clause] -> Declaration
    FunDef  DefInfo
    i QName
    a [Clause]
    b
      killRange (DataSig DefInfo
    i Erased
    a QName
    b GeneralizeTelescope
    c Expr
    d        ) = (DefInfo
     -> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration)
    -> DefInfo
    -> Erased
    -> QName
    -> GeneralizeTelescope
    -> Expr
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo
    -> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
    DataSig DefInfo
    i Erased
    a QName
    b GeneralizeTelescope
    c Expr
    d
      killRange (DataDef DefInfo
    i QName
    a UniverseCheck
    b DataDefParams
    c [Declaration]
    d        ) = (DefInfo
     -> QName
     -> UniverseCheck
     -> DataDefParams
     -> [Declaration]
     -> Declaration)
    -> DefInfo
    -> QName
    -> UniverseCheck
    -> DataDefParams
    -> [Declaration]
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo
    -> QName
    -> UniverseCheck
    -> DataDefParams
    -> [Declaration]
    -> Declaration
    DataDef DefInfo
    i QName
    a UniverseCheck
    b DataDefParams
    c [Declaration]
    d
      killRange (RecSig  DefInfo
    i Erased
    a QName
    b GeneralizeTelescope
    c Expr
    d        ) = (DefInfo
     -> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration)
    -> DefInfo
    -> Erased
    -> QName
    -> GeneralizeTelescope
    -> Expr
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo
    -> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
    RecSig  DefInfo
    i Erased
    a QName
    b GeneralizeTelescope
    c Expr
    d
      killRange (RecDef  DefInfo
    i QName
    a UniverseCheck
    b RecordDirectives
    c DataDefParams
    d Expr
    e [Declaration]
    f    ) = (DefInfo
     -> QName
     -> UniverseCheck
     -> RecordDirectives
     -> DataDefParams
     -> Expr
     -> [Declaration]
     -> Declaration)
    -> DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Declaration]
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Declaration]
    -> Declaration
    RecDef  DefInfo
    i QName
    a UniverseCheck
    b RecordDirectives
    c DataDefParams
    d Expr
    e [Declaration]
    f
      killRange (PatternSynDef QName
    x [WithHiding BindName]
    xs Pattern' Void
    p     ) = (QName -> [WithHiding BindName] -> Pattern' Void -> Declaration)
    -> QName -> [WithHiding BindName] -> Pattern' Void -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> [WithHiding BindName] -> Pattern' Void -> Declaration
    PatternSynDef QName
    x [WithHiding BindName]
    xs Pattern' Void
    p
      killRange (UnquoteDecl MutualInfo
    mi [DefInfo]
    i [QName]
    x Expr
    e     ) = (MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration)
    -> MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
    UnquoteDecl MutualInfo
    mi [DefInfo]
    i [QName]
    x Expr
    e
      killRange (UnquoteDef [DefInfo]
    i [QName]
    x Expr
    e         ) = ([DefInfo] -> [QName] -> Expr -> Declaration)
    -> [DefInfo] -> [QName] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [DefInfo] -> [QName] -> Expr -> Declaration
    UnquoteDef [DefInfo]
    i [QName]
    x Expr
    e
      killRange (UnquoteData [DefInfo]
    i QName
    xs UniverseCheck
    uc [DefInfo]
    j [QName]
    cs Expr
    e) = ([DefInfo]
     -> QName
     -> UniverseCheck
     -> [DefInfo]
     -> [QName]
     -> Expr
     -> Declaration)
    -> [DefInfo]
    -> QName
    -> UniverseCheck
    -> [DefInfo]
    -> [QName]
    -> Expr
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [DefInfo]
    -> QName
    -> UniverseCheck
    -> [DefInfo]
    -> [QName]
    -> Expr
    -> Declaration
    UnquoteData [DefInfo]
    i QName
    xs UniverseCheck
    uc [DefInfo]
    j [QName]
    cs Expr
    e
      killRange (UnfoldingDecl Range
    r [QName]
    xs)         = (Range -> [QName] -> Declaration)
    -> Range -> [QName] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range -> [QName] -> Declaration
    UnfoldingDecl Range
    r [QName]
    xs

    instance KillRange ModuleApplication where
      killRange :: KillRangeT ModuleApplication
    killRange (SectionApp Telescope
    a ModuleName
    b [NamedArg Expr]
    c  ) = (Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication)
    -> Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
    SectionApp Telescope
    a ModuleName
    b [NamedArg Expr]
    c
      killRange (RecordModuleInstance ModuleName
    a) = (ModuleName -> ModuleApplication)
    -> ModuleName -> ModuleApplication
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ModuleName -> ModuleApplication
    RecordModuleInstance ModuleName
    a

    instance KillRange ScopeCopyInfo where
      killRange :: KillRangeT ScopeCopyInfo
    killRange (ScopeCopyInfo Ren ModuleName
    a Ren QName
    b) = (Ren ModuleName -> Ren QName -> ScopeCopyInfo)
    -> Ren ModuleName -> Ren QName -> ScopeCopyInfo
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Ren ModuleName -> Ren QName -> ScopeCopyInfo
    ScopeCopyInfo Ren ModuleName
    a Ren QName
    b

    instance KillRange RecordConName where
      killRange :: KillRangeT RecordConName
    killRange (NamedRecCon QName
    x) = (QName -> RecordConName) -> QName -> RecordConName
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> RecordConName
    NamedRecCon QName
    x
      killRange (FreshRecCon QName
    x) = (QName -> RecordConName) -> QName -> RecordConName
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> RecordConName
    FreshRecCon QName
    x

    instance KillRange e => KillRange (Pattern' e) where
      killRange :: KillRangeT (Pattern' e)
    killRange (VarP BindName
    x)           = (BindName -> Pattern' e) -> BindName -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN BindName -> Pattern' e
    forall e. BindName -> Pattern' e
    VarP BindName
    x
      killRange (ConP ConPatInfo
    i AmbiguousQName
    a NAPs e
    b)        = (ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e)
    -> ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    ConP ConPatInfo
    i AmbiguousQName
    a NAPs e
    b
      killRange (ProjP PatInfo
    i ProjOrigin
    o AmbiguousQName
    a)       = (PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e)
    -> PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    ProjP PatInfo
    i ProjOrigin
    o AmbiguousQName
    a
      killRange (DefP PatInfo
    i AmbiguousQName
    a NAPs e
    b)        = (PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e)
    -> PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    i AmbiguousQName
    a NAPs e
    b
      killRange (WildP PatInfo
    i)           = (PatInfo -> Pattern' e) -> PatInfo -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> Pattern' e
    forall e. PatInfo -> Pattern' e
    WildP PatInfo
    i
      killRange (AsP PatInfo
    i BindName
    a Pattern' e
    b)         = (PatInfo -> BindName -> KillRangeT (Pattern' e))
    -> PatInfo -> BindName -> KillRangeT (Pattern' e)
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> BindName -> KillRangeT (Pattern' e)
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    AsP PatInfo
    i BindName
    a Pattern' e
    b
      killRange (DotP PatInfo
    i e
    a)          = (PatInfo -> e -> Pattern' e) -> PatInfo -> e -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> e -> Pattern' e
    forall e. PatInfo -> e -> Pattern' e
    DotP PatInfo
    i e
    a
      killRange (AbsurdP PatInfo
    i)         = (PatInfo -> Pattern' e) -> PatInfo -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> Pattern' e
    forall e. PatInfo -> Pattern' e
    AbsurdP PatInfo
    i
      killRange (LitP PatInfo
    i Literal
    l)          = (PatInfo -> Literal -> Pattern' e)
    -> PatInfo -> Literal -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> Literal -> Pattern' e
    forall e. PatInfo -> Literal -> Pattern' e
    LitP PatInfo
    i Literal
    l
      killRange (PatternSynP PatInfo
    i AmbiguousQName
    a NAPs e
    p) = (PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e)
    -> PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    PatternSynP PatInfo
    i AmbiguousQName
    a NAPs e
    p
      killRange (RecP KwRange
    kwr ConPatInfo
    i [FieldAssignment' (Pattern' e)]
    as)     = (KwRange
     -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e)
    -> KwRange
    -> ConPatInfo
    -> [FieldAssignment' (Pattern' e)]
    -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    RecP KwRange
    kwr ConPatInfo
    i [FieldAssignment' (Pattern' e)]
    as
      killRange (EqualP PatInfo
    i List1 (e, e)
    es)       = (PatInfo -> List1 (e, e) -> Pattern' e)
    -> PatInfo -> List1 (e, e) -> Pattern' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> List1 (e, e) -> Pattern' e
    forall e. PatInfo -> List1 (e, e) -> Pattern' e
    EqualP PatInfo
    i List1 (e, e)
    es
      killRange (WithP PatInfo
    i Pattern' e
    p)         = (PatInfo -> KillRangeT (Pattern' e))
    -> PatInfo -> KillRangeT (Pattern' e)
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN PatInfo -> KillRangeT (Pattern' e)
    forall e. PatInfo -> Pattern' e -> Pattern' e
    WithP PatInfo
    i Pattern' e
    p

    instance KillRange SpineLHS where
      killRange :: KillRangeT SpineLHS
    killRange (SpineLHS LHSInfo
    i QName
    a [NamedArg Pattern]
    b)  = (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS)
    -> LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
    SpineLHS LHSInfo
    i QName
    a [NamedArg Pattern]
    b

    instance KillRange LHS where
      killRange :: KillRangeT LHS
    killRange (LHS LHSInfo
    i LHSCore
    a)   = (LHSInfo -> LHSCore -> LHS) -> LHSInfo -> LHSCore -> LHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LHSInfo -> LHSCore -> LHS
    LHS LHSInfo
    i LHSCore
    a

    instance KillRange e => KillRange (LHSCore' e) where
      killRange :: KillRangeT (LHSCore' e)
    killRange (LHSHead QName
    a [NamedArg (Pattern' e)]
    b)   = (QName -> [NamedArg (Pattern' e)] -> LHSCore' e)
    -> QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    LHSHead QName
    a [NamedArg (Pattern' e)]
    b
      killRange (LHSProj AmbiguousQName
    a NamedArg (LHSCore' e)
    b [NamedArg (Pattern' e)]
    c) = (AmbiguousQName
     -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e)
    -> AmbiguousQName
    -> NamedArg (LHSCore' e)
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN AmbiguousQName
    -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e.
    AmbiguousQName
    -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
    LHSProj AmbiguousQName
    a NamedArg (LHSCore' e)
    b [NamedArg (Pattern' e)]
    c
      killRange (LHSWith LHSCore' e
    a List1 (Arg (Pattern' e))
    b [NamedArg (Pattern' e)]
    c) = (LHSCore' e
     -> List1 (Arg (Pattern' e))
     -> [NamedArg (Pattern' e)]
     -> LHSCore' e)
    -> LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    LHSWith LHSCore' e
    a List1 (Arg (Pattern' e))
    b [NamedArg (Pattern' e)]
    c

    instance KillRange a => KillRange (Clause' a) where
      killRange :: KillRangeT (Clause' a)
    killRange (Clause a
    lhs [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    ds Catchall
    catchall) = (a
     -> [ProblemEq]
     -> RHS
     -> WhereDeclarations
     -> Catchall
     -> Clause' a)
    -> a
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' a
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN a
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause' a
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    Clause a
    lhs [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    ds Catchall
    catchall

    instance KillRange ProblemEq where
      killRange :: KillRangeT ProblemEq
    killRange (ProblemEq Pattern
    p Term
    v Dom Type
    a) = (Pattern -> Term -> Dom Type -> ProblemEq)
    -> Pattern -> Term -> Dom Type -> ProblemEq
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Pattern -> Term -> Dom Type -> ProblemEq
    ProblemEq Pattern
    p Term
    v Dom Type
    a

    instance KillRange RHS where
      killRange :: RHS -> RHS
    killRange RHS
    AbsurdRHS                = RHS
    AbsurdRHS
      killRange (RHS Expr
    e Maybe Expr
    c)                = (Expr -> Maybe Expr -> RHS) -> Expr -> Maybe Expr -> RHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Expr -> Maybe Expr -> RHS
    RHS Expr
    e Maybe Expr
    c
      killRange (WithRHS QName
    q List1 WithExpr
    e List1 Clause
    cs)         = (QName -> List1 WithExpr -> List1 Clause -> RHS)
    -> QName -> List1 WithExpr -> List1 Clause -> RHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> List1 WithExpr -> List1 Clause -> RHS
    WithRHS QName
    q List1 WithExpr
    e List1 Clause
    cs
      killRange (RewriteRHS [RewriteEqn]
    xes [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    wh) = ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS)
    -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
    RewriteRHS [RewriteEqn]
    xes [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    wh

    instance KillRange WhereDeclarations where
      killRange :: KillRangeT WhereDeclarations
    killRange (WhereDecls Maybe ModuleName
    a Bool
    b Maybe Declaration
    c) = (Maybe ModuleName
     -> Bool -> Maybe Declaration -> WhereDeclarations)
    -> Maybe ModuleName
    -> Bool
    -> Maybe Declaration
    -> WhereDeclarations
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
    WhereDecls Maybe ModuleName
    a Bool
    b Maybe Declaration
    c

    instance KillRange LetBinding where
      killRange :: KillRangeT LetBinding
    killRange (LetBind LetInfo
    i ArgInfo
    info BindName
    a Expr
    b Expr
    c)  = (LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding)
    -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
    LetBind LetInfo
    i ArgInfo
    info BindName
    a Expr
    b Expr
    c
      killRange (LetAxiom LetInfo
    i ArgInfo
    a BindName
    b Expr
    c)      = (LetInfo -> ArgInfo -> BindName -> Expr -> LetBinding)
    -> LetInfo -> ArgInfo -> BindName -> Expr -> LetBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LetInfo -> ArgInfo -> BindName -> Expr -> LetBinding
    LetAxiom LetInfo
    i ArgInfo
    a BindName
    b Expr
    c
      killRange (LetPatBind LetInfo
    i Pattern
    a Expr
    b)      = (LetInfo -> Pattern -> Expr -> LetBinding)
    -> LetInfo -> Pattern -> Expr -> LetBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LetInfo -> Pattern -> Expr -> LetBinding
    LetPatBind LetInfo
    i Pattern
    a Expr
    b
      killRange (LetApply ModuleInfo
    i Erased
    a ModuleName
    b ModuleApplication
    c ScopeCopyInfo
    d ImportDirective
    e)  = (ModuleInfo
     -> Erased
     -> ModuleName
     -> ModuleApplication
     -> ScopeCopyInfo
     -> ImportDirective
     -> LetBinding)
    -> ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> LetBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> LetBinding
    LetApply ModuleInfo
    i Erased
    a ModuleName
    b ModuleApplication
    c ScopeCopyInfo
    d ImportDirective
    e
      killRange (LetOpen ModuleInfo
    i ModuleName
    x ImportDirective
    dir)       = (ModuleInfo -> ModuleName -> ImportDirective -> LetBinding)
    -> ModuleInfo -> ModuleName -> ImportDirective -> LetBinding
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ModuleInfo -> ModuleName -> ImportDirective -> LetBinding
    LetOpen  ModuleInfo
    i ModuleName
    x ImportDirective
    dir

    instance NFData Expr
    instance NFData ScopeCopyInfo
    instance NFData RecordConName
    instance NFData Declaration
    instance NFData ModuleApplication
    instance NFData Pragma
    instance NFData LetBinding
    instance NFData a => NFData (Binder' a)
    instance NFData LamBinding
    instance NFData TypedBinding
    instance NFData TypedBindingInfo
    instance NFData GeneralizeTelescope
    instance NFData DataDefParams
    instance NFData ProblemEq
    instance NFData lhs => NFData (Clause' lhs)
    instance NFData WhereDeclarations
    instance NFData RHS
    instance NFData SpineLHS
    instance NFData LHS
    instance NFData e => NFData (LHSCore' e)
    instance NFData e => NFData (Pattern' e)

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

    -- class AllNames moved to Abstract.Views.DeclaredNames

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

    axiomName :: Declaration -> QName
    axiomName :: Declaration -> QName
    axiomName (Axiom KindOfName
    _ DefInfo
    _ ArgInfo
    _ Maybe PragmaPolarities
    _ QName
    q Expr
    _)  = QName
    q
    axiomName (ScopedDecl ScopeInfo
    _ (Declaration
    d:[Declaration]
    _)) = Declaration -> QName
    axiomName Declaration
    d
    axiomName Declaration
    _                    = QName
    forall a. HasCallStack => a
    __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 :: [a] -> Bool
    anyAbstract = (a -> Bool) -> [a] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    Fold.any a -> Bool
    forall a. AnyAbstract a => a -> Bool
    anyAbstract

    instance AnyAbstract Declaration where
      anyAbstract :: Declaration -> Bool
    anyAbstract (Axiom KindOfName
    _ DefInfo
    i ArgInfo
    _ Maybe PragmaPolarities
    _ QName
    _ Expr
    _)    = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract (Field DefInfo
    i QName
    _ Arg Expr
    _)          = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract (Mutual     MutualInfo
    _ [Declaration]
    ds)      = [Declaration] -> Bool
    forall a. AnyAbstract a => a -> Bool
    anyAbstract [Declaration]
    ds
      anyAbstract (ScopedDecl ScopeInfo
    _ [Declaration]
    ds)      = [Declaration] -> Bool
    forall a. AnyAbstract a => a -> Bool
    anyAbstract [Declaration]
    ds
      anyAbstract (Section Range
    _ Erased
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    ds)   = [Declaration] -> Bool
    forall a. AnyAbstract a => a -> Bool
    anyAbstract [Declaration]
    ds
      anyAbstract (FunDef DefInfo
    i QName
    _ [Clause]
    _)         = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract (DataDef DefInfo
    i QName
    _ UniverseCheck
    _ DataDefParams
    _ [Declaration]
    _)    = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract (RecDef DefInfo
    i QName
    _ UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Expr
    _ [Declaration]
    _) = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract (DataSig DefInfo
    i Erased
    _ QName
    _ GeneralizeTelescope
    _ Expr
    _)    = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract (RecSig DefInfo
    i Erased
    _ QName
    _ GeneralizeTelescope
    _ Expr
    _)     = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef
      anyAbstract Declaration
    _                      = Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Turn a name into an expression.

    class NameToExpr a where
      nameToExpr :: a -> Expr

    -- | Turn an 'AbstractName' into an expression.

    instance NameToExpr AbstractName where
      nameToExpr :: AbstractName -> Expr
    nameToExpr AbstractName
    d =
        case AbstractName -> KindOfName
    anameKind AbstractName
    d of
          KindOfName
    DataName                 -> QName -> Expr
    Def QName
    x
          KindOfName
    RecName                  -> QName -> Expr
    Def QName
    x
          KindOfName
    AxiomName                -> QName -> Expr
    Def QName
    x
          KindOfName
    PrimName                 -> QName -> Expr
    Def QName
    x
          KindOfName
    FunName                  -> QName -> Expr
    Def QName
    x
          KindOfName
    OtherDefName             -> QName -> Expr
    Def QName
    x
          KindOfName
    GeneralizeName           -> QName -> Expr
    Def QName
    x
          KindOfName
    DisallowedGeneralizeName -> QName -> Expr
    Def QName
    x
          KindOfName
    FldName                  -> ProjOrigin -> AmbiguousQName -> Expr
    Proj ProjOrigin
    ProjSystem AmbiguousQName
    ux
          KindOfName
    ConName                  -> AmbiguousQName -> Expr
    Con AmbiguousQName
    ux
          KindOfName
    CoConName                -> AmbiguousQName -> Expr
    Con AmbiguousQName
    ux
          KindOfName
    PatternSynName           -> AmbiguousQName -> Expr
    PatternSyn AmbiguousQName
    ux
          KindOfName
    MacroName                -> QName -> Expr
    Macro QName
    x
          KindOfName
    QuotableName             -> AppInfo -> Expr -> NamedArg Expr -> Expr
    App (Range -> AppInfo
    defaultAppInfo Range
    r) (ExprInfo -> Expr
    Quote ExprInfo
    i) (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg (Expr -> NamedArg Expr) -> Expr -> NamedArg Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Expr
    Def QName
    x)
        where
        x :: QName
    x  = AbstractName -> QName
    anameName AbstractName
    d
        ux :: AmbiguousQName
    ux = QName -> AmbiguousQName
    unambiguous QName
    x
        r :: Range
    r  = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x
        i :: ExprInfo
    i  = Range -> ExprInfo
    ExprRange Range
    r

    -- | Turn a 'ResolvedName' into an expression.
    --
    --   Assumes name is not 'UnknownName'.

    instance NameToExpr ResolvedName where
      nameToExpr :: ResolvedName -> Expr
    nameToExpr = \case
        VarName Name
    x BindingSource
    _          -> Name -> Expr
    Var Name
    x
        DefinedName Access
    _ AbstractName
    x Suffix
    s    -> Suffix -> Expr -> Expr
    withSuffix Suffix
    s (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> Expr
    forall a. NameToExpr a => a -> Expr
    nameToExpr AbstractName
    x  -- Can be 'isDefName', 'MacroName', 'QuotableName'.
        FieldName List1 AbstractName
    xs         -> ProjOrigin -> AmbiguousQName -> Expr
    Proj ProjOrigin
    ProjSystem (AmbiguousQName -> Expr)
    -> (List1 AbstractName -> AmbiguousQName)
    -> List1 AbstractName
    -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty QName -> AmbiguousQName
    AmbQ (NonEmpty QName -> AmbiguousQName)
    -> (List1 AbstractName -> NonEmpty QName)
    -> List1 AbstractName
    -> AmbiguousQName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> QName) -> List1 AbstractName -> NonEmpty QName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractName -> QName
    anameName (List1 AbstractName -> Expr) -> List1 AbstractName -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName
    xs
        ConstructorName Set1 Induction
    _ List1 AbstractName
    xs -> AmbiguousQName -> Expr
    Con (AmbiguousQName -> Expr)
    -> (List1 AbstractName -> AmbiguousQName)
    -> List1 AbstractName
    -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty QName -> AmbiguousQName
    AmbQ (NonEmpty QName -> AmbiguousQName)
    -> (List1 AbstractName -> NonEmpty QName)
    -> List1 AbstractName
    -> AmbiguousQName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> QName) -> List1 AbstractName -> NonEmpty QName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractName -> QName
    anameName (List1 AbstractName -> Expr) -> List1 AbstractName -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName
    xs
        PatternSynResName List1 AbstractName
    xs -> AmbiguousQName -> Expr
    PatternSyn (AmbiguousQName -> Expr)
    -> (List1 AbstractName -> AmbiguousQName)
    -> List1 AbstractName
    -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty QName -> AmbiguousQName
    AmbQ (NonEmpty QName -> AmbiguousQName)
    -> (List1 AbstractName -> NonEmpty QName)
    -> List1 AbstractName
    -> AmbiguousQName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> QName) -> List1 AbstractName -> NonEmpty QName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractName -> QName
    anameName (List1 AbstractName -> Expr) -> List1 AbstractName -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName
    xs
        ResolvedName
    UnknownName          -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        where
          withSuffix :: Suffix -> Expr -> Expr
    withSuffix Suffix
    NoSuffix   Expr
    e       = Expr
    e
          withSuffix s :: Suffix
    s@Suffix{} (Def QName
    x) = QName -> Suffix -> Expr
    Def' QName
    x Suffix
    s
          withSuffix Suffix
    _          Expr
    _       = Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    app :: Expr -> [NamedArg Expr] -> Expr
    app :: Expr -> [NamedArg Expr] -> Expr
    app = (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    defaultAppInfo_)

    mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
    mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
    mkLet ExprInfo
    _ []     Expr
    e = Expr
    e
    mkLet ExprInfo
    i (LetBinding
    d:[LetBinding]
    ds) Expr
    e = ExprInfo -> List1 LetBinding -> Expr -> Expr
    Let ExprInfo
    i (LetBinding
    d LetBinding -> [LetBinding] -> List1 LetBinding
    forall a. a -> [a] -> NonEmpty a
    :| [LetBinding]
    ds) Expr
    e

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

    lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr
    lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr
    lambdaLiftExpr [WithHiding Name]
    ns Expr
    e = (WithHiding Name -> Expr -> Expr)
    -> Expr -> [WithHiding Name] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr WithHiding Name -> Expr -> Expr
    f Expr
    e [WithHiding Name]
    ns
      where
      f :: WithHiding Name -> Expr -> Expr
    f (WithHiding Hiding
    h Name
    n) = ExprInfo -> LamBinding -> Expr -> Expr
    Lam ExprInfo
    exprNoRange (LamBinding -> Expr -> Expr) -> LamBinding -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Hiding -> LamBinding -> LamBinding
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    h (LamBinding -> LamBinding) -> LamBinding -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> LamBinding
    mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ Binder -> NamedArg Binder
    forall a. a -> NamedArg a
    defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    mkBinder_ Name
    n

    -- NOTE: This is only used on expressions that come from right-hand sides of pattern synonyms, and
    -- thus does not have to handle all forms of expressions.
    class SubstExpr a where
      substExpr :: [(Name, Expr)] -> a -> a

      default substExpr
        :: (Functor t, SubstExpr b, t b ~ a)
        => [(Name, Expr)] -> a -> a
      substExpr = (b -> b) -> a -> a
    (b -> b) -> t b -> t b
    forall a b. (a -> b) -> t a -> t b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b -> b) -> a -> a)
    -> ([(Name, Expr)] -> b -> b) -> [(Name, Expr)] -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Name, Expr)] -> b -> b
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr

    instance SubstExpr a => SubstExpr (Maybe a)
    instance SubstExpr a => SubstExpr [a]
    instance SubstExpr a => SubstExpr (List1 a)
    instance SubstExpr a => SubstExpr (Arg a)
    instance SubstExpr a => SubstExpr (Named name a)
    instance SubstExpr a => SubstExpr (FieldAssignment' a)

    instance (SubstExpr a, SubstExpr b) => SubstExpr (a, b) where
      substExpr :: [(Name, Expr)] -> (a, b) -> (a, b)
    substExpr [(Name, Expr)]
    s (a
    x, b
    y) = ([(Name, Expr)] -> a -> a
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s a
    x, [(Name, Expr)] -> b -> b
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s b
    y)

    instance (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) where
      substExpr :: [(Name, Expr)] -> Either a b -> Either a b
    substExpr [(Name, Expr)]
    s (Left a
    x)  = a -> Either a b
    forall a b. a -> Either a b
    Left ([(Name, Expr)] -> a -> a
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s a
    x)
      substExpr [(Name, Expr)]
    s (Right b
    y) = b -> Either a b
    forall a b. b -> Either a b
    Right ([(Name, Expr)] -> b -> b
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s b
    y)

    instance SubstExpr C.Name where
      substExpr :: [(Name, Expr)] -> Name -> Name
    substExpr [(Name, Expr)]
    _ = Name -> Name
    forall a. a -> a
    id

    instance SubstExpr ModuleName where
      substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName
    substExpr [(Name, Expr)]
    _ = ModuleName -> ModuleName
    forall a. a -> a
    id

    instance SubstExpr Expr where
      substExpr :: [(Name, Expr)] -> Expr -> Expr
    substExpr [(Name, Expr)]
    s Expr
    e = case Expr
    e of
        Var Name
    n           -> Expr -> Maybe Expr -> Expr
    forall a. a -> Maybe a -> a
    fromMaybe Expr
    e (Name -> [(Name, Expr)] -> Maybe Expr
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Name
    n [(Name, Expr)]
    s)
        Con AmbiguousQName
    _           -> Expr
    e
        Proj{}          -> Expr
    e
        Def' QName
    _ Suffix
    _        -> Expr
    e
        PatternSyn{}    -> Expr
    e
        Lit ExprInfo
    _ Literal
    _         -> Expr
    e
        Underscore   MetaInfo
    _  -> Expr
    e
        App  AppInfo
    i Expr
    e NamedArg Expr
    e'     -> AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    i ([(Name, Expr)] -> Expr -> Expr
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s Expr
    e) ([(Name, Expr)] -> NamedArg Expr -> NamedArg Expr
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s NamedArg Expr
    e')
        Rec KwRange
    kwr ExprInfo
    i RecordAssigns
    nes   -> KwRange -> ExprInfo -> RecordAssigns -> Expr
    Rec KwRange
    kwr ExprInfo
    i ([(Name, Expr)] -> RecordAssigns -> RecordAssigns
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s RecordAssigns
    nes)
        ScopedExpr ScopeInfo
    si Expr
    e -> ScopeInfo -> Expr -> Expr
    ScopedExpr ScopeInfo
    si ([(Name, Expr)] -> Expr -> Expr
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr [(Name, Expr)]
    s Expr
    e)
        -- The below cannot appear in pattern synonym right-hand sides
        QuestionMark{}  -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Dot{}           -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        WithApp{}       -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Lam{}           -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        AbsurdLam{}     -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        ExtendedLam{}   -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Pi{}            -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Generalized{}   -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Fun{}           -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Let{}           -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        RecUpdate{}     -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Quote{}         -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        QuoteTerm{}     -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Unquote{}       -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        DontCare{}      -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Macro{}         -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- TODO: more informative failure
    insertImplicitPatSynArgs :: forall a. HasRange a
      => (Hiding -> Range -> a)
           -- ^ Thing to insert (wildcard).
      -> Range
           -- ^ Range of the whole pattern synonym expression/pattern.
      -> [WithHiding Name]
           -- ^ The parameters of the pattern synonym (from its definition).
      -> [NamedArg a]
           -- ^ The arguments it is used with.
      -> Maybe ([(Name, a)], [WithHiding Name])
           -- ^ Substitution and left-over parameters.
    insertImplicitPatSynArgs :: forall a.
    HasRange a =>
    (Hiding -> Range -> a)
    -> Range
    -> [WithHiding Name]
    -> [NamedArg a]
    -> Maybe ([(Name, a)], [WithHiding Name])
    insertImplicitPatSynArgs Hiding -> Range -> a
    wild Range
    r [WithHiding Name]
    ns [NamedArg a]
    as = Range
    -> [WithHiding Name]
    -> [NamedArg a]
    -> Maybe ([(Name, a)], [WithHiding Name])
    matchArgs Range
    r [WithHiding Name]
    ns [NamedArg a]
    as
      where
        matchNextArg :: Range -> WithHiding Name -> [NamedArg a] -> Maybe (a, [NamedArg a])
        matchNextArg :: Range -> WithHiding Name -> [NamedArg a] -> Maybe (a, [NamedArg a])
    matchNextArg Range
    r WithHiding Name
    n as :: [NamedArg a]
    as@(~(NamedArg a
    a : [NamedArg a]
    as'))
          | Bool -> Bool
    not ([NamedArg a] -> Bool
    forall a. Null a => a -> Bool
    null [NamedArg a]
    as)
          , WithHiding Name -> NamedArg a -> Bool
    matchNext WithHiding Name
    n NamedArg a
    a  = (a, [NamedArg a]) -> Maybe (a, [NamedArg a])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NamedArg a -> a
    forall a. NamedArg a -> a
    namedArg NamedArg a
    a, [NamedArg a]
    as')
          | WithHiding Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible WithHiding Name
    n      = Maybe (a, [NamedArg a])
    forall a. Maybe a
    Nothing
          | Bool
    otherwise      = (a, [NamedArg a]) -> Maybe (a, [NamedArg a])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Hiding -> Range -> a
    wild (WithHiding Name -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding WithHiding Name
    n) Range
    r, [NamedArg a]
    as)

        matchNext ::
             WithHiding Name  -- Pattern synonym parameter
          -> NamedArg a       -- Argument given to pattern synonym
          -> Bool
        matchNext :: WithHiding Name -> NamedArg a -> Bool
    matchNext WithHiding Name
    n NamedArg a
    a = WithHiding Name -> NamedArg a -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding WithHiding Name
    n NamedArg a
    a Bool -> Bool -> Bool
    && Bool -> (String -> Bool) -> Maybe String -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (String
    x String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (NamedArg a -> Maybe String
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
    bareNameOf NamedArg a
    a)
          where
            x :: String
    x = Name -> String
    C.nameToRawName (Name -> String) -> Name -> String
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ WithHiding Name -> Name
    forall a. WithHiding a -> a
    whThing WithHiding Name
    n

        matchArgs ::
             Range
          -> [WithHiding Name]
          -> [NamedArg a]
          -> Maybe ([(Name, a)], [WithHiding Name])
        matchArgs :: Range
    -> [WithHiding Name]
    -> [NamedArg a]
    -> Maybe ([(Name, a)], [WithHiding Name])
    matchArgs Range
    r [] []     = ([(Name, a)], [WithHiding Name])
    -> Maybe ([(Name, a)], [WithHiding Name])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [])
        matchArgs Range
    r [] [NamedArg a]
    as     = Maybe ([(Name, a)], [WithHiding Name])
    forall a. Maybe a
    Nothing
        matchArgs Range
    r (WithHiding Name
    n:[WithHiding Name]
    ns) [] | WithHiding Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible WithHiding Name
    n = ([(Name, a)], [WithHiding Name])
    -> Maybe ([(Name, a)], [WithHiding Name])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], WithHiding Name
    n WithHiding Name -> [WithHiding Name] -> [WithHiding Name]
    forall a. a -> [a] -> [a]
    : [WithHiding Name]
    ns)    -- under-applied
        matchArgs Range
    r (WithHiding Name
    n:[WithHiding Name]
    ns) [NamedArg a]
    as = do
          (p, as) <- Range -> WithHiding Name -> [NamedArg a] -> Maybe (a, [NamedArg a])
    matchNextArg Range
    r WithHiding Name
    n [NamedArg a]
    as
          first ((whThing n, p) :) <$> matchArgs (getRange p) ns as

    ------------------------------------------------------------------------
    -- Declaration spines
    ------------------------------------------------------------------------

    -- | Declaration spines. Used in debugging to make it easy to see
    -- where constructors such as 'ScopedDecl' and 'Mutual' are placed.

    data DeclarationSpine
      = AxiomS
      | GeneralizeS
      | FieldS
      | PrimitiveS
      | MutualS [DeclarationSpine]
      | SectionS [DeclarationSpine]
      | ApplyS
      | ImportS
      | PragmaS
      | OpenS
      | FunDefS [ClauseSpine]
      | DataSigS
      | DataDefS
      | RecSigS
      | RecDefS [DeclarationSpine]
      | PatternSynDefS
      | UnquoteDeclS
      | UnquoteDefS
      | UnquoteDataS
      | ScopedDeclS [DeclarationSpine]
      | UnfoldingDeclS
      deriving Int -> DeclarationSpine -> ShowS
    [DeclarationSpine] -> ShowS
    DeclarationSpine -> String
    (Int -> DeclarationSpine -> ShowS)
    -> (DeclarationSpine -> String)
    -> ([DeclarationSpine] -> ShowS)
    -> Show DeclarationSpine
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DeclarationSpine -> ShowS
    showsPrec :: Int -> DeclarationSpine -> ShowS
    $cshow :: DeclarationSpine -> String
    show :: DeclarationSpine -> String
    $cshowList :: [DeclarationSpine] -> ShowS
    showList :: [DeclarationSpine] -> ShowS
    Show

    -- | Clause spines.

    data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
      deriving Int -> ClauseSpine -> ShowS
    [ClauseSpine] -> ShowS
    ClauseSpine -> String
    (Int -> ClauseSpine -> ShowS)
    -> (ClauseSpine -> String)
    -> ([ClauseSpine] -> ShowS)
    -> Show ClauseSpine
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ClauseSpine -> ShowS
    showsPrec :: Int -> ClauseSpine -> ShowS
    $cshow :: ClauseSpine -> String
    show :: ClauseSpine -> String
    $cshowList :: [ClauseSpine] -> ShowS
    showList :: [ClauseSpine] -> ShowS
    Show

    -- | Right-hand side spines.

    data RHSSpine
      = RHSS
      | AbsurdRHSS
      | WithRHSS (List1 ClauseSpine)
      | RewriteRHSS RHSSpine WhereDeclarationsSpine
      deriving Int -> RHSSpine -> ShowS
    [RHSSpine] -> ShowS
    RHSSpine -> String
    (Int -> RHSSpine -> ShowS)
    -> (RHSSpine -> String) -> ([RHSSpine] -> ShowS) -> Show RHSSpine
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RHSSpine -> ShowS
    showsPrec :: Int -> RHSSpine -> ShowS
    $cshow :: RHSSpine -> String
    show :: RHSSpine -> String
    $cshowList :: [RHSSpine] -> ShowS
    showList :: [RHSSpine] -> ShowS
    Show

    -- | Spines corresponding to 'WhereDeclarations' values.

    data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
      deriving Int -> WhereDeclarationsSpine -> ShowS
    [WhereDeclarationsSpine] -> ShowS
    WhereDeclarationsSpine -> String
    (Int -> WhereDeclarationsSpine -> ShowS)
    -> (WhereDeclarationsSpine -> String)
    -> ([WhereDeclarationsSpine] -> ShowS)
    -> Show WhereDeclarationsSpine
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> WhereDeclarationsSpine -> ShowS
    showsPrec :: Int -> WhereDeclarationsSpine -> ShowS
    $cshow :: WhereDeclarationsSpine -> String
    show :: WhereDeclarationsSpine -> String
    $cshowList :: [WhereDeclarationsSpine] -> ShowS
    showList :: [WhereDeclarationsSpine] -> ShowS
    Show

    -- | The declaration spine corresponding to a declaration.

    declarationSpine :: Declaration -> DeclarationSpine
    declarationSpine :: Declaration -> DeclarationSpine
    declarationSpine = \case
      Axiom KindOfName
    _ DefInfo
    _ ArgInfo
    _ Maybe PragmaPolarities
    _ QName
    _ Expr
    _       -> DeclarationSpine
    AxiomS
      Generalize Set QName
    _ DefInfo
    _ ArgInfo
    _ QName
    _ Expr
    _    -> DeclarationSpine
    GeneralizeS
      Field DefInfo
    _ QName
    _ Arg Expr
    _             -> DeclarationSpine
    FieldS
      Primitive DefInfo
    _ QName
    _ Arg Expr
    _         -> DeclarationSpine
    PrimitiveS
      Mutual MutualInfo
    _ [Declaration]
    ds             -> [DeclarationSpine] -> DeclarationSpine
    MutualS ((Declaration -> DeclarationSpine)
    -> [Declaration] -> [DeclarationSpine]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> DeclarationSpine
    declarationSpine [Declaration]
    ds)
      Section Range
    _ Erased
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    ds      -> [DeclarationSpine] -> DeclarationSpine
    SectionS ((Declaration -> DeclarationSpine)
    -> [Declaration] -> [DeclarationSpine]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> DeclarationSpine
    declarationSpine [Declaration]
    ds)
      Apply ModuleInfo
    _ Erased
    _ ModuleName
    _ ModuleApplication
    _ ScopeCopyInfo
    _ ImportDirective
    _       -> DeclarationSpine
    ApplyS
      Import ModuleInfo
    _ ModuleName
    _ ImportDirective
    _            -> DeclarationSpine
    ImportS
      Pragma Range
    _ Pragma
    _              -> DeclarationSpine
    PragmaS
      Open ModuleInfo
    _ ModuleName
    _ ImportDirective
    _              -> DeclarationSpine
    OpenS
      FunDef DefInfo
    _ QName
    _ [Clause]
    cs           -> [ClauseSpine] -> DeclarationSpine
    FunDefS ((Clause -> ClauseSpine) -> [Clause] -> [ClauseSpine]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> ClauseSpine
    clauseSpine [Clause]
    cs)
      DataSig DefInfo
    _ Erased
    _ QName
    _ GeneralizeTelescope
    _ Expr
    _       -> DeclarationSpine
    DataSigS
      DataDef DefInfo
    _ QName
    _ UniverseCheck
    _ DataDefParams
    _ [Declaration]
    _       -> DeclarationSpine
    DataDefS
      RecSig DefInfo
    _ Erased
    _ QName
    _ GeneralizeTelescope
    _ Expr
    _        -> DeclarationSpine
    RecSigS
      RecDef DefInfo
    _ QName
    _ UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Expr
    _ [Declaration]
    ds   -> [DeclarationSpine] -> DeclarationSpine
    RecDefS ((Declaration -> DeclarationSpine)
    -> [Declaration] -> [DeclarationSpine]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> DeclarationSpine
    declarationSpine [Declaration]
    ds)
      PatternSynDef QName
    _ [WithHiding BindName]
    _ Pattern' Void
    _     -> DeclarationSpine
    PatternSynDefS
      UnquoteDecl MutualInfo
    _ [DefInfo]
    _ [QName]
    _ Expr
    _     -> DeclarationSpine
    UnquoteDeclS
      UnquoteDef [DefInfo]
    _ [QName]
    _ Expr
    _        -> DeclarationSpine
    UnquoteDefS
      UnquoteData [DefInfo]
    _ QName
    _ UniverseCheck
    _ [DefInfo]
    _ [QName]
    _ Expr
    _ -> DeclarationSpine
    UnquoteDataS
      ScopedDecl ScopeInfo
    _ [Declaration]
    ds         -> [DeclarationSpine] -> DeclarationSpine
    ScopedDeclS ((Declaration -> DeclarationSpine)
    -> [Declaration] -> [DeclarationSpine]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> DeclarationSpine
    declarationSpine [Declaration]
    ds)
      UnfoldingDecl Range
    _ [QName]
    _       -> DeclarationSpine
    UnquoteDeclS

    -- | The clause spine corresponding to a clause.

    clauseSpine :: Clause -> ClauseSpine
    clauseSpine :: Clause -> ClauseSpine
    clauseSpine (Clause LHS
    _ [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    ws Catchall
    _) =
      RHSSpine -> WhereDeclarationsSpine -> ClauseSpine
    ClauseS (RHS -> RHSSpine
    rhsSpine RHS
    rhs) (WhereDeclarations -> WhereDeclarationsSpine
    whereDeclarationsSpine WhereDeclarations
    ws)

    -- | The right-hand side spine corresponding to a right-hand side.

    rhsSpine :: RHS -> RHSSpine
    rhsSpine :: RHS -> RHSSpine
    rhsSpine = \case
      RHS Expr
    _ Maybe Expr
    _               -> RHSSpine
    RHSS
      RHS
    AbsurdRHS             -> RHSSpine
    AbsurdRHSS
      WithRHS QName
    _ List1 WithExpr
    _ List1 Clause
    cs        -> List1 ClauseSpine -> RHSSpine
    WithRHSS (List1 ClauseSpine -> RHSSpine) -> List1 ClauseSpine -> RHSSpine
    forall a b. (a -> b) -> a -> b
    $ (Clause -> ClauseSpine) -> List1 Clause -> List1 ClauseSpine
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Clause -> ClauseSpine
    clauseSpine List1 Clause
    cs
      RewriteRHS [RewriteEqn]
    _ [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    ws ->
        RHSSpine -> WhereDeclarationsSpine -> RHSSpine
    RewriteRHSS (RHS -> RHSSpine
    rhsSpine RHS
    rhs) (WhereDeclarations -> WhereDeclarationsSpine
    whereDeclarationsSpine WhereDeclarations
    ws)

    -- | The spine corresponding to a 'WhereDeclarations' value.

    whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
    whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
    whereDeclarationsSpine (WhereDecls Maybe ModuleName
    _ Bool
    _ Maybe Declaration
    md) =
      Maybe DeclarationSpine -> WhereDeclarationsSpine
    WhereDeclsS ((Declaration -> DeclarationSpine)
    -> Maybe Declaration -> Maybe DeclarationSpine
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Declaration -> DeclarationSpine
    declarationSpine Maybe Declaration
    md)