Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.MetaVars.Occurs

Description

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

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.

defNeedsChecking :: QName -> TCM Bool Source #

Is a def in the list of stuff to be checked?

tallyDef :: QName -> TCM () Source #

Remove a def from the list of defs to be looked at.

OccursM monad and its services

data OccursExtra Source #

Extra environment for the occurs check. (Complements FreeEnv.)

Constructors

OccursExtra 

Fields

type OccursM = ReaderT OccursCtx TCM 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.

Constructors

YesUnfold 
NoUnfold 

Instances

Instances details
Show UnfoldStrategy Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

showsPrec :: Int -> UnfoldStrategy -> ShowS

show :: UnfoldStrategy -> String

showList :: [UnfoldStrategy] -> ShowS

Eq UnfoldStrategy Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

conArgs :: Elims -> OccursM a -> OccursM a Source #

For a path constructor `c : ... -> Path D a b`, we have that e.g. `c es i0` reduces to a. So we have to consider its arguments as flexible when we do not actually unfold.

unfold :: (Instantiate t, Reduce t) => t -> OccursM t Source #

Managing rigidiy during occurs check.

weakly :: OccursM a -> OccursM a Source #

Leave the strongly rigid position.

Error throwing during occurs check.

patternViolation' :: MonadTCM m => Blocker -> Int -> String -> m a Source #

Implementation of the occurs check.

class Occurs t where Source #

Extended occurs check.

Minimal complete definition

occurs

Methods

occurs :: t -> OccursM t Source #

metaOccurs :: MetaId -> t -> TCM () Source #

default metaOccurs :: forall (f :: Type -> Type) a. (Foldable f, Occurs a, f a ~ t) => MetaId -> t -> TCM () Source #

Instances

Instances details
Occurs QName Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Clause Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Elims Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Defn Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs a => Occurs (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Arg a -> OccursM (Arg a) Source #

metaOccurs :: MetaId -> Arg a -> TCM () Source #

Occurs (Abs Term) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs (Abs Type) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs a => Occurs (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Dom a -> OccursM (Dom a) Source #

metaOccurs :: MetaId -> Dom a -> TCM () Source #

occurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t Source #

metaOccurs2 :: (Occurs a, Occurs b) => MetaId -> a -> b -> TCM () Source #

metaOccurs3 :: (Occurs a, Occurs b, Occurs c) => MetaId -> a -> b -> c -> TCM () Source #

occursCheck :: MetaId -> VarMap -> Term -> TCM Term 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.

prune Source #

Arguments

:: (PureTCM m, 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.

hasBadRigid Source #

Arguments

:: forall (m :: Type -> Type). PureTCM 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 non-eliminateable 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 #

Arguments

:: (PureTCM 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.

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> a -> tcm Bool Source #

Instances

Instances details
AnyRigid Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Level -> tcm Bool Source #

AnyRigid PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> PlusLevel -> tcm Bool Source #

AnyRigid Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Sort -> tcm Bool Source #

AnyRigid Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Term -> tcm Bool Source #

AnyRigid Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Type -> tcm Bool Source #

AnyRigid a => AnyRigid (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Arg a -> tcm Bool Source #

(Subst a, AnyRigid a) => AnyRigid (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Abs a -> tcm Bool Source #

AnyRigid a => AnyRigid (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Dom a -> tcm Bool Source #

AnyRigid a => AnyRigid (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Elim' a -> tcm Bool Source #

AnyRigid a => AnyRigid [a] Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> [a] -> tcm Bool Source #

(AnyRigid a, AnyRigid b) => AnyRigid (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> (a, b) -> tcm Bool Source #

data PruneResult Source #

Constructors

NothingToPrune

the kill list is empty or only Falses

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

Instances details
Show PruneResult Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

showsPrec :: Int -> PruneResult -> ShowS

show :: PruneResult -> String

showList :: [PruneResult] -> ShowS

Eq PruneResult Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

(==) :: PruneResult -> PruneResult -> Bool

(/=) :: PruneResult -> PruneResult -> Bool

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 ith 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 #

performKill Source #

Arguments

:: MonadMetaSolver m 
=> [Arg Bool]

Arguments to old meta var in left to right order with Bool indicating whether they can be pruned.

-> 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 # 
Instance details