| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Free.Reduce
Description
Free variable check that reduces the subject to make certain variables not free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.
Synopsis
- class (PrecomputeFreeVars a, Subst a) => ForceNotFree a
- forceNotFree :: (ForceNotFree a, Reduce a) => VarSet -> a -> ReduceM (IntMap IsFree, a)
- forceNoAbs :: (Reduce a, ForceNotFree a) => Dom Type -> Abs a -> ReduceM (Either (Abs a, FlexRig) a)
- forceNoAbsSort :: Dom Type -> Abs Sort -> ReduceM (Either (Abs Sort, FlexRig) Sort)
- reallyFree :: (Reduce a, ForceNotFree a) => VarSet -> a -> ReduceM (Either Blocked_ (Maybe a))
- data IsFree
- nonFreeVars :: IntMap IsFree -> VarSet
Documentation
class (PrecomputeFreeVars a, Subst a) => ForceNotFree a Source #
Minimal complete definition
forceNotFree'
Instances
forceNotFree :: (ForceNotFree a, Reduce a) => VarSet -> a -> ReduceM (IntMap IsFree, a) Source #
Try to enforce a set of variables not occurring in a given type. Returns a possibly reduced version of the type and for each of the given variables whether it is either not free, or maybe free depending on some metavariables.
forceNoAbs :: (Reduce a, ForceNotFree a) => Dom Type -> Abs a -> ReduceM (Either (Abs a, FlexRig) a) Source #
Try to force a binder to be a NoAbs by reducing the body as needed to get rid of the bound variable. Returns either the reduced abstraction and the occurrence of the variable (if removing it failed) or else the strengthened body.
forceNoAbsSort :: Dom Type -> Abs Sort -> ReduceM (Either (Abs Sort, FlexRig) Sort) Source #
András 2026-02-24: we specialize this, because TypeChecking.Reduce imports it via the hs-boot file, and if it's not specialized there, it is impossible to specialzie by GHC.
reallyFree :: (Reduce a, ForceNotFree a) => VarSet -> a -> ReduceM (Either Blocked_ (Maybe a)) Source #
Checks if the given term contains any free variables that are in the given set of variables, possibly reducing the term in the process. Returns `Right Nothing` if there are such variables, `Right (Just v')` if there are none (where v' is the possibly reduced version of the given term) or `Left b` if the problem is blocked on a meta.