{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE GADTs #-}

module Agda.TypeChecking.MetaVars where

import Prelude hiding (null)

import Control.Monad        ( foldM, forM, forM_, liftM2, void )
import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
import Control.Monad.Trans  ( lift )

import Data.Function
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav

import Agda.Interaction.Options

import Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position (getRange, killRange)

import Agda.TypeChecking.Monad
-- import Agda.TypeChecking.Monad.Builtin
-- import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import qualified Agda.TypeChecking.SyntacticEquality as SynEq
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free
import Agda.TypeChecking.Lock
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal
import {-# SOURCE #-} Agda.TypeChecking.Conversion

-- import Agda.TypeChecking.CheckInternal
-- import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (checkInternal)
import Agda.TypeChecking.MetaVars.Occurs

import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( Pretty, prettyShow )
import Agda.Utils.Singleton
import qualified Agda.Utils.Graph.TopSort as Graph
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.WithDefault

import Agda.Utils.Impossible

instance MonadMetaSolver TCM where
  newMeta' :: MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMeta' = MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMetaTCM'
  assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assignV CompareDirection
dir MetaId
x Args
args Term
v CompareAs
t = CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
 MonadDebug m, HasOptions m) =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args) Term
v (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x Args
args Term
v CompareAs
t
  assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTerm' = MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTermTCM'
  etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
etaExpandMeta = [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVar = MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM

  -- Right now we roll back the full state when aborting.
  -- TODO: only roll back the metavariables
  speculateMetas :: TCM () -> TCM KeepMetas -> TCM ()
speculateMetas TCM ()
fallback TCM KeepMetas
m = do
    (KeepMetas
a, TCState
s) <- TCM KeepMetas -> TCM (KeepMetas, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM KeepMetas
m
    case KeepMetas
a of
      KeepMetas
KeepMetas     -> TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
      KeepMetas
RollBackMetas -> TCM ()
fallback

-- | Find position of a value in a list.
--   Used to change metavar argument indices during assignment.
--
--   @reverse@ is necessary because we are directly abstracting over the list.
--
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx :: [a] -> a -> Maybe Int
findIdx [a]
vs a
v = a -> [a] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex a
v ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
vs)

hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta MetaId
x = do
    MetaVariable
m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
    Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe MetaId -> Bool) -> Maybe MetaId -> Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Maybe MetaId
mvTwin MetaVariable
m

-- | Check whether a meta variable is a place holder for a blocked term.
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm MetaId
x = do
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.blocked" Int
12 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"is " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ MetaId -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow MetaId
x ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" a blocked term? "
    MetaInstantiation
i <- MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> TCMT IO MetaVariable -> TCMT IO MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
    let r :: Bool
r = case MetaInstantiation
i of
            BlockedConst{}                 -> Bool
True
            PostponedTypeCheckingProblem{} -> Bool
True
            InstV{}                        -> Bool
False
            Open{}                         -> Bool
False
            OpenInstance{}                 -> Bool
False
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.blocked" Int
12 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$
      if Bool
r then ArgName
"  yes, because " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ MetaInstantiation -> ArgName
forall a. Show a => a -> ArgName
show MetaInstantiation
i else ArgName
"  no"
    Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
r

isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool
isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool
isEtaExpandable [MetaKind]
kinds MetaId
x = do
    MetaInstantiation
i <- MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> TCMT IO MetaVariable -> TCMT IO MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
    Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ case MetaInstantiation
i of
      Open{}                         -> Bool
True
      OpenInstance{}                 -> MetaKind
Records MetaKind -> [MetaKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [MetaKind]
kinds
      InstV{}                        -> Bool
False
      BlockedConst{}                 -> Bool
False
      PostponedTypeCheckingProblem{} -> Bool
False

-- * Performing the assignment

-- | Performing the meta variable assignment.
--
--   The instantiation should not be an 'InstV' and the 'MetaId'
--   should point to something 'Open' or a 'BlockedConst'.
--   Further, the meta variable may not be 'Frozen'.
assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm :: MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm MetaId
x [Arg ArgName]
tel Term
v = do
     -- verify (new) invariants
    m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaId -> [Arg ArgName] -> Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm' MetaId
x [Arg ArgName]
tel Term
v

-- | Skip frozen check.  Used for eta expanding frozen metas.
assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTermTCM' MetaId
x [Arg ArgName]
tel Term
v = do
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"assignTerm" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> 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
      , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg ArgName -> TCM Doc) -> [Arg ArgName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc)
-> (Arg ArgName -> ArgName) -> Arg ArgName -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg ArgName -> ArgName
forall e. Arg e -> e
unArg) [Arg ArgName]
tel)
      ]
     -- verify (new) invariants
    TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    ArgName -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"profile.metas" Int
10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () {-tickMax "max-open-metas" . (fromIntegral . size) =<< getOpenMetas-}
    (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaInstantiation -> MetaStore -> MetaStore
ins MetaId
x (MetaInstantiation -> MetaStore -> MetaStore)
-> MetaInstantiation -> MetaStore -> MetaStore
forall a b. (a -> b) -> a -> b
$ [Arg ArgName] -> Term -> MetaInstantiation
InstV [Arg ArgName]
tel (Term -> MetaInstantiation) -> Term -> MetaInstantiation
forall a b. (a -> b) -> a -> b
$ KillRangeT Term
forall a. KillRange a => KillRangeT a
killRange Term
v
    MetaId -> TCM ()
etaExpandListeners MetaId
x
    MetaId -> TCM ()
wakeupConstraints MetaId
x
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.assign" Int
20 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"completed assignment of " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ MetaId -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow MetaId
x
  where
    ins :: MetaId -> MetaInstantiation -> MetaStore -> MetaStore
ins MetaId
x MetaInstantiation
i = (MetaVariable -> MetaVariable) -> Int -> MetaStore -> MetaStore
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust (\ MetaVariable
mv -> MetaVariable
mv { mvInstantiation :: MetaInstantiation
mvInstantiation = MetaInstantiation
i }) (Int -> MetaStore -> MetaStore) -> Int -> MetaStore -> MetaStore
forall a b. (a -> b) -> a -> b
$ MetaId -> Int
metaId MetaId
x

-- * Creating meta variables.

-- | Create a sort meta that cannot be instantiated with 'Inf' (Setω).
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf = do
  Sort
x <- TCM Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta
  Sort -> TCM ()
hasBiggerSort Sort
x
  Sort -> TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
x

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMeta :: MonadMetaSolver m => m Sort
newSortMeta :: m Sort
newSortMeta =
  m Bool -> m Sort -> m Sort -> m Sort
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (Args -> m Sort
forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
newSortMetaCtx (Args -> m Sort) -> m Args -> m Sort
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs)
  -- else (no universe polymorphism)
  (m Sort -> m Sort) -> m Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ do MetaInfo
i   <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
       let j :: Judgement ()
j = () -> Type -> Judgement ()
forall a. a -> Type -> Judgement a
IsSort () Type
HasCallStack => Type
__DUMMY_TYPE__
       MetaId
x   <- Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement ()
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
Instantiable MetaInfo
i MetaPriority
normalMetaPriority (Int -> Permutation
idP Int
0) Judgement ()
j
       ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.new" Int
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
         TCM Doc
"new sort meta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x
       Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x []

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
newSortMetaCtx :: Args -> m Sort
newSortMetaCtx Args
vs = do
    MetaInfo
i   <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
    Telescope
tel <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    let t :: Type
t = Telescope -> Type -> Type
telePi_ Telescope
tel Type
HasCallStack => Type
__DUMMY_TYPE__
    MetaId
x   <- Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement ()
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
Instantiable MetaInfo
i MetaPriority
normalMetaPriority (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) (Judgement () -> m MetaId) -> Judgement () -> m MetaId
forall a b. (a -> b) -> a -> b
$ () -> Type -> Judgement ()
forall a. a -> Type -> Judgement a
IsSort () Type
t
    ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.new" Int
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"new sort meta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> Elims -> Sort
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs

newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
cmp Sort
s = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type)
-> ((MetaId, Term) -> Term) -> (MetaId, Term) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId, Term) -> Term
forall a b. (a, b) -> b
snd ((MetaId, Term) -> Type) -> TCMT IO (MetaId, Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
cmp (Sort -> Type
sort Sort
s)

newTypeMeta :: Sort -> TCM Type
newTypeMeta :: Sort -> TCM Type
newTypeMeta = Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
CmpLeq

newTypeMeta_ ::  TCM Type
newTypeMeta_ :: TCM Type
newTypeMeta_  = Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
CmpEq (Sort -> TCM Type) -> TCM Sort -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM Sort -> TCM Sort
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Sort -> TCM Sort) -> TCM Sort -> TCM Sort
forall a b. (a -> b) -> a -> b
$ TCM Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta)
-- TODO: (this could be made work with new uni-poly)
-- Andreas, 2011-04-27: If a type meta gets solved, than we do not have to check
-- that it has a sort.  The sort comes from the solution.
-- newTypeMeta_  = newTypeMeta Inf

newLevelMeta :: MonadMetaSolver m => m Level
newLevelMeta :: m Level
newLevelMeta = do
  (MetaId
x, Term
v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpEq (Type -> m (MetaId, Term)) -> m Type -> m (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
  Level -> m Level
forall (m :: * -> *) a. Monad m => a -> m a
return (Level -> m Level) -> Level -> m Level
forall a b. (a -> b) -> a -> b
$ case Term
v of
    Level Level
l    -> Level
l
    Term
_          -> Term -> Level
forall t. t -> Level' t
atomicLevel Term
v

-- | @newInstanceMeta s t cands@ creates a new instance metavariable
--   of type the output type of @t@ with name suggestion @s@.
newInstanceMeta
  :: MonadMetaSolver m
  => MetaNameSuggestion -> Type -> m (MetaId, Term)
newInstanceMeta :: ArgName -> Type -> m (MetaId, Term)
newInstanceMeta ArgName
s Type
t = do
  Args
vs  <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Telescope
ctx <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  ArgName -> Type -> Args -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
ArgName -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx ArgName
s (Telescope -> Type -> Type
telePi_ Telescope
ctx Type
t) Args
vs

newInstanceMetaCtx
  :: MonadMetaSolver m
  => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx :: ArgName -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx ArgName
s Type
t Args
vs = do
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.new" Int
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ TCM Doc
"new instance meta:"
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"|-"
    ]
  -- Andreas, 2017-10-04, issue #2753: no metaOccurs check for instance metas
  MetaInfo
i0 <- RunMetaOccursCheck -> m MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
  let i :: MetaInfo
i = MetaInfo
i0 { miNameSuggestion :: ArgName
miNameSuggestion = ArgName
s }
  TelV Telescope
tel Type
_ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let perm :: Permutation
perm = Int -> Permutation
idP (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel)
  MetaId
x <- MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement ()
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
OpenInstance Frozen
Instantiable MetaInfo
i MetaPriority
normalMetaPriority Permutation
perm (() -> Comparison -> Type -> Judgement ()
forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
CmpLeq Type
t)
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.new" Int
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  let c :: Constraint
c = MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
x Maybe [Candidate]
forall a. Maybe a
Nothing
  -- If we're not already solving instance constraints we should add this
  -- to the awake constraints to make sure we don't forget about it. If we
  -- are solving constraints it will get woken up later (see #2690)
  m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints (Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
alwaysUnblock Constraint
c) (Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addAwakeConstraint Blocker
alwaysUnblock Constraint
c)
  MetaId -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
  (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs)

-- | Create a new value meta with specific dependencies, possibly η-expanding in the process.
newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta :: RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
b ArgName
s Comparison
cmp Type
t = do
  (MetaId
x, Term
v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t
  MetaId -> ArgName -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
x ArgName
s
  (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, Term
v)

-- | Create a new value meta with specific dependencies without η-expanding.
newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' :: RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
b ArgName
s Comparison
cmp Type
t = do
  (MetaId
x, Term
v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t
  MetaId -> ArgName -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
x ArgName
s
  (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, Term
v)

-- | Create a new metavariable, possibly η-expanding in the process.
newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta :: RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t = do
  Args
vs  <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Telescope
tel <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
Instantiable RunMetaOccursCheck
b Comparison
cmp Type
t Telescope
tel (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Args
vs

newValueMetaCtx
  :: MonadMetaSolver m
  => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx :: Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
t Telescope
tel Permutation
perm Args
ctx =
  (Term -> m Term) -> (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) b d a.
Applicative m =>
(b -> m d) -> (a, b) -> m (a, d)
mapSndM Term -> m Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ((MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
t Telescope
tel Permutation
perm Args
ctx

-- | Create a new value meta without η-expanding.
newValueMeta'
  :: MonadMetaSolver m
  => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' :: RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t = do
  Args
vs  <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Telescope
tel <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx' Frozen
Instantiable RunMetaOccursCheck
b Comparison
cmp Type
t Telescope
tel (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Args
vs

newValueMetaCtx'
  :: MonadMetaSolver m
  => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx' :: Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
a Telescope
tel Permutation
perm Args
vs = do
  MetaInfo
i <- RunMetaOccursCheck -> m MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b
  let t :: Type
t     = Telescope -> Type -> Type
telePi_ Telescope
tel Type
a
  MetaId
x <- Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement ()
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
frozen MetaInfo
i MetaPriority
normalMetaPriority Permutation
perm (() -> Comparison -> Type -> Judgement ()
forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
cmp Type
t)
  Modality
modality <- Lens' Modality TCEnv -> m Modality
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Modality TCEnv
eModality
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.new" Int
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> ArgName -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"new meta (" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ IsAbstract -> ArgName
forall a. Show a => a -> ArgName
show (MetaInfo
i MetaInfo -> Lens' IsAbstract MetaInfo -> IsAbstract
forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
Lens' IsAbstract MetaInfo
lensIsAbstract) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"):"
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"|-"
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Modality -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Modality
modality TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  MetaId -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
  -- Andreas, 2012-09-24: for Metas X : Size< u add constraint X+1 <= u
  let u :: Term
u = MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs
  Term -> Telescope -> Type -> m ()
forall (m :: * -> *).
(MonadConstraint m, MonadTCEnv m, ReadTCState m, MonadAddContext m,
 HasOptions m, HasBuiltins m) =>
Term -> Telescope -> Type -> m ()
boundedSizeMetaHook Term
u Telescope
tel Type
a
  (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, Term
u)

newTelMeta :: MonadMetaSolver m => Telescope -> m Args
newTelMeta :: Telescope -> m Args
newTelMeta Telescope
tel = Type -> m Args
forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta (Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
HasCallStack => Type
__DUMMY_TYPE__)

type Condition = Dom Type -> Abs Type -> Bool

trueCondition :: Condition
trueCondition :: Condition
trueCondition Dom Type
_ Abs Type
_ = Bool
True

newArgsMeta :: MonadMetaSolver m => Type -> m Args
newArgsMeta :: Type -> m Args
newArgsMeta = Condition -> Type -> m Args
forall (m :: * -> *).
MonadMetaSolver m =>
Condition -> Type -> m Args
newArgsMeta' Condition
trueCondition

newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args
newArgsMeta' :: Condition -> Type -> m Args
newArgsMeta' Condition
condition Type
t = do
  Args
args <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Telescope
tel  <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' Frozen
Instantiable Condition
condition Type
t Telescope
tel (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Args
args

newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx = Frozen
-> Condition
-> Type
-> Telescope
-> Permutation
-> Args
-> TCM Args
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' Frozen
Instantiable Condition
trueCondition

newArgsMetaCtx'
  :: MonadMetaSolver m
  => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' :: Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' Frozen
frozen Condition
condition (El Sort
s Term
tm) Telescope
tel Permutation
perm Args
ctx = do
  Term
tm <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
tm
  case Term
tm of
    Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
codom | Condition
condition Dom Type
dom Abs Type
codom -> do
      let mod :: Modality
mod  = ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info
          -- Issue #3031: It's not enough to applyModalityToContext, since most (all?)
          -- of the context lives in tel. Don't forget the arguments in ctx.
          tel' :: Telescope
tel' = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$
                 (Dom (ArgName, Type) -> Dom (ArgName, Type)) -> ListTel -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map (Modality
mod Modality -> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$
                 Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
          ctx' :: Args
ctx' = (Arg Term -> Arg Term) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Modality
mod Modality -> Arg Term -> Arg Term
forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) Args
ctx
      (MetaId
m, Term
u) <- ArgInfo -> m (MetaId, Term) -> m (MetaId, Term)
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
                 Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Telescope
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
a Telescope
tel' Permutation
perm Args
ctx'
      -- Jesper, 2021-05-05: When creating a metavariable from a
      -- generalizable variable, we must set the modality at which it
      -- will be generalized.  Don't do this for other metavariables,
      -- as they should keep the defaul modality (see #5363).
      m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((DoGeneralize -> DoGeneralize -> Bool
forall a. Eq a => a -> a -> Bool
== DoGeneralize
YesGeneralizeVar) (DoGeneralize -> Bool) -> m DoGeneralize -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' DoGeneralize TCEnv -> m DoGeneralize
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' DoGeneralize TCEnv
eGeneralizeMetas) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        MetaId -> ArgInfo -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo MetaId
m (ArgInfo -> m ()) -> ArgInfo -> m ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> ArgInfo
forall a. LensHiding a => a -> a
hideOrKeepInstance ArgInfo
info
      MetaId -> ArgName -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
m (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
codom)
      Args
args <- Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' Frozen
frozen Condition
condition (Abs Type
codom Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u) Telescope
tel Permutation
perm Args
ctx
      Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return (Args -> m Args) -> Args -> m Args
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
u Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
: Args
args
    Term
_  -> Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Create a metavariable of record type. This is actually one metavariable
--   for each field.
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta QName
r Args
pars = do
  Args
args <- TCM Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Telescope
tel  <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  Frozen
-> QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx Frozen
Instantiable QName
r Args
pars Telescope
tel (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Args
args

newRecordMetaCtx
  :: Frozen  -- ^ Should the meta be created frozen?
  -> QName   -- ^ Name of record type
  -> Args    -- ^ Parameters of record type.
  -> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx :: Frozen
-> QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx Frozen
frozen QName
r Args
pars Telescope
tel Permutation
perm Args
ctx = do
  Telescope
ftel   <- (Telescope -> Args -> Telescope) -> Args -> Telescope -> Telescope
forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Args
pars (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Telescope
getRecordFieldTypes QName
r
  Args
fields <- Frozen
-> Condition
-> Type
-> Telescope
-> Permutation
-> Args
-> TCM Args
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' Frozen
frozen Condition
trueCondition
              (Telescope -> Type -> Type
telePi_ Telescope
ftel Type
HasCallStack => Type
__DUMMY_TYPE__) Telescope
tel Permutation
perm Args
ctx
  ConHead
con    <- QName -> TCMT IO ConHead
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
r
  Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
fields)

newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark :: InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark InteractionId
ii Comparison
cmp = (Comparison -> Type -> TCMT IO (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark' (RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
RunMetaOccursCheck) InteractionId
ii Comparison
cmp


-- Since we are type-checking some code twice, e.g., record declarations
-- for the sake of the record constructor type and then again for the sake
-- of the record module (issue #434), we may encounter an interaction point
-- for which we already have a meta.  In this case, we want to reuse the meta.
-- Otherwise we get two meta for one interaction point which are not connected,
-- and e.g. Agda might solve one in some way
-- and the user the other in some other way...
--
-- New reference: Andreas, 2021-07-21, issues #5478 and #5463
-- Old reference: Andreas, 2016-07-29, issue 1720-2
-- See also: issue #2257
newQuestionMark'
  :: (Comparison -> Type -> TCM (MetaId, Term))
  -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' :: (Comparison -> Type -> TCMT IO (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark' Comparison -> Type -> TCMT IO (MetaId, Term)
new InteractionId
ii Comparison
cmp Type
t = InteractionId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii TCMT IO (Maybe MetaId)
-> (Maybe MetaId -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

  -- Case: new meta.
  Maybe MetaId
Nothing -> do
    -- Do not run check for recursive occurrence of meta in definitions,
    -- because we want to give the recursive solution interactively (Issue 589)
    (MetaId
x, Term
m) <- Comparison -> Type -> TCMT IO (MetaId, Term)
new Comparison
cmp Type
t
    InteractionId -> MetaId -> TCM ()
forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
x
    (MetaId, Term) -> TCMT IO (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, Term
m)

  -- Case: existing meta.
  Just MetaId
x -> do
    -- Get the context Γ in which the meta was created.
    MetaVar
      { mvInfo :: MetaVariable -> MetaInfo
mvInfo = MetaInfo{ miClosRange :: MetaInfo -> Closure Range
miClosRange = Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv{ envContext :: TCEnv -> Context
envContext = Context
gamma }}}
      , mvPermutation :: MetaVariable -> Permutation
mvPermutation = Permutation
p
      } <- MetaVariable -> Maybe MetaVariable -> MetaVariable
forall a. a -> Maybe a -> a
fromMaybe MetaVariable
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe MetaVariable -> MetaVariable)
-> TCMT IO (Maybe MetaVariable) -> TCMT IO MetaVariable
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
x
    -- Get the current context Δ.
    Context
delta <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
    -- A bit hazardous:
    -- we base our decisions on the names of the context entries.
    -- Ideally, Agda would organize contexts in ancestry trees
    -- with substitutions to move between parent and child.
    let glen :: Int
glen = Context -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
gamma
    let dlen :: Int
dlen = Context -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
delta
    let gxs :: [Name]
gxs  = (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
gamma
    let dxs :: [Name]
dxs  = (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
delta
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"reusing meta"
      , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"creation context:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
      , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"reusage  context:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
      ]

    -- When checking a record declaration (e.g. Σ), creation context Γ
    -- might be of the forms Γ₀,Γ₁ or Γ₀,fst,Γ₁ or Γ₀,fst,snd,Γ₁ whereas
    -- Δ is of the form Γ₀,r,Γ₁,{Δ₂} for record variable r.
    -- So first find the record variable in Δ.
    [Term]
rev_args <- case (Name -> Bool) -> [Name] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex Name -> Bool
nameIsRecordName [Name]
dxs of

      -- Case: no record variable in the context.
      -- Test whether Δ is an extension of Γ.
      Maybe Int
Nothing -> do
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name]
gxs [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` [Name]
dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCM Doc
"expecting meta-creation context"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCM Doc
"to be a suffix of the meta-reuse context"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"impossible" Int
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCM Doc
"expecting meta-creation context"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> ([Name] -> ArgName) -> [Name] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> ArgName
forall a. Show a => a -> ArgName
show) [Name]
gxs
            , TCM Doc
"to be a suffix of the meta-reuse context"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> ([Name] -> ArgName) -> [Name] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> ArgName
forall a. Show a => a -> ArgName
show) [Name]
dxs
            ]
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        -- Apply the meta to |Γ| arguments from Δ.
        [Term] -> TCMT IO [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var [Int
dlen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
glen .. Int
dlen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

      -- Case: record variable in the context.
      Just Int
k -> do
        -- Verify that the contexts relate as expected.
        let g0len :: Int
g0len = [Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
dxs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
        -- Find out the Δ₂ and Γ₁ parts.
        -- However, as they do not share common ancestry, the @nameId@s differ,
        -- so we consider only the original concrete names.
        -- This is a bit risky... blame goes to #434.
        let gys :: [Name]
gys = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameCanonical [Name]
gxs
        let dys :: [Name]
dys = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameCanonical [Name]
dxs
        let (Int
d2len, Int
g1len) = [Name] -> [Name] -> (Int, Int)
forall a. Eq a => [a] -> [a] -> (Int, Int)
findOverlap (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
k [Name]
dys) [Name]
gys
        ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (TCM Doc -> TCM Doc) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2)
          [ TCM Doc
"glen  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
glen
          , TCM Doc
"g0len =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
g0len
          , TCM Doc
"g1len =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
g1len
          , TCM Doc
"d2len =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
d2len
          ]
        -- The Γ₀ part should match.
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (Int
glen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g0len) [Name]
gxs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Name]
dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCM Doc
"expecting meta-creation context (with fields instead of record var)"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCM Doc
"to share ancestry (suffix) with the meta-reuse context (with record var)"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        -- The Γ₁ part should match.
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ( ([Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Name] -> [Name] -> Bool)
-> ([Name] -> [Name]) -> [Name] -> [Name] -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
g1len) [Name]
gys (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop Int
d2len [Name]
dys) ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCM Doc
"expecting meta-creation context (with fields instead of record var)"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCM Doc
"to be an expansion of the meta-reuse context (with record var)"
            , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        let ([Term]
vs1, Term
v : [Term]
vs0) = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
g1len ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var [Int
d2len..Int
dlenInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
        -- We need to expand the record var @v@ into the correct number of fields.
        let numFields :: Int
numFields = Int
glen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g1len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g0len
        if Int
numFields Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then [Term] -> TCMT IO [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ [Term]
vs1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs0 else do
          -- Get the record type.
          let t :: Type
t = (Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Maybe (Dom' Term (Name, Type)) -> (Name, Type))
-> Maybe (Dom' Term (Name, Type))
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom (Dom' Term (Name, Type) -> (Name, Type))
-> (Maybe (Dom' Term (Name, Type)) -> Dom' Term (Name, Type))
-> Maybe (Dom' Term (Name, Type))
-> (Name, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type)
-> Maybe (Dom' Term (Name, Type)) -> Dom' Term (Name, Type)
forall a. a -> Maybe a -> a
fromMaybe Dom' Term (Name, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Dom' Term (Name, Type)) -> Type)
-> Maybe (Dom' Term (Name, Type)) -> Type
forall a b. (a -> b) -> a -> b
$ Context
delta Context -> Int -> Maybe (Dom' Term (Name, Type))
forall a. [a] -> Int -> Maybe a
!!! Int
k
          -- Get the record field names.
          [Dom QName]
fs <- Type -> TCM [Dom QName]
getRecordTypeFields Type
t
          -- Field arguments to the original meta are projections from the record var.
          let vfs :: [Term]
vfs = (Dom QName -> Term) -> [Dom QName] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((\ QName
x -> Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]) (QName -> Term) -> (Dom QName -> QName) -> Dom QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
          -- These are the final args to the original meta:
          [Term] -> TCMT IO [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ [Term]
vs1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term] -> [Term]
forall a. [a] -> [a]
reverse (Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
take Int
numFields [Term]
vfs) [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs0

    -- Use ArgInfo from Γ.
    let args :: Args
args = Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ (Term -> Arg (Name, Type) -> Arg Term)
-> [Term] -> [Arg (Name, Type)] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Term -> Arg (Name, Type) -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [Term]
rev_args ([Arg (Name, Type)] -> Args) -> [Arg (Name, Type)] -> Args
forall a b. (a -> b) -> a -> b
$ (Dom' Term (Name, Type) -> Arg (Name, Type))
-> Context -> [Arg (Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (Name, Type) -> Arg (Name, Type)
forall t a. Dom' t a -> Arg a
argFromDom Context
gamma
    -- Take the permutation into account (see TC.Monad.MetaVars.getMetaContextArgs).
    let vs :: Args
vs = Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Permutation
p) Args
args
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"meta reuse arguments:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs ]
    (MetaId, Term) -> TCMT IO (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs)

-- | Construct a blocked constant if there are constraints.
blockTerm
  :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m)
  => Type -> m Term -> m Term
blockTerm :: Type -> m Term -> m Term
blockTerm Type
t m Term
blocker = do
  (ProblemId
pid, Term
v) <- m Term -> m (ProblemId, Term)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m Term
blocker
  Type -> Term -> ProblemId -> m Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
t Term
v ProblemId
pid

blockTermOnProblem
  :: (MonadMetaSolver m, MonadFresh Nat m)
  => Type -> Term -> ProblemId -> m Term
blockTermOnProblem :: Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
t Term
v ProblemId
pid = do
  -- Andreas, 2012-09-27 do not block on unsolved size constraints
  Bool
solved <- ProblemId -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid
  m Bool -> m Term -> m Term -> m Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
solved m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` ProblemId -> m Bool
forall (m :: * -> *).
(ReadTCState m, HasOptions m, HasBuiltins m) =>
ProblemId -> m Bool
isSizeProblem ProblemId
pid)
      (Term
v Term -> m () -> m Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ArgName -> Int -> ArgName -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.blocked" Int
20 (ArgName
"Not blocking because " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ProblemId -> ArgName
forall a. Show a => a -> ArgName
show ProblemId
pid ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" is " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
                                            if Bool
solved then ArgName
"solved" else ArgName
"a size problem")) (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
    MetaInfo
i   <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
    Elims
es  <- (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> m Args -> m Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    Telescope
tel <- m Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    MetaId
x   <- MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement ()
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' (Term -> MetaInstantiation
BlockedConst (Term -> MetaInstantiation) -> Term -> MetaInstantiation
forall a b. (a -> b) -> a -> b
$ Telescope -> KillRangeT Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Term
v)
                    Frozen
Instantiable
                    MetaInfo
i
                    MetaPriority
lowMetaPriority
                    (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel)
                    (() -> Comparison -> Type -> Judgement ()
forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
CmpLeq (Type -> Judgement ()) -> Type -> Judgement ()
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
telePi_ Telescope
tel Type
t)
                    -- we don't instantiate blocked terms
    m () -> m ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (ProblemId -> Blocker
unblockOnProblem ProblemId
pid) (MetaId -> Constraint
UnBlock MetaId
x)
    ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.blocked" Int
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"blocked" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext
        (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> KillRangeT Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Term
v)
      , TCM Doc
"     by" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Constraints -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Constraints -> TCM Doc) -> TCMT IO Constraints -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProblemId -> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid)
      ]
    Bool
inst <- MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
    if Bool
inst
      then Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es)
      else do
        -- We don't return the blocked term instead create a fresh metavariable
        -- that we compare against the blocked term once it's unblocked. This way
        -- blocked terms can be instantiated before they are unblocked, thus making
        -- constraint solving a bit more robust against instantiation order.
        -- Andreas, 2015-05-22: DontRunMetaOccursCheck to avoid Issue585-17.
        (MetaId
m', Term
v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
t
        ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.blocked" Int
30
          (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$   TCM Doc
"setting twin of"
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m'
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"to be"
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x
        MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m' (\MetaVariable
mv -> MetaVariable
mv { mvTwin :: Maybe MetaId
mvTwin = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x })
        Int
i   <- m Int
forall i (m :: * -> *). MonadFresh i m => m i
fresh
        -- This constraint is woken up when unblocking, so it doesn't need a problem id.
        ProblemConstraint
cmp <- Blocker -> Constraint -> m ProblemConstraint
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint_ (MetaId -> Blocker
unblockOnMeta MetaId
x) (Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpEq (Type -> CompareAs
AsTermsOf Type
t) Term
v (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es))
        ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.constr.add" Int
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"adding constraint" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
cmp
        Listener -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (Int -> ProblemConstraint -> Listener
CheckConstraint Int
i ProblemConstraint
cmp) MetaId
x
        Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

blockTypeOnProblem
  :: (MonadMetaSolver m, MonadFresh Nat m)
  => Type -> ProblemId -> m Type
blockTypeOnProblem :: Type -> ProblemId -> m Type
blockTypeOnProblem (El Sort
s Term
a) ProblemId
pid = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> ProblemId -> m Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem (Sort -> Type
sort Sort
s) Term
a ProblemId
pid

-- | @unblockedTester t@ returns a 'Blocker' for @t@.
--
--   Auxiliary function used when creating a postponed type checking problem.
unblockedTester :: Type -> TCM Blocker
unblockedTester :: Type -> TCM Blocker
unblockedTester Type
t = Type
-> (Blocker -> Type -> TCM Blocker)
-> (NotBlocked -> Type -> TCM Blocker)
-> TCM Blocker
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
b Type
_ -> Blocker -> TCM Blocker
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b) (\ NotBlocked
_ Type
_ -> Blocker -> TCM Blocker
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock)

-- | Create a postponed type checking problem @e : t@ that waits for type @t@
--   to unblock (become instantiated or its constraints resolved).
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ TypeCheckingProblem
p = do
  TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem TypeCheckingProblem
p (Blocker -> TCM Term) -> TCM Blocker -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeCheckingProblem -> TCM Blocker
unblock TypeCheckingProblem
p
  where
    unblock :: TypeCheckingProblem -> TCM Blocker
unblock (CheckExpr Comparison
_ Expr
_ Type
t)         = Type -> TCM Blocker
unblockedTester Type
t
    unblock (CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
_ Type
t Type
_ ArgsCheckState CheckedTarget -> TCM Term
_) = Type -> TCM Blocker
unblockedTester Type
t  -- The type of the head of the application.
    unblock (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
_ Int
_ Term
_ Type
t PrincipalArgTypeMetas
_) = Type -> TCM Blocker
unblockedTester Type
t -- The type of the principal argument
    unblock (CheckLambda Comparison
_ Arg (List1 (WithHiding Name), Maybe Type)
_ Expr
_ Type
t)     = Type -> TCM Blocker
unblockedTester Type
t
    unblock (DoQuoteTerm Comparison
_ Term
_ Type
_)       = TCM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__     -- also quoteTerm problems

-- | Create a postponed type checking problem @e : t@ that waits for conditon
--   @unblock@.  A new meta is created in the current context that has as
--   instantiation the postponed type checking problem.  An 'UnBlock' constraint
--   is added for this meta, which links to this meta.
postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock | Blocker
unblock Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = do
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"impossible" Int
2 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Postponed without blocker:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> TypeCheckingProblem -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TypeCheckingProblem
p
  TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock = do
  MetaInfo
i   <- RunMetaOccursCheck -> TCMT IO MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
  Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  Closure TypeCheckingProblem
cl  <- TypeCheckingProblem -> TCMT IO (Closure TypeCheckingProblem)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure TypeCheckingProblem
p
  let t :: Type
t = TypeCheckingProblem -> Type
problemType TypeCheckingProblem
p
  MetaId
m   <- MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement ()
-> TCM MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' (Closure TypeCheckingProblem -> MetaInstantiation
PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl)
                  Frozen
Instantiable MetaInfo
i MetaPriority
normalMetaPriority (Int -> Permutation
idP (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel))
         (Judgement () -> TCM MetaId) -> Judgement () -> TCM MetaId
forall a b. (a -> b) -> a -> b
$ () -> Comparison -> Type -> Judgement ()
forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
CmpLeq (Type -> Judgement ()) -> Type -> Judgement ()
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
telePi_ Telescope
tel Type
t
  TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.postponed" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"new meta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> Type -> Type
telePi_ Telescope
tel Type
t)
    , TCM Doc
"for postponed typechecking problem" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TypeCheckingProblem -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TypeCheckingProblem
p
    ]

  -- Create the meta that we actually return
  -- Andreas, 2012-03-15
  -- This is an alias to the pptc meta, in order to allow pruning (issue 468)
  -- and instantiation.
  -- Since this meta's solution comes from user code, we do not need
  -- to run the extended occurs check (metaOccurs) to exclude
  -- non-terminating solutions.
  Elims
es  <- (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> TCM Args -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  (MetaId
_, Term
v) <- RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
t
  ProblemConstraint
cmp <- Blocker -> Constraint -> TCMT IO ProblemConstraint
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
Blocker -> Constraint -> m ProblemConstraint
buildProblemConstraint_ (MetaId -> Blocker
unblockOnMeta MetaId
m) (Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpEq (Type -> CompareAs
AsTermsOf Type
t) Term
v (MetaId -> Elims -> Term
MetaV MetaId
m Elims
es))
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.constr.add" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"adding constraint" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
cmp
  Int
i   <- TCM Int -> TCM Int
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Int
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  Listener -> MetaId -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (Int -> ProblemConstraint -> Listener
CheckConstraint Int
i ProblemConstraint
cmp) MetaId
m
  Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock (MetaId -> Constraint
UnBlock MetaId
m)
  Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | Type of the term that is produced by solving the 'TypeCheckingProblem'.
problemType :: TypeCheckingProblem -> Type
problemType :: TypeCheckingProblem -> Type
problemType (CheckExpr Comparison
_ Expr
_ Type
t         ) = Type
t
problemType (CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
_ Type
_ Type
t ArgsCheckState CheckedTarget -> TCM Term
_ ) = Type
t  -- The target type of the application.
problemType (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
t Int
_ Term
_ Type
_ PrincipalArgTypeMetas
_) = Type
t -- The target type of the application
problemType (CheckLambda Comparison
_ Arg (List1 (WithHiding Name), Maybe Type)
_ Expr
_ Type
t     ) = Type
t
problemType (DoQuoteTerm Comparison
_ Term
_ Type
t)        = Type
t

-- | Eta expand metavariables listening on the current meta.
etaExpandListeners :: MetaId -> TCM ()
etaExpandListeners :: MetaId -> TCM ()
etaExpandListeners MetaId
m = do
  [Listener]
ls <- MetaId -> TCMT IO [Listener]
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
m
  MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
clearMetaListeners MetaId
m  -- we don't really have to do this
  (Listener -> TCM ()) -> [Listener] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Listener -> TCM ()
wakeupListener [Listener]
ls

-- | Wake up a meta listener and let it do its thing
wakeupListener :: Listener -> TCM ()
  -- Andreas 2010-10-15: do not expand record mvars, lazyness needed for irrelevance
wakeupListener :: Listener -> TCM ()
wakeupListener (EtaExpand MetaId
x)         = MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
wakeupListener (CheckConstraint Int
_ ProblemConstraint
c) = do
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.blocked" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"waking boxed constraint" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
c
  (Constraints -> Constraints) -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints (ProblemConstraint
cProblemConstraint -> Constraints -> Constraints
forall a. a -> [a] -> [a]
:)
  TCM ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

-- | Do safe eta-expansions for meta (@SingletonRecords,Levels@).
etaExpandMetaSafe :: (MonadMetaSolver m) => MetaId -> m ()
etaExpandMetaSafe :: MetaId -> m ()
etaExpandMetaSafe = [MetaKind] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaKind] -> MetaId -> m ()
etaExpandMeta [MetaKind
SingletonRecords,MetaKind
Levels]

-- | Eta expand a metavariable, if it is of the specified kind.
--   Don't do anything if the metavariable is a blocked term.
etaExpandMetaTCM :: [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM :: [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM [MetaKind]
kinds MetaId
m = TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCM Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (TCEnv -> Bool) -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` [MetaKind] -> MetaId -> TCM Bool
isEtaExpandable [MetaKind]
kinds MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  ArgName -> Int -> ArgName -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.meta.eta" Int
20 (ArgName
"etaExpandMeta " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ MetaId -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let waitFor :: Blocker -> TCM ()
waitFor Blocker
b = do
          ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            TCM Doc
"postponing eta-expansion of meta variable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCM Doc
"which is blocked by" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
b
          (MetaId -> TCM ()) -> [MetaId] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Listener -> MetaId -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (MetaId -> Listener
EtaExpand MetaId
m)) ([MetaId] -> TCM ()) -> [MetaId] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
        dontExpand :: TCM ()
dontExpand = do
          ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            TCM Doc
"we do not expand meta variable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"(requested was expansion of " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [MetaKind] -> ArgName
forall a. Show a => a -> ArgName
show [MetaKind]
kinds ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
")")
    MetaVariable
meta <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
    case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
meta of
      IsSort{} -> TCM ()
dontExpand
      HasType MetaId
_ Comparison
cmp Type
a -> do

        ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"considering eta-expansion at type "
          , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
          , ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
" raw: "
          , Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
          ]

        TelV Telescope
tel Type
b <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
        ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"considering eta-expansion at type"
          , Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
          , ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"under telescope"
          , Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
          ]

        -- Eta expanding metas with a domFinite will just make sure
        -- they go unsolved: conversion will compare them at the
        -- different cases for the domain, so it will not find the
        -- solution for the whole meta.
        if (Dom Type -> Bool) -> [Dom Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Dom Type -> Bool
forall t e. Dom' t e -> Bool
domFinite (Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel) then TCM ()
dontExpand else do

        -- Issue #3774: continue with the right context for b
        Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        -- if the target type @b@ of @m@ is a meta variable @x@ itself
        -- (@NonBlocked (MetaV{})@),
        -- or it is blocked by a meta-variable @x@ (@Blocked@), we cannot
        -- eta expand now, we have to postpone this.  Once @x@ is
        -- instantiated, we can continue eta-expanding m.  This is realized
        -- by adding @m@ to the listeners of @x@.
        Term
-> (Blocker -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
b) (\ Blocker
x Term
_ -> Blocker -> TCM ()
waitFor Blocker
x) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
t -> case Term
t of
          lvl :: Term
lvl@(Def QName
r Elims
es) ->
            TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r) {- then -} (do
              let ps :: Args
ps = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              let expand :: TCM ()
expand = do
                    Term
u <- MetaVariable -> TCM Term -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
meta (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
                      Frozen
-> QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx (MetaVariable -> Frozen
mvFrozen MetaVariable
meta) QName
r Args
ps Telescope
tel (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) (Args -> TCM Term) -> Args -> TCM Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
                    -- Andreas, 2019-03-18, AIM XXIX, issue #3597
                    -- When meta is frozen instantiate it with in-turn frozen metas.
                    TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                          [ TCM Doc
"eta expanding: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" --> "
                          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
                          ]
                      -- Andreas, 2012-03-29: No need for occurrence check etc.
                      -- we directly assign the solution for the meta
                      -- 2012-05-23: We also bypass the check for frozen.
                      TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg ArgName] -> Term -> TCM ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm' MetaId
m (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
tel) Term
u  -- should never produce any constraints
              if MetaKind
Records MetaKind -> [MetaKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaKind]
kinds then
                TCM ()
expand
               else if (MetaKind
SingletonRecords MetaKind -> [MetaKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaKind]
kinds) then
                (Blocker -> TCM ()) -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr (\Blocker
x -> Blocker -> TCM ()
waitFor Blocker
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                 TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> Args -> TCM Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Args -> m Bool
isSingletonRecord QName
r Args
ps) TCM ()
expand TCM ()
dontExpand
                else TCM ()
dontExpand
            ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ {- else -} TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([TCM Bool] -> TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM [ Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ MetaKind
Levels MetaKind -> [MetaKind] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaKind]
kinds
                            , TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType
                            , (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
lvl Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe Term -> Bool) -> TCMT IO (Maybe Term) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
builtinLevel
                            ]) (do
              ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.eta" Int
20 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"Expanding level meta to 0 (type-in-type)"
              -- Andreas, 2012-03-30: No need for occurrence check etc.
              -- we directly assign the solution for the meta
              TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg ArgName] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm MetaId
m (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
tel) (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Level -> Term
Level (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
           ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ {- else -} TCM ()
dontExpand
          Term
_ -> TCM ()
dontExpand

-- | Eta expand blocking metavariables of record type, and reduce the
-- blocked thing.

etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t)
                 => Blocked t -> m (Blocked t)
etaExpandBlocked :: Blocked t -> m (Blocked t)
etaExpandBlocked t :: Blocked t
t@NotBlocked{} = Blocked t -> m (Blocked t)
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked t :: Blocked t
t@(Blocked Blocker
_ t
v) | Just{} <- t -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta t
v = Blocked t -> m (Blocked t)
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked (Blocked Blocker
b t
t)  = do
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.eta" Int
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Eta expanding blockers" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
b
  (MetaId -> m ()) -> [MetaId] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([MetaKind] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaKind] -> MetaId -> m ()
etaExpandMeta [MetaKind
Records]) ([MetaId] -> m ()) -> [MetaId] -> m ()
forall a b. (a -> b) -> a -> b
$ Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
  Blocked t
t <- t -> m (Blocked t)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB t
t
  case Blocked t
t of
    Blocked Blocker
b' t
_ | Blocker
b Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
/= Blocker
b' -> Blocked t -> m (Blocked t)
forall (m :: * -> *) t.
(MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked Blocked t
t
    Blocked t
_                      -> Blocked t -> m (Blocked t)
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t

assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m)
              => CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x Elims
es Term
v m ()
doAssign = do
  m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM ((TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas) m ()
forall b. m b
dontAssign (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ {- else -} do
    ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
10 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ do
      TCM Doc
"term" 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 (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
":" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ CompareDirection -> ArgName
forall a. Show a => a -> ArgName
show CompareDirection
dir) 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
    m () -> m ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints m ()
doAssign m () -> m () -> m ()
forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally` m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

  where dontAssign :: m b
dontAssign = do
          ArgName -> Int -> ArgName -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.assign" Int
10 ArgName
"don't assign metas"
          Blocker -> m b
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- retry again when we are allowed to instantiate metas

-- | Miller pattern unification:
--
--   @assign dir x vs v a@ solves problem @x vs <=(dir) v : a@ for meta @x@
--   if @vs@ are distinct variables (linearity check)
--   and @v@ depends only on these variables
--   and does not contain @x@ itself (occurs check).
--
--   This is the basic story, but we have added some features:
--
--   1. Pruning.
--   2. Benign cases of non-linearity.
--   3. @vs@ may contain record patterns.
--
--   For a reference to some of these extensions, read
--   Andreas Abel and Brigitte Pientka's TLCA 2011 paper.

assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x Args
args Term
v CompareAs
target = Blocker -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker (MetaId -> Blocker
unblockOnMeta MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

  MetaVariable
mvar <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x  -- information associated with meta x
  let t :: Type
t = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar

  -- Andreas, 2011-05-20 TODO!
  -- full normalization  (which also happens during occurs check)
  -- is too expensive! (see Issue 415)
  -- need to do something cheaper, especially if
  -- we are dealing with a Miller pattern that can be solved
  -- immediately!
  -- Ulf, 2011-08-25 DONE!
  -- Just instantiating the top-level meta, which is cheaper. The occurs
  -- check will first try without unfolding any definitions (treating
  -- arguments to definitions as flexible), if that fails it tries again
  -- with full unfolding.
  Term
v <- Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"MetaVars.assign: assigning meta " 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 (MetaId -> Elims -> Term
MetaV MetaId
x []) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCM Doc
" with args " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> (Arg Term -> Term) -> Arg Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Args
args) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCM Doc
" to " 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
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"MetaVars.assign: type of meta: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t

  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
75 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"MetaVars.assign: assigning meta  " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> MetaId -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"  with args  " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Args -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Args
args TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"  to  " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v

  case (Term
v, MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar) of
      (Sort Sort
s, HasType{}) -> Sort -> TCM ()
hasBiggerSort Sort
s
      (Term, Judgement MetaId)
_                   -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  -- Jesper, 2019-09-13: When --no-sort-comparison is enabled,
  -- we equate the sort of the solution with the sort of the
  -- metavariable, in order to solve metavariables in sorts.
  -- Jesper, 2020-04-22: We do this before any of the other steps
  -- because comparing the sorts might lead to some metavariables
  -- being solved, which can help with pruning (see #4615).
  -- Jesper, 2020-08-25: --no-sort-comparison is now the default
  -- behaviour.
  --
  -- Under most circumstances, the conversion checker guarantees that
  -- the solution for the meta has the correct type, so there is no
  -- need to check anything. However, there are two circumstances in
  -- which we do need to check the type of the solution:
  --
  -- 1. When comparing two types they are not guaranteed to have the
  --    same sort.
  --
  -- 2. When --cumulativity is enabled the same can happen when
  --    comparing two terms at a sort type.

  Bool
cumulativity <- PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  let checkSolutionSort :: Comparison -> Sort -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort
s Term
v = do
        Sort
s' <- Term -> TCM Sort
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
sortOf Term
v
        ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCM Doc
"Instantiating sort" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCM Doc
"to sort" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s' TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"of solution" 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
        Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
mvar) MetaId
x (Sort -> Type
sort Sort
s) Term
v) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Comparison -> Sort -> Sort -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s' Sort
s

  case (CompareAs
target , MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar) of
    -- Case 1 (comparing term to meta as types)
    (AsTypes{}   , HasType MetaId
_ Comparison
cmp0 Type
t) -> do
        let cmp :: Comparison
cmp   = if Bool
cumulativity then Comparison
cmp0 else Comparison
CmpEq
            abort :: TCMT IO Empty
abort = Blocker -> TCMT IO Empty
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCMT IO Empty) -> Blocker -> TCMT IO Empty
forall a b. (a -> b) -> a -> b
$ Type -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t -- TODO: make piApplyM' compute unblocker
        Type
t' <- TCMT IO Empty -> Type -> Args -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' TCMT IO Empty
abort Type
t Args
args
        Sort
s <- Type -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort Type
t'
        Comparison -> Sort -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort
s Term
v

    -- Case 2 (comparing term to type-level meta as terms, with --cumulativity)
    (AsTermsOf{} , HasType MetaId
_ Comparison
cmp Type
t)
      | Bool
cumulativity -> do
          let abort :: TCMT IO Empty
abort = Blocker -> TCMT IO Empty
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCMT IO Empty) -> Blocker -> TCMT IO Empty
forall a b. (a -> b) -> a -> b
$ Type -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t
          Type
t' <- TCMT IO Empty -> Type -> Args -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' TCMT IO Empty
abort Type
t Args
args
          TelV Telescope
tel Type
t'' <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t'
          Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCM () -> (Sort -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> m a -> (Sort -> m a) -> m a
ifNotSort Type
t'' (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Sort -> TCM ()) -> TCM ()) -> (Sort -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Sort
s -> do
            let v' :: Term
v' = Int -> KillRangeT Term
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
            Comparison -> Sort -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort
s Term
v'

    (AsTypes{}   , IsSort{}       ) -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (AsTermsOf{} , Judgement MetaId
_              ) -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (AsSizes{}   , Judgement MetaId
_              ) -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- TODO: should we do something similar for sizes?



  -- We don't instantiate frozen mvars
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
== Frozen
Frozen) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.assign" Int
25 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"aborting: meta is frozen!"
    Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock

  -- We never get blocked terms here anymore. TODO: we actually do. why?
  TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCM Bool
isBlockedTerm MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.assign" Int
25 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"aborting: meta is a blocked term!"
    Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (MetaId -> Blocker
unblockOnMeta MetaId
x)

  -- Andreas, 2010-10-15 I want to see whether rhs is blocked
  ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.assign" Int
50 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"MetaVars.assign: I want to see whether rhs is blocked"
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    Blocked Term
v0 <- Term -> TCMT IO (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
    case Blocked Term
v0 of
      Blocked Blocker
m0 Term
_ -> TCM Doc
"r.h.s. blocked on:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
m0
      NotBlocked{} -> TCM Doc
"r.h.s. not blocked"

  -- Turn the assignment problem @_X args >= SizeLt u@ into
  -- @_X args = SizeLt (_Y args@ and constraint
  -- @_Y args >= u@.
  CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt CompareDirection
dir MetaId
x MetaVariable
mvar Type
t Args
args Term
v ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Term
v -> do

    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Telescope
cxt <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"context before projection expansion"
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
cxt
        ]

    -- Normalise and eta contract the arguments to the meta. These are
    -- usually small, and simplifying might let us instantiate more metas.
    -- Also, try to expand away projected vars in meta args.

    Args
-> (Term, CompareAs)
-> (Args -> (Term, CompareAs) -> TCM ())
-> TCM ()
forall a b c.
(Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a,
 PrettyTCM b, TermSubst b) =>
a -> b -> (a -> b -> TCM c) -> TCM c
expandProjectedVars Args
args (Term
v, CompareAs
target) ((Args -> (Term, CompareAs) -> TCM ()) -> TCM ())
-> (Args -> (Term, CompareAs) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Args
args (Term
v, CompareAs
target) -> do

      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        Telescope
cxt <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
        [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"context after projection expansion"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
cxt
          ]

      -- Andreas, 2019-11-16, issue #4159:
      -- We would like to save the work we put into expanding projected variables.
      -- However, the Conversion checker speculatively tries some assignment
      -- in some places (e.g. shortcut) and relies on an exception to be thrown
      -- to try other alternatives next.
      -- If we catch the exception here, this (brittle) mechanism will be broken.
      -- Maybe one possibility would be to rethrow the exception with the
      -- new constraint.  Then, further up, it could be decided whether
      -- to discard the new constraint and do something different,
      -- or add the new constraint when postponing.

      -- BEGIN attempt #4159
      -- let constraint = case v of
      --       -- Sort s -> dirToCmp SortCmp dir (MetaS x $ map Apply args) s
      --       _      -> dirToCmp (\ cmp -> ValueCmp cmp target) dir (MetaV x $ map Apply args) v
      -- reportSDoc "tc.meta.assign.catch" 40 $ sep
      --   [ "assign: catching constraint:"
      --   , prettyTCM constraint
      --   ]
      -- -- reportSDoc "tc.meta.assign.catch" 60 $ sep
      -- --   [ "assign: catching constraint:"
      -- --   , pretty constraint
      -- --   ]
      -- reportSDoc "tc.meta.assign.catch" 80 $ sep
      --   [ "assign: catching constraint (raw):"
      --   , (text . show) constraint
      --   ]
      -- catchConstraint constraint $ do
      -- END attempt #4159


      -- Andreas, 2011-04-21 do the occurs check first
      -- e.g. _1 x (suc x) = suc (_2 x y)
      -- even though the lhs is not a pattern, we can prune the y from _2

      let
                vars :: VarMap
vars        = Args -> VarMap
forall a c t. (IsVarSet a c, Singleton Int c, Free t) => t -> c
freeVars Args
args
                relVL :: [Int]
relVL       = (VarOcc -> Bool) -> VarMap -> [Int]
filterVarMapToList VarOcc -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant  VarMap
vars
                nonstrictVL :: [Int]
nonstrictVL = (VarOcc -> Bool) -> VarMap -> [Int]
filterVarMapToList VarOcc -> Bool
forall a. LensRelevance a => a -> Bool
isNonStrict VarMap
vars
                irrVL :: [Int]
irrVL       = (VarOcc -> Bool) -> VarMap -> [Int]
filterVarMapToList ((Bool -> Bool -> Bool)
-> (VarOcc -> Bool) -> (VarOcc -> Bool) -> VarOcc -> Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) VarOcc -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant VarOcc -> Bool
forall a o. LensFlexRig a o => o -> Bool
isUnguarded) VarMap
vars
            -- Andreas, 2011-10-06 only irrelevant vars that are direct
            -- arguments to the meta, hence, can be abstracted over, may
            -- appear on the rhs.  (test/fail/Issue483b)
            -- Update 2011-03-27: Also irr. vars under record constructors.
            -- Andreas, 2019-06-25:  The reason is that when solving
            -- @X args = v@ we drop all irrelevant arguments that
            -- are not variables (after flattening of record constructors).
            -- (See isVarOrIrrelevant in inverseSubst.)
            -- Thus, the occurs-check needs to ensure only these variables
            -- are mentioned on the rhs.
            -- In the terminology of free variable analysis, the retained
            -- irrelevant variables are exactly the Unguarded ones.
            -- Jesper, 2019-10-15: This is actually wrong since it
            -- will lead to pruning of metas that should not be
            -- pruned, see #4136.

      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          let pr :: Term -> m Doc
pr (Var Int
n []) = ArgName -> m Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Int -> ArgName
forall a. Show a => a -> ArgName
show Int
n)
              pr (Def QName
c []) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c
              pr Term
_          = m Doc
".."
          in [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
               [ TCM Doc
"mvar args:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCM Doc) -> Args -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> TCM Doc
forall (m :: * -> *).
(PureTCM m, MonadInteractionPoints m, MonadFresh NameId m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
Term -> m Doc
pr (Term -> TCM Doc) -> (Arg Term -> Term) -> Arg Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Args
args)
               , TCM Doc
"fvars lhs (rel):" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Int -> TCM Doc) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Int -> ArgName) -> Int -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show) [Int]
relVL)
               , TCM Doc
"fvars lhs (nonstrict):" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Int -> TCM Doc) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Int -> ArgName) -> Int -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show) [Int]
nonstrictVL)
               , TCM Doc
"fvars lhs (irr):" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Int -> TCM Doc) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Int -> ArgName) -> Int -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show) [Int]
irrVL)
               ]

      -- Check that the x doesn't occur in the right hand side.
      -- Prune mvars on rhs such that they can only depend on lhs vars.
      -- Herein, distinguish relevant and irrelevant vars,
      -- since when abstracting irrelevant lhs vars, they may only occur
      -- irrelevantly on rhs.
      -- v <- liftTCM $ occursCheck x (relVL, nonstrictVL, irrVL) v
      Term
v <- TCM Term -> TCM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> VarMap -> Term -> TCM Term
forall a.
(Occurs a, InstantiateFull a, PrettyTCM a) =>
MetaId -> VarMap -> a -> TCM a
occursCheck MetaId
x VarMap
vars Term
v

      ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.meta.assign" Int
15 ArgName
"passed occursCheck"
      ArgName -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"tc.meta.assign" Int
30 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        let n :: Int
n = Term -> Int
forall a. TermSize a => a -> Int
termSize Term
v
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
200) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"size" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Int -> ArgName
forall a. Show a => a -> ArgName
show Int
n)
--              , nest 2 $ "type" <+> prettyTCM t
              , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"term" 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
              ]

      -- Check linearity of @ids@
      -- Andreas, 2010-09-24: Herein, ignore the variables which are not
      -- free in v
      -- Ulf, 2011-09-22: we need to respect irrelevant vars as well, otherwise
      -- we'll build solutions where the irrelevant terms are not valid
      let fvs :: VarSet
fvs = Term -> VarSet
forall t. Free t => t -> VarSet
allFreeVars Term
v
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"fvars rhs:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Int -> TCM Doc) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Int -> ArgName) -> Int -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show) ([Int] -> [TCM Doc]) -> [Int] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Int]
VarSet.toList VarSet
fvs)

      -- Check that the arguments are variables
      Maybe SubstCand
mids <- do
        Either InvertExcept SubstCand
res <- ExceptT InvertExcept TCM SubstCand
-> TCM (Either InvertExcept SubstCand)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT InvertExcept TCM SubstCand
 -> TCM (Either InvertExcept SubstCand))
-> ExceptT InvertExcept TCM SubstCand
-> TCM (Either InvertExcept SubstCand)
forall a b. (a -> b) -> a -> b
$ Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst Args
args
        case Either InvertExcept SubstCand
res of
          -- all args are variables
          Right SubstCand
ids -> do
            ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              TCM Doc
"inverseSubst returns:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (((Int, Term) -> TCM Doc) -> SubstCand -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Term) -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty SubstCand
ids)
            ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              TCM Doc
"inverseSubst returns:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (((Int, Term) -> TCM Doc) -> SubstCand -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Term) -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SubstCand
ids)
            let boundVars :: VarSet
boundVars = [Int] -> VarSet
VarSet.fromList ([Int] -> VarSet) -> [Int] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Int, Term) -> Int) -> SubstCand -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Term) -> Int
forall a b. (a, b) -> a
fst SubstCand
ids
            if VarSet
fvs VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` VarSet
boundVars
              then Maybe SubstCand -> TCMT IO (Maybe SubstCand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SubstCand -> TCMT IO (Maybe SubstCand))
-> Maybe SubstCand -> TCMT IO (Maybe SubstCand)
forall a b. (a -> b) -> a -> b
$ SubstCand -> Maybe SubstCand
forall a. a -> Maybe a
Just SubstCand
ids
              else Maybe SubstCand -> TCMT IO (Maybe SubstCand)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SubstCand
forall a. Maybe a
Nothing
          -- we have proper values as arguments which could be cased on
          -- here, we cannot prune, since offending vars could be eliminated
          Left InvertExcept
CantInvert  -> Maybe SubstCand -> TCMT IO (Maybe SubstCand)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SubstCand
forall a. Maybe a
Nothing
          -- we have non-variables, but these are not eliminateable
          Left InvertExcept
NeutralArg  -> SubstCand -> Maybe SubstCand
forall a. a -> Maybe a
Just (SubstCand -> Maybe SubstCand)
-> TCMT IO SubstCand -> TCMT IO (Maybe SubstCand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Args -> VarSet -> TCMT IO SubstCand
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs
          -- we have a projected variable which could not be eta-expanded away:
          -- same as neutral
          Left ProjVar{}   -> SubstCand -> Maybe SubstCand
forall a. a -> Maybe a
Just (SubstCand -> Maybe SubstCand)
-> TCMT IO SubstCand -> TCMT IO (Maybe SubstCand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Args -> VarSet -> TCMT IO SubstCand
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs

      case Maybe SubstCand
mids of  -- vv Ulf 2014-07-13: actually not needed after all: attemptInertRHSImprovement x args v
        Maybe SubstCand
Nothing  -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v)  -- TODO: more precise
        Just SubstCand
ids -> do
          -- Check linearity
          SubstCand
ids <- do
            Either () SubstCand
res <- ExceptT () TCM SubstCand -> TCM (Either () SubstCand)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () TCM SubstCand -> TCM (Either () SubstCand))
-> ExceptT () TCM SubstCand -> TCM (Either () SubstCand)
forall a b. (a -> b) -> a -> b
$ SubstCand -> ExceptT () TCM SubstCand
checkLinearity {- (`VarSet.member` fvs) -} SubstCand
ids
            case Either () SubstCand
res of
              -- case: linear
              Right SubstCand
ids -> SubstCand -> TCMT IO SubstCand
forall (m :: * -> *) a. Monad m => a -> m a
return SubstCand
ids
              -- case: non-linear variables that could possibly be pruned
              -- If pruning fails we need to unblock on any meta in the rhs, since they might get
              -- rid of the dependency on the non-linear variable. TODO: be more precise (all metas
              -- using non-linear variables need to be solved).
              Left ()   -> Blocker -> TCMT IO SubstCand -> TCMT IO SubstCand
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v) (TCMT IO SubstCand -> TCMT IO SubstCand)
-> TCMT IO SubstCand -> TCMT IO SubstCand
forall a b. (a -> b) -> a -> b
$ MetaId -> Args -> VarSet -> TCMT IO SubstCand
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs

          -- Check ids is time respecting.
          () <- do
            let idvars :: [(Int, VarSet)]
idvars = ((Int, Term) -> (Int, VarSet)) -> SubstCand -> [(Int, VarSet)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> VarSet) -> (Int, Term) -> (Int, VarSet)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd Term -> VarSet
forall t. Free t => t -> VarSet
allFreeVars) SubstCand
ids
            -- earlierThan α v := v "arrives" before α
            let earlierThan :: a -> a -> Bool
earlierThan a
l a
j = a
j a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
l
            TelV Telescope
tel' Type
_ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
telViewUpToPath (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Type
t
            SubstCand -> ((Int, Term) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ SubstCand
ids (((Int, Term) -> TCM ()) -> TCM ())
-> ((Int, Term) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \(Int
i,Term
u) -> do
              Dom' Term (Name, Type)
d <- Int -> TCMT IO (Dom' Term (Name, Type))
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Int -> m (Dom' Term (Name, Type))
lookupBV Int
i
              Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ArgInfo -> Lock
forall a. LensLock a => a -> Lock
getLock (Dom' Term (Name, Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom' Term (Name, Type)
d) Lock -> Lock -> Bool
forall a. Eq a => a -> a -> Bool
== Lock
IsLock) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                let us :: VarSet
us = [VarSet] -> VarSet
forall (f :: * -> *). Foldable f => f VarSet -> VarSet
IntSet.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Int, VarSet) -> VarSet) -> [(Int, VarSet)] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (Int, VarSet) -> VarSet
forall a b. (a, b) -> b
snd ([(Int, VarSet)] -> [VarSet]) -> [(Int, VarSet)] -> [VarSet]
forall a b. (a -> b) -> a -> b
$ ((Int, VarSet) -> Bool) -> [(Int, VarSet)] -> [(Int, VarSet)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
earlierThan Int
i (Int -> Bool) -> ((Int, VarSet) -> Int) -> (Int, VarSet) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, VarSet) -> Int
forall a b. (a, b) -> a
fst) [(Int, VarSet)]
idvars
                -- us Earlier than u
                Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> VarSet -> TCM ()
checkEarlierThan Term
u VarSet
us
                  TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
                     TypeError{} -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (MetaId -> Blocker
unblockOnMeta MetaId
x) -- If the earlier check hard-fails we need to
                     TCErr
err         -> TCErr -> TCM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err                     -- solve this meta in some other way.

          let n :: Int
n = Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args
          TelV Telescope
tel' Type
_ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
telViewUpToPath Int
n Type
t

          -- Check subtyping constraints on the context variables.

          -- Intuition: suppose @_X : (x : A) → B@, then to turn
          --   @
          --     Γ(x : A') ⊢ _X x =?= v : B'@
          --   @
          -- into
          --   @
          --     Γ ⊢ _X =?= λ x → v
          --   @
          -- we need to check that @A <: A'@ (due to contravariance).
          let sigma :: Substitution' Term
sigma = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args
          Bool
hasSubtyping <- WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSubtyping (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hasSubtyping (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ SubstCand -> ((Int, Term) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ SubstCand
ids (((Int, Term) -> TCM ()) -> TCM ())
-> ((Int, Term) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \(Int
i , Term
u) -> do
            -- @u@ is a (projected) variable, so we can infer its type
            Type
a  <- Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
sigma (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (Term -> TCM Type
forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer Term
u)
            Type
a' <- Int -> TCM Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
            Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a' Type
a
              TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
                TypeError{} -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (MetaId -> Blocker
unblockOnMeta MetaId
x) -- If the subtype check hard-fails we need to
                TCErr
err         -> TCErr -> TCM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err                     -- solve this meta in some other way.

          -- Solve.
          Int
m <- TCM Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
          Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' Int
m MetaId
x Type
t Int
n SubstCand
ids Term
v
  where
    -- Try to remove meta arguments from lhs that mention variables not occurring on rhs.
    attemptPruning
      :: MetaId  -- Meta-variable (lhs)
      -> Args    -- Meta arguments (lhs)
      -> FVs     -- Variables occuring on the rhs
      -> TCM a
    attemptPruning :: MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs = do
      -- non-linear lhs: we cannot solve, but prune
      PruneResult
killResult <- MetaId -> Args -> (Int -> Bool) -> TCMT IO PruneResult
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaId -> Args -> (Int -> Bool) -> m PruneResult
prune MetaId
x Args
args ((Int -> Bool) -> TCMT IO PruneResult)
-> (Int -> Bool) -> TCMT IO PruneResult
forall a b. (a -> b) -> a -> b
$ (Int -> VarSet -> Bool
`VarSet.member` VarSet
fvs)
      let success :: Bool
success = PruneResult
killResult PruneResult -> [PruneResult] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PruneResult
PrunedSomething,PruneResult
PrunedEverything]
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"pruning" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> ArgName -> TCM Doc
forall a b. (a -> b) -> a -> b
$ if Bool
success then ArgName
"succeeded" else ArgName
"failed"
      Blocker -> TCM a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (if Bool
success then Blocker
alwaysUnblock  -- If pruning succeeded we want to retry right away
                                   else Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn (Term -> Blocker) -> Term -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)
                                        -- TODO: could be more precise: only unblock on metas
                                        --       applied to offending variables

{- UNUSED
-- | When faced with @_X us == D vs@ for an inert D we can solve this by
--   @_X xs := D _Ys@ with new constraints @_Yi us == vi@. This is important
--   for instance arguments, where knowing the head D might enable progress.
attemptInertRHSImprovement :: MetaId -> Args -> Term -> TCM ()
attemptInertRHSImprovement m args v = do
  reportSDoc "tc.meta.inert" 30 $ vcat
    [ "attempting inert rhs improvement"
    , nest 2 $ sep [ prettyTCM (MetaV m $ map Apply args) <+> "=="
                   , prettyTCM v ] ]
  -- Check that the right-hand side has the form D vs, for some inert constant D.
  -- Returns the type of D and a function to build an application of D.
  (a, mkRHS) <- ensureInert v
  -- Check that all arguments to the meta are neutral and does not have head D.
  -- If there are non-neutral arguments there could be solutions to the meta
  -- that computes over these arguments. If D is an argument to the meta we get
  -- multiple solutions (for instance: _M Nat == Nat can be solved by both
  -- _M := \ x -> x and _M := \ x -> Nat).
  mapM_ (ensureNeutral (mkRHS []) . unArg) args
  tel <- theTel <$> (telView =<< getMetaType m)
  -- When attempting shortcut meta solutions, metas aren't necessarily fully
  -- eta expanded. If this is the case we skip inert improvement.
  when (length args < size tel) $ do
    reportSDoc "tc.meta.inert" 30 $ "not fully applied"
    patternViolation
  -- Solve the meta with _M := \ xs -> D (_Y1 xs) .. (_Yn xs), for fresh metas
  -- _Yi.
  metaArgs <- inTopContext $ addContext tel $ newArgsMeta a
  let varArgs = map Apply $ reverse $ zipWith (\i a -> var i <$ a) [0..] (reverse args)
      sol     = mkRHS metaArgs
      argTel  = map ("x" <$) args
  reportSDoc "tc.meta.inert" 30 $ nest 2 $ vcat
    [ "a       =" <+> prettyTCM a
    , "tel     =" <+> prettyTCM tel
    , "metas   =" <+> prettyList (map prettyTCM metaArgs)
    , "sol     =" <+> prettyTCM sol
    ]
  assignTerm m argTel sol
  patternViolation  -- throwing a pattern violation here lets the constraint
                    -- machinery worry about restarting the comparison.
  where
    ensureInert :: Term -> TCM (Type, Args -> Term)
    ensureInert v = do
      let notInert = do
            reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not inert:" <+> prettyTCM v
            patternViolation
          toArgs elims =
            case allApplyElims elims of
              Nothing -> do
                reportSDoc "tc.meta.inert" 30 $ nest 2 $ "can't do projections from inert"
                patternViolation
              Just args -> return args
      case v of
        Var x elims -> (, Var x . map Apply) <$> typeOfBV x
        Con c ci args  -> notInert -- (, Con c ci) <$> defType <$> getConstInfo (conName c)
        Def f elims -> do
          def <- getConstInfo f
          let good = return (defType def, Def f . map Apply)
          case theDef def of
            Axiom{}       -> good
            Datatype{}    -> good
            Record{}      -> good
            Function{}    -> notInert
            Primitive{}   -> notInert
            Constructor{} -> __IMPOSSIBLE__

        Pi{}       -> notInert -- this is actually inert but improving doesn't buy us anything for Pi
        Lam{}      -> notInert
        Sort{}     -> notInert
        Lit{}      -> notInert
        Level{}    -> notInert
        MetaV{}    -> notInert
        DontCare{} -> notInert

    ensureNeutral :: Term -> Term -> TCM ()
    ensureNeutral rhs v = do
      b <- reduceB v
      let notNeutral v = do
            reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not neutral:" <+> prettyTCM v
            patternViolation
          checkRHS arg
            | arg == rhs = do
              reportSDoc "tc.meta.inert" 30 $ nest 2 $ "argument shares head with RHS:" <+> prettyTCM arg
              patternViolation
            | otherwise  = return ()
      case b of
        Blocked{}      -> notNeutral v
        NotBlocked r v ->                      -- Andrea(s) 2014-12-06 can r be useful?
          case v of
            Var x _    -> checkRHS (Var x [])
            Def f _    -> checkRHS (Def f [])
            Pi{}       -> return ()
            Sort{}     -> return ()
            Level{}    -> return ()
            Lit{}      -> notNeutral v
            DontCare{} -> notNeutral v
            Con{}      -> notNeutral v
            Lam{}      -> notNeutral v
            MetaV{}    -> __IMPOSSIBLE__
-- END UNUSED -}

-- | @assignMeta m x t ids u@ solves @x ids = u@ for meta @x@ of type @t@,
--   where term @u@ lives in a context of length @m@.
--   Precondition: @ids@ is linear.
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta Int
m MetaId
x Type
t [Int]
ids Term
v = do
  let n :: Int
n    = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ids
      cand :: SubstCand
cand = SubstCand -> SubstCand
forall a. Ord a => [a] -> [a]
List.sort (SubstCand -> SubstCand) -> SubstCand -> SubstCand
forall a b. (a -> b) -> a -> b
$ [Int] -> [Term] -> SubstCand
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ids ([Term] -> SubstCand) -> [Term] -> SubstCand
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n
  Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' Int
m MetaId
x Type
t Int
n SubstCand
cand Term
v

-- | @assignMeta' m x t ids u@ solves @x = [ids]u@ for meta @x@ of type @t@,
--   where term @u@ lives in a context of length @m@,
--   and @ids@ is a partial substitution.
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' Int
m MetaId
x Type
t Int
n SubstCand
ids Term
v = do
  -- we are linear, so we can solve!
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"preparing to instantiate: " 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

  -- Rename the variables in v to make it suitable for abstraction over ids.
  -- Basically, if
  --   Γ   = a b c d e
  --   ids = d b e
  -- then
  --   v' = (λ a b c d e. v) _ 1 _ 2 0
  --
  -- Andreas, 2013-10-25 Solve using substitutions:
  -- Convert assocList @ids@ (which is sorted) into substitution,
  -- filling in __IMPOSSIBLE__ for the missing terms, e.g.
  -- [(0,0),(1,2),(3,1)] --> [0, 2, __IMP__, 1, __IMP__]
  -- ALT 1: O(m * size ids), serves as specification
  -- let ivs = [fromMaybe __IMPOSSIBLE__ $ lookup i ids | i <- [0..m-1]]
  -- ALT 2: O(m)
  let assocToList :: Int -> SubstCand -> [Maybe Term]
assocToList Int
i = \case
        SubstCand
_           | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m -> []
        ((Int
j,Term
u) : SubstCand
l) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
u  Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Int -> SubstCand -> [Maybe Term]
assocToList (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SubstCand
l
        SubstCand
l                    -> Maybe Term
forall a. Maybe a
Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Int -> SubstCand -> [Maybe Term]
assocToList (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SubstCand
l
      ivs :: [Maybe Term]
ivs = Int -> SubstCand -> [Maybe Term]
assocToList Int
0 SubstCand
ids
      rho :: Substitution' Term
rho = Impossible
-> [Maybe Term] -> Substitution' Term -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
HasCallStack => Impossible
impossible [Maybe Term]
ivs (Substitution' Term -> Substitution' Term)
-> Substitution' Term -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
n
      v' :: Term
v'  = Substitution' (SubstArg Term) -> KillRangeT Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
rho Term
v

  -- Metas are top-level so we do the assignment at top-level.
  TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    -- Andreas, 2011-04-18 to work with irrelevant parameters
    -- we need to construct tel' from the type of the meta variable
    -- (no longer from ids which may not be the complete variable list
    -- any more)
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"type of meta =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t

    (telv :: TelV Type
telv@(TelV Telescope
tel' Type
a), Boundary
bs) <- Int -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary Int
n Type
t
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel'  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel'
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"#args =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Int -> ArgName
forall a. Show a => a -> ArgName
show Int
n)
    -- Andreas, 2013-09-17 (AIM XVIII): if t does not provide enough
    -- types for the arguments, it might be blocked by a meta;
    -- then we give up. (Issue 903)
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Type
a <- Type -> TCM Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
a
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"not enough pis, but not blocked?" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
      TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__   -- If we get here it was _not_ blocked by a meta!

    -- Perform the assignment (and wake constraints).

    let vsol :: Term
vsol = Telescope -> KillRangeT Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel' Term
v'

    -- Andreas, 2013-10-25 double check solution before assigning
    TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optDoubleCheck  (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      MetaVariable
m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"double checking solution"
      Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (MetaId -> Constraint
CheckMetaInst MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m Term
v' Type
a

    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"solving" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> 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
vsol

    Term
v' <- TelV Type -> Boundary -> Term -> TCM Term
blockOnBoundary TelV Type
telv Boundary
bs Term
v'

    MetaId -> [Arg ArgName] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm MetaId
x (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
tel') Term
v'
  where
    blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term
    blockOnBoundary :: TelV Type -> Boundary -> Term -> TCM Term
blockOnBoundary TelV Type
telv         [] Term
v = Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    blockOnBoundary (TelV Telescope
tel Type
t) Boundary
bs Term
v = Telescope -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
      Type -> TCM Term -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Int m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
        Term
neg <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
        Boundary -> ((Term, (Term, Term)) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Boundary
bs (((Term, (Term, Term)) -> TCM ()) -> TCM ())
-> ((Term, (Term, Term)) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Term
r,(Term
x,Term
y)) -> do
          Term -> Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace (Term
neg Term -> KillRangeT Term
forall t. Apply t => t -> Term -> t
`apply1` Term
r) Type
t Term
x Term
v
          Term -> Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace Term
r  Type
t Term
y Term
v
        Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | Check that the instantiation of the given metavariable fits the
--   type of the metavariable. If the metavariable is not yet
--   instantiated, add a constraint to check the instantiation later.
checkMetaInst :: MetaId -> TCM ()
checkMetaInst :: MetaId -> TCM ()
checkMetaInst MetaId
x = do
  MetaVariable
m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
  let postpone :: TCM ()
postpone = Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
CheckMetaInst MetaId
x
  case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m of
    BlockedConst{} -> TCM ()
postpone
    PostponedTypeCheckingProblem{} -> TCM ()
postpone
    Open{} -> TCM ()
postpone
    OpenInstance{} -> TCM ()
postpone
    InstV [Arg ArgName]
xs Term
v -> do
      let n :: Int
n = [Arg ArgName] -> Int
forall a. Sized a => a -> Int
size [Arg ArgName]
xs
          t :: Type
t = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m
      (telv :: TelV Type
telv@(TelV Telescope
tel Type
a),Boundary
bs) <- Int -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary Int
n Type
t
      Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (MetaId -> Constraint
CheckMetaInst MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m Term
v Type
a

-- | Check that the instantiation of the metavariable with the given
--   term is well-typed.
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m Term
v Type
a = do
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checking solution for meta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x
  case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m of
    HasType{ jComparison :: forall a. Judgement a -> Comparison
jComparison = Comparison
cmp } -> do
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
        MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" : " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> 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
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
        Context
ctx <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"in context: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> PrettyContext -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Context -> PrettyContext
PrettyContext Context
ctx)
      Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x Type
a Term
v) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Term -> Comparison -> Type -> TCM ()
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> Type -> m ()
checkInternal Term
v Comparison
cmp Type
a
    IsSort{}  -> TCM Sort -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCM Sort -> TCM ()) -> TCM Sort -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
        MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> 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 TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" is a sort"
      Sort
s <- Type -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
HasCallStack => Sort
__DUMMY_SORT__ Term
v)
      Call -> TCM Sort -> TCM Sort
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x (Sort -> Type
sort (Sort -> Sort
univSort Sort
s)) (Sort -> Term
Sort Sort
s)) (TCM Sort -> TCM Sort) -> TCM Sort -> TCM Sort
forall a b. (a -> b) -> a -> b
$
        Action TCM -> Sort -> TCM Sort
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort -> m Sort
checkSort Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction Sort
s

-- | Given two types @a@ and @b@ with @a <: b@, check that @a == b@.
checkSubtypeIsEqual :: Type -> Type -> TCM ()
checkSubtypeIsEqual :: Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a Type
b = do
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.subtype" Int
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"checking that subtype" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCM Doc
"of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"is actually equal."
  ((Type
a, Type
b), Bool
equal) <- Type -> Type -> TCMT IO ((Type, Type), Bool)
forall a (m :: * -> *).
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> m ((a, a), Bool)
SynEq.checkSyntacticEquality Type
a Type
b
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
equal (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    Bool
cumulativity <- PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    Term -> TCM Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
b) TCM Term -> (Term -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Sort Sort
sb -> Term -> TCM Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) TCM Term -> (Term -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Sort Sort
sa | Bool
cumulativity -> Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
sa Sort
sb
                             | Bool
otherwise    -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Dummy{} -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: this shouldn't happen but
                             -- currently does because of generalized
                             -- metas being created in a dummy context
        Term
a -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a) -- TODO: can this happen?
      Pi Dom Type
b1 Abs Type
b2 -> Term -> TCM Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) TCM Term -> (Term -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Pi Dom Type
a1 Abs Type
a2
          | Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
a1 Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
b1 -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock -- Can we recover from this?
          | Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Dom Type
a1 Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Dom Type
b1 -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  Dom Type
a1 Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  Dom Type
b1 -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | Bool
otherwise -> do
              Type -> Type -> TCM ()
checkSubtypeIsEqual (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
b1) (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a1)
              Dom Type -> Abs Type -> (Type -> TCM ()) -> TCM ()
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a1 Abs Type
a2 ((Type -> TCM ()) -> TCM ()) -> (Type -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Type
a2' -> Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a2' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b2)
        Dummy{} -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: this shouldn't happen but
                             -- currently does because of generalized
                             -- metas being created in a dummy context
        Term
a -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a)
      -- TODO: check subtyping for Size< types
      Term
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Turn the assignment problem @_X args <= SizeLt u@ into
-- @_X args = SizeLt (_Y args)@ and constraint
-- @_Y args <= u@.
subtypingForSizeLt
  :: CompareDirection -- ^ @dir@
  -> MetaId           -- ^ The meta variable @x@.
  -> MetaVariable     -- ^ Its associated information @mvar <- lookupMeta x@.
  -> Type             -- ^ Its type @t = jMetaType $ mvJudgement mvar@
  -> Args             -- ^ Its arguments.
  -> Term             -- ^ Its to-be-assigned value @v@, such that @x args `dir` v@.
  -> (Term -> TCM ()) -- ^ Continuation taking its possibly assigned value.
  -> TCM ()
subtypingForSizeLt :: CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt CompareDirection
DirEq MetaId
x MetaVariable
mvar Type
t Args
args Term
v Term -> TCM ()
cont = Term -> TCM ()
cont Term
v
subtypingForSizeLt CompareDirection
dir   MetaId
x MetaVariable
mvar Type
t Args
args Term
v Term -> TCM ()
cont = do
  let fallback :: TCM ()
fallback = Term -> TCM ()
cont Term
v
  -- Check whether we have built-ins SIZE and SIZELT
  (Maybe QName
mSize, Maybe QName
mSizeLt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
mSize   TCM ()
fallback ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
qSize   -> do
    Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
mSizeLt TCM ()
fallback ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
qSizeLt -> do
      -- Check whether v is a SIZELT
      Term
v <- Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      case Term
v of
        Def QName
q [Apply (Arg ArgInfo
ai Term
u)] | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
qSizeLt -> do
          -- Clone the meta into a new size meta @y@.
          -- To this end, we swap the target of t for Size.
          TelV Telescope
tel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
          let size :: Type
size = QName -> Type
sizeType_ QName
qSize
              t' :: Type
t'   = Telescope -> Type -> Type
telePi Telescope
tel Type
size
          MetaId
y <- Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement Any
-> TCM MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
Instantiable (MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar) (MetaVariable -> MetaPriority
mvPriority MetaVariable
mvar) (MetaVariable -> Permutation
mvPermutation MetaVariable
mvar)
                       (Any -> Comparison -> Type -> Judgement Any
forall a. a -> Comparison -> Type -> Judgement a
HasType Any
forall a. HasCallStack => a
__IMPOSSIBLE__ Comparison
CmpLeq Type
t')
          -- Note: no eta-expansion of new meta possible/necessary.
          -- Add the size constraint @y args `dir` u@.
          let yArgs :: Term
yArgs = MetaId -> Elims -> Term
MetaV MetaId
y (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args
          Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
y) (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Comparison -> Term -> Term -> Constraint)
-> CompareDirection -> Term -> Term -> Constraint
forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp (Comparison -> CompareAs -> Term -> Term -> Constraint
`ValueCmp` CompareAs
AsSizes) CompareDirection
dir Term
yArgs Term
u
          -- We continue with the new assignment problem, and install
          -- an exception handler, since we created a meta and a constraint,
          -- so we cannot fall back to the original handler.
          let xArgs :: Term
xArgs = MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args
              v' :: Term
v'    = QName -> Elims -> Term
Def QName
qSizeLt [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
yArgs]
              c :: Constraint
c     = (Comparison -> Term -> Term -> Constraint)
-> CompareDirection -> Term -> Term -> Constraint
forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp (Comparison -> CompareAs -> Term -> Term -> Constraint
`ValueCmp` (Type -> CompareAs
AsTermsOf Type
sizeUniv)) CompareDirection
dir Term
xArgs Term
v'
          Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint Constraint
c (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> TCM ()
cont Term
v'
        Term
_ -> TCM ()
fallback

-- | Eta-expand bound variables like @z@ in @X (fst z)@.
expandProjectedVars
  :: ( Pretty a, PrettyTCM a, NoProjectedVar a
     -- , Normalise a, TermLike a, Subst Term a
     , ReduceAndEtaContract a
     , PrettyTCM b, TermSubst b
     )
  => a  -- ^ Meta variable arguments.
  -> b  -- ^ Right hand side.
  -> (a -> b -> TCM c)
  -> TCM c
expandProjectedVars :: a -> b -> (a -> b -> TCM c) -> TCM c
expandProjectedVars a
args b
v a -> b -> TCM c
ret = (a, b) -> TCM c
loop (a
args, b
v) where
  loop :: (a, b) -> TCM c
loop (a
args, b
v) = do
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"meta args: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
args
    a
args <- TCM a -> TCM a
forall a. TCM a -> TCM a
callByName (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ a -> TCM a
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract a
args
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
45 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"norm args: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
args
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
85 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"norm args: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
args
    let done :: TCM c
done = a -> b -> TCM c
ret a
args b
v
    case a -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar a
args of
      Right ()              -> do
        ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCM Doc
"no projected var found in args: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
args
        TCM c
done
      Left (ProjectedVar Int
i [(ProjOrigin, QName)]
_) -> Int -> (a, b) -> TCM c -> ((a, b) -> TCM c) -> TCM c
forall a c.
(PrettyTCM a, TermSubst a) =>
Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Int
i (a
args, b
v) TCM c
done (a, b) -> TCM c
loop

-- | Eta-expand a de Bruijn index of record type in context and passed term(s).
etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar :: Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Int
i a
v TCM c
fail a -> TCM c
succeed = do
  ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"trying to expand projected variable" 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 (Int -> Term
var Int
i)
  TCMT IO (Maybe (Telescope, Substitution' Term, Substitution' Term))
-> TCM c
-> ((Telescope, Substitution' Term, Substitution' Term) -> TCM c)
-> TCM c
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Int
-> TCMT
     IO (Maybe (Telescope, Substitution' Term, Substitution' Term))
etaExpandBoundVar Int
i) TCM c
fail (((Telescope, Substitution' Term, Substitution' Term) -> TCM c)
 -> TCM c)
-> ((Telescope, Substitution' Term, Substitution' Term) -> TCM c)
-> TCM c
forall a b. (a -> b) -> a -> b
$ \ (Telescope
delta, Substitution' Term
sigma, Substitution' Term
tau) -> do
    ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign.proj" Int
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"eta-expanding var " 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 (Int -> Term
var Int
i) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      TCM Doc
" in terms " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
    TCM c -> TCM c
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext (TCM c -> TCM c) -> TCM c -> TCM c
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM c -> TCM c
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (TCM c -> TCM c) -> TCM c -> TCM c
forall a b. (a -> b) -> a -> b
$
      a -> TCM c
succeed (a -> TCM c) -> a -> TCM c
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg a)
tau a
v

-- | Check whether one of the meta args is a projected var.
class NoProjectedVar a where
  noProjectedVar :: a -> Either ProjectedVar ()

  default noProjectedVar
    :: (NoProjectedVar b, Foldable t, t b ~ a)
    => a -> Either ProjectedVar ()
  noProjectedVar = (b -> Either ProjectedVar ()) -> t b -> Either ProjectedVar ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ b -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar

instance NoProjectedVar a => NoProjectedVar (Arg a)
instance NoProjectedVar a => NoProjectedVar [a]

instance NoProjectedVar Term where
  noProjectedVar :: Term -> Either ProjectedVar ()
noProjectedVar = \case
      Var Int
i Elims
es
        | qs :: [(ProjOrigin, QName)]
qs@((ProjOrigin, QName)
_:[(ProjOrigin, QName)]
_) <- (Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName))
-> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName)
forall a. a -> a
id ([Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)])
-> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Maybe (ProjOrigin, QName))
-> Elims -> [Maybe (ProjOrigin, QName)]
forall a b. (a -> b) -> [a] -> [b]
map Elim' Term -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es
        -> ProjectedVar -> Either ProjectedVar ()
forall a b. a -> Either a b
Left (ProjectedVar -> Either ProjectedVar ())
-> ProjectedVar -> Either ProjectedVar ()
forall a b. (a -> b) -> a -> b
$ Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
i [(ProjOrigin, QName)]
qs
      -- Andreas, 2015-09-12 Issue #1316:
      -- Also look in inductive record constructors
      Con (ConHead QName
_ IsRecord{} Induction
Inductive [Arg QName]
_) ConInfo
_ Elims
es
        | Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -> Args -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar Args
vs
      Term
_ -> () -> Either ProjectedVar ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Normalize just far enough to be able to eta-contract maximally.
class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where
  reduceAndEtaContract :: a -> TCM a

  default reduceAndEtaContract
    :: (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a)
    => a -> TCM a
  reduceAndEtaContract = (b -> TCMT IO b) -> f b -> TCMT IO (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM b -> TCMT IO b
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract

instance ReduceAndEtaContract a => ReduceAndEtaContract [a]
instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)

instance ReduceAndEtaContract Term where
  reduceAndEtaContract :: Term -> TCM Term
reduceAndEtaContract Term
u = do
    Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u TCM Term -> (Term -> TCM Term) -> TCM Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      -- In case of lambda or record constructor, it makes sense to
      -- reduce further.
      Lam ArgInfo
ai (Abs ArgName
x Term
b) -> ArgInfo -> ArgName -> Term -> TCM Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ArgInfo -> ArgName -> Term -> m Term
etaLam ArgInfo
ai ArgName
x (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Term
b
      Con ConHead
c ConInfo
ci Elims
es -> ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> TCM Term)
-> TCM Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> m Term)
-> m Term
etaCon ConHead
c ConInfo
ci Elims
es ((QName -> ConHead -> ConInfo -> Args -> TCM Term) -> TCM Term)
-> (QName -> ConHead -> ConInfo -> Args -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ QName
r ConHead
c ConInfo
ci Args
args -> do
        Args
args <- Args -> TCM Args
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Args
args
        QName -> ConHead -> ConInfo -> Args -> TCM Term
forall (m :: * -> *).
HasConstInfo m =>
QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord QName
r ConHead
c ConInfo
ci Args
args
      Term
v -> Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

{- UNUSED, BUT KEEP!
-- Wrong attempt at expanding bound variables.
-- The following code curries meta instead.

-- | @etaExpandProjectedVar mvar x t n qs@
--
--   @mvar@ is the meta var info.
--   @x@ is the meta variable we are trying to solve for.
--   @t@ is its type.
--   @n@ is the number of the meta arg we want to curry (starting at 0).
--   @qs@ is the projection path along which we curry.
--
etaExpandProjectedVar :: MetaVariable -> MetaId -> Type -> Int -> [QName] -> TCM a
etaExpandProjectedVar mvar x t n qs = inTopContext $ do
  (_, uncurry, t') <- curryAt t n
  let TelV tel a = telView' t'
      perm       = idP (size tel)
  y <- newMeta (mvInfo mvar) (mvPriority mvar) perm (HasType __IMPOSSIBLE__ t')
  assignTerm' x (uncurry $ MetaV y [])
  patternViolation
-}

{-
  -- first, strip the leading n domains (which remain unchanged)
  TelV gamma core <- telViewUpTo n t
  case unEl core of
    -- There should be at least one domain left
    Pi (Dom ai a) b -> do
      -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
      -- For now, we only eta-expand once.
      -- This might trigger another call to @etaExpandProjectedVar@ later.
      -- A more efficient version does all the eta-expansions at once here.
      (r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a
      unless (recEtaEquality def) __IMPOSSIBLE__
      let tel = recTel def `apply` pars
          m   = size tel
          v   = Con (recConHead def) $ map var $ downFrom m
          b'  = raise m b `absApp` v
          fs  = recFields def
          vs  = zipWith (\ f i -> Var i [Proj f]) fs $ downFrom m
          -- v = c (n-1) ... 1 0
      (tel, u) <- etaExpandAtRecordType a $ var 0
      -- TODO: compose argInfo ai with tel.
      -- Substitute into @b@.
      -- Abstract over @tel@.
      -- Abstract over @gamma@.
      -- Create new meta.
      -- Solve old meta, using substitution.
      patternViolation
    _ -> __IMPOSSIBLE__
-}

type FVs = VarSet
type SubstCand = [(Int,Term)] -- ^ a possibly non-deterministic substitution

-- | Turn non-det substitution into proper substitution, if possible.
--   Otherwise, raise the error.
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity SubstCand
ids0 = do
  let ids :: SubstCand
ids = ((Int, Term) -> (Int, Term) -> Ordering) -> SubstCand -> SubstCand
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, Term) -> Int) -> (Int, Term) -> (Int, Term) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, Term) -> Int
forall a b. (a, b) -> a
fst) SubstCand
ids0  -- see issue 920
  let grps :: [SubstCand]
grps = ((Int, Term) -> Int) -> SubstCand -> [SubstCand]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupOn (Int, Term) -> Int
forall a b. (a, b) -> a
fst SubstCand
ids
  [SubstCand] -> SubstCand
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([SubstCand] -> SubstCand)
-> ExceptT () TCM [SubstCand] -> ExceptT () TCM SubstCand
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubstCand -> ExceptT () TCM SubstCand)
-> [SubstCand] -> ExceptT () TCM [SubstCand]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubstCand -> ExceptT () TCM SubstCand
makeLinear [SubstCand]
grps
  where
    -- Non-determinism can be healed if type is singleton. [Issue 593]
    -- (Same as for irrelevance.)
    makeLinear :: SubstCand -> ExceptT () TCM SubstCand
    makeLinear :: SubstCand -> ExceptT () TCM SubstCand
makeLinear []            = ExceptT () TCM SubstCand
forall a. HasCallStack => a
__IMPOSSIBLE__
    makeLinear grp :: SubstCand
grp@[(Int, Term)
_]       = SubstCand -> ExceptT () TCM SubstCand
forall (m :: * -> *) a. Monad m => a -> m a
return SubstCand
grp
    makeLinear (p :: (Int, Term)
p@(Int
i,Term
t) : SubstCand
_) =
      ExceptT () TCM Bool
-> ExceptT () TCM SubstCand
-> ExceptT () TCM SubstCand
-> ExceptT () TCM SubstCand
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either Blocker Bool -> Bool)
-> ExceptT () TCM (Either Blocker Bool) -> ExceptT () TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do TCM (Either Blocker Bool) -> ExceptT () TCM (Either Blocker Bool)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Either Blocker Bool) -> ExceptT () TCM (Either Blocker Bool))
-> (Type -> TCM (Either Blocker Bool))
-> Type
-> ExceptT () TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockT TCM Bool -> TCM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT TCM Bool -> TCM (Either Blocker Bool))
-> (Type -> BlockT TCM Bool) -> Type -> TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> BlockT TCM Bool
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance (Type -> ExceptT () TCM (Either Blocker Bool))
-> ExceptT () TCM Type -> ExceptT () TCM (Either Blocker Bool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> ExceptT () TCM Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i)
        (SubstCand -> ExceptT () TCM SubstCand
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, Term)
p])
        (() -> ExceptT () TCM SubstCand
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ())

-- Intermediate result in the following function
type Res = [(Arg Nat, Term)]

-- | Exceptions raised when substitution cannot be inverted.
data InvertExcept
  = CantInvert                -- ^ Cannot recover.
  | NeutralArg                -- ^ A potentially neutral arg: can't invert, but can try pruning.
  | ProjVar ProjectedVar      -- ^ Try to eta-expand var to remove projs.

-- | Check that arguments @args@ to a metavar are in pattern fragment.
--   Assumes all arguments already in whnf and eta-reduced.
--   Parameters are represented as @Var@s so @checkArgs@ really
--   checks that all args are @Var@s and returns the "substitution"
--   to be applied to the rhs of the equation to solve.
--   (If @args@ is considered a substitution, its inverse is returned.)
--
--   The returned list might not be ordered.
--   Linearity, i.e., whether the substitution is deterministic,
--   has to be checked separately.
--
inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst Args
args = ((Arg Int, Term) -> (Int, Term)) -> [(Arg Int, Term)] -> SubstCand
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Int -> Int) -> (Arg Int, Term) -> (Int, Term)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Arg Int -> Int
forall e. Arg e -> e
unArg) ([(Arg Int, Term)] -> SubstCand)
-> ExceptT InvertExcept TCM [(Arg Int, Term)]
-> ExceptT InvertExcept TCM SubstCand
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Arg Term, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
loop (Args -> [Term] -> [(Arg Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip Args
args [Term]
terms)
  where
    loop :: [(Arg Term, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
loop  = ([(Arg Int, Term)]
 -> (Arg Term, Term) -> ExceptT InvertExcept TCM [(Arg Int, Term)])
-> [(Arg Int, Term)]
-> [(Arg Term, Term)]
-> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(Arg Int, Term)]
-> (Arg Term, Term) -> ExceptT InvertExcept TCM [(Arg Int, Term)]
isVarOrIrrelevant []
    terms :: [Term]
terms = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Args -> Int
forall a. Sized a => a -> Int
size Args
args))
    failure :: ExceptT InvertExcept TCM [(Arg Int, Term)]
failure = do
      TCM () -> ExceptT InvertExcept TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ExceptT InvertExcept TCM ())
-> TCM () -> ExceptT InvertExcept TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.meta.assign" Int
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"not all arguments are variables: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
args
        , TCM Doc
"  aborting assignment" ]
      InvertExcept -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvertExcept
CantInvert
    neutralArg :: ExceptT InvertExcept TCM a
neutralArg = InvertExcept -> ExceptT InvertExcept TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvertExcept
NeutralArg

    isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res
    isVarOrIrrelevant :: [(Arg Int, Term)]
-> (Arg Term, Term) -> ExceptT InvertExcept TCM [(Arg Int, Term)]
isVarOrIrrelevant [(Arg Int, Term)]
vars (Arg ArgInfo
info Term
v, Term
t) = do
      let irr :: Bool
irr | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = Bool
True
              | DontCare{} <- Term
v   = Bool
True
              | Bool
otherwise         = Bool
False
      case KillRangeT Term
stripDontCare Term
v of
        -- i := x
        Var Int
i [] -> [(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)])
-> [(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Int -> Arg Int
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Int
i, Term
t) (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
`cons` [(Arg Int, Term)]
vars

        -- π i := x  try to eta-expand projection π away!
        Var Int
i Elims
es | Just [(ProjOrigin, QName)]
qs <- (Elim' Term -> Maybe (ProjOrigin, QName))
-> Elims -> Maybe [(ProjOrigin, QName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim' Term -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es ->
          InvertExcept -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InvertExcept -> ExceptT InvertExcept TCM [(Arg Int, Term)])
-> InvertExcept -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ ProjectedVar -> InvertExcept
ProjVar (ProjectedVar -> InvertExcept) -> ProjectedVar -> InvertExcept
forall a b. (a -> b) -> a -> b
$ Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
i [(ProjOrigin, QName)]
qs

        -- (i, j) := x  becomes  [i := fst x, j := snd x]
        -- Andreas, 2013-09-17 but only if constructor is fully applied
        Con ConHead
c ConInfo
ci Elims
es -> do
          let fallback :: ExceptT InvertExcept TCM [(Arg Int, Term)]
fallback
               | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = [(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Int, Term)]
vars
               | Bool
otherwise                              = ExceptT InvertExcept TCM [(Arg Int, Term)]
failure
          Bool
irrProj <- PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool)
-> ExceptT InvertExcept TCM PragmaOptions
-> ExceptT InvertExcept TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT InvertExcept TCM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
          TCM (Maybe (QName, Defn))
-> ExceptT InvertExcept TCM (Maybe (QName, Defn))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QName -> TCM (Maybe (QName, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor (QName -> TCM (Maybe (QName, Defn)))
-> QName -> TCM (Maybe (QName, Defn))
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) ExceptT InvertExcept TCM (Maybe (QName, Defn))
-> (Maybe (QName, Defn)
    -> ExceptT InvertExcept TCM [(Arg Int, Term)])
-> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just (QName
_, r :: Defn
r@Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs })
              | HasEta' PatternOrCopattern
YesEta <- Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
r  -- Andreas, 2019-11-10, issue #4185: only for eta-records
              , [Dom QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom QName]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Elims -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es
              , ArgInfo -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 ArgInfo
info Bool -> Bool -> Bool
|| (Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Dom QName -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity [Dom QName]
fs     -- Andreas, 2019-11-12/17, issue #4168b
              , Bool
irrProj Bool -> Bool -> Bool
|| (Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Dom QName -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant [Dom QName]
fs -> do
                let aux :: Arg Term -> Dom QName -> (Arg Term, Term)
aux (Arg ArgInfo
_ Term
v) Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = QName
f} = (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v,) (Term -> (Arg Term, Term)) -> Term -> (Arg Term, Term)
forall a b. (a -> b) -> a -> b
$ Term
t Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f] where
                     ai :: ArgInfo
ai = ArgInfo :: Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo
                       { argInfoHiding :: Hiding
argInfoHiding   = Hiding -> Hiding -> Hiding
forall a. Ord a => a -> a -> a
min (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info')
                       , argInfoModality :: Modality
argInfoModality = Modality :: Relevance -> Quantity -> Cohesion -> Modality
Modality
                         { modRelevance :: Relevance
modRelevance  = Relevance -> Relevance -> Relevance
forall a. Ord a => a -> a -> a
max (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info')
                         , modQuantity :: Quantity
modQuantity   = Quantity -> Quantity -> Quantity
forall a. Ord a => a -> a -> a
max (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  ArgInfo
info) (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  ArgInfo
info')
                         , modCohesion :: Cohesion
modCohesion   = Cohesion -> Cohesion -> Cohesion
forall a. Ord a => a -> a -> a
max (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  ArgInfo
info) (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  ArgInfo
info')
                         }
                       , argInfoOrigin :: Origin
argInfoOrigin   = Origin -> Origin -> Origin
forall a. Ord a => a -> a -> a
min (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info) (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info')
                       , argInfoFreeVariables :: FreeVariables
argInfoFreeVariables = FreeVariables
unknownFreeVariables
                       , argInfoAnnotation :: Annotation
argInfoAnnotation    = ArgInfo -> Annotation
argInfoAnnotation ArgInfo
info'
                       }
                    vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                [(Arg Int, Term)]
res <- [(Arg Term, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
loop ([(Arg Term, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)])
-> [(Arg Term, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Dom QName -> (Arg Term, Term))
-> Args -> [Dom QName] -> [(Arg Term, Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Dom QName -> (Arg Term, Term)
aux Args
vs [Dom QName]
fs
                [(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)])
-> [(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ [(Arg Int, Term)]
res [(Arg Int, Term)] -> [(Arg Int, Term)] -> [(Arg Int, Term)]
`append` [(Arg Int, Term)]
vars
              | Bool
otherwise -> ExceptT InvertExcept TCM [(Arg Int, Term)]
fallback
            Maybe (QName, Defn)
_ -> ExceptT InvertExcept TCM [(Arg Int, Term)]
fallback

        -- An irrelevant argument which is not an irrefutable pattern is dropped
        Term
_ | Bool
irr -> [(Arg Int, Term)] -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Int, Term)]
vars

        -- Distinguish args that can be eliminated (Con,Lit,Lam,unsure) ==> failure
        -- from those that can only put somewhere as a whole ==> neutralArg
        Var{}      -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a. ExceptT InvertExcept TCM a
neutralArg
        Def{}      -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a. ExceptT InvertExcept TCM a
neutralArg  -- Note that this Def{} is in normal form and might be prunable.
        Lam{}      -> ExceptT InvertExcept TCM [(Arg Int, Term)]
failure
        Lit{}      -> ExceptT InvertExcept TCM [(Arg Int, Term)]
failure
        MetaV{}    -> ExceptT InvertExcept TCM [(Arg Int, Term)]
failure
        Pi{}       -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a. ExceptT InvertExcept TCM a
neutralArg
        Sort{}     -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a. ExceptT InvertExcept TCM a
neutralArg
        Level{}    -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a. ExceptT InvertExcept TCM a
neutralArg
        DontCare{} -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Ruled out by stripDontCare
        Dummy ArgName
s Elims
_  -> ArgName -> ExceptT InvertExcept TCM [(Arg Int, Term)]
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s

    -- managing an assoc list where duplicate indizes cannot be irrelevant vars
    append :: Res -> Res -> Res
    append :: [(Arg Int, Term)] -> [(Arg Int, Term)] -> [(Arg Int, Term)]
append [(Arg Int, Term)]
res [(Arg Int, Term)]
vars = ((Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)])
-> [(Arg Int, Term)] -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
cons [(Arg Int, Term)]
vars [(Arg Int, Term)]
res

    -- adding an irrelevant entry only if not present
    cons :: (Arg Nat, Term) -> Res -> Res
    cons :: (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
cons a :: (Arg Int, Term)
a@(Arg ArgInfo
ai Int
i, Term
t) [(Arg Int, Term)]
vars
      | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
ai = Bool
-> ([(Arg Int, Term)] -> [(Arg Int, Term)])
-> [(Arg Int, Term)]
-> [(Arg Int, Term)]
forall a. Bool -> (a -> a) -> a -> a
applyUnless (((Arg Int, Term) -> Bool) -> [(Arg Int, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int
iInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool)
-> ((Arg Int, Term) -> Int) -> (Arg Int, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Int -> Int
forall e. Arg e -> e
unArg (Arg Int -> Int)
-> ((Arg Int, Term) -> Arg Int) -> (Arg Int, Term) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Int, Term) -> Arg Int
forall a b. (a, b) -> a
fst) [(Arg Int, Term)]
vars) ((Arg Int, Term)
a (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a. a -> [a] -> [a]
:) [(Arg Int, Term)]
vars
      | Bool
otherwise       = (Arg Int, Term)
a (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a. a -> [a] -> [a]
:  -- adding a relevant entry
          -- filter out duplicate irrelevants
          ((Arg Int, Term) -> Bool) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Arg Int, Term) -> Bool) -> (Arg Int, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ a :: (Arg Int, Term)
a@(Arg ArgInfo
info Int
j, Term
t) -> ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j)) [(Arg Int, Term)]
vars


-- | Turn open metas into postulates.
--
--   Preconditions:
--
--   1. We are 'inTopContext'.
--
--   2. 'envCurrentModule' is set to the top-level module.
--
openMetasToPostulates :: TCM ()
openMetasToPostulates :: TCM ()
openMetasToPostulates = do
  ModuleName
m <- (TCEnv -> ModuleName) -> TCMT IO ModuleName
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ModuleName
envCurrentModule

  -- Go through all open metas.
  [(Int, MetaVariable)]
ms <- MetaStore -> [(Int, MetaVariable)]
forall a. IntMap a -> [(Int, a)]
IntMap.assocs (MetaStore -> [(Int, MetaVariable)])
-> TCMT IO MetaStore -> TCMT IO [(Int, MetaVariable)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' MetaStore TCState -> TCMT IO MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
  [(Int, MetaVariable)] -> ((Int, MetaVariable) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, MetaVariable)]
ms (((Int, MetaVariable) -> TCM ()) -> TCM ())
-> ((Int, MetaVariable) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Int
x, MetaVariable
mv) -> do
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool) -> MetaInstantiation -> Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      let t :: Type
t = Type -> Type
dummyTypeToOmega (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv

      -- Create a name for the new postulate.
      let r :: Range
r = Closure Range -> Range
forall a. Closure a -> a
clValue (Closure Range -> Range) -> Closure Range -> Range
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv
      -- s <- render <$> prettyTCM x -- Using _ is a bad idea, as it prints as prefix op
      let s :: ArgName
s = ArgName
"unsolved#meta." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Int -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow Int
x
      Name
n <- Range -> ArgName -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> ArgName -> m Name
freshName Range
r ArgName
s
      let q :: QName
q = ModuleName -> Name -> QName
A.QName ModuleName
m Name
n

      -- Debug.
      ArgName -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"meta.postulate" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"Turning " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ if MetaVariable -> Bool
isSortMeta_ MetaVariable
mv then ArgName
"sort" else ArgName
"value" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" meta ")
            TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> MetaId
MetaId Int
x) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" into postulate."
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"Name: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
          , TCM Doc
"Type: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
          ]
        ]

      -- Add the new postulate to the signature.
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q Type
t Defn
defaultAxiom

      -- Solve the meta.
      let inst :: MetaInstantiation
inst = [Arg ArgName] -> Term -> MetaInstantiation
InstV [] (Term -> MetaInstantiation) -> Term -> MetaInstantiation
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
      MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar (Int -> MetaId
MetaId Int
x) ((MetaVariable -> MetaVariable) -> TCM ())
-> (MetaVariable -> MetaVariable) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv0 -> MetaVariable
mv0 { mvInstantiation :: MetaInstantiation
mvInstantiation = MetaInstantiation
inst }
      () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    -- Unsolved sort metas can have a type ending in a Dummy if they are allowed to be instantiated
    -- to Setω. This will crash the serializer (issue #3730). To avoid this we replace dummy type
    -- codomains by Setω.
    dummyTypeToOmega :: Type -> Type
dummyTypeToOmega Type
t =
      case Type -> TelV Type
telView' Type
t of
        TelV Telescope
tel (El Sort
_ Dummy{}) -> Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0)
        TelV Type
_ -> Type
t

-- | Sort metas in dependency order.
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas [MetaId]
metas = do
  [(MetaId, MetaId)]
metaGraph <- [[(MetaId, MetaId)]] -> [(MetaId, MetaId)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(MetaId, MetaId)]] -> [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]] -> TCMT IO [(MetaId, MetaId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [MetaId]
-> (MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
metas ((MetaId -> TCMT IO [(MetaId, MetaId)])
 -> TCMT IO [[(MetaId, MetaId)]])
-> (MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]]
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
      Set MetaId
deps <- (MetaId -> Set MetaId) -> Maybe Type -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (\ MetaId
m' -> if MetaId
m' MetaId -> [MetaId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaId]
metas then MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m' else Set MetaId
forall a. Monoid a => a
mempty) (Maybe Type -> Set MetaId)
-> TCMT IO (Maybe Type) -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe Type)
forall (m :: * -> *).
(MonadFail m, MonadReduce m) =>
MetaId -> m (Maybe Type)
getType MetaId
m
      [(MetaId, MetaId)] -> TCMT IO [(MetaId, MetaId)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (MetaId
m, MetaId
m') | MetaId
m' <- Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
deps ]

  Maybe [MetaId] -> TCM (Maybe [MetaId])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [MetaId] -> TCM (Maybe [MetaId]))
-> Maybe [MetaId] -> TCM (Maybe [MetaId])
forall a b. (a -> b) -> a -> b
$ [MetaId] -> [(MetaId, MetaId)] -> Maybe [MetaId]
forall n. Ord n => [n] -> [(n, n)] -> Maybe [n]
Graph.topSort [MetaId]
metas [(MetaId, MetaId)]
metaGraph

  where
    -- Sort metas don't have types, but we still want to sort them.
    getType :: MetaId -> m (Maybe Type)
getType MetaId
m = do
      MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
        IsSort{}                 -> Maybe Type -> m (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
        HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t