{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.MetaVars.Occurs where
import Control.Monad
import Control.Monad.Reader
import Data.Foldable (traverse_)
import Data.Functor
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
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.Constraints ()
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
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
import Agda.Utils.Impossible
modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs f = stOccursCheckDefs `modifyTCLens` 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 <- asksTC 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 <$> useTC stOccursCheckDefs
tallyDef :: QName -> TCM ()
tallyDef d = modifyOccursCheckDefs $ Set.delete d
data OccursExtra = OccursExtra
{ occUnfold :: UnfoldStrategy
, occVars :: VarMap
, occMeta :: MetaId
, occCxtSize :: Nat
}
type OccursCtx = FreeEnv' () OccursExtra AllowedVar
type OccursM = ReaderT OccursCtx TCM
type AllowedVar = Modality -> All
instance IsVarSet () AllowedVar where
withVarOcc o f = f . composeModality (getModality o)
variableCheck :: VarMap -> Maybe Variable -> AllowedVar
variableCheck xs mi q = All $
caseMaybe mi True $ \ i ->
caseMaybe (lookupVarMap i xs) False $ \ o ->
getModality o `moreUsableModality` q
definitionCheck :: QName -> OccursM ()
definitionCheck d = do
cxt <- ask
let irr = isIrrelevant cxt
er = hasQuantity0 cxt
m = occMeta $ feExtra cxt
unless (irr && er) $ do
dmod <- modalityOfConst d
unless (irr || usableRelevance dmod) $ do
reportSDoc "tc.meta.occurs" 35 $ hsep
[ "occursCheck: definition"
, prettyTCM d
, "has relevance"
, prettyTCM (getRelevance dmod)
]
abort $ MetaIrrelevantSolution m $ Def d []
unless (er || usableQuantity dmod) $ do
reportSDoc "tc.meta.occurs" 35 $ hsep
[ "occursCheck: definition"
, prettyTCM d
, "has quantity"
, prettyTCM (getQuantity dmod)
]
abort $ MetaErasedSolution m $ Def d []
allowedVars :: OccursM (Nat -> Bool)
allowedVars = do
n <- liftM2 (-) getContextSize (asks (occCxtSize . feExtra))
xs <- IntMap.keysSet . theVarMap <$> asks (occVars . feExtra)
return $ \ i -> i < n || (i - n) `IntSet.member` xs
data UnfoldStrategy = YesUnfold | NoUnfold
deriving (Eq, Show)
defArgs :: OccursM a -> OccursM a
defArgs m = asks (occUnfold . feExtra) >>= \case
NoUnfold -> flexibly m
YesUnfold -> weakly m
unfoldB :: (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
unfoldB v = do
unfold <- asks $ occUnfold . feExtra
rel <- asks feModality
case unfold of
YesUnfold | not (isIrrelevant rel) -> reduceB v
_ -> notBlocked <$> instantiate v
unfold :: (Instantiate t, Reduce t) => t -> OccursM t
unfold v = asks (occUnfold . feExtra) >>= \case
NoUnfold -> instantiate v
YesUnfold -> reduce v
weakly :: OccursM a -> OccursM a
weakly = local $ over lensFlexRig $ composeFlexRig WeaklyRigid
strongly :: OccursM a -> OccursM a
strongly = local $ over lensFlexRig $ \case
WeaklyRigid -> StronglyRigid
Unguarded -> StronglyRigid
ctx -> ctx
flexibly :: OccursM a -> OccursM a
flexibly = local $ set lensFlexRig $ Flexible ()
patternViolation' :: MonadTCM m => Int -> String -> m a
patternViolation' n err = liftTCM $ do
reportSLn "tc.meta.occurs" n err
patternViolation
abort :: TypeError -> OccursM a
abort err = do
ctx <- ask
lift $ do
if | isIrrelevant ctx -> soft
| StronglyRigid <- ctx ^. lensFlexRig -> hard
| otherwise -> soft
where
hard = typeError err
soft = patternViolation' 70 (show err)
class Occurs t where
occurs :: t -> OccursM t
metaOccurs :: MetaId -> t -> TCM ()
default occurs :: (Traversable f, Occurs a, f a ~ t) => t -> OccursM t
occurs = traverse occurs
default metaOccurs :: (Foldable f, Occurs a, f a ~ t) => MetaId -> t -> TCM ()
metaOccurs = traverse_ . metaOccurs
occursCheck
:: (Occurs a, InstantiateFull a, PrettyTCM a)
=> MetaId -> VarMap -> a -> TCM a
occursCheck m xs v = Bench.billTo [ Bench.Typing, Bench.OccursCheck ] $ do
mv <- lookupMeta m
n <- getContextSize
let initEnv unf = FreeEnv
{ feExtra = OccursExtra
{ occUnfold = unf
, occVars = xs
, occMeta = m
, occCxtSize = n
}
, feFlexRig = StronglyRigid
, feModality = getMetaModality mv
, feSingleton = variableCheck xs
}
initOccursCheck mv
nicerErrorMessage $ do
(occurs v `runReaderT` initEnv NoUnfold) `catchError` \err -> do
case err of
PatternErr{} | not (isIrrelevant $ getMetaModality mv) -> do
initOccursCheck mv
occurs v `runReaderT` initEnv YesUnfold
_ -> throwError err
where
nicerErrorMessage :: TCM a -> TCM a
nicerErrorMessage f = f `catchError` \ err -> case err of
TypeError _ cl -> case clValue cl of
MetaOccursInItself{} ->
typeError . GenericDocError =<<
fsep [ text ("Refuse to construct infinite term by instantiating " ++ prettyShow m ++ " to")
, prettyTCM =<< instantiateFull v
]
MetaCannotDependOn _ i ->
ifM (isSortMeta m `and2M` (not <$> hasUniversePolymorphism))
( typeError . GenericDocError =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to")
, prettyTCM v
, "since universe polymorphism is disabled"
]
)
( typeError . GenericDocError =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to solution")
, prettyTCM v
, "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 . GenericDocError =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to solution")
, prettyTCM v
, "since (part of) the solution was created in an irrelevant context"
]
MetaErasedSolution _ _ ->
typeError . GenericDocError =<<
fsep [ text ("Cannot instantiate the metavariable " ++ prettyShow m ++ " to solution")
, prettyTCM v
, "since (part of) the solution was created in an erased context"
]
_ -> throwError err
_ -> throwError err
instance Occurs Term where
occurs v = do
vb <- unfoldB v
let flexIfBlocked = case vb of
Blocked{} -> flexibly
NotBlocked{blockingStatus = Underapplied} -> flexibly
NotBlocked{} -> id
v <- return $ ignoreBlocking vb
flexIfBlocked $ do
ctx <- ask
let m = occMeta . feExtra $ ctx
reportSDoc "tc.meta.occurs" 45 $
text ("occursCheck " ++ prettyShow m ++ " (" ++ show (feFlexRig ctx) ++ ") of ") <+> prettyTCM v
reportSDoc "tc.meta.occurs" 70 $
nest 2 $ text $ show v
case v of
Var i es -> do
allowed <- getAll . ($ mempty) <$> variable i
if allowed then Var i <$> weakly (occurs es) else do
reportSDoc "tc.meta.occurs" 35 $ "offending variable: " <+> prettyTCM (var i)
t <- typeOfBV i
reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "of type " <+> prettyTCM t
isST <- isSingletonType t
reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "(after singleton test)"
case isST of
Left mid -> patternViolation' 70 $ "Disallowed var " ++ show i ++ " not obviously singleton"
Right Nothing ->
strongly $ abort $ MetaCannotDependOn m i
Right (Just sv) -> return $ sv `applyE` es
Lam h f -> Lam h <$> occurs f
Level l -> Level <$> occurs l
Lit l -> return v
Dummy{} -> return v
DontCare v -> dontCare <$> do underRelevance Irrelevant $ occurs v
Def d es -> do
definitionCheck d
Def d <$> occDef d es
Con c ci vs -> Con c ci <$> occurs vs
Pi a b -> uncurry Pi <$> occurs (a,b)
Sort s -> Sort <$> do underRelevance NonStrict $ occurs s
MetaV m' es -> do
when (m == m') $ patternViolation' 50 $ "occursCheck failed: Found " ++ prettyShow m
(MetaV m' <$> do flexibly $ occurs es) `catchError` \ err -> do
ctx <- ask
reportSDoc "tc.meta.kill" 25 $ vcat
[ text $ "error during flexible occurs check, we are " ++ show (ctx ^. lensFlexRig)
, text $ show err
]
case err of
PatternErr{} | not (isFlexible ctx) -> do
reportSLn "tc.meta.kill" 20 $
"oops, pattern violation for " ++ prettyShow m'
caseMaybe (allApplyElims es) (throwError err) $ \ vs -> do
killResult <- lift . prune m' vs =<< allowedVars
if (killResult == PrunedEverything)
then occurs =<< instantiate (MetaV m' es)
else throwError err
_ -> throwError err
where
occDef d vs = do
m <- asks (occMeta . feExtra)
lift $ metaOccurs m d
ifM (liftTCM $ isJust <$> isDataOrRecordType d)
(occurs vs)
(defArgs $ occurs 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 ()
Dummy{} -> 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 d = __IMPOSSIBLE__
metaOccurs m d = whenM (defNeedsChecking d) $ do
tallyDef d
reportSLn "tc.meta.occurs" 30 $ "Checking for occurrences in " ++ show d
metaOccursQName m d
metaOccursQName :: MetaId -> QName -> TCM ()
metaOccursQName m x = metaOccurs m . theDef =<< do
ignoreAbstractMode $ getConstInfo x
instance Occurs Defn where
occurs def = __IMPOSSIBLE__
metaOccurs m Axiom{} = return ()
metaOccurs m DataOrRecSig{} = return ()
metaOccurs m Function{ funClauses = cls } = metaOccurs m cls
metaOccurs m Datatype{ dataCons = cs } = mapM_ (metaOccursQName m) cs
metaOccurs m Record{ recConHead = c } = metaOccursQName m $ conName c
metaOccurs m Constructor{} = return ()
metaOccurs m Primitive{} = return ()
metaOccurs m AbstractDefn{} = __IMPOSSIBLE__
metaOccurs m GeneralizableVar{} = __IMPOSSIBLE__
instance Occurs Clause where
occurs cl = __IMPOSSIBLE__
metaOccurs m = metaOccurs m . clauseBody
instance Occurs Level where
occurs (Max n as) = Max n <$> occurs as
metaOccurs m (Max _ as) = metaOccurs m as
instance Occurs PlusLevel where
occurs (Plus n l) = Plus n <$> occurs l
metaOccurs m (Plus n l) = metaOccurs m l
instance Occurs LevelAtom where
occurs l = do
unfold l >>= \case
MetaLevel m' args -> do
MetaV m' args <- occurs (MetaV m' args)
return $ MetaLevel m' args
NeutralLevel r v -> NeutralLevel r <$> occurs v
BlockedLevel m' v -> BlockedLevel m' <$> do flexibly $ occurs v
UnreducedLevel v -> UnreducedLevel <$> occurs 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 (El s v) = uncurry El <$> occurs (s,v)
metaOccurs m (El s v) = metaOccurs m (s,v)
instance Occurs Sort where
occurs s = do
unfold s >>= \case
PiSort a s2 -> do
s1' <- flexibly $ occurs $ getSort a
a' <- (a $>) . El s1' <$> do flexibly $ occurs $ unEl $ unDom a
s2' <- mapAbstraction a' (flexibly . occurs) s2
return $ PiSort a' s2'
Type a -> Type <$> occurs a
Prop a -> Prop <$> occurs a
s@Inf -> return s
s@SizeUniv -> return s
UnivSort s -> UnivSort <$> do flexibly $ occurs s
MetaS x es -> do
MetaV x es <- occurs (MetaV x es)
return $ MetaS x es
DefS x es -> do
Def x es <- occurs (Def x es)
return $ DefS x es
DummyS{} -> return s
metaOccurs m s = do
s <- instantiate s
case s of
PiSort a s -> metaOccurs m (a,s)
Type a -> metaOccurs m a
Prop a -> metaOccurs m a
Inf -> return ()
SizeUniv -> return ()
UnivSort s -> metaOccurs m s
MetaS x es -> metaOccurs m $ MetaV x es
DefS d es -> metaOccurs m $ Def d es
DummyS{} -> return ()
instance Occurs a => Occurs (Elim' a) where
occurs e@(Proj _ f) = e <$ definitionCheck f
occurs (Apply a) = Apply <$> occurs a
occurs (IApply x y a) = IApply <$> occurs x <*> occurs y <*> occurs a
metaOccurs m (Proj{} ) = return ()
metaOccurs m (Apply a) = metaOccurs m a
metaOccurs m (IApply x y a) = metaOccurs m (x,(y,a))
instance (Occurs a, Subst t a) => Occurs (Abs a) where
occurs b@(Abs s _) = Abs s <$> do underAbstraction_ b $ underBinder . occurs
occurs (NoAbs s x) = NoAbs s <$> occurs x
metaOccurs m (Abs _ x) = metaOccurs m x
metaOccurs m (NoAbs _ x) = metaOccurs m x
instance Occurs a => Occurs (Arg a) where
occurs (Arg info v) = Arg info <$> do underModality info $ occurs v
metaOccurs m = metaOccurs m . unArg
instance Occurs a => Occurs (Dom a) where
instance Occurs a => Occurs [a] where
instance Occurs a => Occurs (Maybe a) where
instance (Occurs a, Occurs b) => Occurs (a,b) where
occurs (x,y) = (,) <$> occurs x <*> occurs y
metaOccurs m (x,y) = metaOccurs m x >> metaOccurs m y
prune
:: MonadMetaSolver m
=> MetaId
-> Args
-> (Nat -> Bool)
-> m 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
[ "attempting kills"
, nest 2 $ vcat
[ "m' =" <+> pretty m'
, "vs =" <+> prettyList (map prettyTCM vs)
, "kills =" <+> text (show kills)
]
]
killArgs kills m'
hasBadRigid
:: (MonadReduce m, HasConstInfo m, MonadAddContext m)
=> (Nat -> Bool)
-> Term
-> ExceptT () m Bool
hasBadRigid xs t = do
let failure = throwError ()
tb <- reduceB t
let t = ignoreBlocking tb
case t of
Var x _ -> return $ not $ xs x
Lam _ v -> failure
DontCare v -> hasBadRigid xs v
v@(Def f es) -> ifNotM (isNeutral tb f es) failure $ do
lift $ es `rigidVarsNotContainedIn` xs
Pi a b -> lift $ (a,b) `rigidVarsNotContainedIn` xs
Level v -> lift $ v `rigidVarsNotContainedIn` xs
Sort s -> lift $ s `rigidVarsNotContainedIn` xs
Con c _ es | Just args <- allApplyElims es -> do
ifM (isEtaCon (conName c))
(and <$> mapM (hasBadRigid xs . unArg) args)
failure
Con c _ es | otherwise -> failure
Lit{} -> failure
MetaV{} -> failure
Dummy{} -> return False
isNeutral :: (HasConstInfo m) => Blocked t -> QName -> Elims -> m Bool
isNeutral b f es = do
let yes = return True
no = return False
def <- getConstInfo f
if not (null $ 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
GeneralizableVar{} -> __IMPOSSIBLE__
_ -> no
rigidVarsNotContainedIn
:: (MonadReduce m, MonadAddContext m, MonadTCEnv m, MonadDebug m, AnyRigid a)
=> a
-> (Nat -> Bool)
-> m Bool
rigidVarsNotContainedIn v is = do
n0 <- getContextSize
let
levels = is . (n0-1 -)
test i = do
n <- getContextSize
let l = n-1 - i
forbidden = l < n0 && not (levels l)
when forbidden $
reportSLn "tc.meta.kill" 20 $
"found forbidden de Bruijn level " ++ show l
return forbidden
anyRigid test v
class AnyRigid a where
anyRigid :: (MonadReduce tcm, MonadAddContext tcm)
=> (Nat -> tcm Bool) -> a -> tcm Bool
instance AnyRigid Term where
anyRigid f t = do
b <- reduceB t
case ignoreBlocking b of
Var i es -> f i `or2M` anyRigid f es
Lam _ t -> anyRigid f t
Lit{} -> return False
Def _ es -> case b of
Blocked{} -> return False
NotBlocked MissingClauses _ -> return False
_ -> anyRigid f es
Con _ _ ts -> anyRigid f ts
Pi a b -> anyRigid f (a,b)
Sort s -> anyRigid f s
Level l -> anyRigid f l
MetaV{} -> return False
DontCare{} -> return False
Dummy{} -> return False
instance AnyRigid Type where
anyRigid f (El s t) = anyRigid f (s,t)
instance AnyRigid Sort where
anyRigid f s =
case s of
Type l -> anyRigid f l
Prop l -> anyRigid f l
Inf -> return False
SizeUniv -> return False
PiSort a s -> return False
UnivSort s -> anyRigid f s
MetaS{} -> return False
DefS{} -> return False
DummyS{} -> return False
instance AnyRigid Level where
anyRigid f (Max _ ls) = anyRigid f ls
instance AnyRigid PlusLevel where
anyRigid f (Plus _ l) = anyRigid f l
instance AnyRigid LevelAtom where
anyRigid f l =
case l of
MetaLevel{} -> return False
NeutralLevel MissingClauses _ -> return False
NeutralLevel _ l -> anyRigid f l
BlockedLevel _ l -> anyRigid f l
UnreducedLevel l -> anyRigid f l
instance (Subst t a, AnyRigid a) => AnyRigid (Abs a) where
anyRigid f b = underAbstraction_ b $ anyRigid f
instance AnyRigid a => AnyRigid (Arg a) where
anyRigid f a =
case getRelevance a of
Irrelevant -> return False
_ -> anyRigid f $ unArg a
instance AnyRigid a => AnyRigid (Dom a) where
anyRigid f dom = anyRigid f $ unDom dom
instance AnyRigid a => AnyRigid (Elim' a) where
anyRigid f (Apply a) = anyRigid f a
anyRigid f (IApply x y a) = anyRigid f (x,(y,a))
anyRigid f Proj{} = return False
instance AnyRigid a => AnyRigid [a] where
anyRigid f xs = anyM xs $ anyRigid f
instance (AnyRigid a, AnyRigid b) => AnyRigid (a,b) where
anyRigid f (a,b) = anyRigid f a `or2M` anyRigid f b
data PruneResult
= NothingToPrune
| PrunedNothing
| PrunedSomething
| PrunedEverything
deriving (Eq, Show)
killArgs :: (MonadMetaSolver m) => [Bool] -> MetaId -> m PruneResult
killArgs kills _
| not (or kills) = return NothingToPrune
killArgs kills m = do
mv <- lookupMeta m
allowAssign <- asksTC 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
addContext tel $ 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
[ "after kill analysis"
, nest 2 $ vcat
[ "metavar =" <+> prettyTCM m
, "kills =" <+> text (show kills)
, "kills' =" <+> prettyList (map prettyTCM kills')
, "oldType =" <+> prettyTCM a
, "newType =" <+> prettyTCM a'
]
]
killedType :: (MonadReduce m) => [(Dom (ArgName, Type), Bool)] -> Type -> m ([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 :: (MonadReduce m) => [Dom (ArgName, Type)] -> IntSet -> Type -> m (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 :: (MonadReduce m) => IntSet -> Type -> m (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
(fvs , a) <- forceNotFree (IntSet.difference xs rigid) a
let xs = IntMap.keysSet $ IntMap.filter (== NotFree) fvs
return (xs , a)
performKill
:: MonadMetaSolver m
=> [Arg Bool]
-> MetaId
-> Type
-> m ()
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 ]
oldPerm = liftP (max 0 $ n - m) p
where p = mvPermutation mv
m = size p
judg = case mvJudgement mv of
HasType{ jComparison = cmp } -> HasType __IMPOSSIBLE__ cmp a
IsSort{} -> IsSort __IMPOSSIBLE__ a
m' <- newMeta Instantiable (mvInfo mv) (mvPriority mv) (composeP perm oldPerm) 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
[ "actual killing"
, nest 2 $ vcat
[ "new meta:" <+> pretty m'
, "kills :" <+> prettyList_ (map (text . show . unArg) kills)
, "inst :" <+> pretty m <+> ":=" <+> prettyTCM u
]
]