-- | 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 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.Telescope
import Agda.TypeChecking.Pretty

import Agda.Utils.Size

import Agda.Utils.Impossible

reconstructParametersInType :: Type -> TCM Type
reconstructParametersInType :: Type -> TCM Type
reconstructParametersInType Type
a =
  (Term -> TCMT IO Term) -> Type -> TCM Type
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a)) Type
a

reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel Telescope
EmptyTel = Telescope -> TCM Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
forall a. Tele a
EmptyTel
reconstructParametersInTel (ExtendTel Dom Type
a Abs Telescope
tel) = do
  Type
ar <- Type -> TCM Type
reconstructParametersInType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
  (ArgName, Dom Type) -> TCM Telescope -> TCM Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Telescope -> ArgName
forall a. Abs a -> ArgName
absName Abs Telescope
tel, Dom Type
a) (TCM Telescope -> TCM Telescope) -> TCM Telescope -> TCM Telescope
forall a b. (a -> b) -> a -> b
$
    Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
ar Type -> Dom Type -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a) (Abs Telescope -> Telescope)
-> TCMT IO (Abs Telescope) -> TCM Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Telescope -> TCM Telescope)
-> Abs Telescope -> TCMT IO (Abs Telescope)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Telescope -> TCM Telescope
reconstructParametersInTel Abs Telescope
tel

reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView (EqualityType Sort
s QName
eq [Arg Term]
l Arg Term
a Arg Term
u Arg Term
v) =
  Sort
-> QName
-> [Arg Term]
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Sort
s QName
eq [Arg Term]
l (Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> TCMT IO (Arg Term)
-> TCMT IO (Arg Term -> Arg Term -> EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
s) Arg Term
a
                      TCMT IO (Arg Term -> Arg Term -> EqualityView)
-> TCMT IO (Arg Term) -> TCMT IO (Arg Term -> EqualityView)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Arg Term
u
                      TCMT IO (Arg Term -> EqualityView)
-> TCMT IO (Arg Term) -> TCM EqualityView
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Arg Term
v
reconstructParametersInEqView (OtherType Type
a) = Type -> EqualityView
OtherType (Type -> EqualityView) -> TCM Type -> TCM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Type
reconstructParametersInType Type
a

reconstructParameters :: Type -> Term -> TCM Term
reconstructParameters :: Type -> Term -> TCMT IO Term
reconstructParameters Type
a Term
v = do
  ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.with.reconstruct" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"reconstructing parameters in"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
  Term
v <- Action (TCMT IO) -> Term -> Comparison -> Type -> TCMT IO Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' (Action (TCMT IO)
forall (m :: * -> *). Monad m => Action m
defaultAction{ postAction :: Type -> Term -> TCMT IO Term
postAction = Type -> Term -> TCMT IO Term
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m, HasConstInfo m) =>
Type -> Term -> m Term
reconstruct }) Term
v Comparison
CmpLeq Type
a
  ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.with.reconstruct" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"-->" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  where
    reconstruct :: Type -> Term -> m Term
reconstruct Type
a Term
v = do
      case Term
v of
        Con ConHead
h ConInfo
ci Elims
vs -> do
          TelV Telescope
tel Type
a <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
          let under :: VerboseLevel
under = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel  -- under-applied when under > 0
          ArgName -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.with.reconstruct" VerboseLevel
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
            [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"reconstructing"
                , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
                               , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
          case (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) of
            Def QName
d Elims
es -> do
              Just VerboseLevel
n <- Definition -> Maybe VerboseLevel
defParameters (Definition -> Maybe VerboseLevel)
-> m Definition -> m (Maybe VerboseLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
              let ps :: Elims
ps = Substitution' Term -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Empty -> VerboseLevel -> Substitution' Term
forall a. Empty -> VerboseLevel -> Substitution' a
strengthenS Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ VerboseLevel
under) (Elims -> Elims) -> (Elims -> Elims) -> Elims -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Elims -> Elims
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
n (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ Elims
es
              ArgName -> VerboseLevel -> ArgName -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"tc.with.reconstruct" VerboseLevel
50 (ArgName -> m ()) -> ArgName -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ArgName
forall a. Show a => a -> ArgName
show VerboseLevel
n ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" parameters"
              -- TODO: the reconstructed parameters are not reconstructed recursively!
              Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
h ConInfo
ci (Elims
ps Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
vs)
            Term
_ -> m Term
forall a. HasCallStack => a
__IMPOSSIBLE__
        Term
_        -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

dropParameters :: TermLike a => a -> TCM a
dropParameters :: a -> TCM a
dropParameters = (Term -> TCMT IO Term) -> a -> TCM a
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> TCMT IO Term
forall (m :: * -> *). HasConstInfo m => Term -> m Term
dropPars
  where
    dropPars :: Term -> m Term
dropPars Term
v =
      case Term
v of
        Con ConHead
c ConInfo
ci Elims
vs -> do
          Constructor{ conData :: Defn -> QName
conData = QName
d } <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
          Just VerboseLevel
n <- Definition -> Maybe VerboseLevel
defParameters (Definition -> Maybe VerboseLevel)
-> m Definition -> m (Maybe VerboseLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Elims -> Elims
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n Elims
vs
        Term
_        -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v