    {-# OPTIONS_GHC -Wunused-imports #-}

    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 Data.List (partition)
    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.Syntax.Common.Pretty as P
    import Agda.Utils.Size
    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
    $c== :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    == :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    $c/= :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    /= :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
    Eq)

    compileClauses' :: QName -> RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
    compileClauses' :: QName
    -> RunRecordPatternTranslation
    -> [Clause]
    -> Maybe SplitTree
    -> TCM CompiledClauses
    compileClauses' QName
    q 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
      cs <- (Clause -> Cl) -> [Clause] -> Cls
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> Cl
    unBruijn ([Clause] -> Cls) -> TCMT IO [Clause] -> TCMT IO Cls
    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
    forall (m :: * -> *). HasConstInfo m => [Clause] -> m [Clause]
    normaliseProjP ((Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Clause -> Bool
    notUnreachable [Clause]
    cs)

      let 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
    . QName -> CompiledClauses -> IdentityT (TCMT IO) CompiledClauses
    forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    QName -> CompiledClauses -> m CompiledClauses
    translateCompiledClauses QName
    q
                    | Bool
    otherwise                             = CompiledClauses -> TCM CompiledClauses
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

      translate $ caseMaybe mSplitTree (compile cs) $ \SplitTree
    splitTree ->
        SplitTree -> Cls -> CompiledClauses
    compileWithSplitTree SplitTree
    splitTree Cls
    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
    . Cls -> CompiledClauses
    compile (Cls -> CompiledClauses)
    -> ([Clause] -> Cls) -> [Clause] -> CompiledClauses
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Clause -> Cl) -> [Clause] -> Cls
    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
    forall (m :: * -> *). HasConstInfo m => [Clause] -> m [Clause]
    normaliseProjP [Clause]
    cs
        Just (QName
    q, Type
    t)  -> do
          splitTree <- QName -> Type -> [Clause] -> TCM SplitTree
    coverageCheck QName
    q Type
    t [Clause]
    cs

          reportSDoc "tc.cc.tree" 20 $ vcat
            [ "split tree of " <+> prettyTCM q <+> " from coverage check "
            , return $ P.pretty splitTree
            ]

          -- The coverage checker might have added some clauses (#2288)!
          -- Throw away the unreachable clauses (#2723).
          let 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
          cs <- normaliseProjP =<< instantiateFull =<< filter notUnreachable . defClauses <$> getConstInfo q

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

          reportSDoc "tc.cc" 30 $ sep $ do
            ("clauses patterns of " <+> prettyTCM q <+> " before compilation") : do
              map (prettyTCM . map unArg . clPats) cls
          reportSDoc "tc.cc" 50 $
            "clauses of " <+> prettyTCM q <+> " before compilation" <?> pretty cs

          let cc = SplitTree -> Cls -> CompiledClauses
    compileWithSplitTree SplitTree
    splitTree Cls
    cls
          reportSDoc "tc.cc" 20 $ sep
            [ "compiled clauses of " <+> prettyTCM q <+> " (still containing record splits)"
            , nest 2 $ return $ P.pretty cc
            ]

          (cc, becameCopatternLHS) <- runChangeT $ translateCompiledClauses q cc

          reportSDoc "tc.cc" 12 $ sep
            [ "compiled clauses of " <+> prettyTCM q
            , nest 2 $ return $ P.pretty cc
            ]
          return (Just splitTree, becameCopatternLHS, fmap precomputeFreeVars_ 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
    Cls -> ShowS
    Cl -> PatVarName
    (Int -> Cl -> ShowS)
    -> (Cl -> PatVarName) -> (Cls -> ShowS) -> Show Cl
    forall a.
    (Int -> a -> ShowS)
    -> (a -> PatVarName) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Cl -> ShowS
    showsPrec :: Int -> Cl -> ShowS
    $cshow :: Cl -> PatVarName
    show :: Cl -> PatVarName
    $cshowList :: Cls -> ShowS
    showList :: Cls -> 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
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    "->" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    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
    $ ((NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName))
    -> [NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName))
     -> [NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)])
    -> ((Named_ DeBruijnPattern -> Pattern' PatVarName)
        -> NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName))
    -> (Named_ DeBruijnPattern -> Pattern' PatVarName)
    -> [NamedArg DeBruijnPattern]
    -> [Arg (Pattern' PatVarName)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named_ DeBruijnPattern -> Pattern' PatVarName)
    -> NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) ((DBPatVar -> PatVarName) -> DeBruijnPattern -> Pattern' PatVarName
    forall a b. (a -> b) -> Pattern' a -> Pattern' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DBPatVar -> PatVarName
    dbPatVarName (DeBruijnPattern -> Pattern' PatVarName)
    -> (Named_ DeBruijnPattern -> DeBruijnPattern)
    -> Named_ DeBruijnPattern
    -> Pattern' PatVarName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named_ DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing) ([NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)])
    -> [NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)]
    forall a b. (a -> b) -> a -> b
    $ Clause -> [NamedArg DeBruijnPattern]
    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 -> Cls -> CompiledClauses
    compileWithSplitTree SplitTree
    t Cls
    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 Cls -> Case CompiledClauses
    compiles LazySplit
    lz SplitTrees' SplitTag
    ts (Case Cls -> Case CompiledClauses)
    -> Case Cls -> Case CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Cls -> Case Cls
    splitOn (SplitTrees' SplitTag -> Peano
    forall a. Sized a => a -> Peano
    natSize SplitTrees' SplitTag
    ts Peano -> Peano -> Bool
    forall a. Eq a => a -> a -> Bool
    == Peano
    1) (Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    i) Cls
    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 -> Cls -> CompiledClauses
    compile Cls
    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 Cls -> Case CompiledClauses
    compiles LazySplit
    lz SplitTrees' SplitTag
    ts br :: Case Cls
    br@Branches{ projPatterns :: forall c. Case c -> Bool
    projPatterns = Bool
    cop
                                  , conBranches :: forall c. Case c -> Map QName (WithArity c)
    conBranches = Map QName (WithArity Cls)
    cons
                                  , etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
    etaBranch   = Maybe (ConHead, WithArity Cls)
    Nothing
                                  , litBranches :: forall c. Case c -> Map Literal c
    litBranches = Map Literal Cls
    lits
                                  , fallThrough :: forall c. Case c -> Maybe Bool
    fallThrough = Maybe Bool
    fT
                                  , catchallBranch :: forall c. Case c -> Maybe c
    catchallBranch = Maybe Cls
    catchall
                                  , lazyMatch :: forall c. Case c -> Bool
    lazyMatch = Bool
    lazy }
          = Case Cls
    br{ conBranches    = updCons cons
              , etaBranch      = Nothing
              , litBranches    = updLits lits
              , fallThrough    = fT
              , catchallBranch = updCatchall catchall
              , lazyMatch      = lazy || lz == LazySplit
              }
          where
            updCons :: Map QName (WithArity Cls) -> Map QName (WithArity CompiledClauses)
    updCons = (QName -> WithArity Cls -> WithArity CompiledClauses)
    -> Map QName (WithArity Cls)
    -> Map QName (WithArity CompiledClauses)
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey ((QName -> WithArity Cls -> WithArity CompiledClauses)
     -> Map QName (WithArity Cls)
     -> Map QName (WithArity CompiledClauses))
    -> (QName -> WithArity Cls -> WithArity CompiledClauses)
    -> Map QName (WithArity Cls)
    -> Map QName (WithArity CompiledClauses)
    forall a b. (a -> b) -> a -> b
    $ \ QName
    c WithArity Cls
    cl ->
             Maybe SplitTree
    -> (Cls -> CompiledClauses)
    -> (SplitTree -> Cls -> CompiledClauses)
    -> Cls
    -> 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) Cls -> CompiledClauses
    compile SplitTree -> Cls -> CompiledClauses
    compileWithSplitTree (Cls -> CompiledClauses)
    -> WithArity Cls -> WithArity CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> WithArity Cls
    cl
             -- When the split tree is finished, we continue with @compile@.
            updLits :: Map Literal Cls -> Map Literal CompiledClauses
    updLits = (Literal -> Cls -> CompiledClauses)
    -> Map Literal Cls -> Map Literal CompiledClauses
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey ((Literal -> Cls -> CompiledClauses)
     -> Map Literal Cls -> Map Literal CompiledClauses)
    -> (Literal -> Cls -> CompiledClauses)
    -> Map Literal Cls
    -> Map Literal CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ \ Literal
    l Cls
    cl ->
              Maybe SplitTree
    -> (Cls -> CompiledClauses)
    -> (SplitTree -> Cls -> CompiledClauses)
    -> Cls
    -> 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) Cls -> CompiledClauses
    compile SplitTree -> Cls -> CompiledClauses
    compileWithSplitTree Cls
    cl
            updCatchall :: Maybe Cls -> Maybe CompiledClauses
    updCatchall = (Cls -> CompiledClauses) -> Maybe Cls -> Maybe CompiledClauses
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Cls -> CompiledClauses) -> Maybe Cls -> Maybe CompiledClauses)
    -> (Cls -> CompiledClauses) -> Maybe Cls -> Maybe CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Maybe SplitTree
    -> (Cls -> CompiledClauses)
    -> (SplitTree -> Cls -> CompiledClauses)
    -> Cls
    -> 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) Cls -> CompiledClauses
    compile SplitTree -> Cls -> 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 :: Cls -> CompiledClauses
    compile [] = [Arg PatVarName] -> CompiledClauses
    forall a. [Arg PatVarName] -> CompiledClauses' a
    Fail []
    compile Cls
    cs = case Cls -> Maybe (Bool, Arg Int)
    nextSplit Cls
    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
    $ Cls -> CompiledClauses
    compile (Cls -> CompiledClauses) -> Case Cls -> Case CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> Int -> Cls -> Case Cls
    splitOn Bool
    isRecP (Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    n) Cls
    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 a b. (a -> b) -> Arg a -> Arg b
    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 a b. (a -> b) -> Arg a -> Arg b
    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 -> Cls -> Cl
    forall a. a -> [a] -> a
    headWithDefault Cl
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Cls
    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 :: Cls -> Maybe (Bool, Arg Int)
    nextSplit []             = Maybe (Bool, Arg Int)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    nextSplit (Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    _ : Cls
    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 a. Maybe a -> Maybe a -> Maybe a
    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 a b. Maybe a -> Maybe b -> Maybe a
    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) -> Cls -> 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) Cls
    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 -> Cls -> Case Cls
    splitOn Bool
    single Int
    n Cls
    cs = [Case Cls] -> Case Cls
    forall a. Monoid a => [a] -> a
    mconcat ([Case Cls] -> Case Cls) -> [Case Cls] -> Case Cls
    forall a b. (a -> b) -> a -> b
    $ (Cl -> Case Cls) -> Cls -> [Case Cls]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Cl -> Cls) -> Case Cl -> Case Cls
    forall a b. (a -> b) -> Case a -> Case b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Cl -> Cls -> Cls
    forall a. a -> [a] -> [a]
    :[]) (Case Cl -> Case Cls) -> (Cl -> Case Cl) -> Cl -> Case Cls
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Cl -> Case Cl
    splitC Int
    n) (Cls -> [Case Cls]) -> Cls -> [Case Cls]
    forall a b. (a -> b) -> a -> b
    $
      -- (\ cs -> trace ("splitting on " ++ show n ++ " after expandCatchalls " ++ show single ++ ": " ++ prettyShow (P.prettyList cs)) cs) $
        Bool -> Int -> Cls -> Cls
    expandCatchalls Bool
    single Int
    n Cls
    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 a. [a] -> 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 a b. (a -> b) -> Arg a -> Arg b
    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 = conPLazy 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 a. [a] -> 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 a b. (a -> b) -> Arg a -> Arg b
    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 = 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 -> Cls -> Cls
    expandCatchalls Bool
    single Int
    n Cls
    cs =
      case Cls
    cs of
        Cls
    _ -- Andreas, 2013-03-22
          -- if there is a single case (such as for record splits)
          -- we force expansion
          | Bool
    single -> Cl -> Cls
    doExpand (Cl -> Cls) -> Cls -> Cls
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Cls
    cs

          -- If all clauses have a variable at the nth argument, expansion
          -- would have no effect
          | (Cl -> Bool) -> Cls -> 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) Cls
    cs -> Cls
    cs

        c :: Cl
    c@(Cl [Arg (Pattern' PatVarName)]
    ps Maybe Term
    b):Cls
    cs
          -- If the head clause does not have a catch-all pattern for the
          -- nth argument, we can keep it at the head and do no expansion
          | Bool -> Bool
    not ([Arg (Pattern' PatVarName)] -> Bool
    isCatchallNth [Arg (Pattern' PatVarName)]
    ps) -> Cl
    c Cl -> Cls -> Cls
    forall a. a -> [a] -> [a]
    : Bool -> Int -> Cls -> Cls
    expandCatchalls Bool
    False Int
    n Cls
    cs

          -- If there's a DefP clause for this argument later on, then it
          -- should take priority over catch-all clauses, so we rotate them
          -- out of the way.
          -- DefP clauses are always inserted by the system and should
          -- "defeat" user-written inexact patterns.
          | (defps :: Cls
    defps@(Cl
    _:Cls
    _), Cls
    rest) <- (Cl -> Bool) -> Cls -> (Cls, Cls)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Cl -> Bool
    isDefPNth (Cl
    cCl -> Cls -> Cls
    forall a. a -> [a] -> [a]
    :Cls
    cs)
          -> Cls
    defps Cls -> Cls -> Cls
    forall a. [a] -> [a] -> [a]
    ++ Bool -> Int -> Cls -> Cls
    expandCatchalls Bool
    False Int
    n Cls
    rest

          -- If the head clause *does* have an irrefutable pattern for the
          -- nth argument, and there's nothing more important after, then we
          -- duplicate the subsequent overlapping clauses with c's RHS
          -- instead.
          | Bool
    otherwise -> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl)
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    -> Cls
    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 Cls -> Cls -> Cls
    forall a. [a] -> [a] -> [a]
    ++ Cl
    c Cl -> Cls -> Cls
    forall a. a -> [a] -> [a]
    : Bool -> Int -> Cls -> Cls
    expandCatchalls Bool
    False Int
    n Cls
    cs
        Cls
    _ -> Cls
    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 -> Cls
    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))]
    -> Cls
    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 Cls -> Cls -> Cls
    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__

        isDefPNth :: Cl -> Bool
    isDefPNth Cl
    cl = case 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 (Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
    forall a. Int -> [a] -> [a]
    drop Int
    n (Cl -> [Arg (Pattern' PatVarName)]
    clPats Cl
    cl)) of
          Just DefP{} -> Bool
    True
          Maybe (Pattern' PatVarName)
    _ -> Bool
    False

        -- 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))])
    -> (Cls
        -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
    -> Cls
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Cl
     -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)))
    -> Cls
    -> [([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)
                   (Cls -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
    -> Cls
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
    forall a b. (a -> b) -> a -> b
    $ Cls
    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
          p <- [Arg (Pattern' PatVarName)] -> Maybe (Arg (Pattern' PatVarName))
    forall a. [a] -> Maybe a
    listToMaybe [Arg (Pattern' PatVarName)]
    ps2
          guard $ not $ isVar $ unArg p
          return (ps1, 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) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    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 a. [a] -> 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 a b. (a -> b) -> Arg a -> Arg b
    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) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply [Arg Term]
    conArgs)) Maybe Term
    b)
              where
                m :: Int
    m        = [NamedArg (Pattern' PatVarName)] -> Int
    forall a. [a] -> 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 a b. (a -> b) -> Arg a -> Arg b
    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 a. [a] -> 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