    -- | Sanity checking for internal syntax. Mostly checking variable scoping.
    module Agda.Syntax.Internal.SanityCheck where

    import Control.Monad
    import qualified Data.IntSet as Set

    import Agda.Syntax.Internal
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Monad

    import Agda.Utils.List ( dropEnd, initWithDefault )
    import Agda.Utils.Pretty
    import Agda.Utils.Size
    import Agda.Utils.Impossible

    sanityCheckVars :: (Pretty a, Free a) => Telescope -> a -> TCM ()
    sanityCheckVars :: forall a. (Pretty a, Free a) => Telescope -> a -> TCM ()
    sanityCheckVars Telescope
    tel a
    v =
      case (Int -> Bool) -> [Int] -> [Int]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Int -> Bool
    bad (IntSet -> [Int]
    Set.toList (IntSet -> [Int]) -> IntSet -> [Int]
    forall a b. (a -> b) -> a -> b
    $ a -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars a
    v) of
        [] -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        [Int]
    xs -> do
          [Char] -> Int -> TCM Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    1 (TCM Doc -> TCM ()) -> (Doc -> TCM Doc) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc -> Int -> Doc -> Doc
    hang Doc
    "Sanity check failed for" Int
    2
                       (Doc -> Int -> Doc -> Doc
    hang (Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel Doc -> Doc -> Doc
    <+> Doc
    "|-") Int
    2 (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    v))
                , [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "out of scope: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [Char]
    forall a. Show a => a -> [Char]
    show [Int]
    xs ]
          TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        n :: Int
    n     = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
        bad :: Int -> Bool
    bad Int
    x = Int
    x Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0 Bool -> Bool -> Bool
    || Int
    x Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n

    -- | Check that @Γ ⊢ ρ : Δ@.
    sanityCheckSubst :: (Pretty a, Free a) => Telescope -> Substitution' a -> Telescope -> TCM ()
    sanityCheckSubst :: forall a.
    (Pretty a, Free a) =>
    Telescope -> Substitution' a -> Telescope -> TCM ()
    sanityCheckSubst Telescope
    gamma Substitution' a
    rho Telescope
    delta = Telescope -> Substitution' a -> Telescope -> TCM ()
    go Telescope
    gamma Substitution' a
    rho Telescope
    delta
      where
        go :: Telescope -> Substitution' a -> Telescope -> TCM ()
    go Telescope
    gamma Substitution' a
    rho Telescope
    delta =
          case Substitution' a
    rho of
            Substitution' a
    IdS      -> Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gamma Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "idS:" Doc -> Doc -> Doc
    <+> Doc -> Int -> Doc -> Doc
    hang (Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    gamma Doc -> Doc -> Doc
    <+> Doc
    "/=") Int
    2 (Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    delta)
            EmptyS Impossible
    _ -> Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "emptyS:" Doc -> Doc -> Doc
    <+> Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    delta Doc -> Doc -> Doc
    <+> Doc
    "is not empty"
            a
    v :# Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "consS: empty target"
              Telescope -> a -> TCM ()
    forall a. (Pretty a, Free a) => Telescope -> a -> TCM ()
    sanityCheckVars Telescope
    gamma a
    v
              Telescope -> Substitution' a -> Telescope -> TCM ()
    forall a.
    (Pretty a, Free a) =>
    Telescope -> Substitution' a -> Telescope -> TCM ()
    sanityCheckSubst Telescope
    gamma Substitution' a
    rho (Telescope -> Telescope
    dropLast Telescope
    delta)
            Strengthen Impossible
    _ Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "strS: empty target"
              Telescope -> Substitution' a -> Telescope -> TCM ()
    forall a.
    (Pretty a, Free a) =>
    Telescope -> Substitution' a -> Telescope -> TCM ()
    sanityCheckSubst Telescope
    gamma Substitution' a
    rho (Telescope -> Telescope
    dropLast Telescope
    delta)
            Wk Int
    n Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gamma Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "wkS:" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "|" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    gamma Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "|"
                                                                   , [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "< " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n ]
              Telescope -> Substitution' a -> Telescope -> TCM ()
    forall a.
    (Pretty a, Free a) =>
    Telescope -> Substitution' a -> Telescope -> TCM ()
    sanityCheckSubst (Int -> Telescope -> Telescope
    dropLastN Int
    n Telescope
    gamma) Substitution' a
    rho Telescope
    delta
            Lift Int
    n Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gamma Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "liftS: source" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "|" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    gamma Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "|"
                                                                            , [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "< " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n ]
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM ()
    err (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "liftS: target" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "|" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    delta Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "|"
                                                                            , [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "< " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n ]
              Telescope -> Substitution' a -> Telescope -> TCM ()
    forall a.
    (Pretty a, Free a) =>
    Telescope -> Substitution' a -> Telescope -> TCM ()
    sanityCheckSubst (Int -> Telescope -> Telescope
    dropLastN Int
    n Telescope
    gamma) Substitution' a
    rho (Int -> Telescope -> Telescope
    dropLastN Int
    n Telescope
    delta)

        dropLast :: Telescope -> Telescope
    dropLast = ListTel -> Telescope
    telFromList (ListTel -> Telescope)
    -> (Telescope -> ListTel) -> Telescope -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ListTel -> ListTel -> ListTel
    forall a. [a] -> [a] -> [a]
    initWithDefault ListTel
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (ListTel -> ListTel)
    -> (Telescope -> ListTel) -> Telescope -> ListTel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList
        dropLastN :: Int -> Telescope -> Telescope
    dropLastN Int
    n = ListTel -> Telescope
    telFromList (ListTel -> Telescope)
    -> (Telescope -> ListTel) -> Telescope -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> ListTel -> ListTel
    forall a. Int -> [a] -> [a]
    dropEnd Int
    n (ListTel -> ListTel)
    -> (Telescope -> ListTel) -> Telescope -> ListTel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList

        err :: Doc -> TCM ()
    err Doc
    reason = do
          [Char] -> Int -> TCM Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    1 (TCM Doc -> TCM ()) -> (Doc -> TCM Doc) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc -> Int -> Doc -> Doc
    hang Doc
    "Sanity check failed for" Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                  Doc -> Int -> Doc -> Doc
    hang (Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    gamma Doc -> Doc -> Doc
    <+> Doc
    "|-") Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                  Doc -> Int -> Doc -> Doc
    hang (Substitution' a -> Doc
    forall a. Pretty a => a -> Doc
    pretty Substitution' a
    rho Doc -> Doc -> Doc
    <+> Doc
    ":") Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                        Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    delta
                , Doc
    reason ]
          TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__