    {-# LANGUAGE NondecreasingIndentation #-}

    -- | Pattern matcher used in the reducer for clauses that
    --   have not been compiled to case trees yet.

    module Agda.TypeChecking.Patterns.Match where

    import Prelude hiding (null)

    import Control.Monad
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern

    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Reduce.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Monad hiding (constructorForm)
    import Agda.TypeChecking.Monad.Builtin (getName', builtinHComp)
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records

    import Agda.Utils.Empty
    import Agda.Utils.Functor (for, ($>), (<&>))
    import Agda.Utils.Maybe
    import Agda.Utils.Monad ( anyM, or2M)
    import Agda.Utils.Null
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | If matching is inconclusive (@DontKnow@) we want to know whether it is on a
    --   lazy pattern and whether it is due to a particular meta variable.
    data Match a = Yes Simplification (IntMap (Arg a))
                 | No
                 | DontKnow OnlyLazy (Blocked ())
      deriving (forall a b. (a -> b) -> Match a -> Match b)
    -> (forall a b. a -> Match b -> Match a) -> Functor Match
    forall a b. a -> Match b -> Match a
    forall a b. (a -> b) -> Match a -> Match b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Match a -> Match b
    fmap :: forall a b. (a -> b) -> Match a -> Match b
    $c<$ :: forall a b. a -> Match b -> Match a
    <$ :: forall a b. a -> Match b -> Match a
    Functor

    instance Null (Match a) where
      empty :: Match a
    empty = Simplification -> IntMap (Arg a) -> Match a
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    forall a. Null a => a
    empty IntMap (Arg a)
    forall a. Null a => a
    empty
      null :: Match a -> Bool
    null (Yes Simplification
    simpl IntMap (Arg a)
    as) = Simplification -> Bool
    forall a. Null a => a -> Bool
    null Simplification
    simpl Bool -> Bool -> Bool
    && IntMap (Arg a) -> Bool
    forall a. Null a => a -> Bool
    null IntMap (Arg a)
    as
      null Match a
    _              = Bool
    False

    matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
    matchedArgs :: forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
    matchedArgs Empty
    err Int
    n IntMap (Arg a)
    vs = (Maybe (Arg a) -> Arg a) -> [Maybe (Arg a)] -> [Arg a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg a -> Maybe (Arg a) -> Arg a
    forall a. a -> Maybe a -> a
    fromMaybe (Empty -> Arg a
    forall a. Empty -> a
    absurd Empty
    err)) ([Maybe (Arg a)] -> [Arg a]) -> [Maybe (Arg a)] -> [Arg a]
    forall a b. (a -> b) -> a -> b
    $ Int -> IntMap (Arg a) -> [Maybe (Arg a)]
    forall a. Int -> IntMap (Arg a) -> [Maybe (Arg a)]
    matchedArgs' Int
    n IntMap (Arg a)
    vs

    matchedArgs' :: Int -> IntMap (Arg a) -> [Maybe (Arg a)]
    matchedArgs' :: forall a. Int -> IntMap (Arg a) -> [Maybe (Arg a)]
    matchedArgs' Int
    n IntMap (Arg a)
    vs = (Int -> Maybe (Arg a)) -> [Int] -> [Maybe (Arg a)]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Maybe (Arg a)
    get [Int
    0 .. Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
      where
        get :: Int -> Maybe (Arg a)
    get Int
    k = Int -> IntMap (Arg a) -> Maybe (Arg a)
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    k IntMap (Arg a)
    vs

    -- | Builds a proper substitution from an IntMap produced by match(Co)patterns
    buildSubstitution :: (DeBruijn a)
                      => Impossible -> Int -> IntMap (Arg a) -> Substitution' a
    buildSubstitution :: forall a.
    DeBruijn a =>
    Impossible -> Int -> IntMap (Arg a) -> Substitution' a
    buildSubstitution Impossible
    err Int
    n IntMap (Arg a)
    vs = (Maybe (Arg a) -> Substitution' a -> Substitution' a)
    -> Substitution' a -> [Maybe (Arg a)] -> Substitution' a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Maybe (Arg a) -> Substitution' a -> Substitution' a
    cons Substitution' a
    forall a. Substitution' a
    idS ([Maybe (Arg a)] -> Substitution' a)
    -> [Maybe (Arg a)] -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Int -> IntMap (Arg a) -> [Maybe (Arg a)]
    forall a. Int -> IntMap (Arg a) -> [Maybe (Arg a)]
    matchedArgs' Int
    n IntMap (Arg a)
    vs
      where cons :: Maybe (Arg a) -> Substitution' a -> Substitution' a
    cons Maybe (Arg a)
    Nothing  = Impossible -> Int -> Substitution' a -> Substitution' a
    forall a. Impossible -> Int -> Substitution' a -> Substitution' a
    strengthenS' Impossible
    err Int
    1
            cons (Just Arg a
    v) = a -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    v)

    instance Semigroup (Match a) where
        -- @NotBlocked (StuckOn e)@ means blocked by a variable.
        -- In this case, no instantiation of meta-variables will make progress.
        DontKnow OnlyLazy
    l Blocked ()
    b <> :: Match a -> Match a -> Match a
    <> DontKnow OnlyLazy
    l' Blocked ()
    b' = OnlyLazy -> Blocked () -> Match a
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow (OnlyLazy
    l OnlyLazy -> OnlyLazy -> OnlyLazy
    forall a. Semigroup a => a -> a -> a
    <> OnlyLazy
    l') (Blocked ()
    b Blocked () -> Blocked () -> Blocked ()
    forall a. Semigroup a => a -> a -> a
    <> Blocked ()
    b')
        DontKnow OnlyLazy
    l Blocked ()
    m <> Match a
    _              = OnlyLazy -> Blocked () -> Match a
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    l Blocked ()
    m
        Match a
    _            <> DontKnow OnlyLazy
    l Blocked ()
    m   = OnlyLazy -> Blocked () -> Match a
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    l Blocked ()
    m
        -- One could imagine DontKnow _ _ <> No = No, but would break the
        -- equivalence to case-trees (Issue 2964).
        Match a
    No         <> Match a
    _                = Match a
    forall a. Match a
    No
        Match a
    _          <> Match a
    No               = Match a
    forall a. Match a
    No
        Yes Simplification
    s IntMap (Arg a)
    us   <> Yes Simplification
    s' IntMap (Arg a)
    vs        = Simplification -> IntMap (Arg a) -> Match a
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes (Simplification
    s Simplification -> Simplification -> Simplification
    forall a. Semigroup a => a -> a -> a
    <> Simplification
    s') (IntMap (Arg a)
    us IntMap (Arg a) -> IntMap (Arg a) -> IntMap (Arg a)
    forall a. Semigroup a => a -> a -> a
    <> IntMap (Arg a)
    vs)

    instance Monoid (Match a) where
        mempty :: Match a
    mempty = Match a
    forall a. Null a => a
    empty
        mappend :: Match a -> Match a -> Match a
    mappend = Match a -> Match a -> Match a
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Whether the inconclusive matches are only on lazy patterns.
    data OnlyLazy = OnlyLazy | NonLazy

    instance Semigroup OnlyLazy where
      OnlyLazy
    NonLazy  <> :: OnlyLazy -> OnlyLazy -> OnlyLazy
    <> OnlyLazy
    _        = OnlyLazy
    NonLazy
      OnlyLazy
    _        <> OnlyLazy
    NonLazy  = OnlyLazy
    NonLazy
      OnlyLazy
    OnlyLazy <> OnlyLazy
    OnlyLazy = OnlyLazy
    OnlyLazy

    instance Monoid OnlyLazy where
      mempty :: OnlyLazy
    mempty = OnlyLazy
    OnlyLazy
      mappend :: OnlyLazy -> OnlyLazy -> OnlyLazy
    mappend = OnlyLazy -> OnlyLazy -> OnlyLazy
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Instead of 'zipWithM', we need to use this lazy version
    --   of combining pattern matching computations.

    -- Andreas, 2014-05-08, see Issue 1124:
    --
    -- Due to a bug in TypeChecking.Patterns.Match
    -- a failed match of (C n b) against (C O unit)
    -- turned into (C n unit).
    -- This was because all patterns were matched in
    -- parallel, and evaluations of successfull matches
    -- (and a record constructor like unit can always
    -- be successfully matched) were returned, leading
    -- to a reassembly of (C n b) as (C n unit) which is
    -- illtyped.

    -- Now patterns are matched left to right and
    -- upon failure, no further matching is performed.

    foldMatch
      :: forall m p v . (IsProjP p, MonadMatch m)
      => (p -> v -> m (Match Term, v))
      -> [p] -> [v] -> m (Match Term, [v])
    foldMatch :: forall (m :: * -> *) p v.
    (IsProjP p, MonadMatch m) =>
    (p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
    foldMatch p -> v -> m (Match Term, v)
    match = [p] -> [v] -> m (Match Term, [v])
    loop where
      loop :: [p] -> [v] -> m (Match Term, [v])
      loop :: [p] -> [v] -> m (Match Term, [v])
    loop [p]
    ps0 [v]
    vs0 = do
        case ([p]
    ps0, [v]
    vs0) of
          ([], []) -> (Match Term, [v]) -> m (Match Term, [v])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Null a => a
    empty, [])
          (p
    p : [p]
    ps, v
    v : [v]
    vs) -> do
            (r, v') <- p -> v -> m (Match Term, v)
    match p
    p v
    v
            case r of
              Match Term
    No | Just{} <- p -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP p
    p -> (Match Term, [v]) -> m (Match Term, [v])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Match a
    No, v
    v' v -> [v] -> [v]
    forall a. a -> [a] -> [a]
    : [v]
    vs)
              Match Term
    No -> do
                -- Issue 2964: Even when the first pattern doesn't match we should
                -- continue to the next patterns (and potentially block on them)
                -- because the splitting order in the case tree may not be
                -- left-to-right.
                (r', _vs') <- [p] -> [v] -> m (Match Term, [v])
    loop [p]
    ps [v]
    vs
                -- Issue 2968: do not use vs' here, because it might
                -- contain ill-typed terms due to eta-expansion at wrong
                -- type.
                return (r <> r', v' : vs)
              DontKnow OnlyLazy
    OnlyLazy Blocked ()
    _ -> do
                (r', _vs') <- [p] -> [v] -> m (Match Term, [v])
    loop [p]
    ps [v]
    vs
                return (r <> r', v' : vs)
              DontKnow OnlyLazy
    NonLazy Blocked ()
    m -> (Match Term, [v]) -> m (Match Term, [v])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OnlyLazy -> Blocked () -> Match Term
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    NonLazy Blocked ()
    m, v
    v' v -> [v] -> [v]
    forall a. a -> [a] -> [a]
    : [v]
    vs)
              Yes{} -> do
                (r', vs') <- [p] -> [v] -> m (Match Term, [v])
    loop [p]
    ps [v]
    vs
                return (r <> r', v' : vs')
          ([p], [v])
    _ -> m (Match Term, [v])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- TODO refactor matchPattern* to work with Elim instead.
    mergeElim :: Elim -> Arg Term -> Elim
    mergeElim :: Elim -> Arg Term -> Elim
    mergeElim Apply{} Arg Term
    arg = Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    arg
    mergeElim (IApply Term
    x Term
    y Term
    _) Arg Term
    arg = Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply Term
    x Term
    y (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg)
    mergeElim Proj{} Arg Term
    _ = Elim
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    mergeElims :: [Elim] -> [Arg Term] -> [Elim]
    mergeElims :: [Elim] -> [Arg Term] -> [Elim]
    mergeElims = (Elim -> Arg Term -> Elim) -> [Elim] -> [Arg Term] -> [Elim]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Elim -> Arg Term -> Elim
    mergeElim

    type MonadMatch m = PureTCM m

    -- | @matchCopatterns ps es@ matches spine @es@ against copattern spine @ps@.
    --
    --   Returns 'Yes' and a substitution for the pattern variables
    --   (in form of IntMap Term) if matching was successful.
    --
    --   Returns 'No' if there was a constructor or projection mismatch.
    --
    --   Returns 'DontKnow' if an argument could not be evaluated to
    --   constructor form because of a blocking meta variable.
    --
    --   In any case, also returns spine @es@ in reduced form
    --   (with all the weak head reductions performed that were necessary
    --   to come to a decision).
    matchCopatterns :: MonadMatch m
                    => [NamedArg DeBruijnPattern]
                    -> [Elim]
                    -> m (Match Term, [Elim])
    matchCopatterns :: forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg DeBruijnPattern] -> [Elim] -> m (Match Term, [Elim])
    matchCopatterns [NamedArg DeBruijnPattern]
    ps [Elim]
    vs = do
      VerboseKey
    -> Int
    -> TCMT IO Doc
    -> m (Match Term, [Elim])
    -> m (Match Term, [Elim])
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc VerboseKey
    "tc.match" Int
    50
        ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ TCMT IO Doc
    "matchCopatterns"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> TCMT IO Doc)
    -> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (DeBruijnPattern -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
    prettyTCM (DeBruijnPattern -> TCMT IO Doc)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg DeBruijnPattern]
    ps)
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Elim -> TCMT IO Doc) -> [Elim] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM [Elim]
    vs)
              ]) (m (Match Term, [Elim]) -> m (Match Term, [Elim]))
    -> m (Match Term, [Elim]) -> m (Match Term, [Elim])
    forall a b. (a -> b) -> a -> b
    $ do
      -- Buggy, see issue 1124:
      -- mapFst mconcat . unzip <$> zipWithM' (matchCopattern . namedArg) ps vs
      (NamedArg DeBruijnPattern -> Elim -> m (Match Term, Elim))
    -> [NamedArg DeBruijnPattern] -> [Elim] -> m (Match Term, [Elim])
    forall (m :: * -> *) p v.
    (IsProjP p, MonadMatch m) =>
    (p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
    foldMatch (DeBruijnPattern -> Elim -> m (Match Term, Elim)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Elim -> m (Match Term, Elim)
    matchCopattern (DeBruijnPattern -> Elim -> m (Match Term, Elim))
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> Elim
    -> m (Match Term, Elim)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg DeBruijnPattern]
    ps [Elim]
    vs

    -- | Match a single copattern.
    matchCopattern :: MonadMatch m
                   => DeBruijnPattern
                   -> Elim
                   -> m (Match Term, Elim)
    matchCopattern :: forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Elim -> m (Match Term, Elim)
    matchCopattern pat :: DeBruijnPattern
    pat@ProjP{} elim :: Elim
    elim@(Proj ProjOrigin
    _ QName
    q) = do
      p <- DeBruijnPattern -> m DeBruijnPattern
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    forall (m :: * -> *).
    HasConstInfo m =>
    DeBruijnPattern -> m DeBruijnPattern
    normaliseProjP DeBruijnPattern
    pat m DeBruijnPattern -> (DeBruijnPattern -> QName) -> m QName
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
             ProjP ProjOrigin
    _ QName
    p -> QName
    p
             DeBruijnPattern
    _         -> QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      q       <- getOriginalProjection q
      return $ if p == q then (Yes YesSimplification empty, elim)
                         else (No,                          elim)
    -- The following two cases are not impossible, see #2964
    matchCopattern ProjP{} elim :: Elim
    elim@Apply{}   = (Match Term, Elim) -> m (Match Term, Elim)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Match a
    No , Elim
    elim)
    matchCopattern DeBruijnPattern
    _       elim :: Elim
    elim@Proj{}    = (Match Term, Elim) -> m (Match Term, Elim)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Match a
    No , Elim
    elim)
    matchCopattern DeBruijnPattern
    p       (Apply Arg Term
    v) = (Arg Term -> Elim) -> (Match Term, Arg Term) -> (Match Term, Elim)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply ((Match Term, Arg Term) -> (Match Term, Elim))
    -> m (Match Term, Arg Term) -> m (Match Term, Elim)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    matchPattern DeBruijnPattern
    p Arg Term
    v
    matchCopattern DeBruijnPattern
    p       e :: Elim
    e@(IApply Term
    x Term
    y Term
    r) = (Arg Term -> Elim) -> (Match Term, Arg Term) -> (Match Term, Elim)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd (Elim -> Arg Term -> Elim
    mergeElim Elim
    e) ((Match Term, Arg Term) -> (Match Term, Elim))
    -> m (Match Term, Arg Term) -> m (Match Term, Elim)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    matchPattern DeBruijnPattern
    p (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    r)

    {-# SPECIALIZE matchPatterns :: [NamedArg DeBruijnPattern] -> [Arg Term] -> TCM (Match Term, [Arg Term]) #-}
    matchPatterns :: MonadMatch m
                  => [NamedArg DeBruijnPattern]
                  -> [Arg Term]
                  -> m (Match Term, [Arg Term])
    matchPatterns :: forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg DeBruijnPattern]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    matchPatterns [NamedArg DeBruijnPattern]
    ps [Arg Term]
    vs = do
      VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.match" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
         [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ TCMT IO Doc
    "matchPatterns"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [NamedArg DeBruijnPattern] -> TCMT IO Doc
    forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m Doc
    prettyTCMPatternList [NamedArg DeBruijnPattern]
    ps
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    vs)
              ]

      VerboseKey
    -> Int
    -> TCMT IO Doc
    -> m (Match Term, [Arg Term])
    -> m (Match Term, [Arg Term])
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc VerboseKey
    "tc.match" Int
    50
        ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ TCMT IO Doc
    "matchPatterns"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> TCMT IO Doc)
    -> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (VerboseKey -> TCMT IO Doc)
    -> (NamedArg DeBruijnPattern -> VerboseKey)
    -> NamedArg DeBruijnPattern
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show) [NamedArg DeBruijnPattern]
    ps)
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    vs)
              ]) (m (Match Term, [Arg Term]) -> m (Match Term, [Arg Term]))
    -> m (Match Term, [Arg Term]) -> m (Match Term, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ do
      -- Buggy, see issue 1124:
      -- (ms,vs) <- unzip <$> zipWithM' (matchPattern . namedArg) ps vs
      -- return (mconcat ms, vs)
      (NamedArg DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term))
    -> [NamedArg DeBruijnPattern]
    -> [Arg Term]
    -> m (Match Term, [Arg Term])
    forall (m :: * -> *) p v.
    (IsProjP p, MonadMatch m) =>
    (p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
    foldMatch (DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    matchPattern (DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term))
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> Arg Term
    -> m (Match Term, Arg Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg DeBruijnPattern]
    ps [Arg Term]
    vs

    -- | Match a single pattern.
    matchPattern :: MonadMatch m
                 => DeBruijnPattern
                 -> Arg Term
                 -> m (Match Term, Arg Term)
    matchPattern :: forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    matchPattern DeBruijnPattern
    p Arg Term
    u = case (DeBruijnPattern
    p, Arg Term
    u) of
      (ProjP{}, Arg Term
    _            ) -> m (Match Term, Arg Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      (IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x , Arg Term
    arg ) -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Simplification -> IntMap (Arg Term) -> Match Term
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    NoSimplification IntMap (Arg Term)
    entry, Arg Term
    arg)
        where entry :: IntMap (Arg Term)
    entry = (Int, Arg Term) -> IntMap (Arg Term)
    forall el coll. Singleton el coll => el -> coll
    singleton (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x, Arg Term
    arg)
      (VarP PatternInfo
    _ DBPatVar
    x , Arg Term
    arg          ) -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Simplification -> IntMap (Arg Term) -> Match Term
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    NoSimplification IntMap (Arg Term)
    entry, Arg Term
    arg)
        where entry :: IntMap (Arg Term)
    entry = (Int, Arg Term) -> IntMap (Arg Term)
    forall el coll. Singleton el coll => el -> coll
    singleton (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x, Arg Term
    arg)
      (DotP PatternInfo
    _ Term
    _ , arg :: Arg Term
    arg@(Arg ArgInfo
    _ Term
    v)) -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Simplification -> IntMap (Arg Term) -> Match Term
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    NoSimplification IntMap (Arg Term)
    forall a. Null a => a
    empty, Arg Term
    arg)
      (LitP PatternInfo
    _ Literal
    l , arg :: Arg Term
    arg@(Arg ArgInfo
    _ Term
    v)) -> do
        w <- Term -> m (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    v
        let arg' = Arg Term
    arg Arg Term -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    w
        case w of
          NotBlocked NotBlocked' Term
    _ (Lit Literal
    l')
              | Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l'            -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Simplification -> IntMap (Arg Term) -> Match Term
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    YesSimplification IntMap (Arg Term)
    forall a. Null a => a
    empty , Arg Term
    arg')
              | Bool
    otherwise          -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Match a
    No                          , Arg Term
    arg')
          Blocked Blocker
    b Term
    _              -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OnlyLazy -> Blocked () -> Match Term
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    NonLazy (Blocked () -> Match Term) -> Blocked () -> Match Term
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked ()
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b ()     , Arg Term
    arg')
          NotBlocked NotBlocked' Term
    r Term
    t           -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OnlyLazy -> Blocked () -> Match Term
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    NonLazy (Blocked () -> Match Term) -> Blocked () -> Match Term
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    r' () , Arg Term
    arg')
            where r' :: NotBlocked' Term
    r' = Elim -> NotBlocked' Term -> NotBlocked' Term
    forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    arg') NotBlocked' Term
    r

      -- Case constructor pattern.
      (ConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps, Arg ArgInfo
    info Term
    v) -> do
        let lazy :: OnlyLazy
    lazy = if ConPatternInfo -> Bool
    conPLazy ConPatternInfo
    cpi then OnlyLazy
    OnlyLazy else OnlyLazy
    NonLazy
        if Bool -> Bool
    not (ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    cpi) then ConHead
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    ConHead
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    fallback ConHead
    c OnlyLazy
    lazy [NamedArg DeBruijnPattern]
    ps (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Term
    v) else do
        QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isEtaRecordConstructor (ConHead -> QName
    conName ConHead
    c) m (Maybe (QName, RecordData))
    -> (Maybe (QName, RecordData) -> m (Match Term, Arg Term))
    -> m (Match Term, Arg 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
          Maybe (QName, RecordData)
    Nothing -> ConHead
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    ConHead
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    fallback ConHead
    c OnlyLazy
    lazy [NamedArg DeBruijnPattern]
    ps (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Term
    v)
          -- Case: Eta record constructor.
          -- This case is necessary if we want to use the clauses before
          -- record pattern translation (e.g., in type-checking definitions by copatterns).
          Just (QName
    _r, RecordData
    def) -> do
            VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.match" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "matchPattern: eta record"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "c  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ps = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [NamedArg DeBruijnPattern] -> TCMT IO Doc
    forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m Doc
    prettyTCMPatternList [NamedArg DeBruijnPattern]
    ps
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "v  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
              ]
            -- Issue #7266: in case we are brazenly matching potentially ill-typed arguments,
            -- `v` might be an application of a *different* constructor.
            -- In that case we certainly have no match.
            case Term
    v of
              Con ConHead
    c' ConInfo
    _ [Elim]
    _ | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ConHead
    c' -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Match a
    No, Arg Term
    u)
              Term
    _ -> do
                let fs :: [Arg QName]
    fs = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ RecordData -> [Dom QName]
    _recFields RecordData
    def
                Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Arg QName] -> Int
    forall a. Sized a => a -> Int
    size [Arg QName]
    fs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [NamedArg DeBruijnPattern] -> Int
    forall a. Sized a => a -> Int
    size [NamedArg DeBruijnPattern]
    ps) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ([Arg Term] -> Arg Term)
    -> (Match Term, [Arg Term]) -> (Match Term, Arg Term)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Term -> Arg Term)
    -> ([Arg Term] -> Term) -> [Arg Term] -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    c (ConPatternInfo -> ConInfo
    fromConPatternInfo ConPatternInfo
    cpi) ([Elim] -> Term) -> ([Arg Term] -> [Elim]) -> [Arg Term] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim) -> [Arg Term] -> [Elim]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply) ((Match Term, [Arg Term]) -> (Match Term, Arg Term))
    -> m (Match Term, [Arg Term]) -> m (Match Term, Arg Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                  [NamedArg DeBruijnPattern]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg DeBruijnPattern]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    matchPatterns [NamedArg DeBruijnPattern]
    ps ([Arg Term] -> m (Match Term, [Arg Term]))
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ [Arg QName] -> (Arg QName -> Arg Term) -> [Arg Term]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    for [Arg QName]
    fs ((Arg QName -> Arg Term) -> [Arg Term])
    -> (Arg QName -> Arg Term) -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ \ (Arg ArgInfo
    ai QName
    f) -> 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
    $ Term
    v Term -> [Elim] -> Term
    forall t. Apply t => t -> [Elim] -> t
    `applyE` [ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
      (DefP PatternInfo
    o QName
    q [NamedArg DeBruijnPattern]
    ps, Arg Term
    v) -> do
        let f :: Term -> Maybe ([Elim] -> Term, [Elim])
    f (Def QName
    q' [Elim]
    vs) | QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    q' = ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
    forall a. a -> Maybe a
    Just (QName -> [Elim] -> Term
    Def QName
    q, [Elim]
    vs)
            f Term
    _                     = Maybe ([Elim] -> Term, [Elim])
    forall a. Maybe a
    Nothing
        (Term -> Maybe ([Elim] -> Term, [Elim]))
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    (Term -> Maybe ([Elim] -> Term, [Elim]))
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    fallback' Term -> Maybe ([Elim] -> Term, [Elim])
    f OnlyLazy
    NonLazy [NamedArg DeBruijnPattern]
    ps Arg Term
    v
     where
        -- Default: not an eta record constructor.
      fallback :: MonadMatch m
               => ConHead -> OnlyLazy -> [NamedArg DeBruijnPattern] -> Arg Term -> m (Match Term, Arg Term)
      fallback :: forall (m :: * -> *).
    MonadMatch m =>
    ConHead
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    fallback ConHead
    c OnlyLazy
    lazy [NamedArg DeBruijnPattern]
    ps Arg Term
    v = do
        let f :: Term -> Maybe ([Elim] -> Term, [Elim])
    f (Con ConHead
    c' ConInfo
    ci' [Elim]
    vs) | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c' = ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
    forall a. a -> Maybe a
    Just (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    c' ConInfo
    ci',[Elim]
    vs)
            f Term
    _                         = Maybe ([Elim] -> Term, [Elim])
    forall a. Maybe a
    Nothing
        (Term -> Maybe ([Elim] -> Term, [Elim]))
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    (Term -> Maybe ([Elim] -> Term, [Elim]))
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    fallback' Term -> Maybe ([Elim] -> Term, [Elim])
    f OnlyLazy
    lazy [NamedArg DeBruijnPattern]
    ps Arg Term
    v

      -- Regardless of blocking, constructors and a properly applied @hcomp@
      -- can be matched on.
      isMatchable' :: HasBuiltins m => m (Blocked Term -> Maybe Term)
      isMatchable' :: forall (m :: * -> *).
    HasBuiltins m =>
    m (Blocked Term -> Maybe Term)
    isMatchable' = do
        mhcomp <- PrimitiveId -> m (Maybe QName)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' PrimitiveId
    builtinHComp
        return $ \ Blocked Term
    r ->
          case Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    r of
            t :: Term
    t@Con{} -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    t
            t :: Term
    t@(Def QName
    q [Elim
    l,Elim
    a,Elim
    phi,Elim
    u,Elim
    u0]) | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mhcomp
                    -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    t
            -- TODO this covers the transpIx functions, but it's a hack.
            t :: Term
    t@(Def QName
    q [Elim]
    _) | NotBlocked{blockingStatus :: forall t a. Blocked' t a -> NotBlocked' t
    blockingStatus = MissingClauses QName
    _} <- Blocked Term
    r -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    t
            Term
    _       -> Maybe Term
    forall a. Maybe a
    Nothing

      -- DefP hcomp and ConP matching.
      fallback' :: MonadMatch m
                => (Term -> Maybe (Elims -> Term , Elims))
                -> OnlyLazy
                -> [NamedArg DeBruijnPattern]
                -> Arg Term
                -> m (Match Term, Arg Term)
      fallback' :: forall (m :: * -> *).
    MonadMatch m =>
    (Term -> Maybe ([Elim] -> Term, [Elim]))
    -> OnlyLazy
    -> [NamedArg DeBruijnPattern]
    -> Arg Term
    -> m (Match Term, Arg Term)
    fallback' Term -> Maybe ([Elim] -> Term, [Elim])
    mtc OnlyLazy
    lazy [NamedArg DeBruijnPattern]
    ps (Arg ArgInfo
    info Term
    v) = do
            isMatchable <- m (Blocked Term -> Maybe Term)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Blocked Term -> Maybe Term)
    isMatchable'

            w <- reduceB v
            -- Unfold delayed (corecursive) definitions one step. This is
            -- only necessary if c is a coinductive constructor, but
            -- it does not hurt to do it all the time.
    {-
            w <- case w of
                   NotBlocked r (Def f es) ->   -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
                     unfoldDefinitionE True reduceB' (Def f []) f es
                       -- reduceB is used here because some constructors
                       -- are actually definitions which need to be
                       -- unfolded (due to open public).
                   _ -> return w
    -}
            -- Jesper, 23-06-2016: Note that unfoldCorecursion may destroy
            -- constructor forms, so we only call constructorForm after.
            w <- traverse constructorForm =<< case w of
                   NotBlocked NotBlocked' Term
    r Term
    u -> ReduceM (Blocked Term) -> m (Blocked Term)
    forall a. ReduceM a -> m a
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
    liftReduce (ReduceM (Blocked Term) -> m (Blocked Term))
    -> ReduceM (Blocked Term) -> m (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ReduceM (Blocked Term)
    unfoldCorecursion Term
    u  -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
                   Blocked Term
    _ -> Blocked Term -> m (Blocked Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocked Term
    w
            let v = Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    w
                arg = ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Term
    v  -- the reduced argument

            case w of
              Blocked Term
    b | Just Term
    t <- Blocked Term -> Maybe Term
    isMatchable Blocked Term
    b ->
                case Term -> Maybe ([Elim] -> Term, [Elim])
    mtc Term
    t of
                  Just ([Elim] -> Term
    bld, [Elim]
    vs) -> do
                    (m, vs1) <- [NamedArg DeBruijnPattern]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg DeBruijnPattern]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    matchPatterns [NamedArg DeBruijnPattern]
    ps ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    vs)
                    return (yesSimplification m, Arg info $ bld (mergeElims vs vs1))
                  Maybe ([Elim] -> Term, [Elim])
    Nothing
                                        -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match Term
    forall a. Match a
    No                          , Arg Term
    arg)
              Blocked Blocker
    b Term
    _               -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OnlyLazy -> Blocked () -> Match Term
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    lazy (Blocked () -> Match Term) -> Blocked () -> Match Term
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked ()
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b ()     , Arg Term
    arg)
              NotBlocked NotBlocked' Term
    r Term
    _            -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OnlyLazy -> Blocked () -> Match Term
    forall a. OnlyLazy -> Blocked () -> Match a
    DontKnow OnlyLazy
    lazy (Blocked () -> Match Term) -> Blocked () -> Match Term
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    r' () , Arg Term
    arg)
                where r' :: NotBlocked' Term
    r' = Elim -> NotBlocked' Term -> NotBlocked' Term
    forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    arg) NotBlocked' Term
    r

    yesSimplification :: Match a -> Match a
    yesSimplification :: forall a. Match a -> Match a
    yesSimplification = \case
      Yes Simplification
    _ IntMap (Arg a)
    vs -> Simplification -> IntMap (Arg a) -> Match a
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    YesSimplification IntMap (Arg a)
    vs
      Match a
    m -> Match a
    m

    -- Matching patterns against patterns -------------------------------------

    -- | Match a single pattern.
    matchPatternP :: MonadMatch m
                  => DeBruijnPattern
                  -> Arg DeBruijnPattern
                  -> m (Match DeBruijnPattern)
    matchPatternP :: forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
    matchPatternP DeBruijnPattern
    p (Arg ArgInfo
    info (DotP PatternInfo
    _ Term
    v)) = do
      (m, arg) <- DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    matchPattern DeBruijnPattern
    p (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Term
    v)
      return $ fmap (DotP defaultPatternInfo) m
    matchPatternP DeBruijnPattern
    p arg :: Arg DeBruijnPattern
    arg@(Arg ArgInfo
    info DeBruijnPattern
    q) = do
      let varMatch :: DBPatVar -> m (Match DeBruijnPattern)
    varMatch DBPatVar
    x = Match DeBruijnPattern -> m (Match DeBruijnPattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match DeBruijnPattern -> m (Match DeBruijnPattern))
    -> Match DeBruijnPattern -> m (Match DeBruijnPattern)
    forall a b. (a -> b) -> a -> b
    $ Simplification
    -> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    NoSimplification (IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern)
    -> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ (Int, Arg DeBruijnPattern) -> IntMap (Arg DeBruijnPattern)
    forall el coll. Singleton el coll => el -> coll
    singleton (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x, Arg DeBruijnPattern
    arg)
          termMatch :: m (Match DeBruijnPattern)
    termMatch  = do
            (m, arg) <- DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
    matchPattern DeBruijnPattern
    p ((DeBruijnPattern -> Term) -> Arg DeBruijnPattern -> Arg Term
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DeBruijnPattern -> Term
    patternToTerm Arg DeBruijnPattern
    arg)
            return $ fmap (DotP defaultPatternInfo) m
      case DeBruijnPattern
    p of
        ProjP{}         -> m (Match DeBruijnPattern)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x -> DBPatVar -> m (Match DeBruijnPattern)
    varMatch DBPatVar
    x
        VarP PatternInfo
    _ DBPatVar
    x        -> DBPatVar -> m (Match DeBruijnPattern)
    varMatch DBPatVar
    x
        DotP PatternInfo
    _ Term
    _        -> Match DeBruijnPattern -> m (Match DeBruijnPattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Match DeBruijnPattern -> m (Match DeBruijnPattern))
    -> Match DeBruijnPattern -> m (Match DeBruijnPattern)
    forall a b. (a -> b) -> a -> b
    $ Simplification
    -> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
    forall a. Simplification -> IntMap (Arg a) -> Match a
    Yes Simplification
    NoSimplification IntMap (Arg DeBruijnPattern)
    forall a. Null a => a
    empty
        LitP{}          -> m (Match DeBruijnPattern)
    termMatch -- Literal patterns bind no variables so we can fall back to the Term version.
        DefP{}          -> m (Match DeBruijnPattern)
    termMatch

        ConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps ->
          case DeBruijnPattern
    q of
            ConP ConHead
    c' ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    qs | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c'   -> [NamedArg DeBruijnPattern]
    -> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg DeBruijnPattern]
    -> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
    matchPatternsP [NamedArg DeBruijnPattern]
    ps (((NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
     -> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern])
    -> ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
        -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
    -> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> [NamedArg DeBruijnPattern]
    -> [Arg DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing [NamedArg DeBruijnPattern]
    qs)
                         | Bool
    otherwise -> Match DeBruijnPattern -> m (Match DeBruijnPattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Match DeBruijnPattern
    forall a. Match a
    No
            LitP{} -> (DeBruijnPattern -> DeBruijnPattern)
    -> Match DeBruijnPattern -> Match DeBruijnPattern
    forall a b. (a -> b) -> Match a -> Match b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DeBruijnPattern -> DeBruijnPattern
    forall {x} {a}. Pattern' x -> Pattern' a
    toLitP (Match DeBruijnPattern -> Match DeBruijnPattern)
    -> m (Match DeBruijnPattern) -> m (Match DeBruijnPattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Match DeBruijnPattern)
    termMatch
              where toLitP :: Pattern' x -> Pattern' a
    toLitP (DotP PatternInfo
    _ (Lit Literal
    l)) = Literal -> Pattern' a
    forall a. Literal -> Pattern' a
    litP Literal
    l   -- All bindings should be to literals
                    toLitP Pattern' x
    _                = Pattern' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            DeBruijnPattern
    _      -> m (Match DeBruijnPattern)
    termMatch

    matchPatternsP :: MonadMatch m
                   => [NamedArg DeBruijnPattern]
                   -> [Arg DeBruijnPattern]
                   -> m (Match DeBruijnPattern)
    matchPatternsP :: forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg DeBruijnPattern]
    -> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
    matchPatternsP [NamedArg DeBruijnPattern]
    ps [Arg DeBruijnPattern]
    qs = do
      [Match DeBruijnPattern] -> Match DeBruijnPattern
    forall a. Monoid a => [a] -> a
    mconcat ([Match DeBruijnPattern] -> Match DeBruijnPattern)
    -> m [Match DeBruijnPattern] -> m (Match DeBruijnPattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (DeBruijnPattern
     -> Arg DeBruijnPattern -> m (Match DeBruijnPattern))
    -> [DeBruijnPattern]
    -> [Arg DeBruijnPattern]
    -> m [Match DeBruijnPattern]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
    forall (m :: * -> *).
    MonadMatch m =>
    DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
    matchPatternP ((NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg [NamedArg DeBruijnPattern]
    ps) [Arg DeBruijnPattern]
    qs

    -- | Does the pattern perform a match that could fail?
    properlyMatching :: HasConstInfo m => Pattern' a -> m Bool
    properlyMatching :: forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
    properlyMatching = Bool -> Bool -> Pattern' a -> m Bool
    forall (m :: * -> *) a.
    HasConstInfo m =>
    Bool -> Bool -> Pattern' a -> m Bool
    properlyMatching' Bool
    True Bool
    True

    properlyMatching' :: HasConstInfo m
      => Bool       -- ^ Should absurd patterns count as proper match?
      -> Bool       -- ^ Should projection patterns count as proper match?
      -> Pattern' a -- ^ The pattern.
      -> m Bool
    properlyMatching' :: forall (m :: * -> *) a.
    HasConstInfo m =>
    Bool -> Bool -> Pattern' a -> m Bool
    properlyMatching' Bool
    absP Bool
    projP = \case
      Pattern' a
    p | Bool
    absP Bool -> Bool -> Bool
    && Pattern' a -> Maybe PatOrigin
    forall x. Pattern' x -> Maybe PatOrigin
    patternOrigin Pattern' a
    p Maybe PatOrigin -> Maybe PatOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatOrigin -> Maybe PatOrigin
    forall a. a -> Maybe a
    Just PatOrigin
    PatOAbsurd -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
      ConP ConHead
    con ConPatternInfo
    ci [NamedArg (Pattern' a)]
    ps    -- eta record constructors do not count as proper matches themselves
        | ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    ci -> (Maybe (QName, RecordData) -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe (QName, RecordData) -> Bool)
    -> m (Maybe (QName, RecordData)) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isEtaRecordConstructor (ConHead -> QName
    conName ConHead
    con)) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (NamedArg (Pattern' a) -> m Bool)
    -> [NamedArg (Pattern' a)] -> m Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    (a -> m Bool) -> f a -> m Bool
    anyM (Pattern' a -> m Bool
    forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
    properlyMatching (Pattern' a -> m Bool)
    -> (NamedArg (Pattern' a) -> Pattern' a)
    -> NamedArg (Pattern' a)
    -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg) [NamedArg (Pattern' a)]
    ps
        | Bool
    otherwise     -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
      LitP{}    -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
      DefP{}    -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
      ProjP{}   -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    projP
      VarP{}    -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      DotP{}    -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      IApplyP{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False