    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    {- | Various utility functions dealing with the non-linear, higher-order
         patterns used for rewrite rules.
    -}

    module Agda.TypeChecking.Rewriting.NonLinPattern where

    import Prelude hiding ( null )

    import Control.Monad.Reader ( asks )

    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Defs
    import Agda.Syntax.Internal.MetaVars ( AllMetas, unblockOnAllMetasIn )

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Free.Lazy
    import Agda.TypeChecking.Irrelevance (isPropM)
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Primitive.Cubical.Base

    import Agda.Utils.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.List
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    -- | Turn a term into a non-linear pattern, treating the
    --   free variables as pattern variables.
    --   The first argument indicates the relevance we are working under: if this
    --   is Irrelevant, then we construct a pattern that never fails to match.
    --   The second argument is the number of bound variables (from pattern lambdas).
    --   The third argument is the type of the term.

    class PatternFrom a b where
      patternFrom :: Relevance -> Int -> TypeOf a -> a -> TCM b

    instance (PatternFrom a b) => PatternFrom (Arg a) (Arg b) where
      patternFrom :: Relevance -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b)
    patternFrom Relevance
    r Int
    k TypeOf (Arg a)
    t Arg a
    u = let r' :: Relevance
    r' = Relevance
    r Relevance -> Relevance -> Relevance
    `composeRelevance` Arg a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Arg a
    u
                            in  (a -> TCMT IO b) -> Arg a -> TCM (Arg b)
    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 (Relevance -> Int -> TypeOf a -> a -> TCMT IO b
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r' Int
    k (TypeOf a -> a -> TCMT IO b) -> TypeOf a -> a -> TCMT IO b
    forall a b. (a -> b) -> a -> b
    $ Dom' Term (TypeOf a) -> TypeOf a
    forall t e. Dom' t e -> e
    unDom TypeOf (Arg a)
    Dom' Term (TypeOf a)
    t) Arg a
    u

    instance PatternFrom Elims [Elim' NLPat] where
      patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat]
    patternFrom Relevance
    r Int
    k (Type
    t,Elims -> Term
    hd) = \case
        [] -> [Elim' NLPat] -> TCM [Elim' NLPat]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        (Apply Arg Term
    u : Elims
    es) -> do
          (a, b) <- Type -> TCM (Dom Type, Abs Type)
    assertPi Type
    t
          p   <- patternFrom r k a u
          let t'  = Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u)
          let hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Arg Term
    uElim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
          ps  <- patternFrom r k (t',hd') es
          return $ Apply p : ps
        (IApply Term
    x Term
    y Term
    i : Elims
    es) -> do
          (s, q, l, b, u, v) <- Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    assertPath Type
    t
          let t' = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    b Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    i ]
          let hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term -> Term -> Elim' Term
    forall a. a -> a -> a -> Elim' a
    IApply Term
    x Term
    y Term
    iElim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
          interval <- primIntervalType
          p   <- patternFrom r k interval i
          ps  <- patternFrom r k (t',hd') es
          return $ IApply (PTerm x) (PTerm y) p : ps
        (Proj ProjOrigin
    o QName
    f : Elims
    es) -> do
          (a,b) <- QName -> Type -> TCM (Dom Type, Abs Type)
    assertProjOf QName
    f Type
    t
          let u = Elims -> Term
    hd []
              t' = Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    u
          hd' <- applyDef o f (argFromDom a $> u)
          ps  <- patternFrom r k (t',applyE hd') es
          return $ Proj o f : ps

    instance (PatternFrom a b) => PatternFrom (Dom a) (Dom b) where
      patternFrom :: Relevance -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b)
    patternFrom Relevance
    r Int
    k TypeOf (Dom a)
    t = (a -> TCMT IO b) -> Dom a -> TCM (Dom b)
    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) -> Dom' Term a -> f (Dom' Term b)
    traverse ((a -> TCMT IO b) -> Dom a -> TCM (Dom b))
    -> (a -> TCMT IO b) -> Dom a -> TCM (Dom b)
    forall a b. (a -> b) -> a -> b
    $ Relevance -> Int -> TypeOf a -> a -> TCMT IO b
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r Int
    k TypeOf a
    TypeOf (Dom a)
    t

    instance PatternFrom Type NLPType where
      patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType
    patternFrom Relevance
    r Int
    k TypeOf Type
    _ Type
    a = TCM NLPType -> TCM NLPType
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCM NLPType -> TCM NLPType) -> TCM NLPType -> TCM NLPType
    forall a b. (a -> b) -> a -> b
    $
        NLPSort -> NLPat -> NLPType
    NLPType (NLPSort -> NLPat -> NLPType)
    -> TCMT IO NLPSort -> TCMT IO (NLPat -> NLPType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r Int
    k () (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    a)
                TCMT IO (NLPat -> NLPType) -> TCM NLPat -> TCM NLPType
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r Int
    k (Sort -> Type
    sort (Sort -> Type) -> Sort -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    a) (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a)

    instance PatternFrom Sort NLPSort where
      patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
    patternFrom Relevance
    r Int
    k TypeOf Sort
    _ Sort
    s = do
        s <- Sort -> TCMT IO Sort
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Sort
    s
        case s of
          Univ Univ
    u Level' Term
    l -> Univ -> NLPat -> NLPSort
    PUniv Univ
    u (NLPat -> NLPSort) -> TCM NLPat -> TCMT IO NLPSort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Relevance
    -> Int -> TypeOf (Level' Term) -> Level' Term -> TCM NLPat
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r Int
    k () Level' Term
    l
          Inf Univ
    u Integer
    n  -> NLPSort -> TCMT IO NLPSort
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NLPSort -> TCMT IO NLPSort) -> NLPSort -> TCMT IO NLPSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> NLPSort
    PInf Univ
    u Integer
    n
          Sort
    SizeUniv -> NLPSort -> TCMT IO NLPSort
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NLPSort
    PSizeUniv
          Sort
    LockUniv -> NLPSort -> TCMT IO NLPSort
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NLPSort
    PLockUniv
          Sort
    LevelUniv -> NLPSort -> TCMT IO NLPSort
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NLPSort
    PLevelUniv
          Sort
    IntervalUniv -> NLPSort -> TCMT IO NLPSort
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NLPSort
    PIntervalUniv
          PiSort Dom' Term Term
    _ Sort
    _ Abs Sort
    _ -> TCMT IO NLPSort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          FunSort Sort
    _ Sort
    _ -> TCMT IO NLPSort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          UnivSort Sort
    _ -> TCMT IO NLPSort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaS{}  -> TCMT IO NLPSort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DefS{}   -> TCMT IO NLPSort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DummyS String
    s -> do
            String -> Int -> [String] -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    String -> Int -> a -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> [String] -> m ()
    reportS String
    "impossible" Int
    10
              [ String
    "patternFrom: hit dummy sort with content:"
              , String
    s
              ]
            TCMT IO NLPSort
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance PatternFrom Level NLPat where
      patternFrom :: Relevance
    -> Int -> TypeOf (Level' Term) -> Level' Term -> TCM NLPat
    patternFrom Relevance
    r Int
    k TypeOf (Level' Term)
    _ Level' Term
    l = do
        t <- TCMT IO Type
    forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
    levelType
        v <- reallyUnLevelView l
        patternFrom r k t v

    instance PatternFrom Term NLPat where
      patternFrom :: Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
    patternFrom Relevance
    r0 Int
    k TypeOf Term
    t Term
    v = do
        t <- Type -> TCMT IO Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked TypeOf Term
    Type
    t
        etaRecord <- isEtaRecordType t
        prop <- isPropM t
        let r = if Bool
    prop then Relevance
    irrelevant else Relevance
    r0
        v <- unLevel =<< abortIfBlocked v
        reportSDoc "rewriting.build" 60 $ sep
          [ "building a pattern from term v = " <+> prettyTCM v
          , " of type " <+> prettyTCM t
          ]
        pview <- pathViewAsPi'whnf
        let done = Term -> TCMT IO ()
    forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
    blockOnMetasIn Term
    v TCMT IO () -> TCM NLPat -> TCM NLPat
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> NLPat -> TCM NLPat
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> NLPat
    PTerm Term
    v)
        case (unEl t , stripDontCare v) of
          (Pi Dom Type
    a Abs Type
    b , Term
    _) -> do
            let body :: Term
    body = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a) (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0 ]
            p <- Dom Type -> TCM NLPat -> TCM NLPat
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
    addContext Dom Type
    a (Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r (Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) Term
    body)
            return $ PLam (domInfo a) $ Abs (absName b) p
          (Term, Term)
    _ | Left ((Dom Type
    a,Abs Type
    b),(Term
    x,Term
    y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    pview Type
    t -> do
            let body :: Term
    body = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Term
    v Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ Term -> Term -> Term -> Elim' Term
    forall a. a -> a -> a -> Elim' a
    IApply (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term
    x) (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term
    y) (Term -> Elim' Term) -> Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0 ]
            p <- Dom Type -> TCM NLPat -> TCM NLPat
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
    addContext Dom Type
    a (Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r (Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) Term
    body)
            return $ PLam (domInfo a) $ Abs (absName b) p
          (Term
    _ , Var Int
    i Elims
    es)
           | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    k     -> do
               t <- Int -> TCMT IO Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
               PBoundVar i <$> patternFrom r k (t , Var i) es
           -- The arguments of `var i` should be distinct bound variables
           -- in order to build a Miller pattern
           | Just Args
    vs <- Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es -> do
               TelV tel rest <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath (Type -> TCMT IO (TelV Type))
    -> TCMT IO Type -> TCMT IO (TelV Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> TCMT IO Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
               unless (natSize tel >= natSize vs) $ blockOnMetasIn rest >> addContext tel (errNotPi rest)
               let ts = Substitution' (SubstArg [Type]) -> [Type] -> [Type]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst ([SubstArg [Type]] -> Substitution' (SubstArg [Type])
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([SubstArg [Type]] -> Substitution' (SubstArg [Type]))
    -> [SubstArg [Type]] -> Substitution' (SubstArg [Type])
    forall a b. (a -> b) -> a -> b
    $ [SubstArg [Type]] -> [SubstArg [Type]]
    forall a. [a] -> [a]
    reverse ([SubstArg [Type]] -> [SubstArg [Type]])
    -> [SubstArg [Type]] -> [SubstArg [Type]]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    vs) ([Type] -> [Type]) -> [Type] -> [Type]
    forall a b. (a -> b) -> a -> b
    $ (Dom Type -> Type) -> [Dom Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom ([Dom Type] -> [Type]) -> [Dom Type] -> [Type]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel
               mbvs <- forM (zip ts vs) $ \(Type
    t , Arg Term
    v) -> do
                 (Arg Term, Type) -> TCMT IO ()
    forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
    blockOnMetasIn (Arg Term
    v,Type
    t)
                 Term -> Type -> TCMT IO (Maybe Int)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v) Type
    t TCMT IO (Maybe Int)
    -> (Maybe Int -> TCMT IO (Maybe (Arg Int)))
    -> TCMT IO (Maybe (Arg Int))
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                   Just Int
    j | Int
    j Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    k -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int)))
    -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
    forall a b. (a -> b) -> a -> b
    $ Arg Int -> Maybe (Arg Int)
    forall a. a -> Maybe a
    Just (Arg Int -> Maybe (Arg Int)) -> Arg Int -> Maybe (Arg Int)
    forall a b. (a -> b) -> a -> b
    $ Arg Term
    v Arg Term -> Int -> Arg Int
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int
    j
                   Maybe Int
    _              -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Arg Int)
    forall a. Maybe a
    Nothing
               case sequence mbvs of
                 Just [Arg Int]
    bvs | [Arg Int] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct [Arg Int]
    bvs -> do
                   let allBoundVars :: IntSet
    allBoundVars = [Int] -> IntSet
    IntSet.fromList (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    k)
                       ok :: Bool
    ok = Bool -> Bool
    not (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r) Bool -> Bool -> Bool
    ||
                            [Int] -> IntSet
    IntSet.fromList ((Arg Int -> Int) -> [Arg Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Int -> Int
    forall e. Arg e -> e
    unArg [Arg Int]
    bvs) IntSet -> IntSet -> Bool
    forall a. Eq a => a -> a -> Bool
    == IntSet
    allBoundVars
                   if Bool
    ok then NLPat -> TCM NLPat
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> [Arg Int] -> NLPat
    PVar Int
    i [Arg Int]
    bvs) else TCM NLPat
    done
                 Maybe [Arg Int]
    _ -> TCM NLPat
    done
           | Bool
    otherwise -> TCM NLPat
    done
          (Term
    _ , Term
    _ ) | Just (QName
    d, Args
    pars) <- Maybe (QName, Args)
    etaRecord -> do
            RecordDefn def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
            (tel, c, ci, vs) <- etaExpandRecord_ d pars def v
            ct <- assertConOf c t
            PDef (conName c) <$> patternFrom r k (ct , Con c ci) (map Apply vs)
          (Term
    _ , Lam{})   -> Type -> TCM NLPat
    forall a. Type -> TCM a
    errNotPi Type
    t
          (Term
    _ , Lit{})   -> TCM NLPat
    done
          (Term
    _ , Def QName
    f Elims
    es) | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r -> TCM NLPat
    done
          (Term
    _ , Def QName
    f Elims
    es) -> do
            Def lsuc [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc
            Def lmax [] <- primLevelMax
            case es of
              [Elim' Term
    x]     | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    lsuc -> TCM NLPat
    done
              [Elim' Term
    x , Elim' Term
    y] | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    lmax -> TCM NLPat
    done
              Elims
    _                   -> do
                ft <- Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
                PDef f <$> patternFrom r k (ft , Def f) es
          (Term
    _ , Con ConHead
    c ConInfo
    ci Elims
    vs) | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r -> TCM NLPat
    done
          (Term
    _ , Con ConHead
    c ConInfo
    ci Elims
    vs) -> do
            ct <- ConHead -> Type -> TCMT IO Type
    assertConOf ConHead
    c Type
    t
            PDef (conName c) <$> patternFrom r k (ct , Con c ci) vs
          (Term
    _ , Pi Dom Type
    a Abs Type
    b) | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r -> TCM NLPat
    done
          (Term
    _ , Pi Dom Type
    a Abs Type
    b) -> do
            pa <- Relevance
    -> Int -> TypeOf (Dom Type) -> Dom Type -> TCM (Dom NLPType)
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r Int
    k () Dom Type
    a
            pb <- addContext a (patternFrom r (k + 1) () $ absBody b)
            return $ PPi pa (Abs (absName b) pb)
          (Term
    _ , Sort Sort
    s)     -> NLPSort -> NLPat
    PSort (NLPSort -> NLPat) -> TCMT IO NLPSort -> TCM NLPat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
    forall a b.
    PatternFrom a b =>
    Relevance -> Int -> TypeOf a -> a -> TCM b
    patternFrom Relevance
    r Int
    k () Sort
    s
          (Term
    _ , Level Level' Term
    l)    -> TCM NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          (Term
    _ , DontCare{}) -> TCM NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          (Term
    _ , MetaV MetaId
    m Elims
    _)  -> TCM NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          (Term
    _ , Dummy String
    s Elims
    _)  -> String -> TCM NLPat
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s

    -- | Convert from a non-linear pattern to a term.

    class NLPatToTerm p a where
      nlPatToTerm :: PureTCM m => p -> m a

      default nlPatToTerm ::
        ( NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a'
        , PureTCM m
        ) => p -> m a
      nlPatToTerm = (p' -> m a') -> f p' -> m (f a')
    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) -> f a -> f (f b)
    traverse p' -> m a'
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => p' -> m a'
    nlPatToTerm

    instance NLPatToTerm p a => NLPatToTerm [p] [a] where
    instance NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) where
    instance NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) where
    instance NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) where
    instance NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) where

    instance NLPatToTerm Nat Term where
      nlPatToTerm :: forall (m :: * -> *). PureTCM m => Int -> m Term
    nlPatToTerm = Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> (Int -> Term) -> Int -> m Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var

    instance NLPatToTerm NLPat Term where
      nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPat -> m Term
    nlPatToTerm = \case
        PVar Int
    i [Arg Int]
    xs      -> Int -> Elims -> Term
    Var Int
    i (Elims -> Term) -> (Args -> Elims) -> Args -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Term) -> m Args -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Int] -> m Args
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => [Arg Int] -> m Args
    nlPatToTerm [Arg Int]
    xs
        PTerm Term
    u        -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u
        PDef QName
    f [Elim' NLPat]
    es      -> (Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f) m Defn -> (Defn -> m Term) -> m Term
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Constructor{ conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c } -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ConOSystem (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Elim' NLPat] -> m Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
    nlPatToTerm [Elim' NLPat]
    es
          Defn
    _                            -> QName -> Elims -> Term
    Def QName
    f (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Elim' NLPat] -> m Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
    nlPatToTerm [Elim' NLPat]
    es
        PLam ArgInfo
    i Abs NLPat
    u       -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i (Abs Term -> Term) -> m (Abs Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs NLPat -> m (Abs Term)
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => Abs NLPat -> m (Abs Term)
    nlPatToTerm Abs NLPat
    u
        PPi Dom NLPType
    a Abs NLPType
    b        -> Dom Type -> Abs Type -> Term
    Pi    (Dom Type -> Abs Type -> Term)
    -> m (Dom Type) -> m (Abs Type -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom NLPType -> m (Dom Type)
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => Dom NLPType -> m (Dom Type)
    nlPatToTerm Dom NLPType
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs NLPType -> m (Abs Type)
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => Abs NLPType -> m (Abs Type)
    nlPatToTerm Abs NLPType
    b
        PSort NLPSort
    s        -> Sort -> Term
    Sort  (Sort -> Term) -> m Sort -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NLPSort -> m Sort
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
    nlPatToTerm NLPSort
    s
        PBoundVar Int
    i [Elim' NLPat]
    es -> Int -> Elims -> Term
    Var Int
    i (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Elim' NLPat] -> m Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
    nlPatToTerm [Elim' NLPat]
    es

    instance NLPatToTerm NLPat Level where
      nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPat -> m (Level' Term)
    nlPatToTerm = NLPat -> m Term
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => NLPat -> m Term
    nlPatToTerm (NLPat -> m Term)
    -> (Term -> m (Level' Term)) -> NLPat -> m (Level' Term)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Term -> m (Level' Term)
    forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
    levelView

    instance NLPatToTerm NLPType Type where
      nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPType -> m Type
    nlPatToTerm (NLPType NLPSort
    s NLPat
    a) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort -> Term -> Type) -> m Sort -> m (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NLPSort -> m Sort
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
    nlPatToTerm NLPSort
    s m (Term -> Type) -> m Term -> m Type
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NLPat -> m Term
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => NLPat -> m Term
    nlPatToTerm NLPat
    a

    instance NLPatToTerm NLPSort Sort where
      nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
    nlPatToTerm (PUniv Univ
    u NLPat
    l) = Univ -> Level' Term -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (Level' Term -> Sort) -> m (Level' Term) -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NLPat -> m (Level' Term)
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => NLPat -> m (Level' Term)
    nlPatToTerm NLPat
    l
      nlPatToTerm (PInf Univ
    u Integer
    n) = Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    u Integer
    n
      nlPatToTerm NLPSort
    PSizeUniv = Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    forall t. Sort' t
    SizeUniv
      nlPatToTerm NLPSort
    PLockUniv = Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    forall t. Sort' t
    LockUniv
      nlPatToTerm NLPSort
    PLevelUniv = Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    forall t. Sort' t
    LevelUniv
      nlPatToTerm NLPSort
    PIntervalUniv = Sort -> m Sort
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    forall t. Sort' t
    IntervalUniv

    -- | Gather the set of pattern variables of a non-linear pattern
    class NLPatVars a where
      nlPatVarsUnder :: Int -> a -> IntSet

      nlPatVars :: a -> IntSet
      nlPatVars = Int -> a -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    0

    instance {-# OVERLAPPABLE #-} (Foldable f, NLPatVars a) => NLPatVars (f a) where
      nlPatVarsUnder :: Int -> f a -> IntSet
    nlPatVarsUnder Int
    k = (a -> IntSet) -> f a -> IntSet
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((a -> IntSet) -> f a -> IntSet) -> (a -> IntSet) -> f a -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Int -> a -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k

    instance NLPatVars NLPType where
      nlPatVarsUnder :: Int -> NLPType -> IntSet
    nlPatVarsUnder Int
    k (NLPType NLPSort
    l NLPat
    a) = Int -> (NLPSort, NLPat) -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k (NLPSort
    l, NLPat
    a)

    instance NLPatVars NLPSort where
      nlPatVarsUnder :: Int -> NLPSort -> IntSet
    nlPatVarsUnder Int
    k = \case
        PUniv Univ
    _ NLPat
    l   -> Int -> NLPat -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k NLPat
    l
        PInf Univ
    f Integer
    n  -> IntSet
    forall a. Null a => a
    empty
        NLPSort
    PSizeUniv -> IntSet
    forall a. Null a => a
    empty
        NLPSort
    PLockUniv -> IntSet
    forall a. Null a => a
    empty
        NLPSort
    PLevelUniv -> IntSet
    forall a. Null a => a
    empty
        NLPSort
    PIntervalUniv -> IntSet
    forall a. Null a => a
    empty

    instance NLPatVars NLPat where
      nlPatVarsUnder :: Int -> NLPat -> IntSet
    nlPatVarsUnder Int
    k = \case
          PVar Int
    i [Arg Int]
    _  -> Int -> IntSet
    forall el coll. Singleton el coll => el -> coll
    singleton (Int -> IntSet) -> Int -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k
          PDef QName
    _ [Elim' NLPat]
    es -> Int -> [Elim' NLPat] -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k [Elim' NLPat]
    es
          PLam ArgInfo
    _ Abs NLPat
    p  -> Int -> Abs NLPat -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k Abs NLPat
    p
          PPi Dom NLPType
    a Abs NLPType
    b   -> Int -> (Dom NLPType, Abs NLPType) -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k (Dom NLPType
    a, Abs NLPType
    b)
          PSort NLPSort
    s   -> Int -> NLPSort -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k NLPSort
    s
          PBoundVar Int
    _ [Elim' NLPat]
    es -> Int -> [Elim' NLPat] -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k [Elim' NLPat]
    es
          PTerm{}   -> IntSet
    forall a. Null a => a
    empty

    instance (NLPatVars a, NLPatVars b) => NLPatVars (a,b) where
      nlPatVarsUnder :: Int -> (a, b) -> IntSet
    nlPatVarsUnder Int
    k (a
    a,b
    b) = Int -> a -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k a
    a IntSet -> IntSet -> IntSet
    forall a. Monoid a => a -> a -> a
    `mappend` Int -> b -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k b
    b

    instance NLPatVars a => NLPatVars (Abs a) where
      nlPatVarsUnder :: Int -> Abs a -> IntSet
    nlPatVarsUnder Int
    k = \case
        Abs   String
    _ a
    v -> Int -> a -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder (Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) a
    v
        NoAbs String
    _ a
    v -> Int -> a -> IntSet
    forall a. NLPatVars a => Int -> a -> IntSet
    nlPatVarsUnder Int
    k a
    v

    -- | Get all symbols that a non-linear pattern matches against
    class GetMatchables a where
      getMatchables :: a -> [QName]

      default getMatchables :: (Foldable f, GetMatchables a', a ~ f a') => a -> [QName]
      getMatchables = (a' -> [QName]) -> f a' -> [QName]
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap a' -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables

    instance GetMatchables a => GetMatchables [a] where
    instance GetMatchables a => GetMatchables (Arg a) where
    instance GetMatchables a => GetMatchables (Dom a) where
    instance GetMatchables a => GetMatchables (Elim' a) where
    instance GetMatchables a => GetMatchables (Abs a) where

    instance (GetMatchables a, GetMatchables b) => GetMatchables (a,b) where
      getMatchables :: (a, b) -> [QName]
    getMatchables (a
    x,b
    y) = a -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables a
    x [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ b -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables b
    y

    instance GetMatchables NLPat where
      getMatchables :: NLPat -> [QName]
    getMatchables NLPat
    p =
        case NLPat
    p of
          PVar Int
    _ [Arg Int]
    _       -> [QName]
    forall a. Null a => a
    empty
          PDef QName
    f [Elim' NLPat]
    es      -> QName -> [QName]
    forall el coll. Singleton el coll => el -> coll
    singleton QName
    f [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ [Elim' NLPat] -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables [Elim' NLPat]
    es
          PLam ArgInfo
    _ Abs NLPat
    x       -> Abs NLPat -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables Abs NLPat
    x
          PPi Dom NLPType
    a Abs NLPType
    b        -> (Dom NLPType, Abs NLPType) -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables (Dom NLPType
    a,Abs NLPType
    b)
          PSort NLPSort
    s        -> NLPSort -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables NLPSort
    s
          PBoundVar Int
    i [Elim' NLPat]
    es -> [Elim' NLPat] -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables [Elim' NLPat]
    es
          PTerm Term
    u        -> Term -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables Term
    u

    instance GetMatchables NLPType where
      getMatchables :: NLPType -> [QName]
    getMatchables = NLPat -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables (NLPat -> [QName]) -> (NLPType -> NLPat) -> NLPType -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NLPType -> NLPat
    nlpTypeUnEl

    instance GetMatchables NLPSort where
      getMatchables :: NLPSort -> [QName]
    getMatchables = \case
        PUniv Univ
    _ NLPat
    l -> NLPat -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables NLPat
    l
        PInf Univ
    f Integer
    n  -> [QName]
    forall a. Null a => a
    empty
        NLPSort
    PSizeUniv -> [QName]
    forall a. Null a => a
    empty
        NLPSort
    PLockUniv -> [QName]
    forall a. Null a => a
    empty
        NLPSort
    PLevelUniv -> [QName]
    forall a. Null a => a
    empty
        NLPSort
    PIntervalUniv -> [QName]
    forall a. Null a => a
    empty

    instance GetMatchables Term where
      getMatchables :: Term -> [QName]
    getMatchables = (MetaId -> Maybe Term) -> (QName -> [QName]) -> Term -> [QName]
    forall a b.
    (GetDefs a, Monoid b) =>
    (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
    getDefs' MetaId -> Maybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ QName -> [QName]
    forall el coll. Singleton el coll => el -> coll
    singleton

    instance GetMatchables RewriteRule where
      getMatchables :: RewriteRule -> [QName]
    getMatchables = [Elim' NLPat] -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables ([Elim' NLPat] -> [QName])
    -> (RewriteRule -> [Elim' NLPat]) -> RewriteRule -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> [Elim' NLPat]
    rewPats

    -- | Only computes free variables that are not bound (see 'nlPatVars'),
    --   i.e., those in a 'PTerm'.

    instance Free NLPat where
      freeVars' :: forall a c. IsVarSet a c => NLPat -> FreeM a c
    freeVars' = \case
        PVar Int
    _ [Arg Int]
    _       -> FreeM a c
    forall a. Monoid a => a
    mempty
        PDef QName
    _ [Elim' NLPat]
    es      -> [Elim' NLPat] -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => [Elim' NLPat] -> FreeM a c
    freeVars' [Elim' NLPat]
    es
        PLam ArgInfo
    _ Abs NLPat
    u       -> Abs NLPat -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Abs NLPat -> FreeM a c
    freeVars' Abs NLPat
    u
        PPi Dom NLPType
    a Abs NLPType
    b        -> (Dom NLPType, Abs NLPType) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (Dom NLPType, Abs NLPType) -> FreeM a c
    freeVars' (Dom NLPType
    a,Abs NLPType
    b)
        PSort NLPSort
    s        -> NLPSort -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => NLPSort -> FreeM a c
    freeVars' NLPSort
    s
        PBoundVar Int
    _ [Elim' NLPat]
    es -> [Elim' NLPat] -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => [Elim' NLPat] -> FreeM a c
    freeVars' [Elim' NLPat]
    es
        PTerm Term
    t        -> Term -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => Term -> FreeM a c
    freeVars' Term
    t

    instance Free NLPType where
      freeVars' :: forall a c. IsVarSet a c => NLPType -> FreeM a c
    freeVars' (NLPType NLPSort
    s NLPat
    a) =
        ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((FreeEnv' a IgnoreSorts c -> Bool)
    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((IgnoreSorts
    IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (IgnoreSorts -> Bool)
    -> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
    -> FreeEnv' a IgnoreSorts c
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FreeEnv' a IgnoreSorts c -> IgnoreSorts
    forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
    feIgnoreSorts))
          {- then -} ((NLPSort, NLPat) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => (NLPSort, NLPat) -> FreeM a c
    freeVars' (NLPSort
    s, NLPat
    a))
          {- else -} (NLPat -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => NLPat -> FreeM a c
    freeVars' NLPat
    a)

    instance Free NLPSort where
      freeVars' :: forall a c. IsVarSet a c => NLPSort -> FreeM a c
    freeVars' = \case
        PUniv Univ
    _ NLPat
    l -> NLPat -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    forall a c. IsVarSet a c => NLPat -> FreeM a c
    freeVars' NLPat
    l
        PInf Univ
    f Integer
    n  -> FreeM a c
    forall a. Monoid a => a
    mempty
        NLPSort
    PSizeUniv -> FreeM a c
    forall a. Monoid a => a
    mempty
        NLPSort
    PLockUniv -> FreeM a c
    forall a. Monoid a => a
    mempty
        NLPSort
    PLevelUniv -> FreeM a c
    forall a. Monoid a => a
    mempty
        NLPSort
    PIntervalUniv -> FreeM a c
    forall a. Monoid a => a
    mempty

    -- Throws a pattern violation if the given term contains any
    -- metavariables.
    blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m ()
    blockOnMetasIn :: forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
    blockOnMetasIn t
    t = case t -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAllMetasIn t
    t of
      UnblockOnAll Set Blocker
    ms | Set Blocker -> Bool
    forall a. Null a => a -> Bool
    null Set Blocker
    ms -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      Blocker
    b -> Blocker -> m ()
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    b

    -- Helper functions

    assertPi :: Type -> TCM (Dom Type, Abs Type)
    assertPi :: Type -> TCM (Dom Type, Abs Type)
    assertPi Type
    t = Type -> TCMT IO Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t TCMT IO Type
    -> (Type -> TCM (Dom Type, Abs Type)) -> TCM (Dom Type, Abs Type)
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      El Sort
    _ (Pi Dom Type
    a Abs Type
    b) -> (Dom Type, Abs Type) -> TCM (Dom Type, Abs Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type
    a,Abs Type
    b)
      Type
    t             -> Type -> TCM (Dom Type, Abs Type)
    forall a. Type -> TCM a
    errNotPi Type
    t

    errNotPi :: Type -> TCM a
    errNotPi :: forall a. Type -> TCM a
    errNotPi Type
    t = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
        [ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
        , TCMT IO Doc
    "should be a function type, but it isn't."
        , TCMT IO Doc
    "Do you have any non-confluent rewrite rules?"
        ]

    assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    assertPath Type
    t = Type -> TCMT IO Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t TCMT IO Type -> (Type -> TCMT IO PathView) -> TCMT IO PathView
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Type -> TCMT IO PathView
    forall (m :: * -> *). HasBuiltins m => Type -> m PathView
    pathView TCMT IO PathView
    -> (PathView
        -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term))
    -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      PathType Sort
    s QName
    q Arg Term
    l Arg Term
    b Arg Term
    u Arg Term
    v -> (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort
    s,QName
    q,Arg Term
    l,Arg Term
    b,Arg Term
    u,Arg Term
    v)
      OType Type
    t -> Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
    forall a. Type -> TCM a
    errNotPath Type
    t

    errNotPath :: Type -> TCM a
    errNotPath :: forall a. Type -> TCM a
    errNotPath Type
    t = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
        [ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
        , TCMT IO Doc
    "should be a path type, but it isn't."
        , TCMT IO Doc
    "Do you have any non-confluent rewrite rules?"
        ]

    assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type)
    assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type)
    assertProjOf QName
    f Type
    t = do
      t <- Type -> TCMT IO Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t
      getDefType f t >>= \case
        Just (El Sort
    _ (Pi Dom Type
    a Abs Type
    b)) -> (Dom Type, Abs Type) -> TCM (Dom Type, Abs Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type
    a,Abs Type
    b)
        Maybe Type
    _ -> QName -> Type -> TCM (Dom Type, Abs Type)
    forall a. QName -> Type -> TCM a
    errNotProjOf QName
    f Type
    t

    errNotProjOf :: QName -> Type -> TCM a
    errNotProjOf :: forall a. QName -> Type -> TCM a
    errNotProjOf QName
    f Type
    t = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
          [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f , TCMT IO Doc
    "should be a projection from type"
          , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t , TCMT IO Doc
    "but it isn't."
          , TCMT IO Doc
    "Do you have any non-confluent rewrite rules?"
          ]

    assertConOf :: ConHead -> Type -> TCM Type
    assertConOf :: ConHead -> Type -> TCMT IO Type
    assertConOf ConHead
    c Type
    t = ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t TCMT IO (Maybe ((QName, Type, Args), Type))
    -> (Maybe ((QName, Type, Args), Type) -> TCMT IO Type)
    -> TCMT IO Type
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just ((QName, Type, Args)
    _ , Type
    ct) -> Type -> TCMT IO Type
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ct
        Maybe ((QName, Type, Args), Type)
    Nothing -> ConHead -> Type -> TCMT IO Type
    forall a. ConHead -> Type -> TCM a
    errNotConOf ConHead
    c Type
    t

    errNotConOf :: ConHead -> Type -> TCM a
    errNotConOf :: forall a. ConHead -> Type -> TCM a
    errNotConOf ConHead
    c Type
    t = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
          [ ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c , TCMT IO Doc
    "should be a constructor of type"
          , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t , TCMT IO Doc
    "but it isn't."
          , TCMT IO Doc
    "Do you have any non-confluent rewrite rules?"
          ]