    module Agda.TypeChecking.CompiledClause.Compile where

    import Prelude hiding (null)

    import Control.Applicative
    import Control.Monad
    import Control.Monad.Trans.Identity

    import Data.Maybe
    import qualified Data.Map as Map

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Coverage
    import Agda.TypeChecking.Coverage.SplitTree
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.RecordPatterns
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Free.Precompute
    import Agda.TypeChecking.Reduce

    import Agda.Utils.Functor
    import Agda.Utils.Maybe
    import Agda.Utils.List
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    data RunRecordPatternTranslation = RunRecordPatternTranslation | DontRunRecordPatternTranslation
      deriving (RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    (RunRecordPatternTranslation
     -> RunRecordPatternTranslation -> Bool)
    -> (RunRecordPatternTranslation
        -> RunRecordPatternTranslation -> Bool)
    -> Eq RunRecordPatternTranslation
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    $c/= :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    == :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    $c== :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    Eq)

    compileClauses' :: RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
    compileClauses' :: RunRecordPatternTranslation
    -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
    compileClauses' RunRecordPatternTranslation
    recpat [Clause]
    cs Maybe SplitTree
    mSplitTree = do

      -- Throw away the unreachable clauses (#2723).
      let notUnreachable :: Clause -> Bool
    notUnreachable = (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Bool
    clauseUnreachable
      [Cl]
    cs <- (Clause -> Cl) -> [Clause] -> [Cl]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> Cl
    unBruijn ([Clause] -> [Cl]) -> TCMT IO [Clause] -> TCMT IO [Cl]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Clause] -> TCMT IO [Clause]
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP ((Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Clause -> Bool
    notUnreachable [Clause]
    cs)

      let translate :: CompiledClauses -> TCM CompiledClauses
    translate | RunRecordPatternTranslation
    recpat RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    forall a. Eq a => a -> a -> Bool
    == RunRecordPatternTranslation
    RunRecordPatternTranslation = IdentityT (TCMT IO) CompiledClauses -> TCM CompiledClauses
    forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
    runIdentityT (IdentityT (TCMT IO) CompiledClauses -> TCM CompiledClauses)
    -> (CompiledClauses -> IdentityT (TCMT IO) CompiledClauses)
    -> CompiledClauses
    -> TCM CompiledClauses
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CompiledClauses -> IdentityT (TCMT IO) CompiledClauses
    forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    CompiledClauses -> m CompiledClauses
    translateCompiledClauses
                    | Bool
    otherwise                             = CompiledClauses -> TCM CompiledClauses
    forall (m :: * -> *) a. Monad m => a -> m a
    return

      CompiledClauses -> TCM CompiledClauses
    translate (CompiledClauses -> TCM CompiledClauses)
    -> CompiledClauses -> TCM CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Maybe SplitTree
    -> CompiledClauses
    -> (SplitTree -> CompiledClauses)
    -> CompiledClauses
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe SplitTree
    mSplitTree ([Cl] -> CompiledClauses
    compile [Cl]
    cs) ((SplitTree -> CompiledClauses) -> CompiledClauses)
    -> (SplitTree -> CompiledClauses) -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ \SplitTree
    splitTree ->
        SplitTree -> [Cl] -> CompiledClauses
    compileWithSplitTree SplitTree
    splitTree [Cl]
    cs

    -- | Process function clauses into case tree.
    --   This involves:
    --   1. Coverage checking, generating a split tree.
    --   2. Translation of lhs record patterns into rhs uses of projection.
    --      Update the split tree.
    --   3. Generating a case tree from the split tree.
    --   Phases 1. and 2. are skipped if @Nothing@.
    compileClauses ::
      Maybe (QName, Type) -- ^ Translate record patterns and coverage check with given type?
      -> [Clause]
      -> TCM (Maybe SplitTree, Bool, CompiledClauses)
         -- ^ The 'Bool' indicates whether we turned a record expression into a copattern match.
    compileClauses :: Maybe (QName, Type)
    -> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    mt [Clause]
    cs = do
      -- Construct clauses with pattern variables bound in left-to-right order.
      -- Discard de Bruijn indices in patterns.
      case Maybe (QName, Type)
    mt of
        Maybe (QName, Type)
    Nothing -> (Maybe SplitTree
    forall a. Maybe a
    Nothing,Bool
    False,) (CompiledClauses -> (Maybe SplitTree, Bool, CompiledClauses))
    -> ([Clause] -> CompiledClauses)
    -> [Clause]
    -> (Maybe SplitTree, Bool, CompiledClauses)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Cl] -> CompiledClauses
    compile ([Cl] -> CompiledClauses)
    -> ([Clause] -> [Cl]) -> [Clause] -> CompiledClauses
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Clause -> Cl) -> [Clause] -> [Cl]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> Cl
    unBruijn ([Clause] -> (Maybe SplitTree, Bool, CompiledClauses))
    -> TCMT IO [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Clause] -> TCMT IO [Clause]
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP [Clause]
    cs
        Just (QName
    q, Type
    t)  -> do
          SplitTree
    splitTree <- QName -> Type -> [Clause] -> TCM SplitTree
    coverageCheck QName
    q Type
    t [Clause]
    cs

          PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Int -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc.tree" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    "split tree of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " from coverage check "
            , Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ SplitTree -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty SplitTree
    splitTree
            ]

          -- The coverage checker might have added some clauses (#2288)!
          -- Throw away the unreachable clauses (#2723).
          let notUnreachable :: Clause -> Bool
    notUnreachable = (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Bool
    clauseUnreachable
          [Clause]
    cs <- [Clause] -> TCMT IO [Clause]
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP ([Clause] -> TCMT IO [Clause])
    -> TCMT IO [Clause] -> TCMT IO [Clause]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Clause] -> TCMT IO [Clause]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull ([Clause] -> TCMT IO [Clause])
    -> TCMT IO [Clause] -> TCMT IO [Clause]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Clause -> Bool
    notUnreachable ([Clause] -> [Clause])
    -> (Definition -> [Clause]) -> Definition -> [Clause]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> [Clause]
    defClauses (Definition -> [Clause]) -> TCMT IO Definition -> TCMT IO [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

          let cls :: [Cl]
    cls = (Clause -> Cl) -> [Clause] -> [Cl]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> Cl
    unBruijn [Clause]
    cs

          PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Int -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ do
            (TCMT IO Doc
    "clauses patterns of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " before compilation") TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : do
              (Cl -> TCMT IO Doc) -> [Cl] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Pattern' PatVarName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Pattern' PatVarName] -> TCMT IO Doc)
    -> (Cl -> [Pattern' PatVarName]) -> Cl -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
    -> [Arg (Pattern' PatVarName)] -> [Pattern' PatVarName]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg ([Arg (Pattern' PatVarName)] -> [Pattern' PatVarName])
    -> (Cl -> [Arg (Pattern' PatVarName)])
    -> Cl
    -> [Pattern' PatVarName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Cl -> [Arg (Pattern' PatVarName)]
    clPats) [Cl]
    cls
          PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Int -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " before compilation" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> [Clause] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Clause]
    cs
          let cc :: CompiledClauses
    cc = SplitTree -> [Cl] -> CompiledClauses
    compileWithSplitTree SplitTree
    splitTree [Cl]
    cls
          PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Int -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    sep
            [ TCMT IO Doc
    "compiled clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " (still containing record splits)"
            , 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
    $ Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty CompiledClauses
    cc
            ]
          (CompiledClauses
    cc, Bool
    becameCopatternLHS) <- ChangeT (TCMT IO) CompiledClauses
    -> TCMT IO (CompiledClauses, Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT (TCMT IO) CompiledClauses
     -> TCMT IO (CompiledClauses, Bool))
    -> ChangeT (TCMT IO) CompiledClauses
    -> TCMT IO (CompiledClauses, Bool)
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> ChangeT (TCMT IO) CompiledClauses
    forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    CompiledClauses -> m CompiledClauses
    translateCompiledClauses CompiledClauses
    cc
          PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Int -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc" Int
    12 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    sep
            [ TCMT IO Doc
    "compiled clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q
            , 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
    $ Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty CompiledClauses
    cc
            ]
          (Maybe SplitTree, Bool, CompiledClauses)
    -> TCM (Maybe SplitTree, Bool, CompiledClauses)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SplitTree -> Maybe SplitTree
    forall a. a -> Maybe a
    Just SplitTree
    splitTree, Bool
    becameCopatternLHS, (Term -> Term) -> CompiledClauses -> CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Term
    forall a. PrecomputeFreeVars a => a -> a
    precomputeFreeVars_ CompiledClauses
    cc)

    -- | Stripped-down version of 'Agda.Syntax.Internal.Clause'
    --   used in clause compiler.
    data Cl = Cl
      { Cl -> [Arg (Pattern' PatVarName)]
    clPats :: [Arg Pattern]
          -- ^ Pattern variables are considered in left-to-right order.
      , Cl -> Maybe Term
    clBody :: Maybe Term
      } deriving (Int -> Cl -> ShowS
    [Cl] -> ShowS
    Cl -> PatVarName
    (Int -> Cl -> ShowS)
    -> (Cl -> PatVarName) -> ([Cl] -> ShowS) -> Show Cl
    forall a.
    (Int -> a -> ShowS)
    -> (a -> PatVarName) -> ([a] -> ShowS) -> Show a
    showList :: [Cl] -> ShowS
    $cshowList :: [Cl] -> ShowS
    show :: Cl -> PatVarName
    $cshow :: Cl -> PatVarName
    showsPrec :: Int -> Cl -> ShowS
    $cshowsPrec :: Int -> Cl -> ShowS
    Show)

    instance P.Pretty Cl where
      pretty :: Cl -> Doc
    pretty (Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b) = [Arg (Pattern' PatVarName)] -> Doc
    forall a. Pretty a => [a] -> Doc
    P.prettyList [Arg (Pattern' PatVarName)]
    ps Doc -> Doc -> Doc
    P.<+> Doc
    "->" Doc -> Doc -> Doc
    P.<+> Doc -> (Term -> Doc) -> Maybe Term -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    "_|_" Term -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty Maybe Term
    b

    type Cls = [Cl]

    -- | Strip down a clause. Don't forget to apply the substitution to the dot
    --   patterns!
    unBruijn :: Clause -> Cl
    unBruijn :: Clause -> Cl
    unBruijn Clause
    c = [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl (Substitution' (SubstArg [Arg (Pattern' PatVarName)])
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg [Arg (Pattern' PatVarName)])
    sub ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> a -> b
    $ ((Arg (Named NamedName (Pattern' DBPatVar))
     -> Arg (Pattern' PatVarName))
    -> [Arg (Named NamedName (Pattern' DBPatVar))]
    -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Arg (Named NamedName (Pattern' DBPatVar))
      -> Arg (Pattern' PatVarName))
     -> [Arg (Named NamedName (Pattern' DBPatVar))]
     -> [Arg (Pattern' PatVarName)])
    -> ((Named NamedName (Pattern' DBPatVar) -> Pattern' PatVarName)
        -> Arg (Named NamedName (Pattern' DBPatVar))
        -> Arg (Pattern' PatVarName))
    -> (Named NamedName (Pattern' DBPatVar) -> Pattern' PatVarName)
    -> [Arg (Named NamedName (Pattern' DBPatVar))]
    -> [Arg (Pattern' PatVarName)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName (Pattern' DBPatVar) -> Pattern' PatVarName)
    -> Arg (Named NamedName (Pattern' DBPatVar))
    -> Arg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) ((DBPatVar -> PatVarName)
    -> Pattern' DBPatVar -> Pattern' PatVarName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DBPatVar -> PatVarName
    dbPatVarName (Pattern' DBPatVar -> Pattern' PatVarName)
    -> (Named NamedName (Pattern' DBPatVar) -> Pattern' DBPatVar)
    -> Named NamedName (Pattern' DBPatVar)
    -> Pattern' PatVarName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named NamedName (Pattern' DBPatVar) -> Pattern' DBPatVar
    forall name a. Named name a -> a
    namedThing) ([Arg (Named NamedName (Pattern' DBPatVar))]
     -> [Arg (Pattern' PatVarName)])
    -> [Arg (Named NamedName (Pattern' DBPatVar))]
    -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> a -> b
    $ Clause -> [Arg (Named NamedName (Pattern' DBPatVar))]
    namedClausePats Clause
    c)
                    (Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Maybe Term))
    sub (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    c)
      where
        sub :: Substitution' Term
    sub = Permutation -> Substitution' Term
    forall a. DeBruijn a => Permutation -> Substitution' a
    renamingR (Permutation -> Substitution' Term)
    -> Permutation -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Clause -> Maybe Permutation
    clausePerm Clause
    c)

    compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses
    compileWithSplitTree :: SplitTree -> [Cl] -> CompiledClauses
    compileWithSplitTree SplitTree
    t [Cl]
    cs = case SplitTree
    t of
      SplitAt Arg Int
    i LazySplit
    lz SplitTrees' SplitTag
    ts -> Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Arg Int
    i (Case CompiledClauses -> CompiledClauses)
    -> Case CompiledClauses -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ LazySplit
    -> SplitTrees' SplitTag -> Case [Cl] -> Case CompiledClauses
    compiles LazySplit
    lz SplitTrees' SplitTag
    ts (Case [Cl] -> Case CompiledClauses)
    -> Case [Cl] -> Case CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> [Cl] -> Case [Cl]
    splitOn (SplitTrees' SplitTag -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length SplitTrees' SplitTag
    ts Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1) (Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    i) [Cl]
    cs
            -- if there is just one case, we force expansion of catch-alls
            -- this is needed to generate a sound tree on which we can
            -- collapse record pattern splits
      SplittingDone Int
    n -> [Cl] -> CompiledClauses
    compile [Cl]
    cs
        -- after end of split tree, continue with left-to-right strategy

      where
        compiles :: LazySplit -> SplitTrees -> Case Cls -> Case CompiledClauses
        compiles :: LazySplit
    -> SplitTrees' SplitTag -> Case [Cl] -> Case CompiledClauses
    compiles LazySplit
    lz SplitTrees' SplitTag
    ts br :: Case [Cl]
    br@Branches{ projPatterns :: forall c. Case c -> Bool
    projPatterns = Bool
    cop
                                  , conBranches :: forall c. Case c -> Map QName (WithArity c)
    conBranches = Map QName (WithArity [Cl])
    cons
                                  , etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
    etaBranch   = Maybe (ConHead, WithArity [Cl])
    Nothing
                                  , litBranches :: forall c. Case c -> Map Literal c
    litBranches = Map Literal [Cl]
    lits
                                  , fallThrough :: forall c. Case c -> Maybe Bool
    fallThrough = Maybe Bool
    fT
                                  , catchAllBranch :: forall c. Case c -> Maybe c
    catchAllBranch = Maybe [Cl]
    catchAll
                                  , lazyMatch :: forall c. Case c -> Bool
    lazyMatch = Bool
    lazy }
          = Case [Cl]
    br{ conBranches :: Map QName (WithArity CompiledClauses)
    conBranches    = Map QName (WithArity [Cl]) -> Map QName (WithArity CompiledClauses)
    updCons Map QName (WithArity [Cl])
    cons
              , etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
    etaBranch      = Maybe (ConHead, WithArity CompiledClauses)
    forall a. Maybe a
    Nothing
              , litBranches :: Map Literal CompiledClauses
    litBranches    = Map Literal [Cl] -> Map Literal CompiledClauses
    updLits Map Literal [Cl]
    lits
              , fallThrough :: Maybe Bool
    fallThrough    = Maybe Bool
    fT
              , catchAllBranch :: Maybe CompiledClauses
    catchAllBranch = Maybe [Cl] -> Maybe CompiledClauses
    updCatchall Maybe [Cl]
    catchAll
              , lazyMatch :: Bool
    lazyMatch      = Bool
    lazy Bool -> Bool -> Bool
    || LazySplit
    lz LazySplit -> LazySplit -> Bool
    forall a. Eq a => a -> a -> Bool
    == LazySplit
    LazySplit
              }
          where
            updCons :: Map QName (WithArity [Cl]) -> Map QName (WithArity CompiledClauses)
    updCons = (QName -> WithArity [Cl] -> WithArity CompiledClauses)
    -> Map QName (WithArity [Cl])
    -> Map QName (WithArity CompiledClauses)
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey ((QName -> WithArity [Cl] -> WithArity CompiledClauses)
     -> Map QName (WithArity [Cl])
     -> Map QName (WithArity CompiledClauses))
    -> (QName -> WithArity [Cl] -> WithArity CompiledClauses)
    -> Map QName (WithArity [Cl])
    -> Map QName (WithArity CompiledClauses)
    forall a b. (a -> b) -> a -> b
    $ \ QName
    c WithArity [Cl]
    cl ->
             Maybe SplitTree
    -> ([Cl] -> CompiledClauses)
    -> (SplitTree -> [Cl] -> CompiledClauses)
    -> [Cl]
    -> CompiledClauses
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (SplitTag -> SplitTrees' SplitTag -> Maybe SplitTree
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (QName -> SplitTag
    SplitCon QName
    c) SplitTrees' SplitTag
    ts) [Cl] -> CompiledClauses
    compile SplitTree -> [Cl] -> CompiledClauses
    compileWithSplitTree ([Cl] -> CompiledClauses)
    -> WithArity [Cl] -> WithArity CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> WithArity [Cl]
    cl
             -- When the split tree is finished, we continue with @compile@.
            updLits :: Map Literal [Cl] -> Map Literal CompiledClauses
    updLits = (Literal -> [Cl] -> CompiledClauses)
    -> Map Literal [Cl] -> Map Literal CompiledClauses
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey ((Literal -> [Cl] -> CompiledClauses)
     -> Map Literal [Cl] -> Map Literal CompiledClauses)
    -> (Literal -> [Cl] -> CompiledClauses)
    -> Map Literal [Cl]
    -> Map Literal CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ \ Literal
    l [Cl]
    cl ->
              Maybe SplitTree
    -> ([Cl] -> CompiledClauses)
    -> (SplitTree -> [Cl] -> CompiledClauses)
    -> [Cl]
    -> CompiledClauses
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (SplitTag -> SplitTrees' SplitTag -> Maybe SplitTree
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (Literal -> SplitTag
    SplitLit Literal
    l) SplitTrees' SplitTag
    ts) [Cl] -> CompiledClauses
    compile SplitTree -> [Cl] -> CompiledClauses
    compileWithSplitTree [Cl]
    cl
            updCatchall :: Maybe [Cl] -> Maybe CompiledClauses
    updCatchall = ([Cl] -> CompiledClauses) -> Maybe [Cl] -> Maybe CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([Cl] -> CompiledClauses) -> Maybe [Cl] -> Maybe CompiledClauses)
    -> ([Cl] -> CompiledClauses) -> Maybe [Cl] -> Maybe CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Maybe SplitTree
    -> ([Cl] -> CompiledClauses)
    -> (SplitTree -> [Cl] -> CompiledClauses)
    -> [Cl]
    -> CompiledClauses
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (SplitTag -> SplitTrees' SplitTag -> Maybe SplitTree
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup SplitTag
    SplitCatchall SplitTrees' SplitTag
    ts) [Cl] -> CompiledClauses
    compile SplitTree -> [Cl] -> CompiledClauses
    compileWithSplitTree
        compiles LazySplit
    _ SplitTrees' SplitTag
    _ Branches{etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
    etaBranch = Just{}} = Case CompiledClauses
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- we haven't inserted eta matches yet

    compile :: Cls -> CompiledClauses
    compile :: [Cl] -> CompiledClauses
    compile [] = [Arg PatVarName] -> CompiledClauses
    forall a. [Arg PatVarName] -> CompiledClauses' a
    Fail []
    compile [Cl]
    cs = case [Cl] -> Maybe (Bool, Arg Int)
    nextSplit [Cl]
    cs of
      Just (Bool
    isRecP, Arg Int
    n) -> Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Arg Int
    n (Case CompiledClauses -> CompiledClauses)
    -> Case CompiledClauses -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ [Cl] -> CompiledClauses
    compile ([Cl] -> CompiledClauses) -> Case [Cl] -> Case CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> Int -> [Cl] -> Case [Cl]
    splitOn Bool
    isRecP (Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    n) [Cl]
    cs
      Maybe (Bool, Arg Int)
    Nothing -> case Cl -> Maybe Term
    clBody Cl
    c of
        -- It's possible to get more than one clause here due to
        -- catch-all expansion.
        Just Term
    t  -> [Arg PatVarName] -> Term -> CompiledClauses
    forall a. [Arg PatVarName] -> a -> CompiledClauses' a
    Done ((Arg (Pattern' PatVarName) -> Arg PatVarName)
    -> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' PatVarName -> PatVarName)
    -> Arg (Pattern' PatVarName) -> Arg PatVarName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' PatVarName -> PatVarName
    forall {x}. Underscore x => Pattern' x -> x
    name) ([Arg (Pattern' PatVarName)] -> [Arg PatVarName])
    -> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
    forall a b. (a -> b) -> a -> b
    $ Cl -> [Arg (Pattern' PatVarName)]
    clPats Cl
    c) Term
    t
        Maybe Term
    Nothing -> [Arg PatVarName] -> CompiledClauses
    forall a. [Arg PatVarName] -> CompiledClauses' a
    Fail ((Arg (Pattern' PatVarName) -> Arg PatVarName)
    -> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' PatVarName -> PatVarName)
    -> Arg (Pattern' PatVarName) -> Arg PatVarName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' PatVarName -> PatVarName
    forall {x}. Underscore x => Pattern' x -> x
    name) ([Arg (Pattern' PatVarName)] -> [Arg PatVarName])
    -> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
    forall a b. (a -> b) -> a -> b
    $ Cl -> [Arg (Pattern' PatVarName)]
    clPats Cl
    c)
      where
        -- If there are more than one clauses, take the first one.
        c :: Cl
    c = Cl -> [Cl] -> Cl
    forall a. a -> [a] -> a
    headWithDefault Cl
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Cl]
    cs
        name :: Pattern' x -> x
    name (VarP PatternInfo
    _ x
    x) = x
    x
        name (DotP PatternInfo
    _ Term
    _) = x
    forall a. Underscore a => a
    underscore
        name ConP{}  = x
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        name DefP{}  = x
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        name LitP{}  = x
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        name ProjP{} = x
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        name (IApplyP PatternInfo
    _ Term
    _ Term
    _ x
    x) = x
    x

    -- | Get the index of the next argument we need to split on.
    --   This the number of the first pattern that does a (non-lazy) match in the first clause.
    --   Or the first lazy match where all clauses agree on the constructor, if there are no
    --   non-lazy matches.
    nextSplit :: Cls -> Maybe (Bool, Arg Int)
    nextSplit :: [Cl] -> Maybe (Bool, Arg Int)
    nextSplit []             = Maybe (Bool, Arg Int)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    nextSplit (Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    _ : [Cl]
    cs) = (Int -> Pattern' PatVarName -> Bool)
    -> [Arg (Pattern' PatVarName)] -> Maybe (Bool, Arg Int)
    forall {t} {a}.
    (Num t, Enum t) =>
    (t -> Pattern' a -> Bool)
    -> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
    findSplit Int -> Pattern' PatVarName -> Bool
    forall {p} {x}. p -> Pattern' x -> Bool
    nonLazy [Arg (Pattern' PatVarName)]
    ps Maybe (Bool, Arg Int)
    -> Maybe (Bool, Arg Int) -> Maybe (Bool, Arg Int)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Int -> Pattern' PatVarName -> Bool)
    -> [Arg (Pattern' PatVarName)] -> Maybe (Bool, Arg Int)
    forall {t} {a}.
    (Num t, Enum t) =>
    (t -> Pattern' a -> Bool)
    -> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
    findSplit Int -> Pattern' PatVarName -> Bool
    allAgree [Arg (Pattern' PatVarName)]
    ps
      where
        nonLazy :: p -> Pattern' x -> Bool
    nonLazy p
    _ (ConP ConHead
    _ ConPatternInfo
    cpi [NamedArg (Pattern' x)]
    _) = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> Bool
    conPLazy ConPatternInfo
    cpi
        nonLazy p
    _ Pattern' x
    _              = Bool
    True

        findSplit :: (t -> Pattern' a -> Bool)
    -> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
    findSplit t -> Pattern' a -> Bool
    okPat [Arg (Pattern' a)]
    ps = [(Bool, Arg t)] -> Maybe (Bool, Arg t)
    forall a. [a] -> Maybe a
    listToMaybe ([Maybe (Bool, Arg t)] -> [(Bool, Arg t)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (Bool, Arg t)] -> [(Bool, Arg t)])
    -> [Maybe (Bool, Arg t)] -> [(Bool, Arg t)]
    forall a b. (a -> b) -> a -> b
    $
          (Arg (Pattern' a) -> t -> Maybe (Bool, Arg t))
    -> [Arg (Pattern' a)] -> [t] -> [Maybe (Bool, Arg t)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ (Arg ArgInfo
    ai Pattern' a
    p) t
    n -> (, ArgInfo -> t -> Arg t
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai t
    n) (Bool -> (Bool, Arg t)) -> Maybe Bool -> Maybe (Bool, Arg t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern' a -> Maybe Bool
    forall a. Pattern' a -> Maybe Bool
    properSplit Pattern' a
    p Maybe (Bool, Arg t) -> Maybe () -> Maybe (Bool, Arg t)
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (t -> Pattern' a -> Bool
    okPat t
    n Pattern' a
    p)) [Arg (Pattern' a)]
    ps [t
    0..])

        allAgree :: Int -> Pattern' PatVarName -> Bool
    allAgree Int
    i (ConP ConHead
    c ConPatternInfo
    _ [NamedArg (Pattern' PatVarName)]
    _) = (Cl -> Bool) -> [Cl] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    c)) (Maybe QName -> Bool) -> (Cl -> Maybe QName) -> Cl -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Pattern' PatVarName] -> Maybe QName
    forall {x}. [Pattern' x] -> Maybe QName
    getCon ([Pattern' PatVarName] -> Maybe QName)
    -> (Cl -> [Pattern' PatVarName]) -> Cl -> Maybe QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
    -> [Arg (Pattern' PatVarName)] -> [Pattern' PatVarName]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg ([Arg (Pattern' PatVarName)] -> [Pattern' PatVarName])
    -> (Cl -> [Arg (Pattern' PatVarName)])
    -> Cl
    -> [Pattern' PatVarName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    drop Int
    i ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
    -> (Cl -> [Arg (Pattern' PatVarName)])
    -> Cl
    -> [Arg (Pattern' PatVarName)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Cl -> [Arg (Pattern' PatVarName)]
    clPats) [Cl]
    cs
        allAgree Int
    _ Pattern' PatVarName
    _            = Bool
    False

        getCon :: [Pattern' x] -> Maybe QName
    getCon (ConP ConHead
    c ConPatternInfo
    _ [NamedArg (Pattern' x)]
    _ : [Pattern' x]
    _) = QName -> Maybe QName
    forall a. a -> Maybe a
    Just (QName -> Maybe QName) -> QName -> Maybe QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
        getCon [Pattern' x]
    _                = Maybe QName
    forall a. Maybe a
    Nothing

    -- | Is is not a variable pattern?
    --   And if yes, is it a record pattern and/or a fallThrough one?
    properSplit :: Pattern' a -> Maybe Bool
    properSplit :: forall a. Pattern' a -> Maybe Bool
    properSplit (ConP ConHead
    _ ConPatternInfo
    cpi [NamedArg (Pattern' a)]
    _) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just ((ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    cpi Bool -> Bool -> Bool
    && PatternInfo -> PatOrigin
    patOrigin (ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    cpi) PatOrigin -> PatOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatOrigin
    PatORec) Bool -> Bool -> Bool
    || ConPatternInfo -> Bool
    conPFallThrough ConPatternInfo
    cpi)
    properSplit DefP{}    = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    properSplit LitP{}    = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    properSplit ProjP{}   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    properSplit IApplyP{} = Maybe Bool
    forall a. Maybe a
    Nothing
    properSplit VarP{}    = Maybe Bool
    forall a. Maybe a
    Nothing
    properSplit DotP{}    = Maybe Bool
    forall a. Maybe a
    Nothing

    -- | Is this a variable pattern?
    --
    --   Maintain invariant: @isVar = isNothing . properSplit@!
    isVar :: Pattern' a -> Bool
    isVar :: forall a. Pattern' a -> Bool
    isVar IApplyP{} = Bool
    True
    isVar VarP{}    = Bool
    True
    isVar DotP{}    = Bool
    True
    isVar ConP{}    = Bool
    False
    isVar DefP{}    = Bool
    False
    isVar LitP{}    = Bool
    False
    isVar ProjP{}   = Bool
    False

    -- | @splitOn single n cs@ will force expansion of catch-alls
    --   if @single@.
    splitOn :: Bool -> Int -> Cls -> Case Cls
    splitOn :: Bool -> Int -> [Cl] -> Case [Cl]
    splitOn Bool
    single Int
    n [Cl]
    cs = [Case [Cl]] -> Case [Cl]
    forall a. Monoid a => [a] -> a
    mconcat ([Case [Cl]] -> Case [Cl]) -> [Case [Cl]] -> Case [Cl]
    forall a b. (a -> b) -> a -> b
    $ (Cl -> Case [Cl]) -> [Cl] -> [Case [Cl]]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Cl -> [Cl]) -> Case Cl -> Case [Cl]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Cl -> [Cl] -> [Cl]
    forall a. a -> [a] -> [a]
    :[]) (Case Cl -> Case [Cl]) -> (Cl -> Case Cl) -> Cl -> Case [Cl]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Cl -> Case Cl
    splitC Int
    n) ([Cl] -> [Case [Cl]]) -> [Cl] -> [Case [Cl]]
    forall a b. (a -> b) -> a -> b
    $
      -- (\ cs -> trace ("splitting on " ++ show n ++ " after expandCatchAlls " ++ show single ++ ": " ++ prettyShow (P.prettyList cs)) cs) $
        Bool -> Int -> [Cl] -> [Cl]
    expandCatchAlls Bool
    single Int
    n [Cl]
    cs

    splitC :: Int -> Cl -> Case Cl
    splitC :: Int -> Cl -> Case Cl
    splitC Int
    n (Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b) = Maybe (Pattern' PatVarName)
    -> Case Cl -> (Pattern' PatVarName -> Case Cl) -> Case Cl
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe (Pattern' PatVarName)
    mp Case Cl
    fallback ((Pattern' PatVarName -> Case Cl) -> Case Cl)
    -> (Pattern' PatVarName -> Case Cl) -> Case Cl
    forall a b. (a -> b) -> a -> b
    $ \case
      ProjP ProjOrigin
    _ QName
    d   -> QName -> Cl -> Case Cl
    forall c. QName -> c -> Case c
    projCase QName
    d (Cl -> Case Cl) -> Cl -> Case Cl
    forall a b. (a -> b) -> a -> b
    $ [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1) Maybe Term
    b
      IApplyP{}   -> Case Cl
    fallback
      ConP ConHead
    c ConPatternInfo
    i [NamedArg (Pattern' PatVarName)]
    qs -> (QName -> Bool -> WithArity Cl -> Case Cl
    forall c. QName -> Bool -> WithArity c -> Case c
    conCase (ConHead -> QName
    conName ConHead
    c) (ConPatternInfo -> Bool
    conPFallThrough ConPatternInfo
    i) (WithArity Cl -> Case Cl) -> WithArity Cl -> Case Cl
    forall a b. (a -> b) -> a -> b
    $ Int -> Cl -> WithArity Cl
    forall c. Int -> c -> WithArity c
    WithArity ([NamedArg (Pattern' PatVarName)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg (Pattern' PatVarName)]
    qs) (Cl -> WithArity Cl) -> Cl -> WithArity Cl
    forall a b. (a -> b) -> a -> b
    $
                       [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ (NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName))
    -> [NamedArg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName)
    -> NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName
    forall name a. Named name a -> a
    namedThing) [NamedArg (Pattern' PatVarName)]
    qs [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1) Maybe Term
    b) { lazyMatch :: Bool
    lazyMatch = ConPatternInfo -> Bool
    conPLazy ConPatternInfo
    i }
      DefP PatternInfo
    o QName
    q [NamedArg (Pattern' PatVarName)]
    qs -> (QName -> Bool -> WithArity Cl -> Case Cl
    forall c. QName -> Bool -> WithArity c -> Case c
    conCase QName
    q Bool
    False (WithArity Cl -> Case Cl) -> WithArity Cl -> Case Cl
    forall a b. (a -> b) -> a -> b
    $ Int -> Cl -> WithArity Cl
    forall c. Int -> c -> WithArity c
    WithArity ([NamedArg (Pattern' PatVarName)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg (Pattern' PatVarName)]
    qs) (Cl -> WithArity Cl) -> Cl -> WithArity Cl
    forall a b. (a -> b) -> a -> b
    $
                       [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ (NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName))
    -> [NamedArg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName)
    -> NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName
    forall name a. Named name a -> a
    namedThing) [NamedArg (Pattern' PatVarName)]
    qs [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1) Maybe Term
    b) { lazyMatch :: Bool
    lazyMatch = Bool
    False }
      LitP PatternInfo
    _ Literal
    l    -> Literal -> Cl -> Case Cl
    forall c. Literal -> c -> Case c
    litCase Literal
    l (Cl -> Case Cl) -> Cl -> Case Cl
    forall a b. (a -> b) -> a -> b
    $ [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1) Maybe Term
    b
      VarP{}      -> Case Cl
    fallback
      DotP{}      -> Case Cl
    fallback
      where
        ([Arg (Pattern' PatVarName)]
    ps0, [Arg (Pattern' PatVarName)]
    rest) = Int
    -> [Arg (Pattern' PatVarName)]
    -> ([Arg (Pattern' PatVarName)], [Arg (Pattern' PatVarName)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [Arg (Pattern' PatVarName)]
    ps
        mp :: Maybe (Pattern' PatVarName)
    mp          = Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
    -> Maybe (Arg (Pattern' PatVarName)) -> Maybe (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg (Pattern' PatVarName)] -> Maybe (Arg (Pattern' PatVarName))
    forall a. [a] -> Maybe a
    listToMaybe [Arg (Pattern' PatVarName)]
    rest
        ps1 :: [Arg (Pattern' PatVarName)]
    ps1         = Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    drop Int
    1 [Arg (Pattern' PatVarName)]
    rest
        fallback :: Case Cl
    fallback    = Cl -> Case Cl
    forall c. c -> Case c
    catchAll (Cl -> Case Cl) -> Cl -> Case Cl
    forall a b. (a -> b) -> a -> b
    $ [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b

    -- | Expand catch-alls that appear before actual matches.
    --
    -- Example:
    --
    -- @
    --    true  y
    --    x     false
    --    false y
    -- @
    --
    -- will expand the catch-all @x@ to @false@.
    --
    -- Catch-alls need also to be expanded if
    -- they come before/after a record pattern, otherwise we get into
    -- trouble when we want to eliminate splits on records later.
    --
    -- Another example (see Issue 1650):
    -- @
    --   f (x, (y, z)) true  = a
    --   f _           false = b
    -- @
    -- Split tree:
    -- @
    --   0 (first argument of f)
    --    \- 1 (second component of the pair)
    --        \- 3 (last argument of f)
    --            \-- true  -> a
    --             \- false -> b
    -- @
    -- We would like to get the following case tree:
    -- @
    --   case 0 of
    --   _,_ -> case 1 of
    --          _,_ -> case 3 of true  -> a; false -> b
    --          _   -> case 3 of true  -> a; false -> b
    --   _          -> case 3 of true  -> a; false -> b
    -- @
    --
    -- Example from issue #2168:
    -- @
    --   f x     false = a
    --   f false       = \ _ -> b
    --   f x     true  = c
    -- @
    -- case tree:
    -- @
    --   f x y = case y of
    --     true  -> case x of
    --       true  -> c
    --       false -> b
    --     false -> a
    -- @
    --
    -- Example from issue #3628:
    -- @
    --   f i j k (i = i0)(k = i1) = base
    --   f i j k (j = i1)         = base
    -- @
    -- case tree:
    -- @
    --   f i j k o = case i of
    --     i0 -> case k of
    --             i1 -> base
    --             _  -> case j of
    --                     i1 -> base
    --     _  -> case j of
    --             i1 -> base
    -- @
    expandCatchAlls :: Bool -> Int -> Cls -> Cls
    expandCatchAlls :: Bool -> Int -> [Cl] -> [Cl]
    expandCatchAlls Bool
    single Int
    n [Cl]
    cs =
      -- Andreas, 2013-03-22
      -- if there is a single case (such as for record splits)
      -- we force expansion
      if Bool
    single then Cl -> [Cl]
    doExpand (Cl -> [Cl]) -> [Cl] -> [Cl]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Cl]
    cs else
      case [Cl]
    cs of
      [Cl]
    _                | (Cl -> Bool) -> [Cl] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ([Arg (Pattern' PatVarName)] -> Bool
    isCatchAllNth ([Arg (Pattern' PatVarName)] -> Bool)
    -> (Cl -> [Arg (Pattern' PatVarName)]) -> Cl -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Cl -> [Arg (Pattern' PatVarName)]
    clPats) [Cl]
    cs -> [Cl]
    cs
      c :: Cl
    c@(Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b) : [Cl]
    cs | Bool -> Bool
    not ([Arg (Pattern' PatVarName)] -> Bool
    isCatchAllNth [Arg (Pattern' PatVarName)]
    ps) -> Cl
    c Cl -> [Cl] -> [Cl]
    forall a. a -> [a] -> [a]
    : Bool -> Int -> [Cl] -> [Cl]
    expandCatchAlls Bool
    False Int
    n [Cl]
    cs
                       | Bool
    otherwise -> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl)
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    -> [Cl]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cl
    -> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl
    expand Cl
    c) [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    expansions [Cl] -> [Cl] -> [Cl]
    forall a. [a] -> [a] -> [a]
    ++ Cl
    c Cl -> [Cl] -> [Cl]
    forall a. a -> [a] -> [a]
    : Bool -> Int -> [Cl] -> [Cl]
    expandCatchAlls Bool
    False Int
    n [Cl]
    cs
      [Cl]
    _ -> [Cl]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        -- In case there is only one branch in the split tree, we expand all
        -- catch-alls for this position
        -- The @expansions@ are collected from all the clauses @cs@ then.
        -- Note: @expansions@ could be empty, so we keep the orignal clause.
        doExpand :: Cl -> [Cl]
    doExpand c :: Cl
    c@(Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    _)
          | [Arg (Pattern' PatVarName)] -> Bool
    exCatchAllNth [Arg (Pattern' PatVarName)]
    ps = (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl)
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    -> [Cl]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cl
    -> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl
    expand Cl
    c) [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    expansions [Cl] -> [Cl] -> [Cl]
    forall a. [a] -> [a] -> [a]
    ++ [Cl
    c]
          | Bool
    otherwise = [Cl
    c]

        -- True if nth pattern is variable or there are less than n patterns.
        isCatchAllNth :: [Arg (Pattern' PatVarName)] -> Bool
    isCatchAllNth [Arg (Pattern' PatVarName)]
    ps = (Arg (Pattern' PatVarName) -> Bool)
    -> [Arg (Pattern' PatVarName)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Pattern' PatVarName -> Bool
    forall a. Pattern' a -> Bool
    isVar (Pattern' PatVarName -> Bool)
    -> (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
    -> Arg (Pattern' PatVarName)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg) ([Arg (Pattern' PatVarName)] -> Bool)
    -> [Arg (Pattern' PatVarName)] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    take Int
    1 ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Arg (Pattern' PatVarName)]
    ps

        -- True if nth pattern exists and is variable.
        exCatchAllNth :: [Arg (Pattern' PatVarName)] -> Bool
    exCatchAllNth [Arg (Pattern' PatVarName)]
    ps = (Arg (Pattern' PatVarName) -> Bool)
    -> [Arg (Pattern' PatVarName)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Pattern' PatVarName -> Bool
    forall a. Pattern' a -> Bool
    isVar (Pattern' PatVarName -> Bool)
    -> (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
    -> Arg (Pattern' PatVarName)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg) ([Arg (Pattern' PatVarName)] -> Bool)
    -> [Arg (Pattern' PatVarName)] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    take Int
    1 ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Arg (Pattern' PatVarName)]
    ps

        classify :: Pattern' x -> Either Literal (Either ConHead QName)
    classify (LitP PatternInfo
    _ Literal
    l)   = Literal -> Either Literal (Either ConHead QName)
    forall a b. a -> Either a b
    Left Literal
    l
        classify (ConP ConHead
    c ConPatternInfo
    _ [NamedArg (Pattern' x)]
    _) = Either ConHead QName -> Either Literal (Either ConHead QName)
    forall a b. b -> Either a b
    Right (ConHead -> Either ConHead QName
    forall a b. a -> Either a b
    Left ConHead
    c)
        classify (DefP PatternInfo
    _ QName
    q [NamedArg (Pattern' x)]
    _) = Either ConHead QName -> Either Literal (Either ConHead QName)
    forall a b. b -> Either a b
    Right (QName -> Either ConHead QName
    forall a b. b -> Either a b
    Right QName
    q)
        classify Pattern' x
    _            = Either Literal (Either ConHead QName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- All non-catch-all patterns following this one (at position n).
        -- These are the cases the wildcard needs to be expanded into.
        expansions :: [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    expansions = (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
     -> Either Literal (Either ConHead QName))
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn (Pattern' PatVarName -> Either Literal (Either ConHead QName)
    forall {x}. Pattern' x -> Either Literal (Either ConHead QName)
    classify (Pattern' PatVarName -> Either Literal (Either ConHead QName))
    -> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
        -> Pattern' PatVarName)
    -> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    -> Either Literal (Either ConHead QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
    -> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
        -> Arg (Pattern' PatVarName))
    -> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    -> Pattern' PatVarName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    -> Arg (Pattern' PatVarName)
    forall a b. (a, b) -> b
    snd)
                   ([([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
     -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
    -> ([Cl]
        -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
    -> [Cl]
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Cl
     -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)))
    -> [Cl]
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ([Arg (Pattern' PatVarName)]
    -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    notVarNth ([Arg (Pattern' PatVarName)]
     -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)))
    -> (Cl -> [Arg (Pattern' PatVarName)])
    -> Cl
    -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Cl -> [Arg (Pattern' PatVarName)]
    clPats)
                   ([Cl]
     -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
    -> [Cl]
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    forall a b. (a -> b) -> a -> b
    $ [Cl]
    cs
        notVarNth
          :: [Arg Pattern]
          -> Maybe ([Arg Pattern]  -- First @n@ patterns.
                   , Arg Pattern)  -- @n+1@st pattern, not a variable
        notVarNth :: [Arg (Pattern' PatVarName)]
    -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    notVarNth [Arg (Pattern' PatVarName)]
    ps = do
          let ([Arg (Pattern' PatVarName)]
    ps1, [Arg (Pattern' PatVarName)]
    ps2) = Int
    -> [Arg (Pattern' PatVarName)]
    -> ([Arg (Pattern' PatVarName)], [Arg (Pattern' PatVarName)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [Arg (Pattern' PatVarName)]
    ps
          Arg (Pattern' PatVarName)
    p <- [Arg (Pattern' PatVarName)] -> Maybe (Arg (Pattern' PatVarName))
    forall a. [a] -> Maybe a
    listToMaybe [Arg (Pattern' PatVarName)]
    ps2
          Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Pattern' PatVarName -> Bool
    forall a. Pattern' a -> Bool
    isVar (Pattern' PatVarName -> Bool) -> Pattern' PatVarName -> Bool
    forall a b. (a -> b) -> a -> b
    $ Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg Arg (Pattern' PatVarName)
    p
          ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Arg (Pattern' PatVarName)]
    ps1, Arg (Pattern' PatVarName)
    p)

        expand :: Cl
    -> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl
    expand Cl
    cl ([Arg (Pattern' PatVarName)]
    qs, Arg (Pattern' PatVarName)
    q) =
          case Arg (Pattern' PatVarName) -> Pattern' PatVarName
    forall e. Arg e -> e
    unArg Arg (Pattern' PatVarName)
    q of
            ConP ConHead
    c ConPatternInfo
    mt [NamedArg (Pattern' PatVarName)]
    qs' -> [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)
    q Arg (Pattern' PatVarName)
    -> Pattern' PatVarName -> Arg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' PatVarName)]
    -> Pattern' PatVarName
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    mt [NamedArg (Pattern' PatVarName)]
    conPArgs] [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1)
                                (Int -> Int -> SubstArg (Maybe Term) -> Maybe Term -> Maybe Term
    forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
    substBody Int
    n' Int
    m (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Arg Term]
    conArgs)) Maybe Term
    b)
              where
                ci :: ConInfo
    ci       = ConPatternInfo -> ConInfo
    fromConPatternInfo ConPatternInfo
    mt
                m :: Int
    m        = [NamedArg (Pattern' PatVarName)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg (Pattern' PatVarName)]
    qs'
                -- replace all direct subpatterns of q by _
                -- TODO Andrea: might need these to sometimes be IApply?
                conPArgs :: [NamedArg (Pattern' PatVarName)]
    conPArgs = (NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName))
    -> [NamedArg (Pattern' PatVarName)]
    -> [NamedArg (Pattern' PatVarName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName (Pattern' PatVarName)
     -> Named NamedName (Pattern' PatVarName))
    -> NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Named NamedName (Pattern' PatVarName)
    -> Pattern' PatVarName -> Named NamedName (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> PatVarName -> Pattern' PatVarName
    forall a. a -> Pattern' a
    varP PatVarName
    "_")) [NamedArg (Pattern' PatVarName)]
    qs'
                conArgs :: [Arg Term]
    conArgs  = (NamedArg (Pattern' PatVarName) -> Int -> Arg Term)
    -> [NamedArg (Pattern' PatVarName)] -> [Int] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ NamedArg (Pattern' PatVarName)
    q' Int
    i -> NamedArg (Pattern' PatVarName)
    q' NamedArg (Pattern' PatVarName) -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int -> Term
    var Int
    i) [NamedArg (Pattern' PatVarName)]
    qs' ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    m
            LitP PatternInfo
    i Literal
    l -> [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)
    q Arg (Pattern' PatVarName)
    -> Pattern' PatVarName -> Arg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> PatternInfo -> Literal -> Pattern' PatVarName
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP PatternInfo
    i Literal
    l] [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1) (Int -> Int -> SubstArg (Maybe Term) -> Maybe Term -> Maybe Term
    forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
    substBody Int
    n' Int
    0 (Literal -> Term
    Lit Literal
    l) Maybe Term
    b)
            DefP PatternInfo
    o QName
    d [NamedArg (Pattern' PatVarName)]
    qs' -> [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps0 [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)
    q Arg (Pattern' PatVarName)
    -> Pattern' PatVarName -> Arg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> PatternInfo
    -> QName -> [NamedArg (Pattern' PatVarName)] -> Pattern' PatVarName
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    o QName
    d [NamedArg (Pattern' PatVarName)]
    conPArgs] [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps1)
                                (Int -> Int -> SubstArg (Maybe Term) -> Maybe Term -> Maybe Term
    forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
    substBody Int
    n' Int
    m (QName -> Elims -> Term
    Def QName
    d ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Arg Term]
    conArgs)) Maybe Term
    b)
              where
                m :: Int
    m        = [NamedArg (Pattern' PatVarName)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg (Pattern' PatVarName)]
    qs'
                -- replace all direct subpatterns of q by _
                conPArgs :: [NamedArg (Pattern' PatVarName)]
    conPArgs = (NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName))
    -> [NamedArg (Pattern' PatVarName)]
    -> [NamedArg (Pattern' PatVarName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName (Pattern' PatVarName)
     -> Named NamedName (Pattern' PatVarName))
    -> NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Named NamedName (Pattern' PatVarName)
    -> Pattern' PatVarName -> Named NamedName (Pattern' PatVarName)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> PatVarName -> Pattern' PatVarName
    forall a. a -> Pattern' a
    varP PatVarName
    "_")) [NamedArg (Pattern' PatVarName)]
    qs'
                conArgs :: [Arg Term]
    conArgs  = (NamedArg (Pattern' PatVarName) -> Int -> Arg Term)
    -> [NamedArg (Pattern' PatVarName)] -> [Int] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ NamedArg (Pattern' PatVarName)
    q' Int
    i -> NamedArg (Pattern' PatVarName)
    q' NamedArg (Pattern' PatVarName) -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int -> Term
    var Int
    i) [NamedArg (Pattern' PatVarName)]
    qs' ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    m
            Pattern' PatVarName
    _ -> Cl
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          where
            -- Andreas, 2016-09-19 issue #2168
            -- Due to varying function arity, some clauses might be eta-contracted.
            -- Thus, we eta-expand them.
            Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b = Int -> [ArgInfo] -> Cl -> Cl
    ensureNPatterns (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) ((Arg (Pattern' PatVarName) -> ArgInfo)
    -> [Arg (Pattern' PatVarName)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Pattern' PatVarName) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo ([Arg (Pattern' PatVarName)] -> [ArgInfo])
    -> [Arg (Pattern' PatVarName)] -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ [Arg (Pattern' PatVarName)]
    qs [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)
    q]) Cl
    cl
            -- The following pattern match cannot fail (by construction of @ps@).
            ([Arg (Pattern' PatVarName)]
    ps0, Arg (Pattern' PatVarName)
    _:[Arg (Pattern' PatVarName)]
    ps1) = Int
    -> [Arg (Pattern' PatVarName)]
    -> ([Arg (Pattern' PatVarName)], [Arg (Pattern' PatVarName)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [Arg (Pattern' PatVarName)]
    ps

            n' :: Int
    n' = [Arg (Pattern' PatVarName)] -> Int
    forall a. CountPatternVars a => a -> Int
    countPatternVars [Arg (Pattern' PatVarName)]
    ps1

    -- | Make sure (by eta-expansion) that clause has arity at least @n@
    --   where @n@ is also the length of the provided list.
    ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
    ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
    ensureNPatterns Int
    n [ArgInfo]
    ais0 cl :: Cl
    cl@(Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b)
      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0    = Cl
    cl
      | Bool
    otherwise = [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
    Cl ([Arg (Pattern' PatVarName)]
    ps [Arg (Pattern' PatVarName)]
    -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Pattern' PatVarName)]
    ps') (Int -> Maybe Term -> Maybe Term
    forall a. Subst a => Int -> a -> a
    raise Int
    m Maybe Term
    b Maybe Term -> [Arg Term] -> Maybe Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    args)
      where
      k :: Int
    k    = [Arg (Pattern' PatVarName)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg (Pattern' PatVarName)]
    ps
      ais :: [ArgInfo]
    ais  = Int -> [ArgInfo] -> [ArgInfo]
    forall a. Int -> [a] -> [a]
    drop Int
    k [ArgInfo]
    ais0
      -- m = Number of arguments to add
      m :: Int
    m    = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k
      ps' :: [Arg (Pattern' PatVarName)]
    ps'  = [ArgInfo]
    -> (ArgInfo -> Arg (Pattern' PatVarName))
    -> [Arg (Pattern' PatVarName)]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [ArgInfo]
    ais ((ArgInfo -> Arg (Pattern' PatVarName))
     -> [Arg (Pattern' PatVarName)])
    -> (ArgInfo -> Arg (Pattern' PatVarName))
    -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> a -> b
    $ \ ArgInfo
    ai -> ArgInfo -> Pattern' PatVarName -> Arg (Pattern' PatVarName)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Pattern' PatVarName -> Arg (Pattern' PatVarName))
    -> Pattern' PatVarName -> Arg (Pattern' PatVarName)
    forall a b. (a -> b) -> a -> b
    $ PatVarName -> Pattern' PatVarName
    forall a. a -> Pattern' a
    varP PatVarName
    "_"
      args :: [Arg Term]
    args = (Int -> ArgInfo -> Arg Term) -> [Int] -> [ArgInfo] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Int
    i ArgInfo
    ai -> 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
    $ Int -> Term
    var Int
    i) (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    m) [ArgInfo]
    ais

    substBody :: Subst a => Int -> Int -> SubstArg a -> a -> a
    substBody :: forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
    substBody Int
    n Int
    m SubstArg a
    v = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution' (SubstArg a) -> a -> a)
    -> Substitution' (SubstArg a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ Int -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n (Substitution' (SubstArg a) -> Substitution' (SubstArg a))
    -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a b. (a -> b) -> a -> b
    $ SubstArg a
    v SubstArg a
    -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a. a -> Substitution' a -> Substitution' a
    :# Int -> Substitution' (SubstArg a)
    forall a. Int -> Substitution' a
    raiseS Int
    m

    instance PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) where