Agda.TypeChecking.Free.Reduce

Free variable check that reduces the subject to make certain variables not free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.

Documentation

forceNotFree :: IntSet -> Type -> TCM (IntSet, Type)

Try to enforce a set of variables not occurring in a given type. Returns a possibly reduced version of the type and the subset of variables that does indeed not occur in the reduced type.