Safe Haskell  None 

Language  Haskell2010 
The occurs check for unification. Does pruning on the fly.
When hitting a meta variable:
 Compute flex/rigid for its arguments.
 Compare to allowed variables.
 Mark arguments with rigid occurrences of disallowed variables for deletion.
 Attempt to delete marked arguments.
 We don't need to check for success, we can just continue occurs checking.
Synopsis
 modifyOccursCheckDefs :: (Set QName > Set QName) > TCM ()
 initOccursCheck :: MetaVariable > TCM ()
 defNeedsChecking :: QName > TCM Bool
 tallyDef :: QName > TCM ()
 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
 variableCheck :: VarMap > Maybe Variable > AllowedVar
 definitionCheck :: QName > OccursM ()
 allowedVars :: OccursM (Nat > Bool)
 data UnfoldStrategy
 defArgs :: OccursM a > OccursM a
 unfoldB :: (Instantiate t, Reduce t) => t > OccursM (Blocked t)
 unfold :: (Instantiate t, Reduce t) => t > OccursM t
 weakly :: OccursM a > OccursM a
 strongly :: OccursM a > OccursM a
 flexibly :: OccursM a > OccursM a
 patternViolation' :: MonadTCM m => Int > String > m a
 abort :: TypeError > OccursM a
 class Occurs t where
 occurs :: t > OccursM t
 metaOccurs :: MetaId > t > TCM ()
 occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId > VarMap > a > TCM a
 metaOccursQName :: MetaId > QName > TCM ()
 prune :: MonadMetaSolver m => MetaId > Args > (Nat > Bool) > m PruneResult
 hasBadRigid :: (MonadReduce m, HasConstInfo m, MonadAddContext m) => (Nat > Bool) > Term > ExceptT () m Bool
 isNeutral :: HasConstInfo m => Blocked t > QName > Elims > m Bool
 rigidVarsNotContainedIn :: (MonadReduce m, MonadAddContext m, MonadTCEnv m, MonadDebug m, AnyRigid a) => a > (Nat > Bool) > m Bool
 class AnyRigid a where
 anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat > tcm Bool) > a > tcm Bool
 data PruneResult
 killArgs :: MonadMetaSolver m => [Bool] > MetaId > m PruneResult
 killedType :: MonadReduce m => [(Dom (ArgName, Type), Bool)] > Type > m ([Arg Bool], Type)
 reallyNotFreeIn :: MonadReduce m => IntSet > Type > m (IntSet, Type)
 performKill :: MonadMetaSolver m => [Arg Bool] > MetaId > Type > m ()
MetaOccursCheck: going into definitions to exclude cyclic solutions
initOccursCheck :: MetaVariable > TCM () Source #
Set the names of definitions to be looked at to the defs in the current mutual block.
OccursM monad and its services
data OccursExtra Source #
Extra environment for the occurs check. (Complements FreeEnv'
.)
OccursExtra  

type OccursCtx = FreeEnv' () OccursExtra AllowedVar Source #
Modality handling.
type AllowedVar = Modality > All Source #
The passed modality is the one of the current context.
variableCheck :: VarMap > Maybe Variable > AllowedVar Source #
Check whether a free variable is allowed in the context as specified by the modality.
definitionCheck :: QName > OccursM () Source #
Occurs check fails if a defined name is not available since it was declared in irrelevant or erased context.
allowedVars :: OccursM (Nat > Bool) Source #
Construct a test whether a de Bruijn index is allowed or needs to be pruned.
Unfolding during occurs check.
data UnfoldStrategy Source #
Unfold definitions during occurs check? This effectively runs the occurs check on the normal form.
Instances
Eq UnfoldStrategy Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs (==) :: UnfoldStrategy > UnfoldStrategy > Bool # (/=) :: UnfoldStrategy > UnfoldStrategy > Bool #  
Show UnfoldStrategy Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs showsPrec :: Int > UnfoldStrategy > ShowS # show :: UnfoldStrategy > String # showList :: [UnfoldStrategy] > ShowS # 
Managing rigidiy during occurs check.
Error throwing during occurs check.
Implementation of the occurs check.
Extended occurs check.
Nothing
occurs :: t > OccursM t Source #
metaOccurs :: MetaId > t > TCM () Source #
occurs :: (Traversable f, Occurs a, f a ~ t) => t > OccursM t Source #
metaOccurs :: (Foldable f, Occurs a, f a ~ t) => MetaId > t > TCM () Source #
Instances
Occurs QName Source #  
Occurs Clause Source #  
Occurs LevelAtom Source #  
Occurs PlusLevel Source #  
Occurs Level Source #  
Occurs Sort Source #  
Occurs Type Source #  
Occurs Term Source #  
Occurs Defn Source #  
Occurs a => Occurs [a] Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs  
Occurs a => Occurs (Maybe a) Source #  
Occurs a => Occurs (Arg a) Source #  
(Occurs a, Subst t a) => Occurs (Abs a) Source #  
Occurs a => Occurs (Elim' a) Source #  
Occurs a => Occurs (Dom a) Source #  
(Occurs a, Occurs b) => Occurs (a, b) Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs 
occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId > VarMap > a > TCM a Source #
When assigning m xs := v
, check that m
does not occur in v
and that the free variables of v
are contained in xs
.
Pruning: getting rid of flexible occurrences.
:: MonadMetaSolver m  
=> MetaId  Meta to prune. 
> Args  Arguments to meta variable. 
> (Nat > Bool)  Test for allowed variable (de Bruijn index). 
> m PruneResult 
prune m' vs xs
attempts to remove all arguments from vs
whose
free variables are not contained in xs
.
If successful, m'
is solved by the new, pruned meta variable and we
return True
else False
.
Issue 1147:
If any of the meta args vs
is matchable, e.g., is a constructor term,
we cannot prune, because the offending variables could be removed by
reduction for a suitable instantiation of the meta variable.
:: (MonadReduce m, HasConstInfo m, MonadAddContext m)  
=> (Nat > Bool)  Test for allowed variable (de Bruijn index). 
> Term  Argument of meta variable. 
> ExceptT () m Bool  Exception if argument is matchable. 
hasBadRigid xs v = Just True
iff one of the rigid variables in v
is not in xs
.
Actually we can only prune if a bad variable is in the head. See issue 458.
Or in a noneliminateable position (see succeed/PruningNonMillerPattern).
hasBadRigid xs v = Nothing
means that
we cannot prune at all as one of the meta args is matchable.
(See issue 1147.)
isNeutral :: HasConstInfo m => Blocked t > QName > Elims > m Bool Source #
Check whether a term Def f es
is finally stuck.
Currently, we give only a crude approximation.
rigidVarsNotContainedIn Source #
:: (MonadReduce m, MonadAddContext m, MonadTCEnv m, MonadDebug m, AnyRigid a)  
=> a  
> (Nat > Bool)  Test for allowed variable (de Bruijn index). 
> m Bool 
Check whether any of the variables (given as de Bruijn indices) occurs *definitely* in the term in a rigid position. Reduces the term successively to remove variables in dead subterms. This fixes issue 1386.
class AnyRigid a where Source #
Collect the *definitely* rigid variables in a monoid. We need to successively reduce the expression to do this.
anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat > tcm Bool) > a > tcm Bool Source #
Instances
data PruneResult Source #
NothingToPrune  the kill list is empty or only 
PrunedNothing  there is no possible kill (because of type dep.) 
PrunedSomething  managed to kill some args in the list 
PrunedEverything  all prescribed kills where performed 
Instances
Eq PruneResult Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs (==) :: PruneResult > PruneResult > Bool # (/=) :: PruneResult > PruneResult > Bool #  
Show PruneResult Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs showsPrec :: Int > PruneResult > ShowS # show :: PruneResult > String # showList :: [PruneResult] > ShowS # 
killArgs :: MonadMetaSolver m => [Bool] > MetaId > m PruneResult Source #
killArgs [k1,...,kn] X
prunes argument i
from metavar X
if ki==True
.
Pruning is carried out whenever > 0 arguments can be pruned.
killedType :: MonadReduce m => [(Dom (ArgName, Type), Bool)] > Type > m ([Arg Bool], Type) Source #
killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')
(ignoring Dom
). Let t' = (xs:as) > b
.
Invariant: k'i == True
iff ki == True
and pruning the i
th argument from
type b
is possible without creating unbound variables.
t'
is type t
after pruning all k'i==True
.
reallyNotFreeIn :: MonadReduce m => IntSet > Type > m (IntSet, Type) Source #
:: MonadMetaSolver m  
=> [Arg Bool]  Arguments to old meta var in left to right order
with 
> MetaId  The old meta var to receive pruning. 
> Type  The pruned type of the new meta var. 
> m () 
Instantiate a meta variable with a new one that only takes the arguments which are not pruneable.
Orphan instances
IsVarSet () AllowedVar Source #  
withVarOcc :: VarOcc' () > AllowedVar > AllowedVar Source # 