{-# 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.IntSet as IntSet
import qualified Data.List as List
import qualified Data.Map.Strict as MapS
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, render)
import qualified Agda.Utils.ProfileOptions as Profile
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' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMeta' = 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 = forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
 MonadDebug m, HasOptions m) =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args) Term
v 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' :: MonadMetaSolver (TCMT IO) =>
MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTerm' = MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTermTCM'
  etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
etaExpandMeta = [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVar = HasCallStack => 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) <- forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM KeepMetas
m
    case KeepMetas
a of
      KeepMetas
KeepMetas     -> 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 :: forall a. Eq a => [a] -> a -> Maybe Nat
findIdx [a]
vs a
v = forall a. Eq a => a -> [a] -> Maybe Nat
List.elemIndex a
v (forall a. [a] -> [a]
reverse [a]
vs)

-- | Does the given local meta-variable have a twin meta-variable?

hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta MetaId
x = do
    MetaVariable
m <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust 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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.blocked" Nat
12 forall a b. (a -> b) -> a -> b
$ [Char]
"is " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
x forall a. [a] -> [a] -> [a]
++ [Char]
" a blocked term? "
    MetaInstantiation
i <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation 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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.blocked" Nat
12 forall a b. (a -> b) -> a -> b
$
      if Bool
r then [Char]
"  yes, because " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaInstantiation
i else [Char]
"  no"
    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 <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case MetaInstantiation
i of
      Open{}                         -> Bool
True
      OpenInstance{}                 -> MetaKind
Records 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 :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
x [Arg [Char]]
tel Term
v = do
     -- verify (new) invariants
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) forall a. HasCallStack => a
__IMPOSSIBLE__
    forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
x [Arg [Char]]
tel Term
v

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

    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Metas forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return () {-tickMax "max-open-metas" . (fromIntegral . size) =<< getOpenMetas-}
    HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
x forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
      MetaVariable
mv { mvInstantiation :: MetaInstantiation
mvInstantiation = Instantiation -> MetaInstantiation
InstV forall a b. (a -> b) -> a -> b
$ Instantiation
             { instTel :: [Arg [Char]]
instTel = [Arg [Char]]
tel
             , instBody :: Term
instBody = Term
v
             -- Andreas, 2022-04-28, issue #5875:
             -- Can't killRange the meta-solution, since this will destroy
             -- ranges of termination errors (and potentially other passes
             -- that run on internal syntax)!
             -- , instBody = killRange v
             }
         }
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
x
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
wakeupConstraints MetaId
x
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
20 forall a b. (a -> b) -> a -> b
$ [Char]
"completed assignment of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
x

-- * Creating meta variables.

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

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMeta :: MonadMetaSolver m => m Sort
newSortMeta :: forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
newSortMeta =
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (forall (m :: * -> *). MonadMetaSolver m => Args -> m (Sort' Term)
newSortMetaCtx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs)
  -- else (no universe polymorphism)
  forall a b. (a -> b) -> a -> b
$ do MetaInfo
i   <- forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
       let j :: Judgement ()
j = forall a. a -> Type -> Judgement a
IsSort () HasCallStack => Type
__DUMMY_TYPE__
       MetaId
x   <- forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
Instantiable MetaInfo
i MetaPriority
normalMetaPriority (Nat -> Permutation
idP Nat
0) Judgement ()
j
       forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 forall a b. (a -> b) -> a -> b
$
         TCMT IO Doc
"new sort meta" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 :: forall (m :: * -> *). MonadMetaSolver m => Args -> m (Sort' Term)
newSortMetaCtx Args
vs = do
    MetaInfo
i   <- forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
    Tele (Dom Type)
tel <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
    let t :: Type
t = Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel HasCallStack => Type
__DUMMY_TYPE__
    MetaId
x   <- forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
Instantiable MetaInfo
i MetaPriority
normalMetaPriority (Nat -> Permutation
idP forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$ forall a. a -> Type -> Judgement a
IsSort () Type
t
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"new sort meta" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
vs

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

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

newTypeMeta_ ::  TCM Type
newTypeMeta_ :: TCM Type
newTypeMeta_  = Comparison -> Sort' Term -> TCM Type
newTypeMeta' Comparison
CmpEq forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
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 :: forall (m :: * -> *). MonadMetaSolver m => m Level
newLevelMeta = do
  (MetaId
x, Term
v) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpEq forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Term
v of
    Level Level
l    -> Level
l
    Term
_          -> 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 :: forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> m (MetaId, Term)
newInstanceMeta [Char]
s Type
t = do
  Args
vs  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Tele (Dom Type)
ctx <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
  forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx [Char]
s (Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
ctx Type
t) Args
vs

newInstanceMetaCtx
  :: MonadMetaSolver m
  => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx :: forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx [Char]
s Type
t Args
vs = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ TCMT IO Doc
"new instance meta:"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"|-"
    ]
  -- Andreas, 2017-10-04, issue #2753: no metaOccurs check for instance metas
  MetaInfo
i0 <- forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
  let i :: MetaInfo
i = MetaInfo
i0 { miNameSuggestion :: [Char]
miNameSuggestion = [Char]
s }
  TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let perm :: Permutation
perm = Nat -> Permutation
idP (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel)
  MetaId
x <- 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 (forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
CmpLeq Type
t)
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 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)
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints (forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
alwaysUnblock Constraint
c) (forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addAwakeConstraint Blocker
alwaysUnblock Constraint
c)
  forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
  forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, MetaId -> Elims -> Term
MetaV MetaId
x forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
b [Char]
s Comparison
cmp Type
t = do
  (MetaId
x, Term
v) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t
  forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
x [Char]
s
  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' :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
b [Char]
s Comparison
cmp Type
t = do
  (MetaId
x, Term
v) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t
  forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
x [Char]
s
  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 :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t = do
  Args
vs  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Tele (Dom Type)
tel <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
  forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
Instantiable RunMetaOccursCheck
b Comparison
cmp Type
t Tele (Dom Type)
tel (Nat -> Permutation
idP forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Args
vs

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

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

newValueMetaCtx'
  :: MonadMetaSolver m
  => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx' :: forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
a Tele (Dom Type)
tel Permutation
perm Args
vs = do
  MetaInfo
i <- forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b
  let t :: Type
t     = Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
a
  MetaId
x <- forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
frozen MetaInfo
i MetaPriority
normalMetaPriority Permutation
perm (forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
cmp Type
t)
  Modality
modality <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Modality TCEnv
eModality
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"new meta (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (MetaInfo
i forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract) forall a. [a] -> [a] -> [a]
++ [Char]
"):"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"|-"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Modality
modality forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
vs
  forall (m :: * -> *).
(MonadConstraint m, MonadTCEnv m, ReadTCState m, MonadAddContext m,
 HasOptions m, HasBuiltins m) =>
Term -> Tele (Dom Type) -> Type -> m ()
boundedSizeMetaHook Term
u Tele (Dom Type)
tel Type
a
  forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, Term
u)

newTelMeta :: MonadMetaSolver m => Telescope -> m Args
newTelMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Tele (Dom Type) -> m Args
newTelMeta Tele (Dom Type)
tel = forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ 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 :: forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta = forall (m :: * -> *).
MonadMetaSolver m =>
Condition -> Type -> m Args
newArgsMeta' Condition
trueCondition

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

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

newArgsMetaCtx'
  :: MonadMetaSolver m
  => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' :: forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx' Frozen
frozen Condition
condition (El Sort' Term
s Term
tm) Tele (Dom Type)
tel Permutation
perm Args
ctx = do
  Term
tm <- 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  = 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' :: Tele (Dom Type)
tel' = ListTel -> Tele (Dom Type)
telFromList forall a b. (a -> b) -> a -> b
$
                 forall a b. (a -> b) -> [a] -> [b]
map (Modality
mod forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) forall a b. (a -> b) -> a -> b
$
                 forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
          ctx' :: Args
ctx' = forall a b. (a -> b) -> [a] -> [b]
map (Modality
mod forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) Args
ctx
      (MetaId
m, Term
u) <- forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info forall a b. (a -> b) -> a -> b
$
                 forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
a Tele (Dom Type)
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).
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((forall a. Eq a => a -> a -> Bool
== DoGeneralize
YesGeneralizeVar) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' DoGeneralize TCEnv
eGeneralizeMetas) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo MetaId
m forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> a
hideOrKeepInstance ArgInfo
info
      forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
m (forall a. Abs a -> [Char]
absName Abs Type
codom)
      Args
args <- forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx' Frozen
frozen Condition
condition (Abs Type
codom forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
u) Tele (Dom Type)
tel Permutation
perm Args
ctx
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
u forall a. a -> [a] -> [a]
: Args
args
    Term
_  -> 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 <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Tele (Dom Type)
tel  <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
  Frozen
-> QName
-> Args
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCM Term
newRecordMetaCtx Frozen
Instantiable QName
r Args
pars Tele (Dom Type)
tel (Nat -> Permutation
idP forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
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
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCM Term
newRecordMetaCtx Frozen
frozen QName
r Args
pars Tele (Dom Type)
tel Permutation
perm Args
ctx = do
  Tele (Dom Type)
ftel   <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall t. Apply t => t -> Args -> t
apply Args
pars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Tele (Dom Type))
getRecordFieldTypes QName
r
  Args
fields <- forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx' Frozen
frozen Condition
trueCondition
              (Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
ftel HasCallStack => Type
__DUMMY_TYPE__) Tele (Dom Type)
tel Permutation
perm Args
ctx
  ConHead
con    <- forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
r
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
fields)

newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark InteractionId
ii Comparison
cmp = (Comparison -> Type -> TCM (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' (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 -> TCM (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' Comparison -> Type -> TCM (MetaId, Term)
new InteractionId
ii Comparison
cmp Type
t = forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii 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 -> TCM (MetaId, Term)
new Comparison
cmp Type
t
    forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
x
    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
      } <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
    -- Get the current context Δ.
    Context
delta <- 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 :: Nat
glen = forall (t :: * -> *) a. Foldable t => t a -> Nat
length Context
gamma
    let dlen :: Nat
dlen = forall (t :: * -> *) a. Foldable t => t a -> Nat
length Context
delta
    let gxs :: [Name]
gxs  = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Context
gamma
    let dxs :: [Name]
dxs  = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Context
delta
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.interaction" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"reusing meta"
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"creation context:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"reusage  context:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 forall a. (a -> Bool) -> [a] -> Maybe Nat
List.findIndex Name -> Bool
nameIsRecordName [Name]
dxs of

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

      -- Case: record variable in the context.
      Just Nat
k -> do
        -- Verify that the contexts relate as expected.
        let g0len :: Nat
g0len = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Name]
dxs forall a. Num a => a -> a -> a
- Nat
k forall a. Num a => a -> a -> a
- Nat
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 = forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameCanonical [Name]
gxs
        let dys :: [Name]
dys = forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameCanonical [Name]
dxs
        let (Nat
d2len, Nat
g1len) = forall a. Eq a => [a] -> [a] -> (Nat, Nat)
findOverlap (forall a. Nat -> [a] -> [a]
take Nat
k [Name]
dys) [Name]
gys
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.interaction" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2)
          [ TCMT IO Doc
"glen  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
glen
          , TCMT IO Doc
"g0len =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
g0len
          , TCMT IO Doc
"g1len =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
g1len
          , TCMT IO Doc
"d2len =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
d2len
          ]
        -- The Γ₀ part should match.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Nat -> [a] -> [a]
drop (Nat
glen forall a. Num a => a -> a -> a
- Nat
g0len) [Name]
gxs forall a. Eq a => a -> a -> Bool
== forall a. Nat -> [a] -> [a]
drop (Nat
k forall a. Num a => a -> a -> a
+ Nat
1) [Name]
dxs) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"expecting meta-creation context (with fields instead of record var)"
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCMT IO Doc
"to share ancestry (suffix) with the meta-reuse context (with record var)"
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
        -- The Γ₁ part should match.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ( (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Nat -> [a] -> [a]
take Nat
g1len) [Name]
gys (forall a. Nat -> [a] -> [a]
drop Nat
d2len [Name]
dys) ) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"expecting meta-creation context (with fields instead of record var)"
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCMT IO Doc
"to be an expansion of the meta-reuse context (with record var)"
            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
        let ([Term]
vs1, Term
v : [Term]
vs0) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
g1len forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var [Nat
d2len..Nat
dlenforall a. Num a => a -> a -> a
-Nat
1]
        -- We need to expand the record var @v@ into the correct number of fields.
        let numFields :: Nat
numFields = Nat
glen forall a. Num a => a -> a -> a
- Nat
g1len forall a. Num a => a -> a -> a
- Nat
g0len
        if Nat
numFields forall a. Ord a => a -> a -> Bool
<= Nat
0 then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Term]
vs1 forall a. [a] -> [a] -> [a]
++ [Term]
vs0 else do
          -- Get the record type.
          let t :: Type
t = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Context
delta forall a. [a] -> Nat -> Maybe a
!!! Nat
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 = forall a b. (a -> b) -> [a] -> [b]
map ((\ QName
x -> Term
v forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
          -- These are the final args to the original meta:
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Term]
vs1 forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [a]
reverse (forall a. Nat -> [a] -> [a]
take Nat
numFields [Term]
vfs) forall a. [a] -> [a] -> [a]
++ [Term]
vs0

    -- Use ArgInfo from Γ.
    let args :: Args
args = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [Term]
rev_args forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 = forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
takeP (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args) Permutation
p) Args
args
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.interaction" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"meta reuse arguments:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs ]
    forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
x, MetaId -> Elims -> Term
MetaV MetaId
x forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 :: forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t m Term
blocker = do
  (ProblemId
pid, Term
v) <- forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m Term
blocker
  forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat 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 :: forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
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 <- forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
solved forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` forall (m :: * -> *).
(ReadTCState m, HasOptions m, HasBuiltins m) =>
ProblemId -> m Bool
isSizeProblem ProblemId
pid)
      (Term
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.blocked" Nat
20 ([Char]
"Not blocking because " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ProblemId
pid forall a. [a] -> [a] -> [a]
++ [Char]
" is " forall a. [a] -> [a] -> [a]
++
                                            if Bool
solved then [Char]
"solved" else [Char]
"a size problem")) forall a b. (a -> b) -> a -> b
$ do
    MetaInfo
i   <- forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
    Elims
es  <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    Tele (Dom Type)
tel <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
    MetaId
x   <- forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' (Term -> MetaInstantiation
BlockedConst forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Term
v)
                    Frozen
Instantiable
                    MetaInfo
i
                    MetaPriority
lowMetaPriority
                    (Nat -> Permutation
idP forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel)
                    (forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
CmpLeq forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
t)
                    -- we don't instantiate blocked terms
    forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (ProblemId -> Blocker
unblockOnProblem ProblemId
pid) (MetaId -> Constraint
UnBlock MetaId
x)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.blocked" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"blocked" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext
        (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel Term
v)
      , TCMT IO Doc
"     by" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid)
      ]
    Bool
inst <- forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
    if Bool
inst
      then 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) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
t
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.blocked" Nat
30
          forall a b. (a -> b) -> a -> b
$   TCMT IO Doc
"setting twin of"
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m'
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to be"
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x
        forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m' (\MetaVariable
mv -> MetaVariable
mv { mvTwin :: Maybe MetaId
mvTwin = forall a. a -> Maybe a
Just MetaId
x })
        Nat
i   <- 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 <- 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))
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.add" Nat
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"adding constraint" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
cmp
        forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (Nat -> ProblemConstraint -> Listener
CheckConstraint Nat
i ProblemConstraint
cmp) MetaId
x
        forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

blockTypeOnProblem
  :: (MonadMetaSolver m, MonadFresh Nat m)
  => Type -> ProblemId -> m Type
blockTypeOnProblem :: forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
Type -> ProblemId -> m Type
blockTypeOnProblem (El Sort' Term
s Term
a) ProblemId
pid = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem (Sort' Term -> Type
sort Sort' Term
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 = 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b) (\ NotBlocked
_ Type
_ -> 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 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
_ Nat
_ 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
_)       = 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 forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Postponed without blocker:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TypeCheckingProblem
p
  forall a. HasCallStack => a
__IMPOSSIBLE__
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock = do
  MetaInfo
i   <- forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
  Tele (Dom Type)
tel <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
  Closure TypeCheckingProblem
cl  <- 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   <- 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 (Nat -> Permutation
idP (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel))
         forall a b. (a -> b) -> a -> b
$ forall a. a -> Comparison -> Type -> Judgement a
HasType () Comparison
CmpLeq forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
t
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.postponed" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"new meta" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
t)
    , TCMT IO Doc
"for postponed typechecking problem" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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  <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  (MetaId
_, Term
v) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
t
  ProblemConstraint
cmp <- 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))
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.add" Nat
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"adding constraint" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
cmp
  Nat
i   <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall i (m :: * -> *). MonadFresh i m => m i
fresh
  forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (Nat -> ProblemConstraint -> Listener
CheckConstraint Nat
i ProblemConstraint
cmp) MetaId
m
  forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock (MetaId -> Constraint
UnBlock MetaId
m)
  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 Nat
_ 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 a local meta-variable, if it is of the specified kind.
--   Don't do anything if the meta-variable is a blocked term.
etaExpandMetaTCM :: [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM :: [MetaKind] -> MetaId -> TCM ()
etaExpandMetaTCM [MetaKind]
kinds MetaId
m = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` [MetaKind] -> MetaId -> TCM Bool
isEtaExpandable [MetaKind]
kinds MetaId
m) forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Nat -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.meta.eta" Nat
20 ([Char]
"etaExpandMeta " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) forall a b. (a -> b) -> a -> b
$ do
    let waitFor :: Blocker -> TCM ()
waitFor Blocker
b = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
20 forall a b. (a -> b) -> a -> b
$ do
            TCMT IO Doc
"postponing eta-expansion of meta variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCMT IO Doc
"which is blocked by" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
b
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (MetaId -> Listener
EtaExpand MetaId
m)) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
        dontExpand :: TCM ()
dontExpand = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
20 forall a b. (a -> b) -> a -> b
$ do
            TCMT IO Doc
"we do not expand meta variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"(requested was expansion of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [MetaKind]
kinds forall a. [a] -> [a] -> [a]
++ [Char]
")")
    MetaVariable
meta <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
    case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
meta of
      IsSort{} -> TCM ()
dontExpand
      HasType MetaId
_ Comparison
cmp Type
a -> do

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

        TelV Tele (Dom Type)
tel Type
b <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"considering eta-expansion at type"
          , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"under telescope"
          , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
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 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall t e. Dom' t e -> Bool
domIsFinite (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel) then TCM ()
dontExpand else do

        -- Issue #3774: continue with the right context for b
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel 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@.
        forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (forall t a. Type'' t a -> a
unEl Type
b) (\ Blocker
x Term
_ -> Blocker -> TCM ()
waitFor Blocker
x) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
t -> case Term
t of
          lvl :: Term
lvl@(Def QName
r Elims
es) ->
            forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r) {- then -} (do
              let ps :: Args
ps = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              let expand :: TCM ()
expand = do
                    Term
u <- forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
meta forall a b. (a -> b) -> a -> b
$
                      Frozen
-> QName
-> Args
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCM Term
newRecordMetaCtx (MetaVariable -> Frozen
mvFrozen MetaVariable
meta) QName
r Args
ps Tele (Dom Type)
tel (Nat -> Permutation
idP forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel
                    -- Andreas, 2019-03-18, AIM XXIX, issue #3597
                    -- When meta is frozen instantiate it with in-turn frozen metas.
                    forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
                      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
                          [ TCMT IO Doc
"eta expanding: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" --> "
                          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ 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.
                      forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
m (forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Tele (Dom Type)
tel) Term
u  -- should never produce any constraints
              if MetaKind
Records forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaKind]
kinds then
                TCM ()
expand
               else if (MetaKind
SingletonRecords forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaKind]
kinds) then
                forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr (\Blocker
x -> Blocker -> TCM ()
waitFor Blocker
x) forall a b. (a -> b) -> a -> b
$ do
                 forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Args -> m Bool
isSingletonRecord QName
r Args
ps) TCM ()
expand TCM ()
dontExpand
                else TCM ()
dontExpand
            ) forall a b. (a -> b) -> a -> b
$ {- else -} forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM [ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaKind
Levels forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaKind]
kinds
                            , forall (m :: * -> *). HasOptions m => m Bool
typeInType
                            , (forall a. a -> Maybe a
Just Term
lvl forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getBuiltin' [Char]
builtinLevel
                            ]) (do
              forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.eta" Nat
20 forall a b. (a -> b) -> a -> b
$ [Char]
"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
              forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
m (forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$ Level -> Term
Level forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
           ) 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 :: forall (m :: * -> *) t.
(MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked t :: Blocked t
t@NotBlocked{} = forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked t :: Blocked t
t@(Blocked Blocker
_ t
v) | Just{} <- forall a. IsMeta a => a -> Maybe MetaId
isMeta t
v = forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked (Blocked Blocker
b t
t)  = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Eta expanding blockers" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
b
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
MonadMetaSolver m =>
[MetaKind] -> MetaId -> m ()
etaExpandMeta [MetaKind
Records]) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
  Blocked t
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 forall a. Eq a => a -> a -> Bool
/= Blocker
b' -> forall (m :: * -> *) t.
(MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked Blocked t
t
    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 :: forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
 MonadDebug m, HasOptions m) =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x Elims
es Term
v m ()
doAssign = do
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas) forall {b}. m b
dontAssign forall a b. (a -> b) -> a -> b
$ {- else -} do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
10 forall a b. (a -> b) -> a -> b
$ do
      TCMT IO Doc
"term" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
":" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow CompareDirection
dir) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints m ()
doAssign forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally` forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

  where dontAssign :: m b
dontAssign = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
10 [Char]
"don't assign metas"
          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 = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker (MetaId -> Blocker
unblockOnMeta MetaId
x) forall a b. (a -> b) -> a -> b
$ do

  MetaVariable
mvar <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x  -- information associated with meta x
  let t :: Type
t = forall a. Judgement a -> Type
jMetaType 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 <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
45 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"MetaVars.assign: assigning meta " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCMT IO Doc
" with args " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) Args
args) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCMT IO Doc
" to " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
45 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"MetaVars.assign: type of meta: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
75 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"MetaVars.assign: assigning meta  " forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"  with args  " forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Args
args forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"  to  " forall a. Semigroup a => a -> a -> a
<> 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' Term
s, HasType{}) -> Sort' Term -> TCM ()
hasBiggerSort Sort' Term
s
      (Term, Judgement MetaId)
_                   -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  let checkSolutionSort :: Comparison -> Sort' Term -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort' Term
s Term
v = do
        Sort' Term
s' <- forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (Sort' Term)
sortOf Term
v
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
40 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Instantiating sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCMT IO Doc
"to sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s' forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of solution" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (forall a. HasRange a => a -> Range
getRange MetaVariable
mvar) MetaId
x (Sort' Term -> Type
sort Sort' Term
s) Term
v) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort' Term -> Sort' Term -> m ()
compareSort Comparison
cmp Sort' Term
s' Sort' Term
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 = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation forall a b. (a -> b) -> a -> b
$ forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t -- TODO: make piApplyM' compute unblocker
        Type
t' <- 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' Term
s <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m (Sort' Term)
shouldBeSort Type
t'
        Comparison -> Sort' Term -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort' Term
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 = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation forall a b. (a -> b) -> a -> b
$ forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t
          Type
t' <- 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 Tele (Dom Type)
tel Type
t'' <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t'
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadReduce m, MonadBlock m) =>
Type -> m a -> (Sort' Term -> m a) -> m a
ifNotSort Type
t'' (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \Sort' Term
s -> do
            let v' :: Term
v' = forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Term
v forall t. Apply t => t -> Args -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel
            Comparison -> Sort' Term -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort' Term
s Term
v'

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



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

  -- We never get blocked terms here anymore. TODO: we actually do. why?
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCM Bool
isBlockedTerm MetaId
x) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
25 forall a b. (a -> b) -> a -> b
$ [Char]
"aborting: meta is a blocked term!"
    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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
50 forall a b. (a -> b) -> a -> b
$ [Char]
"MetaVars.assign: I want to see whether rhs is blocked"
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
25 forall a b. (a -> b) -> a -> b
$ do
    Blocked Term
v0 <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
    case Blocked Term
v0 of
      Blocked Blocker
m0 Term
_ -> TCMT IO Doc
"r.h.s. blocked on:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
m0
      NotBlocked{} -> TCMT IO 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 forall a b. (a -> b) -> a -> b
$ \ Term
v -> do

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 forall a b. (a -> b) -> a -> b
$ do
      Tele (Dom Type)
cxt <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"context before projection expansion"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
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.

    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) forall a b. (a -> b) -> a -> b
$ \ Args
args (Term
v, CompareAs
target) -> do

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 forall a b. (a -> b) -> a -> b
$ do
        Tele (Dom Type)
cxt <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"context after projection expansion"
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
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        = forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
freeVars Args
args
                relVL :: [Nat]
relVL       = (VarOcc -> Bool) -> VarMap -> [Nat]
filterVarMapToList forall a. LensRelevance a => a -> Bool
isRelevant  VarMap
vars
                nonstrictVL :: [Nat]
nonstrictVL = (VarOcc -> Bool) -> VarMap -> [Nat]
filterVarMapToList forall a. LensRelevance a => a -> Bool
isNonStrict VarMap
vars
                irrVL :: [Nat]
irrVL       = (VarOcc -> Bool) -> VarMap -> [Nat]
filterVarMapToList (forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) forall a. LensRelevance a => a -> Bool
isIrrelevant 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.

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
20 forall a b. (a -> b) -> a -> b
$
          let pr :: Term -> m Doc
pr (Var Nat
n []) = forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Nat
n)
              pr (Def QName
c []) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c
              pr Term
_          = m Doc
".."
          in forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
               [ TCMT IO Doc
"mvar args:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
Term -> m Doc
pr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) Args
args)
               , TCMT IO Doc
"fvars lhs (rel):" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [Nat]
relVL)
               , TCMT IO Doc
"fvars lhs (nonstrict):" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [Nat]
nonstrictVL)
               , TCMT IO Doc
"fvars lhs (irr):" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [Nat]
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 <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a.
(Occurs a, InstantiateFull a, PrettyTCM a) =>
MetaId -> VarMap -> a -> TCM a
occursCheck MetaId
x VarMap
vars Term
v

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
15 [Char]
"passed occursCheck"
      forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
verboseS [Char]
"tc.meta.assign" Nat
30 forall a b. (a -> b) -> a -> b
$ do
        let n :: Nat
n = forall a. TermSize a => a -> Nat
termSize Term
v
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Nat
n forall a. Ord a => a -> a -> Bool
> Nat
200) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
30 forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"size" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Nat
n)
--              , nest 2 $ "type" <+> prettyTCM t
              , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"term" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 = forall t. Free t => t -> VarSet
allFreeVars Term
v
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
20 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"fvars rhs:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) forall a b. (a -> b) -> a -> b
$ VarSet -> [Nat]
VarSet.toList VarSet
fvs)

      -- Check that the arguments are variables
      Maybe SubstCand
mids <- do
        Either InvertExcept SubstCand
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ Args -> ExceptT InvertExcept (TCMT IO) SubstCand
inverseSubst Args
args
        case Either InvertExcept SubstCand
res of
          -- all args are variables
          Right SubstCand
ids -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
60 forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"inverseSubst returns:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty SubstCand
ids)
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
50 forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"inverseSubst returns:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SubstCand
ids)
            let boundVars :: VarSet
boundVars = [Nat] -> VarSet
VarSet.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst SubstCand
ids
            if VarSet
fvs VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` VarSet
boundVars
              then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SubstCand
ids
              else forall (m :: * -> *) a. Monad m => a -> m a
return 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
          -- we have non-variables, but these are not eliminateable
          Left InvertExcept
NeutralArg  -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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{}   -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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  -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v)  -- TODO: more precise
        Just SubstCand
ids -> do
          -- Check linearity
          SubstCand
ids <- do
            Either () SubstCand
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ SubstCand -> ExceptT () (TCMT IO) SubstCand
checkLinearity {- (`VarSet.member` fvs) -} SubstCand
ids
            case Either () SubstCand
res of
              -- case: linear
              Right SubstCand
ids -> 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 ()   -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker (forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v) forall a b. (a -> b) -> a -> b
$ forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs

          -- Check ids is time respecting.
          () <- do
            let idvars :: [(Nat, VarSet)]
idvars = forall a b. (a -> b) -> [a] -> [b]
map (forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd 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 forall a. Ord a => a -> a -> Bool
> a
l
            TelV Tele (Dom Type)
tel' Type
_ <- forall (m :: * -> *). PureTCM m => Nat -> Type -> m (TelV Type)
telViewUpToPath (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args) Type
t
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ SubstCand
ids forall a b. (a -> b) -> a -> b
$ \(Nat
i,Term
u) -> do
              Dom (Name, Type)
d <- forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Nat -> m (Dom (Name, Type))
lookupBV Nat
i
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. LensLock a => a -> Lock
getLock (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom (Name, Type)
d) forall a. Eq a => a -> a -> Bool
== Lock
IsLock) forall a b. (a -> b) -> a -> b
$ do
                let us :: VarSet
us = forall (f :: * -> *). Foldable f => f VarSet -> VarSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
earlierThan Nat
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Nat, VarSet)]
idvars
                -- us Earlier than u
                forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel' forall a b. (a -> b) -> a -> b
$ Term -> VarSet -> TCM ()
checkEarlierThan Term
u VarSet
us
                  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
                     TypeError{} -> 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         -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err                     -- solve this meta in some other way.

          let n :: Nat
n = forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args
          TelV Tele (Dom Type)
tel' Type
_ <- forall (m :: * -> *). PureTCM m => Nat -> Type -> m (TelV Type)
telViewUpToPath Nat
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 = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
args
          Bool
hasSubtyping <- PragmaOptions -> Bool
optCumulativity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hasSubtyping forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ SubstCand
ids forall a b. (a -> b) -> a -> b
$ \(Nat
i , Term
u) -> do
            -- @u@ is a (projected) variable, so we can infer its type
            Type
a  <- forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sigma forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel' (forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer Term
u)
            Type
a' <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
i
            Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a' Type
a
              forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
                TypeError{} -> 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         -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err                     -- solve this meta in some other way.

          -- Solve.
          Nat
m <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
          Nat -> MetaId -> Type -> Nat -> SubstCand -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Type
t Nat
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 :: forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs = do
      -- non-linear lhs: we cannot solve, but prune
      PruneResult
killResult <- forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaId -> Args -> (Nat -> Bool) -> m PruneResult
prune MetaId
x Args
args forall a b. (a -> b) -> a -> b
$ (Nat -> VarSet -> Bool
`VarSet.member` VarSet
fvs)
      let success :: Bool
success = PruneResult
killResult forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PruneResult
PrunedSomething,PruneResult
PrunedEverything]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
10 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"pruning" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ if Bool
success then [Char]
"succeeded" else [Char]
"failed"
      Blocker
blocker <- if
        | Bool
success   -> forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock  -- If pruning succeeded we want to retry right away
        | Bool
otherwise -> forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Elims -> Term
MetaV MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Args
args
             -- TODO: could be more precise: only unblock on metas
             --       applied to offending variables
      forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker

{- 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 :: Nat -> MetaId -> Type -> [Nat] -> Term -> TCM ()
assignMeta Nat
m MetaId
x Type
t [Nat]
ids Term
v = do
  let n :: Nat
n    = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Nat]
ids
      cand :: SubstCand
cand = forall a. Ord a => [a] -> [a]
List.sort forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Nat]
ids forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Nat
n
  Nat -> MetaId -> Type -> Nat -> SubstCand -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Type
t Nat
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' :: Nat -> MetaId -> Type -> Nat -> SubstCand -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Type
t Nat
n SubstCand
ids Term
v = do
  -- we are linear, so we can solve!
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
25 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"preparing to instantiate: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 :: Nat -> SubstCand -> [Maybe Term]
assocToList Nat
i = \case
        SubstCand
_           | Nat
i forall a. Ord a => a -> a -> Bool
>= Nat
m -> []
        ((Nat
j,Term
u) : SubstCand
l) | Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j -> forall a. a -> Maybe a
Just Term
u  forall a. a -> [a] -> [a]
: Nat -> SubstCand -> [Maybe Term]
assocToList (Nat
iforall a. Num a => a -> a -> a
+Nat
1) SubstCand
l
        SubstCand
l                    -> forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: Nat -> SubstCand -> [Maybe Term]
assocToList (Nat
iforall a. Num a => a -> a -> a
+Nat
1) SubstCand
l
      ivs :: [Maybe Term]
ivs = Nat -> SubstCand -> [Maybe Term]
assocToList Nat
0 SubstCand
ids
      rho :: Substitution' Term
rho = forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS HasCallStack => Impossible
impossible [Maybe Term]
ivs forall a b. (a -> b) -> a -> b
$ forall a. Nat -> Substitution' a
raiseS Nat
n
      v' :: Term
v'  = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
rho Term
v

  -- Metas are top-level so we do the assignment at top-level.
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext 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)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"type of meta =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t

    (telv :: TelV Type
telv@(TelV Tele (Dom Type)
tel' Type
a), Boundary
bs) <- forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary Nat
n Type
t
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel'  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel'
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"#args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Nat
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)
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel' forall a. Ord a => a -> a -> Bool
< Nat
n) forall a b. (a -> b) -> a -> b
$ do
      Type
a <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
a
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"not enough pis, but not blocked?" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
      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 = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel' Term
v'

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

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
10 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"solving" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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'

    forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
x (forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Tele (Dom Type)
tel') Term
v'
  where
    blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term
    blockOnBoundary :: TelV Type -> Boundary -> Term -> TCM Term
blockOnBoundary TelV Type
telv         [] Term
v = forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    blockOnBoundary (TelV Tele (Dom Type)
tel Type
t) Boundary
bs Term
v = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t forall a b. (a -> b) -> a -> b
$ do
        Term
neg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Boundary
bs forall a b. (a -> b) -> a -> b
$ \ (Term
r,(Term
x,Term
y)) -> do
          forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace (Term
neg forall t. Apply t => t -> Term -> t
`apply1` Term
r) Type
t Term
x Term
v
          forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace Term
r  Type
t Term
y Term
v
        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 <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
  let postpone :: TCM ()
postpone = forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) 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 Instantiation
inst -> do
      let n :: Nat
n = forall a. Sized a => a -> Nat
size (Instantiation -> [Arg [Char]]
instTel Instantiation
inst)
          t :: Type
t = forall a. Judgement a -> Type
jMetaType forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m
      (telv :: TelV Type
telv@(TelV Tele (Dom Type)
tel Type
a),Boundary
bs) <- forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary Nat
n Type
t
      forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (MetaId -> Constraint
CheckMetaInst MetaId
x) forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$
        MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m (Instantiation -> Term
instBody Instantiation
inst) 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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking solution for meta" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ do
        Context
ctx <- forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"in context: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Context -> PrettyContext
PrettyContext Context
ctx)
      forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x Type
a Term
v) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> Type -> m ()
checkInternal Term
v Comparison
cmp Type
a
    IsSort{}  -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is a sort"
      Sort' Term
s <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m (Sort' Term)
shouldBeSort (forall t a. Sort' t -> a -> Type'' t a
El HasCallStack => Sort' Term
__DUMMY_SORT__ Term
v)
      forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x (Sort' Term -> Type
sort (Sort' Term -> Sort' Term
univSort Sort' Term
s)) (Sort' Term -> Term
Sort Sort' Term
s)) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Sort' Term -> m (Sort' Term)
checkSort forall (m :: * -> *). PureTCM m => Action m
defaultAction Sort' Term
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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.subtype" Nat
30 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"checking that subtype" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCMT IO Doc
"of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is actually equal."
  forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Type
a Type
b (\Type
_ Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \Type
a Type
b -> do
    Bool
cumulativity <- PragmaOptions -> Bool
optCumulativity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall t a. Type'' t a -> a
unEl Type
b) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Sort Sort' Term
sb -> forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall t a. Type'' t a -> a
unEl Type
a) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Sort Sort' Term
sa | Bool
cumulativity -> forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
equalSort Sort' Term
sa Sort' Term
sb
                             | Bool
otherwise    -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Dummy{} -> 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 -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a) -- TODO: can this happen?
      Pi Dom Type
b1 Abs Type
b2 -> forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall t a. Type'' t a -> a
unEl Type
a) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Pi Dom Type
a1 Abs Type
a2
          | forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
a1 forall a. Eq a => a -> a -> Bool
/= forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
b1 -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock -- Can we recover from this?
          | forall a. LensQuantity a => a -> Quantity
getQuantity  Dom Type
a1 forall a. Eq a => a -> a -> Bool
/= forall a. LensQuantity a => a -> Quantity
getQuantity  Dom Type
b1 -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | forall a. LensCohesion a => a -> Cohesion
getCohesion  Dom Type
a1 forall a. Eq a => a -> a -> Bool
/= forall a. LensCohesion a => a -> Cohesion
getCohesion  Dom Type
b1 -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | Bool
otherwise -> do
              Type -> Type -> TCM ()
checkSubtypeIsEqual (forall t e. Dom' t e -> e
unDom Dom Type
b1) (forall t e. Dom' t e -> e
unDom Dom Type
a1)
              forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a1 Abs Type
a2 forall a b. (a -> b) -> a -> b
$ \Type
a2' -> Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a2' (forall a. Subst a => Abs a -> a
absBody Abs Type
b2)
        Dummy{} -> 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 -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a)
      -- TODO: check subtyping for Size< types
      Term
_ -> 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 local meta-variable @x@.
  -> MetaVariable     -- ^ Its associated information @mvar <- lookupLocalMeta 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) <- forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
mSize   TCM ()
fallback forall a b. (a -> b) -> a -> b
$ \ QName
qSize   -> do
    forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
mSizeLt TCM ()
fallback forall a b. (a -> b) -> a -> b
$ \ QName
qSizeLt -> do
      -- Check whether v is a SIZELT
      Term
v <- 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 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 Tele (Dom Type)
tel 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'   = Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
size
          MetaId
y <- 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)
                       (forall a. a -> Comparison -> Type -> Judgement a
HasType 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args
          forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
y) forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args
              v' :: Term
v'    = QName -> Elims -> Term
Def QName
qSizeLt [forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
yArgs]
              c :: Constraint
c     = 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'
          forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint Constraint
c 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 :: 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 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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"meta args: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
args
    a
args <- forall a. TCM a -> TCM a
callByName forall a b. (a -> b) -> a -> b
$ forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract a
args
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"norm args: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
args
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
85 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"norm args: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar a
args of
      Right ()              -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
40 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"no projected var found in args: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
args
        TCM c
done
      Left (ProjectedVar Nat
i [(ProjOrigin, QName)]
_) -> forall a c.
(PrettyTCM a, TermSubst a) =>
Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Nat
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 :: forall a c.
(PrettyTCM a, TermSubst a) =>
Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Nat
i a
v TCM c
fail a -> TCM c
succeed = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
40 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"trying to expand projected variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Nat -> Term
var Nat
i)
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Nat
-> TCM
     (Maybe (Tele (Dom Type), Substitution' Term, Substitution' Term))
etaExpandBoundVar Nat
i) TCM c
fail forall a b. (a -> b) -> a -> b
$ \ (Tele (Dom Type)
delta, Substitution' Term
sigma, Substitution' Term
tau) -> do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
25 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"eta-expanding var " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Nat -> Term
var Nat
i) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
      TCMT IO Doc
" in terms " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
    forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
delta forall a b. (a -> b) -> a -> b
$
      a -> TCM c
succeed forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ 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 Nat
i Elims
es
        | qs :: [(ProjOrigin, QName)]
qs@((ProjOrigin, QName)
_:[(ProjOrigin, QName)]
_) <- forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es
        -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
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 <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -> forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar Args
vs
      Term
_ -> 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM 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
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u 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 [Char]
x Term
b) -> forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ArgInfo -> [Char] -> Term -> m Term
etaLam ArgInfo
ai [Char]
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Term
b
      Con ConHead
c ConInfo
ci Elims
es -> 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 forall a b. (a -> b) -> a -> b
$ \ QName
r ConHead
c ConInfo
ci Args
args -> do
        Args
args <- forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Args
args
        forall (m :: * -> *).
HasConstInfo m =>
QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord QName
r ConHead
c ConInfo
ci Args
args
      Term
v -> 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 () (TCMT IO) SubstCand
checkLinearity SubstCand
ids0 = do
  let ids :: SubstCand
ids = forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) SubstCand
ids0  -- see issue 920
  let grps :: [SubstCand]
grps = forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupOn forall a b. (a, b) -> a
fst SubstCand
ids
  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubstCand -> ExceptT () (TCMT IO) 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 () (TCMT IO) SubstCand
makeLinear []            = forall a. HasCallStack => a
__IMPOSSIBLE__
    makeLinear grp :: SubstCand
grp@[(Nat, Term)
_]       = forall (m :: * -> *) a. Monad m => a -> m a
return SubstCand
grp
    makeLinear (p :: (Nat, Term)
p@(Nat
i,Term
t) : SubstCand
_) =
      forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((forall a b. b -> Either a b
Right Bool
True forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
i)
        (forall (m :: * -> *) a. Monad m => a -> m a
return [(Nat, Term)
p])
        (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 (TCMT IO) SubstCand
inverseSubst Args
args = forall a b. (a -> b) -> [a] -> [b]
map (forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall e. Arg e -> e
unArg) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Arg Term, Term)] -> ExceptT InvertExcept (TCMT IO) Res
loop (forall a b. [a] -> [b] -> [(a, b)]
zip Args
args [Term]
terms)
  where
  loop :: [(Arg Term, Term)] -> ExceptT InvertExcept (TCMT IO) Res
loop  = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Res -> (Arg Term, Term) -> ExceptT InvertExcept (TCMT IO) Res
isVarOrIrrelevant []
  terms :: [Term]
terms = forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var (forall a. Integral a => a -> [a]
downFrom (forall a. Sized a => a -> Nat
size Args
args))
  failure :: ExceptT InvertExcept (TCMT IO) Res
failure = do
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"not all arguments are variables: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
args
      , TCMT IO Doc
"  aborting assignment" ]
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvertExcept
CantInvert
  neutralArg :: ExceptT InvertExcept (TCMT IO) a
neutralArg = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvertExcept
NeutralArg

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

      -- π i := x  try to eta-expand projection π away!
      Var Nat
i Elims
es | Just [(ProjOrigin, QName)]
qs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ProjectedVar -> InvertExcept
ProjVar forall a b. (a -> b) -> a -> b
$ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
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 (TCMT IO) Res
fallback
             | forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = forall (m :: * -> *) a. Monad m => a -> m a
return Res
vars
             | Bool
otherwise                              = ExceptT InvertExcept (TCMT IO) Res
failure
        Bool
irrProj <- PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) 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
            , forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom QName]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es
            , forall a. LensQuantity a => a -> Bool
hasQuantity0 ArgInfo
info Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. LensQuantity a => a -> Bool
usableQuantity [Dom QName]
fs     -- Andreas, 2019-11-12/17, issue #4168b
            , Bool
irrProj Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all 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} =
                    (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v,) forall a b. (a -> b) -> a -> b
$ Term
t forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
                    where
                    ai :: ArgInfo
ai = ArgInfo
                      { argInfoHiding :: Hiding
argInfoHiding   = forall a. Ord a => a -> a -> a
min (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info')
                      , argInfoModality :: Modality
argInfoModality = Modality
                        { modRelevance :: Relevance
modRelevance  = forall a. Ord a => a -> a -> a
max (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info')
                        , modQuantity :: Quantity
modQuantity   = forall a. Ord a => a -> a -> a
max (forall a. LensQuantity a => a -> Quantity
getQuantity  ArgInfo
info) (forall a. LensQuantity a => a -> Quantity
getQuantity  ArgInfo
info')
                        , modCohesion :: Cohesion
modCohesion   = forall a. Ord a => a -> a -> a
max (forall a. LensCohesion a => a -> Cohesion
getCohesion  ArgInfo
info) (forall a. LensCohesion a => a -> Cohesion
getCohesion  ArgInfo
info')
                        }
                      , argInfoOrigin :: Origin
argInfoOrigin   = forall a. Ord a => a -> a -> a
min (forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info) (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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              Res
res <- [(Arg Term, Term)] -> ExceptT InvertExcept (TCMT IO) Res
loop forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Dom QName -> (Arg Term, Term)
aux Args
vs [Dom QName]
fs
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Res
res Res -> Res -> Res
`append` Res
vars
            | Bool
otherwise -> ExceptT InvertExcept (TCMT IO) Res
fallback
          Maybe (QName, Defn)
_ -> ExceptT InvertExcept (TCMT IO) Res
fallback

      -- An irrelevant argument which is not an irrefutable pattern is dropped
      Term
_ | Bool
irr -> forall (m :: * -> *) a. Monad m => a -> m a
return Res
vars

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

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

  -- adding an irrelevant entry only if not present
  cons :: (Arg Nat, Term) -> Res -> Res
  cons :: (Arg Nat, Term) -> Res -> Res
cons a :: (Arg Nat, Term)
a@(Arg ArgInfo
ai Nat
i, Term
t) Res
vars
    | forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
ai = forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Nat
iforall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Res
vars) ((Arg Nat, Term)
a forall a. a -> [a] -> [a]
:) Res
vars
    | Bool
otherwise       = (Arg Nat, Term)
a forall a. a -> [a] -> [a]
:  -- adding a relevant entry
        -- filter out duplicate irrelevants
        forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ a :: (Arg Nat, Term)
a@(Arg ArgInfo
info Nat
j, Term
t) -> forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info Bool -> Bool -> Bool
&& Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j)) Res
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 <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ModuleName
envCurrentModule

  -- Go through all open metas.
  [(MetaId, MetaVariable)]
ms <- forall k a. Map k a -> [(k, a)]
MapS.assocs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' LocalMetaStore TCState
stOpenMetaStore
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(MetaId, MetaVariable)]
ms forall a b. (a -> b) -> a -> b
$ \ (MetaId
x, MetaVariable
mv) -> do
    let t :: Type
t = Type -> Type
dummyTypeToOmega forall a b. (a -> b) -> a -> b
$ forall a. Judgement a -> Type
jMetaType forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv

    -- Create a name for the new postulate.
    let r :: Range
r = forall a. Closure a -> a
clValue forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv
    [Char]
s' <- Doc -> [Char]
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x -- Using _ is a bad idea, as it prints as prefix op
    let s :: [Char]
s = [Char]
"unsolved#meta." forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
'_') [Char]
s'
    Name
n <- forall (m :: * -> *).
MonadFresh NameId m =>
Range -> [Char] -> m Name
freshName Range
r [Char]
s
    let q :: QName
q = ModuleName -> Name -> QName
A.QName ModuleName
m Name
n

    -- Debug.
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"meta.postulate" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Turning " forall a. [a] -> [a] -> [a]
++ if MetaVariable -> Bool
isSortMeta_ MetaVariable
mv then [Char]
"sort" else [Char]
"value" forall a. [a] -> [a] -> [a]
++ [Char]
" meta ")
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" into postulate."
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"Name: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
        , TCMT IO Doc
"Type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 = Instantiation -> MetaInstantiation
InstV forall a b. (a -> b) -> a -> b
$ Instantiation
                 { instTel :: [Arg [Char]]
instTel = [], instBody :: Term
instBody = QName -> Elims -> Term
Def QName
q [] }
    forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
x forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv0 -> MetaVariable
mv0 { mvInstantiation :: MetaInstantiation
mvInstantiation = MetaInstantiation
inst }
    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 Tele (Dom Type)
tel (El Sort' Term
_ Dummy{}) -> forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Sort' Term -> Type
sort forall a b. (a -> b) -> a -> b
$ 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 <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
metas forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
      Set MetaId
deps <- forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (\MetaId
m' -> if MetaId
m' forall a. Ord a => a -> Set a -> Bool
`Set.member` Set MetaId
metas'
                               then forall el coll. Singleton el coll => el -> coll
singleton MetaId
m'
                               else forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                forall {m :: * -> *}. MonadReduce m => MetaId -> m (Maybe Type)
getType MetaId
m
      forall (m :: * -> *) a. Monad m => a -> m a
return [ (MetaId
m, MetaId
m') | MetaId
m' <- forall a. Set a -> [a]
Set.toList Set MetaId
deps ]

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

  where
    metas' :: Set MetaId
metas' = forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas

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