    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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.Syntax.Common.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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        [Int]
    xs -> do
          [Char] -> Int -> TCM (Doc Aspects) -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM (Doc Aspects) -> m ()
    alwaysReportSDoc [Char]
    "impossible" Int
    1 (TCM (Doc Aspects) -> TCM ())
    -> (Doc Aspects -> TCM (Doc Aspects)) -> Doc Aspects -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc Aspects -> TCM (Doc Aspects)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects -> Int -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Int -> Doc a -> Doc a
    hang Doc Aspects
    "Sanity check failed for" Int
    2
                       (Doc Aspects -> Int -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Int -> Doc a -> Doc a
    hang (Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    tel Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "|-") Int
    2 (a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty a
    v))
                , [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    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      -> 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. 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 Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Doc Aspects
    "idS:" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects -> Int -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Int -> Doc a -> Doc a
    hang (Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    gamma Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "/=") Int
    2 (Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    delta)

            EmptyS Impossible
    _ -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Bool
    forall a. Tele a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Telescope
    delta) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Doc Aspects
    "emptyS:" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    delta Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "is not empty"

            a
    v :# Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Telescope -> Bool
    forall a. Tele a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Telescope
    delta) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "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
    _ Int
    n Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Peano
    forall a. Sized a => a -> Peano
    natSize Telescope
    delta Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Peano
    forall a. Enum a => Int -> a
    toEnum Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "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 (Int -> Telescope -> Telescope
    dropLastN Int
    n Telescope
    delta)

            Wk Int
    n Substitution' a
    rho -> do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Peano
    forall a. Sized a => a -> Peano
    natSize Telescope
    gamma Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Peano
    forall a. Enum a => Int -> a
    toEnum Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Doc Aspects
    "wkS:" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "|" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    gamma Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects
    "|" , [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    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 -> Peano
    forall a. Sized a => a -> Peano
    natSize Telescope
    gamma Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Peano
    forall a. Enum a => Int -> a
    toEnum Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Doc Aspects
    "liftS: source" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "|" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    gamma Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects
    "|" , [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    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 -> Peano
    forall a. Sized a => a -> Peano
    natSize Telescope
    delta Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Peano
    forall a. Enum a => Int -> a
    toEnum Int
    n) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> TCM ()
    err (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Doc Aspects
    "liftS: target" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "|" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    delta Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Semigroup a => a -> a -> a
    <> Doc Aspects
    "|" , [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    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 Aspects -> TCM ()
    err Doc Aspects
    reason = do
          [Char] -> Int -> TCM (Doc Aspects) -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM (Doc Aspects) -> m ()
    alwaysReportSDoc [Char]
    "impossible" Int
    1 (TCM (Doc Aspects) -> TCM ())
    -> (Doc Aspects -> TCM (Doc Aspects)) -> Doc Aspects -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc Aspects -> TCM (Doc Aspects)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc Aspects -> TCM ()) -> Doc Aspects -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects -> Int -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Int -> Doc a -> Doc a
    hang Doc Aspects
    "Sanity check failed for" Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                  Doc Aspects -> Int -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Int -> Doc a -> Doc a
    hang (Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    gamma Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "|-") Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                  Doc Aspects -> Int -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Int -> Doc a -> Doc a
    hang (Substitution' a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Substitution' a
    rho Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    ":") Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $
                        Telescope -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty Telescope
    delta
                , Doc Aspects
    reason ]
          TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__