    {-# LANGUAGE CPP #-}
    {-# LANGUAGE ApplicativeDo #-}  -- see exprToPattern

    {-| The concrete syntax is a raw representation of the program text
        without any desugaring at all.  This is what the parser produces.
        The idea is that if we figure out how to keep the concrete syntax
        around, it can be printed exactly as the user wrote it.
    -}
    module Agda.Syntax.Concrete
      ( -- * Expressions
        Expr(..)
      , OpApp(..), fromOrdinary
      , OpAppArgs, OpAppArgs', OpAppArgs0
      , module Agda.Syntax.Concrete.Name
      , AppView(..), appView, unAppView
      , toNamedArg, unNamedArg
      , rawApp, rawAppP
      , isSingleIdentifierP, removeParenP
      , isPattern, isAbsurdP, isBinderP
      , observeHiding
      , observeRelevance
      , observeModifiers
      , exprToPatternWithHoles
      , returnExpr
        -- * Bindings
      , Binder'(..)
      , Binder
      , mkBinder_
      , mkBinder
      , LamBinding
      , LamBinding'(..)
      , dropTypeAndModality
      , TypedBinding
      , TypedBinding'(..)
      , RecordAssignment
      , RecordAssignments
      , FieldAssignment, FieldAssignment'(..), nameFieldA, exprFieldA
      , ModuleAssignment(..)
      , BoundName(..), mkBoundName_, mkBoundName
      , TacticAttribute
      , TacticAttribute'(..)
      , Telescope, Telescope1
      , lamBindingsToTelescope
      , makePi
      , mkLam, mkLet, mkTLet
        -- * Declarations
      , Declaration(..)
      , isPragma
      , RecordDirective(..)
      , RecordDirectives
      , ModuleApplication(..)
      , TypeSignature
      , TypeSignatureOrInstanceBlock
      , ImportDirective, Using, ImportedName
      , Renaming, RenamingDirective, HidingDirective
      , AsName'(..), AsName
      , OpenShortHand(..), RewriteEqn, WithExpr
      , LHS(..), Pattern(..), LHSCore(..)
      , LamClause(..)
      , RHS, RHS'(..)
      , WhereClause, WhereClause'(..), WhereClause_(..), ExprWhere(..)
      , whereClause_
      , DoStmt(..)
      , Pragma(..)
      , Module(..)
      , ThingWithFixity(..)
      , HoleContent, HoleContent'(..)
      , spanAllowedBeforeModule
      , ungatherRecordDirectives
      )
      where

    import Prelude hiding (null)

    import Control.DeepSeq

    import Data.Bifunctor   ( second )
    import Data.DList       ( DList )
    import qualified Data.DList as DL
    import Data.Function    ( (&) )
    import Data.Functor.Identity
    import Data.Maybe
    import Data.Text        ( Text )
    -- import Data.Traversable ( forM )

    import GHC.Generics     ( Generic )

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Aspect (NameKind)
    import Agda.Syntax.Fixity
    import Agda.Syntax.Literal

    import Agda.Syntax.Concrete.Name
    import qualified Agda.Syntax.Abstract.Name as A

    import Agda.TypeChecking.Positivity.Occurrence

    import Agda.Utils.Applicative ( forA )
    import Agda.Utils.Either      ( maybeLeft )
    import Agda.Utils.Lens
    import Agda.Utils.List1       ( List1, pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.List2       ( List2, pattern List2 )
    import Agda.Utils.Null
    import Agda.Utils.Set1        ( Set1 )
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    data OpApp e
      = SyntaxBindingLambda Range (List1 LamBinding) e
        -- ^ An abstraction inside a special syntax declaration
        --   (see Issue 358 why we introduce this).
      | Ordinary e
      deriving ((forall a b. (a -> b) -> OpApp a -> OpApp b)
    -> (forall a b. a -> OpApp b -> OpApp a) -> Functor OpApp
    forall a b. a -> OpApp b -> OpApp a
    forall a b. (a -> b) -> OpApp a -> OpApp 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) -> OpApp a -> OpApp b
    fmap :: forall a b. (a -> b) -> OpApp a -> OpApp b
    $c<$ :: forall a b. a -> OpApp b -> OpApp a
    <$ :: forall a b. a -> OpApp b -> OpApp a
    Functor, (forall m. Monoid m => OpApp m -> m)
    -> (forall m a. Monoid m => (a -> m) -> OpApp a -> m)
    -> (forall m a. Monoid m => (a -> m) -> OpApp a -> m)
    -> (forall a b. (a -> b -> b) -> b -> OpApp a -> b)
    -> (forall a b. (a -> b -> b) -> b -> OpApp a -> b)
    -> (forall b a. (b -> a -> b) -> b -> OpApp a -> b)
    -> (forall b a. (b -> a -> b) -> b -> OpApp a -> b)
    -> (forall a. (a -> a -> a) -> OpApp a -> a)
    -> (forall a. (a -> a -> a) -> OpApp a -> a)
    -> (forall a. OpApp a -> [a])
    -> (forall a. OpApp a -> Bool)
    -> (forall a. OpApp a -> Int)
    -> (forall a. Eq a => a -> OpApp a -> Bool)
    -> (forall a. Ord a => OpApp a -> a)
    -> (forall a. Ord a => OpApp a -> a)
    -> (forall a. Num a => OpApp a -> a)
    -> (forall a. Num a => OpApp a -> a)
    -> Foldable OpApp
    forall a. Eq a => a -> OpApp a -> Bool
    forall a. Num a => OpApp a -> a
    forall a. Ord a => OpApp a -> a
    forall m. Monoid m => OpApp m -> m
    forall a. OpApp a -> Bool
    forall a. OpApp a -> Int
    forall a. OpApp a -> [a]
    forall a. (a -> a -> a) -> OpApp a -> a
    forall m a. Monoid m => (a -> m) -> OpApp a -> m
    forall b a. (b -> a -> b) -> b -> OpApp a -> b
    forall a b. (a -> b -> b) -> b -> OpApp 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 => OpApp m -> m
    fold :: forall m. Monoid m => OpApp m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> OpApp a -> a
    foldr1 :: forall a. (a -> a -> a) -> OpApp a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> OpApp a -> a
    foldl1 :: forall a. (a -> a -> a) -> OpApp a -> a
    $ctoList :: forall a. OpApp a -> [a]
    toList :: forall a. OpApp a -> [a]
    $cnull :: forall a. OpApp a -> Bool
    null :: forall a. OpApp a -> Bool
    $clength :: forall a. OpApp a -> Int
    length :: forall a. OpApp a -> Int
    $celem :: forall a. Eq a => a -> OpApp a -> Bool
    elem :: forall a. Eq a => a -> OpApp a -> Bool
    $cmaximum :: forall a. Ord a => OpApp a -> a
    maximum :: forall a. Ord a => OpApp a -> a
    $cminimum :: forall a. Ord a => OpApp a -> a
    minimum :: forall a. Ord a => OpApp a -> a
    $csum :: forall a. Num a => OpApp a -> a
    sum :: forall a. Num a => OpApp a -> a
    $cproduct :: forall a. Num a => OpApp a -> a
    product :: forall a. Num a => OpApp a -> a
    Foldable, Functor OpApp
    Foldable OpApp
    (Functor OpApp, Foldable OpApp) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> OpApp a -> f (OpApp b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        OpApp (f a) -> f (OpApp a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> OpApp a -> m (OpApp b))
    -> (forall (m :: * -> *) a. Monad m => OpApp (m a) -> m (OpApp a))
    -> Traversable OpApp
    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 => OpApp (m a) -> m (OpApp a)
    forall (f :: * -> *) a. Applicative f => OpApp (f a) -> f (OpApp a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> OpApp a -> m (OpApp b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> OpApp a -> f (OpApp b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> OpApp a -> f (OpApp b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> OpApp a -> f (OpApp b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => OpApp (f a) -> f (OpApp a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => OpApp (f a) -> f (OpApp a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> OpApp a -> m (OpApp b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> OpApp a -> m (OpApp b)
    $csequence :: forall (m :: * -> *) a. Monad m => OpApp (m a) -> m (OpApp a)
    sequence :: forall (m :: * -> *) a. Monad m => OpApp (m a) -> m (OpApp a)
    Traversable, OpApp e -> OpApp e -> Bool
    (OpApp e -> OpApp e -> Bool)
    -> (OpApp e -> OpApp e -> Bool) -> Eq (OpApp e)
    forall e. Eq e => OpApp e -> OpApp e -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall e. Eq e => OpApp e -> OpApp e -> Bool
    == :: OpApp e -> OpApp e -> Bool
    $c/= :: forall e. Eq e => OpApp e -> OpApp e -> Bool
    /= :: OpApp e -> OpApp e -> Bool
    Eq)

    fromOrdinary :: e -> OpApp e -> e
    fromOrdinary :: forall e. e -> OpApp e -> e
    fromOrdinary e
    d (Ordinary e
    e) = e
    e
    fromOrdinary e
    d OpApp e
    _            = e
    d

    data FieldAssignment' a = FieldAssignment { forall a. FieldAssignment' a -> Name
    _nameFieldA :: Name, forall a. FieldAssignment' a -> a
    _exprFieldA :: a }
      deriving ((forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b)
    -> (forall a b. a -> FieldAssignment' b -> FieldAssignment' a)
    -> Functor FieldAssignment'
    forall a b. a -> FieldAssignment' b -> FieldAssignment' a
    forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' 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) -> FieldAssignment' a -> FieldAssignment' b
    fmap :: forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
    $c<$ :: forall a b. a -> FieldAssignment' b -> FieldAssignment' a
    <$ :: forall a b. a -> FieldAssignment' b -> FieldAssignment' a
    Functor, (forall m. Monoid m => FieldAssignment' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b)
    -> (forall a. (a -> a -> a) -> FieldAssignment' a -> a)
    -> (forall a. (a -> a -> a) -> FieldAssignment' a -> a)
    -> (forall a. FieldAssignment' a -> [a])
    -> (forall a. FieldAssignment' a -> Bool)
    -> (forall a. FieldAssignment' a -> Int)
    -> (forall a. Eq a => a -> FieldAssignment' a -> Bool)
    -> (forall a. Ord a => FieldAssignment' a -> a)
    -> (forall a. Ord a => FieldAssignment' a -> a)
    -> (forall a. Num a => FieldAssignment' a -> a)
    -> (forall a. Num a => FieldAssignment' a -> a)
    -> Foldable FieldAssignment'
    forall a. Eq a => a -> FieldAssignment' a -> Bool
    forall a. Num a => FieldAssignment' a -> a
    forall a. Ord a => FieldAssignment' a -> a
    forall m. Monoid m => FieldAssignment' m -> m
    forall a. FieldAssignment' a -> Bool
    forall a. FieldAssignment' a -> Int
    forall a. FieldAssignment' a -> [a]
    forall a. (a -> a -> a) -> FieldAssignment' a -> a
    forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
    forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
    forall a b. (a -> b -> b) -> b -> FieldAssignment' 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 => FieldAssignment' m -> m
    fold :: forall m. Monoid m => FieldAssignment' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
    foldr1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
    foldl1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
    $ctoList :: forall a. FieldAssignment' a -> [a]
    toList :: forall a. FieldAssignment' a -> [a]
    $cnull :: forall a. FieldAssignment' a -> Bool
    null :: forall a. FieldAssignment' a -> Bool
    $clength :: forall a. FieldAssignment' a -> Int
    length :: forall a. FieldAssignment' a -> Int
    $celem :: forall a. Eq a => a -> FieldAssignment' a -> Bool
    elem :: forall a. Eq a => a -> FieldAssignment' a -> Bool
    $cmaximum :: forall a. Ord a => FieldAssignment' a -> a
    maximum :: forall a. Ord a => FieldAssignment' a -> a
    $cminimum :: forall a. Ord a => FieldAssignment' a -> a
    minimum :: forall a. Ord a => FieldAssignment' a -> a
    $csum :: forall a. Num a => FieldAssignment' a -> a
    sum :: forall a. Num a => FieldAssignment' a -> a
    $cproduct :: forall a. Num a => FieldAssignment' a -> a
    product :: forall a. Num a => FieldAssignment' a -> a
    Foldable, Functor FieldAssignment'
    Foldable FieldAssignment'
    (Functor FieldAssignment', Foldable FieldAssignment') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        FieldAssignment' (f a) -> f (FieldAssignment' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        FieldAssignment' (m a) -> m (FieldAssignment' a))
    -> Traversable FieldAssignment'
    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 =>
    FieldAssignment' (m a) -> m (FieldAssignment' a)
    forall (f :: * -> *) a.
    Applicative f =>
    FieldAssignment' (f a) -> f (FieldAssignment' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FieldAssignment' (f a) -> f (FieldAssignment' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FieldAssignment' (f a) -> f (FieldAssignment' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    FieldAssignment' (m a) -> m (FieldAssignment' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    FieldAssignment' (m a) -> m (FieldAssignment' a)
    Traversable, Int -> FieldAssignment' a -> ShowS
    [FieldAssignment' a] -> ShowS
    FieldAssignment' a -> String
    (Int -> FieldAssignment' a -> ShowS)
    -> (FieldAssignment' a -> String)
    -> ([FieldAssignment' a] -> ShowS)
    -> Show (FieldAssignment' a)
    forall a. Show a => Int -> FieldAssignment' a -> ShowS
    forall a. Show a => [FieldAssignment' a] -> ShowS
    forall a. Show a => FieldAssignment' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> FieldAssignment' a -> ShowS
    showsPrec :: Int -> FieldAssignment' a -> ShowS
    $cshow :: forall a. Show a => FieldAssignment' a -> String
    show :: FieldAssignment' a -> String
    $cshowList :: forall a. Show a => [FieldAssignment' a] -> ShowS
    showList :: [FieldAssignment' a] -> ShowS
    Show, FieldAssignment' a -> FieldAssignment' a -> Bool
    (FieldAssignment' a -> FieldAssignment' a -> Bool)
    -> (FieldAssignment' a -> FieldAssignment' a -> Bool)
    -> Eq (FieldAssignment' a)
    forall a. Eq a => FieldAssignment' a -> FieldAssignment' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => FieldAssignment' a -> FieldAssignment' a -> Bool
    == :: FieldAssignment' a -> FieldAssignment' a -> Bool
    $c/= :: forall a. Eq a => FieldAssignment' a -> FieldAssignment' a -> Bool
    /= :: FieldAssignment' a -> FieldAssignment' a -> Bool
    Eq)

    type FieldAssignment = FieldAssignment' Expr

    data ModuleAssignment  = ModuleAssignment
                               { ModuleAssignment -> QName
    _qnameModA     :: QName
                               , ModuleAssignment -> [Expr]
    _exprModA      :: [Expr]
                               , ModuleAssignment -> ImportDirective
    _importDirModA :: ImportDirective
                               }
      deriving ModuleAssignment -> ModuleAssignment -> Bool
    (ModuleAssignment -> ModuleAssignment -> Bool)
    -> (ModuleAssignment -> ModuleAssignment -> Bool)
    -> Eq ModuleAssignment
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ModuleAssignment -> ModuleAssignment -> Bool
    == :: ModuleAssignment -> ModuleAssignment -> Bool
    $c/= :: ModuleAssignment -> ModuleAssignment -> Bool
    /= :: ModuleAssignment -> ModuleAssignment -> Bool
    Eq

    type RecordAssignment  = Either FieldAssignment ModuleAssignment
    type RecordAssignments = [RecordAssignment]

    nameFieldA :: Lens' (FieldAssignment' a) Name
    nameFieldA :: forall a (f :: * -> *).
    Functor f =>
    (Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a)
    nameFieldA Name -> f Name
    f FieldAssignment' a
    r = Name -> f Name
    f (FieldAssignment' a -> Name
    forall a. FieldAssignment' a -> Name
    _nameFieldA FieldAssignment' a
    r) f Name -> (Name -> FieldAssignment' a) -> f (FieldAssignment' a)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \Name
    x -> FieldAssignment' a
    r { _nameFieldA = x }

    exprFieldA :: Lens' (FieldAssignment' a) a
    exprFieldA :: forall a (f :: * -> *).
    Functor f =>
    (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a)
    exprFieldA a -> f a
    f FieldAssignment' a
    r = a -> f a
    f (FieldAssignment' a -> a
    forall a. FieldAssignment' a -> a
    _exprFieldA FieldAssignment' a
    r) f a -> (a -> FieldAssignment' a) -> f (FieldAssignment' a)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \a
    x -> FieldAssignment' a
    r { _exprFieldA = x }

    -- UNUSED Liang-Ting Chen 2019-07-16
    --qnameModA :: Lens' ModuleAssignment QName
    --qnameModA f r = f (_qnameModA r) <&> \x -> r { _qnameModA = x }
    --
    --exprModA :: Lens' [Expr] ModuleAssignment
    --exprModA f r = f (_exprModA r) <&> \x -> r { _exprModA = x }
    --
    --importDirModA :: Lens' ModuleAssignment ImportDirective
    --importDirModA f r = f (_importDirModA r) <&> \x -> r { _importDirModA = x }

    -- | Concrete expressions. Should represent exactly what the user wrote.
    data Expr
      = Ident QName                                -- ^ ex: @x@
      | Lit Range Literal                          -- ^ ex: @1@ or @\"foo\"@
      | QuestionMark Range (Maybe Nat)             -- ^ ex: @?@ or @{! ... !}@
      | Underscore Range (Maybe String)            -- ^ ex: @_@ or @_A_5@
      | RawApp Range (List2 Expr)                  -- ^ before parsing operators
      | App Range Expr (NamedArg Expr)             -- ^ ex: @e e@, @e {e}@, or @e {x = e}@
      | OpApp Range QName (Set1 A.Name) OpAppArgs  -- ^ ex: @e + e@
                                                   -- The 'QName' is possibly ambiguous,
                                                   -- but it must correspond to one of the names in the set.
      | WithApp Range Expr (List1 Expr)            -- ^ ex: @e | e1 | .. | en@
      | HiddenArg Range (Named_ Expr)              -- ^ ex: @{e}@ or @{x=e}@
      | InstanceArg Range (Named_ Expr)            -- ^ ex: @{{e}}@ or @{{x=e}}@
      | Lam Range (List1 LamBinding) Expr          -- ^ ex: @\\x {y} -> e@ or @\\(x:A){y:B} -> e@
      | AbsurdLam Range Hiding                     -- ^ ex: @\\ ()@
      | ExtendedLam Range Erased
          (List1 LamClause)                        -- ^ ex: @\\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }@
      | Fun Range (Arg Expr) Expr                  -- ^ ex: @e -> e@ or @.e -> e@ (NYI: @{e} -> e@)
      | Pi Telescope1 Expr                         -- ^ ex: @(xs:e) -> e@ or @{xs:e} -> e@
      | Rec KwRange Range RecordAssignments        -- ^ ex: @record {x = a; y = b}@, or @record { x = a; M1; M2 }@
                                                   --   The 'KwRange' is for the @record@ keyword.
      | RecUpdate KwRange Range Expr [FieldAssignment]
                                                   -- ^ ex: @record e {x = a; y = b}@
                                                   --   The 'KwRange' is for the @record@ keyword.
      | Let Range (List1 Declaration) (Maybe Expr) -- ^ ex: @let Ds in e@, missing body when parsing do-notation let
      | Paren Range Expr                           -- ^ ex: @(e)@
      | IdiomBrackets Range [Expr]                 -- ^ ex: @(| e1 | e2 | .. | en |)@ or @(|)@
      | DoBlock Range (List1 DoStmt)               -- ^ ex: @do x <- m1; m2@
      | Absurd Range                               -- ^ ex: @()@ or @{}@, only in patterns
      | As Range Name Expr                         -- ^ ex: @x\@p@, only in patterns
      | Dot KwRange Expr                           -- ^ ex: @.p@, only in patterns
      | DoubleDot KwRange Expr                     -- ^ ex: @..A@, used for parsing @..A -> B@
      | Quote Range                                -- ^ ex: @quote@, should be applied to a name
      | QuoteTerm Range                            -- ^ ex: @quoteTerm@, should be applied to a term
      | Tactic Range Expr                          -- ^ ex: @\@(tactic t)@, used to declare tactic arguments
      | Unquote Range                              -- ^ ex: @unquote@, should be applied to a term of type @Term@
      | DontCare Expr                              -- ^ to print irrelevant things
      | Equal Range Expr Expr                      -- ^ ex: @a = b@, used internally in the parser
      | Ellipsis Range                             -- ^ @...@, used internally to parse patterns.
      | KnownIdent NameKind QName
        -- ^ An identifier coming from abstract syntax, for which we know a
        -- precise syntactic highlighting class (used in printing).
      | KnownOpApp NameKind Range QName (Set1 A.Name) OpAppArgs
        -- ^ An operator application coming from abstract syntax, for which
        -- we know a precise syntactic highlighting class (used in
        -- printing).
      | Generalized Expr
      deriving Expr -> Expr -> Bool
    (Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Expr -> Expr -> Bool
    == :: Expr -> Expr -> Bool
    $c/= :: Expr -> Expr -> Bool
    /= :: Expr -> Expr -> Bool
    Eq

    type OpAppArgs = OpAppArgs' Expr
    type OpAppArgs' e = List1 (NamedArg (MaybePlaceholder (OpApp e)))
    type OpAppArgs0 e = [NamedArg (MaybePlaceholder (OpApp e))]

    -- | Concrete patterns. No literals in patterns at the moment.
    data Pattern
      = IdentP Bool QName                      -- ^ @c@ or @x@
                                               --
                                               -- If the boolean is
                                               -- 'False', then the
                                               -- 'QName' must not refer
                                               -- to a constructor or a
                                               -- pattern synonym. The
                                               -- value 'False' is used
                                               -- when a hidden argument
                                               -- pun is expanded.
      | QuoteP Range                           -- ^ @quote@
      | AppP Pattern (NamedArg Pattern)        -- ^ @p p'@ or @p {x = p'}@
      | RawAppP Range (List2 Pattern)          -- ^ @p1..pn@ before parsing operators
      | OpAppP Range QName (Set1 A.Name)
          (List1 (NamedArg Pattern))           -- ^ eg: @p => p'@ for operator @_=>_@
                                               -- The 'QName' is possibly
                                               -- ambiguous, but it must
                                               -- correspond to one of
                                               -- the names in the set.
      | HiddenP Range (Named_ Pattern)         -- ^ @{p}@ or @{x = p}@
      | InstanceP Range (Named_ Pattern)       -- ^ @{{p}}@ or @{{x = p}}@
      | ParenP Range Pattern                   -- ^ @(p)@
      | WildP Range                            -- ^ @_@
      | AbsurdP Range                          -- ^ @()@
      | AsP Range Name Pattern                 -- ^ @x\@p@
      | DotP KwRange Range Expr                -- ^ @.e@, the 'KwRange' is for the dot,
                                               --   the 'Range' for the whole thing (including the dot).
      | LitP Range Literal                     -- ^ @0@, @1@, etc.
      | RecP KwRange Range [FieldAssignment' Pattern]
          -- ^ @record {x = p; y = q}@.  The 'KwRange' is for the @record@ keyword.
      | EqualP Range (List1 (Expr,Expr))       -- ^ @i = i1@ i.e. cubical face lattice generator
      | EllipsisP Range (Maybe Pattern)        -- ^ @...@, only as left-most pattern.
                                               --   Second arg is @Nothing@ before expansion, and
                                               --   @Just p@ after expanding ellipsis to @p@.
      | WithP Range Pattern                    -- ^ @| p@, for with-patterns.
      deriving Pattern -> Pattern -> Bool
    (Pattern -> Pattern -> Bool)
    -> (Pattern -> Pattern -> Bool) -> Eq Pattern
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Pattern -> Pattern -> Bool
    == :: Pattern -> Pattern -> Bool
    $c/= :: Pattern -> Pattern -> Bool
    /= :: Pattern -> Pattern -> Bool
    Eq

    data DoStmt
      = DoBind Range Pattern Expr [LamClause]   -- ^ @p ← e where cs@
      | DoThen Expr
      | DoLet Range (List1 Declaration)
      deriving DoStmt -> DoStmt -> Bool
    (DoStmt -> DoStmt -> Bool)
    -> (DoStmt -> DoStmt -> Bool) -> Eq DoStmt
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DoStmt -> DoStmt -> Bool
    == :: DoStmt -> DoStmt -> Bool
    $c/= :: DoStmt -> DoStmt -> Bool
    /= :: DoStmt -> DoStmt -> Bool
    Eq

    -- | 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 (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)

    type Binder = Binder' BoundName

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

    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

    -- | A lambda binding is either domain free or typed.

    type LamBinding = LamBinding' TypedBinding
    data LamBinding' a
      = DomainFree (NamedArg Binder)
        -- ^ . @x@ or @{x}@ or @.x@ or @.{x}@ or @{.x}@ or @x\@p@ or @(p)@
      | DomainFull a
        -- ^ . @(xs : e)@ or @{xs : e}@
      deriving ((forall a b. (a -> b) -> LamBinding' a -> LamBinding' b)
    -> (forall a b. a -> LamBinding' b -> LamBinding' a)
    -> Functor LamBinding'
    forall a b. a -> LamBinding' b -> LamBinding' a
    forall a b. (a -> b) -> LamBinding' a -> LamBinding' 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) -> LamBinding' a -> LamBinding' b
    fmap :: forall a b. (a -> b) -> LamBinding' a -> LamBinding' b
    $c<$ :: forall a b. a -> LamBinding' b -> LamBinding' a
    <$ :: forall a b. a -> LamBinding' b -> LamBinding' a
    Functor, (forall m. Monoid m => LamBinding' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> LamBinding' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> LamBinding' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> LamBinding' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> LamBinding' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> LamBinding' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> LamBinding' a -> b)
    -> (forall a. (a -> a -> a) -> LamBinding' a -> a)
    -> (forall a. (a -> a -> a) -> LamBinding' a -> a)
    -> (forall a. LamBinding' a -> [a])
    -> (forall a. LamBinding' a -> Bool)
    -> (forall a. LamBinding' a -> Int)
    -> (forall a. Eq a => a -> LamBinding' a -> Bool)
    -> (forall a. Ord a => LamBinding' a -> a)
    -> (forall a. Ord a => LamBinding' a -> a)
    -> (forall a. Num a => LamBinding' a -> a)
    -> (forall a. Num a => LamBinding' a -> a)
    -> Foldable LamBinding'
    forall a. Eq a => a -> LamBinding' a -> Bool
    forall a. Num a => LamBinding' a -> a
    forall a. Ord a => LamBinding' a -> a
    forall m. Monoid m => LamBinding' m -> m
    forall a. LamBinding' a -> Bool
    forall a. LamBinding' a -> Int
    forall a. LamBinding' a -> [a]
    forall a. (a -> a -> a) -> LamBinding' a -> a
    forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
    forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
    forall a b. (a -> b -> b) -> b -> LamBinding' 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 => LamBinding' m -> m
    fold :: forall m. Monoid m => LamBinding' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
    foldr1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
    foldl1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
    $ctoList :: forall a. LamBinding' a -> [a]
    toList :: forall a. LamBinding' a -> [a]
    $cnull :: forall a. LamBinding' a -> Bool
    null :: forall a. LamBinding' a -> Bool
    $clength :: forall a. LamBinding' a -> Int
    length :: forall a. LamBinding' a -> Int
    $celem :: forall a. Eq a => a -> LamBinding' a -> Bool
    elem :: forall a. Eq a => a -> LamBinding' a -> Bool
    $cmaximum :: forall a. Ord a => LamBinding' a -> a
    maximum :: forall a. Ord a => LamBinding' a -> a
    $cminimum :: forall a. Ord a => LamBinding' a -> a
    minimum :: forall a. Ord a => LamBinding' a -> a
    $csum :: forall a. Num a => LamBinding' a -> a
    sum :: forall a. Num a => LamBinding' a -> a
    $cproduct :: forall a. Num a => LamBinding' a -> a
    product :: forall a. Num a => LamBinding' a -> a
    Foldable, Functor LamBinding'
    Foldable LamBinding'
    (Functor LamBinding', Foldable LamBinding') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> LamBinding' a -> f (LamBinding' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        LamBinding' (f a) -> f (LamBinding' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> LamBinding' a -> m (LamBinding' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        LamBinding' (m a) -> m (LamBinding' a))
    -> Traversable LamBinding'
    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 =>
    LamBinding' (m a) -> m (LamBinding' a)
    forall (f :: * -> *) a.
    Applicative f =>
    LamBinding' (f a) -> f (LamBinding' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LamBinding' a -> m (LamBinding' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LamBinding' a -> f (LamBinding' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LamBinding' a -> f (LamBinding' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LamBinding' a -> f (LamBinding' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    LamBinding' (f a) -> f (LamBinding' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    LamBinding' (f a) -> f (LamBinding' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LamBinding' a -> m (LamBinding' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LamBinding' a -> m (LamBinding' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    LamBinding' (m a) -> m (LamBinding' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    LamBinding' (m a) -> m (LamBinding' a)
    Traversable, LamBinding' a -> LamBinding' a -> Bool
    (LamBinding' a -> LamBinding' a -> Bool)
    -> (LamBinding' a -> LamBinding' a -> Bool) -> Eq (LamBinding' a)
    forall a. Eq a => LamBinding' a -> LamBinding' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => LamBinding' a -> LamBinding' a -> Bool
    == :: LamBinding' a -> LamBinding' a -> Bool
    $c/= :: forall a. Eq a => LamBinding' a -> LamBinding' a -> Bool
    /= :: LamBinding' a -> LamBinding' a -> Bool
    Eq)

    -- | Drop type annotations and lets from bindings.
    dropTypeAndModality :: LamBinding -> [LamBinding]
    dropTypeAndModality :: LamBinding -> [LamBinding]
    dropTypeAndModality (DomainFull (TBind Range
    _ List1 (NamedArg Binder)
    xs Expr
    _)) =
      (NamedArg Binder -> LamBinding)
    -> [NamedArg Binder] -> [LamBinding]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedArg Binder -> LamBinding
    forall a. NamedArg Binder -> LamBinding' a
    DomainFree (NamedArg Binder -> LamBinding)
    -> (NamedArg Binder -> NamedArg Binder)
    -> NamedArg Binder
    -> LamBinding
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Modality -> NamedArg Binder -> NamedArg Binder
    forall a. LensModality a => Modality -> a -> a
    setModality Modality
    defaultModality) ([NamedArg Binder] -> [LamBinding])
    -> [NamedArg Binder] -> [LamBinding]
    forall a b. (a -> b) -> a -> b
    $ List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (NamedArg Binder)
    xs
    dropTypeAndModality (DomainFull TLet{}) = []
    dropTypeAndModality (DomainFree NamedArg Binder
    x) = [NamedArg Binder -> LamBinding
    forall a. NamedArg Binder -> LamBinding' a
    DomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ Modality -> NamedArg Binder -> NamedArg Binder
    forall a. LensModality a => Modality -> a -> a
    setModality Modality
    defaultModality NamedArg Binder
    x]

    data BoundName = BName
      { BoundName -> Name
    boundName       :: Name
      , BoundName -> Fixity'
    bnameFixity     :: Fixity'
      , BoundName -> TacticAttribute
    bnameTactic     :: TacticAttribute
          -- ^ From @\@tactic@ attribute.
      , BoundName -> Bool
    bnameIsFinite   :: Bool
          -- ^ The @\@finite@ cannot be parsed, it comes from the builtin @Partial@ only.
      }
      deriving BoundName -> BoundName -> Bool
    (BoundName -> BoundName -> Bool)
    -> (BoundName -> BoundName -> Bool) -> Eq BoundName
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: BoundName -> BoundName -> Bool
    == :: BoundName -> BoundName -> Bool
    $c/= :: BoundName -> BoundName -> Bool
    /= :: BoundName -> BoundName -> Bool
    Eq

    newtype TacticAttribute' a = TacticAttribute { forall a. TacticAttribute' a -> Maybe (Ranged a)
    theTacticAttribute :: Maybe (Ranged a) }
      deriving (TacticAttribute' a -> TacticAttribute' a -> Bool
    (TacticAttribute' a -> TacticAttribute' a -> Bool)
    -> (TacticAttribute' a -> TacticAttribute' a -> Bool)
    -> Eq (TacticAttribute' a)
    forall a. Eq a => TacticAttribute' a -> TacticAttribute' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => TacticAttribute' a -> TacticAttribute' a -> Bool
    == :: TacticAttribute' a -> TacticAttribute' a -> Bool
    $c/= :: forall a. Eq a => TacticAttribute' a -> TacticAttribute' a -> Bool
    /= :: TacticAttribute' a -> TacticAttribute' a -> Bool
    Eq, Int -> TacticAttribute' a -> ShowS
    [TacticAttribute' a] -> ShowS
    TacticAttribute' a -> String
    (Int -> TacticAttribute' a -> ShowS)
    -> (TacticAttribute' a -> String)
    -> ([TacticAttribute' a] -> ShowS)
    -> Show (TacticAttribute' a)
    forall a. Show a => Int -> TacticAttribute' a -> ShowS
    forall a. Show a => [TacticAttribute' a] -> ShowS
    forall a. Show a => TacticAttribute' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> TacticAttribute' a -> ShowS
    showsPrec :: Int -> TacticAttribute' a -> ShowS
    $cshow :: forall a. Show a => TacticAttribute' a -> String
    show :: TacticAttribute' a -> String
    $cshowList :: forall a. Show a => [TacticAttribute' a] -> ShowS
    showList :: [TacticAttribute' a] -> ShowS
    Show, TacticAttribute' a -> ()
    (TacticAttribute' a -> ()) -> NFData (TacticAttribute' a)
    forall a. NFData a => TacticAttribute' a -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall a. NFData a => TacticAttribute' a -> ()
    rnf :: TacticAttribute' a -> ()
    NFData, (forall a b. (a -> b) -> TacticAttribute' a -> TacticAttribute' b)
    -> (forall a b. a -> TacticAttribute' b -> TacticAttribute' a)
    -> Functor TacticAttribute'
    forall a b. a -> TacticAttribute' b -> TacticAttribute' a
    forall a b. (a -> b) -> TacticAttribute' a -> TacticAttribute' 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) -> TacticAttribute' a -> TacticAttribute' b
    fmap :: forall a b. (a -> b) -> TacticAttribute' a -> TacticAttribute' b
    $c<$ :: forall a b. a -> TacticAttribute' b -> TacticAttribute' a
    <$ :: forall a b. a -> TacticAttribute' b -> TacticAttribute' a
    Functor, (forall m. Monoid m => TacticAttribute' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b)
    -> (forall a. (a -> a -> a) -> TacticAttribute' a -> a)
    -> (forall a. (a -> a -> a) -> TacticAttribute' a -> a)
    -> (forall a. TacticAttribute' a -> [a])
    -> (forall a. TacticAttribute' a -> Bool)
    -> (forall a. TacticAttribute' a -> Int)
    -> (forall a. Eq a => a -> TacticAttribute' a -> Bool)
    -> (forall a. Ord a => TacticAttribute' a -> a)
    -> (forall a. Ord a => TacticAttribute' a -> a)
    -> (forall a. Num a => TacticAttribute' a -> a)
    -> (forall a. Num a => TacticAttribute' a -> a)
    -> Foldable TacticAttribute'
    forall a. Eq a => a -> TacticAttribute' a -> Bool
    forall a. Num a => TacticAttribute' a -> a
    forall a. Ord a => TacticAttribute' a -> a
    forall m. Monoid m => TacticAttribute' m -> m
    forall a. TacticAttribute' a -> Bool
    forall a. TacticAttribute' a -> Int
    forall a. TacticAttribute' a -> [a]
    forall a. (a -> a -> a) -> TacticAttribute' a -> a
    forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
    forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
    forall a b. (a -> b -> b) -> b -> TacticAttribute' 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 => TacticAttribute' m -> m
    fold :: forall m. Monoid m => TacticAttribute' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
    foldr1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
    foldl1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
    $ctoList :: forall a. TacticAttribute' a -> [a]
    toList :: forall a. TacticAttribute' a -> [a]
    $cnull :: forall a. TacticAttribute' a -> Bool
    null :: forall a. TacticAttribute' a -> Bool
    $clength :: forall a. TacticAttribute' a -> Int
    length :: forall a. TacticAttribute' a -> Int
    $celem :: forall a. Eq a => a -> TacticAttribute' a -> Bool
    elem :: forall a. Eq a => a -> TacticAttribute' a -> Bool
    $cmaximum :: forall a. Ord a => TacticAttribute' a -> a
    maximum :: forall a. Ord a => TacticAttribute' a -> a
    $cminimum :: forall a. Ord a => TacticAttribute' a -> a
    minimum :: forall a. Ord a => TacticAttribute' a -> a
    $csum :: forall a. Num a => TacticAttribute' a -> a
    sum :: forall a. Num a => TacticAttribute' a -> a
    $cproduct :: forall a. Num a => TacticAttribute' a -> a
    product :: forall a. Num a => TacticAttribute' a -> a
    Foldable, Functor TacticAttribute'
    Foldable TacticAttribute'
    (Functor TacticAttribute', Foldable TacticAttribute') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        TacticAttribute' (f a) -> f (TacticAttribute' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        TacticAttribute' (m a) -> m (TacticAttribute' a))
    -> Traversable TacticAttribute'
    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 =>
    TacticAttribute' (m a) -> m (TacticAttribute' a)
    forall (f :: * -> *) a.
    Applicative f =>
    TacticAttribute' (f a) -> f (TacticAttribute' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    TacticAttribute' (f a) -> f (TacticAttribute' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    TacticAttribute' (f a) -> f (TacticAttribute' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    TacticAttribute' (m a) -> m (TacticAttribute' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    TacticAttribute' (m a) -> m (TacticAttribute' a)
    Traversable, KillRangeT (TacticAttribute' a)
    KillRangeT (TacticAttribute' a) -> KillRange (TacticAttribute' a)
    forall a. KillRangeT (TacticAttribute' a)
    forall a. KillRangeT a -> KillRange a
    $ckillRange :: forall a. KillRangeT (TacticAttribute' a)
    killRange :: KillRangeT (TacticAttribute' a)
    KillRange)
    type TacticAttribute = TacticAttribute' Expr

    instance Null (TacticAttribute' a) where
      null :: TacticAttribute' a -> Bool
    null = Maybe (Ranged a) -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe (Ranged a) -> Bool)
    -> (TacticAttribute' a -> Maybe (Ranged a))
    -> TacticAttribute' a
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TacticAttribute' a -> Maybe (Ranged a)
    forall a. TacticAttribute' a -> Maybe (Ranged a)
    theTacticAttribute
      empty :: TacticAttribute' a
    empty = Maybe (Ranged a) -> TacticAttribute' a
    forall a. Maybe (Ranged a) -> TacticAttribute' a
    TacticAttribute Maybe (Ranged a)
    forall a. Maybe a
    Nothing

    mkBoundName_ :: Name -> BoundName
    mkBoundName_ :: Name -> BoundName
    mkBoundName_ Name
    x = Name -> Fixity' -> BoundName
    mkBoundName Name
    x Fixity'
    noFixity'

    mkBoundName :: Name -> Fixity' -> BoundName
    mkBoundName :: Name -> Fixity' -> BoundName
    mkBoundName Name
    x Fixity'
    f = Name -> Fixity' -> TacticAttribute -> Bool -> BoundName
    BName Name
    x Fixity'
    f TacticAttribute
    forall a. Null a => a
    empty Bool
    False

    -- | A typed binding.

    type TypedBinding = TypedBinding' Expr

    data TypedBinding' e
      = TBind Range (List1 (NamedArg Binder)) e
        -- ^ Binding @(x1\@p1 ... xn\@pn : A)@.
      | TLet  Range (List1 Declaration)
        -- ^ Let binding @(let Ds)@ or @(open M args)@.
      deriving ((forall a b. (a -> b) -> TypedBinding' a -> TypedBinding' b)
    -> (forall a b. a -> TypedBinding' b -> TypedBinding' a)
    -> Functor TypedBinding'
    forall a b. a -> TypedBinding' b -> TypedBinding' a
    forall a b. (a -> b) -> TypedBinding' a -> TypedBinding' 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) -> TypedBinding' a -> TypedBinding' b
    fmap :: forall a b. (a -> b) -> TypedBinding' a -> TypedBinding' b
    $c<$ :: forall a b. a -> TypedBinding' b -> TypedBinding' a
    <$ :: forall a b. a -> TypedBinding' b -> TypedBinding' a
    Functor, (forall m. Monoid m => TypedBinding' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b)
    -> (forall a. (a -> a -> a) -> TypedBinding' a -> a)
    -> (forall a. (a -> a -> a) -> TypedBinding' a -> a)
    -> (forall a. TypedBinding' a -> [a])
    -> (forall a. TypedBinding' a -> Bool)
    -> (forall a. TypedBinding' a -> Int)
    -> (forall a. Eq a => a -> TypedBinding' a -> Bool)
    -> (forall a. Ord a => TypedBinding' a -> a)
    -> (forall a. Ord a => TypedBinding' a -> a)
    -> (forall a. Num a => TypedBinding' a -> a)
    -> (forall a. Num a => TypedBinding' a -> a)
    -> Foldable TypedBinding'
    forall a. Eq a => a -> TypedBinding' a -> Bool
    forall a. Num a => TypedBinding' a -> a
    forall a. Ord a => TypedBinding' a -> a
    forall m. Monoid m => TypedBinding' m -> m
    forall a. TypedBinding' a -> Bool
    forall a. TypedBinding' a -> Int
    forall a. TypedBinding' a -> [a]
    forall a. (a -> a -> a) -> TypedBinding' a -> a
    forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
    forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
    forall a b. (a -> b -> b) -> b -> TypedBinding' 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 => TypedBinding' m -> m
    fold :: forall m. Monoid m => TypedBinding' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
    foldr1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
    foldl1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
    $ctoList :: forall a. TypedBinding' a -> [a]
    toList :: forall a. TypedBinding' a -> [a]
    $cnull :: forall a. TypedBinding' a -> Bool
    null :: forall a. TypedBinding' a -> Bool
    $clength :: forall a. TypedBinding' a -> Int
    length :: forall a. TypedBinding' a -> Int
    $celem :: forall a. Eq a => a -> TypedBinding' a -> Bool
    elem :: forall a. Eq a => a -> TypedBinding' a -> Bool
    $cmaximum :: forall a. Ord a => TypedBinding' a -> a
    maximum :: forall a. Ord a => TypedBinding' a -> a
    $cminimum :: forall a. Ord a => TypedBinding' a -> a
    minimum :: forall a. Ord a => TypedBinding' a -> a
    $csum :: forall a. Num a => TypedBinding' a -> a
    sum :: forall a. Num a => TypedBinding' a -> a
    $cproduct :: forall a. Num a => TypedBinding' a -> a
    product :: forall a. Num a => TypedBinding' a -> a
    Foldable, Functor TypedBinding'
    Foldable TypedBinding'
    (Functor TypedBinding', Foldable TypedBinding') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> TypedBinding' a -> f (TypedBinding' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        TypedBinding' (f a) -> f (TypedBinding' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> TypedBinding' a -> m (TypedBinding' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        TypedBinding' (m a) -> m (TypedBinding' a))
    -> Traversable TypedBinding'
    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 =>
    TypedBinding' (m a) -> m (TypedBinding' a)
    forall (f :: * -> *) a.
    Applicative f =>
    TypedBinding' (f a) -> f (TypedBinding' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypedBinding' a -> m (TypedBinding' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TypedBinding' a -> f (TypedBinding' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TypedBinding' a -> f (TypedBinding' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TypedBinding' a -> f (TypedBinding' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    TypedBinding' (f a) -> f (TypedBinding' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    TypedBinding' (f a) -> f (TypedBinding' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypedBinding' a -> m (TypedBinding' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypedBinding' a -> m (TypedBinding' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    TypedBinding' (m a) -> m (TypedBinding' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    TypedBinding' (m a) -> m (TypedBinding' a)
    Traversable, TypedBinding' e -> TypedBinding' e -> Bool
    (TypedBinding' e -> TypedBinding' e -> Bool)
    -> (TypedBinding' e -> TypedBinding' e -> Bool)
    -> Eq (TypedBinding' e)
    forall e. Eq e => TypedBinding' e -> TypedBinding' e -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall e. Eq e => TypedBinding' e -> TypedBinding' e -> Bool
    == :: TypedBinding' e -> TypedBinding' e -> Bool
    $c/= :: forall e. Eq e => TypedBinding' e -> TypedBinding' e -> Bool
    /= :: TypedBinding' e -> TypedBinding' e -> Bool
    Eq)

    -- | A telescope is a sequence of typed bindings. Bound variables are in scope
    --   in later types.
    type Telescope1 = List1 TypedBinding
    type Telescope  = [TypedBinding]

    -- | We can try to get a @Telescope@ from a @[LamBinding]@.
    --   If we have a type annotation already, we're happy.
    --   Otherwise we manufacture a binder with an underscore for the type.
    lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
    lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
    lamBindingsToTelescope Range
    r = (LamBinding -> TypedBinding' Expr) -> [LamBinding] -> Telescope
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LamBinding -> TypedBinding' Expr) -> [LamBinding] -> Telescope)
    -> (LamBinding -> TypedBinding' Expr) -> [LamBinding] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ \case
      DomainFull TypedBinding' Expr
    ty -> TypedBinding' Expr
    ty
      DomainFree NamedArg Binder
    nm -> Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    r (NamedArg Binder -> List1 (NamedArg Binder)
    forall a. a -> NonEmpty a
    List1.singleton NamedArg Binder
    nm) (Expr -> TypedBinding' Expr) -> Expr -> TypedBinding' Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe String -> Expr
    Underscore Range
    r Maybe String
    forall a. Maybe a
    Nothing

    -- | Smart constructor for @Pi@: check whether the @Telescope@ is empty

    makePi :: Telescope -> Expr -> Expr
    makePi :: Telescope -> Expr -> Expr
    makePi []     = Expr -> Expr
    forall a. a -> a
    id
    makePi (TypedBinding' Expr
    b:Telescope
    bs) = Telescope1 -> Expr -> Expr
    Pi (TypedBinding' Expr
    b TypedBinding' Expr -> Telescope -> Telescope1
    forall a. a -> [a] -> NonEmpty a
    :| Telescope
    bs)

    -- | Smart constructor for @Lam@: check for non-zero bindings.

    mkLam :: Range -> [LamBinding] -> Expr -> Expr
    mkLam :: Range -> [LamBinding] -> Expr -> Expr
    mkLam Range
    r []     Expr
    e = Expr
    e
    mkLam Range
    r (LamBinding
    x:[LamBinding]
    xs) Expr
    e = Range -> List1 LamBinding -> Expr -> Expr
    Lam Range
    r (LamBinding
    x LamBinding -> [LamBinding] -> List1 LamBinding
    forall a. a -> [a] -> NonEmpty a
    :| [LamBinding]
    xs) Expr
    e

    -- | Smart constructor for @Let@: check for non-zero let bindings.

    mkLet :: Range -> [Declaration] -> Expr -> Expr
    mkLet :: Range -> [Declaration] -> Expr -> Expr
    mkLet Range
    r []     Expr
    e = Expr
    e
    mkLet Range
    r (Declaration
    d:[Declaration]
    ds) Expr
    e = Range -> List1 Declaration -> Maybe Expr -> Expr
    Let Range
    r (Declaration
    d Declaration -> [Declaration] -> List1 Declaration
    forall a. a -> [a] -> NonEmpty a
    :| [Declaration]
    ds) (Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    e)

    -- | Smart constructor for @TLet@: check for non-zero let bindings.

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

    {-| Left hand sides can be written in infix style. For example:

        > n + suc m = suc (n + m)
        > (f ∘ g) x = f (g x)

       We use fixity information to see which name is actually defined.
    -}
    data LHS = LHS  -- ^ Original pattern (including with-patterns), rewrite equations and with-expressions.
      { LHS -> Pattern
    lhsOriginalPattern :: Pattern
        -- ^ e.g. @f ps | wps@
      , LHS -> [RewriteEqn]
    lhsRewriteEqn      :: [RewriteEqn]
        -- ^ @(rewrite e | with p <- e in eq)@ (many)
      , LHS -> [WithExpr]
    lhsWithExpr        :: [WithExpr]
        -- ^ @with e1 in eq | {e2} | ...@ (many)
      }
      deriving LHS -> LHS -> Bool
    (LHS -> LHS -> Bool) -> (LHS -> LHS -> Bool) -> Eq LHS
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LHS -> LHS -> Bool
    == :: LHS -> LHS -> Bool
    $c/= :: LHS -> LHS -> Bool
    /= :: LHS -> LHS -> Bool
    Eq

    type RewriteEqn = RewriteEqn' () Name Pattern Expr
    type WithExpr   = Named Name (Arg Expr)

    -- | Processed (operator-parsed) intermediate form of the core @f ps@ of 'LHS'.
    --   Corresponds to 'lhsOriginalPattern'.
    data LHSCore
      = LHSHead  { LHSCore -> QName
    lhsDefName      :: QName               -- ^ @f@
                 , LHSCore -> [NamedArg Pattern]
    lhsPats         :: [NamedArg Pattern]  -- ^ @ps@
                 }
      | LHSProj  { LHSCore -> QName
    lhsDestructor   :: QName               -- ^ Record projection.
                 , LHSCore -> [NamedArg Pattern]
    lhsPatsLeft     :: [NamedArg Pattern]  -- ^ Patterns for record indices (currently none).
                 , LHSCore -> NamedArg LHSCore
    lhsFocus        :: NamedArg LHSCore    -- ^ Main argument.
                 , lhsPats         :: [NamedArg Pattern]  -- ^ More application patterns.
                 }
      | LHSWith  { LHSCore -> LHSCore
    lhsHead         :: LHSCore
                 , LHSCore -> List1 Pattern
    lhsWithPatterns :: List1 Pattern      -- ^ At least one @(| p)@.
                 , lhsPats         :: [NamedArg Pattern] -- ^ More application patterns.
                 }
      | LHSEllipsis
                 { LHSCore -> Range
    lhsEllipsisRange :: Range
                 , LHSCore -> LHSCore
    lhsEllipsisPat   :: LHSCore           -- ^ Pattern that was expanded from an ellipsis @...@.
                 }
      deriving LHSCore -> LHSCore -> Bool
    (LHSCore -> LHSCore -> Bool)
    -> (LHSCore -> LHSCore -> Bool) -> Eq LHSCore
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LHSCore -> LHSCore -> Bool
    == :: LHSCore -> LHSCore -> Bool
    $c/= :: LHSCore -> LHSCore -> Bool
    /= :: LHSCore -> LHSCore -> Bool
    Eq

    type RHS = RHS' Expr
    data RHS' e
      = AbsurdRHS -- ^ No right hand side because of absurd match.
      | RHS e
      deriving ((forall a b. (a -> b) -> RHS' a -> RHS' b)
    -> (forall a b. a -> RHS' b -> RHS' a) -> Functor RHS'
    forall a b. a -> RHS' b -> RHS' a
    forall a b. (a -> b) -> RHS' a -> RHS' 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) -> RHS' a -> RHS' b
    fmap :: forall a b. (a -> b) -> RHS' a -> RHS' b
    $c<$ :: forall a b. a -> RHS' b -> RHS' a
    <$ :: forall a b. a -> RHS' b -> RHS' a
    Functor, (forall m. Monoid m => RHS' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> RHS' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> RHS' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> RHS' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> RHS' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> RHS' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> RHS' a -> b)
    -> (forall a. (a -> a -> a) -> RHS' a -> a)
    -> (forall a. (a -> a -> a) -> RHS' a -> a)
    -> (forall a. RHS' a -> [a])
    -> (forall a. RHS' a -> Bool)
    -> (forall a. RHS' a -> Int)
    -> (forall a. Eq a => a -> RHS' a -> Bool)
    -> (forall a. Ord a => RHS' a -> a)
    -> (forall a. Ord a => RHS' a -> a)
    -> (forall a. Num a => RHS' a -> a)
    -> (forall a. Num a => RHS' a -> a)
    -> Foldable RHS'
    forall a. Eq a => a -> RHS' a -> Bool
    forall a. Num a => RHS' a -> a
    forall a. Ord a => RHS' a -> a
    forall m. Monoid m => RHS' m -> m
    forall a. RHS' a -> Bool
    forall a. RHS' a -> Int
    forall a. RHS' a -> [a]
    forall a. (a -> a -> a) -> RHS' a -> a
    forall m a. Monoid m => (a -> m) -> RHS' a -> m
    forall b a. (b -> a -> b) -> b -> RHS' a -> b
    forall a b. (a -> b -> b) -> b -> RHS' 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 => RHS' m -> m
    fold :: forall m. Monoid m => RHS' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> RHS' a -> a
    foldr1 :: forall a. (a -> a -> a) -> RHS' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> RHS' a -> a
    foldl1 :: forall a. (a -> a -> a) -> RHS' a -> a
    $ctoList :: forall a. RHS' a -> [a]
    toList :: forall a. RHS' a -> [a]
    $cnull :: forall a. RHS' a -> Bool
    null :: forall a. RHS' a -> Bool
    $clength :: forall a. RHS' a -> Int
    length :: forall a. RHS' a -> Int
    $celem :: forall a. Eq a => a -> RHS' a -> Bool
    elem :: forall a. Eq a => a -> RHS' a -> Bool
    $cmaximum :: forall a. Ord a => RHS' a -> a
    maximum :: forall a. Ord a => RHS' a -> a
    $cminimum :: forall a. Ord a => RHS' a -> a
    minimum :: forall a. Ord a => RHS' a -> a
    $csum :: forall a. Num a => RHS' a -> a
    sum :: forall a. Num a => RHS' a -> a
    $cproduct :: forall a. Num a => RHS' a -> a
    product :: forall a. Num a => RHS' a -> a
    Foldable, Functor RHS'
    Foldable RHS'
    (Functor RHS', Foldable RHS') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> RHS' a -> f (RHS' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        RHS' (f a) -> f (RHS' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> RHS' a -> m (RHS' b))
    -> (forall (m :: * -> *) a. Monad m => RHS' (m a) -> m (RHS' a))
    -> Traversable RHS'
    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 => RHS' (m a) -> m (RHS' a)
    forall (f :: * -> *) a. Applicative f => RHS' (f a) -> f (RHS' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> RHS' a -> m (RHS' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RHS' a -> f (RHS' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RHS' a -> f (RHS' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RHS' a -> f (RHS' b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => RHS' (f a) -> f (RHS' a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => RHS' (f a) -> f (RHS' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> RHS' a -> m (RHS' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> RHS' a -> m (RHS' b)
    $csequence :: forall (m :: * -> *) a. Monad m => RHS' (m a) -> m (RHS' a)
    sequence :: forall (m :: * -> *) a. Monad m => RHS' (m a) -> m (RHS' a)
    Traversable, RHS' e -> RHS' e -> Bool
    (RHS' e -> RHS' e -> Bool)
    -> (RHS' e -> RHS' e -> Bool) -> Eq (RHS' e)
    forall e. Eq e => RHS' e -> RHS' e -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall e. Eq e => RHS' e -> RHS' e -> Bool
    == :: RHS' e -> RHS' e -> Bool
    $c/= :: forall e. Eq e => RHS' e -> RHS' e -> Bool
    /= :: RHS' e -> RHS' e -> Bool
    Eq)

    -- | @where@ block following a clause.
    type WhereClause = WhereClause' [Declaration]

    -- | The generalization @WhereClause'@ is for the sake of "Agda.Concrete.Generic".
    data WhereClause' decls
      = NoWhere
          -- ^ No @where@ clauses.
      | AnyWhere Range decls
          -- ^ Ordinary @where@.  'Range' of the @where@ keyword.
          --   List of declarations can be empty.
      | SomeWhere Range Erased Name Access decls
          -- ^ Named where: @module M where ds@.
          --   'Range' of the keywords @module@ and @where@.
          --   The 'Access' flag applies to the 'Name' (not the module contents!)
          --   and is propagated from the parent function.
          --   List of declarations can be empty.
      deriving (WhereClause' decls -> WhereClause' decls -> Bool
    (WhereClause' decls -> WhereClause' decls -> Bool)
    -> (WhereClause' decls -> WhereClause' decls -> Bool)
    -> Eq (WhereClause' decls)
    forall decls.
    Eq decls =>
    WhereClause' decls -> WhereClause' decls -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall decls.
    Eq decls =>
    WhereClause' decls -> WhereClause' decls -> Bool
    == :: WhereClause' decls -> WhereClause' decls -> Bool
    $c/= :: forall decls.
    Eq decls =>
    WhereClause' decls -> WhereClause' decls -> Bool
    /= :: WhereClause' decls -> WhereClause' decls -> Bool
    Eq, (forall a b. (a -> b) -> WhereClause' a -> WhereClause' b)
    -> (forall a b. a -> WhereClause' b -> WhereClause' a)
    -> Functor WhereClause'
    forall a b. a -> WhereClause' b -> WhereClause' a
    forall a b. (a -> b) -> WhereClause' a -> WhereClause' 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) -> WhereClause' a -> WhereClause' b
    fmap :: forall a b. (a -> b) -> WhereClause' a -> WhereClause' b
    $c<$ :: forall a b. a -> WhereClause' b -> WhereClause' a
    <$ :: forall a b. a -> WhereClause' b -> WhereClause' a
    Functor, (forall m. Monoid m => WhereClause' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> WhereClause' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> WhereClause' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> WhereClause' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> WhereClause' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> WhereClause' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> WhereClause' a -> b)
    -> (forall a. (a -> a -> a) -> WhereClause' a -> a)
    -> (forall a. (a -> a -> a) -> WhereClause' a -> a)
    -> (forall a. WhereClause' a -> [a])
    -> (forall a. WhereClause' a -> Bool)
    -> (forall a. WhereClause' a -> Int)
    -> (forall a. Eq a => a -> WhereClause' a -> Bool)
    -> (forall a. Ord a => WhereClause' a -> a)
    -> (forall a. Ord a => WhereClause' a -> a)
    -> (forall a. Num a => WhereClause' a -> a)
    -> (forall a. Num a => WhereClause' a -> a)
    -> Foldable WhereClause'
    forall a. Eq a => a -> WhereClause' a -> Bool
    forall a. Num a => WhereClause' a -> a
    forall a. Ord a => WhereClause' a -> a
    forall m. Monoid m => WhereClause' m -> m
    forall a. WhereClause' a -> Bool
    forall a. WhereClause' a -> Int
    forall a. WhereClause' a -> [a]
    forall a. (a -> a -> a) -> WhereClause' a -> a
    forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
    forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
    forall a b. (a -> b -> b) -> b -> WhereClause' 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 => WhereClause' m -> m
    fold :: forall m. Monoid m => WhereClause' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
    foldr1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
    foldl1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
    $ctoList :: forall a. WhereClause' a -> [a]
    toList :: forall a. WhereClause' a -> [a]
    $cnull :: forall a. WhereClause' a -> Bool
    null :: forall a. WhereClause' a -> Bool
    $clength :: forall a. WhereClause' a -> Int
    length :: forall a. WhereClause' a -> Int
    $celem :: forall a. Eq a => a -> WhereClause' a -> Bool
    elem :: forall a. Eq a => a -> WhereClause' a -> Bool
    $cmaximum :: forall a. Ord a => WhereClause' a -> a
    maximum :: forall a. Ord a => WhereClause' a -> a
    $cminimum :: forall a. Ord a => WhereClause' a -> a
    minimum :: forall a. Ord a => WhereClause' a -> a
    $csum :: forall a. Num a => WhereClause' a -> a
    sum :: forall a. Num a => WhereClause' a -> a
    $cproduct :: forall a. Num a => WhereClause' a -> a
    product :: forall a. Num a => WhereClause' a -> a
    Foldable, Functor WhereClause'
    Foldable WhereClause'
    (Functor WhereClause', Foldable WhereClause') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> WhereClause' a -> f (WhereClause' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        WhereClause' (f a) -> f (WhereClause' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> WhereClause' a -> m (WhereClause' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        WhereClause' (m a) -> m (WhereClause' a))
    -> Traversable WhereClause'
    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 =>
    WhereClause' (m a) -> m (WhereClause' a)
    forall (f :: * -> *) a.
    Applicative f =>
    WhereClause' (f a) -> f (WhereClause' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WhereClause' a -> m (WhereClause' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WhereClause' a -> f (WhereClause' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WhereClause' a -> f (WhereClause' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WhereClause' a -> f (WhereClause' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    WhereClause' (f a) -> f (WhereClause' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    WhereClause' (f a) -> f (WhereClause' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WhereClause' a -> m (WhereClause' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WhereClause' a -> m (WhereClause' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    WhereClause' (m a) -> m (WhereClause' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    WhereClause' (m a) -> m (WhereClause' a)
    Traversable)

    -- | Type of @where@ block following a clause.
    data WhereClause_
      = NoWhere_     -- ^ No @where@ clauses.
      | AnyWhere_    -- ^ Ordinary @where@.
      | SomeWhere_   -- ^ Named where: @module M where ...@.
      deriving (WhereClause_ -> WhereClause_ -> Bool
    (WhereClause_ -> WhereClause_ -> Bool)
    -> (WhereClause_ -> WhereClause_ -> Bool) -> Eq WhereClause_
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: WhereClause_ -> WhereClause_ -> Bool
    == :: WhereClause_ -> WhereClause_ -> Bool
    $c/= :: WhereClause_ -> WhereClause_ -> Bool
    /= :: WhereClause_ -> WhereClause_ -> Bool
    Eq, (forall x. WhereClause_ -> Rep WhereClause_ x)
    -> (forall x. Rep WhereClause_ x -> WhereClause_)
    -> Generic WhereClause_
    forall x. Rep WhereClause_ x -> WhereClause_
    forall x. WhereClause_ -> Rep WhereClause_ x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. WhereClause_ -> Rep WhereClause_ x
    from :: forall x. WhereClause_ -> Rep WhereClause_ x
    $cto :: forall x. Rep WhereClause_ x -> WhereClause_
    to :: forall x. Rep WhereClause_ x -> WhereClause_
    Generic)

    whereClause_ :: WhereClause' a -> WhereClause_
    whereClause_ :: forall a. WhereClause' a -> WhereClause_
    whereClause_ = \case
      NoWhere  {} -> WhereClause_
    NoWhere_
      AnyWhere {} -> WhereClause_
    AnyWhere_
      SomeWhere{} -> WhereClause_
    SomeWhere_

    data LamClause = LamClause
      { LamClause -> [Pattern]
    lamLHS      :: [Pattern]   -- ^ Possibly empty sequence.
      , LamClause -> RHS
    lamRHS      :: RHS
      , LamClause -> Catchall
    lamCatchall :: Catchall
      }
      deriving LamClause -> LamClause -> Bool
    (LamClause -> LamClause -> Bool)
    -> (LamClause -> LamClause -> Bool) -> Eq LamClause
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LamClause -> LamClause -> Bool
    == :: LamClause -> LamClause -> Bool
    $c/= :: LamClause -> LamClause -> Bool
    /= :: LamClause -> LamClause -> Bool
    Eq

    -- | An expression followed by a where clause.
    --   Currently only used to give better a better error message in interaction.
    data ExprWhere = ExprWhere Expr WhereClause

    -- | The things you are allowed to say when you shuffle names between name
    --   spaces (i.e. in @import@, @namespace@, or @open@ declarations).
    type ImportDirective = ImportDirective' Name Name
    type Using           = Using'           Name Name
    type Renaming        = Renaming'        Name Name
    type RenamingDirective = RenamingDirective' Name Name
    type HidingDirective   = HidingDirective'   Name Name  -- 'Hiding' is already taken

    -- | An imported name can be a module or a defined name.
    type ImportedName = ImportedName' Name Name

    -- | The content of the @as@-clause of the import statement.
    data AsName' a = AsName
      { forall a. AsName' a -> a
    asName  :: a
        -- ^ The \"as\" name.
      , forall a. AsName' a -> Range
    asRange :: Range
        -- ^ The range of the \"as\" keyword.  Retained for highlighting purposes.
      }
      deriving (Int -> AsName' a -> ShowS
    [AsName' a] -> ShowS
    AsName' a -> String
    (Int -> AsName' a -> ShowS)
    -> (AsName' a -> String)
    -> ([AsName' a] -> ShowS)
    -> Show (AsName' a)
    forall a. Show a => Int -> AsName' a -> ShowS
    forall a. Show a => [AsName' a] -> ShowS
    forall a. Show a => AsName' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> AsName' a -> ShowS
    showsPrec :: Int -> AsName' a -> ShowS
    $cshow :: forall a. Show a => AsName' a -> String
    show :: AsName' a -> String
    $cshowList :: forall a. Show a => [AsName' a] -> ShowS
    showList :: [AsName' a] -> ShowS
    Show, (forall a b. (a -> b) -> AsName' a -> AsName' b)
    -> (forall a b. a -> AsName' b -> AsName' a) -> Functor AsName'
    forall a b. a -> AsName' b -> AsName' a
    forall a b. (a -> b) -> AsName' a -> AsName' 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) -> AsName' a -> AsName' b
    fmap :: forall a b. (a -> b) -> AsName' a -> AsName' b
    $c<$ :: forall a b. a -> AsName' b -> AsName' a
    <$ :: forall a b. a -> AsName' b -> AsName' a
    Functor, (forall m. Monoid m => AsName' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> AsName' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> AsName' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> AsName' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> AsName' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> AsName' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> AsName' a -> b)
    -> (forall a. (a -> a -> a) -> AsName' a -> a)
    -> (forall a. (a -> a -> a) -> AsName' a -> a)
    -> (forall a. AsName' a -> [a])
    -> (forall a. AsName' a -> Bool)
    -> (forall a. AsName' a -> Int)
    -> (forall a. Eq a => a -> AsName' a -> Bool)
    -> (forall a. Ord a => AsName' a -> a)
    -> (forall a. Ord a => AsName' a -> a)
    -> (forall a. Num a => AsName' a -> a)
    -> (forall a. Num a => AsName' a -> a)
    -> Foldable AsName'
    forall a. Eq a => a -> AsName' a -> Bool
    forall a. Num a => AsName' a -> a
    forall a. Ord a => AsName' a -> a
    forall m. Monoid m => AsName' m -> m
    forall a. AsName' a -> Bool
    forall a. AsName' a -> Int
    forall a. AsName' a -> [a]
    forall a. (a -> a -> a) -> AsName' a -> a
    forall m a. Monoid m => (a -> m) -> AsName' a -> m
    forall b a. (b -> a -> b) -> b -> AsName' a -> b
    forall a b. (a -> b -> b) -> b -> AsName' 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 => AsName' m -> m
    fold :: forall m. Monoid m => AsName' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> AsName' a -> a
    foldr1 :: forall a. (a -> a -> a) -> AsName' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> AsName' a -> a
    foldl1 :: forall a. (a -> a -> a) -> AsName' a -> a
    $ctoList :: forall a. AsName' a -> [a]
    toList :: forall a. AsName' a -> [a]
    $cnull :: forall a. AsName' a -> Bool
    null :: forall a. AsName' a -> Bool
    $clength :: forall a. AsName' a -> Int
    length :: forall a. AsName' a -> Int
    $celem :: forall a. Eq a => a -> AsName' a -> Bool
    elem :: forall a. Eq a => a -> AsName' a -> Bool
    $cmaximum :: forall a. Ord a => AsName' a -> a
    maximum :: forall a. Ord a => AsName' a -> a
    $cminimum :: forall a. Ord a => AsName' a -> a
    minimum :: forall a. Ord a => AsName' a -> a
    $csum :: forall a. Num a => AsName' a -> a
    sum :: forall a. Num a => AsName' a -> a
    $cproduct :: forall a. Num a => AsName' a -> a
    product :: forall a. Num a => AsName' a -> a
    Foldable, Functor AsName'
    Foldable AsName'
    (Functor AsName', Foldable AsName') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> AsName' a -> f (AsName' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        AsName' (f a) -> f (AsName' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> AsName' a -> m (AsName' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        AsName' (m a) -> m (AsName' a))
    -> Traversable AsName'
    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 => AsName' (m a) -> m (AsName' a)
    forall (f :: * -> *) a.
    Applicative f =>
    AsName' (f a) -> f (AsName' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AsName' a -> m (AsName' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AsName' a -> f (AsName' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AsName' a -> f (AsName' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AsName' a -> f (AsName' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    AsName' (f a) -> f (AsName' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    AsName' (f a) -> f (AsName' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AsName' a -> m (AsName' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AsName' a -> m (AsName' b)
    $csequence :: forall (m :: * -> *) a. Monad m => AsName' (m a) -> m (AsName' a)
    sequence :: forall (m :: * -> *) a. Monad m => AsName' (m a) -> m (AsName' a)
    Traversable, AsName' a -> AsName' a -> Bool
    (AsName' a -> AsName' a -> Bool)
    -> (AsName' a -> AsName' a -> Bool) -> Eq (AsName' a)
    forall a. Eq a => AsName' a -> AsName' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => AsName' a -> AsName' a -> Bool
    == :: AsName' a -> AsName' a -> Bool
    $c/= :: forall a. Eq a => AsName' a -> AsName' a -> Bool
    /= :: AsName' a -> AsName' a -> Bool
    Eq)

    -- | From the parser, we get an expression for the @as@-'Name', which
    --   we have to parse into a 'Name'.
    type AsName = AsName' (Either Expr Name)

    {--------------------------------------------------------------------------
        Declarations
     --------------------------------------------------------------------------}

    -- | Just type signatures.
    type TypeSignature = Declaration

    -- | Just field signatures
    type FieldSignature = Declaration

    -- | Just type signatures or instance blocks.
    type TypeSignatureOrInstanceBlock = Declaration

    -- | Isolated record directives parsed as Declarations
    data RecordDirective
       = Induction (Ranged Induction)
           -- ^ Range of keyword @[co]inductive@.
       | Constructor Name IsInstance
       | Eta         (Ranged HasEta0)
           -- ^ Range of @[no-]eta-equality@ keyword.
       | PatternOrCopattern Range
           -- ^ If declaration @pattern@ is present, give its range.
       deriving (RecordDirective -> RecordDirective -> Bool
    (RecordDirective -> RecordDirective -> Bool)
    -> (RecordDirective -> RecordDirective -> Bool)
    -> Eq RecordDirective
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: RecordDirective -> RecordDirective -> Bool
    == :: RecordDirective -> RecordDirective -> Bool
    $c/= :: RecordDirective -> RecordDirective -> Bool
    /= :: RecordDirective -> RecordDirective -> Bool
    Eq, Int -> RecordDirective -> ShowS
    [RecordDirective] -> ShowS
    RecordDirective -> String
    (Int -> RecordDirective -> ShowS)
    -> (RecordDirective -> String)
    -> ([RecordDirective] -> ShowS)
    -> Show RecordDirective
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RecordDirective -> ShowS
    showsPrec :: Int -> RecordDirective -> ShowS
    $cshow :: RecordDirective -> String
    show :: RecordDirective -> String
    $cshowList :: [RecordDirective] -> ShowS
    showList :: [RecordDirective] -> ShowS
    Show)

    type RecordDirectives = RecordDirectives' (Maybe (Name, IsInstance))

    ungatherRecordDirectives :: RecordDirectives -> [RecordDirective]
    ungatherRecordDirectives :: RecordDirectives -> [RecordDirective]
    ungatherRecordDirectives (RecordDirectives Maybe (Ranged Induction)
    ind Maybe (Ranged HasEta0)
    eta Maybe Range
    pat Maybe (Name, IsInstance)
    con) = [Maybe RecordDirective] -> [RecordDirective]
    forall a. [Maybe a] -> [a]
    catMaybes
      [ Ranged Induction -> RecordDirective
    Induction (Ranged Induction -> RecordDirective)
    -> Maybe (Ranged Induction) -> Maybe RecordDirective
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Ranged Induction)
    ind
      , Ranged HasEta0 -> RecordDirective
    Eta (Ranged HasEta0 -> RecordDirective)
    -> Maybe (Ranged HasEta0) -> Maybe RecordDirective
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Ranged HasEta0)
    eta
      , Range -> RecordDirective
    PatternOrCopattern (Range -> RecordDirective) -> Maybe Range -> Maybe RecordDirective
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Range
    pat
      , (Name -> IsInstance -> RecordDirective)
    -> (Name, IsInstance) -> RecordDirective
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> IsInstance -> RecordDirective
    Constructor ((Name, IsInstance) -> RecordDirective)
    -> Maybe (Name, IsInstance) -> Maybe RecordDirective
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Name, IsInstance)
    con
      ]

    {-| The representation type of a declaration. The comments indicate
        which type in the intended family the constructor targets.
    -}

    data Declaration
      = TypeSig ArgInfo TacticAttribute Name Expr
          -- ^ Axioms and functions can be irrelevant. (Hiding should be NotHidden)
      | FieldSig IsInstance TacticAttribute Name (Arg Expr)
      | Generalize KwRange [TypeSignature] -- ^ Variables to be generalized, can be hidden and/or irrelevant.
      | Field KwRange [FieldSignature]
      | FunClause LHS RHS WhereClause Catchall
      | DataSig     Range Erased Name [LamBinding] Expr -- ^ lone data signature in mutual block
      | Data        Range Erased Name [LamBinding] Expr
                    [TypeSignatureOrInstanceBlock]
      | DataDef     Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
      | RecordSig   Range Erased Name [LamBinding] Expr -- ^ lone record signature in mutual block
      | RecordDef   Range Name [RecordDirective] [LamBinding] [Declaration]
      | Record      Range Erased Name [RecordDirective] [LamBinding] Expr
                    [Declaration]
      | Infix Fixity (List1 Name)
      | Syntax      Name Notation -- ^ notation declaration for a name
      | PatternSyn  Range Name [WithHiding Name] Pattern
      | Mutual      KwRange [Declaration]
      | InterleavedMutual KwRange [Declaration]
      | Abstract    KwRange [Declaration]
      | Private     KwRange Origin [Declaration]
        -- ^ In "Agda.Syntax.Concrete.Definitions" we generate private blocks
        --   temporarily, which should be treated different that user-declared
        --   private blocks.  Thus the 'Origin'.
      | InstanceB   KwRange [Declaration]
        -- ^ The 'KwRange' here only refers to the range of the
        --   @instance@ keyword.  The range of the whole block @InstanceB r ds@
        --   is @fuseRange r ds@.
      | LoneConstructor KwRange [Declaration]
      | Macro       KwRange [Declaration]
      | Postulate   KwRange [TypeSignatureOrInstanceBlock]
      | Primitive   KwRange [TypeSignature]
      | Open        Range QName ImportDirective
      | Import      Range QName (Maybe AsName) !OpenShortHand ImportDirective
      | ModuleMacro Range Erased  Name ModuleApplication !OpenShortHand
                    ImportDirective
      | Module      Range Erased QName Telescope [Declaration]
      | UnquoteDecl Range [Name] Expr
          -- ^ @unquoteDecl xs = e@
      | UnquoteDef  Range [Name] Expr
          -- ^ @unquoteDef xs = e@
      | UnquoteData Range Name [Name] Expr
          -- ^ @unquoteDecl data d constructor xs = e@
      | Pragma      Pragma
      | Opaque      KwRange [Declaration]
        -- ^ @opaque ...@
      | Unfolding   KwRange [QName]
        -- ^ @unfolding ...@
      deriving Declaration -> Declaration -> Bool
    (Declaration -> Declaration -> Bool)
    -> (Declaration -> Declaration -> Bool) -> Eq Declaration
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Declaration -> Declaration -> Bool
    == :: Declaration -> Declaration -> Bool
    $c/= :: Declaration -> Declaration -> Bool
    /= :: Declaration -> Declaration -> Bool
    Eq

    -- | Return 'Pragma' if 'Declaration' is 'Pragma'.
    {-# SPECIALIZE isPragma :: Declaration -> Maybe Pragma #-}
    {-# SPECIALIZE isPragma :: Declaration -> [Pragma] #-}
    isPragma :: CMaybe Pragma m => Declaration -> m
    isPragma :: forall m. CMaybe Pragma m => Declaration -> m
    isPragma = \case
        Pragma Pragma
    p                -> Pragma -> m
    forall el coll. Singleton el coll => el -> coll
    singleton Pragma
    p
        Private  KwRange
    _ Origin
    _ [Declaration]
    _          -> m
    forall a. Null a => a
    empty
        Abstract KwRange
    _ [Declaration]
    _            -> m
    forall a. Null a => a
    empty
        InstanceB KwRange
    _ [Declaration]
    _           -> m
    forall a. Null a => a
    empty
        Mutual KwRange
    _ [Declaration]
    _              -> m
    forall a. Null a => a
    empty
        Module Range
    _ Erased
    _ QName
    _ Telescope
    _ [Declaration]
    _        -> m
    forall a. Null a => a
    empty
        Macro KwRange
    _ [Declaration]
    _               -> m
    forall a. Null a => a
    empty
        Record Range
    _ Erased
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ Expr
    _ [Declaration]
    _    -> m
    forall a. Null a => a
    empty
        RecordDef Range
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ [Declaration]
    _     -> m
    forall a. Null a => a
    empty
        TypeSig ArgInfo
    _ TacticAttribute
    _ Name
    _ Expr
    _         -> m
    forall a. Null a => a
    empty
        FieldSig IsInstance
    _ TacticAttribute
    _ Name
    _ Arg Expr
    _        -> m
    forall a. Null a => a
    empty
        Generalize KwRange
    _ [Declaration]
    _          -> m
    forall a. Null a => a
    empty
        Field KwRange
    _ [Declaration]
    _               -> m
    forall a. Null a => a
    empty
        FunClause LHS
    _ RHS
    _ WhereClause
    _ Catchall
    _       -> m
    forall a. Null a => a
    empty
        DataSig Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _       -> m
    forall a. Null a => a
    empty
        Data Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _ [Declaration]
    _        -> m
    forall a. Null a => a
    empty
        DataDef Range
    _ Name
    _ [LamBinding]
    _ [Declaration]
    _         -> m
    forall a. Null a => a
    empty
        RecordSig Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _     -> m
    forall a. Null a => a
    empty
        Infix Fixity
    _ List1 Name
    _               -> m
    forall a. Null a => a
    empty
        Syntax Name
    _ Notation
    _              -> m
    forall a. Null a => a
    empty
        PatternSyn Range
    _ Name
    _ [WithHiding Name]
    _ Pattern
    _      -> m
    forall a. Null a => a
    empty
        InterleavedMutual KwRange
    _ [Declaration]
    _   -> m
    forall a. Null a => a
    empty
        LoneConstructor KwRange
    _ [Declaration]
    _     -> m
    forall a. Null a => a
    empty
        Postulate KwRange
    _ [Declaration]
    _           -> m
    forall a. Null a => a
    empty
        Primitive KwRange
    _ [Declaration]
    _           -> m
    forall a. Null a => a
    empty
        Open Range
    _ QName
    _ ImportDirective
    _              -> m
    forall a. Null a => a
    empty
        Import Range
    _ QName
    _ Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _        -> m
    forall a. Null a => a
    empty
        ModuleMacro Range
    _ Erased
    _ Name
    _ ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _ -> m
    forall a. Null a => a
    empty
        UnquoteDecl Range
    _ [Name]
    _ Expr
    _       -> m
    forall a. Null a => a
    empty
        UnquoteDef Range
    _ [Name]
    _ Expr
    _        -> m
    forall a. Null a => a
    empty
        UnquoteData Range
    _ Name
    _ [Name]
    _ Expr
    _     -> m
    forall a. Null a => a
    empty
        Opaque KwRange
    _ [Declaration]
    _              -> m
    forall a. Null a => a
    empty
        Unfolding KwRange
    _ [QName]
    _           -> m
    forall a. Null a => a
    empty

    data ModuleApplication
      = SectionApp Range Telescope QName [Expr]
        -- ^ @tel M exprs@ where @M exprs@ is a 'RawApp' just after parsing.
      | RecordModuleInstance Range QName
        -- ^ @M {{...}}@
      deriving 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

    data OpenShortHand = DoOpen | DontOpen
      deriving (OpenShortHand -> OpenShortHand -> Bool
    (OpenShortHand -> OpenShortHand -> Bool)
    -> (OpenShortHand -> OpenShortHand -> Bool) -> Eq OpenShortHand
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: OpenShortHand -> OpenShortHand -> Bool
    == :: OpenShortHand -> OpenShortHand -> Bool
    $c/= :: OpenShortHand -> OpenShortHand -> Bool
    /= :: OpenShortHand -> OpenShortHand -> Bool
    Eq, Int -> OpenShortHand -> ShowS
    [OpenShortHand] -> ShowS
    OpenShortHand -> String
    (Int -> OpenShortHand -> ShowS)
    -> (OpenShortHand -> String)
    -> ([OpenShortHand] -> ShowS)
    -> Show OpenShortHand
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> OpenShortHand -> ShowS
    showsPrec :: Int -> OpenShortHand -> ShowS
    $cshow :: OpenShortHand -> String
    show :: OpenShortHand -> String
    $cshowList :: [OpenShortHand] -> ShowS
    showList :: [OpenShortHand] -> ShowS
    Show, (forall x. OpenShortHand -> Rep OpenShortHand x)
    -> (forall x. Rep OpenShortHand x -> OpenShortHand)
    -> Generic OpenShortHand
    forall x. Rep OpenShortHand x -> OpenShortHand
    forall x. OpenShortHand -> Rep OpenShortHand x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. OpenShortHand -> Rep OpenShortHand x
    from :: forall x. OpenShortHand -> Rep OpenShortHand x
    $cto :: forall x. Rep OpenShortHand x -> OpenShortHand
    to :: forall x. Rep OpenShortHand x -> OpenShortHand
    Generic)

    -- Pragmas ----------------------------------------------------------------

    data Pragma
      = OptionsPragma               Range [String]
      | BuiltinPragma               Range RString QName
      | RewritePragma               Range Range [QName]        -- ^ Second Range is for REWRITE keyword.
      | ForeignPragma               Range (Ranged BackendName) String
      | CompilePragma               Range (Ranged BackendName) QName String
      | StaticPragma                Range QName
      | InlinePragma                Range Bool QName  -- ^ INLINE or NOINLINE

      | ImpossiblePragma            Range [String]
        -- ^ Throws an internal error in the scope checker.
        --   The 'String's are words to be displayed with the error.
      | EtaPragma                   Range QName
        -- ^ For coinductive records, use pragma instead of regular
        --   @eta-equality@ definition (as it is might make Agda loop).
      | WarningOnUsage              Range QName Text
        -- ^ Applies to the named function
      | WarningOnImport             Range Text
        -- ^ Applies to the current module
      | InjectivePragma             Range QName
        -- ^ Mark a definition as injective for the pattern matching unifier.
      | InjectiveForInferencePragma Range QName
        -- ^ Mark a definition as injective for the conversion checker
      | DisplayPragma               Range Pattern Expr
        -- ^ Display lhs as rhs (modifies the printer).

      -- Attached (more or less) pragmas handled in the nicifier (Concrete.Definitions):
      | CatchallPragma              Range
        -- ^ Applies to the following function clause.
      | TerminationCheckPragma      Range (TerminationCheck Name)
        -- ^ Applies to the following function (and all that are mutually recursive with it)
        --   or to the functions in the following mutual block.
      | NoCoverageCheckPragma       Range
        -- ^ Applies to the following function (and all that are mutually recursive with it)
        --   or to the functions in the following mutual block.
      | NoPositivityCheckPragma     Range
        -- ^ Applies to the following data/record type or mutual block.
      | PolarityPragma              Range Name [Ranged Occurrence]
      | NoUniverseCheckPragma       Range
        -- ^ Applies to the following data/record type.
      | NotProjectionLikePragma     Range QName
        -- ^ Applies to the stated function
      | OverlapPragma             Range [QName] OverlapMode
        -- ^ Applies to the given name(s), which must be instance names
        -- (checked by the type checker).
      deriving 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

    ---------------------------------------------------------------------------

    -- | Modules: Top-level pragmas plus other top-level declarations.

    data Module = Mod
      { Module -> [Pragma]
    modPragmas :: [Pragma]
      , Module -> [Declaration]
    modDecls   :: [Declaration]
      }

    -- | Splits off allowed (= import) declarations before the first
    --   non-allowed declaration.
    --   After successful parsing, the first non-allowed declaration
    --   should be a module declaration.
    spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
    spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
    spanAllowedBeforeModule = (Declaration -> Bool)
    -> [Declaration] -> ([Declaration], [Declaration])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span Declaration -> Bool
    isAllowedBeforeModule
      where
        isAllowedBeforeModule :: Declaration -> Bool
    isAllowedBeforeModule (Pragma OptionsPragma{}) = Bool
    True
        isAllowedBeforeModule (Pragma BuiltinPragma{}) = Bool
    True
        isAllowedBeforeModule (Private KwRange
    _ Origin
    _ [Declaration]
    ds) = (Declaration -> Bool) -> [Declaration] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Declaration -> Bool
    isAllowedBeforeModule [Declaration]
    ds
        isAllowedBeforeModule Import{}       = Bool
    True
        isAllowedBeforeModule ModuleMacro{}  = Bool
    True
        isAllowedBeforeModule Open{}         = Bool
    True
        isAllowedBeforeModule Declaration
    _              = Bool
    False

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

    -- | Extended content of an interaction hole.
    data HoleContent' qn nm p e
      = HoleContentExpr    e                       -- ^ @e@
      | HoleContentRewrite [RewriteEqn' qn nm p e] -- ^ @(rewrite | invert) e0 | ... | en@
      deriving ((forall a b.
     (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b)
    -> (forall a b.
        a -> HoleContent' qn nm p b -> HoleContent' qn nm p a)
    -> Functor (HoleContent' qn nm p)
    forall a b. a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
    forall a b.
    (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
    forall qn nm p a b.
    a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
    forall qn nm p a b.
    (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall qn nm p a b.
    (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
    fmap :: forall a b.
    (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
    $c<$ :: forall qn nm p a b.
    a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
    <$ :: forall a b. a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
    Functor, (forall m. Monoid m => HoleContent' qn nm p m -> m)
    -> (forall m a.
        Monoid m =>
        (a -> m) -> HoleContent' qn nm p a -> m)
    -> (forall m a.
        Monoid m =>
        (a -> m) -> HoleContent' qn nm p a -> m)
    -> (forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b)
    -> (forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b)
    -> (forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b)
    -> (forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b)
    -> (forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a)
    -> (forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a)
    -> (forall a. HoleContent' qn nm p a -> [a])
    -> (forall a. HoleContent' qn nm p a -> Bool)
    -> (forall a. HoleContent' qn nm p a -> Int)
    -> (forall a. Eq a => a -> HoleContent' qn nm p a -> Bool)
    -> (forall a. Ord a => HoleContent' qn nm p a -> a)
    -> (forall a. Ord a => HoleContent' qn nm p a -> a)
    -> (forall a. Num a => HoleContent' qn nm p a -> a)
    -> (forall a. Num a => HoleContent' qn nm p a -> a)
    -> Foldable (HoleContent' qn nm p)
    forall a. Eq a => a -> HoleContent' qn nm p a -> Bool
    forall a. Num a => HoleContent' qn nm p a -> a
    forall a. Ord a => HoleContent' qn nm p a -> a
    forall m. Monoid m => HoleContent' qn nm p m -> m
    forall a. HoleContent' qn nm p a -> Bool
    forall a. HoleContent' qn nm p a -> Int
    forall a. HoleContent' qn nm p a -> [a]
    forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a
    forall m a. Monoid m => (a -> m) -> HoleContent' qn nm p a -> m
    forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
    forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
    forall qn nm p a. Eq a => a -> HoleContent' qn nm p a -> Bool
    forall qn nm p a. Num a => HoleContent' qn nm p a -> a
    forall qn nm p a. Ord a => HoleContent' qn nm p a -> a
    forall qn nm p m. Monoid m => HoleContent' qn nm p m -> m
    forall qn nm p a. HoleContent' qn nm p a -> Bool
    forall qn nm p a. HoleContent' qn nm p a -> Int
    forall qn nm p a. HoleContent' qn nm p a -> [a]
    forall qn nm p a. (a -> a -> a) -> HoleContent' qn nm p a -> a
    forall qn nm p m a.
    Monoid m =>
    (a -> m) -> HoleContent' qn nm p a -> m
    forall qn nm p b a.
    (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
    forall qn nm p a b.
    (a -> b -> b) -> b -> HoleContent' qn nm p 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 qn nm p m. Monoid m => HoleContent' qn nm p m -> m
    fold :: forall m. Monoid m => HoleContent' qn nm p m -> m
    $cfoldMap :: forall qn nm p m a.
    Monoid m =>
    (a -> m) -> HoleContent' qn nm p a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> HoleContent' qn nm p a -> m
    $cfoldMap' :: forall qn nm p m a.
    Monoid m =>
    (a -> m) -> HoleContent' qn nm p a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> HoleContent' qn nm p a -> m
    $cfoldr :: forall qn nm p a b.
    (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
    $cfoldr' :: forall qn nm p a b.
    (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
    $cfoldl :: forall qn nm p b a.
    (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
    $cfoldl' :: forall qn nm p b a.
    (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
    $cfoldr1 :: forall qn nm p a. (a -> a -> a) -> HoleContent' qn nm p a -> a
    foldr1 :: forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a
    $cfoldl1 :: forall qn nm p a. (a -> a -> a) -> HoleContent' qn nm p a -> a
    foldl1 :: forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a
    $ctoList :: forall qn nm p a. HoleContent' qn nm p a -> [a]
    toList :: forall a. HoleContent' qn nm p a -> [a]
    $cnull :: forall qn nm p a. HoleContent' qn nm p a -> Bool
    null :: forall a. HoleContent' qn nm p a -> Bool
    $clength :: forall qn nm p a. HoleContent' qn nm p a -> Int
    length :: forall a. HoleContent' qn nm p a -> Int
    $celem :: forall qn nm p a. Eq a => a -> HoleContent' qn nm p a -> Bool
    elem :: forall a. Eq a => a -> HoleContent' qn nm p a -> Bool
    $cmaximum :: forall qn nm p a. Ord a => HoleContent' qn nm p a -> a
    maximum :: forall a. Ord a => HoleContent' qn nm p a -> a
    $cminimum :: forall qn nm p a. Ord a => HoleContent' qn nm p a -> a
    minimum :: forall a. Ord a => HoleContent' qn nm p a -> a
    $csum :: forall qn nm p a. Num a => HoleContent' qn nm p a -> a
    sum :: forall a. Num a => HoleContent' qn nm p a -> a
    $cproduct :: forall qn nm p a. Num a => HoleContent' qn nm p a -> a
    product :: forall a. Num a => HoleContent' qn nm p a -> a
    Foldable, Functor (HoleContent' qn nm p)
    Foldable (HoleContent' qn nm p)
    (Functor (HoleContent' qn nm p),
     Foldable (HoleContent' qn nm p)) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a))
    -> Traversable (HoleContent' qn nm p)
    forall qn nm p. Functor (HoleContent' qn nm p)
    forall qn nm p. Foldable (HoleContent' qn nm p)
    forall qn nm p (m :: * -> *) a.
    Monad m =>
    HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
    forall qn nm p (f :: * -> *) a.
    Applicative f =>
    HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
    forall qn nm p (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
    forall qn nm p (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
    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 =>
    HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
    forall (f :: * -> *) a.
    Applicative f =>
    HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
    $ctraverse :: forall qn nm p (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
    $csequenceA :: forall qn nm p (f :: * -> *) a.
    Applicative f =>
    HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
    $cmapM :: forall qn nm p (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
    $csequence :: forall qn nm p (m :: * -> *) a.
    Monad m =>
    HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
    Traversable)

    type HoleContent = HoleContent' () Name Pattern Expr

    ---------------------------------------------------------------------------
    -- * Smart constructors
    ---------------------------------------------------------------------------

    rawApp :: List1 Expr -> Expr
    rawApp :: List1 Expr -> Expr
    rawApp es :: List1 Expr
    es@(Expr
    e1 :| Expr
    e2 : [Expr]
    rest) = Range -> List2 Expr -> Expr
    RawApp (List1 Expr -> Range
    forall a. HasRange a => a -> Range
    getRange List1 Expr
    es) (List2 Expr -> Expr) -> List2 Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr -> [Expr] -> List2 Expr
    forall a. a -> a -> [a] -> List2 a
    List2 Expr
    e1 Expr
    e2 [Expr]
    rest
    rawApp (Expr
    e :| []) = Expr
    e

    rawAppP :: List1 Pattern -> Pattern
    rawAppP :: List1 Pattern -> Pattern
    rawAppP ps :: List1 Pattern
    ps@(Pattern
    p1 :| Pattern
    p2 : [Pattern]
    rest) = Range -> List2 Pattern -> Pattern
    RawAppP (List1 Pattern -> Range
    forall a. HasRange a => a -> Range
    getRange List1 Pattern
    ps) (List2 Pattern -> Pattern) -> List2 Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Pattern -> [Pattern] -> List2 Pattern
    forall a. a -> a -> [a] -> List2 a
    List2 Pattern
    p1 Pattern
    p2 [Pattern]
    rest
    rawAppP (Pattern
    p :| []) = Pattern
    p

    {--------------------------------------------------------------------------
        Views
     --------------------------------------------------------------------------}

    -- | The 'Expr' is not an application.
    data AppView = AppView Expr [NamedArg Expr]

    appView :: Expr -> AppView
    appView :: Expr -> AppView
    appView Expr
    e = [NamedArg Expr] -> AppView
    f (DList (NamedArg Expr) -> [NamedArg Expr]
    forall a. DList a -> [a]
    DL.toList DList (NamedArg Expr)
    ess)
      where
        ([NamedArg Expr] -> AppView
    f, DList (NamedArg Expr)
    ess) = Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    appView' Expr
    e

        appView' :: Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
        appView' :: Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    appView' = \case
          App Range
    r Expr
    e1 NamedArg Expr
    e2      -> Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    appView' Expr
    e1 ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    -> (([NamedArg Expr] -> AppView, DList (NamedArg Expr))
        -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr)))
    -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    forall a b. a -> (a -> b) -> b
    & (DList (NamedArg Expr) -> DList (NamedArg Expr))
    -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (DList (NamedArg Expr) -> NamedArg Expr -> DList (NamedArg Expr)
    forall a. DList a -> a -> DList a
    `DL.snoc` NamedArg Expr
    e2)
          RawApp Range
    _ (List2 Expr
    e1 Expr
    e2 [Expr]
    es)
                           -> (Expr -> [NamedArg Expr] -> AppView
    AppView Expr
    e1, [NamedArg Expr] -> DList (NamedArg Expr)
    forall a. [a] -> DList a
    DL.fromList ((Expr -> NamedArg Expr) -> [Expr] -> [NamedArg Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> NamedArg Expr
    toNamedArg (Expr
    e2 Expr -> [Expr] -> [Expr]
    forall a. a -> [a] -> [a]
    : [Expr]
    es)))
          Expr
    e                -> (Expr -> [NamedArg Expr] -> AppView
    AppView Expr
    e, DList (NamedArg Expr)
    forall a. Monoid a => a
    mempty)

    unAppView :: AppView -> Expr
    unAppView :: AppView -> Expr
    unAppView (AppView Expr
    e [NamedArg Expr]
    nargs) = List1 Expr -> Expr
    rawApp (Expr
    e Expr -> [Expr] -> List1 Expr
    forall a. a -> [a] -> NonEmpty a
    :| (NamedArg Expr -> Expr) -> [NamedArg Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> Expr
    unNamedArg [NamedArg Expr]
    nargs)

    -- | Parse outermost hiding information.
    toNamedArg :: Expr -> NamedArg Expr
    toNamedArg :: Expr -> NamedArg Expr
    toNamedArg = \case
      HiddenArg   Range
    _ Named NamedName Expr
    e -> NamedArg Expr -> NamedArg Expr
    forall a. LensHiding a => a -> a
    hide         (NamedArg Expr -> NamedArg Expr) -> NamedArg Expr -> NamedArg Expr
    forall a b. (a -> b) -> a -> b
    $ Named NamedName Expr -> NamedArg Expr
    forall a. a -> Arg a
    defaultArg Named NamedName Expr
    e
      InstanceArg Range
    _ Named NamedName Expr
    e -> NamedArg Expr -> NamedArg Expr
    forall a. LensHiding a => a -> a
    makeInstance (NamedArg Expr -> NamedArg Expr) -> NamedArg Expr -> NamedArg Expr
    forall a b. (a -> b) -> a -> b
    $ Named NamedName Expr -> NamedArg Expr
    forall a. a -> Arg a
    defaultArg Named NamedName Expr
    e
      Expr
    e -> Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    e

    -- | Unparse hiding information.
    unNamedArg :: NamedArg Expr -> Expr
    unNamedArg :: NamedArg Expr -> Expr
    unNamedArg NamedArg Expr
    narg = ((Named NamedName Expr -> Expr) -> Named NamedName Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ NamedArg Expr -> Named NamedName Expr
    forall e. Arg e -> e
    unArg NamedArg Expr
    narg) ((Named NamedName Expr -> Expr) -> Expr)
    -> (Named NamedName Expr -> Expr) -> Expr
    forall a b. (a -> b) -> a -> b
    $ case NamedArg Expr -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg Expr
    narg of
      Hiding
    Hidden     -> Range -> Named NamedName Expr -> Expr
    HiddenArg (NamedArg Expr -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg Expr
    narg)
      Hiding
    NotHidden  -> Named NamedName Expr -> Expr
    forall name a. Named name a -> a
    namedThing
      Instance{} -> Range -> Named NamedName Expr -> Expr
    InstanceArg (NamedArg Expr -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg Expr
    narg)

    isSingleIdentifierP :: Pattern -> Maybe Name
    isSingleIdentifierP :: Pattern -> Maybe Name
    isSingleIdentifierP = \case
      IdentP Bool
    _ (QName Name
    x) -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
      WildP Range
    r            -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just (Name -> Maybe Name) -> Name -> Maybe Name
    forall a b. (a -> b) -> a -> b
    $ Range -> Name
    noName Range
    r
      ParenP Range
    _ Pattern
    p         -> Pattern -> Maybe Name
    isSingleIdentifierP Pattern
    p
      Pattern
    _                  -> Maybe Name
    forall a. Maybe a
    Nothing

    removeParenP :: Pattern -> Pattern
    removeParenP :: Pattern -> Pattern
    removeParenP = \case
        ParenP Range
    _ Pattern
    p -> Pattern -> Pattern
    removeParenP Pattern
    p
        Pattern
    p -> Pattern
    p

    -- | Observe the hiding status of an expression
    observeHiding :: Expr -> WithHiding Expr
    observeHiding :: Expr -> WithHiding Expr
    observeHiding = \case
      HiddenArg Range
    _   (Named Maybe NamedName
    Nothing Expr
    e) -> Hiding -> Expr -> WithHiding Expr
    forall a. Hiding -> a -> WithHiding a
    WithHiding Hiding
    Hidden Expr
    e
      InstanceArg Range
    _ (Named Maybe NamedName
    Nothing Expr
    e) -> Hiding -> Expr -> WithHiding Expr
    forall a. Hiding -> a -> WithHiding a
    WithHiding (Overlappable -> Hiding
    Instance Overlappable
    NoOverlap) Expr
    e
      Expr
    e                               -> Hiding -> Expr -> WithHiding Expr
    forall a. Hiding -> a -> WithHiding a
    WithHiding Hiding
    NotHidden Expr
    e

    -- | Observe the relevance status of an expression
    observeRelevance :: Expr -> (Relevance, Expr)
    observeRelevance :: Expr -> (Relevance, Expr)
    observeRelevance = \case
      Dot KwRange
    kwr Expr
    e       -> (OriginIrrelevant -> Relevance
    Irrelevant (Range -> OriginIrrelevant
    OIrrDot (KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr)), Expr
    e)
      DoubleDot KwRange
    kwr Expr
    e -> (OriginShapeIrrelevant -> Relevance
    ShapeIrrelevant (Range -> OriginShapeIrrelevant
    OShIrrDotDot (KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr)), Expr
    e)
      Expr
    e               -> (OriginRelevant -> Relevance
    Relevant OriginRelevant
    forall a. Null a => a
    empty, Expr
    e)

    -- | Observe various modifiers applied to an expression
    observeModifiers :: Expr -> Arg Expr
    observeModifiers :: Expr -> Arg Expr
    observeModifiers Expr
    e =
      let (Relevance
    rel, WithHiding Hiding
    hid Expr
    e') = (Expr -> WithHiding Expr)
    -> (Relevance, Expr) -> (Relevance, WithHiding Expr)
    forall a b. (a -> b) -> (Relevance, a) -> (Relevance, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> WithHiding Expr
    observeHiding (Expr -> (Relevance, Expr)
    observeRelevance Expr
    e) in
      Relevance -> Arg Expr -> Arg Expr
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    rel (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
    forall a b. (a -> b) -> a -> b
    $ Hiding -> Arg Expr -> Arg Expr
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    hid (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Arg Expr
    forall a. a -> Arg a
    defaultArg Expr
    e'

    returnExpr :: Expr -> Maybe Expr
    returnExpr :: Expr -> Maybe Expr
    returnExpr (Pi Telescope1
    _ Expr
    e)        = Expr -> Maybe Expr
    returnExpr Expr
    e
    returnExpr (Fun Range
    _ Arg Expr
    _  Expr
    e)    = Expr -> Maybe Expr
    returnExpr Expr
    e
    returnExpr (Let Range
    _ List1 Declaration
    _ Maybe Expr
    e)     = Expr -> Maybe Expr
    returnExpr (Expr -> Maybe Expr) -> Maybe Expr -> Maybe Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Maybe Expr
    e
    returnExpr (Paren Range
    _ Expr
    e)     = Expr -> Maybe Expr
    returnExpr Expr
    e
    returnExpr (Generalized Expr
    e) = Expr -> Maybe Expr
    returnExpr Expr
    e
    returnExpr Expr
    e               = Expr -> Maybe Expr
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e

    -- | Turn an expression into a pattern. Fails if the expression is not a
    --   valid pattern.

    isPattern :: Expr -> Maybe Pattern
    isPattern :: Expr -> Maybe Pattern
    isPattern = (Expr -> Maybe Pattern) -> Expr -> Maybe Pattern
    forall (m :: * -> *).
    Applicative m =>
    (Expr -> m Pattern) -> Expr -> m Pattern
    exprToPattern (Maybe Pattern -> Expr -> Maybe Pattern
    forall a b. a -> b -> a
    const Maybe Pattern
    forall a. Maybe a
    Nothing)

    -- | Turn an expression into a pattern, turning non-pattern subexpressions into 'WildP'.

    exprToPatternWithHoles :: Expr -> Pattern
    exprToPatternWithHoles :: Expr -> Pattern
    exprToPatternWithHoles = Identity Pattern -> Pattern
    forall a. Identity a -> a
    runIdentity (Identity Pattern -> Pattern)
    -> (Expr -> Identity Pattern) -> Expr -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Identity Pattern) -> Expr -> Identity Pattern
    forall (m :: * -> *).
    Applicative m =>
    (Expr -> m Pattern) -> Expr -> m Pattern
    exprToPattern (Pattern -> Identity Pattern
    forall a. a -> Identity a
    Identity (Pattern -> Identity Pattern)
    -> (Expr -> Pattern) -> Expr -> Identity Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Pattern
    WildP (Range -> Pattern) -> (Expr -> Range) -> Expr -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Range
    forall a. HasRange a => a -> Range
    getRange)

    -- | Generic expression to pattern conversion.

    exprToPattern :: Applicative m
      => (Expr -> m Pattern)  -- ^ Default result for non-pattern things.
      -> Expr                 -- ^ The expression to translate.
      -> m Pattern            -- ^ The translated pattern (maybe).
    exprToPattern :: forall (m :: * -> *).
    Applicative m =>
    (Expr -> m Pattern) -> Expr -> m Pattern
    exprToPattern Expr -> m Pattern
    fallback = Expr -> m Pattern
    loop
      where
      loop :: Expr -> m Pattern
    loop = \case
        Ident       QName
    x        -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Bool -> QName -> Pattern
    IdentP Bool
    True QName
    x
        App         Range
    _ Expr
    e1 NamedArg Expr
    e2  -> Pattern -> NamedArg Pattern -> Pattern
    AppP (Pattern -> NamedArg Pattern -> Pattern)
    -> m Pattern -> m (NamedArg Pattern -> Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Pattern
    loop Expr
    e1 m (NamedArg Pattern -> Pattern)
    -> m (NamedArg Pattern) -> m Pattern
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Named NamedName Expr -> m (Named_ Pattern))
    -> NamedArg Expr -> m (NamedArg Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((Expr -> m Pattern) -> Named NamedName Expr -> m (Named_ Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Expr -> m Pattern
    loop) NamedArg Expr
    e2
        Paren       Range
    r Expr
    e      -> Range -> Pattern -> Pattern
    ParenP Range
    r (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Pattern
    loop Expr
    e
        Underscore  Range
    r Maybe String
    _      -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Pattern
    WildP Range
    r
        Absurd      Range
    r        -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Pattern
    AbsurdP Range
    r
        As          Range
    r Name
    x Expr
    e    -> Range -> (Pattern -> Pattern) -> Pattern -> Pattern
    pushUnderBracesP Range
    r (Range -> Name -> Pattern -> Pattern
    AsP Range
    r Name
    x) (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Pattern
    loop Expr
    e
        e0 :: Expr
    e0@(Dot       KwRange
    kwr Expr
    e) -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> (Expr -> Pattern) -> Expr -> Pattern
    pushUnderBracesE Range
    r (KwRange -> Range -> Expr -> Pattern
    DotP KwRange
    kwr Range
    r) Expr
    e
          where r :: Range
    r = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e0
        -- Wen, 2020-08-27: We disallow Float patterns, since equality for floating
        -- point numbers is not stable across architectures and with different
        -- compiler flags.
        e :: Expr
    e@(Lit Range
    _ LitFloat{}) -> Expr -> m Pattern
    fallback Expr
    e
        Lit         Range
    r Literal
    l      -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Literal -> Pattern
    LitP Range
    r Literal
    l
        HiddenArg   Range
    r Named NamedName Expr
    e      -> Range -> Named_ Pattern -> Pattern
    HiddenP   Range
    r (Named_ Pattern -> Pattern) -> m (Named_ Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Pattern) -> Named NamedName Expr -> m (Named_ Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Expr -> m Pattern
    loop Named NamedName Expr
    e
        InstanceArg Range
    r Named NamedName Expr
    e      -> Range -> Named_ Pattern -> Pattern
    InstanceP Range
    r (Named_ Pattern -> Pattern) -> m (Named_ Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Pattern) -> Named NamedName Expr -> m (Named_ Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Expr -> m Pattern
    loop Named NamedName Expr
    e
        RawApp      Range
    r List2 Expr
    es     -> Range -> List2 Pattern -> Pattern
    RawAppP   Range
    r (List2 Pattern -> Pattern) -> m (List2 Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Pattern) -> List2 Expr -> m (List2 Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> List2 a -> f (List2 b)
    traverse Expr -> m Pattern
    loop List2 Expr
    es
        Quote       Range
    r        -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Pattern
    QuoteP Range
    r
        Equal       Range
    r Expr
    e1 Expr
    e2  -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 (Expr, Expr) -> Pattern
    EqualP Range
    r (List1 (Expr, Expr) -> Pattern) -> List1 (Expr, Expr) -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Expr, Expr) -> List1 (Expr, Expr)
    forall el coll. Singleton el coll => el -> coll
    singleton (Expr
    e1, Expr
    e2)
        Ellipsis    Range
    r        -> Pattern -> m Pattern
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r Maybe Pattern
    forall a. Maybe a
    Nothing
        e :: Expr
    e@(Rec KwRange
    kwr Range
    r RecordAssignments
    es)
            -- We cannot translate record expressions with module parts.
          | Just [FieldAssignment]
    fs <- (Either FieldAssignment ModuleAssignment -> Maybe FieldAssignment)
    -> RecordAssignments -> Maybe [FieldAssignment]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Either FieldAssignment ModuleAssignment -> Maybe FieldAssignment
    forall a b. Either a b -> Maybe a
    maybeLeft RecordAssignments
    es -> KwRange -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP KwRange
    kwr Range
    r ([FieldAssignment' Pattern] -> Pattern)
    -> m [FieldAssignment' Pattern] -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FieldAssignment -> m (FieldAssignment' Pattern))
    -> [FieldAssignment] -> m [FieldAssignment' Pattern]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Expr -> m Pattern)
    -> FieldAssignment -> m (FieldAssignment' Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
    traverse Expr -> m Pattern
    loop) [FieldAssignment]
    fs
          | Bool
    otherwise -> Expr -> m Pattern
    fallback Expr
    e
        -- WithApp has already lost the range information of the bars '|'
        WithApp     Range
    r Expr
    e List1 Expr
    es   -> do -- ApplicativeDo
          Pattern
    p  <- Expr -> m Pattern
    loop Expr
    e
          List1 (NamedArg Pattern)
    ps <- List1 Expr
    -> (Expr -> m (NamedArg Pattern)) -> m (List1 (NamedArg Pattern))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    t a -> (a -> f b) -> f (t b)
    forA List1 Expr
    es ((Expr -> m (NamedArg Pattern)) -> m (List1 (NamedArg Pattern)))
    -> (Expr -> m (NamedArg Pattern)) -> m (List1 (NamedArg Pattern))
    forall a b. (a -> b) -> a -> b
    $ \ Expr
    e -> do -- ApplicativeDo
            Pattern
    p <- Expr -> m Pattern
    loop Expr
    e
            pure $ Pattern -> NamedArg Pattern
    forall a. a -> NamedArg a
    defaultNamedArg (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Pattern -> Pattern
    WithP (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e) Pattern
    p   -- TODO #2822: Range!
          pure $ (Pattern -> NamedArg Pattern -> Pattern)
    -> Pattern -> List1 (NamedArg Pattern) -> Pattern
    forall b a. (b -> a -> b) -> b -> NonEmpty a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Pattern -> NamedArg Pattern -> Pattern
    AppP Pattern
    p List1 (NamedArg Pattern)
    ps
        Expr
    e -> Expr -> m Pattern
    fallback Expr
    e

      pushUnderBracesP :: Range -> (Pattern -> Pattern) -> (Pattern -> Pattern)
      pushUnderBracesP :: Range -> (Pattern -> Pattern) -> Pattern -> Pattern
    pushUnderBracesP Range
    r Pattern -> Pattern
    f = \case
        HiddenP   Range
    _ Named_ Pattern
    p   -> Range -> Named_ Pattern -> Pattern
    HiddenP   Range
    r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Pattern) -> Named_ Pattern -> Named_ Pattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern -> Pattern
    f Named_ Pattern
    p
        InstanceP Range
    _ Named_ Pattern
    p   -> Range -> Named_ Pattern -> Pattern
    InstanceP Range
    r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Pattern) -> Named_ Pattern -> Named_ Pattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern -> Pattern
    f Named_ Pattern
    p
        Pattern
    p               -> Pattern -> Pattern
    f Pattern
    p

      pushUnderBracesE :: Range -> (Expr -> Pattern) -> (Expr -> Pattern)
      pushUnderBracesE :: Range -> (Expr -> Pattern) -> Expr -> Pattern
    pushUnderBracesE Range
    r Expr -> Pattern
    f = \case
        HiddenArg   Range
    _ Named NamedName Expr
    p -> Range -> Named_ Pattern -> Pattern
    HiddenP   Range
    r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Pattern) -> Named NamedName Expr -> Named_ Pattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> Pattern
    f Named NamedName Expr
    p
        InstanceArg Range
    _ Named NamedName Expr
    p -> Range -> Named_ Pattern -> Pattern
    InstanceP Range
    r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Pattern) -> Named NamedName Expr -> Named_ Pattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> Pattern
    f Named NamedName Expr
    p
        Expr
    p               -> Expr -> Pattern
    f Expr
    p

    isAbsurdP :: Pattern -> Maybe (Range, Hiding)
    isAbsurdP :: Pattern -> Maybe (Range, Hiding)
    isAbsurdP = \case
      AbsurdP Range
    r      -> (Range, Hiding) -> Maybe (Range, Hiding)
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Range
    r, Hiding
    NotHidden)
      AsP Range
    _ Name
    _      Pattern
    p -> Pattern -> Maybe (Range, Hiding)
    isAbsurdP Pattern
    p
      ParenP Range
    _     Pattern
    p -> Pattern -> Maybe (Range, Hiding)
    isAbsurdP Pattern
    p
      HiddenP   Range
    _ Named_ Pattern
    np -> (Hiding
    Hidden Hiding -> (Range, Hiding) -> (Range, Hiding)
    forall a b. a -> (Range, b) -> (Range, a)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$)              ((Range, Hiding) -> (Range, Hiding))
    -> Maybe (Range, Hiding) -> Maybe (Range, Hiding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> Maybe (Range, Hiding)
    isAbsurdP (Named_ Pattern -> Pattern
    forall name a. Named name a -> a
    namedThing Named_ Pattern
    np)
      InstanceP Range
    _ Named_ Pattern
    np -> (Overlappable -> Hiding
    Instance Overlappable
    YesOverlap Hiding -> (Range, Hiding) -> (Range, Hiding)
    forall a b. a -> (Range, b) -> (Range, a)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) ((Range, Hiding) -> (Range, Hiding))
    -> Maybe (Range, Hiding) -> Maybe (Range, Hiding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> Maybe (Range, Hiding)
    isAbsurdP (Named_ Pattern -> Pattern
    forall name a. Named name a -> a
    namedThing Named_ Pattern
    np)
      Pattern
    _ -> Maybe (Range, Hiding)
    forall a. Maybe a
    Nothing

    isBinderP :: Pattern -> Maybe Binder
    isBinderP :: Pattern -> Maybe Binder
    isBinderP = \case
      IdentP Bool
    _ QName
    qn
                 -> Name -> Binder
    mkBinder_ (Name -> Binder) -> Maybe Name -> Maybe Binder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Maybe Name
    isUnqualified QName
    qn
      WildP Range
    r    -> Binder -> Maybe Binder
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Binder -> Maybe Binder) -> Binder -> Maybe Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    mkBinder_ (Name -> Binder) -> Name -> Binder
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    simpleHole
      AsP Range
    r Name
    n Pattern
    p  -> Binder -> Maybe Binder
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Binder -> Maybe Binder) -> Binder -> Maybe Binder
    forall a b. (a -> b) -> a -> b
    $ Maybe Pattern -> BinderNameOrigin -> BoundName -> Binder
    forall a. Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    Binder (Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just Pattern
    p) BinderNameOrigin
    UserBinderName (BoundName -> Binder) -> BoundName -> Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> BoundName
    mkBoundName_ Name
    n
      ParenP Range
    r Pattern
    p -> Binder -> Maybe Binder
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Binder -> Maybe Binder) -> Binder -> Maybe Binder
    forall a b. (a -> b) -> a -> b
    $ Maybe Pattern -> BinderNameOrigin -> BoundName -> Binder
    forall a. Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    Binder (Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just Pattern
    p) BinderNameOrigin
    UserBinderName (BoundName -> Binder) -> BoundName -> Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> BoundName
    mkBoundName_ (Name -> BoundName) -> Name -> BoundName
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    simpleHole
      Pattern
    _ -> Maybe Binder
    forall a. Maybe a
    Nothing

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

    -- Null
    ------------------------------------------------------------------------

    -- | A 'WhereClause' is 'null' when the @where@ keyword is absent.
    --   An empty list of declarations does not count as 'null' here.

    instance Null (WhereClause' a) where
      empty :: WhereClause' a
    empty = WhereClause' a
    forall a. WhereClause' a
    NoWhere
      null :: WhereClause' a -> Bool
    null WhereClause' a
    NoWhere = Bool
    True
      null AnyWhere{} = Bool
    False
      null SomeWhere{} = Bool
    False

    instance Null WhereClause_ where
      empty :: WhereClause_
    empty = WhereClause_
    NoWhere_
      null :: WhereClause_ -> Bool
    null WhereClause_
    NoWhere_ = Bool
    True
      null WhereClause_
    AnyWhere_ = Bool
    False
      null WhereClause_
    SomeWhere_ = Bool
    False

    -- Lenses
    ------------------------------------------------------------------------

    instance LensHiding LamBinding where
      getHiding :: LamBinding -> Hiding
    getHiding   (DomainFree NamedArg Binder
    x) = NamedArg Binder -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg Binder
    x
      getHiding   (DomainFull TypedBinding' Expr
    a) = TypedBinding' Expr -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding TypedBinding' Expr
    a
      mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding
    mapHiding Hiding -> Hiding
    f (DomainFree NamedArg Binder
    x) = NamedArg Binder -> LamBinding
    forall a. NamedArg Binder -> LamBinding' a
    DomainFree (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' Expr
    a) = TypedBinding' Expr -> LamBinding
    forall a. a -> LamBinding' a
    DomainFull (TypedBinding' Expr -> LamBinding)
    -> TypedBinding' Expr -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ (Hiding -> Hiding) -> TypedBinding' Expr -> TypedBinding' Expr
    forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
    mapHiding Hiding -> Hiding
    f TypedBinding' Expr
    a

    instance LensHiding TypedBinding where
      getHiding :: TypedBinding' Expr -> Hiding
    getHiding (TBind Range
    _ (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' Expr -> TypedBinding' Expr
    mapHiding Hiding -> Hiding
    f (TBind Range
    r List1 (NamedArg Binder)
    xs Expr
    e) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    r ((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 ((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' Expr
    b@TLet{}       = TypedBinding' Expr
    b

    instance LensRelevance TypedBinding where
      getRelevance :: TypedBinding' Expr -> Relevance
    getRelevance (TBind Range
    _ (NamedArg Binder
    x :| [NamedArg Binder]
    _) Expr
    _) = NamedArg Binder -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance NamedArg Binder
    x   -- Slightly dubious
      getRelevance TLet{}               = Relevance
    unitRelevance
      mapRelevance :: (Relevance -> Relevance)
    -> TypedBinding' Expr -> TypedBinding' Expr
    mapRelevance Relevance -> Relevance
    f (TBind Range
    r List1 (NamedArg Binder)
    xs Expr
    e) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    r ((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 ((Relevance -> Relevance) -> NamedArg Binder -> NamedArg Binder
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance Relevance -> Relevance
    f) List1 (NamedArg Binder)
    xs) Expr
    e
      mapRelevance Relevance -> Relevance
    f b :: TypedBinding' Expr
    b@TLet{}       = TypedBinding' Expr
    b

    -- HasRange instances
    ------------------------------------------------------------------------

    instance HasRange e => HasRange (OpApp e) where
      getRange :: OpApp e -> Range
    getRange = \case
        Ordinary e
    e -> e -> Range
    forall a. HasRange a => a -> Range
    getRange e
    e
        SyntaxBindingLambda Range
    r List1 LamBinding
    _ e
    _ -> Range
    r

    instance HasRange Expr where
      getRange :: Expr -> Range
    getRange = \case
          Ident QName
    x            -> QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x
          Lit Range
    r Literal
    _            -> Range
    r
          QuestionMark Range
    r Maybe Int
    _   -> Range
    r
          Underscore Range
    r Maybe String
    _     -> Range
    r
          App Range
    r Expr
    _ NamedArg Expr
    _          -> Range
    r
          RawApp Range
    r List2 Expr
    _         -> Range
    r
          OpApp Range
    r QName
    _ Set1 Name
    _ OpAppArgs
    _      -> Range
    r
          WithApp Range
    r Expr
    _ List1 Expr
    _      -> Range
    r
          Lam Range
    r List1 LamBinding
    _ Expr
    _          -> Range
    r
          AbsurdLam Range
    r Hiding
    _      -> Range
    r
          ExtendedLam Range
    r Erased
    _ List1 LamClause
    _  -> Range
    r
          Fun Range
    r Arg Expr
    _ Expr
    _          -> Range
    r
          Pi Telescope1
    b Expr
    e             -> Telescope1 -> Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Telescope1
    b Expr
    e
          Let Range
    r List1 Declaration
    _ Maybe Expr
    _          -> Range
    r
          Paren Range
    r Expr
    _          -> Range
    r
          IdiomBrackets Range
    r [Expr]
    _  -> Range
    r
          DoBlock Range
    r List1 DoStmt
    _        -> Range
    r
          As Range
    r Name
    _ Expr
    _           -> Range
    r
          Dot KwRange
    r Expr
    e            -> (KwRange, Expr) -> Range
    forall a. HasRange a => a -> Range
    getRange (KwRange
    r, Expr
    e)
          DoubleDot KwRange
    r Expr
    e      -> (KwRange, Expr) -> Range
    forall a. HasRange a => a -> Range
    getRange (KwRange
    r, Expr
    e)
          Absurd Range
    r           -> Range
    r
          HiddenArg Range
    r Named NamedName Expr
    _      -> Range
    r
          InstanceArg Range
    r Named NamedName Expr
    _    -> Range
    r
          Rec KwRange
    _ Range
    r RecordAssignments
    _          -> Range
    r
          RecUpdate KwRange
    _ Range
    r Expr
    _ [FieldAssignment]
    _  -> Range
    r
          Quote Range
    r            -> Range
    r
          QuoteTerm Range
    r        -> Range
    r
          Unquote Range
    r          -> Range
    r
          Tactic Range
    r Expr
    _         -> Range
    r
          DontCare{}         -> Range
    forall a. Range' a
    noRange
          Equal Range
    r Expr
    _ Expr
    _        -> Range
    r
          Ellipsis Range
    r         -> Range
    r
          Generalized Expr
    e      -> Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e
          KnownIdent NameKind
    _ QName
    q     -> QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    q
          KnownOpApp NameKind
    _ Range
    r QName
    _ Set1 Name
    _ OpAppArgs
    _ -> Range
    r

    -- instance HasRange Telescope where
    --     getRange (TeleBind bs) = getRange bs
    --     getRange (TeleFun x y) = fuseRange x y

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

    instance HasRange (TacticAttribute' a) where
      getRange :: TacticAttribute' a -> Range
    getRange = Range -> (Ranged a -> Range) -> Maybe (Ranged a) -> Range
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Range
    forall a. Range' a
    noRange Ranged a -> Range
    forall a. HasRange a => a -> Range
    getRange (Maybe (Ranged a) -> Range)
    -> (TacticAttribute' a -> Maybe (Ranged a))
    -> TacticAttribute' a
    -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TacticAttribute' a -> Maybe (Ranged a)
    forall a. TacticAttribute' a -> Maybe (Ranged a)
    theTacticAttribute

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

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

    instance HasRange BoundName where
      getRange :: BoundName -> Range
    getRange = Name -> Range
    forall a. HasRange a => a -> Range
    getRange (Name -> Range) -> (BoundName -> Name) -> BoundName -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BoundName -> Name
    boundName

    instance HasRange WhereClause where
      getRange :: WhereClause -> Range
    getRange  WhereClause
    NoWhere               = Range
    forall a. Range' a
    noRange
      getRange (AnyWhere Range
    r [Declaration]
    ds)        = (Range, [Declaration]) -> Range
    forall a. HasRange a => a -> Range
    getRange (Range
    r, [Declaration]
    ds)
      getRange (SomeWhere Range
    r Erased
    e Name
    x Access
    _ [Declaration]
    ds) = (Range, Erased, Name, [Declaration]) -> Range
    forall a. HasRange a => a -> Range
    getRange (Range
    r, Erased
    e, Name
    x, [Declaration]
    ds)

    instance HasRange ModuleApplication where
      getRange :: ModuleApplication -> Range
    getRange (SectionApp Range
    r Telescope
    _ QName
    _ [Expr]
    _) = Range
    r
      getRange (RecordModuleInstance Range
    r QName
    _) = Range
    r

    instance HasRange a => HasRange (FieldAssignment' a) where
      getRange :: FieldAssignment' a -> Range
    getRange (FieldAssignment Name
    a a
    b) = Name -> a -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Name
    a a
    b

    instance HasRange ModuleAssignment where
      getRange :: ModuleAssignment -> Range
    getRange (ModuleAssignment QName
    a [Expr]
    b ImportDirective
    c) = QName -> [Expr] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange QName
    a [Expr]
    b Range -> ImportDirective -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` ImportDirective
    c

    instance HasRange RecordDirective where
      getRange :: RecordDirective -> Range
    getRange (Induction Ranged Induction
    a)          = Ranged Induction -> Range
    forall a. HasRange a => a -> Range
    getRange Ranged Induction
    a
      getRange (Eta Ranged HasEta0
    a    )            = Ranged HasEta0 -> Range
    forall a. HasRange a => a -> Range
    getRange Ranged HasEta0
    a
      getRange (Constructor Name
    a IsInstance
    b)      = (Name, IsInstance) -> Range
    forall a. HasRange a => a -> Range
    getRange (Name
    a, IsInstance
    b)
      getRange (PatternOrCopattern Range
    r) = Range
    r

    instance HasRange Declaration where
      getRange :: Declaration -> Range
    getRange (TypeSig ArgInfo
    _ TacticAttribute
    _ Name
    x Expr
    t)       = Name -> Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Name
    x Expr
    t
      getRange (FieldSig IsInstance
    _ TacticAttribute
    _ Name
    x Arg Expr
    t)      = Name -> Arg Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Name
    x Arg Expr
    t
      getRange (Field KwRange
    kwr [Declaration]
    ds)          = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    _) = LHS -> RHS -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange LHS
    lhs RHS
    rhs Range -> WhereClause -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` WhereClause
    wh
      getRange (DataSig Range
    r Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _)     = Range
    r
      getRange (Data Range
    r Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _ [Declaration]
    _)      = Range
    r
      getRange (DataDef Range
    r Name
    _ [LamBinding]
    _ [Declaration]
    _)       = Range
    r
      getRange (RecordSig Range
    r Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _)   = Range
    r
      getRange (RecordDef Range
    r Name
    _ [RecordDirective]
    _ [LamBinding]
    _ [Declaration]
    _)   = Range
    r
      getRange (Record Range
    r Erased
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ Expr
    _ [Declaration]
    _)  = Range
    r
      getRange (Mutual KwRange
    kwr [Declaration]
    ds)         = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (InterleavedMutual KwRange
    kwr [Declaration]
    ds) = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (LoneConstructor KwRange
    kwr [Declaration]
    ds)= KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Abstract KwRange
    kwr [Declaration]
    ds)       = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Generalize KwRange
    kwr [Declaration]
    ds)     = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Open Range
    r QName
    _ ImportDirective
    _)            = Range
    r
      getRange (ModuleMacro Range
    r Erased
    _ Name
    _ ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _)
                                       = Range
    r
      getRange (Import Range
    r QName
    _ Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _)      = Range
    r
      getRange (InstanceB KwRange
    kwr [Declaration]
    _)       = KwRange -> Range
    forall a. HasRange a => a -> Range
    getRange KwRange
    kwr
      getRange (Macro KwRange
    kwr [Declaration]
    ds)          = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Private KwRange
    kwr Origin
    _ [Declaration]
    ds)      = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Postulate KwRange
    kwr [Declaration]
    ds)      = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Primitive KwRange
    kwr [Declaration]
    ds)      = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Module Range
    r Erased
    _ QName
    _ Telescope
    _ [Declaration]
    _)      = Range
    r
      getRange (Infix Fixity
    f List1 Name
    _)             = Fixity -> Range
    forall a. HasRange a => a -> Range
    getRange Fixity
    f
      getRange (Syntax Name
    n Notation
    _)            = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    n
      getRange (PatternSyn Range
    r Name
    _ [WithHiding Name]
    _ Pattern
    _)    = Range
    r
      getRange (UnquoteDecl Range
    r [Name]
    _ Expr
    _)     = Range
    r
      getRange (UnquoteDef Range
    r [Name]
    _ Expr
    _)      = Range
    r
      getRange (UnquoteData Range
    r Name
    _ [Name]
    _ Expr
    _)   = Range
    r
      getRange (Pragma Pragma
    p)              = Pragma -> Range
    forall a. HasRange a => a -> Range
    getRange Pragma
    p
      getRange (Opaque KwRange
    kwr [Declaration]
    ds)         = KwRange -> [Declaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [Declaration]
    ds
      getRange (Unfolding KwRange
    kwr [QName]
    ds)      = KwRange -> [QName] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [QName]
    ds

    instance HasRange LHS where
      getRange :: LHS -> Range
    getRange (LHS Pattern
    p [RewriteEqn]
    eqns [WithExpr]
    ws) = Pattern
    p Pattern -> [RewriteEqn] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [RewriteEqn]
    eqns Range -> [WithExpr] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [WithExpr]
    ws

    instance HasRange LHSCore where
      getRange :: LHSCore -> Range
    getRange (LHSHead QName
    f [NamedArg Pattern]
    ps)              = QName -> [NamedArg Pattern] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange QName
    f [NamedArg Pattern]
    ps
      getRange (LHSProj QName
    d [NamedArg Pattern]
    ps1 NamedArg LHSCore
    lhscore [NamedArg Pattern]
    ps2) = QName
    d QName -> [NamedArg Pattern] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [NamedArg Pattern]
    ps1 Range -> NamedArg LHSCore -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` NamedArg LHSCore
    lhscore Range -> [NamedArg Pattern] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [NamedArg Pattern]
    ps2
      getRange (LHSWith LHSCore
    f List1 Pattern
    wps [NamedArg Pattern]
    ps)          = LHSCore
    f LHSCore -> List1 Pattern -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` List1 Pattern
    wps Range -> [NamedArg Pattern] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    `fuseRange` [NamedArg Pattern]
    ps
      getRange (LHSEllipsis Range
    r LHSCore
    p)           = Range
    r

    instance HasRange RHS where
      getRange :: RHS -> Range
    getRange RHS
    AbsurdRHS = Range
    forall a. Range' a
    noRange
      getRange (RHS Expr
    e)   = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e

    instance HasRange LamClause where
      getRange :: LamClause -> Range
    getRange (LamClause [Pattern]
    lhs RHS
    rhs Catchall
    _) = ([Pattern], RHS) -> Range
    forall a. HasRange a => a -> Range
    getRange ([Pattern]
    lhs, RHS
    rhs)

    instance HasRange DoStmt where
      getRange :: DoStmt -> Range
    getRange (DoBind Range
    r Pattern
    _ Expr
    _ [LamClause]
    _) = Range
    r
      getRange (DoThen Expr
    e)       = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e
      getRange (DoLet Range
    r List1 Declaration
    _)      = Range
    r

    instance HasRange Pragma where
      getRange :: Pragma -> Range
    getRange (OptionsPragma Range
    r [String]
    _)               = Range
    r
      getRange (BuiltinPragma Range
    r Ranged String
    _ QName
    _)             = Range
    r
      getRange (RewritePragma Range
    r Range
    _ [QName]
    _)             = Range
    r
      getRange (CompilePragma Range
    r Ranged BackendName
    _ QName
    _ String
    _)           = Range
    r
      getRange (ForeignPragma Range
    r Ranged BackendName
    _ String
    _)             = Range
    r
      getRange (StaticPragma Range
    r QName
    _)                = Range
    r
      getRange (InjectivePragma Range
    r QName
    _)             = Range
    r
      getRange (InjectiveForInferencePragma Range
    r QName
    _) = Range
    r
      getRange (InlinePragma Range
    r Bool
    _ QName
    _)              = Range
    r
      getRange (ImpossiblePragma Range
    r [String]
    _)            = Range
    r
      getRange (EtaPragma Range
    r QName
    _)                   = Range
    r
      getRange (TerminationCheckPragma Range
    r TerminationCheck Name
    _)      = Range
    r
      getRange (NoCoverageCheckPragma Range
    r)         = Range
    r
      getRange (WarningOnUsage Range
    r QName
    _ BackendName
    _)            = Range
    r
      getRange (WarningOnImport Range
    r BackendName
    _)             = Range
    r
      getRange (CatchallPragma Range
    r)                = Range
    r
      getRange (DisplayPragma Range
    r Pattern
    _ Expr
    _)             = Range
    r
      getRange (NoPositivityCheckPragma Range
    r)       = Range
    r
      getRange (PolarityPragma Range
    r Name
    _ [Ranged Occurrence]
    _)            = Range
    r
      getRange (NoUniverseCheckPragma Range
    r)         = Range
    r
      getRange (NotProjectionLikePragma Range
    r QName
    _)     = Range
    r
      getRange (OverlapPragma Range
    r [QName]
    _ OverlapMode
    _)             = Range
    r

    instance HasRange AsName where
      getRange :: AsName -> Range
    getRange AsName
    a = (Range, Either Expr Name) -> Range
    forall a. HasRange a => a -> Range
    getRange (AsName -> Range
    forall a. AsName' a -> Range
    asRange AsName
    a, AsName -> Either Expr Name
    forall a. AsName' a -> a
    asName AsName
    a)

    instance HasRange Pattern where
      getRange :: Pattern -> Range
    getRange (IdentP Bool
    _ QName
    x)       = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x
      getRange (AppP Pattern
    p NamedArg Pattern
    q)         = Pattern -> NamedArg Pattern -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Pattern
    p NamedArg Pattern
    q
      getRange (OpAppP Range
    r QName
    _ Set1 Name
    _ List1 (NamedArg Pattern)
    _)   = Range
    r
      getRange (RawAppP Range
    r List2 Pattern
    _)      = Range
    r
      getRange (ParenP Range
    r Pattern
    _)       = Range
    r
      getRange (WildP Range
    r)          = Range
    r
      getRange (AsP Range
    r Name
    _ Pattern
    _)        = Range
    r
      getRange (AbsurdP Range
    r)        = Range
    r
      getRange (LitP Range
    r Literal
    _)         = Range
    r
      getRange (QuoteP Range
    r)         = Range
    r
      getRange (HiddenP Range
    r Named_ Pattern
    _)      = Range
    r
      getRange (InstanceP Range
    r Named_ Pattern
    _)    = Range
    r
      getRange (DotP KwRange
    _kwr Range
    r Expr
    _)    = Range
    r
      getRange (RecP KwRange
    _kwr Range
    r [FieldAssignment' Pattern]
    _)    = Range
    r
      getRange (EqualP Range
    r List1 (Expr, Expr)
    _)       = Range
    r
      getRange (EllipsisP Range
    r Maybe Pattern
    _)    = Range
    r
      getRange (WithP Range
    r Pattern
    _)        = Range
    r

    -- SetRange instances
    ------------------------------------------------------------------------

    instance SetRange Pattern where
      setRange :: Range -> Pattern -> Pattern
    setRange Range
    r (IdentP Bool
    c QName
    x)       = Bool -> QName -> Pattern
    IdentP Bool
    c (Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r QName
    x)
      setRange Range
    r (AppP Pattern
    p NamedArg Pattern
    q)         = Pattern -> NamedArg Pattern -> Pattern
    AppP (Range -> Pattern -> Pattern
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Pattern
    p) (Range -> NamedArg Pattern -> NamedArg Pattern
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r NamedArg Pattern
    q)
      setRange Range
    r (OpAppP Range
    _ QName
    x Set1 Name
    ns List1 (NamedArg Pattern)
    ps) = Range -> QName -> Set1 Name -> List1 (NamedArg Pattern) -> Pattern
    OpAppP Range
    r QName
    x Set1 Name
    ns List1 (NamedArg Pattern)
    ps
      setRange Range
    r (RawAppP Range
    _ List2 Pattern
    ps)     = Range -> List2 Pattern -> Pattern
    RawAppP Range
    r List2 Pattern
    ps
      setRange Range
    r (ParenP Range
    _ Pattern
    p)       = Range -> Pattern -> Pattern
    ParenP Range
    r Pattern
    p
      setRange Range
    r (WildP Range
    _)          = Range -> Pattern
    WildP Range
    r
      setRange Range
    r (AsP Range
    _ Name
    x Pattern
    p)        = Range -> Name -> Pattern -> Pattern
    AsP Range
    r (Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    x) Pattern
    p
      setRange Range
    r (AbsurdP Range
    _)        = Range -> Pattern
    AbsurdP Range
    r
      setRange Range
    r (LitP Range
    _ Literal
    l)         = Range -> Literal -> Pattern
    LitP Range
    r Literal
    l
      setRange Range
    r (QuoteP Range
    _)         = Range -> Pattern
    QuoteP Range
    r
      setRange Range
    r (HiddenP Range
    _ Named_ Pattern
    p)      = Range -> Named_ Pattern -> Pattern
    HiddenP Range
    r Named_ Pattern
    p
      setRange Range
    r (InstanceP Range
    _ Named_ Pattern
    p)    = Range -> Named_ Pattern -> Pattern
    InstanceP Range
    r Named_ Pattern
    p
      setRange Range
    r (DotP KwRange
    _ Range
    _ Expr
    e)       = KwRange -> Range -> Expr -> Pattern
    DotP KwRange
    forall a. Null a => a
    empty Range
    r Expr
    e
      setRange Range
    r (RecP KwRange
    _ Range
    _ [FieldAssignment' Pattern]
    fs)      = KwRange -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP KwRange
    forall a. Null a => a
    empty Range
    r [FieldAssignment' Pattern]
    fs
      setRange Range
    r (EqualP Range
    _ List1 (Expr, Expr)
    es)      = Range -> List1 (Expr, Expr) -> Pattern
    EqualP Range
    r List1 (Expr, Expr)
    es
      setRange Range
    r (EllipsisP Range
    _ Maybe Pattern
    mp)   = Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r Maybe Pattern
    mp
      setRange Range
    r (WithP Range
    _ Pattern
    p)        = Range -> Pattern -> Pattern
    WithP Range
    r Pattern
    p

    instance SetRange TypedBinding where
      setRange :: Range -> TypedBinding' Expr -> TypedBinding' Expr
    setRange Range
    r (TBind Range
    _ List1 (NamedArg Binder)
    xs Expr
    e) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    r List1 (NamedArg Binder)
    xs Expr
    e
      setRange Range
    r (TLet Range
    _ List1 Declaration
    ds)    = Range -> List1 Declaration -> TypedBinding' Expr
    forall e. Range -> List1 Declaration -> TypedBinding' e
    TLet Range
    r List1 Declaration
    ds

    -- KillRange instances
    ------------------------------------------------------------------------

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

    instance KillRange ModuleAssignment where
      killRange :: KillRangeT ModuleAssignment
    killRange (ModuleAssignment QName
    a [Expr]
    b ImportDirective
    c) = (QName -> [Expr] -> ImportDirective -> ModuleAssignment)
    -> QName -> [Expr] -> ImportDirective -> ModuleAssignment
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> [Expr] -> ImportDirective -> ModuleAssignment
    ModuleAssignment QName
    a [Expr]
    b ImportDirective
    c

    instance KillRange AsName where
      killRange :: KillRangeT AsName
    killRange (AsName Either Expr Name
    n Range
    _) = (Either Expr Name -> AsName) -> Either Expr Name -> AsName
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN ((Either Expr Name -> Range -> AsName)
    -> Range -> Either Expr Name -> AsName
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Either Expr Name -> Range -> AsName
    forall a. a -> Range -> AsName' a
    AsName Range
    forall a. Range' a
    noRange) Either Expr Name
    n

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

    instance KillRange BoundName where
      killRange :: KillRangeT BoundName
    killRange (BName Name
    n Fixity'
    f TacticAttribute
    t Bool
    b) = (Name -> Fixity' -> TacticAttribute -> Bool -> BoundName)
    -> Name -> Fixity' -> TacticAttribute -> Bool -> BoundName
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Name -> Fixity' -> TacticAttribute -> Bool -> BoundName
    BName Name
    n Fixity'
    f TacticAttribute
    t Bool
    b

    instance KillRange RecordDirective where
      killRange :: KillRangeT RecordDirective
    killRange (Induction Ranged Induction
    a)          = (Ranged Induction -> RecordDirective)
    -> Ranged Induction -> RecordDirective
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Ranged Induction -> RecordDirective
    Induction Ranged Induction
    a
      killRange (Eta Ranged HasEta0
    a    )            = (Ranged HasEta0 -> RecordDirective)
    -> Ranged HasEta0 -> RecordDirective
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Ranged HasEta0 -> RecordDirective
    Eta Ranged HasEta0
    a
      killRange (Constructor Name
    a IsInstance
    b)      = (Name -> IsInstance -> RecordDirective)
    -> Name -> IsInstance -> RecordDirective
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Name -> IsInstance -> RecordDirective
    Constructor Name
    a IsInstance
    b
      killRange (PatternOrCopattern Range
    _) = Range -> RecordDirective
    PatternOrCopattern Range
    forall a. Range' a
    noRange

    instance KillRange Declaration where
      killRange :: KillRangeT Declaration
    killRange (TypeSig ArgInfo
    i TacticAttribute
    t Name
    n Expr
    e)       = (TacticAttribute -> Name -> Expr -> Declaration)
    -> TacticAttribute -> Name -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    i) TacticAttribute
    t Name
    n Expr
    e
      killRange (FieldSig IsInstance
    i TacticAttribute
    t Name
    n Arg Expr
    e)      = (IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration)
    -> IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
    FieldSig IsInstance
    i TacticAttribute
    t Name
    n Arg Expr
    e
      killRange (Generalize KwRange
    r [Declaration]
    ds )      = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Generalize KwRange
    forall a. Null a => a
    empty) [Declaration]
    ds
      killRange (Field KwRange
    r [Declaration]
    fs)            = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Field KwRange
    forall a. Null a => a
    empty) [Declaration]
    fs
      killRange (FunClause LHS
    l RHS
    r WhereClause
    w Catchall
    ca)    = (LHS -> RHS -> WhereClause -> Catchall -> Declaration)
    -> LHS -> RHS -> WhereClause -> Catchall -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN LHS -> RHS -> WhereClause -> Catchall -> Declaration
    FunClause LHS
    l RHS
    r WhereClause
    w Catchall
    ca
      killRange (DataSig Range
    _ Erased
    er Name
    n [LamBinding]
    l Expr
    e)    = (Erased -> Name -> [LamBinding] -> Expr -> Declaration)
    -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    DataSig Range
    forall a. Range' a
    noRange) Erased
    er Name
    n [LamBinding]
    l Expr
    e
      killRange (Data Range
    _ Erased
    er Name
    n [LamBinding]
    l Expr
    e [Declaration]
    c)     = (Erased
     -> Name -> [LamBinding] -> Expr -> [Declaration] -> Declaration)
    -> Erased
    -> Name
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range
    -> Erased
    -> Name
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    Data Range
    forall a. Range' a
    noRange) Erased
    er Name
    n [LamBinding]
    l Expr
    e [Declaration]
    c
      killRange (DataDef Range
    _ Name
    n [LamBinding]
    l [Declaration]
    c)       = (Name -> [LamBinding] -> [Declaration] -> Declaration)
    -> Name -> [LamBinding] -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
    DataDef Range
    forall a. Range' a
    noRange) Name
    n [LamBinding]
    l [Declaration]
    c
      killRange (RecordSig Range
    _ Erased
    er Name
    n [LamBinding]
    l Expr
    e)  = (Erased -> Name -> [LamBinding] -> Expr -> Declaration)
    -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    RecordSig Range
    forall a. Range' a
    noRange) Erased
    er Name
    n [LamBinding]
    l Expr
    e
      killRange (RecordDef Range
    _ Name
    n [RecordDirective]
    dir [LamBinding]
    k [Declaration]
    d) = (Name
     -> [RecordDirective]
     -> [LamBinding]
     -> [Declaration]
     -> Declaration)
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> Declaration
    RecordDef Range
    forall a. Range' a
    noRange) Name
    n [RecordDirective]
    dir [LamBinding]
    k [Declaration]
    d
      killRange (Record Range
    _ Erased
    er Name
    n [RecordDirective]
    dir [LamBinding]
    k Expr
    e [Declaration]
    d)
                                        = (Erased
     -> Name
     -> [RecordDirective]
     -> [LamBinding]
     -> Expr
     -> [Declaration]
     -> Declaration)
    -> Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range
    -> Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    Record Range
    forall a. Range' a
    noRange) Erased
    er Name
    n [RecordDirective]
    dir [LamBinding]
    k Expr
    e [Declaration]
    d
      killRange (Infix Fixity
    f List1 Name
    n)             = (Fixity -> List1 Name -> Declaration)
    -> Fixity -> List1 Name -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Fixity -> List1 Name -> Declaration
    Infix Fixity
    f List1 Name
    n
      killRange (Syntax Name
    n Notation
    no)           = (Name -> Declaration) -> Name -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (\Name
    n -> Name -> Notation -> Declaration
    Syntax Name
    n Notation
    no) Name
    n
      killRange (PatternSyn Range
    _ Name
    n [WithHiding Name]
    ns Pattern
    p)   = (Name -> [WithHiding Name] -> Pattern -> Declaration)
    -> Name -> [WithHiding Name] -> Pattern -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Name -> [WithHiding Name] -> Pattern -> Declaration
    PatternSyn Range
    forall a. Range' a
    noRange) Name
    n [WithHiding Name]
    ns Pattern
    p
      killRange (Mutual KwRange
    _ [Declaration]
    d)            = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Mutual KwRange
    forall a. Null a => a
    empty) [Declaration]
    d
      killRange (InterleavedMutual KwRange
    _ [Declaration]
    d) = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    InterleavedMutual KwRange
    forall a. Null a => a
    empty) [Declaration]
    d
      killRange (LoneConstructor KwRange
    _ [Declaration]
    d)   = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    LoneConstructor KwRange
    forall a. Null a => a
    empty) [Declaration]
    d
      killRange (Abstract KwRange
    _ [Declaration]
    d)          = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Abstract KwRange
    forall a. Null a => a
    empty) [Declaration]
    d
      killRange (Private KwRange
    _ Origin
    o [Declaration]
    d)         = (Origin -> [Declaration] -> Declaration)
    -> Origin -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Origin -> [Declaration] -> Declaration
    Private KwRange
    forall a. Null a => a
    empty) Origin
    o [Declaration]
    d
      killRange (InstanceB KwRange
    _ [Declaration]
    d)         = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    InstanceB KwRange
    forall a. Null a => a
    empty) [Declaration]
    d
      killRange (Macro KwRange
    _ [Declaration]
    d)             = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Macro KwRange
    forall a. Null a => a
    empty) [Declaration]
    d
      killRange (Postulate KwRange
    _ [Declaration]
    t)         = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Postulate KwRange
    forall a. Null a => a
    empty) [Declaration]
    t
      killRange (Primitive KwRange
    _ [Declaration]
    t)         = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Primitive KwRange
    forall a. Null a => a
    empty) [Declaration]
    t
      killRange (Open Range
    _ QName
    q ImportDirective
    i)            = (QName -> ImportDirective -> Declaration)
    -> QName -> ImportDirective -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> ImportDirective -> Declaration
    Open Range
    forall a. Range' a
    noRange) QName
    q ImportDirective
    i
      killRange (Import Range
    _ QName
    q Maybe AsName
    a OpenShortHand
    o ImportDirective
    i)      = (QName -> Maybe AsName -> ImportDirective -> Declaration)
    -> QName -> Maybe AsName -> ImportDirective -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (\QName
    q Maybe AsName
    a -> Range
    -> QName
    -> Maybe AsName
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    Import Range
    forall a. Range' a
    noRange QName
    q Maybe AsName
    a OpenShortHand
    o) QName
    q Maybe AsName
    a ImportDirective
    i
      killRange (ModuleMacro Range
    _ Erased
    e Name
    n ModuleApplication
    m OpenShortHand
    o ImportDirective
    i)
                                        = (Erased
     -> Name -> ModuleApplication -> ImportDirective -> Declaration)
    -> Erased
    -> Name
    -> ModuleApplication
    -> ImportDirective
    -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN
                                            (\Erased
    e Name
    n ModuleApplication
    m -> Range
    -> Erased
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    ModuleMacro Range
    forall a. Range' a
    noRange Erased
    e Name
    n ModuleApplication
    m OpenShortHand
    o)
                                            Erased
    e Name
    n ModuleApplication
    m ImportDirective
    i
      killRange (Module Range
    _ Erased
    e QName
    q Telescope
    t [Declaration]
    d)      = (Erased -> QName -> Telescope -> [Declaration] -> Declaration)
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    forall a. Range' a
    noRange) Erased
    e QName
    q Telescope
    t [Declaration]
    d
      killRange (UnquoteDecl Range
    _ [Name]
    x Expr
    t)     = ([Name] -> Expr -> Declaration) -> [Name] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> [Name] -> Expr -> Declaration
    UnquoteDecl Range
    forall a. Range' a
    noRange) [Name]
    x Expr
    t
      killRange (UnquoteDef Range
    _ [Name]
    x Expr
    t)      = ([Name] -> Expr -> Declaration) -> [Name] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> [Name] -> Expr -> Declaration
    UnquoteDef Range
    forall a. Range' a
    noRange) [Name]
    x Expr
    t
      killRange (UnquoteData Range
    _ Name
    xs [Name]
    cs Expr
    t) = (Name -> [Name] -> Expr -> Declaration)
    -> Name -> [Name] -> Expr -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Name -> [Name] -> Expr -> Declaration
    UnquoteData Range
    forall a. Range' a
    noRange) Name
    xs [Name]
    cs Expr
    t
      killRange (Pragma Pragma
    p)              = (Pragma -> Declaration) -> Pragma -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Pragma -> Declaration
    Pragma Pragma
    p
      killRange (Opaque KwRange
    r [Declaration]
    xs)           = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [Declaration] -> Declaration
    Opaque KwRange
    forall a. Null a => a
    empty) [Declaration]
    xs
      killRange (Unfolding KwRange
    r [QName]
    xs)        = ([QName] -> Declaration) -> [QName] -> Declaration
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> [QName] -> Declaration
    Unfolding KwRange
    forall a. Null a => a
    empty) [QName]
    xs

    instance KillRange Expr where
      killRange :: Expr -> Expr
    killRange (Ident QName
    q)              = (QName -> Expr) -> QName -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> Expr
    Ident QName
    q
      killRange (Lit Range
    _ Literal
    l)              = (Literal -> Expr) -> Literal -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Literal -> Expr
    Lit Range
    forall a. Range' a
    noRange) Literal
    l
      killRange (QuestionMark Range
    _ Maybe Int
    n)     = Range -> Maybe Int -> Expr
    QuestionMark Range
    forall a. Range' a
    noRange Maybe Int
    n
      killRange (Underscore Range
    _ Maybe String
    n)       = Range -> Maybe String -> Expr
    Underscore Range
    forall a. Range' a
    noRange Maybe String
    n
      killRange (RawApp Range
    _ List2 Expr
    e)           = (List2 Expr -> Expr) -> List2 Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List2 Expr -> Expr
    RawApp Range
    forall a. Range' a
    noRange) List2 Expr
    e
      killRange (App Range
    _ Expr
    e NamedArg Expr
    a)            = (Expr -> NamedArg Expr -> Expr) -> Expr -> NamedArg Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Expr -> NamedArg Expr -> Expr
    App Range
    forall a. Range' a
    noRange) Expr
    e NamedArg Expr
    a
      killRange (OpApp Range
    _ QName
    n Set1 Name
    ns OpAppArgs
    o)       = (QName -> Set1 Name -> OpAppArgs -> Expr)
    -> QName -> Set1 Name -> OpAppArgs -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> Set1 Name -> OpAppArgs -> Expr
    OpApp Range
    forall a. Range' a
    noRange) QName
    n Set1 Name
    ns OpAppArgs
    o
      killRange (WithApp Range
    _ Expr
    e List1 Expr
    es)       = (Expr -> List1 Expr -> Expr) -> Expr -> List1 Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Expr -> List1 Expr -> Expr
    WithApp Range
    forall a. Range' a
    noRange) Expr
    e List1 Expr
    es
      killRange (HiddenArg Range
    _ Named NamedName Expr
    n)        = (Named NamedName Expr -> Expr) -> Named NamedName Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Named NamedName Expr -> Expr
    HiddenArg Range
    forall a. Range' a
    noRange) Named NamedName Expr
    n
      killRange (InstanceArg Range
    _ Named NamedName Expr
    n)      = (Named NamedName Expr -> Expr) -> Named NamedName Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Named NamedName Expr -> Expr
    InstanceArg Range
    forall a. Range' a
    noRange) Named NamedName Expr
    n
      killRange (Lam Range
    _ List1 LamBinding
    l Expr
    e)            = (List1 LamBinding -> Expr -> Expr)
    -> List1 LamBinding -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List1 LamBinding -> Expr -> Expr
    Lam Range
    forall a. Range' a
    noRange) List1 LamBinding
    l Expr
    e
      killRange (AbsurdLam Range
    _ Hiding
    h)        = (Hiding -> Expr) -> Hiding -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Hiding -> Expr
    AbsurdLam Range
    forall a. Range' a
    noRange) Hiding
    h
      killRange (ExtendedLam Range
    _ Erased
    e List1 LamClause
    lrw)  = (Erased -> List1 LamClause -> Expr)
    -> Erased -> List1 LamClause -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Erased -> List1 LamClause -> Expr
    ExtendedLam Range
    forall a. Range' a
    noRange) Erased
    e List1 LamClause
    lrw
      killRange (Fun Range
    _ Arg Expr
    e1 Expr
    e2)          = (Arg Expr -> Expr -> Expr) -> Arg Expr -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Arg Expr -> Expr -> Expr
    Fun Range
    forall a. Range' a
    noRange) Arg Expr
    e1 Expr
    e2
      killRange (Pi Telescope1
    t Expr
    e)               = (Telescope1 -> Expr -> Expr) -> Telescope1 -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Telescope1 -> Expr -> Expr
    Pi Telescope1
    t Expr
    e
      killRange (Rec KwRange
    _ Range
    _ RecordAssignments
    ne)           = (RecordAssignments -> Expr) -> RecordAssignments -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Range -> RecordAssignments -> Expr
    Rec KwRange
    forall a. Null a => a
    empty Range
    forall a. Range' a
    noRange) RecordAssignments
    ne
      killRange (RecUpdate KwRange
    _ Range
    _ Expr
    e [FieldAssignment]
    ne)   = (Expr -> [FieldAssignment] -> Expr)
    -> Expr -> [FieldAssignment] -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Range -> Expr -> [FieldAssignment] -> Expr
    RecUpdate KwRange
    forall a. Null a => a
    empty Range
    forall a. Range' a
    noRange) Expr
    e [FieldAssignment]
    ne
      killRange (Let Range
    _ List1 Declaration
    d Maybe Expr
    e)            = (List1 Declaration -> Maybe Expr -> Expr)
    -> List1 Declaration -> Maybe Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List1 Declaration -> Maybe Expr -> Expr
    Let Range
    forall a. Range' a
    noRange) List1 Declaration
    d Maybe Expr
    e
      killRange (Paren Range
    _ Expr
    e)            = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Expr -> Expr
    Paren Range
    forall a. Range' a
    noRange) Expr
    e
      killRange (IdiomBrackets Range
    _ [Expr]
    es)   = ([Expr] -> Expr) -> [Expr] -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> [Expr] -> Expr
    IdiomBrackets Range
    forall a. Range' a
    noRange) [Expr]
    es
      killRange (DoBlock Range
    _ List1 DoStmt
    ss)         = (List1 DoStmt -> Expr) -> List1 DoStmt -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List1 DoStmt -> Expr
    DoBlock Range
    forall a. Range' a
    noRange) List1 DoStmt
    ss
      killRange (Absurd Range
    _)             = Range -> Expr
    Absurd Range
    forall a. Range' a
    noRange
      killRange (As Range
    _ Name
    n Expr
    e)             = (Name -> Expr -> Expr) -> Name -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Name -> Expr -> Expr
    As Range
    forall a. Range' a
    noRange) Name
    n Expr
    e
      killRange (Dot KwRange
    _ Expr
    e)              = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Expr -> Expr
    Dot KwRange
    forall a. Null a => a
    empty) Expr
    e
      killRange (DoubleDot KwRange
    _ Expr
    e)        = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Expr -> Expr
    DoubleDot KwRange
    forall a. Null a => a
    empty) Expr
    e
      killRange (Quote Range
    _)              = Range -> Expr
    Quote Range
    forall a. Range' a
    noRange
      killRange (QuoteTerm Range
    _)          = Range -> Expr
    QuoteTerm Range
    forall a. Range' a
    noRange
      killRange (Unquote Range
    _)            = Range -> Expr
    Unquote Range
    forall a. Range' a
    noRange
      killRange (Tactic Range
    _ Expr
    t)           = (Expr -> Expr) -> Expr -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Expr -> Expr
    Tactic Range
    forall a. Range' a
    noRange) Expr
    t
      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 (Equal Range
    _ Expr
    x Expr
    y)          = Range -> Expr -> Expr -> Expr
    Equal Range
    forall a. Range' a
    noRange Expr
    x Expr
    y
      killRange (Ellipsis Range
    _)           = Range -> Expr
    Ellipsis Range
    forall a. Range' a
    noRange
      killRange (Generalized 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
    Generalized Expr
    e
      killRange (KnownIdent NameKind
    a QName
    b)       = (QName -> Expr) -> QName -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (NameKind -> QName -> Expr
    KnownIdent NameKind
    a) QName
    b
      killRange (KnownOpApp NameKind
    a Range
    b QName
    c Set1 Name
    d OpAppArgs
    e) = (Range -> QName -> Set1 Name -> OpAppArgs -> Expr)
    -> Range -> QName -> Set1 Name -> OpAppArgs -> Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (NameKind -> Range -> QName -> Set1 Name -> OpAppArgs -> Expr
    KnownOpApp NameKind
    a) Range
    b QName
    c Set1 Name
    d OpAppArgs
    e

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

    instance KillRange LHS where
      killRange :: KillRangeT LHS
    killRange (LHS Pattern
    p [RewriteEqn]
    r [WithExpr]
    w)  = (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS)
    -> Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
    LHS Pattern
    p [RewriteEqn]
    r [WithExpr]
    w

    instance KillRange LamClause where
      killRange :: KillRangeT LamClause
    killRange (LamClause [Pattern]
    a RHS
    b Catchall
    c) = ([Pattern] -> RHS -> Catchall -> LamClause)
    -> [Pattern] -> RHS -> Catchall -> LamClause
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [Pattern] -> RHS -> Catchall -> LamClause
    LamClause [Pattern]
    a RHS
    b Catchall
    c

    instance KillRange DoStmt where
      killRange :: KillRangeT DoStmt
    killRange (DoBind Range
    r Pattern
    p Expr
    e [LamClause]
    w) = (Range -> Pattern -> Expr -> [LamClause] -> DoStmt)
    -> Range -> Pattern -> Expr -> [LamClause] -> DoStmt
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range -> Pattern -> Expr -> [LamClause] -> DoStmt
    DoBind Range
    r Pattern
    p Expr
    e [LamClause]
    w
      killRange (DoThen Expr
    e)       = (Expr -> DoStmt) -> Expr -> DoStmt
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Expr -> DoStmt
    DoThen Expr
    e
      killRange (DoLet Range
    r List1 Declaration
    ds)     = (Range -> List1 Declaration -> DoStmt)
    -> Range -> List1 Declaration -> DoStmt
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range -> List1 Declaration -> DoStmt
    DoLet Range
    r List1 Declaration
    ds

    instance KillRange ModuleApplication where
      killRange :: KillRangeT ModuleApplication
    killRange (SectionApp Range
    _ Telescope
    t QName
    x [Expr]
    es)      = (Telescope -> QName -> [Expr] -> ModuleApplication)
    -> Telescope -> QName -> [Expr] -> ModuleApplication
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Telescope -> QName -> [Expr] -> ModuleApplication
    SectionApp Range
    forall a. Range' a
    noRange) Telescope
    t QName
    x [Expr]
    es
      killRange (RecordModuleInstance Range
    _ QName
    q) = (QName -> ModuleApplication) -> QName -> ModuleApplication
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> ModuleApplication
    RecordModuleInstance Range
    forall a. Range' a
    noRange) QName
    q

    instance KillRange e => KillRange (OpApp e) where
      killRange :: KillRangeT (OpApp e)
    killRange (SyntaxBindingLambda Range
    _ List1 LamBinding
    l e
    e) = (List1 LamBinding -> e -> OpApp e)
    -> List1 LamBinding -> e -> OpApp e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List1 LamBinding -> e -> OpApp e
    forall e. Range -> List1 LamBinding -> e -> OpApp e
    SyntaxBindingLambda Range
    forall a. Range' a
    noRange) List1 LamBinding
    l e
    e
      killRange (Ordinary e
    e)                = (e -> OpApp e) -> e -> OpApp e
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN e -> OpApp e
    forall e. e -> OpApp e
    Ordinary e
    e

    instance KillRange Pattern where
      killRange :: Pattern -> Pattern
    killRange (IdentP Bool
    c QName
    q)      = (Bool -> QName -> Pattern) -> Bool -> QName -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Bool -> QName -> Pattern
    IdentP Bool
    c QName
    q
      killRange (AppP Pattern
    p NamedArg Pattern
    ps)       = (Pattern -> NamedArg Pattern -> Pattern)
    -> Pattern -> NamedArg Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Pattern -> NamedArg Pattern -> Pattern
    AppP Pattern
    p NamedArg Pattern
    ps
      killRange (RawAppP Range
    _ List2 Pattern
    p)     = (List2 Pattern -> Pattern) -> List2 Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List2 Pattern -> Pattern
    RawAppP Range
    forall a. Range' a
    noRange) List2 Pattern
    p
      killRange (OpAppP Range
    _ QName
    n Set1 Name
    ns List1 (NamedArg Pattern)
    p) = (QName -> Set1 Name -> List1 (NamedArg Pattern) -> Pattern)
    -> QName -> Set1 Name -> List1 (NamedArg Pattern) -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> Set1 Name -> List1 (NamedArg Pattern) -> Pattern
    OpAppP Range
    forall a. Range' a
    noRange) QName
    n Set1 Name
    ns List1 (NamedArg Pattern)
    p
      killRange (HiddenP Range
    _ Named_ Pattern
    n)     = (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Named_ Pattern -> Pattern
    HiddenP Range
    forall a. Range' a
    noRange) Named_ Pattern
    n
      killRange (InstanceP Range
    _ Named_ Pattern
    n)   = (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Named_ Pattern -> Pattern
    InstanceP Range
    forall a. Range' a
    noRange) Named_ Pattern
    n
      killRange (ParenP Range
    _ Pattern
    p)      = (Pattern -> Pattern) -> Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Pattern -> Pattern
    ParenP Range
    forall a. Range' a
    noRange) Pattern
    p
      killRange (WildP Range
    _)         = Range -> Pattern
    WildP Range
    forall a. Range' a
    noRange
      killRange (AbsurdP Range
    _)       = Range -> Pattern
    AbsurdP Range
    forall a. Range' a
    noRange
      killRange (AsP Range
    _ Name
    n Pattern
    p)       = (Name -> Pattern -> Pattern) -> Name -> Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Name -> Pattern -> Pattern
    AsP Range
    forall a. Range' a
    noRange) Name
    n Pattern
    p
      killRange (DotP KwRange
    _ Range
    _ Expr
    e)      = (Expr -> Pattern) -> Expr -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Range -> Expr -> Pattern
    DotP KwRange
    forall a. Null a => a
    empty Range
    forall a. Range' a
    noRange) Expr
    e
      killRange (LitP Range
    _ Literal
    l)        = (Literal -> Pattern) -> Literal -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Literal -> Pattern
    LitP Range
    forall a. Range' a
    noRange) Literal
    l
      killRange (QuoteP Range
    _)        = Range -> Pattern
    QuoteP Range
    forall a. Range' a
    noRange
      killRange (RecP KwRange
    _ Range
    _ [FieldAssignment' Pattern]
    fs)     = ([FieldAssignment' Pattern] -> Pattern)
    -> [FieldAssignment' Pattern] -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (KwRange -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP KwRange
    forall a. Null a => a
    empty Range
    forall a. Range' a
    noRange) [FieldAssignment' Pattern]
    fs
      killRange (EqualP Range
    _ List1 (Expr, Expr)
    es)     = (List1 (Expr, Expr) -> Pattern) -> List1 (Expr, Expr) -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List1 (Expr, Expr) -> Pattern
    EqualP Range
    forall a. Range' a
    noRange) List1 (Expr, Expr)
    es
      killRange (EllipsisP Range
    _ Maybe Pattern
    mp)  = (Maybe Pattern -> Pattern) -> Maybe Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    forall a. Range' a
    noRange) Maybe Pattern
    mp
      killRange (WithP Range
    _ Pattern
    p)       = (Pattern -> Pattern) -> Pattern -> Pattern
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Pattern -> Pattern
    WithP Range
    forall a. Range' a
    noRange) Pattern
    p

    instance KillRange Pragma where
      killRange :: KillRangeT Pragma
    killRange (OptionsPragma Range
    _ [String]
    s)               = Range -> [String] -> Pragma
    OptionsPragma Range
    forall a. Range' a
    noRange [String]
    s
      killRange (BuiltinPragma Range
    _ Ranged String
    s QName
    e)             = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Ranged String -> QName -> Pragma
    BuiltinPragma Range
    forall a. Range' a
    noRange Ranged String
    s) QName
    e
      killRange (RewritePragma Range
    _ Range
    _ [QName]
    qs)            = ([QName] -> Pragma) -> [QName] -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Range -> [QName] -> Pragma
    RewritePragma Range
    forall a. Range' a
    noRange Range
    forall a. Range' a
    noRange) [QName]
    qs
      killRange (StaticPragma Range
    _ QName
    q)                = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> Pragma
    StaticPragma Range
    forall a. Range' a
    noRange) QName
    q
      killRange (InjectivePragma Range
    _ QName
    q)             = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> Pragma
    InjectivePragma Range
    forall a. Range' a
    noRange) QName
    q
      killRange (InjectiveForInferencePragma Range
    _ QName
    q) = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> Pragma
    InjectiveForInferencePragma Range
    forall a. Range' a
    noRange) QName
    q
      killRange (InlinePragma Range
    _ Bool
    b QName
    q)              = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Bool -> QName -> Pragma
    InlinePragma Range
    forall a. Range' a
    noRange Bool
    b) QName
    q
      killRange (CompilePragma Range
    _ Ranged BackendName
    b QName
    q String
    s)           = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (\ QName
    q -> Range -> Ranged BackendName -> QName -> String -> Pragma
    CompilePragma Range
    forall a. Range' a
    noRange Ranged BackendName
    b QName
    q String
    s) QName
    q
      killRange (ForeignPragma Range
    _ Ranged BackendName
    b String
    s)             = Range -> Ranged BackendName -> String -> Pragma
    ForeignPragma Range
    forall a. Range' a
    noRange Ranged BackendName
    b String
    s
      killRange (ImpossiblePragma Range
    _ [String]
    strs)         = Range -> [String] -> Pragma
    ImpossiblePragma Range
    forall a. Range' a
    noRange [String]
    strs
      killRange (TerminationCheckPragma Range
    _ TerminationCheck Name
    t)      = Range -> TerminationCheck Name -> Pragma
    TerminationCheckPragma Range
    forall a. Range' a
    noRange (KillRangeT (TerminationCheck Name)
    forall a. KillRange a => KillRangeT a
    killRange TerminationCheck Name
    t)
      killRange (NoCoverageCheckPragma Range
    _)         = Range -> Pragma
    NoCoverageCheckPragma Range
    forall a. Range' a
    noRange
      killRange (WarningOnUsage Range
    _ QName
    nm BackendName
    str)         = Range -> QName -> BackendName -> Pragma
    WarningOnUsage Range
    forall a. Range' a
    noRange (QName -> QName
    forall a. KillRange a => KillRangeT a
    killRange QName
    nm) BackendName
    str
      killRange (WarningOnImport Range
    _ BackendName
    str)           = Range -> BackendName -> Pragma
    WarningOnImport Range
    forall a. Range' a
    noRange BackendName
    str
      killRange (CatchallPragma Range
    _)                = Range -> Pragma
    CatchallPragma Range
    forall a. Range' a
    noRange
      killRange (DisplayPragma Range
    _ Pattern
    lhs Expr
    rhs)         = (Pattern -> Expr -> Pragma) -> Pattern -> Expr -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Pattern -> Expr -> Pragma
    DisplayPragma Range
    forall a. Range' a
    noRange) Pattern
    lhs Expr
    rhs
      killRange (EtaPragma Range
    _ QName
    q)                   = (QName -> Pragma) -> QName -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> QName -> Pragma
    EtaPragma Range
    forall a. Range' a
    noRange) QName
    q
      killRange (NoPositivityCheckPragma Range
    _)       = Range -> Pragma
    NoPositivityCheckPragma Range
    forall a. Range' a
    noRange
      killRange (PolarityPragma Range
    _ Name
    q [Ranged Occurrence]
    occs)         = (Name -> Pragma) -> Name -> Pragma
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (\Name
    q -> Range -> Name -> [Ranged Occurrence] -> Pragma
    PolarityPragma Range
    forall a. Range' a
    noRange Name
    q [Ranged Occurrence]
    occs) Name
    q
      killRange (NoUniverseCheckPragma Range
    _)         = Range -> Pragma
    NoUniverseCheckPragma Range
    forall a. Range' a
    noRange
      killRange (NotProjectionLikePragma Range
    _ QName
    q)     = Range -> QName -> Pragma
    NotProjectionLikePragma Range
    forall a. Range' a
    noRange QName
    q
      killRange (OverlapPragma Range
    _ [QName]
    q OverlapMode
    i)             = Range -> [QName] -> OverlapMode -> Pragma
    OverlapPragma Range
    forall a. Range' a
    noRange [QName]
    q OverlapMode
    i

    instance KillRange RHS where
      killRange :: KillRangeT RHS
    killRange RHS
    AbsurdRHS = RHS
    forall e. RHS' e
    AbsurdRHS
      killRange (RHS Expr
    e)   = (Expr -> RHS) -> Expr -> RHS
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Expr -> RHS
    forall e. e -> RHS' e
    RHS Expr
    e

    instance KillRange TypedBinding where
      killRange :: TypedBinding' Expr -> TypedBinding' Expr
    killRange (TBind Range
    _ List1 (NamedArg Binder)
    b Expr
    e) = (List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr)
    -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    forall a. Range' a
    noRange) List1 (NamedArg Binder)
    b Expr
    e
      killRange (TLet Range
    r List1 Declaration
    ds)   = (Range -> List1 Declaration -> TypedBinding' Expr)
    -> Range -> List1 Declaration -> TypedBinding' Expr
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Range -> List1 Declaration -> TypedBinding' Expr
    forall e. Range -> List1 Declaration -> TypedBinding' e
    TLet Range
    r List1 Declaration
    ds

    instance KillRange WhereClause where
      killRange :: KillRangeT WhereClause
    killRange WhereClause
    NoWhere               = WhereClause
    forall a. WhereClause' a
    NoWhere
      killRange (AnyWhere Range
    r [Declaration]
    d)        = ([Declaration] -> WhereClause) -> [Declaration] -> WhereClause
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> [Declaration] -> WhereClause
    forall decls. Range -> decls -> WhereClause' decls
    AnyWhere Range
    forall a. Range' a
    noRange) [Declaration]
    d
      killRange (SomeWhere Range
    r Erased
    e Name
    n Access
    a [Declaration]
    d) =
        (Erased -> Name -> Access -> [Declaration] -> WhereClause)
    -> Erased -> Name -> Access -> [Declaration] -> WhereClause
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
    forall decls.
    Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
    SomeWhere Range
    forall a. Range' a
    noRange) Erased
    e Name
    n Access
    a [Declaration]
    d

    ------------------------------------------------------------------------
    -- NFData instances

    -- | Ranges are not forced.

    instance NFData Expr where
      rnf :: Expr -> ()
    rnf (Ident QName
    a)           = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a
      rnf (Lit Range
    _ Literal
    a)           = Literal -> ()
    forall a. NFData a => a -> ()
    rnf Literal
    a
      rnf (QuestionMark Range
    _ Maybe Int
    a)  = Maybe Int -> ()
    forall a. NFData a => a -> ()
    rnf Maybe Int
    a
      rnf (Underscore Range
    _ Maybe String
    a)    = Maybe String -> ()
    forall a. NFData a => a -> ()
    rnf Maybe String
    a
      rnf (RawApp Range
    _ List2 Expr
    a)        = List2 Expr -> ()
    forall a. NFData a => a -> ()
    rnf List2 Expr
    a
      rnf (App Range
    _ Expr
    a NamedArg Expr
    b)         = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` NamedArg Expr -> ()
    forall a. NFData a => a -> ()
    rnf NamedArg Expr
    b
      rnf (OpApp Range
    _ QName
    a Set1 Name
    b OpAppArgs
    c)     = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Set1 Name -> ()
    forall a. NFData a => a -> ()
    rnf Set1 Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` OpAppArgs -> ()
    forall a. NFData a => a -> ()
    rnf OpAppArgs
    c
      rnf (WithApp Range
    _ Expr
    a List1 Expr
    b)     = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` List1 Expr -> ()
    forall a. NFData a => a -> ()
    rnf List1 Expr
    b
      rnf (HiddenArg Range
    _ Named NamedName Expr
    a)     = Named NamedName Expr -> ()
    forall a. NFData a => a -> ()
    rnf Named NamedName Expr
    a
      rnf (InstanceArg Range
    _ Named NamedName Expr
    a)   = Named NamedName Expr -> ()
    forall a. NFData a => a -> ()
    rnf Named NamedName Expr
    a
      rnf (Lam Range
    _ List1 LamBinding
    a Expr
    b)         = List1 LamBinding -> ()
    forall a. NFData a => a -> ()
    rnf List1 LamBinding
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (AbsurdLam Range
    _ Hiding
    a)     = Hiding -> ()
    forall a. NFData a => a -> ()
    rnf Hiding
    a
      rnf (ExtendedLam Range
    _ Erased
    a List1 LamClause
    b) = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` List1 LamClause -> ()
    forall a. NFData a => a -> ()
    rnf List1 LamClause
    b
      rnf (Fun Range
    _ Arg Expr
    a Expr
    b)         = Arg Expr -> ()
    forall a. NFData a => a -> ()
    rnf Arg Expr
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (Pi Telescope1
    a Expr
    b)            = Telescope1 -> ()
    forall a. NFData a => a -> ()
    rnf Telescope1
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (Rec KwRange
    _ Range
    _ RecordAssignments
    a)         = RecordAssignments -> ()
    forall a. NFData a => a -> ()
    rnf RecordAssignments
    a
      rnf (RecUpdate KwRange
    _ Range
    _ Expr
    a [FieldAssignment]
    b) = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [FieldAssignment] -> ()
    forall a. NFData a => a -> ()
    rnf [FieldAssignment]
    b
      rnf (Let Range
    _ List1 Declaration
    a Maybe Expr
    b)         = List1 Declaration -> ()
    forall a. NFData a => a -> ()
    rnf List1 Declaration
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe Expr -> ()
    forall a. NFData a => a -> ()
    rnf Maybe Expr
    b
      rnf (Paren Range
    _ Expr
    a)         = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a
      rnf (IdiomBrackets Range
    _ [Expr]
    a) = [Expr] -> ()
    forall a. NFData a => a -> ()
    rnf [Expr]
    a
      rnf (DoBlock Range
    _ List1 DoStmt
    a)       = List1 DoStmt -> ()
    forall a. NFData a => a -> ()
    rnf List1 DoStmt
    a
      rnf (Absurd Range
    _)          = ()
      rnf (As Range
    _ Name
    a Expr
    b)          = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (Dot KwRange
    _ Expr
    a)           = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a
      rnf (DoubleDot KwRange
    _ Expr
    a)     = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a
      rnf (Quote Range
    _)           = ()
      rnf (QuoteTerm Range
    _)       = ()
      rnf (Tactic Range
    _ Expr
    a)        = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a
      rnf (Unquote Range
    _)         = ()
      rnf (DontCare Expr
    a)        = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a
      rnf (Equal Range
    _ Expr
    a Expr
    b)       = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (Ellipsis Range
    _)        = ()
      rnf (Generalized Expr
    e)     = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    e
      rnf (KnownIdent NameKind
    a QName
    b)    = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    b
      rnf (KnownOpApp NameKind
    a Range
    b QName
    c Set1 Name
    d OpAppArgs
    e) = NameKind -> ()
    forall a. NFData a => a -> ()
    rnf NameKind
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Range -> ()
    forall a. NFData a => a -> ()
    rnf Range
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Set1 Name -> ()
    forall a. NFData a => a -> ()
    rnf Set1 Name
    d () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    c

    -- | Ranges are not forced.

    instance NFData Pattern where
      rnf :: Pattern -> ()
    rnf (IdentP Bool
    a QName
    b)     = Bool -> ()
    forall a. NFData a => a -> ()
    rnf Bool
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    b
      rnf (QuoteP Range
    _)       = ()
      rnf (AppP Pattern
    a NamedArg Pattern
    b)       = Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` NamedArg Pattern -> ()
    forall a. NFData a => a -> ()
    rnf NamedArg Pattern
    b
      rnf (RawAppP Range
    _ List2 Pattern
    a)    = List2 Pattern -> ()
    forall a. NFData a => a -> ()
    rnf List2 Pattern
    a
      rnf (OpAppP Range
    _ QName
    a Set1 Name
    b List1 (NamedArg Pattern)
    c) = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Set1 Name -> ()
    forall a. NFData a => a -> ()
    rnf Set1 Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` List1 (NamedArg Pattern) -> ()
    forall a. NFData a => a -> ()
    rnf List1 (NamedArg Pattern)
    c
      rnf (HiddenP Range
    _ Named_ Pattern
    a)    = Named_ Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Named_ Pattern
    a
      rnf (InstanceP Range
    _ Named_ Pattern
    a)  = Named_ Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Named_ Pattern
    a
      rnf (ParenP Range
    _ Pattern
    a)     = Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    a
      rnf (WildP Range
    _)        = ()
      rnf (AbsurdP Range
    _)      = ()
      rnf (AsP Range
    _ Name
    a Pattern
    b)      = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    b
      rnf (DotP KwRange
    _ Range
    _ Expr
    a)     = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    a
      rnf (LitP Range
    _ Literal
    a)       = Literal -> ()
    forall a. NFData a => a -> ()
    rnf Literal
    a
      rnf (RecP KwRange
    _ Range
    _ [FieldAssignment' Pattern]
    a)     = [FieldAssignment' Pattern] -> ()
    forall a. NFData a => a -> ()
    rnf [FieldAssignment' Pattern]
    a
      rnf (EqualP Range
    _ List1 (Expr, Expr)
    es)    = List1 (Expr, Expr) -> ()
    forall a. NFData a => a -> ()
    rnf List1 (Expr, Expr)
    es
      rnf (EllipsisP Range
    _ Maybe Pattern
    mp) = Maybe Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Maybe Pattern
    mp
      rnf (WithP Range
    _ Pattern
    a)      = Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    a

    -- | Ranges are not forced.

    instance NFData RecordDirective where
      rnf :: RecordDirective -> ()
    rnf (Induction Ranged Induction
    a)          = Ranged Induction -> ()
    forall a. NFData a => a -> ()
    rnf Ranged Induction
    a
      rnf (Eta Ranged HasEta0
    a    )            = Ranged HasEta0 -> ()
    forall a. NFData a => a -> ()
    rnf Ranged HasEta0
    a
      rnf (Constructor Name
    a IsInstance
    b)      = (Name, IsInstance) -> ()
    forall a. NFData a => a -> ()
    rnf (Name
    a, IsInstance
    b)
      rnf (PatternOrCopattern Range
    _) = ()

    instance NFData Declaration where
      rnf :: Declaration -> ()
    rnf (TypeSig ArgInfo
    a TacticAttribute
    b Name
    c Expr
    d)       = ArgInfo -> ()
    forall a. NFData a => a -> ()
    rnf ArgInfo
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` TacticAttribute -> ()
    forall a. NFData a => a -> ()
    rnf TacticAttribute
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    d
      rnf (FieldSig IsInstance
    a TacticAttribute
    b Name
    c Arg Expr
    d)      = IsInstance -> ()
    forall a. NFData a => a -> ()
    rnf IsInstance
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` TacticAttribute -> ()
    forall a. NFData a => a -> ()
    rnf TacticAttribute
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Arg Expr -> ()
    forall a. NFData a => a -> ()
    rnf Arg Expr
    d
      rnf (Generalize KwRange
    _ [Declaration]
    a)        = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Field KwRange
    _ [Declaration]
    fs)            = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    fs
      rnf (FunClause LHS
    a RHS
    b WhereClause
    c Catchall
    d)     = LHS -> ()
    forall a. NFData a => a -> ()
    rnf LHS
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` RHS -> ()
    forall a. NFData a => a -> ()
    rnf RHS
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` WhereClause -> ()
    forall a. NFData a => a -> ()
    rnf WhereClause
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Catchall -> ()
    forall a. NFData a => a -> ()
    rnf Catchall
    d
      rnf (DataSig Range
    _ Erased
    a Name
    b [LamBinding]
    c Expr
    d)     = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [LamBinding] -> ()
    forall a. NFData a => a -> ()
    rnf [LamBinding]
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    d
      rnf (Data Range
    _ Erased
    a Name
    b [LamBinding]
    c Expr
    d [Declaration]
    e)      = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [LamBinding] -> ()
    forall a. NFData a => a -> ()
    rnf [LamBinding]
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    d
                                          () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    e
      rnf (DataDef Range
    _ Name
    a [LamBinding]
    b [Declaration]
    c)       = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [LamBinding] -> ()
    forall a. NFData a => a -> ()
    rnf [LamBinding]
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    c
      rnf (RecordSig Range
    _ Erased
    a Name
    b [LamBinding]
    c Expr
    d)   = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [LamBinding] -> ()
    forall a. NFData a => a -> ()
    rnf [LamBinding]
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    d
      rnf (RecordDef Range
    _ Name
    a [RecordDirective]
    b [LamBinding]
    c [Declaration]
    d)   = (Name, [RecordDirective], [LamBinding], [Declaration]) -> ()
    forall a. NFData a => a -> ()
    rnf (Name
    a, [RecordDirective]
    b, [LamBinding]
    c, [Declaration]
    d)
      rnf (Record Range
    _ Erased
    a Name
    b [RecordDirective]
    c [LamBinding]
    d Expr
    e [Declaration]
    f)  = (Erased, Name, [RecordDirective], [LamBinding], Expr,
     [Declaration])
    -> ()
    forall a. NFData a => a -> ()
    rnf (Erased
    a, Name
    b, [RecordDirective]
    c, [LamBinding]
    d, Expr
    e, [Declaration]
    f)
      rnf (Infix Fixity
    a List1 Name
    b)             = Fixity -> ()
    forall a. NFData a => a -> ()
    rnf Fixity
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` List1 Name -> ()
    forall a. NFData a => a -> ()
    rnf List1 Name
    b
      rnf (Syntax Name
    a Notation
    b)            = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Notation -> ()
    forall a. NFData a => a -> ()
    rnf Notation
    b
      rnf (PatternSyn Range
    _ Name
    a [WithHiding Name]
    b Pattern
    c)    = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [WithHiding Name] -> ()
    forall a. NFData a => a -> ()
    rnf [WithHiding Name]
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    c
      rnf (Mutual KwRange
    _ [Declaration]
    a)            = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (InterleavedMutual KwRange
    _ [Declaration]
    a) = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (LoneConstructor KwRange
    _ [Declaration]
    a)   = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Abstract KwRange
    _ [Declaration]
    a)          = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Private KwRange
    _ Origin
    _ [Declaration]
    a)         = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (InstanceB KwRange
    _ [Declaration]
    a)         = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Macro KwRange
    _ [Declaration]
    a)             = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Postulate KwRange
    _ [Declaration]
    a)         = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Primitive KwRange
    _ [Declaration]
    a)         = [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    a
      rnf (Open Range
    _ QName
    a ImportDirective
    b)            = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` ImportDirective -> ()
    forall a. NFData a => a -> ()
    rnf ImportDirective
    b
      rnf (Import Range
    _ QName
    a Maybe AsName
    b OpenShortHand
    _ ImportDirective
    c)      = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Maybe AsName -> ()
    forall a. NFData a => a -> ()
    rnf Maybe AsName
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` ImportDirective -> ()
    forall a. NFData a => a -> ()
    rnf ImportDirective
    c
      rnf (ModuleMacro Range
    _ Erased
    a Name
    b ModuleApplication
    c OpenShortHand
    _ ImportDirective
    d)
                                  = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` ModuleApplication -> ()
    forall a. NFData a => a -> ()
    rnf ModuleApplication
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` ImportDirective -> ()
    forall a. NFData a => a -> ()
    rnf ImportDirective
    d
      rnf (Module Range
    _ Erased
    a QName
    b Telescope
    c [Declaration]
    d)      = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` Telescope -> ()
    forall a. NFData a => a -> ()
    rnf Telescope
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    d
      rnf (UnquoteDecl Range
    _ [Name]
    a Expr
    b)     = [Name] -> ()
    forall a. NFData a => a -> ()
    rnf [Name]
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (UnquoteDef Range
    _ [Name]
    a Expr
    b)      = [Name] -> ()
    forall a. NFData a => a -> ()
    rnf [Name]
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (UnquoteData Range
    _ Name
    a [Name]
    b Expr
    c)   = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Name] -> ()
    forall a. NFData a => a -> ()
    rnf [Name]
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    c
      rnf (Pragma Pragma
    a)              = Pragma -> ()
    forall a. NFData a => a -> ()
    rnf Pragma
    a
      rnf (Opaque KwRange
    r [Declaration]
    xs)           = KwRange -> ()
    forall a. NFData a => a -> ()
    rnf KwRange
    r () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Declaration] -> ()
    forall a. NFData a => a -> ()
    rnf [Declaration]
    xs
      rnf (Unfolding KwRange
    r [QName]
    xs)        = KwRange -> ()
    forall a. NFData a => a -> ()
    rnf KwRange
    r () -> () -> ()
    forall a b. a -> b -> b
    `seq` [QName] -> ()
    forall a. NFData a => a -> ()
    rnf [QName]
    xs

    instance NFData OpenShortHand

    -- | Ranges are not forced.

    instance NFData Pragma where
      rnf :: Pragma -> ()
    rnf (OptionsPragma Range
    _ [String]
    a)               = [String] -> ()
    forall a. NFData a => a -> ()
    rnf [String]
    a
      rnf (BuiltinPragma Range
    _ Ranged String
    a QName
    b)             = Ranged String -> ()
    forall a. NFData a => a -> ()
    rnf Ranged String
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    b
      rnf (RewritePragma Range
    _ Range
    _ [QName]
    a)             = [QName] -> ()
    forall a. NFData a => a -> ()
    rnf [QName]
    a
      rnf (CompilePragma Range
    _ Ranged BackendName
    a QName
    b String
    c)           = Ranged BackendName -> ()
    forall a. NFData a => a -> ()
    rnf Ranged BackendName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` String -> ()
    forall a. NFData a => a -> ()
    rnf String
    c
      rnf (ForeignPragma Range
    _ Ranged BackendName
    b String
    s)             = Ranged BackendName -> ()
    forall a. NFData a => a -> ()
    rnf Ranged BackendName
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` String -> ()
    forall a. NFData a => a -> ()
    rnf String
    s
      rnf (StaticPragma Range
    _ QName
    a)                = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a
      rnf (InjectivePragma Range
    _ QName
    a)             = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a
      rnf (InjectiveForInferencePragma Range
    _ QName
    a) = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a
      rnf (InlinePragma Range
    _ Bool
    _ QName
    a)              = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a
      rnf (ImpossiblePragma Range
    _ [String]
    a)            = [String] -> ()
    forall a. NFData a => a -> ()
    rnf [String]
    a
      rnf (EtaPragma Range
    _ QName
    a)                   = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a
      rnf (TerminationCheckPragma Range
    _ TerminationCheck Name
    a)      = TerminationCheck Name -> ()
    forall a. NFData a => a -> ()
    rnf TerminationCheck Name
    a
      rnf (NoCoverageCheckPragma Range
    _)         = ()
      rnf (WarningOnUsage Range
    _ QName
    a BackendName
    b)            = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` BackendName -> ()
    forall a. NFData a => a -> ()
    rnf BackendName
    b
      rnf (WarningOnImport Range
    _ BackendName
    a)             = BackendName -> ()
    forall a. NFData a => a -> ()
    rnf BackendName
    a
      rnf (CatchallPragma Range
    _)                = ()
      rnf (DisplayPragma Range
    _ Pattern
    a Expr
    b)             = Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    b
      rnf (NoPositivityCheckPragma Range
    _)       = ()
      rnf (PolarityPragma Range
    _ Name
    a [Ranged Occurrence]
    b)            = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Ranged Occurrence] -> ()
    forall a. NFData a => a -> ()
    rnf [Ranged Occurrence]
    b
      rnf (NoUniverseCheckPragma Range
    _)         = ()
      rnf (NotProjectionLikePragma Range
    _ QName
    q)     = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    q
      rnf (OverlapPragma Range
    _ [QName]
    q OverlapMode
    i)             = [QName] -> ()
    forall a. NFData a => a -> ()
    rnf [QName]
    q () -> () -> ()
    forall a b. a -> b -> b
    `seq` OverlapMode -> ()
    forall a. NFData a => a -> ()
    rnf OverlapMode
    i

    -- | Ranges are not forced.

    instance NFData AsName where
      rnf :: AsName -> ()
    rnf (AsName Either Expr Name
    a Range
    _) = Either Expr Name -> ()
    forall a. NFData a => a -> ()
    rnf Either Expr Name
    a

    -- | Ranges are not forced.

    instance NFData a => NFData (TypedBinding' a) where
      rnf :: TypedBinding' a -> ()
    rnf (TBind Range
    _ List1 (NamedArg Binder)
    a a
    b) = List1 (NamedArg Binder) -> ()
    forall a. NFData a => a -> ()
    rnf List1 (NamedArg Binder)
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    b
      rnf (TLet Range
    _ List1 Declaration
    a)    = List1 Declaration -> ()
    forall a. NFData a => a -> ()
    rnf List1 Declaration
    a

    -- | Ranges are not forced.

    instance NFData ModuleApplication where
      rnf :: ModuleApplication -> ()
    rnf (SectionApp Range
    _ Telescope
    a QName
    b [Expr]
    c)       = Telescope -> ()
    forall a. NFData a => a -> ()
    rnf Telescope
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Expr] -> ()
    forall a. NFData a => a -> ()
    rnf [Expr]
    c
      rnf (RecordModuleInstance Range
    _ QName
    a) = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a

    -- | Ranges are not forced.

    instance NFData a => NFData (OpApp a) where
      rnf :: OpApp a -> ()
    rnf (SyntaxBindingLambda Range
    _ List1 LamBinding
    a a
    b) = List1 LamBinding -> ()
    forall a. NFData a => a -> ()
    rnf List1 LamBinding
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    b
      rnf (Ordinary a
    a)                = a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a

    -- | Ranges are not forced.

    instance NFData LHS where
      rnf :: LHS -> ()
    rnf (LHS Pattern
    a [RewriteEqn]
    b [WithExpr]
    c) = Pattern -> ()
    forall a. NFData a => a -> ()
    rnf Pattern
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [RewriteEqn] -> ()
    forall a. NFData a => a -> ()
    rnf [RewriteEqn]
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` [WithExpr] -> ()
    forall a. NFData a => a -> ()
    rnf [WithExpr]
    c

    instance NFData a => NFData (FieldAssignment' a) where
      rnf :: FieldAssignment' a -> ()
    rnf (FieldAssignment Name
    a a
    b) = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    b

    instance NFData ModuleAssignment where
      rnf :: ModuleAssignment -> ()
    rnf (ModuleAssignment QName
    a [Expr]
    b ImportDirective
    c) = QName -> ()
    forall a. NFData a => a -> ()
    rnf QName
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` [Expr] -> ()
    forall a. NFData a => a -> ()
    rnf [Expr]
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` ImportDirective -> ()
    forall a. NFData a => a -> ()
    rnf ImportDirective
    c

    instance NFData a => NFData (WhereClause' a) where
      rnf :: WhereClause' a -> ()
    rnf WhereClause' a
    NoWhere               = ()
      rnf (AnyWhere Range
    _ a
    a)        = a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a
      rnf (SomeWhere Range
    _ Erased
    a Name
    b Access
    c a
    d) = Erased -> ()
    forall a. NFData a => a -> ()
    rnf Erased
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` Access -> ()
    forall a. NFData a => a -> ()
    rnf Access
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    d

    instance NFData WhereClause_

    instance NFData LamClause where
      rnf :: LamClause -> ()
    rnf (LamClause [Pattern]
    a RHS
    b Catchall
    c) = ([Pattern], RHS, Catchall) -> ()
    forall a. NFData a => a -> ()
    rnf ([Pattern]
    a, RHS
    b, Catchall
    c)

    instance NFData a => NFData (LamBinding' a) where
      rnf :: LamBinding' a -> ()
    rnf (DomainFree NamedArg Binder
    a) = NamedArg Binder -> ()
    forall a. NFData a => a -> ()
    rnf NamedArg Binder
    a
      rnf (DomainFull a
    a) = a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a

    instance NFData Binder where
      rnf :: Binder -> ()
    rnf (Binder Maybe Pattern
    a BinderNameOrigin
    o BoundName
    b) = (Maybe Pattern, BinderNameOrigin, BoundName) -> ()
    forall a. NFData a => a -> ()
    rnf (Maybe Pattern
    a, BinderNameOrigin
    o, BoundName
    b)

    instance NFData BoundName where
      rnf :: BoundName -> ()
    rnf (BName Name
    a Fixity'
    b TacticAttribute
    c Bool
    d) = Name -> ()
    forall a. NFData a => a -> ()
    rnf Name
    a () -> () -> ()
    forall a b. a -> b -> b
    `seq` Fixity' -> ()
    forall a. NFData a => a -> ()
    rnf Fixity'
    b () -> () -> ()
    forall a b. a -> b -> b
    `seq` TacticAttribute -> ()
    forall a. NFData a => a -> ()
    rnf TacticAttribute
    c () -> () -> ()
    forall a b. a -> b -> b
    `seq` Bool -> ()
    forall a. NFData a => a -> ()
    rnf Bool
    d

    instance NFData a => NFData (RHS' a) where
      rnf :: RHS' a -> ()
    rnf RHS' a
    AbsurdRHS = ()
      rnf (RHS a
    a)   = a -> ()
    forall a. NFData a => a -> ()
    rnf a
    a

    instance NFData DoStmt where
      rnf :: DoStmt -> ()
    rnf (DoBind Range
    _ Pattern
    p Expr
    e [LamClause]
    w) = (Pattern, Expr, [LamClause]) -> ()
    forall a. NFData a => a -> ()
    rnf (Pattern
    p, Expr
    e, [LamClause]
    w)
      rnf (DoThen Expr
    e)       = Expr -> ()
    forall a. NFData a => a -> ()
    rnf Expr
    e
      rnf (DoLet Range
    _ List1 Declaration
    ds)     = List1 Declaration -> ()
    forall a. NFData a => a -> ()
    rnf List1 Declaration
    ds