| 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, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a)
- reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))
- data IsFree
Documentation
class (PrecomputeFreeVars a, Subst a) => ForceNotFree a Source #
Minimal complete definition
forceNotFree'
Instances
forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (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.
reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (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.