{-# LANGUAGE Trustworthy #-}
module DeBruijn.RenExtras (
    weakenUsingSize,
) where

import DeBruijn.Ctx
import DeBruijn.Ren
import DeBruijn.Size

import Unsafe.Coerce (unsafeCoerce)

-- | Weaken closed term to arbitrary context.
--
-- Note: this has different requirements than 'sinkSize'.
weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx
weakenUsingSize :: forall (t :: Ctx -> *) (ctx :: Ctx).
Renamable t =>
Size ctx -> t EmptyCtx -> t ctx
weakenUsingSize Size ctx
_ = t EmptyCtx -> t ctx
forall a b. a -> b
unsafeCoerce