{-# LANGUAGE CPP #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.MetaVars.Occurs where
import Control.Monad
import Control.Monad.Reader
import Data.Foldable (foldMap)
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import Data.Traversable (traverse)
import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free hiding (Occurrence(..))
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Records
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.Utils.Either
import Agda.Utils.Except
( ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Lens
import Agda.Utils.List (downFrom)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs f = stOccursCheckDefs %= f
initOccursCheck :: MetaVariable -> TCM ()
initOccursCheck mv = modifyOccursCheckDefs . const =<<
if (miMetaOccursCheck (mvInfo mv) == DontRunMetaOccursCheck)
then do
reportSLn "tc.meta.occurs" 20 $
"initOccursCheck: we do not look into definitions"
return Set.empty
else do
reportSLn "tc.meta.occurs" 20 $
"initOccursCheck: we look into the following definitions:"
mb <- asks envMutualBlock
case mb of
Nothing -> do
reportSLn "tc.meta.occurs" 20 $ "(none)"
return Set.empty
Just b -> do
ds <- mutualNames <$> lookupMutualBlock b
reportSDoc "tc.meta.occurs" 20 $ sep $ map prettyTCM $ Set.toList ds
return ds
defNeedsChecking :: QName -> TCM Bool
defNeedsChecking d = Set.member d <$> use stOccursCheckDefs
tallyDef :: QName -> TCM ()
tallyDef d = modifyOccursCheckDefs $ \ s -> Set.delete d s
data OccursCtx
= Flex
| Rigid
| StronglyRigid
| Irrel
deriving (Eq, Show)
data UnfoldStrategy = YesUnfold | NoUnfold
deriving (Eq, Show)
defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
defArgs NoUnfold _ = Flex
defArgs YesUnfold ctx = weakly ctx
unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
unfold NoUnfold v = notBlocked <$> instantiate v
unfold YesUnfold v = reduceB v
weakly :: OccursCtx -> OccursCtx
weakly StronglyRigid = Rigid
weakly ctx = ctx
strongly :: OccursCtx -> OccursCtx
strongly Rigid = StronglyRigid
strongly ctx = ctx
patternViolation' :: Int -> String -> TCM a
patternViolation' n err = do
reportSLn "tc.meta.occurs" n err
patternViolation
abort :: OccursCtx -> TypeError -> TCM a
abort StronglyRigid err = typeError err
abort Flex err = patternViolation' 70 (show err)
abort Rigid err = patternViolation' 70 (show err)
abort Irrel err = patternViolation' 70 (show err)
type Vars = ([Nat],[Nat],[Nat])
goIrrelevant :: Vars -> Vars
goIrrelevant (relVs, nonstrictVs, irrVs) = (irrVs ++ nonstrictVs ++ relVs, [], [])
goNonStrict :: Vars -> Vars
goNonStrict (relVs, nonstrictVs, irrVs) = (nonstrictVs ++ relVs, [], irrVs)
allowedVar :: Nat -> Vars -> Bool
allowedVar i (relVs, nonstrictVs, irrVs) = i `elem` relVs
takeRelevant :: Vars -> [Nat]
takeRelevant (relVs, nonstrictVs, irrVs) = relVs
takeAll :: Vars -> [Nat]
takeAll (rel, nst, irr) = rel ++ nst ++ irr
liftUnderAbs :: Vars -> Vars
liftUnderAbs (relVs, nonstrictVs, irrVs) = (0 : map (1+) relVs, map (+1) nonstrictVs, map (1+) irrVs)
class Occurs t where
occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t
metaOccurs :: MetaId -> t -> TCM ()
occursCheck
:: (Occurs a, InstantiateFull a, PrettyTCM a)
=> MetaId -> Vars -> a -> TCM a
occursCheck m xs v = disableDestructiveUpdate $ Bench.billTo [ Bench.Typing, Bench.OccursCheck ] $ do
mv <- lookupMeta m
let ctx = if isIrrelevant (getMetaRelevance mv) then Irrel else StronglyRigid
initOccursCheck mv
let redo m = m
redo (occurs NoUnfold ctx m xs v) `catchError` \_ -> do
initOccursCheck mv
redo (occurs YesUnfold ctx m xs v) `catchError` \err -> case err of
TypeError _ cl -> case clValue cl of
MetaOccursInItself{} ->
typeError . GenericError . show =<<
fsep [ text ("Refuse to construct infinite term by instantiating " ++ prettyShow m ++ " to")
, prettyTCM =<< instantiateFull v
]
MetaCannotDependOn _ _ i ->
ifM (isSortMeta m `and2M` (not <$> hasUniversePolymorphism))
( typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to")
, prettyTCM v
, text "since universe polymorphism is disabled"
]
)
( typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to solution")
, prettyTCM v
, text "since it contains the variable"
, enterClosure cl $ \_ -> prettyTCM (Var i [])
, text $ "which is not in scope of the metavariable or irrelevant in the metavariable but relevant in the solution"
]
)
MetaIrrelevantSolution _ _ ->
typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to solution")
, prettyTCM v
, text "since (part of) the solution was created in an irrelevant context."
]
_ -> throwError err
_ -> throwError err
instance Occurs Term where
occurs red ctx m xs v = do
v <- unfold red v
case v of
NotBlocked _ v -> occurs' ctx v
Blocked _ v -> occurs' Flex v
where
occurs' ctx v = do
reportSDoc "tc.meta.occurs" 45 $
text ("occursCheck " ++ prettyShow m ++ " (" ++ show ctx ++ ") of ") <+> prettyTCM v
reportSDoc "tc.meta.occurs" 70 $
nest 2 $ text $ show v
case v of
Var i es -> do
if (i `allowedVar` xs) then Var i <$> occ (weakly ctx) es else do
reportSDoc "tc.meta.occurs" 35 $ text "offending variable: " <+> prettyTCM (var i)
t <- typeOfBV i
reportSDoc "tc.meta.occurs" 35 $ nest 2 $ text "of type " <+> prettyTCM t
isST <- isSingletonType t
reportSDoc "tc.meta.occurs" 35 $ nest 2 $ text "(after singleton test)"
case isST of
Left mid -> patternViolation' 70 $ "Disallowed var " ++ show i ++ " not obviously singleton"
Right Nothing ->
abort (strongly ctx) $ MetaCannotDependOn m (takeRelevant xs) i
Right (Just sv) -> return $ sv `applyE` es
Lam h f -> Lam h <$> occ ctx f
Level l -> Level <$> occ ctx l
Lit l -> return v
DontCare v -> if ctx == Irrel then
dontCare <$> occurs red ctx m xs v
else
abort (strongly ctx) $ MetaIrrelevantSolution m v
Def d es -> do
drel <- relOfConst d
unless (not (unusableRelevance drel) || ctx == Irrel) $ do
reportSDoc "tc.meta.occurs" 35 $ text ("relevance of definition: " ++ show drel)
abort ctx $ MetaIrrelevantSolution m $ Def d []
Def d <$> occDef d ctx es
Con c ci vs -> Con c ci <$> occ ctx vs
Pi a b -> uncurry Pi <$> occ ctx (a,b)
Sort s -> Sort <$> occurs red ctx m (goNonStrict xs) s
MetaV m' es -> do
when (m == m') $ patternViolation' 50 $ "occursCheck failed: Found " ++ prettyShow m
(MetaV m' <$> occurs red Flex m xs es) `catchError` \err -> do
reportSDoc "tc.meta.kill" 25 $ vcat
[ text $ "error during flexible occurs check, we are " ++ show ctx
, text $ show err
]
case err of
PatternErr{} | ctx /= Flex -> do
reportSLn "tc.meta.kill" 20 $
"oops, pattern violation for " ++ prettyShow m'
caseMaybe (allApplyElims es) (throwError err) $ \ vs -> do
killResult <- prune m' vs (takeAll xs)
if (killResult == PrunedEverything)
then occurs red ctx m xs =<< instantiate (MetaV m' es)
else throwError err
_ -> throwError err
where
occ ctx v = occurs red ctx m xs v
occDef d ctx vs = do
metaOccurs m d
ifM (isJust <$> isDataOrRecordType d)
(occ ctx vs)
(occ (defArgs red ctx) vs)
metaOccurs m v = do
v <- instantiate v
case v of
Var i vs -> metaOccurs m vs
Lam h f -> metaOccurs m f
Level l -> metaOccurs m l
Lit l -> return ()
DontCare v -> metaOccurs m v
Def d vs -> metaOccurs m d >> metaOccurs m vs
Con c _ vs -> metaOccurs m vs
Pi a b -> metaOccurs m (a,b)
Sort s -> metaOccurs m s
MetaV m' vs | m == m' -> patternViolation' 50 $ "Found occurrence of " ++ prettyShow m
| otherwise -> metaOccurs m vs
instance Occurs QName where
occurs red ctx m xs d = __IMPOSSIBLE__
metaOccurs m d = whenM (defNeedsChecking d) $ do
tallyDef d
reportSLn "tc.meta.occurs" 30 $ "Checking for occurrences in " ++ show d
metaOccurs m . theDef =<< ignoreAbstractMode (getConstInfo d)
instance Occurs Defn where
occurs red ctx m xs def = __IMPOSSIBLE__
metaOccurs m Axiom{} = return ()
metaOccurs m Function{ funClauses = cls } = metaOccurs m cls
metaOccurs m Datatype{ dataCons = cs } = mapM_ mocc cs
where mocc c = metaOccurs m . defType =<< getConstInfo c
metaOccurs m Record{ recConHead = c } = metaOccurs m . defType =<< getConstInfo (conName c)
metaOccurs m Constructor{} = return ()
metaOccurs m Primitive{} = return ()
metaOccurs m AbstractDefn{} = __IMPOSSIBLE__
instance Occurs Clause where
occurs red ctx m xs cl = __IMPOSSIBLE__
metaOccurs m = metaOccurs m . clauseBody
instance Occurs Level where
occurs red ctx m xs (Max as) = Max <$> occurs red ctx m xs as
metaOccurs m (Max as) = metaOccurs m as
instance Occurs PlusLevel where
occurs red ctx m xs l@ClosedLevel{} = return l
occurs red ctx m xs (Plus n l) = Plus n <$> occurs red ctx m xs l
metaOccurs m ClosedLevel{} = return ()
metaOccurs m (Plus n l) = metaOccurs m l
instance Occurs LevelAtom where
occurs red ctx m xs l = do
l <- case red of
YesUnfold -> reduce l
NoUnfold -> instantiate l
case l of
MetaLevel m' args -> do
MetaV m' args <- occurs red ctx m xs (MetaV m' args)
return $ MetaLevel m' args
NeutralLevel r v -> NeutralLevel r <$> occurs red ctx m xs v
BlockedLevel m' v -> BlockedLevel m' <$> occurs red Flex m xs v
UnreducedLevel v -> UnreducedLevel <$> occurs red ctx m xs v
metaOccurs m l = do
l <- instantiate l
case l of
MetaLevel m' args -> metaOccurs m $ MetaV m' args
NeutralLevel _ v -> metaOccurs m v
BlockedLevel _ v -> metaOccurs m v
UnreducedLevel v -> metaOccurs m v
instance Occurs Type where
occurs red ctx m xs (El s v) = uncurry El <$> occurs red ctx m xs (s,v)
metaOccurs m (El s v) = metaOccurs m (s,v)
instance Occurs Sort where
occurs red ctx m xs s = do
s' <- case red of
YesUnfold -> reduce s
NoUnfold -> instantiate s
case s' of
PiSort s1 s2 -> uncurry PiSort <$> occurs red (weakly ctx) m xs (s1,s2)
Type a -> Type <$> occurs red ctx m xs a
Prop -> return s'
Inf -> return s'
SizeUniv -> return s'
UnivSort s -> UnivSort <$> occurs red (weakly ctx) m xs s
MetaS x es -> do
MetaV x es <- occurs red ctx m xs (MetaV x es)
return $ MetaS x es
metaOccurs m s = do
s <- instantiate s
case s of
PiSort s1 s2 -> metaOccurs m (s1,s2)
Type a -> metaOccurs m a
Prop -> return ()
Inf -> return ()
SizeUniv -> return ()
UnivSort s -> metaOccurs m s
MetaS x es -> metaOccurs m $ MetaV x es
instance Occurs a => Occurs (Elim' a) where
occurs red ctx m xs e@(Proj _ f) = do
frel <- relOfConst f
unless (not (unusableRelevance frel) || ctx == Irrel) $ do
reportSDoc "tc.meta.occurs" 35 $ text ("relevance of projection: " ++ show frel)
abort ctx $ MetaIrrelevantSolution m $ Def f []
return e
occurs red ctx m xs (Apply a) = Apply <$> occurs red ctx m xs a
metaOccurs m (Proj{} ) = return ()
metaOccurs m (Apply a) = metaOccurs m a
instance (Occurs a, Subst t a) => Occurs (Abs a) where
occurs red ctx m xs b@(Abs s x) = Abs s <$> underAbstraction_ b (occurs red ctx m (liftUnderAbs xs))
occurs red ctx m xs b@(NoAbs s x) = NoAbs s <$> occurs red ctx m xs x
metaOccurs m (Abs s x) = metaOccurs m x
metaOccurs m (NoAbs s x) = metaOccurs m x
instance Occurs a => Occurs (Arg a) where
occurs red ctx m xs (Arg info x) | isIrrelevant info = Arg info <$>
occurs red Irrel m (goIrrelevant xs) x
occurs red ctx m xs (Arg info x) | isNonStrict info = Arg info <$>
occurs red ctx m (goNonStrict xs) x
occurs red ctx m xs (Arg info x) = Arg info <$>
occurs red ctx m xs x
metaOccurs m a = metaOccurs m (unArg a)
instance Occurs a => Occurs (Dom a) where
occurs red ctx m xs (Dom info x) = Dom info <$> occurs red ctx m xs x
metaOccurs m = metaOccurs m . unDom
instance (Occurs a, Occurs b) => Occurs (a,b) where
occurs red ctx m xs (x,y) = (,) <$> occurs red ctx m xs x <*> occurs red ctx m xs y
metaOccurs m (x,y) = metaOccurs m x >> metaOccurs m y
instance Occurs a => Occurs [a] where
occurs red ctx m xs ys = mapM (occurs red ctx m xs) ys
metaOccurs m ys = mapM_ (metaOccurs m) ys
instance Occurs a => Occurs (Maybe a) where
occurs red ctx m mx my = traverse (occurs red ctx m mx) my
metaOccurs m = maybe (return ()) (metaOccurs m)
prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
prune m' vs xs = do
caseEitherM (runExceptT $ mapM (hasBadRigid xs) $ map unArg vs)
(const $ return PrunedNothing) $ \ kills -> do
reportSDoc "tc.meta.kill" 10 $ vcat
[ text "attempting kills"
, nest 2 $ vcat
[ text "m' =" <+> pretty m'
, text "xs =" <+> prettyList (map (prettyTCM . var) xs)
, text "vs =" <+> prettyList (map prettyTCM vs)
, text "kills =" <+> text (show kills)
]
]
killArgs kills m'
hasBadRigid :: [Nat] -> Term -> ExceptT () TCM Bool
hasBadRigid xs t = do
let failure = throwError ()
tb <- liftTCM $ reduceB t
let t = ignoreBlocking tb
case t of
Var x _ -> return $ notElem x xs
Lam _ v -> failure
DontCare v -> hasBadRigid xs v
v@(Def f es) -> ifNotM (isNeutral tb f es) failure $ do
es `rigidVarsNotContainedIn` xs
Pi a b -> (a,b) `rigidVarsNotContainedIn` xs
Level v -> v `rigidVarsNotContainedIn` xs
Sort s -> s `rigidVarsNotContainedIn` xs
Con c _ es | Just args <- allApplyElims es -> do
ifM (liftTCM $ isEtaCon (conName c))
(and <$> mapM (hasBadRigid xs . unArg) args)
failure
Con c _ es | otherwise -> failure
Lit{} -> failure
MetaV{} -> failure
isNeutral :: MonadTCM tcm => Blocked t -> QName -> Elims -> tcm Bool
isNeutral b f es = liftTCM $ do
let yes = return True
no = return False
def <- getConstInfo f
if defMatchable def then no else do
case theDef def of
AbstractDefn{} -> yes
Axiom{} -> yes
Datatype{} -> yes
Record{} -> yes
Function{} -> case b of
NotBlocked StuckOn{} _ -> yes
NotBlocked AbsurdMatch _ -> yes
_ -> no
_ -> no
rigidVarsNotContainedIn :: (MonadTCM tcm, FoldRigid a) => a -> [Nat] -> tcm Bool
rigidVarsNotContainedIn v is = liftTCM $ do
n0 <- getContextSize
let
levels = Set.fromList $ map (n0-1 -) is
test i = do
n <- getContextSize
let l = n-1 - i
forbidden = l < n0 && not (l `Set.member` levels)
when forbidden $
reportSLn "tc.meta.kill" 20 $
"found forbidden de Bruijn level " ++ show l
return $ Any forbidden
getAny <$> foldRigid test v
class FoldRigid a where
foldRigid :: (Monoid (TCM m)) => (Nat -> TCM m) -> a -> TCM m
instance FoldRigid Term where
foldRigid f t = do
b <- liftTCM $ reduceB t
case ignoreBlocking b of
Var i es -> f i `mappend` fold es
Lam _ t -> fold t
Lit{} -> mempty
Def _ es -> case b of
Blocked{} -> mempty
NotBlocked MissingClauses _ -> mempty
_ -> fold es
Con _ _ ts -> fold ts
Pi a b -> fold (a,b)
Sort s -> fold s
Level l -> fold l
MetaV{} -> mempty
DontCare{} -> mempty
where fold = foldRigid f
instance FoldRigid Type where
foldRigid f (El s t) = foldRigid f (s,t)
instance FoldRigid Sort where
foldRigid f s =
case s of
Type l -> fold l
Prop -> mempty
Inf -> mempty
SizeUniv -> mempty
PiSort s1 s2 -> fold (s1, s2)
UnivSort s -> fold s
MetaS{} -> mempty
where fold = foldRigid f
instance FoldRigid Level where
foldRigid f (Max ls) = foldRigid f ls
instance FoldRigid PlusLevel where
foldRigid f ClosedLevel{} = mempty
foldRigid f (Plus _ l) = foldRigid f l
instance FoldRigid LevelAtom where
foldRigid f l =
case l of
MetaLevel{} -> mempty
NeutralLevel MissingClauses _ -> mempty
NeutralLevel _ l -> fold l
BlockedLevel _ l -> fold l
UnreducedLevel l -> fold l
where fold = foldRigid f
instance (Subst t a, FoldRigid a) => FoldRigid (Abs a) where
foldRigid f b = underAbstraction_ b $ foldRigid f
instance FoldRigid a => FoldRigid (Arg a) where
foldRigid f a =
case getRelevance a of
Irrelevant -> mempty
_ -> foldRigid f $ unArg a
instance FoldRigid a => FoldRigid (Dom a) where
foldRigid f dom = foldRigid f $ unDom dom
instance FoldRigid a => FoldRigid (Elim' a) where
foldRigid f (Apply a) = foldRigid f a
foldRigid f Proj{} = mempty
instance FoldRigid a => FoldRigid [a] where
foldRigid f = foldMap $ foldRigid f
instance (FoldRigid a, FoldRigid b) => FoldRigid (a,b) where
foldRigid f (a,b) = foldRigid f a `mappend` foldRigid f b
data PruneResult
= NothingToPrune
| PrunedNothing
| PrunedSomething
| PrunedEverything
deriving (Eq, Show)
killArgs :: [Bool] -> MetaId -> TCM PruneResult
killArgs kills _
| not (or kills) = return NothingToPrune
killArgs kills m = do
mv <- lookupMeta m
allowAssign <- asks envAssignMetas
if mvFrozen mv == Frozen || not allowAssign then return PrunedNothing else do
let a = jMetaType $ mvJudgement mv
TelV tel b <- telView' <$> instantiateFull a
let args = zip (telToList tel) (kills ++ repeat False)
(kills', a') <- killedType args b
dbg kills' a a'
if not (any unArg kills') then return PrunedNothing else do
performKill kills' m a'
return $ if (and $ zipWith implies kills $ map unArg kills')
then PrunedEverything
else PrunedSomething
where
implies :: Bool -> Bool -> Bool
implies False _ = True
implies True x = x
dbg kills' a a' =
reportSDoc "tc.meta.kill" 10 $ vcat
[ text "after kill analysis"
, nest 2 $ vcat
[ text "metavar =" <+> prettyTCM m
, text "kills =" <+> text (show kills)
, text "kills' =" <+> text (show kills')
, text "oldType =" <+> prettyTCM a
, text "newType =" <+> prettyTCM a'
]
]
killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> TCM ([Arg Bool], Type)
killedType args b = do
let tokill = IntSet.fromList [ i | ((_, True), i) <- zip (reverse args) [0..] ]
(tokill, b) <- reallyNotFreeIn tokill b
(killed, b) <- go (reverse $ map fst args) tokill b
let kills = [ Arg (getArgInfo dom) (IntSet.member i killed)
| (i, (dom, _)) <- reverse $ zip [0..] $ reverse args ]
return (kills, b)
where
down = IntSet.map pred
up = IntSet.map succ
go :: [Dom (ArgName, Type)] -> IntSet -> Type -> TCM (IntSet, Type)
go [] xs b | IntSet.null xs = return (xs, b)
| otherwise = __IMPOSSIBLE__
go (arg : args) xs b
| IntSet.member 0 xs = do
let ys = down (IntSet.delete 0 xs)
(ys, b) <- go args ys $ strengthen __IMPOSSIBLE__ b
return (IntSet.insert 0 $ up ys, b)
| otherwise = do
let xs' = down xs
(name, a) = unDom arg
(ys, a) <- reallyNotFreeIn xs' a
(zs, b) <- go args ys (mkPi ((name, a) <$ arg) b)
return (up zs, b)
reallyNotFreeIn :: IntSet -> Type -> TCM (IntSet, Type)
reallyNotFreeIn xs a | IntSet.null xs = return (xs, a)
reallyNotFreeIn xs a = do
let fvs = freeVars a
anywhere = allVars fvs
rigid = IntSet.unions [stronglyRigidVars fvs, unguardedVars fvs]
nonrigid = IntSet.difference anywhere rigid
hasNo = IntSet.null . IntSet.intersection xs
if | hasNo nonrigid ->
return (IntSet.difference xs rigid, a)
| otherwise -> do
forceNotFree (IntSet.difference xs rigid) a
performKill
:: [Arg Bool]
-> MetaId
-> Type
-> TCM ()
performKill kills m a = do
mv <- lookupMeta m
when (mvFrozen mv == Frozen) __IMPOSSIBLE__
let n = size kills
let perm = Perm n
[ i | (i, Arg _ False) <- zip [0..] kills ]
judg = case mvJudgement mv of
HasType{} -> HasType __IMPOSSIBLE__ a
IsSort{} -> IsSort __IMPOSSIBLE__ a
m' <- newMeta (mvInfo mv) (mvPriority mv) perm judg
etaExpandMetaSafe m'
let
vars = [ Arg info (var i)
| (i, Arg info False) <- zip (downFrom n) kills ]
u = MetaV m' $ map Apply vars
tel = map ("v" <$) kills
dbg m' u
assignTerm m tel u
where
dbg m' u = reportSDoc "tc.meta.kill" 10 $ vcat
[ text "actual killing"
, nest 2 $ vcat
[ text "new meta:" <+> pretty m'
, text "kills :" <+> text (show kills)
, text "inst :" <+> pretty m <+> text ":=" <+> prettyTCM u
]
]