    {-# LANGUAGE CPP #-}

    -- | Reconstruct dropped parameters from constructors.  Used by
    --   with-abstraction to avoid ill-typed abstractions (#745). Note that the
    --   term is invalid after parameter reconstruction. Parameters need to be
    --   dropped again before using it.

    module Agda.TypeChecking.ReconstructParameters where

    import Data.Traversable

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Generic

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Pretty

    import Agda.Utils.Size

    import Agda.Utils.Impossible
    #include "undefined.h"

    reconstructParametersInType :: Type -> TCM Type
    reconstructParametersInType a =
      traverse (reconstructParameters (sort $ getSort a)) a

    reconstructParametersInTel :: Telescope -> TCM Telescope
    reconstructParametersInTel EmptyTel = return EmptyTel
    reconstructParametersInTel (ExtendTel a tel) = do
      ar <- reconstructParametersInType (unDom a)
      addContext (absName tel, a) $
        ExtendTel (ar <$ a) <$> traverse reconstructParametersInTel tel

    reconstructParametersInEqView :: EqualityView -> TCM EqualityView
    reconstructParametersInEqView (EqualityType s eq l a u v) =
      EqualityType s eq l <$> traverse (reconstructParameters $ sort s) a
                          <*> traverse (reconstructParameters $ El s $ unArg a) u
                          <*> traverse (reconstructParameters $ El s $ unArg a) v
    reconstructParametersInEqView (OtherType a) = OtherType <$> reconstructParametersInType a

    reconstructParameters :: Type -> Term -> TCM Term
    reconstructParameters a v = do
      reportSDoc "tc.with.reconstruct" 30 $
        sep [ "reconstructing parameters in"
            , nest 2 $ sep [ prettyTCM v <+> ":", nest 2 $ prettyTCM a ] ]
      v <- checkInternal' (defaultAction{ postAction = reconstruct }) v a
      reportSDoc "tc.with.reconstruct" 30 $
        nest 2 $ "-->" <+> prettyTCM v
      return v
      where
        reconstruct a v = do
          case v of
            Con h ci vs -> do
              TelV tel a <- telView a
              let under = size tel  -- under-applied when under > 0
              reportSDoc "tc.with.reconstruct" 50 $
                sep [ "reconstructing"
                    , nest 2 $ sep [ prettyTCM v <+> ":"
                                   , nest 2 $ prettyTCM a ] ]
              case (unEl a) of
                Def d es -> do
                  Just n <- defParameters <$> getConstInfo d
                  let ps = applySubst (strengthenS __IMPOSSIBLE__ under) . take n $ es
                  reportSLn "tc.with.reconstruct" 50 $ show n ++ " parameters"
                  -- TODO: the reconstructed parameters are not reconstructed recursively!
                  return $ Con h ci (ps ++ vs)
                _ -> __IMPOSSIBLE__
            _        -> return v

    dropParameters :: TermLike a => a -> TCM a
    dropParameters = traverseTermM dropPars
      where
        dropPars v =
          case v of
            Con c ci vs -> do
              Constructor{ conData = d } <- theDef <$> getConstInfo (conName c)
              Just n <- defParameters <$> getConstInfo d
              return $ Con c ci $ drop n vs
            _        -> return v