    module Agda.Auto.CaseSplit where

    import Control.Monad.State as St hiding (lift)
    import Control.Monad.Reader as Rd hiding (lift)
    import qualified Control.Monad.State as St
    import Control.Monad.IO.Class ( MonadIO(..) )

    import Data.Function
    import Data.IORef
    import Data.Tuple (swap)
    import Data.List (elemIndex)
    -- Import of <> needed for 8.2.2, but redundant in 8.8.3
    import Data.Monoid ((<>), Sum(..))
    import qualified Data.Set    as Set
    import qualified Data.IntMap as IntMap

    import Agda.Syntax.Common (Hiding(..))
    import Agda.Auto.NarrowingSearch
    import Agda.Auto.Syntax

    import Agda.Auto.SearchControl
    import Agda.Auto.Typecheck

    import Agda.Utils.Impossible
    import Agda.Utils.Monad (or2M)
    import Agda.Utils.List (last1)

    abspatvarname :: String
    abspatvarname :: String
    abspatvarname = String
    "\0absurdPattern"

    costCaseSplitVeryHigh, costCaseSplitHigh, costCaseSplitLow, costAddVarDepth
      :: Cost
    costCaseSplitVeryHigh :: Cost
    costCaseSplitVeryHigh = Cost
    10000
    costCaseSplitHigh :: Cost
    costCaseSplitHigh     = Cost
    5000
    costCaseSplitLow :: Cost
    costCaseSplitLow      = Cost
    2000
    costAddVarDepth :: Cost
    costAddVarDepth       = Cost
    1000

    data HI a = HI Hiding a

    drophid :: [HI a] -> [a]
    drophid :: forall a. [HI a] -> [a]
    drophid = (HI a -> a) -> [HI a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(HI Hiding
    _ a
    x) -> a
    x)

    type CSPat o = HI (CSPatI o)
    type CSCtx o = [HI (MId, MExp o)]

    data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]
                  | CSPatVar Nat
                  | CSPatExp (MExp o)
                  | CSWith (MExp o) -- always an App
                  | CSAbsurd

                  | CSOmittedArg
    type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]

    caseSplitSearch ::
      forall o . IORef Int -> Int -> [ConstRef o] ->
      Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o ->
      CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
    caseSplitSearch :: forall o.
    IORef Nat
    -> Nat
    -> [ConstRef o]
    -> Maybe (EqReasoningConsts o)
    -> Nat
    -> Cost
    -> ConstRef o
    -> CSCtx o
    -> MExp o
    -> [CSPat o]
    -> IO [Sol o]
    caseSplitSearch IORef Nat
    ticks Nat
    nsolwanted [ConstRef o]
    chints Maybe (EqReasoningConsts o)
    meqr Nat
    depthinterval Cost
    depth ConstRef o
    recdef CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats = do
     let branchsearch :: Cost -> CSCtx o -> MExp o ->
                         ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
         branchsearch :: Cost
    -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
    branchsearch Cost
    depth CSCtx o
    ctx MExp o
    tt ([Nat], Nat, [Nat])
    termcheckenv = do

          IORef Nat
    nsol <- Nat -> IO (IORef Nat)
    forall a. a -> IO (IORef a)
    newIORef Nat
    1
          Metavar (Exp o) (RefInfo o)
    m <- IO (Metavar (Exp o) (RefInfo o))
    forall a blk. IO (Metavar a blk)
    initMeta
          IORef (Maybe (MExp o))
    sol <- Maybe (MExp o) -> IO (IORef (Maybe (MExp o)))
    forall a. a -> IO (IORef a)
    newIORef Maybe (MExp o)
    forall a. Maybe a
    Nothing
          let trm :: MExp o
    trm = Metavar (Exp o) (RefInfo o) -> MExp o
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar (Exp o) (RefInfo o)
    m
              hsol :: IO ()
    hsol = do MExp o
    trm' <- MExp o -> IO (MExp o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MExp o
    trm
                        IORef (Maybe (MExp o)) -> Maybe (MExp o) -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef (Maybe (MExp o))
    sol (MExp o -> Maybe (MExp o)
    forall a. a -> Maybe a
    Just MExp o
    trm')
              initcon :: MetaEnv (PB (RefInfo o))
    initcon = Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret
                      (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
    Sidecondition
                        (([Nat], Nat, [Nat])
    -> ConstRef o -> MExp o -> MetaEnv (PB (RefInfo o))
    forall o.
    ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
    localTerminationSidecond ([Nat], Nat, [Nat])
    termcheckenv ConstRef o
    recdef MExp o
    trm)
                      (MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall a b. (a -> b) -> a -> b
    $ (case Maybe (EqReasoningConsts o)
    meqr of
                            Maybe (EqReasoningConsts o)
    Nothing  -> MetaEnv (PB (RefInfo o)) -> MetaEnv (PB (RefInfo o))
    forall a. a -> a
    id
                            Just EqReasoningConsts o
    eqr -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> (MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o))
    -> MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
    Sidecondition (EqReasoningConsts o -> MExp o -> MetaEnv (PB (RefInfo o))
    forall o. EqReasoningConsts o -> MExp o -> EE (MyPB o)
    calcEqRState EqReasoningConsts o
    eqr MExp o
    trm)
                         ) (MetaEnv (PB (RefInfo o)) -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o)) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ Bool -> Ctx o -> CExp o -> MExp o -> MetaEnv (PB (RefInfo o))
    forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
    tcSearch Bool
    False (((MId, MExp o) -> (MId, CExp o)) -> [(MId, MExp o)] -> Ctx o
    forall a b. (a -> b) -> [a] -> [b]
    map ((MExp o -> CExp o) -> (MId, MExp o) -> (MId, CExp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap MExp o -> CExp o
    forall o. MExp o -> CExp o
    closify) (CSCtx o -> [(MId, MExp o)]
    forall a. [HI a] -> [a]
    drophid CSCtx o
    ctx))
                             (MExp o -> CExp o
    forall o. MExp o -> CExp o
    closify MExp o
    tt) MExp o
    trm
          ConstDef o
    recdefd <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    recdef
          let env :: RefInfo o
    env = RIEnv :: forall o.
    [(ConstRef o, HintMode)]
    -> Nat -> Maybe (EqReasoningConsts o) -> RefInfo o
    RIEnv { rieHints :: [(ConstRef o, HintMode)]
    rieHints = (ConstRef o
    recdef, HintMode
    HMRecCall) (ConstRef o, HintMode)
    -> [(ConstRef o, HintMode)] -> [(ConstRef o, HintMode)]
    forall a. a -> [a] -> [a]
    : (ConstRef o -> (ConstRef o, HintMode))
    -> [ConstRef o] -> [(ConstRef o, HintMode)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, HintMode
    HMNormal) [ConstRef o]
    chints
                          , rieDefFreeVars :: Nat
    rieDefFreeVars = ConstDef o -> Nat
    forall o. ConstDef o -> Nat
    cddeffreevars ConstDef o
    recdefd
                          , rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
    rieEqReasoningConsts = Maybe (EqReasoningConsts o)
    meqr
                          }
          Bool
    depreached <- IORef Nat
    -> IORef Nat
    -> IO ()
    -> RefInfo o
    -> MetaEnv (PB (RefInfo o))
    -> Cost
    -> Cost
    -> IO Bool
    forall blk.
    IORef Nat
    -> IORef Nat
    -> IO ()
    -> blk
    -> MetaEnv (PB blk)
    -> Cost
    -> Cost
    -> IO Bool
    topSearch IORef Nat
    ticks IORef Nat
    nsol IO ()
    hsol RefInfo o
    env MetaEnv (PB (RefInfo o))
    initcon Cost
    depth (Cost
    depth Cost -> Cost -> Cost
    forall a. Num a => a -> a -> a
    + Cost
    1)
          IORef (Maybe (MExp o)) -> IO (Maybe (MExp o))
    forall a. IORef a -> IO a
    readIORef IORef (Maybe (MExp o))
    sol
         ctx' :: CSCtx o
    ctx' = Nat -> CSCtx o -> CSCtx o
    forall {b} {a}. Lift b => Nat -> [HI (a, b)] -> [HI (a, b)]
    ff Nat
    1 CSCtx o
    ctx
         ff :: Nat -> [HI (a, b)] -> [HI (a, b)]
    ff Nat
    _ [] = []
         ff Nat
    n (HI Hiding
    hid (a
    id, b
    t) : [HI (a, b)]
    ctx) = Hiding -> (a, b) -> HI (a, b)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (a
    id, Nat -> b -> b
    forall t. Lift t => Nat -> t -> t
    lift Nat
    n b
    t) HI (a, b) -> [HI (a, b)] -> [HI (a, b)]
    forall a. a -> [a] -> [a]
    : Nat -> [HI (a, b)] -> [HI (a, b)]
    ff (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [HI (a, b)]
    ctx
     (Cost
     -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
    -> Nat
    -> Cost
    -> ConstRef o
    -> CSCtx o
    -> MExp o
    -> [CSPat o]
    -> IO [Sol o]
    forall o.
    (Cost
     -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
    -> Nat
    -> Cost
    -> ConstRef o
    -> CSCtx o
    -> MExp o
    -> [CSPat o]
    -> IO [Sol o]
    caseSplitSearch' Cost
    -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
    branchsearch Nat
    depthinterval Cost
    depth ConstRef o
    recdef CSCtx o
    ctx' MExp o
    tt [CSPat o]
    pats

    caseSplitSearch' :: forall o .
      (Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) ->
      Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
    caseSplitSearch' :: forall o.
    (Cost
     -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
    -> Nat
    -> Cost
    -> ConstRef o
    -> CSCtx o
    -> MExp o
    -> [CSPat o]
    -> IO [Sol o]
    caseSplitSearch' Cost
    -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
    branchsearch Nat
    depthinterval Cost
    depth ConstRef o
    recdef CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats = do
      ConstDef o
    recdefd <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    recdef
      Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
    rc Cost
    depth (ConstDef o -> Nat
    forall o. ConstDef o -> Nat
    cddeffreevars ConstDef o
    recdefd) CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats
     where
      rc :: Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
      rc :: Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
    rc Cost
    depth Nat
    _ CSCtx o
    _ MExp o
    _ [CSPat o]
    _ | Cost
    depth Cost -> Cost -> Bool
    forall a. Ord a => a -> a -> Bool
    < Cost
    0 = [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      rc Cost
    depth Nat
    nscrutavoid CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats = do

        [Nat]
    mblkvar <- MExp o -> IO [Nat]
    forall o. MExp o -> IO [Nat]
    getblks MExp o
    tt
        [Nat] -> IO [Sol o]
    fork
         [Nat]
    mblkvar
       where
       fork :: [Nat] -> IO [Sol o]
       fork :: [Nat] -> IO [Sol o]
    fork [Nat]
    mblkvar = do
        [Sol o]
    sols1 <- IO [Sol o]
    dobody
        case [Sol o]
    sols1 of
         (Sol o
    _:[Sol o]
    _) -> [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Sol o]
    sols1
         [] -> do
          let r :: [Nat] -> IO [Sol o]
              r :: [Nat] -> IO [Sol o]
    r [] = [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
              r (Nat
    v:[Nat]
    vs) = do
               [Sol o]
    sols2 <- [Nat] -> Nat -> IO [Sol o]
    splitvar [Nat]
    mblkvar Nat
    v
               case [Sol o]
    sols2 of
                (Sol o
    _:[Sol o]
    _) -> [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Sol o]
    sols2
                [] -> [Nat] -> IO [Sol o]
    r [Nat]
    vs
          [Nat] -> IO [Sol o]
    r [Nat
    nv Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    x | Nat
    x <- [Nat
    0..Nat
    nv]] -- [0..length ctx - 1 - nscrutavoid]
        where nv :: Nat
    nv = CSCtx o -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length CSCtx o
    ctx Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1
       dobody :: IO [Sol o]
       dobody :: IO [Sol o]
    dobody = do
        case [MExp o] -> Maybe [Nat]
    forall o. [MExp o] -> Maybe [Nat]
    findperm (((MId, MExp o) -> MExp o) -> [(MId, MExp o)] -> [MExp o]
    forall a b. (a -> b) -> [a] -> [b]
    map (MId, MExp o) -> MExp o
    forall a b. (a, b) -> b
    snd (CSCtx o -> [(MId, MExp o)]
    forall a. [HI a] -> [a]
    drophid CSCtx o
    ctx)) of
         Just [Nat]
    perm -> do
          let (CSCtx o
    ctx', MExp o
    tt', [CSPat o]
    pats') = [Nat]
    -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
    forall o.
    [Nat]
    -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
    applyperm [Nat]
    perm CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats
          Maybe (MExp o)
    res <- Cost
    -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
    branchsearch Cost
    depth CSCtx o
    ctx' MExp o
    tt' ([CSPat o] -> ([Nat], Nat, [Nat])
    forall o. [CSPat o] -> ([Nat], Nat, [Nat])
    localTerminationEnv [CSPat o]
    pats')
          [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Sol o] -> IO [Sol o]) -> [Sol o] -> IO [Sol o]
    forall a b. (a -> b) -> a -> b
    $ case Maybe (MExp o)
    res of
           Just MExp o
    trm -> [[(CSCtx o
    ctx', [CSPat o]
    pats', MExp o -> Maybe (MExp o)
    forall a. a -> Maybe a
    Just MExp o
    trm)]]
           Maybe (MExp o)
    Nothing -> []
         Maybe [Nat]
    Nothing -> IO [Sol o]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- no permutation found
       splitvar :: [Nat] -> Nat -> IO [Sol o]
       splitvar :: [Nat] -> Nat -> IO [Sol o]
    splitvar [Nat]
    mblkvar Nat
    scrut = do
        let scruttype :: MExp o
    scruttype = CSCtx o -> Nat -> MExp o
    forall o. CSCtx o -> Nat -> MExp o
    infertypevar CSCtx o
    ctx Nat
    scrut
        case Empty -> MExp o -> Exp o
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MExp o
    scruttype of
         App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Const ConstRef o
    c) MArgList o
    _ -> do
          ConstDef o
    cd <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c
          case ConstDef o -> DeclCont o
    forall o. ConstDef o -> DeclCont o
    cdcont ConstDef o
    cd of
           Datatype [ConstRef o]
    cons [ConstRef o]
    _ -> do
             [Sol o]
    sols <- [ConstRef o] -> IO [Sol o]
    dobranches [ConstRef o]
    cons
             [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Sol o] -> IO [Sol o]) -> [Sol o] -> IO [Sol o]
    forall a b. (a -> b) -> a -> b
    $ (Sol o -> Sol o) -> [Sol o] -> [Sol o]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Sol o
    sol -> case Sol o
    sol of
              [] ->
               case [MExp o] -> Maybe [Nat]
    forall o. [MExp o] -> Maybe [Nat]
    findperm (((MId, MExp o) -> MExp o) -> [(MId, MExp o)] -> [MExp o]
    forall a b. (a -> b) -> [a] -> [b]
    map (MId, MExp o) -> MExp o
    forall a b. (a, b) -> b
    snd (CSCtx o -> [(MId, MExp o)]
    forall a. [HI a] -> [a]
    drophid CSCtx o
    ctx)) of
                Just [Nat]
    perm ->
                 let HI Hiding
    scrhid(MId
    _, MExp o
    scrt) = CSCtx o
    ctx CSCtx o -> Nat -> HI (MId, MExp o)
    forall a. [a] -> Nat -> a
    !! Nat
    scrut
                     ctx1 :: CSCtx o
    ctx1 = Nat -> CSCtx o -> CSCtx o
    forall a. Nat -> [a] -> [a]
    take Nat
    scrut CSCtx o
    ctx CSCtx o -> CSCtx o -> CSCtx o
    forall a. [a] -> [a] -> [a]
    ++ (Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    scrhid (String -> MId
    Id String
    abspatvarname, MExp o
    scrt)) HI (MId, MExp o) -> CSCtx o -> CSCtx o
    forall a. a -> [a] -> [a]
    : Nat -> CSCtx o -> CSCtx o
    forall a. Nat -> [a] -> [a]
    drop (Nat
    scrut Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) CSCtx o
    ctx
                     (CSCtx o
    ctx', MExp o
    _, [CSPat o]
    pats') = [Nat]
    -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
    forall o.
    [Nat]
    -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
    applyperm [Nat]
    perm CSCtx o
    ctx1 MExp o
    tt ({-map (replacep scrut 1 CSAbsurd __IMPOSSIBLE__) -}[CSPat o]
    pats)
                 in [(CSCtx o
    ctx', [CSPat o]
    pats', Maybe (MExp o)
    forall a. Maybe a
    Nothing)]
                Maybe [Nat]
    Nothing -> Sol o
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- no permutation found
              Sol o
    _ -> Sol o
    sol
              ) [Sol o]
    sols
            where
             dobranches :: [ConstRef o] -> IO [Sol o]
             dobranches :: [ConstRef o] -> IO [Sol o]
    dobranches [] = [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [[]]
             dobranches (ConstRef o
    con : [ConstRef o]
    cons) = do
              ConstDef o
    cond <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    con
              let ff :: MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
    ff MExp o
    t = case Empty -> MExp o -> Exp o
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MExp o
    t of
                            Pi Maybe (UId o)
    _ Hiding
    h Bool
    _ MExp o
    it (Abs MId
    id MExp o
    ot) ->
                             let ([((Hiding, Nat), MId, MExp o)]
    xs, MExp o
    inft) = MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
    ff MExp o
    ot
                             in (((Hiding
    h, Nat
    scrut Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + [((Hiding, Nat), MId, MExp o)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [((Hiding, Nat), MId, MExp o)]
    xs), MId
    id, Nat -> MExp o -> MExp o
    forall t. Lift t => Nat -> t -> t
    lift (Nat
    scrut Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + [((Hiding, Nat), MId, MExp o)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [((Hiding, Nat), MId, MExp o)]
    xs Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) MExp o
    it) ((Hiding, Nat), MId, MExp o)
    -> [((Hiding, Nat), MId, MExp o)] -> [((Hiding, Nat), MId, MExp o)]
    forall a. a -> [a] -> [a]
    : [((Hiding, Nat), MId, MExp o)]
    xs, MExp o
    inft)
                            Exp o
    _ -> ([], Nat -> MExp o -> MExp o
    forall t. Lift t => Nat -> t -> t
    lift Nat
    scrut MExp o
    t)
                  ([((Hiding, Nat), MId, MExp o)]
    newvars, MExp o
    inftype) = MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
    ff (ConstDef o -> MExp o
    forall o. ConstDef o -> MExp o
    cdtype ConstDef o
    cond)
                  constrapp :: MExp o
    constrapp = Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    forall a. Maybe a
    Nothing (OKVal -> OKHandle (RefInfo o)
    forall a blk. a -> MM a blk
    NotM OKVal
    OKVal) (ConstRef o -> Elr o
    forall o. ConstRef o -> Elr o
    Const ConstRef o
    con) ((MArgList o -> ((Hiding, Nat), MId, MExp o) -> MArgList o)
    -> MArgList o -> [((Hiding, Nat), MId, MExp o)] -> MArgList o
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\MArgList o
    xs ((Hiding
    h, Nat
    v), MId
    _, MExp o
    _) -> ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MArgList o) -> ArgList o -> MArgList o
    forall a b. (a -> b) -> a -> b
    $ Hiding -> MExp o -> MArgList o -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    h (Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    forall a. Maybe a
    Nothing (OKVal -> OKHandle (RefInfo o)
    forall a blk. a -> MM a blk
    NotM OKVal
    OKVal) (Nat -> Elr o
    forall o. Nat -> Elr o
    Var Nat
    v) (ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM ArgList o
    forall o. ArgList o
    ALNil)) MArgList o
    xs) (ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM ArgList o
    forall o. ArgList o
    ALNil) ([((Hiding, Nat), MId, MExp o)] -> [((Hiding, Nat), MId, MExp o)]
    forall a. [a] -> [a]
    reverse [((Hiding, Nat), MId, MExp o)]
    newvars))
                  pconstrapp :: CSPatI o
    pconstrapp = ConstRef o -> [CSPat o] -> CSPatI o
    forall o. ConstRef o -> [CSPat o] -> CSPatI o
    CSPatConApp ConstRef o
    con ((((Hiding, Nat), MId, MExp o) -> CSPat o)
    -> [((Hiding, Nat), MId, MExp o)] -> [CSPat o]
    forall a b. (a -> b) -> [a] -> [b]
    map (\((Hiding
    hid, Nat
    v), MId
    _, MExp o
    _) -> Hiding -> CSPatI o -> CSPat o
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (Nat -> CSPatI o
    forall o. Nat -> CSPatI o
    CSPatVar Nat
    v)) [((Hiding, Nat), MId, MExp o)]
    newvars)
                  thesub :: MExp o -> MExp o
    thesub = Nat
    -> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
    forall t u.
    Replace t u =>
    Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace Nat
    scrut ([((Hiding, Nat), MId, MExp o)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [((Hiding, Nat), MId, MExp o)]
    newvars) MExp o
    MExp (ReplaceWith (MExp o) (MExp o))
    constrapp
                  Id String
    newvarprefix = (MId, MExp o) -> MId
    forall a b. (a, b) -> a
    fst ((MId, MExp o) -> MId) -> (MId, MExp o) -> MId
    forall a b. (a -> b) -> a -> b
    $ (CSCtx o -> [(MId, MExp o)]
    forall a. [HI a] -> [a]
    drophid CSCtx o
    ctx) [(MId, MExp o)] -> Nat -> (MId, MExp o)
    forall a. [a] -> Nat -> a
    !! Nat
    scrut
                  ctx1 :: CSCtx o
    ctx1 = (HI (MId, MExp o) -> HI (MId, MExp o)) -> CSCtx o -> CSCtx o
    forall a b. (a -> b) -> [a] -> [b]
    map (\(HI Hiding
    hid (MId
    id, MExp o
    t)) -> Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (MId
    id, MExp o -> MExp o
    thesub MExp o
    t)) (Nat -> CSCtx o -> CSCtx o
    forall a. Nat -> [a] -> [a]
    take Nat
    scrut CSCtx o
    ctx) CSCtx o -> CSCtx o -> CSCtx o
    forall a. [a] -> [a] -> [a]
    ++
                         CSCtx o -> CSCtx o
    forall a. [a] -> [a]
    reverse ((((Hiding, Nat), MId, MExp o) -> Integer -> HI (MId, MExp o))
    -> [((Hiding, Nat), MId, MExp o)] -> [Integer] -> CSCtx o
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\((Hiding
    hid, Nat
    _), MId
    id, MExp o
    t) Integer
    i ->
                           Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (String -> MId
    Id (case MId
    id of {MId
    NoId -> String
    newvarprefix{- ++ show i-}; Id String
    id -> String
    id}), MExp o
    t)
                          ) [((Hiding, Nat), MId, MExp o)]
    newvars [Integer
    0..]) CSCtx o -> CSCtx o -> CSCtx o
    forall a. [a] -> [a] -> [a]
    ++
                         (HI (MId, MExp o) -> HI (MId, MExp o)) -> CSCtx o -> CSCtx o
    forall a b. (a -> b) -> [a] -> [b]
    map (\(HI Hiding
    hid (MId
    id, MExp o
    t)) -> Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (MId
    id, MExp o -> MExp o
    thesub MExp o
    t)) (Nat -> CSCtx o -> CSCtx o
    forall a. Nat -> [a] -> [a]
    drop (Nat
    scrut Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) CSCtx o
    ctx)
                  tt' :: MExp o
    tt' = MExp o -> MExp o
    thesub MExp o
    tt
                  pats' :: [CSPat o]
    pats' = (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
    forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
    replacep Nat
    scrut ([((Hiding, Nat), MId, MExp o)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [((Hiding, Nat), MId, MExp o)]
    newvars) CSPatI o
    pconstrapp MExp o
    constrapp) [CSPat o]
    pats
                  scruttype' :: MExp o
    scruttype' = MExp o -> MExp o
    thesub MExp o
    scruttype  -- scruttype shouldn't really refer to scrutvar so lift is enough, but what if circular ref has been created and this is not detected until case split is done
              case MExp o -> MExp o -> Maybe [(Nat, MExp o)]
    forall o. MExp o -> MExp o -> Maybe [(Nat, MExp o)]
    unifyexp MExp o
    inftype MExp o
    scruttype' of
               Maybe [(Nat, MExp o)]
    Nothing -> do
                Bool
    res <- Nat -> Nat -> MExp o -> MExp o -> IO Bool
    forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
    notequal Nat
    scrut ([((Hiding, Nat), MId, MExp o)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [((Hiding, Nat), MId, MExp o)]
    newvars) MExp o
    scruttype' MExp o
    inftype
                if Bool
    res then -- branch absurd
                  [ConstRef o] -> IO [Sol o]
    dobranches [ConstRef o]
    cons
                 else -- branch dont know
                  [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
               Just [(Nat, MExp o)]
    unif ->
                do
                 let (CSCtx o
    ctx2, MExp o
    tt2, [CSPat o]
    pats2) = CSCtx o
    -> MExp o
    -> [CSPat o]
    -> [(Nat, MExp o)]
    -> (CSCtx o, MExp o, [CSPat o])
    forall o.
    CSCtx o
    -> MExp o
    -> [CSPat o]
    -> [(Nat, MExp o)]
    -> (CSCtx o, MExp o, [CSPat o])
    removevar CSCtx o
    ctx1 MExp o
    tt' [CSPat o]
    pats' [(Nat, MExp o)]
    unif
                     --cost = if elem scrut mblkvar then costCaseSplit - (costCaseSplit - costCaseSplitFollow) `div` (length mblkvar) else costCaseSplit
                     cost :: Cost
    cost
                       | [Nat] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Nat]
    mblkvar Bool -> Bool -> Bool
    && Nat
    scrut Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < CSCtx o -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length CSCtx o
    ctx Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    nscrutavoid Bool -> Bool -> Bool
    && Bool
    nothid
                                                                    = Cost
    costCaseSplitLow Cost -> Cost -> Cost
    forall a. Num a => a -> a -> a
    +
                                                                      Cost
    costAddVarDepth Cost -> Cost -> Cost
    forall a. Num a => a -> a -> a
    *
                                                                      Nat -> Cost
    Cost (Nat -> [CSPat o] -> Nat
    forall o. Nat -> [CSPat o] -> Nat
    depthofvar Nat
    scrut [CSPat o]
    pats)
                       | [Nat] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Nat]
    mblkvar                               = Cost
    costCaseSplitVeryHigh
                       | Nat
    scrut Nat -> [Nat] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Nat]
    mblkvar                       = Cost
    costCaseSplitLow
                       | Nat
    scrut Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < CSCtx o -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length CSCtx o
    ctx Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    nscrutavoid Bool -> Bool -> Bool
    && Bool
    nothid = Cost
    costCaseSplitHigh
                       | Bool
    otherwise                                  = Cost
    costCaseSplitVeryHigh

                     nothid :: Bool
    nothid = let HI Hiding
    hid (MId, MExp o)
    _ = CSCtx o
    ctx CSCtx o -> Nat -> HI (MId, MExp o)
    forall a. [a] -> Nat -> a
    !! Nat
    scrut
                              in Hiding
    hid Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    NotHidden

                 [Sol o]
    sols <- Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
    rc (Cost
    depth Cost -> Cost -> Cost
    forall a. Num a => a -> a -> a
    - Cost
    cost) (CSCtx o -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length CSCtx o
    ctx Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    scrut) CSCtx o
    ctx2 MExp o
    tt2 [CSPat o]
    pats2
                 case [Sol o]
    sols of
                  [] -> [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
                  [Sol o]
    _ -> do
                   [Sol o]
    sols2 <- [ConstRef o] -> IO [Sol o]
    dobranches [ConstRef o]
    cons
                   [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Sol o] -> IO [Sol o]) -> [Sol o] -> IO [Sol o]
    forall a b. (a -> b) -> a -> b
    $ (Sol o -> [Sol o]) -> [Sol o] -> [Sol o]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\Sol o
    sol -> (Sol o -> Sol o) -> [Sol o] -> [Sol o]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Sol o
    sol2 -> Sol o
    sol Sol o -> Sol o -> Sol o
    forall a. [a] -> [a] -> [a]
    ++ Sol o
    sol2) [Sol o]
    sols2) [Sol o]
    sols
           DeclCont o
    _ -> [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] -- split failed "scrut type is not datatype"
         Exp o
    _ -> [Sol o] -> IO [Sol o]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] -- split failed "scrut type is not datatype"

    infertypevar :: CSCtx o -> Nat -> MExp o
    infertypevar :: forall o. CSCtx o -> Nat -> MExp o
    infertypevar CSCtx o
    ctx Nat
    v = (MId, MExp o) -> MExp o
    forall a b. (a, b) -> b
    snd ((MId, MExp o) -> MExp o) -> (MId, MExp o) -> MExp o
    forall a b. (a -> b) -> a -> b
    $ (CSCtx o -> [(MId, MExp o)]
    forall a. [HI a] -> [a]
    drophid CSCtx o
    ctx) [(MId, MExp o)] -> Nat -> (MId, MExp o)
    forall a. [a] -> Nat -> a
    !! Nat
    v

    class Replace t u where
      type ReplaceWith t u
      replace' :: Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u

    replace :: Replace t u => Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace :: forall t u.
    Replace t u =>
    Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace Nat
    sv Nat
    nnew MExp (ReplaceWith t u)
    e t
    t = Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    0 MExp (ReplaceWith t u)
    e t
    t Reader (Nat, Nat) u -> (Nat, Nat) -> u
    forall r a. Reader r a -> r -> a
    `runReader` (Nat
    sv, Nat
    nnew)

    instance Replace t u => Replace (Abs t) (Abs u) where
      type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u
      replace' :: Nat
    -> MExp (ReplaceWith (Abs t) (Abs u))
    -> Abs t
    -> Reader (Nat, Nat) (Abs u)
    replace' Nat
    n MExp (ReplaceWith (Abs t) (Abs u))
    re (Abs MId
    mid t
    b) = MId -> u -> Abs u
    forall a. MId -> a -> Abs a
    Abs MId
    mid (u -> Abs u)
    -> ReaderT (Nat, Nat) Identity u -> Reader (Nat, Nat) (Abs u)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> MExp (ReplaceWith t u) -> t -> ReaderT (Nat, Nat) Identity u
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) MExp (ReplaceWith t u)
    MExp (ReplaceWith (Abs t) (Abs u))
    re t
    b

    instance Replace (Exp o) (MExp o) where
      type ReplaceWith (Exp o) (MExp o) = o
      replace' :: Nat
    -> MExp (ReplaceWith (Exp o) (MExp o))
    -> Exp o
    -> Reader (Nat, Nat) (MExp o)
    replace' Nat
    n MExp (ReplaceWith (Exp o) (MExp o))
    re = \case
        App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok elr :: Elr o
    elr@(Var Nat
    v) MArgList o
    args -> do
          MArgList o
    ih         <- ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MArgList o)
    -> ReaderT (Nat, Nat) Identity (ArgList o)
    -> ReaderT (Nat, Nat) Identity (MArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (MArgList o) (ArgList o))
    -> MArgList o
    -> ReaderT (Nat, Nat) Identity (ArgList o)
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MArgList o) (ArgList o))
    MExp (ReplaceWith (Exp o) (MExp o))
    re MArgList o
    args
          (Nat
    sv, Nat
    nnew) <- ReaderT (Nat, Nat) Identity (Nat, Nat)
    forall r (m :: * -> *). MonadReader r m => m r
    ask
          MExp o -> Reader (Nat, Nat) (MExp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MExp o -> Reader (Nat, Nat) (MExp o))
    -> MExp o -> Reader (Nat, Nat) (MExp o)
    forall a b. (a -> b) -> a -> b
    $
            if Nat
    v Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    n
            then if Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    sv
                 then MExp o -> MArgList o -> MExp o
    forall o. MExp o -> MArgList o -> MExp o
    betareduce (Nat -> MExp o -> MExp o
    forall t. Lift t => Nat -> t -> t
    lift Nat
    n MExp o
    MExp (ReplaceWith (Exp o) (MExp o))
    re) MArgList o
    ih
                 else if Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    sv
                      then Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok (Nat -> Elr o
    forall o. Nat -> Elr o
    Var (Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    nnew Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)) MArgList o
    ih
                      else Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr MArgList o
    ih
            else Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr MArgList o
    ih
        App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok elr :: Elr o
    elr@Const{} MArgList o
    args ->
          Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> (ArgList o -> Exp o) -> ArgList o -> MExp o
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr (MArgList o -> Exp o)
    -> (ArgList o -> MArgList o) -> ArgList o -> Exp o
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MExp o)
    -> ReaderT (Nat, Nat) Identity (ArgList o)
    -> Reader (Nat, Nat) (MExp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (MArgList o) (ArgList o))
    -> MArgList o
    -> ReaderT (Nat, Nat) Identity (ArgList o)
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MArgList o) (ArgList o))
    MExp (ReplaceWith (Exp o) (MExp o))
    re MArgList o
    args
        Lam Hiding
    hid Abs (MExp o)
    b -> Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o)
    -> (Abs (MExp o) -> Exp o) -> Abs (MExp o) -> MExp o
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Hiding -> Abs (MExp o) -> Exp o
    forall o. Hiding -> Abs (MExp o) -> Exp o
    Lam Hiding
    hid (Abs (MExp o) -> MExp o)
    -> ReaderT (Nat, Nat) Identity (Abs (MExp o))
    -> Reader (Nat, Nat) (MExp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
    -> Abs (MExp o)
    -> ReaderT (Nat, Nat) Identity (Abs (MExp o))
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) MExp (ReplaceWith (Exp o) (MExp o))
    MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
    re Abs (MExp o)
    b
        Pi Maybe (UId o)
    uid Hiding
    hid Bool
    possdep MExp o
    it Abs (MExp o)
    b ->
          (Exp o -> MExp o)
    -> ReaderT (Nat, Nat) Identity (Exp o)
    -> Reader (Nat, Nat) (MExp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (ReaderT (Nat, Nat) Identity (Exp o) -> Reader (Nat, Nat) (MExp o))
    -> ReaderT (Nat, Nat) Identity (Exp o)
    -> Reader (Nat, Nat) (MExp o)
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
    forall o.
    Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
    Pi Maybe (UId o)
    uid Hiding
    hid Bool
    possdep (MExp o -> Abs (MExp o) -> Exp o)
    -> Reader (Nat, Nat) (MExp o)
    -> ReaderT (Nat, Nat) Identity (Abs (MExp o) -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (MExp o) (MExp o))
    -> MExp o
    -> Reader (Nat, Nat) (MExp o)
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MExp o) (MExp o))
    MExp (ReplaceWith (Exp o) (MExp o))
    re MExp o
    it ReaderT (Nat, Nat) Identity (Abs (MExp o) -> Exp o)
    -> ReaderT (Nat, Nat) Identity (Abs (MExp o))
    -> ReaderT (Nat, Nat) Identity (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Nat
    -> MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
    -> Abs (MExp o)
    -> ReaderT (Nat, Nat) Identity (Abs (MExp o))
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (Exp o) (MExp o))
    MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
    re Abs (MExp o)
    b
        e :: Exp o
    e@Sort{} -> MExp o -> Reader (Nat, Nat) (MExp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MExp o -> Reader (Nat, Nat) (MExp o))
    -> MExp o -> Reader (Nat, Nat) (MExp o)
    forall a b. (a -> b) -> a -> b
    $ Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM Exp o
    e
        e :: Exp o
    e@AbsurdLambda{} -> MExp o -> Reader (Nat, Nat) (MExp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MExp o -> Reader (Nat, Nat) (MExp o))
    -> MExp o -> Reader (Nat, Nat) (MExp o)
    forall a b. (a -> b) -> a -> b
    $ Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM Exp o
    e

    instance Replace t u => Replace (MM t (RefInfo o)) u where
      type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u
      replace' :: Nat
    -> MExp (ReplaceWith (MM t (RefInfo o)) u)
    -> MM t (RefInfo o)
    -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MM t (RefInfo o)) u)
    re = Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith t u)
    MExp (ReplaceWith (MM t (RefInfo o)) u)
    re (t -> Reader (Nat, Nat) u)
    -> (MM t (RefInfo o) -> t)
    -> MM t (RefInfo o)
    -> Reader (Nat, Nat) u
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Empty -> MM t (RefInfo o) -> t
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Replace (ArgList o) (ArgList o) where
      type ReplaceWith (ArgList o) (ArgList o) = o
      replace' :: Nat
    -> MExp (ReplaceWith (ArgList o) (ArgList o))
    -> ArgList o
    -> Reader (Nat, Nat) (ArgList o)
    replace' Nat
    n MExp (ReplaceWith (ArgList o) (ArgList o))
    re ArgList o
    args = case ArgList o
    args of
        ArgList o
    ALNil           -> ArgList o -> Reader (Nat, Nat) (ArgList o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArgList o
    forall o. ArgList o
    ALNil
        ALCons Hiding
    hid MExp o
    a MArgList o
    as ->
          Hiding -> MExp o -> MArgList o -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    hid (MExp o -> MArgList o -> ArgList o)
    -> ReaderT (Nat, Nat) Identity (MExp o)
    -> ReaderT (Nat, Nat) Identity (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (MExp o) (MExp o))
    -> MExp o
    -> ReaderT (Nat, Nat) Identity (MExp o)
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MExp o) (MExp o))
    MExp (ReplaceWith (ArgList o) (ArgList o))
    re MExp o
    a ReaderT (Nat, Nat) Identity (MArgList o -> ArgList o)
    -> ReaderT (Nat, Nat) Identity (MArgList o)
    -> Reader (Nat, Nat) (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MArgList o)
    -> Reader (Nat, Nat) (ArgList o)
    -> ReaderT (Nat, Nat) Identity (MArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (MArgList o) (ArgList o))
    -> MArgList o
    -> Reader (Nat, Nat) (ArgList o)
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MArgList o) (ArgList o))
    MExp (ReplaceWith (ArgList o) (ArgList o))
    re MArgList o
    as)
        ALProj{}        -> Reader (Nat, Nat) (ArgList o)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        ALConPar MArgList o
    as     -> MArgList o -> ArgList o
    forall o. MArgList o -> ArgList o
    ALConPar (MArgList o -> ArgList o)
    -> (ArgList o -> MArgList o) -> ArgList o -> ArgList o
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> ArgList o)
    -> Reader (Nat, Nat) (ArgList o) -> Reader (Nat, Nat) (ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> MExp (ReplaceWith (MArgList o) (ArgList o))
    -> MArgList o
    -> Reader (Nat, Nat) (ArgList o)
    forall t u.
    Replace t u =>
    Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
    replace' Nat
    n MExp (ReplaceWith (MArgList o) (ArgList o))
    MExp (ReplaceWith (ArgList o) (ArgList o))
    re MArgList o
    as

    betareduce :: MExp o -> MArgList o -> MExp o
    betareduce :: forall o. MExp o -> MArgList o -> MExp o
    betareduce MExp o
    e MArgList o
    args = case Empty -> MArgList o -> ArgList o
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MArgList o
    args of
     ArgList o
    ALNil -> MExp o
    e
     ALCons Hiding
    _ MExp o
    a MArgList o
    rargs -> case Empty -> MExp o -> Exp o
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MExp o
    e of
      App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr MArgList o
    eargs -> Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr (MArgList o -> MArgList o -> MArgList o
    forall o. MArgList o -> MArgList o -> MArgList o
    concatargs MArgList o
    eargs MArgList o
    args)
      Lam Hiding
    _ (Abs MId
    _ MExp o
    b) -> MExp o -> MArgList o -> MExp o
    forall o. MExp o -> MArgList o -> MExp o
    betareduce (Nat
    -> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
    forall t u.
    Replace t u =>
    Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace Nat
    0 Nat
    0 MExp o
    MExp (ReplaceWith (MExp o) (MExp o))
    a MExp o
    b) MArgList o
    rargs
      Exp o
    _ -> MExp o
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- not type correct if this happens
     ALProj{} -> MExp o
    forall a. HasCallStack => a
    __IMPOSSIBLE__
     ALConPar MArgList o
    as -> MExp o
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    concatargs :: MArgList o -> MArgList o -> MArgList o
    concatargs :: forall o. MArgList o -> MArgList o -> MArgList o
    concatargs MArgList o
    xs MArgList o
    ys = case Empty -> MArgList o -> ArgList o
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MArgList o
    xs of
      ArgList o
    ALNil -> MArgList o
    ys

      ALCons Hiding
    hid MExp o
    x MArgList o
    xs -> ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MArgList o) -> ArgList o -> MArgList o
    forall a b. (a -> b) -> a -> b
    $ Hiding -> MExp o -> MArgList o -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    hid MExp o
    x (MArgList o -> MArgList o -> MArgList o
    forall o. MArgList o -> MArgList o -> MArgList o
    concatargs MArgList o
    xs MArgList o
    ys)

      ALProj{} -> MArgList o
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      ALConPar MArgList o
    as -> ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MArgList o) -> ArgList o -> MArgList o
    forall a b. (a -> b) -> a -> b
    $ MArgList o -> ArgList o
    forall o. MArgList o -> ArgList o
    ALConPar (MArgList o -> MArgList o -> MArgList o
    forall o. MArgList o -> MArgList o -> MArgList o
    concatargs MArgList o
    xs MArgList o
    ys)

    replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
    replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
    replacep Nat
    sv Nat
    nnew CSPatI o
    rp MExp o
    re = CSPat o -> CSPat o
    r
     where
      r :: CSPat o -> CSPat o
      r :: CSPat o -> CSPat o
    r (HI Hiding
    hid (CSPatConApp ConstRef o
    c [CSPat o]
    ps)) = Hiding -> CSPatI o -> CSPat o
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (ConstRef o -> [CSPat o] -> CSPatI o
    forall o. ConstRef o -> [CSPat o] -> CSPatI o
    CSPatConApp ConstRef o
    c ((CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
    forall a b. (a -> b) -> [a] -> [b]
    map CSPat o -> CSPat o
    r [CSPat o]
    ps))
      r (HI Hiding
    hid (CSPatVar Nat
    v)) | Nat
    v Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    sv   = Hiding -> CSPatI o -> CSPat o
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid CSPatI o
    rp
                              | Nat
    v Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    sv    = Hiding -> CSPatI o -> CSPat o
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (Nat -> CSPatI o
    forall o. Nat -> CSPatI o
    CSPatVar (Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    nnew Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1))
                              | Bool
    otherwise = Hiding -> CSPatI o -> CSPat o
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (Nat -> CSPatI o
    forall o. Nat -> CSPatI o
    CSPatVar Nat
    v)
      r (HI Hiding
    hid (CSPatExp MExp o
    e)) = Hiding -> CSPatI o -> CSPat o
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (MExp o -> CSPatI o
    forall o. MExp o -> CSPatI o
    CSPatExp (MExp o -> CSPatI o) -> MExp o -> CSPatI o
    forall a b. (a -> b) -> a -> b
    $ Nat
    -> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
    forall t u.
    Replace t u =>
    Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace Nat
    sv Nat
    nnew MExp o
    MExp (ReplaceWith (MExp o) (MExp o))
    re MExp o
    e)

      r p :: CSPat o
    p@(HI Hiding
    _ CSPatI o
    CSOmittedArg) = CSPat o
    p

      r CSPat o
    _ = CSPat o
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- other constructors dont appear in indata Pats

    -- Unification takes two values of the same type and generates a list
    -- of assignments making the two terms equal.

    type Assignments o = [(Nat, Exp o)]

    class Unify t where
      type UnifiesTo t
      unify'    :: t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
      notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool

    unify :: Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
    unify :: forall t. Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
    unify t
    t t
    u = t -> t -> StateT [(Nat, Exp (UnifiesTo t))] Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' t
    t t
    u StateT [(Nat, Exp (UnifiesTo t))] Maybe ()
    -> [(Nat, Exp (UnifiesTo t))] -> Maybe [(Nat, Exp (UnifiesTo t))]
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    `execStateT` []

    notequal :: Unify t => Nat -> Nat -> t -> t -> IO Bool
    notequal :: forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
    notequal Nat
    fstnew Nat
    nbnew t
    t1 t
    t2 = t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' t
    t1 t
    t2 ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    -> (Nat, Nat) -> StateT (Assignments (UnifiesTo t)) IO Bool
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` (Nat
    fstnew, Nat
    nbnew)
                                                  StateT (Assignments (UnifiesTo t)) IO Bool
    -> Assignments (UnifiesTo t) -> IO Bool
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    `evalStateT` []

    instance (Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) where
      type UnifiesTo (MM t (RefInfo o)) = o

      unify' :: MM t (RefInfo o)
    -> MM t (RefInfo o)
    -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()
    unify' = t -> t -> StateT [(Nat, Exp o)] Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' (t -> t -> StateT [(Nat, Exp o)] Maybe ())
    -> (MM t (RefInfo o) -> t)
    -> MM t (RefInfo o)
    -> MM t (RefInfo o)
    -> StateT [(Nat, Exp o)] Maybe ()
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Empty -> MM t (RefInfo o) -> t
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      notequal' :: MM t (RefInfo o)
    -> MM t (RefInfo o)
    -> ReaderT
         (Nat, Nat)
         (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO)
         Bool
    notequal' = t -> t -> ReaderT (Nat, Nat) (StateT [(Nat, Exp o)] IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' (t -> t -> ReaderT (Nat, Nat) (StateT [(Nat, Exp o)] IO) Bool)
    -> (MM t (RefInfo o) -> t)
    -> MM t (RefInfo o)
    -> MM t (RefInfo o)
    -> ReaderT (Nat, Nat) (StateT [(Nat, Exp o)] IO) Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Empty -> MM t (RefInfo o) -> t
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe ()
    unifyVar :: forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
    unifyVar Nat
    v Exp o
    e = do
      Assignments o
    unif <- StateT (Assignments o) Maybe (Assignments o)
    forall s (m :: * -> *). MonadState s m => m s
    get
      case Nat -> Assignments o -> Maybe (Exp o)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Nat
    v Assignments o
    unif of
        Maybe (Exp o)
    Nothing -> (Assignments o -> Assignments o) -> StateT (Assignments o) Maybe ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Nat
    v, Exp o
    e) (Nat, Exp o) -> Assignments o -> Assignments o
    forall a. a -> [a] -> [a]
    :)
        Just Exp o
    e' -> Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' Exp o
    e Exp o
    e'

    instance Unify t => Unify (Abs t) where
      type UnifiesTo (Abs t) = UnifiesTo t
      unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe ()
    unify' (Abs MId
    _ t
    b1) (Abs MId
    _ t
    b2) = t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' t
    b1 t
    b2

      notequal' :: Abs t
    -> Abs t
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool
    notequal' (Abs MId
    _ t
    b1) (Abs MId
    _ t
    b2) = t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' t
    b1 t
    b2

    instance Unify (Exp o) where
      type UnifiesTo (Exp o) = o

      unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()
    unify' Exp o
    e1 Exp o
    e2 = case (Exp o
    e1, Exp o
    e2) of
       (App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    elr1 MArgList o
    args1, App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    elr2 MArgList o
    args2) | Elr o
    elr1 Elr o -> Elr o -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elr o
    elr2 -> MArgList o
    -> MArgList o
    -> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MArgList o
    args1 MArgList o
    args2
       (Lam Hiding
    hid1 Abs (MExp o)
    b1, Lam Hiding
    hid2 Abs (MExp o)
    b2)               | Hiding
    hid1 Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    hid2 -> Abs (MExp o)
    -> Abs (MExp o)
    -> StateT (Assignments (UnifiesTo (Abs (MExp o)))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' Abs (MExp o)
    b1 Abs (MExp o)
    b2
       (Pi Maybe (UId o)
    _ Hiding
    hid1 Bool
    _ MExp o
    a1 Abs (MExp o)
    b1, Pi Maybe (UId o)
    _ Hiding
    hid2 Bool
    _ MExp o
    a2 Abs (MExp o)
    b2)   | Hiding
    hid1 Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    hid2 -> MExp o
    -> MExp o -> StateT (Assignments (UnifiesTo (MExp o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MExp o
    a1 MExp o
    a2
                                                               StateT (Assignments o) Maybe ()
    -> StateT (Assignments o) Maybe ()
    -> StateT (Assignments o) Maybe ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Abs (MExp o)
    -> Abs (MExp o)
    -> StateT (Assignments (UnifiesTo (Abs (MExp o)))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' Abs (MExp o)
    b1 Abs (MExp o)
    b2
       (Sort Sort
    _, Sort Sort
    _) -> () -> StateT (Assignments o) Maybe ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- a bit sloppy
       (App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v) (NotM ArgList o
    ALNil), Exp o
    _)
         | Nat
    v Nat -> Set Nat -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` (Exp o -> Set Nat
    forall t. FreeVars t => t -> Set Nat
    freeVars Exp o
    e2) -> Maybe () -> StateT (Assignments o) Maybe ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    St.lift Maybe ()
    forall a. Maybe a
    Nothing -- Occurs check
       (Exp o
    _, App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v) (NotM ArgList o
    ALNil))
         | Nat
    v Nat -> Set Nat -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` (Exp o -> Set Nat
    forall t. FreeVars t => t -> Set Nat
    freeVars Exp o
    e1) -> Maybe () -> StateT (Assignments o) Maybe ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    St.lift Maybe ()
    forall a. Maybe a
    Nothing -- Occurs check
       (App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v) (NotM ArgList o
    ALNil), Exp o
    _) -> Nat -> Exp o -> StateT (Assignments o) Maybe ()
    forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
    unifyVar Nat
    v Exp o
    e2
       (Exp o
    _, App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v) (NotM ArgList o
    ALNil)) -> Nat -> Exp o -> StateT (Assignments o) Maybe ()
    forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
    unifyVar Nat
    v Exp o
    e1
       (Exp o, Exp o)
    _ -> Maybe () -> StateT (Assignments o) Maybe ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    St.lift Maybe ()
    forall a. Maybe a
    Nothing

      notequal' :: Exp o
    -> Exp o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
    notequal' Exp o
    e1 Exp o
    e2 = do
        (Nat
    fstnew, Nat
    nbnew) <- ReaderT (Nat, Nat) (StateT (Assignments o) IO) (Nat, Nat)
    forall r (m :: * -> *). MonadReader r m => m r
    ask
        Assignments o
    unifier         <- ReaderT (Nat, Nat) (StateT (Assignments o) IO) (Assignments o)
    forall s (m :: * -> *). MonadState s m => m s
    get
        case (Exp o
    e1, Exp o
    e2) of
          (App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    elr1 MArgList o
    es1, App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    elr2 MArgList o
    es2) | Elr o
    elr1 Elr o -> Elr o -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elr o
    elr2 -> MArgList o
    -> MArgList o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' MArgList o
    es1 MArgList o
    es2
          (Exp o
    _, App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v2) (NotM ArgList o
    ALNil)) -- why is this not symmetric?!
            | Nat
    fstnew Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Nat
    v2 Bool -> Bool -> Bool
    && Nat
    v2 Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    fstnew Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    nbnew ->
            case Nat -> Assignments o -> Maybe (Exp o)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Nat
    v2 Assignments o
    unifier of
              Maybe (Exp o)
    Nothing  -> (Assignments o -> Assignments o)
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Nat
    v2, Exp o
    e1)(Nat, Exp o) -> Assignments o -> Assignments o
    forall a. a -> [a] -> [a]
    :) ReaderT (Nat, Nat) (StateT (Assignments o) IO) ()
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
              Just Exp o
    e2' -> Exp o
    -> Exp o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' Exp o
    e1 Exp o
    e2'
    {-
      GA: Skipped these: Not sure why we'd claim they're impossible
          (_, App _ _ (Var v2) (NotM ALProj{})) -> __IMPOSSIBLE__
          (_, App _ _ (Var v2) (NotM ALConPar{})) -> __IMPOSSIBLE__
    -}
          (App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Const ConstRef o
    c1) MArgList o
    es1, App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Const ConstRef o
    c2) MArgList o
    es2) -> do
            ConstDef o
    cd1 <- IO (ConstDef o)
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (ConstDef o)
     -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o))
    -> IO (ConstDef o)
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
    forall a b. (a -> b) -> a -> b
    $ ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c1
            ConstDef o
    cd2 <- IO (ConstDef o)
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (ConstDef o)
     -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o))
    -> IO (ConstDef o)
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
    forall a b. (a -> b) -> a -> b
    $ ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c2
            case (ConstDef o -> DeclCont o
    forall o. ConstDef o -> DeclCont o
    cdcont ConstDef o
    cd1, ConstDef o -> DeclCont o
    forall o. ConstDef o -> DeclCont o
    cdcont ConstDef o
    cd2) of
              (Constructor{}, Constructor{}) -> if ConstRef o
    c1 ConstRef o -> ConstRef o -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConstRef o
    c2 then MArgList o
    -> MArgList o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' MArgList o
    es1 MArgList o
    es2
                                                else Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
              (DeclCont o, DeclCont o)
    _ -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
    {- GA: Why don't we have a case for distinct heads after all these
           unification cases for vars with no spines & metas that can
           be looked up?
          (App _ _ elr1 _, App _ _ elr2 _) | elr1 <> elr2 -> return True
    -}
          (Exp o, Exp o)
    _ -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    instance Unify (ArgList o) where
      type UnifiesTo (ArgList o) = o

      unify' :: ArgList o
    -> ArgList o
    -> StateT (Assignments (UnifiesTo (ArgList o))) Maybe ()
    unify' ArgList o
    args1 ArgList o
    args2 = case (ArgList o
    args1, ArgList o
    args2) of
       (ArgList o
    ALNil, ArgList o
    ALNil) -> () -> StateT (Assignments o) Maybe ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
       (ALCons Hiding
    hid1 MExp o
    a1 MArgList o
    as1, ALCons Hiding
    hid2 MExp o
    a2 MArgList o
    as2) | Hiding
    hid1 Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    hid2 -> MExp o
    -> MExp o -> StateT (Assignments (UnifiesTo (MExp o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MExp o
    a1 MExp o
    a2
                                                               StateT (Assignments o) Maybe ()
    -> StateT (Assignments o) Maybe ()
    -> StateT (Assignments o) Maybe ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MArgList o
    -> MArgList o
    -> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MArgList o
    as1 MArgList o
    as2
       (ALConPar MArgList o
    as1, ALCons Hiding
    _ MExp o
    _ MArgList o
    as2) -> MArgList o
    -> MArgList o
    -> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MArgList o
    as1 MArgList o
    as2
       (ALCons Hiding
    _ MExp o
    _ MArgList o
    as1, ALConPar MArgList o
    as2) -> MArgList o
    -> MArgList o
    -> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MArgList o
    as1 MArgList o
    as2
       (ALConPar MArgList o
    as1, ALConPar MArgList o
    as2)   -> MArgList o
    -> MArgList o
    -> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
    forall t.
    Unify t =>
    t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
    unify' MArgList o
    as1 MArgList o
    as2
       (ArgList o, ArgList o)
    _ -> Maybe () -> StateT (Assignments o) Maybe ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    St.lift Maybe ()
    forall a. Maybe a
    Nothing

      notequal' :: ArgList o
    -> ArgList o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool
    notequal' ArgList o
    args1 ArgList o
    args2 = case (ArgList o
    args1, ArgList o
    args2) of
        (ALCons Hiding
    _ MExp o
    e MArgList o
    es, ALCons Hiding
    _ MExp o
    f MArgList o
    fs) -> MExp o
    -> MExp o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (MExp o))) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' MExp o
    e MExp o
    f ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` MArgList o
    -> MArgList o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' MArgList o
    es MArgList o
    fs
        (ALConPar MArgList o
    es1, ALConPar MArgList o
    es2)   -> MArgList o
    -> MArgList o
    -> ReaderT
         (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
    forall t.
    Unify t =>
    t
    -> t
    -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
    notequal' MArgList o
    es1 MArgList o
    es2
        (ArgList o, ArgList o)
    _                              -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- This definition is only here to respect the previous interface.
    unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
    unifyexp :: forall o. MExp o -> MExp o -> Maybe [(Nat, MExp o)]
    unifyexp MExp o
    e1 MExp o
    e2 = ((Nat, Exp o) -> (Nat, MExp o))
    -> [(Nat, Exp o)] -> [(Nat, MExp o)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> (Nat, Exp o) -> (Nat, MExp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) ([(Nat, Exp o)] -> [(Nat, MExp o)])
    -> Maybe [(Nat, Exp o)] -> Maybe [(Nat, MExp o)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MExp o -> MExp o -> Maybe (Assignments (UnifiesTo (MExp o)))
    forall t. Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
    unify MExp o
    e1 MExp o
    e2

    class Lift t where
      lift' :: Nat -> Nat -> t -> t

    lift :: Lift t => Nat -> t -> t
    lift :: forall t. Lift t => Nat -> t -> t
    lift Nat
    0 = t -> t
    forall a. a -> a
    id
    lift Nat
    n = Nat -> Nat -> t -> t
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    0

    instance Lift t => Lift (Abs t) where
      lift' :: Nat -> Nat -> Abs t -> Abs t
    lift' Nat
    n Nat
    j (Abs MId
    mid t
    b) = MId -> t -> Abs t
    forall a. MId -> a -> Abs a
    Abs MId
    mid (Nat -> Nat -> t -> t
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n (Nat
    j Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) t
    b)

    instance Lift t => Lift (MM t r) where
      lift' :: Nat -> Nat -> MM t r -> MM t r
    lift' Nat
    n Nat
    j = t -> MM t r
    forall a blk. a -> MM a blk
    NotM (t -> MM t r) -> (MM t r -> t) -> MM t r -> MM t r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Nat -> t -> t
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j (t -> t) -> (MM t r -> t) -> MM t r -> t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Empty -> MM t r -> t
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Lift (Exp o) where
      lift' :: Nat -> Nat -> Exp o -> Exp o
    lift' Nat
    n Nat
    j = \case
        App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr MArgList o
    args -> case Elr o
    elr of
          Var Nat
    v | Nat
    v Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    j -> Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok (Nat -> Elr o
    forall o. Nat -> Elr o
    Var (Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n)) (Nat -> Nat -> MArgList o -> MArgList o
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j MArgList o
    args)
          Elr o
    _ -> Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr (Nat -> Nat -> MArgList o -> MArgList o
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j MArgList o
    args)
        Lam Hiding
    hid Abs (MExp o)
    b -> Hiding -> Abs (MExp o) -> Exp o
    forall o. Hiding -> Abs (MExp o) -> Exp o
    Lam Hiding
    hid (Nat -> Nat -> Abs (MExp o) -> Abs (MExp o)
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j Abs (MExp o)
    b)
        Pi Maybe (UId o)
    uid Hiding
    hid Bool
    possdep MExp o
    it Abs (MExp o)
    b -> Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
    forall o.
    Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
    Pi Maybe (UId o)
    uid Hiding
    hid Bool
    possdep (Nat -> Nat -> MExp o -> MExp o
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j MExp o
    it) (Nat -> Nat -> Abs (MExp o) -> Abs (MExp o)
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j Abs (MExp o)
    b)
        e :: Exp o
    e@Sort{} -> Exp o
    e
        e :: Exp o
    e@AbsurdLambda{} -> Exp o
    e

    instance Lift (ArgList o) where
      lift' :: Nat -> Nat -> ArgList o -> ArgList o
    lift' Nat
    n Nat
    j ArgList o
    args = case ArgList o
    args of
        ArgList o
    ALNil           -> ArgList o
    forall o. ArgList o
    ALNil
        ALCons Hiding
    hid MExp o
    a MArgList o
    as -> Hiding -> MExp o -> MArgList o -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    hid (Nat -> Nat -> MExp o -> MExp o
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j MExp o
    a) (Nat -> Nat -> MArgList o -> MArgList o
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j MArgList o
    as)
        ALProj{}        -> ArgList o
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        ALConPar MArgList o
    as     -> MArgList o -> ArgList o
    forall o. MArgList o -> ArgList o
    ALConPar (Nat -> Nat -> MArgList o -> MArgList o
    forall t. Lift t => Nat -> Nat -> t -> t
    lift' Nat
    n Nat
    j MArgList o
    as)

    removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])
    removevar :: forall o.
    CSCtx o
    -> MExp o
    -> [CSPat o]
    -> [(Nat, MExp o)]
    -> (CSCtx o, MExp o, [CSPat o])
    removevar CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats [] = (CSCtx o
    ctx, MExp o
    tt, [CSPat o]
    pats)
    removevar CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats ((Nat
    v, MExp o
    e) : [(Nat, MExp o)]
    unif) =
     let
      e2 :: MExp o
    e2 = Nat
    -> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
    forall t u.
    Replace t u =>
    Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace Nat
    v Nat
    0 MExp (ReplaceWith (MExp o) (MExp o))
    forall a. HasCallStack => a
    __IMPOSSIBLE__ {- occurs check failed -} MExp o
    e
      thesub :: MExp o -> MExp o
    thesub = Nat
    -> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
    forall t u.
    Replace t u =>
    Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
    replace Nat
    v Nat
    0 MExp o
    MExp (ReplaceWith (MExp o) (MExp o))
    e2
      ctx1 :: CSCtx o
    ctx1 = (HI (MId, MExp o) -> HI (MId, MExp o)) -> CSCtx o -> CSCtx o
    forall a b. (a -> b) -> [a] -> [b]
    map (\(HI Hiding
    hid (MId
    id, MExp o
    t)) -> Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (MId
    id, MExp o -> MExp o
    thesub MExp o
    t)) (Nat -> CSCtx o -> CSCtx o
    forall a. Nat -> [a] -> [a]
    take Nat
    v CSCtx o
    ctx) CSCtx o -> CSCtx o -> CSCtx o
    forall a. [a] -> [a] -> [a]
    ++
             (HI (MId, MExp o) -> HI (MId, MExp o)) -> CSCtx o -> CSCtx o
    forall a b. (a -> b) -> [a] -> [b]
    map (\(HI Hiding
    hid (MId
    id, MExp o
    t)) -> Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (MId
    id, MExp o -> MExp o
    thesub MExp o
    t)) (Nat -> CSCtx o -> CSCtx o
    forall a. Nat -> [a] -> [a]
    drop (Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) CSCtx o
    ctx)
      tt' :: MExp o
    tt' = MExp o -> MExp o
    thesub MExp o
    tt
      pats' :: [CSPat o]
    pats' = (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
    forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
    replacep Nat
    v Nat
    0 (MExp o -> CSPatI o
    forall o. MExp o -> CSPatI o
    CSPatExp MExp o
    e2) MExp o
    e2) [CSPat o]
    pats
      unif' :: [(Nat, MExp o)]
    unif' = ((Nat, MExp o) -> (Nat, MExp o))
    -> [(Nat, MExp o)] -> [(Nat, MExp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Nat
    uv, MExp o
    ue) -> (if Nat
    uv Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    v then Nat
    uv Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1 else Nat
    uv, MExp o -> MExp o
    thesub MExp o
    ue)) [(Nat, MExp o)]
    unif
     in
      CSCtx o
    -> MExp o
    -> [CSPat o]
    -> [(Nat, MExp o)]
    -> (CSCtx o, MExp o, [CSPat o])
    forall o.
    CSCtx o
    -> MExp o
    -> [CSPat o]
    -> [(Nat, MExp o)]
    -> (CSCtx o, MExp o, [CSPat o])
    removevar CSCtx o
    ctx1 MExp o
    tt' [CSPat o]
    pats' [(Nat, MExp o)]
    unif'

    findperm :: [MExp o] -> Maybe [Nat]
    findperm :: forall o. [MExp o] -> Maybe [Nat]
    findperm [MExp o]
    ts =
     let
      frees :: [[Nat]]
    frees = (MExp o -> [Nat]) -> [MExp o] -> [[Nat]]
    forall a b. (a -> b) -> [a] -> [b]
    map MExp o -> [Nat]
    forall t. FreeVars t => t -> [Nat]
    freevars [MExp o]
    ts
      m :: IntMap Nat
    m = [(Nat, Nat)] -> IntMap Nat
    forall a. [(Nat, a)] -> IntMap a
    IntMap.fromList ([(Nat, Nat)] -> IntMap Nat) -> [(Nat, Nat)] -> IntMap Nat
    forall a b. (a -> b) -> a -> b
    $
          (Nat -> (Nat, Nat)) -> [Nat] -> [(Nat, Nat)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Nat
    i -> (Nat
    i, [[Nat]] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length (([Nat] -> Bool) -> [[Nat]] -> [[Nat]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Nat -> [Nat] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem Nat
    i) [[Nat]]
    frees)))
              [Nat
    0..[MExp o] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [MExp o]
    ts Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
      r :: IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
    r IntMap Nat
    _ [Nat]
    perm Nat
    0 = [Nat] -> Maybe [Nat]
    forall a. a -> Maybe a
    Just ([Nat] -> Maybe [Nat]) -> [Nat] -> Maybe [Nat]
    forall a b. (a -> b) -> a -> b
    $ [Nat] -> [Nat]
    forall a. [a] -> [a]
    reverse [Nat]
    perm
      r IntMap Nat
    m [Nat]
    perm Nat
    n =
       case Nat -> [(Nat, Nat)] -> Maybe Nat
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Nat
    0 (((Nat, Nat) -> (Nat, Nat)) -> [(Nat, Nat)] -> [(Nat, Nat)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat, Nat) -> (Nat, Nat)
    forall a b. (a, b) -> (b, a)
    swap (IntMap Nat -> [(Nat, Nat)]
    forall a. IntMap a -> [(Nat, a)]
    IntMap.toList IntMap Nat
    m)) of
        Maybe Nat
    Nothing -> Maybe [Nat]
    forall a. Maybe a
    Nothing
        Just Nat
    i -> IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
    r ((IntMap Nat -> Nat -> IntMap Nat)
    -> IntMap Nat -> [Nat] -> IntMap Nat
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ((Nat -> IntMap Nat -> IntMap Nat)
    -> IntMap Nat -> Nat -> IntMap Nat
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Nat -> IntMap Nat -> IntMap Nat)
     -> IntMap Nat -> Nat -> IntMap Nat)
    -> (Nat -> IntMap Nat -> IntMap Nat)
    -> IntMap Nat
    -> Nat
    -> IntMap Nat
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Nat) -> Nat -> IntMap Nat -> IntMap Nat
    forall a. (a -> a) -> Nat -> IntMap a -> IntMap a
    IntMap.adjust (Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    subtract Nat
    1))
                           (Nat -> Nat -> IntMap Nat -> IntMap Nat
    forall a. Nat -> a -> IntMap a -> IntMap a
    IntMap.insert Nat
    i (-Nat
    1) IntMap Nat
    m)
                           ([[Nat]]
    frees [[Nat]] -> Nat -> [Nat]
    forall a. [a] -> Nat -> a
    !! Nat
    i))
                     (Nat
    i Nat -> [Nat] -> [Nat]
    forall a. a -> [a] -> [a]
    : [Nat]
    perm) (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)
     in IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
    r IntMap Nat
    m [] ([MExp o] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [MExp o]
    ts)

    freevars :: FreeVars t => t -> [Nat]
    freevars :: forall t. FreeVars t => t -> [Nat]
    freevars = Set Nat -> [Nat]
    forall a. Set a -> [a]
    Set.toList (Set Nat -> [Nat]) -> (t -> Set Nat) -> t -> [Nat]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t -> Set Nat
    forall t. FreeVars t => t -> Set Nat
    freeVars

    applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] ->
                 (CSCtx o, MExp o, [CSPat o])
    applyperm :: forall o.
    [Nat]
    -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
    applyperm [Nat]
    perm CSCtx o
    ctx MExp o
    tt [CSPat o]
    pats =
     let ctx1 :: CSCtx o
    ctx1 = (HI (MId, MExp o) -> HI (MId, MExp o)) -> CSCtx o -> CSCtx o
    forall a b. (a -> b) -> [a] -> [b]
    map (\(HI Hiding
    hid (MId
    id, MExp o
    t)) -> Hiding -> (MId, MExp o) -> HI (MId, MExp o)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (MId
    id, (Nat -> Nat) -> MExp o -> MExp o
    forall t. Renaming t => (Nat -> Nat) -> t -> t
    rename ([Nat] -> Nat -> Nat
    ren [Nat]
    perm) MExp o
    t)) CSCtx o
    ctx
         ctx2 :: CSCtx o
    ctx2 = (Nat -> HI (MId, MExp o)) -> [Nat] -> CSCtx o
    forall a b. (a -> b) -> [a] -> [b]
    map (\Nat
    i -> CSCtx o
    ctx1 CSCtx o -> Nat -> HI (MId, MExp o)
    forall a. [a] -> Nat -> a
    !! Nat
    i) [Nat]
    perm
         ctx3 :: CSCtx o
    ctx3 = CSCtx o -> CSCtx o
    forall o. CSCtx o -> CSCtx o
    seqctx CSCtx o
    ctx2
         tt' :: MExp o
    tt' = (Nat -> Nat) -> MExp o -> MExp o
    forall t. Renaming t => (Nat -> Nat) -> t -> t
    rename ([Nat] -> Nat -> Nat
    ren [Nat]
    perm) MExp o
    tt
         pats' :: [CSPat o]
    pats' = (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Nat -> Nat) -> CSPat o -> CSPat o
    forall t. Renaming t => (Nat -> Nat) -> t -> t
    rename ([Nat] -> Nat -> Nat
    ren [Nat]
    perm)) [CSPat o]
    pats
     in (CSCtx o
    ctx3, MExp o
    tt', [CSPat o]
    pats')

    ren :: [Nat] -> Nat -> Int
    ren :: [Nat] -> Nat -> Nat
    ren [Nat]
    n Nat
    i = let Just Nat
    j = Nat -> [Nat] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    elemIndex Nat
    i [Nat]
    n in Nat
    j

    instance Renaming t => Renaming (HI t) where
      renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t
    renameOffset Nat
    j Nat -> Nat
    ren (HI Hiding
    hid t
    t) = Hiding -> t -> HI t
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (t -> HI t) -> t -> HI t
    forall a b. (a -> b) -> a -> b
    $ Nat -> (Nat -> Nat) -> t -> t
    forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
    renameOffset Nat
    j Nat -> Nat
    ren t
    t

    instance Renaming (CSPatI o) where
      renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o
    renameOffset Nat
    j Nat -> Nat
    ren = \case
        CSPatConApp ConstRef o
    c [CSPat o]
    pats -> ConstRef o -> [CSPat o] -> CSPatI o
    forall o. ConstRef o -> [CSPat o] -> CSPatI o
    CSPatConApp ConstRef o
    c ([CSPat o] -> CSPatI o) -> [CSPat o] -> CSPatI o
    forall a b. (a -> b) -> a -> b
    $ (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat -> (Nat -> Nat) -> CSPat o -> CSPat o
    forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
    renameOffset Nat
    j Nat -> Nat
    ren) [CSPat o]
    pats
        CSPatVar Nat
    i         -> Nat -> CSPatI o
    forall o. Nat -> CSPatI o
    CSPatVar (Nat -> CSPatI o) -> Nat -> CSPatI o
    forall a b. (a -> b) -> a -> b
    $ Nat
    j Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat -> Nat
    ren Nat
    i
        CSPatExp MExp o
    e         -> MExp o -> CSPatI o
    forall o. MExp o -> CSPatI o
    CSPatExp (MExp o -> CSPatI o) -> MExp o -> CSPatI o
    forall a b. (a -> b) -> a -> b
    $ Nat -> (Nat -> Nat) -> MExp o -> MExp o
    forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
    renameOffset Nat
    j Nat -> Nat
    ren MExp o
    e
        e :: CSPatI o
    e@CSPatI o
    CSOmittedArg     -> CSPatI o
    e
        CSPatI o
    _                  -> CSPatI o
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    seqctx :: CSCtx o -> CSCtx o
    seqctx :: forall o. CSCtx o -> CSCtx o
    seqctx = Nat -> [HI (MId, MExp o)] -> [HI (MId, MExp o)]
    forall {b} {a}. Lift b => Nat -> [HI (a, b)] -> [HI (a, b)]
    r (-Nat
    1)
     where
      r :: Nat -> [HI (a, b)] -> [HI (a, b)]
    r Nat
    _ [] = []
      r Nat
    n (HI Hiding
    hid (a
    id, b
    t) : [HI (a, b)]
    ctx) = Hiding -> (a, b) -> HI (a, b)
    forall a. Hiding -> a -> HI a
    HI Hiding
    hid (a
    id, Nat -> b -> b
    forall t. Lift t => Nat -> t -> t
    lift Nat
    n b
    t) HI (a, b) -> [HI (a, b)] -> [HI (a, b)]
    forall a. a -> [a] -> [a]
    : Nat -> [HI (a, b)] -> [HI (a, b)]
    r (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) [HI (a, b)]
    ctx
    -- --------------------

    depthofvar :: Nat -> [CSPat o] -> Nat
    depthofvar :: forall o. Nat -> [CSPat o] -> Nat
    depthofvar Nat
    v [CSPat o]
    pats =
     let [Nat
    depth] = (CSPatI o -> [Nat]) -> [CSPatI o] -> [Nat]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Nat -> CSPatI o -> [Nat]
    f Nat
    0) ([CSPat o] -> [CSPatI o]
    forall a. [HI a] -> [a]
    drophid [CSPat o]
    pats)
         f :: Nat -> CSPatI o -> [Nat]
    f Nat
    d (CSPatConApp ConstRef o
    _ [CSPat o]
    pats) = (CSPatI o -> [Nat]) -> [CSPatI o] -> [Nat]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Nat -> CSPatI o -> [Nat]
    f (Nat
    d Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)) ([CSPat o] -> [CSPatI o]
    forall a. [HI a] -> [a]
    drophid [CSPat o]
    pats)
         f Nat
    d (CSPatVar Nat
    v') = [Nat
    d | Nat
    v Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    v']
         f Nat
    _ CSPatI o
    _ = []
     in Nat
    depth

    -- --------------------
    -- | Speculation: Type class computing the size (?) of a pattern
    --   and collecting the vars it introduces
    class LocalTerminationEnv a where
      sizeAndBoundVars :: a -> (Sum Nat, [Nat])

    instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where
      sizeAndBoundVars :: HI a -> (Sum Nat, [Nat])
    sizeAndBoundVars (HI Hiding
    _ a
    p) = a -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars a
    p

    instance LocalTerminationEnv (CSPatI o) where
      sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat])
    sizeAndBoundVars = \case
        CSPatConApp ConstRef o
    _ [CSPat o]
    ps -> (Sum Nat
    1, []) (Sum Nat, [Nat]) -> (Sum Nat, [Nat]) -> (Sum Nat, [Nat])
    forall a. Semigroup a => a -> a -> a
    <> [CSPat o] -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars [CSPat o]
    ps
        CSPatVar Nat
    n       -> (Sum Nat
    0, [Nat
    n])
        CSPatExp MExp o
    e       -> MExp o -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars MExp o
    e
        CSPatI o
    _                -> (Sum Nat
    0, [])

    instance LocalTerminationEnv a => LocalTerminationEnv [a] where
      sizeAndBoundVars :: [a] -> (Sum Nat, [Nat])
    sizeAndBoundVars = (a -> (Sum Nat, [Nat])) -> [a] -> (Sum Nat, [Nat])
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap a -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars

    instance LocalTerminationEnv (MExp o) where
    --  sizeAndBoundVars e = case rm __IMPOSSIBLE__ e of
    -- GA: 2017 06 27: Not actually impossible! (cf. #2620)
      sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])
    sizeAndBoundVars Meta{} = (Sum Nat
    0, [])
    -- Does this default behaviour even make sense? The catchall in the
    -- following match seems to suggest it does
      sizeAndBoundVars (NotM Exp o
    e) = case Exp o
    e of
        App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v) MArgList o
    _      -> (Sum Nat
    0, [Nat
    v])
        App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Const ConstRef o
    _) MArgList o
    args -> (Sum Nat
    1, []) (Sum Nat, [Nat]) -> (Sum Nat, [Nat]) -> (Sum Nat, [Nat])
    forall a. Semigroup a => a -> a -> a
    <> MArgList o -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars MArgList o
    args
        Exp o
    _                      -> (Sum Nat
    0, [])

    instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where
      sizeAndBoundVars :: (a, b) -> (Sum Nat, [Nat])
    sizeAndBoundVars (a
    a, b
    b) = a -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars a
    a (Sum Nat, [Nat]) -> (Sum Nat, [Nat]) -> (Sum Nat, [Nat])
    forall a. Semigroup a => a -> a -> a
    <> b -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars b
    b

    instance LocalTerminationEnv (MArgList o) where
      sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])
    sizeAndBoundVars MArgList o
    as = case Empty -> MArgList o -> ArgList o
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MArgList o
    as of
        ArgList o
    ALNil         -> (Sum Nat
    0, [])
        ALCons Hiding
    _ MExp o
    a MArgList o
    as -> (MExp o, MArgList o) -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars (MExp o
    a, MArgList o
    as)
        ALProj{}      -> (Sum Nat, [Nat])
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        ALConPar MArgList o
    as   -> MArgList o -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars MArgList o
    as

    -- | Take a list of patterns and returns (is, size, vars) where (speculation):
    ---  * the is are the pattern indices the vars are contained in
    --   * size is total number of constructors removed (?) to access vars
    localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])
    localTerminationEnv :: forall o. [CSPat o] -> ([Nat], Nat, [Nat])
    localTerminationEnv [CSPat o]
    pats = ([Nat]
    is, Sum Nat -> Nat
    forall a. Sum a -> a
    getSum Sum Nat
    s, [Nat]
    vs) where

      ([Nat]
    is , Sum Nat
    s , [Nat]
    vs) = Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    g Nat
    0 [CSPat o]
    pats

      g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
      g :: forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    g Nat
    _ [] = ([], Sum Nat
    0, [])
      g Nat
    i (hp :: CSPat o
    hp@(HI Hiding
    _ CSPatI o
    p) : [CSPat o]
    ps) = case CSPatI o
    p of
        CSPatConApp{} -> let (Sum Nat
    size, [Nat]
    vars) = CSPat o -> (Sum Nat, [Nat])
    forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
    sizeAndBoundVars CSPat o
    hp
                         in ([Nat
    i], Sum Nat
    size, [Nat]
    vars) ([Nat], Sum Nat, [Nat])
    -> ([Nat], Sum Nat, [Nat]) -> ([Nat], Sum Nat, [Nat])
    forall a. Semigroup a => a -> a -> a
    <> Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    g (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [CSPat o]
    ps
        CSPatI o
    _ -> Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
    g (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [CSPat o]
    ps

    localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
    localTerminationSidecond :: forall o.
    ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
    localTerminationSidecond ([Nat]
    is, Nat
    size, [Nat]
    vars) ConstRef o
    reccallc MExp o
    b =
      MExp o -> MetaEnv (PB (RefInfo o))
    ok MExp o
    b
     where
         ok :: MExp o -> MetaEnv (PB (RefInfo o))
    ok MExp o
    e = BlkInfo (RefInfo o)
    -> MExp o
    -> (Exp o -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall a blk.
    Refinable a blk =>
    BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase (Bool
    False, Prio
    prioNo, Maybe (RefInfo o)
    forall a. Maybe a
    Nothing) MExp o
    e ((Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o)))
    -> (Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \Exp o
    e -> case Exp o
    e of
          App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    elr MArgList o
    args -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
    Sidecondition
           (MArgList o -> MetaEnv (PB (RefInfo o))
    oks MArgList o
    args)
           (case Elr o
    elr of
              Const ConstRef o
    c | ConstRef o
    c ConstRef o -> ConstRef o -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConstRef o
    reccallc -> if Nat
    size Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0 then Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (String -> Prop (RefInfo o)
    forall blk. String -> Prop blk
    Error String
    "localTerminationSidecond: no size to decrement") else Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
    okcall Nat
    0 Nat
    size [Nat]
    vars MArgList o
    args
              Elr o
    _ -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop (RefInfo o)
    forall blk. Prop blk
    OK
           )
          Lam Hiding
    _ (Abs MId
    _ MExp o
    e) -> MExp o -> MetaEnv (PB (RefInfo o))
    ok MExp o
    e
          Pi Maybe (UId o)
    _ Hiding
    _ Bool
    _ MExp o
    it (Abs MId
    _ MExp o
    ot) -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
    Sidecondition
           (MExp o -> MetaEnv (PB (RefInfo o))
    ok MExp o
    it)
           (MExp o -> MetaEnv (PB (RefInfo o))
    ok MExp o
    ot)
          Sort{} -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop (RefInfo o)
    forall blk. Prop blk
    OK

          AbsurdLambda{} -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop (RefInfo o)
    forall blk. Prop blk
    OK

         oks :: MArgList o -> MetaEnv (PB (RefInfo o))
    oks MArgList o
    as = BlkInfo (RefInfo o)
    -> MArgList o
    -> (ArgList o -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall a blk.
    Refinable a blk =>
    BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase (Bool
    False, Prio
    prioNo, Maybe (RefInfo o)
    forall a. Maybe a
    Nothing) MArgList o
    as ((ArgList o -> MetaEnv (PB (RefInfo o)))
     -> MetaEnv (PB (RefInfo o)))
    -> (ArgList o -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \ArgList o
    as -> case ArgList o
    as of
          ArgList o
    ALNil -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop (RefInfo o)
    forall blk. Prop blk
    OK
          ALCons Hiding
    _ MExp o
    a MArgList o
    as -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
    Sidecondition
           (MExp o -> MetaEnv (PB (RefInfo o))
    ok MExp o
    a)
           (MArgList o -> MetaEnv (PB (RefInfo o))
    oks MArgList o
    as)

          ALProj MArgList o
    eas MM (ConstRef o) (RefInfo o)
    _ Hiding
    _ MArgList o
    as -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ MetaEnv (PB (RefInfo o))
    -> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
    forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
    Sidecondition (MArgList o -> MetaEnv (PB (RefInfo o))
    oks MArgList o
    eas) (MArgList o -> MetaEnv (PB (RefInfo o))
    oks MArgList o
    as)

          ALConPar MArgList o
    as -> MArgList o -> MetaEnv (PB (RefInfo o))
    oks MArgList o
    as

         okcall :: Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
    okcall Nat
    i Nat
    size [Nat]
    vars MArgList o
    as = BlkInfo (RefInfo o)
    -> MArgList o
    -> (ArgList o -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall a blk.
    Refinable a blk =>
    BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase (Bool
    False, Prio
    prioNo, Maybe (RefInfo o)
    forall a. Maybe a
    Nothing) MArgList o
    as ((ArgList o -> MetaEnv (PB (RefInfo o)))
     -> MetaEnv (PB (RefInfo o)))
    -> (ArgList o -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \ArgList o
    as -> case ArgList o
    as of
          ArgList o
    ALNil -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop (RefInfo o)
    forall blk. Prop blk
    OK
          ALCons Hiding
    _ MExp o
    a MArgList o
    as | Nat
    i Nat -> [Nat] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Nat]
    is ->
           Prio
    -> Maybe (RefInfo o)
    -> MetaEnv (MB (Maybe (Nat, [Nat])) (RefInfo o))
    -> (Maybe (Nat, [Nat]) -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall blk a.
    Prio
    -> Maybe blk
    -> MetaEnv (MB a blk)
    -> (a -> MetaEnv (PB blk))
    -> MetaEnv (PB blk)
    mbpcase Prio
    prioNo Maybe (RefInfo o)
    forall a. Maybe a
    Nothing (Nat
    -> [Nat] -> MExp o -> MetaEnv (MB (Maybe (Nat, [Nat])) (RefInfo o))
    forall {a} {o}.
    (Eq a, Num a) =>
    a
    -> [Nat]
    -> MM (Exp o) (RefInfo o)
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    he Nat
    size [Nat]
    vars MExp o
    a) ((Maybe (Nat, [Nat]) -> MetaEnv (PB (RefInfo o)))
     -> MetaEnv (PB (RefInfo o)))
    -> (Maybe (Nat, [Nat]) -> MetaEnv (PB (RefInfo o)))
    -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \Maybe (Nat, [Nat])
    x -> case Maybe (Nat, [Nat])
    x of
            Maybe (Nat, [Nat])
    Nothing -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
    -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ String -> Prop (RefInfo o)
    forall blk. String -> Prop blk
    Error String
    "localTerminationSidecond: reccall not ok"
            Just (Nat
    size', [Nat]
    vars') -> Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
    okcall (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) Nat
    size' [Nat]
    vars' MArgList o
    as
          ALCons Hiding
    _ MExp o
    a MArgList o
    as -> Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
    okcall (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) Nat
    size [Nat]
    vars MArgList o
    as

          ALProj{} -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
    forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop (RefInfo o)
    forall blk. Prop blk
    OK

          ALConPar MArgList o
    as -> MetaEnv (PB (RefInfo o))
    forall a. HasCallStack => a
    __IMPOSSIBLE__

         he :: a
    -> [Nat]
    -> MM (Exp o) (RefInfo o)
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    he a
    size [Nat]
    vars MM (Exp o) (RefInfo o)
    e = MM (Exp o) (RefInfo o)
    -> (Exp o -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk b.
    Refinable a blk =>
    MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmcase MM (Exp o) (RefInfo o)
    e ((Exp o -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
     -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> (Exp o -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \Exp o
    e -> case Exp o
    e of
          App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Var Nat
    v) MArgList o
    _ ->
           case Nat -> [Nat] -> Maybe [Nat]
    forall {a}. Eq a => a -> [a] -> Maybe [a]
    remove Nat
    v [Nat]
    vars of
            Maybe [Nat]
    Nothing -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret Maybe (a, [Nat])
    forall a. Maybe a
    Nothing
            Just [Nat]
    vars' -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret (Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ (a, [Nat]) -> Maybe (a, [Nat])
    forall a. a -> Maybe a
    Just (a
    size, [Nat]
    vars')
          App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ (Const ConstRef o
    c) MArgList o
    args -> do
           ConstDef o
    cd <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c
           case ConstDef o -> DeclCont o
    forall o. ConstDef o -> DeclCont o
    cdcont ConstDef o
    cd of
            Constructor{} ->
             if a
    size a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    1 then
              Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret Maybe (a, [Nat])
    forall a. Maybe a
    Nothing
             else
              a
    -> [Nat]
    -> MArgList o
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    hes (a
    size a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    1) [Nat]
    vars MArgList o
    args
            DeclCont o
    _ -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret Maybe (a, [Nat])
    forall a. Maybe a
    Nothing
          Exp o
    _ -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret Maybe (a, [Nat])
    forall a. Maybe a
    Nothing
         hes :: a
    -> [Nat]
    -> MArgList o
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    hes a
    size [Nat]
    vars MArgList o
    as = MArgList o
    -> (ArgList o -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk b.
    Refinable a blk =>
    MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmcase MArgList o
    as ((ArgList o -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
     -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> (ArgList o -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \ArgList o
    as -> case ArgList o
    as of
          ArgList o
    ALNil -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret (Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ (a, [Nat]) -> Maybe (a, [Nat])
    forall a. a -> Maybe a
    Just (a
    size, [Nat]
    vars)
          ALCons Hiding
    _ MM (Exp o) (RefInfo o)
    a MArgList o
    as ->
           MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    -> (Maybe (a, [Nat])
        -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk b.
    MetaEnv (MB a blk)
    -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mbcase (a
    -> [Nat]
    -> MM (Exp o) (RefInfo o)
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    he a
    size [Nat]
    vars MM (Exp o) (RefInfo o)
    a) ((Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
     -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> (Maybe (a, [Nat])
        -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o)))
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ \Maybe (a, [Nat])
    x -> case Maybe (a, [Nat])
    x of
            Maybe (a, [Nat])
    Nothing -> Maybe (a, [Nat]) -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a blk. a -> MetaEnv (MB a blk)
    mbret Maybe (a, [Nat])
    forall a. Maybe a
    Nothing
            Just (a
    size', [Nat]
    vars') -> a
    -> [Nat]
    -> MArgList o
    -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    hes a
    size' [Nat]
    vars' MArgList o
    as

          ALProj{} -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          ALConPar MArgList o
    as -> MetaEnv (MB (Maybe (a, [Nat])) (RefInfo o))
    forall a. HasCallStack => a
    __IMPOSSIBLE__

         remove :: a -> [a] -> Maybe [a]
    remove a
    _ [] = Maybe [a]
    forall a. Maybe a
    Nothing
         remove a
    x (a
    y : [a]
    ys) | a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y = [a] -> Maybe [a]
    forall a. a -> Maybe a
    Just [a]
    ys
         remove a
    x (a
    y : [a]
    ys) = case a -> [a] -> Maybe [a]
    remove a
    x [a]
    ys of {Maybe [a]
    Nothing -> Maybe [a]
    forall a. Maybe a
    Nothing; Just [a]
    ys' -> [a] -> Maybe [a]
    forall a. a -> Maybe a
    Just (a
    y a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    ys')}

    -- ---------------------------

    getblks :: MExp o -> IO [Nat]
    getblks :: forall o. MExp o -> IO [Nat]
    getblks MExp o
    tt = do
     NotB (HNExp o
    hntt, HNNBlks o
    blks) <- ICExp o -> EE (MB (HNExp o, HNNBlks o) (RefInfo o))
    forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
    hnn_blks ([CAction o] -> MExp o -> ICExp o
    forall a o. [CAction o] -> a -> Clos a o
    Clos [] MExp o
    tt)
     case HNNBlks o -> Maybe Nat
    forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
    f HNNBlks o
    blks of
      Just Nat
    v -> [Nat] -> IO [Nat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Nat
    v]
      Maybe Nat
    Nothing -> case HNExp o -> HNExp' o
    forall a o. WithSeenUIds a o -> a
    rawValue HNExp o
    hntt of
       HNApp (Const ConstRef o
    c) ICArgList o
    args -> do
        ConstDef o
    cd <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c
        case ConstDef o -> DeclCont o
    forall o. ConstDef o -> DeclCont o
    cdcont ConstDef o
    cd of
         Datatype{} -> [Nat] -> ICArgList o -> IO [Nat]
    forall {o}. [Nat] -> ICArgList o -> IO [Nat]
    g [] ICArgList o
    args
         DeclCont o
    _ -> [Nat] -> IO [Nat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
       HNExp' o
    _ -> [Nat] -> IO [Nat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
     where
      f :: [WithSeenUIds (HNExp' o) o] -> Maybe Nat
    f [WithSeenUIds (HNExp' o) o]
    blks = case [WithSeenUIds (HNExp' o) o]
    blks of
                 (WithSeenUIds (HNExp' o) o
    b : [WithSeenUIds (HNExp' o) o]
    bs) -> case WithSeenUIds (HNExp' o) o -> HNExp' o
    forall a o. WithSeenUIds a o -> a
    rawValue (WithSeenUIds (HNExp' o) o
    -> [WithSeenUIds (HNExp' o) o] -> WithSeenUIds (HNExp' o) o
    forall a. a -> [a] -> a
    last1 WithSeenUIds (HNExp' o) o
    b [WithSeenUIds (HNExp' o) o]
    bs) of
                  HNApp (Var Nat
    v) ICArgList o
    _ -> Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just Nat
    v
                  HNExp' o
    _ -> Maybe Nat
    forall a. Maybe a
    Nothing
                 [WithSeenUIds (HNExp' o) o]
    _ -> Maybe Nat
    forall a. Maybe a
    Nothing
      g :: [Nat] -> ICArgList o -> IO [Nat]
    g [Nat]
    vs ICArgList o
    args = do
       NotB HNArgList o
    hnargs <- ICArgList o -> EE (MB (HNArgList o) (RefInfo o))
    forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
    hnarglist ICArgList o
    args
       case HNArgList o
    hnargs of
        HNALCons Hiding
    _ ICExp o
    a ICArgList o
    as -> do
         NotB (HNExp o
    _, HNNBlks o
    blks) <- ICExp o -> EE (MB (HNExp o, HNNBlks o) (RefInfo o))
    forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
    hnn_blks ICExp o
    a
         let vs' :: [Nat]
    vs' = case HNNBlks o -> Maybe Nat
    forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
    f HNNBlks o
    blks of
                    Just Nat
    v | Nat
    v Nat -> [Nat] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [Nat]
    vs -> Nat
    v Nat -> [Nat] -> [Nat]
    forall a. a -> [a] -> [a]
    : [Nat]
    vs
                    Maybe Nat
    _ -> [Nat]
    vs
         [Nat] -> ICArgList o -> IO [Nat]
    g [Nat]
    vs' ICArgList o
    as
        HNArgList o
    _ -> [Nat] -> IO [Nat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Nat]
    vs
    -- ---------------------------