    module Agda.Auto.Syntax where

    import Data.IORef
    import qualified Data.Set as Set

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

    import Agda.Utils.Impossible

    -- | Unique identifiers for variable occurrences in unification.
    type UId o = Metavar (Exp o) (RefInfo o)

    data HintMode = HMNormal
                  | HMRecCall

    data EqReasoningConsts o = EqReasoningConsts
      { forall o. EqReasoningConsts o -> ConstRef o
    eqrcId    -- "_≡_"
      , forall o. EqReasoningConsts o -> ConstRef o
    eqrcBegin -- "begin_"
      , forall o. EqReasoningConsts o -> ConstRef o
    eqrcStep  -- "_≡⟨_⟩_"
      , forall o. EqReasoningConsts o -> ConstRef o
    eqrcEnd   -- "_∎"
      , forall o. EqReasoningConsts o -> ConstRef o
    eqrcSym   -- "sym"
      , forall o. EqReasoningConsts o -> ConstRef o
    eqrcCong  -- "cong"
      :: ConstRef o
      }

    data EqReasoningState = EqRSNone | EqRSChain | EqRSPrf1 | EqRSPrf2 | EqRSPrf3
     deriving (EqReasoningState -> EqReasoningState -> Bool
    (EqReasoningState -> EqReasoningState -> Bool)
    -> (EqReasoningState -> EqReasoningState -> Bool)
    -> Eq EqReasoningState
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: EqReasoningState -> EqReasoningState -> Bool
    $c/= :: EqReasoningState -> EqReasoningState -> Bool
    == :: EqReasoningState -> EqReasoningState -> Bool
    $c== :: EqReasoningState -> EqReasoningState -> Bool
    Eq, Int -> EqReasoningState -> ShowS
    [EqReasoningState] -> ShowS
    EqReasoningState -> String
    (Int -> EqReasoningState -> ShowS)
    -> (EqReasoningState -> String)
    -> ([EqReasoningState] -> ShowS)
    -> Show EqReasoningState
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [EqReasoningState] -> ShowS
    $cshowList :: [EqReasoningState] -> ShowS
    show :: EqReasoningState -> String
    $cshow :: EqReasoningState -> String
    showsPrec :: Int -> EqReasoningState -> ShowS
    $cshowsPrec :: Int -> EqReasoningState -> ShowS
    Show)

    -- | The concrete instance of the 'blk' parameter in 'Metavar'.
    --   I.e., the information passed to the search control.

    data RefInfo o
      = RIEnv
        { forall o. RefInfo o -> [(ConstRef o, HintMode)]
    rieHints :: [(ConstRef o, HintMode)]
        , forall o. RefInfo o -> Int
    rieDefFreeVars :: Nat
          -- ^ Nat - deffreevars
          --   (to make cost of using module parameters correspond to that of hints).
        , forall o. RefInfo o -> Maybe (EqReasoningConsts o)
    rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
        }
      | RIMainInfo
        { forall o. RefInfo o -> Int
    riMainCxtLength :: Nat
          -- ^ Size of typing context in which meta was created.
        , forall o. RefInfo o -> HNExp o
    riMainType      :: HNExp o
          -- ^ Head normal form of type of meta.
        , forall o. RefInfo o -> Bool
    riMainIota      :: Bool
           -- ^ True if iota steps performed when normalising target type
           --   (used to put cost when traversing a definition
           --    by construction instantiation).
        }
      | RIUnifInfo [CAction o] (HNExp o)
        -- meta environment, opp hne
      | RICopyInfo (ICExp o)
      | RIIotaStep Bool -- True - semiflex
      | RIInferredTypeUnknown
      | RINotConstructor
      | RIUsedVars [UId o] [Elr o]
      | RIPickSubsvar

      | RIEqRState EqReasoningState

      | RICheckElim Bool -- isdep
      | RICheckProjIndex [ConstRef o] -- noof proj functions

    type MyPB o = PB (RefInfo o)
    type MyMB a o = MB a (RefInfo o)

    type Nat = Int

    data MId = Id String
             | NoId

    -- | Abstraction with maybe a name.
    --
    --   Different from Agda, where there is also info
    --   whether function is constant.
    data Abs a = Abs MId a

    -- | Constant signatures.

    data ConstDef o = ConstDef
      { forall o. ConstDef o -> String
    cdname        :: String
        -- ^ For debug printing.
      , forall o. ConstDef o -> o
    cdorigin      :: o
        -- ^ Reference to the Agda constant.
      , forall o. ConstDef o -> MExp o
    cdtype        :: MExp o
        -- ^ Type of constant.
      , forall o. ConstDef o -> DeclCont o
    cdcont        :: DeclCont o
        -- ^ Constant definition.
      , forall o. ConstDef o -> Int
    cddeffreevars :: Nat
        -- ^ Free vars of the module where the constant is defined..
      } -- contains no metas

    -- | Constant definitions.

    data DeclCont o
      = Def Nat [Clause o] (Maybe Nat) -- maybe an index to elimand argument
                           (Maybe Nat) -- maybe index to elim arg if semiflex
      | Datatype [ConstRef o] -- constructors
                 [ConstRef o] -- projection functions (in case it is a record)

      | Constructor Nat -- number of omitted args
      | Postulate

    type Clause o = ([Pat o], MExp o)

    data Pat o
      = PatConApp (ConstRef o) [Pat o]
      | PatVar String
      | PatExp
        -- ^ Dot pattern.
    {- TODO: projection patterns.
      | PatProj (ConstRef o)
        -- ^ Projection pattern.
    -}

    type ConstRef o = IORef (ConstDef o)

    -- | Head of application (elimination).
    data Elr o
      = Var Nat
      | Const (ConstRef o)
      deriving (Elr o -> Elr o -> Bool
    (Elr o -> Elr o -> Bool) -> (Elr o -> Elr o -> Bool) -> Eq (Elr o)
    forall o. Elr o -> Elr o -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Elr o -> Elr o -> Bool
    $c/= :: forall o. Elr o -> Elr o -> Bool
    == :: Elr o -> Elr o -> Bool
    $c== :: forall o. Elr o -> Elr o -> Bool
    Eq)

    getVar :: Elr o -> Maybe Nat
    getVar :: forall o. Elr o -> Maybe Int
    getVar (Var Int
    n) = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    n
    getVar Const{} = Maybe Int
    forall a. Maybe a
    Nothing

    getConst :: Elr o -> Maybe (ConstRef o)
    getConst :: forall o. Elr o -> Maybe (ConstRef o)
    getConst (Const ConstRef o
    c) = ConstRef o -> Maybe (ConstRef o)
    forall a. a -> Maybe a
    Just ConstRef o
    c
    getConst Var{}     = Maybe (ConstRef o)
    forall a. Maybe a
    Nothing

    data Sort
      = Set Nat
      | UnknownSort
      | Type

    -- | Agsy's internal syntax.
    data Exp o
      = App
        { forall o. Exp o -> Maybe (UId o)
    appUId   :: Maybe (UId o)
          -- ^ Unique identifier of the head.
        , forall o. Exp o -> OKHandle (RefInfo o)
    appOK    :: OKHandle (RefInfo o)
          -- ^ This application has been type-checked.
        , forall o. Exp o -> Elr o
    appHead  :: Elr o
          -- ^ Head.
        , forall o. Exp o -> MArgList o
    appElims :: MArgList o
          -- ^ Arguments.
        }
      | Lam Hiding (Abs (MExp o))
        -- ^ Lambda with hiding information.
      | Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))
        -- ^ @True@ if possibly dependent (var not known to not occur).
        --   @False@ if non-dependent.
      | Sort Sort
      | AbsurdLambda Hiding
        -- ^ Absurd lambda with hiding information.

    dontCare :: Exp o
    dontCare :: forall o. Exp o
    dontCare = Sort -> Exp o
    forall o. Sort -> Exp o
    Sort Sort
    UnknownSort

    -- | "Maybe expression":  Expression or reference to meta variable.
    type MExp o = MM (Exp o) (RefInfo o)

    data ArgList o
      = ALNil
        -- ^ No more eliminations.
      | ALCons Hiding (MExp o) (MArgList o)
        -- ^ Application and tail.

      | ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)
        -- ^ proj pre args, projfcn idx, tail

      | ALConPar (MArgList o)
        -- ^ Constructor parameter (missing in Agda).
        --   Agsy has monomorphic constructors.
        --   Inserted to cover glitch of polymorphic constructor
        --   applications coming from Agda

    type MArgList o = MM (ArgList o) (RefInfo o)

    data WithSeenUIds a o = WithSeenUIds
      { forall a o. WithSeenUIds a o -> [Maybe (UId o)]
    seenUIds :: [Maybe (UId o)]
      , forall a o. WithSeenUIds a o -> a
    rawValue :: a
      }

    type HNExp o = WithSeenUIds (HNExp' o) o

    data HNExp' o =
        HNApp  (Elr o) (ICArgList o)
      | HNLam  Hiding (Abs (ICExp o))
      | HNPi   Hiding Bool (ICExp o) (Abs (ICExp o))
      | HNSort Sort

    -- | Head-normal form of 'ICArgList'.  First entry is exposed.
    --
    --   Q: Why are there no projection eliminations?
    data HNArgList o = HNALNil
                     | HNALCons Hiding (ICExp o) (ICArgList o)
                     | HNALConPar (ICArgList o)

    -- | Lazy concatenation of argument lists under explicit substitutions.
    data ICArgList o = CALNil
                     | CALConcat (Clos (MArgList o) o) (ICArgList o)

    -- | An expression @a@ in an explicit substitution @[CAction a]@.
    type ICExp o  = Clos (MExp o) o
    data Clos a o = Clos [CAction o] a

    type CExp o   = TrBr (ICExp o) o
    data TrBr a o = TrBr [MExp o] a

    -- | Entry of an explicit substitution.
    --
    --   An explicit substitution is a list of @CAction@s.
    --   This is isomorphic to the usual presentation where
    --   @Skip@ and @Weak@ would be constructors of exp. substs.

    data CAction o
      = Sub (ICExp o)
        -- ^ Instantation of variable.
      | Skip
        -- ^ For going under a binder, often called "Lift".
      | Weak Nat
        -- ^ Shifting substitution (going to a larger context).

    type Ctx o = [(MId, CExp o)]

    type EE = IO

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

    detecteliminand :: [Clause o] -> Maybe Nat
    detecteliminand :: forall o. [Clause o] -> Maybe Int
    detecteliminand [Clause o]
    cls =
     case (Clause o -> Maybe Int) -> [Clause o] -> [Maybe Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause o -> Maybe Int
    forall {t} {o} {b}. Num t => ([Pat o], b) -> Maybe t
    cleli [Clause o]
    cls of
      [] -> Maybe Int
    forall a. Maybe a
    Nothing
      (Maybe Int
    i:[Maybe Int]
    is) -> if (Maybe Int -> Bool) -> [Maybe Int] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Maybe Int
    i Maybe Int -> Maybe Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) [Maybe Int]
    is then Maybe Int
    i else Maybe Int
    forall a. Maybe a
    Nothing
     where
      cleli :: ([Pat o], b) -> Maybe t
    cleli ([Pat o]
    pats, b
    _) = t -> [Pat o] -> Maybe t
    forall {t} {o}. Num t => t -> [Pat o] -> Maybe t
    pateli t
    0 [Pat o]
    pats
      pateli :: t -> [Pat o] -> Maybe t
    pateli t
    i (PatConApp ConstRef o
    _ [Pat o]
    args : [Pat o]
    pats) = if (Pat o -> Bool) -> [Pat o] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Pat o -> Bool
    forall {o}. Pat o -> Bool
    notcon ([Pat o]
    args [Pat o] -> [Pat o] -> [Pat o]
    forall a. [a] -> [a] -> [a]
    ++ [Pat o]
    pats) then t -> Maybe t
    forall a. a -> Maybe a
    Just t
    i else Maybe t
    forall a. Maybe a
    Nothing
      pateli t
    i (Pat o
    _ : [Pat o]
    pats) = t -> [Pat o] -> Maybe t
    pateli (t
    i t -> t -> t
    forall a. Num a => a -> a -> a
    + t
    1) [Pat o]
    pats
      pateli t
    i [] = Maybe t
    forall a. Maybe a
    Nothing
      notcon :: Pat o -> Bool
    notcon PatConApp{} = Bool
    False
      notcon Pat o
    _ = Bool
    True

    detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
    detectsemiflex :: forall o. ConstRef o -> [Clause o] -> IO Bool
    detectsemiflex ConstRef o
    _ [Clause o]
    _ = Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False -- disabled

    categorizedecl :: ConstRef o -> IO ()
    categorizedecl :: forall o. ConstRef o -> IO ()
    categorizedecl ConstRef o
    c = 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
      Def Int
    narg [Clause o]
    cls Maybe Int
    _ Maybe Int
    _ -> do
       Bool
    semif <- ConstRef o -> [Clause o] -> IO Bool
    forall o. ConstRef o -> [Clause o] -> IO Bool
    detectsemiflex ConstRef o
    c [Clause o]
    cls
       let elim :: Maybe Int
    elim = [Clause o] -> Maybe Int
    forall o. [Clause o] -> Maybe Int
    detecteliminand [Clause o]
    cls
           semifb :: Maybe Int
    semifb = case (Bool
    semif, Maybe Int
    elim) of
                     (Bool
    True, Just Int
    i) -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i -- just copying val of elim arg. this should be changed
                     (Bool
    _, Maybe Int
    _) -> Maybe Int
    forall a. Maybe a
    Nothing
       ConstRef o -> ConstDef o -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef ConstRef o
    c (ConstDef o
    cd {cdcont :: DeclCont o
    cdcont = Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
    forall o. Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
    Def Int
    narg [Clause o]
    cls Maybe Int
    elim Maybe Int
    semifb})
      DeclCont o
    _ -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

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

    class MetaliseOKH t where
      metaliseOKH :: t -> IO t

    instance MetaliseOKH t => MetaliseOKH (MM t a) where
      metaliseOKH :: MM t a -> IO (MM t a)
    metaliseOKH = \case
        Meta Metavar t a
    m -> MM t a -> IO (MM t a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MM t a -> IO (MM t a)) -> MM t a -> IO (MM t a)
    forall a b. (a -> b) -> a -> b
    $ Metavar t a -> MM t a
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar t a
    m
        NotM t
    e -> t -> MM t a
    forall a blk. a -> MM a blk
    NotM (t -> MM t a) -> IO t -> IO (MM t a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> IO t
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH t
    e

    instance MetaliseOKH t => MetaliseOKH (Abs t) where
      metaliseOKH :: Abs t -> IO (Abs t)
    metaliseOKH (Abs MId
    id t
    b) = MId -> t -> Abs t
    forall a. MId -> a -> Abs a
    Abs MId
    id (t -> Abs t) -> IO t -> IO (Abs t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> IO t
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH t
    b

    instance MetaliseOKH (Exp o) where
      metaliseOKH :: Exp o -> IO (Exp o)
    metaliseOKH = \case
        App Maybe (UId o)
    uid OKHandle (RefInfo o)
    okh Elr o
    elr MArgList o
    args ->
          (\ OKHandle (RefInfo o)
    m -> 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)
    m Elr o
    elr) (OKHandle (RefInfo o) -> MArgList o -> Exp o)
    -> IO (OKHandle (RefInfo o)) -> IO (MArgList o -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Metavar OKVal (RefInfo o) -> OKHandle (RefInfo o)
    forall a blk. Metavar a blk -> MM a blk
    Meta (Metavar OKVal (RefInfo o) -> OKHandle (RefInfo o))
    -> IO (Metavar OKVal (RefInfo o)) -> IO (OKHandle (RefInfo o))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO (Metavar OKVal (RefInfo o))
    forall a blk. IO (Metavar a blk)
    initMeta) IO (MArgList o -> Exp o) -> IO (MArgList o) -> IO (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MArgList o -> IO (MArgList o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH 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 (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (MExp o) -> IO (Abs (MExp o))
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH Abs (MExp o)
    b
        Pi Maybe (UId o)
    uid Hiding
    hid Bool
    dep MExp o
    it Abs (MExp o)
    ot ->
          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
    dep (MExp o -> Abs (MExp o) -> Exp o)
    -> IO (MExp o) -> IO (Abs (MExp o) -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MExp o -> IO (MExp o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH MExp o
    it IO (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs (MExp o) -> IO (Abs (MExp o))
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH Abs (MExp o)
    ot
        e :: Exp o
    e@Sort{} -> Exp o -> IO (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp o
    e
        e :: Exp o
    e@AbsurdLambda{} -> Exp o -> IO (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp o
    e

    instance MetaliseOKH (ArgList o) where
      metaliseOKH :: ArgList o -> IO (ArgList o)
    metaliseOKH = \case
        ArgList o
    ALNil -> ArgList o -> IO (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)
    -> IO (MExp o) -> IO (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MExp o -> IO (MExp o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH MExp o
    a IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MArgList o -> IO (MArgList o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH MArgList o
    as
        ALProj MArgList o
    eas MM (ConstRef o) (RefInfo o)
    idx Hiding
    hid MArgList o
    as ->
          (\ MArgList o
    eas -> MArgList o
    -> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
    forall o.
    MArgList o
    -> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
    ALProj MArgList o
    eas MM (ConstRef o) (RefInfo o)
    idx Hiding
    hid) (MArgList o -> MArgList o -> ArgList o)
    -> IO (MArgList o) -> IO (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MArgList o -> IO (MArgList o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH MArgList o
    eas IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MArgList o -> IO (MArgList o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH MArgList o
    as
        ALConPar MArgList o
    as -> MArgList o -> ArgList o
    forall o. MArgList o -> ArgList o
    ALConPar (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MArgList o -> IO (MArgList o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH MArgList o
    as

    metaliseokh :: MExp o -> IO (MExp o)
    metaliseokh :: forall o. MExp o -> IO (MExp o)
    metaliseokh = MExp o -> IO (MExp o)
    forall t. MetaliseOKH t => t -> IO t
    metaliseOKH

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

    class ExpandMetas t where
      expandMetas :: t -> IO t

    instance ExpandMetas t => ExpandMetas (MM t a) where
      expandMetas :: MM t a -> IO (MM t a)
    expandMetas = \case
        NotM t
    e -> t -> MM t a
    forall a blk. a -> MM a blk
    NotM (t -> MM t a) -> IO t -> IO (MM t a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> IO t
    forall t. ExpandMetas t => t -> IO t
    expandMetas t
    e
        Meta Metavar t a
    m -> do
          Maybe t
    mb <- IORef (Maybe t) -> IO (Maybe t)
    forall a. IORef a -> IO a
    readIORef (Metavar t a -> IORef (Maybe t)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind Metavar t a
    m)
          case Maybe t
    mb of
            Maybe t
    Nothing -> MM t a -> IO (MM t a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MM t a -> IO (MM t a)) -> MM t a -> IO (MM t a)
    forall a b. (a -> b) -> a -> b
    $ Metavar t a -> MM t a
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar t a
    m
            Just t
    e  -> t -> MM t a
    forall a blk. a -> MM a blk
    NotM (t -> MM t a) -> IO t -> IO (MM t a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> IO t
    forall t. ExpandMetas t => t -> IO t
    expandMetas t
    e

    instance ExpandMetas t => ExpandMetas (Abs t) where
      expandMetas :: Abs t -> IO (Abs t)
    expandMetas (Abs MId
    id t
    b) = MId -> t -> Abs t
    forall a. MId -> a -> Abs a
    Abs MId
    id (t -> Abs t) -> IO t -> IO (Abs t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> IO t
    forall t. ExpandMetas t => t -> IO t
    expandMetas t
    b

    instance ExpandMetas (Exp o) where
      expandMetas :: Exp o -> IO (Exp o)
    expandMetas = \case
        App Maybe (UId o)
    uid OKHandle (RefInfo o)
    okh Elr o
    elr MArgList o
    args -> 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)
    okh Elr o
    elr (MArgList o -> Exp o) -> IO (MArgList o) -> IO (Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MArgList o -> IO (MArgList o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas 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 (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (MExp o) -> IO (Abs (MExp o))
    forall t. ExpandMetas t => t -> IO t
    expandMetas Abs (MExp o)
    b
        Pi Maybe (UId o)
    uid Hiding
    hid Bool
    dep MExp o
    it Abs (MExp o)
    ot ->
          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
    dep (MExp o -> Abs (MExp o) -> Exp o)
    -> IO (MExp o) -> IO (Abs (MExp o) -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MExp o -> IO (MExp o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MExp o
    it IO (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs (MExp o) -> IO (Abs (MExp o))
    forall t. ExpandMetas t => t -> IO t
    expandMetas Abs (MExp o)
    ot
        t :: Exp o
    t@Sort{} -> Exp o -> IO (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp o
    t
        t :: Exp o
    t@AbsurdLambda{} -> Exp o -> IO (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp o
    t

    instance ExpandMetas (ArgList o) where
      expandMetas :: ArgList o -> IO (ArgList o)
    expandMetas = \case
        ArgList o
    ALNil -> ArgList o -> IO (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)
    -> IO (MExp o) -> IO (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MExp o -> IO (MExp o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MExp o
    a IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MArgList o -> IO (MArgList o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MArgList o
    as
        ALProj MArgList o
    eas MM (ConstRef o) (RefInfo o)
    idx Hiding
    hid MArgList o
    as ->
          (\ MArgList o
    a MM (ConstRef o) (RefInfo o)
    b -> MArgList o
    -> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
    forall o.
    MArgList o
    -> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
    ALProj MArgList o
    a MM (ConstRef o) (RefInfo o)
    b Hiding
    hid) (MArgList o
     -> MM (ConstRef o) (RefInfo o) -> MArgList o -> ArgList o)
    -> IO (MArgList o)
    -> IO (MM (ConstRef o) (RefInfo o) -> MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MArgList o -> IO (MArgList o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MArgList o
    eas
          IO (MM (ConstRef o) (RefInfo o) -> MArgList o -> ArgList o)
    -> IO (MM (ConstRef o) (RefInfo o)) -> IO (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MM (ConstRef o) (RefInfo o) -> IO (MM (ConstRef o) (RefInfo o))
    forall a blk. MM a blk -> MetaEnv (MM a blk)
    expandbind MM (ConstRef o) (RefInfo o)
    idx IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MArgList o -> IO (MArgList o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MArgList o
    as
        ALConPar MArgList o
    as -> MArgList o -> ArgList o
    forall o. MArgList o -> ArgList o
    ALConPar (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MArgList o -> IO (MArgList o)
    forall t. ExpandMetas t => t -> IO t
    expandMetas MArgList o
    as

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

    addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
    addtrailingargs :: forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
    addtrailingargs Clos (MArgList o) o
    newargs ICArgList o
    CALNil = Clos (MArgList o) o -> ICArgList o -> ICArgList o
    forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
    CALConcat Clos (MArgList o) o
    newargs ICArgList o
    forall o. ICArgList o
    CALNil
    addtrailingargs Clos (MArgList o) o
    newargs (CALConcat Clos (MArgList o) o
    x ICArgList o
    xs) = Clos (MArgList o) o -> ICArgList o -> ICArgList o
    forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
    CALConcat Clos (MArgList o) o
    x (Clos (MArgList o) o -> ICArgList o -> ICArgList o
    forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
    addtrailingargs Clos (MArgList o) o
    newargs ICArgList o
    xs)

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

    closify :: MExp o -> CExp o
    closify :: forall o. MExp o -> CExp o
    closify MExp o
    e = [MExp o] -> Clos (MExp o) o -> TrBr (Clos (MExp o) o) o
    forall a o. [MExp o] -> a -> TrBr a o
    TrBr [MExp o
    e] ([CAction o] -> MExp o -> Clos (MExp o) o
    forall a o. [CAction o] -> a -> Clos a o
    Clos [] MExp o
    e)

    sub :: MExp o -> CExp o -> CExp o
    -- sub e (Clos [] x) = Clos [Sub e] x
    sub :: forall o. MExp o -> CExp o -> CExp o
    sub MExp o
    e (TrBr [MExp o]
    trs (Clos (CAction o
    Skip : [CAction o]
    as) MExp o
    x)) = [MExp o] -> ICExp o -> TrBr (ICExp o) o
    forall a o. [MExp o] -> a -> TrBr a o
    TrBr (MExp o
    e MExp o -> [MExp o] -> [MExp o]
    forall a. a -> [a] -> [a]
    : [MExp o]
    trs) ([CAction o] -> MExp o -> ICExp o
    forall a o. [CAction o] -> a -> Clos a o
    Clos (ICExp o -> CAction o
    forall o. ICExp o -> CAction o
    Sub ([CAction o] -> MExp o -> ICExp o
    forall a o. [CAction o] -> a -> Clos a o
    Clos [] MExp o
    e) CAction o -> [CAction o] -> [CAction o]
    forall a. a -> [a] -> [a]
    : [CAction o]
    as) MExp o
    x)
    {-sub e (Clos (Weak n : as) x) = if n == 1 then
                                    Clos as x
                                   else
                                    Clos (Weak (n - 1) : as) x-}
    sub MExp o
    _ TrBr (ICExp o) o
    _ = TrBr (ICExp o) o
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    subi :: MExp o -> ICExp o -> ICExp o
    subi :: forall o. MExp o -> ICExp o -> ICExp o
    subi MExp o
    e (Clos (CAction o
    Skip : [CAction o]
    as) MExp o
    x) = [CAction o] -> MExp o -> Clos (MExp o) o
    forall a o. [CAction o] -> a -> Clos a o
    Clos (Clos (MExp o) o -> CAction o
    forall o. ICExp o -> CAction o
    Sub ([CAction o] -> MExp o -> Clos (MExp o) o
    forall a o. [CAction o] -> a -> Clos a o
    Clos [] MExp o
    e) CAction o -> [CAction o] -> [CAction o]
    forall a. a -> [a] -> [a]
    : [CAction o]
    as) MExp o
    x
    subi MExp o
    _ Clos (MExp o) o
    _ = Clos (MExp o) o
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    weak :: Weakening t => Nat -> t -> t
    weak :: forall t. Weakening t => Int -> t -> t
    weak Int
    0 = t -> t
    forall a. a -> a
    id
    weak Int
    n = Int -> t -> t
    forall t. Weakening t => Int -> t -> t
    weak' Int
    n

    class Weakening t where
      weak' :: Nat -> t -> t

    instance Weakening a => Weakening (TrBr a o) where
      weak' :: Int -> TrBr a o -> TrBr a o
    weak' Int
    n (TrBr [MExp o]
    trs a
    e) = [MExp o] -> a -> TrBr a o
    forall a o. [MExp o] -> a -> TrBr a o
    TrBr [MExp o]
    trs (Int -> a -> a
    forall t. Weakening t => Int -> t -> t
    weak' Int
    n a
    e)

    instance Weakening (Clos a o) where
      weak' :: Int -> Clos a o -> Clos a o
    weak' Int
    n (Clos [CAction o]
    as a
    x) = [CAction o] -> a -> Clos a o
    forall a o. [CAction o] -> a -> Clos a o
    Clos (Int -> CAction o
    forall o. Int -> CAction o
    Weak Int
    n CAction o -> [CAction o] -> [CAction o]
    forall a. a -> [a] -> [a]
    : [CAction o]
    as) a
    x

    instance Weakening (ICArgList o) where
      weak' :: Int -> ICArgList o -> ICArgList o
    weak' Int
    n = \case
        ICArgList o
    CALNil         -> ICArgList o
    forall o. ICArgList o
    CALNil
        CALConcat Clos (MArgList o) o
    a ICArgList o
    as -> Clos (MArgList o) o -> ICArgList o -> ICArgList o
    forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
    CALConcat (Int -> Clos (MArgList o) o -> Clos (MArgList o) o
    forall t. Weakening t => Int -> t -> t
    weak' Int
    n Clos (MArgList o) o
    a) (Int -> ICArgList o -> ICArgList o
    forall t. Weakening t => Int -> t -> t
    weak' Int
    n ICArgList o
    as)

    instance Weakening (Elr o) where
      weak' :: Int -> Elr o -> Elr o
    weak' Int
    n = (Int -> Int) -> Elr o -> Elr o
    forall t. Renaming t => (Int -> Int) -> t -> t
    rename (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +)

    -- | Substituting for a variable.
    doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)
    doclos :: forall o. [CAction o] -> Int -> Either Int (ICExp o)
    doclos = Int -> [CAction o] -> Int -> Either Int (ICExp o)
    forall {o}. Int -> [CAction o] -> Int -> Either Int (ICExp o)
    f Int
    0
     where
      -- ns is the number of weakenings
      f :: Int -> [CAction o] -> Int -> Either Int (ICExp o)
    f Int
    ns []            Int
    i = Int -> Either Int (ICExp o)
    forall a b. a -> Either a b
    Left (Int
    ns Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    i)
      f Int
    ns (Weak Int
    n : [CAction o]
    xs) Int
    i = Int -> [CAction o] -> Int -> Either Int (ICExp o)
    f (Int
    ns Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n) [CAction o]
    xs Int
    i
      f Int
    ns (Sub ICExp o
    s  : [CAction o]
    _ ) Int
    0 = ICExp o -> Either Int (ICExp o)
    forall a b. b -> Either a b
    Right (Int -> ICExp o -> ICExp o
    forall t. Weakening t => Int -> t -> t
    weak Int
    ns ICExp o
    s)
      f Int
    ns (CAction o
    Skip   : [CAction o]
    _ ) Int
    0 = Int -> Either Int (ICExp o)
    forall a b. a -> Either a b
    Left Int
    ns
      f Int
    ns (CAction o
    Skip   : [CAction o]
    xs) Int
    i = Int -> [CAction o] -> Int -> Either Int (ICExp o)
    f (Int
    ns Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [CAction o]
    xs (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
      f Int
    ns (Sub ICExp o
    _  : [CAction o]
    xs) Int
    i = Int -> [CAction o] -> Int -> Either Int (ICExp o)
    f Int
    ns [CAction o]
    xs (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)

    -- | FreeVars class and instances

    freeVars :: FreeVars t => t -> Set.Set Nat
    freeVars :: forall t. FreeVars t => t -> Set Int
    freeVars = Int -> t -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    0

    class FreeVars t where
      freeVarsOffset :: Nat -> t -> Set.Set Nat

    instance (FreeVars a, FreeVars b) => FreeVars (a, b) where
      freeVarsOffset :: Int -> (a, b) -> Set Int
    freeVarsOffset Int
    n (a
    a, b
    b) = Set Int -> Set Int -> Set Int
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (Int -> a -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n a
    a) (Int -> b -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n b
    b)

    instance FreeVars t => FreeVars (MM t a) where
      freeVarsOffset :: Int -> MM t a -> Set Int
    freeVarsOffset Int
    n MM t a
    e = Int -> t -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n (Empty -> MM t a -> t
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MM t a
    e)

    instance FreeVars t => FreeVars (Abs t) where
      freeVarsOffset :: Int -> Abs t -> Set Int
    freeVarsOffset Int
    n (Abs MId
    id t
    e) = Int -> t -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) t
    e

    instance FreeVars (Elr o) where
      freeVarsOffset :: Int -> Elr o -> Set Int
    freeVarsOffset Int
    n = \case
        Var Int
    v   -> Int -> Set Int
    forall a. a -> Set a
    Set.singleton (Int
    v Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n)
        Const{} -> Set Int
    forall a. Set a
    Set.empty

    instance FreeVars (Exp o) where
      freeVarsOffset :: Int -> Exp o -> Set Int
    freeVarsOffset Int
    n = \case
       App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    elr MArgList o
    args -> Int -> (Elr o, MArgList o) -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n (Elr o
    elr, MArgList o
    args)
       Lam Hiding
    _ Abs (MExp o)
    b          -> Int -> Abs (MExp o) -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n Abs (MExp o)
    b
       Pi Maybe (UId o)
    _ Hiding
    _ Bool
    _ MExp o
    it Abs (MExp o)
    ot   -> Int -> (MExp o, Abs (MExp o)) -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n (MExp o
    it, Abs (MExp o)
    ot)
       Sort{}           -> Set Int
    forall a. Set a
    Set.empty
       AbsurdLambda{}   -> Set Int
    forall a. Set a
    Set.empty

    instance FreeVars (ArgList o) where
      freeVarsOffset :: Int -> ArgList o -> Set Int
    freeVarsOffset Int
    n ArgList o
    es = case ArgList o
    es of
        ArgList o
    ALNil         -> Set Int
    forall a. Set a
    Set.empty
        ALCons Hiding
    _ MExp o
    e MArgList o
    es -> Int -> (MExp o, MArgList o) -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n (MExp o
    e, MArgList o
    es)
        ALConPar MArgList o
    es   -> Int -> MArgList o -> Set Int
    forall t. FreeVars t => Int -> t -> Set Int
    freeVarsOffset Int
    n MArgList o
    es
        ALProj{}      -> Set Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Renaming Typeclass and instances
    rename :: Renaming t => (Nat -> Nat) -> t -> t
    rename :: forall t. Renaming t => (Int -> Int) -> t -> t
    rename = Int -> (Int -> Int) -> t -> t
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    0

    class Renaming t where
      renameOffset :: Nat -> (Nat -> Nat) -> t -> t

    instance (Renaming a, Renaming b) => Renaming (a, b) where
      renameOffset :: Int -> (Int -> Int) -> (a, b) -> (a, b)
    renameOffset Int
    j Int -> Int
    ren (a
    a, b
    b) = (Int -> (Int -> Int) -> a -> a
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren a
    a, Int -> (Int -> Int) -> b -> b
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren b
    b)

    instance Renaming t => Renaming (MM t a) where
      renameOffset :: Int -> (Int -> Int) -> MM t a -> MM t a
    renameOffset Int
    j Int -> Int
    ren MM t a
    e = t -> MM t a
    forall a blk. a -> MM a blk
    NotM (t -> MM t a) -> t -> MM t a
    forall a b. (a -> b) -> a -> b
    $ Int -> (Int -> Int) -> t -> t
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren (Empty -> MM t a -> t
    forall a b. Empty -> MM a b -> a
    rm Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MM t a
    e)

    instance Renaming t => Renaming (Abs t) where
      renameOffset :: Int -> (Int -> Int) -> Abs t -> Abs t
    renameOffset Int
    j Int -> Int
    ren (Abs MId
    id t
    e) = MId -> t -> Abs t
    forall a. MId -> a -> Abs a
    Abs MId
    id (t -> Abs t) -> t -> Abs t
    forall a b. (a -> b) -> a -> b
    $ Int -> (Int -> Int) -> t -> t
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset (Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Int -> Int
    ren t
    e

    instance Renaming (Elr o) where
      renameOffset :: Int -> (Int -> Int) -> Elr o -> Elr o
    renameOffset Int
    j Int -> Int
    ren = \case
        Var Int
    v | Int
    v Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    j -> Int -> Elr o
    forall o. Int -> Elr o
    Var (Int -> Int
    ren (Int
    v Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    j) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    j)
        Elr o
    e              -> Elr o
    e

    instance Renaming (Exp o) where
      renameOffset :: Int -> (Int -> Int) -> Exp o -> Exp o
    renameOffset Int
    j Int -> Int
    ren = \case
        App Maybe (UId o)
    uid OKHandle (RefInfo o)
    ok Elr o
    elr MArgList o
    args -> (Elr o -> MArgList o -> Exp o) -> (Elr o, MArgList o) -> Exp o
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (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, MArgList o) -> Exp o) -> (Elr o, MArgList o) -> Exp o
    forall a b. (a -> b) -> a -> b
    $ Int -> (Int -> Int) -> (Elr o, MArgList o) -> (Elr o, MArgList o)
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren (Elr o
    elr, MArgList o
    args)
        Lam Hiding
    hid Abs (MExp o)
    e -> Hiding -> Abs (MExp o) -> Exp o
    forall o. Hiding -> Abs (MExp o) -> Exp o
    Lam Hiding
    hid (Int -> (Int -> Int) -> Abs (MExp o) -> Abs (MExp o)
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren Abs (MExp o)
    e)
        Pi Maybe (UId o)
    a Hiding
    b Bool
    c MExp o
    it Abs (MExp o)
    ot -> (MExp o -> Abs (MExp o) -> Exp o)
    -> (MExp o, Abs (MExp o)) -> Exp o
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (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)
    a Hiding
    b Bool
    c) ((MExp o, Abs (MExp o)) -> Exp o)
    -> (MExp o, Abs (MExp o)) -> Exp o
    forall a b. (a -> b) -> a -> b
    $ Int
    -> (Int -> Int) -> (MExp o, Abs (MExp o)) -> (MExp o, Abs (MExp o))
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren (MExp o
    it, Abs (MExp o)
    ot)
        e :: Exp o
    e@Sort{}         -> Exp o
    e
        e :: Exp o
    e@AbsurdLambda{} -> Exp o
    e

    instance Renaming (ArgList o) where
      renameOffset :: Int -> (Int -> Int) -> ArgList o -> ArgList o
    renameOffset Int
    j Int -> Int
    ren = \case
        ArgList o
    ALNil           -> ArgList o
    forall o. ArgList o
    ALNil
        ALCons Hiding
    hid MExp o
    a MArgList o
    as -> (MExp o -> MArgList o -> ArgList o)
    -> (MExp o, MArgList o) -> ArgList o
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (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)
    -> (MExp o, MArgList o) -> ArgList o
    forall a b. (a -> b) -> a -> b
    $ Int -> (Int -> Int) -> (MExp o, MArgList o) -> (MExp o, MArgList o)
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren (MExp o
    a, MArgList o
    as)
        ALConPar MArgList o
    as     -> MArgList o -> ArgList o
    forall o. MArgList o -> ArgList o
    ALConPar (Int -> (Int -> Int) -> MArgList o -> MArgList o
    forall t. Renaming t => Int -> (Int -> Int) -> t -> t
    renameOffset Int
    j Int -> Int
    ren MArgList o
    as)
        ALProj{}        -> ArgList o
    forall a. HasCallStack => a
    __IMPOSSIBLE__