    {-# LANGUAGE UndecidableInstances #-}  -- for Arg a => Elim' a

    -- | Tools for 'DisplayTerm' and 'DisplayForm'.

    module Agda.TypeChecking.DisplayForm (displayForm) where

    import Control.Monad
    import Control.Monad.Trans (lift)
    import Control.Monad.Trans.Maybe

    import Data.Monoid (All(..))
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Names
    import Agda.Syntax.Scope.Base (inverseScopeLookupName)

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Reduce (instantiate)

    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Pretty

    import Agda.Utils.Impossible

    -- | Convert a 'DisplayTerm' into a 'Term'.
    dtermToTerm :: DisplayTerm -> Term
    dtermToTerm :: DisplayTerm -> Term
    dtermToTerm DisplayTerm
    dt = case DisplayTerm
    dt of
      DWithApp DisplayTerm
    d [DisplayTerm]
    ds Elims
    es ->
        DisplayTerm -> Term
    dtermToTerm DisplayTerm
    d Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` (DisplayTerm -> Arg Term) -> [DisplayTerm] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term)
    -> (DisplayTerm -> Term) -> DisplayTerm -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DisplayTerm -> Term
    dtermToTerm) [DisplayTerm]
    ds Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es
      DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    args   -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg DisplayTerm -> Elim' Term) -> [Arg DisplayTerm] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term)
    -> (Arg DisplayTerm -> Arg Term) -> Arg DisplayTerm -> Elim' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DisplayTerm -> Term) -> Arg DisplayTerm -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DisplayTerm -> Term
    dtermToTerm) [Arg DisplayTerm]
    args
      DDef QName
    f [Elim' DisplayTerm]
    es        -> QName -> Elims -> Term
    Def QName
    f (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Elim' DisplayTerm -> Elim' Term) -> [Elim' DisplayTerm] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map ((DisplayTerm -> Term) -> Elim' DisplayTerm -> Elim' Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DisplayTerm -> Term
    dtermToTerm) [Elim' DisplayTerm]
    es
      DDot Term
    v           -> Term
    v
      DTerm Term
    v          -> Term
    v

    -- | Get the arities of all display forms for a name.
    displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int]
    displayFormArities :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [Nat]
    displayFormArities QName
    q = (Open DisplayForm -> Nat) -> [Open DisplayForm] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length (Elims -> Nat)
    -> (Open DisplayForm -> Elims) -> Open DisplayForm -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DisplayForm -> Elims
    dfPats (DisplayForm -> Elims)
    -> (Open DisplayForm -> DisplayForm) -> Open DisplayForm -> Elims
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Open DisplayForm -> DisplayForm
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget) ([Open DisplayForm] -> [Nat]) -> m [Open DisplayForm] -> m [Nat]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m [Open DisplayForm]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [Open DisplayForm]
    getDisplayForms QName
    q

    -- | Lift a local display form to an outer context. The substitution goes from the parent context to
    --   the context of the local display form (see Issue 958). Current only handles pure extensions of
    --   the parent context.
    liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
    liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
    liftLocalDisplayForm Substitution
    IdS DisplayForm
    df = DisplayForm -> Maybe DisplayForm
    forall a. a -> Maybe a
    Just DisplayForm
    df
    liftLocalDisplayForm (Wk Nat
    n Substitution
    IdS) (Display Nat
    m Elims
    lhs DisplayTerm
    rhs) =
      -- We lift a display form by turning matches on free variables into pattern variables, which can
      -- be done by simply adding to the dfPatternVars field.
      DisplayForm -> Maybe DisplayForm
    forall a. a -> Maybe a
    Just (DisplayForm -> Maybe DisplayForm)
    -> DisplayForm -> Maybe DisplayForm
    forall a b. (a -> b) -> a -> b
    $ Nat -> Elims -> DisplayTerm -> DisplayForm
    Display (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    m) Elims
    lhs DisplayTerm
    rhs
    liftLocalDisplayForm Substitution
    _ DisplayForm
    _ = Maybe DisplayForm
    forall a. Maybe a
    Nothing

    type MonadDisplayForm m =
      ( MonadReduce m
      , ReadTCState m
      , HasConstInfo m
      , HasBuiltins m
      , MonadDebug m
      )

    -- | Find a matching display form for @q es@.
    --   In essence this tries to rewrite @q es@ with any
    --   display form @q ps --> dt@ and returns the instantiated
    --   @dt@ if successful.  First match wins.
    displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
    displayForm :: forall (m :: * -> *).
    MonadDisplayForm m =>
    QName -> Elims -> m (Maybe DisplayTerm)
    displayForm QName
    q Elims
    es = do
      -- Get display forms for name q.
      [Open DisplayForm]
    odfs  <- QName -> m [Open DisplayForm]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [Open DisplayForm]
    getDisplayForms QName
    q
      if ([Open DisplayForm] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Open DisplayForm]
    odfs) then do
        [Char] -> Nat -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.display.top" Nat
    101 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "no displayForm for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q
        Maybe DisplayTerm -> m (Maybe DisplayTerm)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe DisplayTerm
    forall a. Maybe a
    Nothing
      else do
        -- Display debug info about the @Open@s.
        m () -> m ()
    forall (m :: * -> *). MonadDebug m => m () -> m ()
    unlessDebugPrinting (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.display.top" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
          Map CheckpointId Substitution
    cps <- Lens' (Map CheckpointId Substitution) TCEnv
    -> TCMT IO (Map CheckpointId Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Map CheckpointId Substitution) TCEnv
    eCheckpoints
          Telescope
    cxt <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
          Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
            [ Doc
    "displayForm for" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
            , Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "cxt =" Doc -> Doc -> Doc
    <+> Telescope -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    cxt
            , Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "cps =" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (((CheckpointId, Substitution) -> Doc)
    -> [(CheckpointId, Substitution)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (CheckpointId, Substitution) -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Map CheckpointId Substitution -> [(CheckpointId, Substitution)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map CheckpointId Substitution
    cps))
            , Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "dfs =" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Open DisplayForm -> Doc) -> [Open DisplayForm] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Open DisplayForm -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Open DisplayForm]
    odfs) ]
        -- Use only the display forms that can be opened in the current context.
        [DisplayForm]
    dfs   <- [Maybe DisplayForm] -> [DisplayForm]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe DisplayForm] -> [DisplayForm])
    -> m [Maybe DisplayForm] -> m [DisplayForm]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Open DisplayForm -> m (Maybe DisplayForm))
    -> [Open DisplayForm] -> m [Maybe DisplayForm]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Substitution -> DisplayForm -> Maybe DisplayForm)
    -> Open DisplayForm -> m (Maybe DisplayForm)
    forall a (m :: * -> *).
    (TermSubst a, ReadTCState m, MonadTCEnv m) =>
    (Substitution -> a -> Maybe a) -> Open a -> m (Maybe a)
    tryGetOpen Substitution -> DisplayForm -> Maybe DisplayForm
    liftLocalDisplayForm) [Open DisplayForm]
    odfs
        ScopeInfo
    scope <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
        -- Keep the display forms that match the application @q es@.
        [DisplayTerm]
    ms <- do
          [Maybe (DisplayForm, DisplayTerm)]
    ms <- (DisplayForm -> m (Maybe (DisplayForm, DisplayTerm)))
    -> [DisplayForm] -> m [Maybe (DisplayForm, DisplayTerm)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (MaybeT m (DisplayForm, DisplayTerm)
    -> m (Maybe (DisplayForm, DisplayTerm))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m (DisplayForm, DisplayTerm)
     -> m (Maybe (DisplayForm, DisplayTerm)))
    -> (DisplayForm -> MaybeT m (DisplayForm, DisplayTerm))
    -> DisplayForm
    -> m (Maybe (DisplayForm, DisplayTerm))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
    forall (m :: * -> *).
    MonadDisplayForm m =>
    DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
    `matchDisplayForm` Elims
    es)) [DisplayForm]
    dfs
          [DisplayTerm] -> m [DisplayTerm]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ DisplayTerm
    m | Just (DisplayForm
    d, DisplayTerm
    m) <- [Maybe (DisplayForm, DisplayTerm)]
    ms, ScopeInfo -> DisplayForm -> Bool
    wellScoped ScopeInfo
    scope DisplayForm
    d ]
        -- Not safe when printing non-terminating terms.
        -- (nfdfs, us) <- normalise (dfs, es)
        m () -> m ()
    forall (m :: * -> *). MonadDebug m => m () -> m ()
    unlessDebugPrinting (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.display.top" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Doc
    "name        :" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
          , Doc
    "displayForms:" Doc -> Doc -> Doc
    <+> [DisplayForm] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [DisplayForm]
    dfs
          , Doc
    "arguments   :" Doc -> Doc -> Doc
    <+> Elims -> Doc
    forall a. Pretty a => a -> Doc
    pretty Elims
    es
          , Doc
    "matches     :" Doc -> Doc -> Doc
    <+> [DisplayTerm] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [DisplayTerm]
    ms
          , Doc
    "result      :" Doc -> Doc -> Doc
    <+> Maybe DisplayTerm -> Doc
    forall a. Pretty a => a -> Doc
    pretty ([DisplayTerm] -> Maybe DisplayTerm
    forall a. [a] -> Maybe a
    listToMaybe [DisplayTerm]
    ms)
          ]
        -- Return the first display form that matches.
        Maybe DisplayTerm -> m (Maybe DisplayTerm)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DisplayTerm -> m (Maybe DisplayTerm))
    -> Maybe DisplayTerm -> m (Maybe DisplayTerm)
    forall a b. (a -> b) -> a -> b
    $ [DisplayTerm] -> Maybe DisplayTerm
    forall a. [a] -> Maybe a
    listToMaybe [DisplayTerm]
    ms
      where
        -- Look at the original display form, not the instantiated result when
        -- checking if it's well-scoped. Otherwise we might pick up out of scope
        -- identifiers coming from the source term.
        wellScoped :: ScopeInfo -> DisplayForm -> Bool
    wellScoped ScopeInfo
    scope (Display Nat
    _ Elims
    _ DisplayTerm
    d)
          | DisplayTerm -> Bool
    isWithDisplay DisplayTerm
    d = Bool
    True
          | Bool
    otherwise       = All -> Bool
    getAll (All -> Bool) -> All -> Bool
    forall a b. (a -> b) -> a -> b
    $ (QName -> All) -> DisplayTerm -> All
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' (Bool -> All
    All (Bool -> All) -> (QName -> Bool) -> QName -> All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> QName -> Bool
    inScope ScopeInfo
    scope) DisplayTerm
    d  -- all names in d should be in scope

        inScope :: ScopeInfo -> QName -> Bool
    inScope ScopeInfo
    scope QName
    x = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [QName] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([QName] -> Bool) -> [QName] -> Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> ScopeInfo -> [QName]
    inverseScopeLookupName QName
    x ScopeInfo
    scope

        isWithDisplay :: DisplayTerm -> Bool
    isWithDisplay DWithApp{} = Bool
    True
        isWithDisplay DisplayTerm
    _          = Bool
    False

    -- | Match a 'DisplayForm' @q ps = v@ against @q es@.
    --   Return the 'DisplayTerm' @v[us]@ if the match was successful,
    --   i.e., @es / ps = Just us@.
    matchDisplayForm :: MonadDisplayForm m
                     => DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
    matchDisplayForm :: forall (m :: * -> *).
    MonadDisplayForm m =>
    DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
    matchDisplayForm d :: DisplayForm
    d@(Display Nat
    n Elims
    ps DisplayTerm
    v) Elims
    es
      | Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    ps Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es = MaybeT m (DisplayForm, DisplayTerm)
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      | Bool
    otherwise             = do
          let (Elims
    es0, Elims
    es1) = Nat -> Elims -> (Elims, Elims)
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    ps) Elims
    es
          MatchResult
    mm <- Window -> Elims -> Elims -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match (Nat -> Nat -> Window
    Window Nat
    0 Nat
    n) Elims
    ps Elims
    es0
          [WithOrigin Term]
    us <- [Nat]
    -> (Nat -> MaybeT m (WithOrigin Term))
    -> MaybeT m [WithOrigin Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Nat
    0 .. Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1] ((Nat -> MaybeT m (WithOrigin Term)) -> MaybeT m [WithOrigin Term])
    -> (Nat -> MaybeT m (WithOrigin Term))
    -> MaybeT m [WithOrigin Term]
    forall a b. (a -> b) -> a -> b
    $ \ Nat
    i -> do
                  -- #5294: Fail if we don't have bindings for all variables. This can
                  --        happen outside parameterised modules when some of the parameters
                  --        are not used in the lhs.
                  Just WithOrigin Term
    u <- Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term)))
    -> Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term))
    forall a b. (a -> b) -> a -> b
    $ Nat -> MatchResult -> Maybe (WithOrigin Term)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Nat
    i MatchResult
    mm
                  WithOrigin Term -> MaybeT m (WithOrigin Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return WithOrigin Term
    u
          (DisplayForm, DisplayTerm) -> MaybeT m (DisplayForm, DisplayTerm)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DisplayForm
    d, Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin ([Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> [Term] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ (WithOrigin Term -> Term) -> [WithOrigin Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map WithOrigin Term -> Term
    forall a. WithOrigin a -> a
    woThing [WithOrigin Term]
    us) [WithOrigin Term]
    us DisplayTerm
    v DisplayTerm -> Elims -> DisplayTerm
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es1)

    type MatchResult = Map Int (WithOrigin Term)

    unionMatch :: Monad m => MatchResult -> MatchResult -> MaybeT m MatchResult
    unionMatch :: forall (m :: * -> *).
    Monad m =>
    MatchResult -> MatchResult -> MaybeT m MatchResult
    unionMatch MatchResult
    m1 MatchResult
    m2
      | Set Nat -> Set Nat -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    Set.disjoint (MatchResult -> Set Nat
    forall k a. Map k a -> Set k
    Map.keysSet MatchResult
    m1) (MatchResult -> Set Nat
    forall k a. Map k a -> Set k
    Map.keysSet MatchResult
    m2) = MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MatchResult -> MaybeT m MatchResult)
    -> MatchResult -> MaybeT m MatchResult
    forall a b. (a -> b) -> a -> b
    $ MatchResult -> MatchResult -> MatchResult
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union MatchResult
    m1 MatchResult
    m2
      | Bool
    otherwise = MaybeT m MatchResult
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero  -- Non-linear pattern, fail for now.

    unionsMatch :: Monad m => [MatchResult] -> MaybeT m MatchResult
    unionsMatch :: forall (m :: * -> *).
    Monad m =>
    [MatchResult] -> MaybeT m MatchResult
    unionsMatch = (MatchResult -> MatchResult -> MaybeT m MatchResult)
    -> MatchResult -> [MatchResult] -> MaybeT m MatchResult
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM MatchResult -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *).
    Monad m =>
    MatchResult -> MatchResult -> MaybeT m MatchResult
    unionMatch MatchResult
    forall k a. Map k a
    Map.empty

    data Window = Window {Window -> Nat
    dbLo, Window -> Nat
    dbHi :: Nat}

    inWindow :: Window -> Nat -> Maybe Nat
    inWindow :: Window -> Nat -> Maybe Nat
    inWindow (Window Nat
    lo Nat
    hi) Nat
    n | Nat
    lo Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Nat
    n, Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    hi = Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    lo)
                              | Bool
    otherwise       = Maybe Nat
    forall a. Maybe a
    Nothing

    shiftWindow :: Window -> Window
    shiftWindow :: Window -> Window
    shiftWindow (Window Nat
    lo Nat
    hi) = Nat -> Nat -> Window
    Window (Nat
    lo Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) (Nat
    hi Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)

    -- | Class @Match@ for matching a term @p@ in the role of a pattern
    --   against a term @v@.
    --
    --   Free variables inside the window in @p@ are pattern variables and
    --   the result of matching is a map from pattern variables (shifted down to start at 0) to subterms
    --   of @v@.
    class Match a where
      match :: MonadDisplayForm m => Window -> a -> a -> MaybeT m MatchResult

    instance Match a => Match [a] where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> [a] -> [a] -> MaybeT m MatchResult
    match Window
    n [a]
    xs [a]
    ys = [MatchResult] -> MaybeT m MatchResult
    forall (m :: * -> *).
    Monad m =>
    [MatchResult] -> MaybeT m MatchResult
    unionsMatch ([MatchResult] -> MaybeT m MatchResult)
    -> MaybeT m [MatchResult] -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (a -> a -> MaybeT m MatchResult)
    -> [a] -> [a] -> MaybeT m [MatchResult]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (Window -> a -> a -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    n) [a]
    xs [a]
    ys

    instance Match a => Match (Arg a) where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Arg a -> Arg a -> MaybeT m MatchResult
    match Window
    n Arg a
    p Arg a
    v = (WithOrigin Term -> WithOrigin Term) -> MatchResult -> MatchResult
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map (Origin -> WithOrigin Term -> WithOrigin Term
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin (Arg a -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin Arg a
    v)) (MatchResult -> MatchResult)
    -> MaybeT m MatchResult -> MaybeT m MatchResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Window -> a -> a -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    n (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    p) (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    v)

    instance Match a => Match (Elim' a) where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Elim' a -> Elim' a -> MaybeT m MatchResult
    match Window
    n Elim' a
    p Elim' a
    v =
        case (Elim' a
    p, Elim' a
    v) of
          (Proj ProjOrigin
    _ QName
    f, Proj ProjOrigin
    _ QName
    f') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall k a. Map k a
    Map.empty
          (Elim' a, Elim' a)
    _ | Just Arg a
    a  <- Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elim' a
    p
            , Just Arg a
    a' <- Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elim' a
    v    -> Window -> Arg a -> Arg a -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    n Arg a
    a Arg a
    a'
          -- we do not care to differentiate between Apply and IApply for
          -- printing.
          (Elim' a, Elim' a)
    _                               -> MaybeT m MatchResult
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match Term where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Term -> Term -> MaybeT m MatchResult
    match Window
    w Term
    p Term
    v = m Term -> MaybeT m Term
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Term -> m Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v) MaybeT m Term
    -> (Term -> MaybeT m MatchResult) -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ Term
    v -> case (Term -> Term
    unSpine Term
    p, Term -> Term
    unSpine Term
    v) of
        (Var Nat
    i [], Term
    v)    | Just Nat
    j <- Window -> Nat -> Maybe Nat
    inWindow Window
    w Nat
    i -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MatchResult -> MaybeT m MatchResult)
    -> MatchResult -> MaybeT m MatchResult
    forall a b. (a -> b) -> a -> b
    $ Nat -> WithOrigin Term -> MatchResult
    forall k a. k -> a -> Map k a
    Map.singleton Nat
    j (Origin -> Term -> WithOrigin Term
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted Term
    v)
        (Var Nat
    i (Elim' Term
    _:Elims
    _), Term
    v) | Just{} <- Window -> Nat -> Maybe Nat
    inWindow Window
    w Nat
    i -> MaybeT m MatchResult
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero  -- Higher-order pattern, fail for now.
        (Var Nat
    i Elims
    ps, Var Nat
    j Elims
    vs) | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j  -> Window -> Elims -> Elims -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Elims
    ps Elims
    vs
        (Def QName
    c Elims
    ps, Def QName
    d Elims
    vs) | QName
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d  -> Window -> Elims -> Elims -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Elims
    ps Elims
    vs
        (Con ConHead
    c ConInfo
    _ Elims
    ps, Con ConHead
    d ConInfo
    _ Elims
    vs) | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    d -> Window -> Elims -> Elims -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Elims
    ps Elims
    vs
        (Lit Literal
    l, Lit Literal
    l')      | Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l' -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall k a. Map k a
    Map.empty
        (Lam ArgInfo
    h Abs Term
    p, Lam ArgInfo
    h' Abs Term
    v)  | ArgInfo
    h ArgInfo -> ArgInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgInfo
    h' -> Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match (Window -> Window
    shiftWindow Window
    w) (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    p) (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    v)
        (Term
    p, Term
    v)               | Term
    p Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    v  -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall k a. Map k a
    Map.empty  -- TODO: this is wrong (this is why we lifted the rhs before)
        (Term
    p, Level Level
    l)                   -> Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Term
    p (Term -> MaybeT m MatchResult)
    -> MaybeT m Term -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    l
        (Sort Sort
    ps, Sort Sort
    pv)             -> Window -> Sort -> Sort -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Sort
    ps Sort
    pv
        (Term
    p, Sort (Type Level
    v))             -> Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Term
    p (Term -> MaybeT m MatchResult)
    -> MaybeT m Term -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    v
        (Term, Term)
    _                              -> MaybeT m MatchResult
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match Sort where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Sort -> Sort -> MaybeT m MatchResult
    match Window
    w Sort
    p Sort
    v = case (Sort
    p, Sort
    v) of
        (Type Level
    pl, Type Level
    vl) -> Window -> Level -> Level -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Level
    pl Level
    vl
        (Sort, Sort)
    _ | Sort
    p Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    v -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall k a. Map k a
    Map.empty
        (Sort, Sort)
    _          -> MaybeT m MatchResult
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match Level where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Level -> Level -> MaybeT m MatchResult
    match Window
    w Level
    p Level
    v = do
        Term
    p <- Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    p
        Term
    v <- Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    v
        Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    w Term
    p Term
    v

    -- | Substitute terms with origin into display terms,
    --   replacing variables along with their origins.
    --
    --   The purpose is to replace the pattern variables in a with-display form,
    --   and only on the top level of the lhs.  Thus, we are happy to fall back
    --   to ordinary substitution where it does not matter.
    --   This fixes issue #2590.

    class SubstWithOrigin a where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a

    instance SubstWithOrigin a => SubstWithOrigin [a] where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> [a] -> [a]
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots)

    instance (SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a) where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Apply Arg a
    arg) = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a) -> Arg a -> Elim' a
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Arg a -> Arg a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Arg a
    arg
      substWithOrigin Substitution
    rho [WithOrigin Term]
    ots e :: Elim' a
    e@Proj{}    = Elim' a
    e
      substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (IApply a
    u a
    v a
    w) = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply
        (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots a
    u)
        (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots a
    v)
        (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots a
    w)

    instance SubstWithOrigin (Arg Term) where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Arg ArgInfo
    ai Term
    v) =
        case Term
    v of
          -- pattern variable: replace origin if better
          Var Nat
    x [] -> case [WithOrigin Term]
    ots [WithOrigin Term] -> Nat -> Maybe (WithOrigin Term)
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    x of
            Just (WithOrigin Origin
    o Term
    u) -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ((Origin -> Origin) -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => (Origin -> Origin) -> a -> a
    mapOrigin (Origin -> Origin -> Origin
    replaceOrigin Origin
    o) ArgInfo
    ai) Term
    u
            Maybe (WithOrigin Term)
    Nothing -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v -- Issue #2717, not __IMPOSSIBLE__
          -- constructor: recurse
          Con ConHead
    c ConInfo
    ci Elims
    args -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Elims -> Elims
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Elims
    args
          -- def: recurse
          Def QName
    q Elims
    es -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    q (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Elims -> Elims
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Elims
    es
          -- otherwise: fall back to ordinary substitution
          Term
    _ -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v
        where
          replaceOrigin :: Origin -> Origin -> Origin
    replaceOrigin Origin
    _ Origin
    UserWritten = Origin
    UserWritten
          replaceOrigin Origin
    o Origin
    _           = Origin
    o

    instance SubstWithOrigin Term where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Term
    v =
        case Term
    v of
          -- constructor: recurse
          Con ConHead
    c ConInfo
    ci Elims
    args -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Elims -> Elims
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Elims
    args
          -- def: recurse
          Def QName
    q Elims
    es -> QName -> Elims -> Term
    Def QName
    q (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Elims -> Elims
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Elims
    es
          -- otherwise: fall back to oridinary substitution
          Term
    _ -> Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v

    -- Do not go into dot pattern, otherwise interaction test #231 fails
    instance SubstWithOrigin DisplayTerm where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots DisplayTerm
    dt =
        case DisplayTerm
    dt of
          DTerm Term
    v        -> Term -> DisplayTerm
    DTerm     (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Term -> Term
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Term
    v
          DDot  Term
    v        -> Term -> DisplayTerm
    DDot      (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v
          DDef QName
    q [Elim' DisplayTerm]
    es      -> QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    q    ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim' DisplayTerm]
    es
          DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    args -> ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Arg DisplayTerm]
    args
          DWithApp DisplayTerm
    t [DisplayTerm]
    ts Elims
    es -> DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
    DWithApp
            (Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots DisplayTerm
    t)
            (Substitution -> [WithOrigin Term] -> [DisplayTerm] -> [DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [DisplayTerm]
    ts)
            (Substitution -> [WithOrigin Term] -> Elims -> Elims
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Elims
    es)

    -- Do not go into dot pattern, otherwise interaction test #231 fails
    instance SubstWithOrigin (Arg DisplayTerm) where
      substWithOrigin :: Substitution
    -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Arg ArgInfo
    ai DisplayTerm
    dt) =
        case DisplayTerm
    dt of
          DTerm Term
    v        -> (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm (Arg Term -> Arg DisplayTerm) -> Arg Term -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    v
          DDot  Term
    v        -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term -> DisplayTerm
    DDot      (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v
          DDef QName
    q [Elim' DisplayTerm]
    es      -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    q    ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim' DisplayTerm]
    es
          DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    args -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Arg DisplayTerm]
    args
          DWithApp DisplayTerm
    t [DisplayTerm]
    ts Elims
    es -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
    DWithApp
            (Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots DisplayTerm
    t)
            (Substitution -> [WithOrigin Term] -> [DisplayTerm] -> [DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [DisplayTerm]
    ts)
            (Substitution -> [WithOrigin Term] -> Elims -> Elims
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Elims
    es)