<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.TypeChecking.MetaVars.Occurs</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-TypeChecking-MetaVars-Occurs.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-MetaVars-Occurs.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.TypeChecking.MetaVars.Occurs</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Getting rid of flexible occurrences
</a></li></ul></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><a href="#v:modifyOccursCheckDefs">modifyOccursCheckDefs</a> :: (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:initOccursCheck">initOccursCheck</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MetaVariable">MetaVariable</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:defNeedsChecking">defNeedsChecking</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:tallyDef">tallyDef</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:OccursCtx">OccursCtx</a> <ul class="subs"><li>= <a href="#v:Flex">Flex</a> </li><li>| <a href="#v:Rigid">Rigid</a> </li><li>| <a href="#v:StronglyRigid">StronglyRigid</a> </li><li>| <a href="#v:Top">Top</a> </li><li>| <a href="#v:Irrel">Irrel</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:UnfoldStrategy">UnfoldStrategy</a> <ul class="subs"><li>= <a href="#v:YesUnfold">YesUnfold</a> </li><li>| <a href="#v:NoUnfold">NoUnfold</a> </li></ul></li><li class="src short"><a href="#v:defArgs">defArgs</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a></li><li class="src short"><a href="#v:unfold">unfold</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Syntax-Internal.html#t:Blocked">Blocked</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)</li><li class="src short"><a href="#v:leaveTop">leaveTop</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a></li><li class="src short"><a href="#v:weakly">weakly</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a></li><li class="src short"><a href="#v:strongly">strongly</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a></li><li class="src short"><a href="#v:abort">abort</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TypeError">TypeError</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><span class="keyword">type</span> <a href="#t:Vars">Vars</a> = ([<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>], [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>])</li><li class="src short"><a href="#v:goIrrelevant">goIrrelevant</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a></li><li class="src short"><a href="#v:allowedVar">allowedVar</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:takeRelevant">takeRelevant</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>]</li><li class="src short"><a href="#v:liftUnderAbs">liftUnderAbs</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a></li><li class="src short"><span class="keyword">class</span> <a href="#t:Occurs">Occurs</a> t <span class="keyword">where</span><ul class="subs"><li><a href="#v:occurs">occurs</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> t -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> t</li><li><a href="#v:metaOccurs">metaOccurs</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> t -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li></ul></li><li class="src short"><a href="#v:occursCheck">occursCheck</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:prune">prune</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">PruneResult</a></li><li class="src short"><a href="#v:hasBadRigid">hasBadRigid</a> :: [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>] -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:rigidVarsNotContainedIn">rigidVarsNotContainedIn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => a -> [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:PruneResult">PruneResult</a> <ul class="subs"><li>= <a href="#v:NothingToPrune">NothingToPrune</a> </li><li>| <a href="#v:PrunedNothing">PrunedNothing</a> </li><li>| <a href="#v:PrunedSomething">PrunedSomething</a> </li><li>| <a href="#v:PrunedEverything">PrunedEverything</a> </li></ul></li><li class="src short"><a href="#v:killArgs">killArgs</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>] -> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">PruneResult</a></li><li class="src short"><a href="#v:killedType">killedType</a> :: [(<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>), <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>)] -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> ([<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>], <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)</li><li class="src short"><a href="#v:performKill">performKill</a> :: [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>] -> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:modifyOccursCheckDefs" class="def">modifyOccursCheckDefs</a> :: (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#modifyOccursCheckDefs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:initOccursCheck" class="def">initOccursCheck</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MetaVariable">MetaVariable</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#initOccursCheck" class="link">Source</a></p><div class="doc"><p>Set the names of definitions to be looked at
to the defs in the current mutual block.
</p></div></div><div class="top"><p class="src"><a name="v:defNeedsChecking" class="def">defNeedsChecking</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#defNeedsChecking" class="link">Source</a></p><div class="doc"><p>Is a def in the list of stuff to be checked?
</p></div></div><div class="top"><p class="src"><a name="v:tallyDef" class="def">tallyDef</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#tallyDef" class="link">Source</a></p><div class="doc"><p>Remove a def from the list of defs to be looked at.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:OccursCtx" class="def">OccursCtx</a> <a href="src/Agda-TypeChecking-MetaVars-Occurs.html#OccursCtx" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Flex" class="def">Flex</a></td><td class="doc"><p>we are in arguments of a meta
</p></td></tr><tr><td class="src"><a name="v:Rigid" class="def">Rigid</a></td><td class="doc"><p>we are not in arguments of a meta but a bound var
</p></td></tr><tr><td class="src"><a name="v:StronglyRigid" class="def">StronglyRigid</a></td><td class="doc"><p>we are at the start or in the arguments of a constructor
</p></td></tr><tr><td class="src"><a name="v:Top" class="def">Top</a></td><td class="doc"><p>we are at the term root (this turns into <code>StronglyRigid</code>)
</p></td></tr><tr><td class="src"><a name="v:Irrel" class="def">Irrel</a></td><td class="doc"><p>we are in an irrelevant argument
</p></td></tr></table></div><div class="subs instances"><p id="control.i:OccursCtx" class="caption collapser" onclick="toggleSection('i:OccursCtx')">Instances</p><div id="section.i:OccursCtx" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:UnfoldStrategy" class="def">UnfoldStrategy</a> <a href="src/Agda-TypeChecking-MetaVars-Occurs.html#UnfoldStrategy" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:YesUnfold" class="def">YesUnfold</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:NoUnfold" class="def">NoUnfold</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:UnfoldStrategy" class="caption collapser" onclick="toggleSection('i:UnfoldStrategy')">Instances</p><div id="section.i:UnfoldStrategy" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:defArgs" class="def">defArgs</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#defArgs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:unfold" class="def">unfold</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Syntax-Internal.html#t:Blocked">Blocked</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)<a href="src/Agda-TypeChecking-MetaVars-Occurs.html#unfold" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:leaveTop" class="def">leaveTop</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#leaveTop" class="link">Source</a></p><div class="doc"><p>Leave the top position.
</p></div></div><div class="top"><p class="src"><a name="v:weakly" class="def">weakly</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#weakly" class="link">Source</a></p><div class="doc"><p>Leave the strongly rigid position.
</p></div></div><div class="top"><p class="src"><a name="v:strongly" class="def">strongly</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#strongly" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:abort" class="def">abort</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TypeError">TypeError</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-MetaVars-Occurs.html#abort" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Vars" class="def">Vars</a> = ([<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>], [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>])<a href="src/Agda-TypeChecking-MetaVars-Occurs.html#Vars" class="link">Source</a></p><div class="doc"><p>Distinguish relevant and irrelevant variables in occurs check.
</p></div></div><div class="top"><p class="src"><a name="v:goIrrelevant" class="def">goIrrelevant</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#goIrrelevant" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:allowedVar" class="def">allowedVar</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#allowedVar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:takeRelevant" class="def">takeRelevant</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>]<a href="src/Agda-TypeChecking-MetaVars-Occurs.html#takeRelevant" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:liftUnderAbs" class="def">liftUnderAbs</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#liftUnderAbs" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Occurs" class="def">Occurs</a> t <span class="keyword">where</span><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#Occurs" class="link">Source</a></p><div class="doc"><p>Extended occurs check.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:occurs" class="def">occurs</a> :: <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">UnfoldStrategy</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:OccursCtx">OccursCtx</a> -> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> t -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> t<a href="src/Agda-TypeChecking-MetaVars-Occurs.html#occurs" class="link">Source</a></p><p class="src"><a name="v:metaOccurs" class="def">metaOccurs</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> t -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#metaOccurs" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Occurs" class="caption collapser" onclick="toggleSection('i:Occurs')">Instances</p><div id="section.i:Occurs" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:LevelAtom">LevelAtom</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:PlusLevel">PlusLevel</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:Level">Level</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> [a]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a, <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> b) => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> (a, b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:occursCheck" class="def">occursCheck</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Vars">Vars</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#occursCheck" class="link">Source</a></p><div class="doc"><p>When assigning <code>m xs := v</code>, check that <code>m</code> does not occur in <code>v</code>
and that the free variables of <code>v</code> are contained in <code>xs</code>.
</p></div></div><h1 id="g:1">Getting rid of flexible occurrences
</h1><div class="top"><p class="src"><a name="v:prune" class="def">prune</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">PruneResult</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#prune" class="link">Source</a></p><div class="doc"><p><code>prune m' vs xs</code> attempts to remove all arguments from <code>vs</code> whose
free variables are not contained in <code>xs</code>.
If successful, <code>m'</code> is solved by the new, pruned meta variable and we
return <code>True</code> else <code>False</code>.
</p></div></div><div class="top"><p class="src"><a name="v:hasBadRigid" class="def">hasBadRigid</a> :: [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>] -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#hasBadRigid" class="link">Source</a></p><div class="doc"><p><code>hasBadRigid xs v = True</code> iff one of the rigid variables in <code>v</code> is not in <code>xs</code>.
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).
</p></div></div><div class="top"><p class="src"><a name="v:rigidVarsNotContainedIn" class="def">rigidVarsNotContainedIn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => a -> [<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#rigidVarsNotContainedIn" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:PruneResult" class="def">PruneResult</a> <a href="src/Agda-TypeChecking-MetaVars-Occurs.html#PruneResult" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NothingToPrune" class="def">NothingToPrune</a></td><td class="doc"><p>the kill list is empty or only <code>False</code>s
</p></td></tr><tr><td class="src"><a name="v:PrunedNothing" class="def">PrunedNothing</a></td><td class="doc"><p>there is no possible kill (because of type dep.)
</p></td></tr><tr><td class="src"><a name="v:PrunedSomething" class="def">PrunedSomething</a></td><td class="doc"><p>managed to kill some args in the list
</p></td></tr><tr><td class="src"><a name="v:PrunedEverything" class="def">PrunedEverything</a></td><td class="doc"><p>all prescribed kills where performed
</p></td></tr></table></div><div class="subs instances"><p id="control.i:PruneResult" class="caption collapser" onclick="toggleSection('i:PruneResult')">Instances</p><div id="section.i:PruneResult" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">PruneResult</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">PruneResult</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:killArgs" class="def">killArgs</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>] -> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">PruneResult</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#killArgs" class="link">Source</a></p><div class="doc"><p><code>killArgs [k1,...,kn] X</code> prunes argument <code>i</code> from metavar <code>X</code> if <code>ki==True</code>.
Pruning is carried out whenever > 0 arguments can be pruned.
<code>True</code> is only returned if all arguments could be pruned.
</p></div></div><div class="top"><p class="src"><a name="v:killedType" class="def">killedType</a> :: [(<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>), <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>)] -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> ([<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>], <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)<a href="src/Agda-TypeChecking-MetaVars-Occurs.html#killedType" class="link">Source</a></p><div class="doc"><p><code>killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')</code>
(ignoring <code>Dom</code>). Let <code>t' = (xs:as) -> b</code>.
Invariant: <code>k'i == True</code> iff <code>ki == True</code> and pruning the <code>i</code>th argument from
type <code>b</code> is possible without creating unbound variables.
<code>t'</code> is type <code>t</code> after pruning all <code>k'i==True</code>.
</p></div></div><div class="top"><p class="src"><a name="v:performKill" class="def">performKill</a> :: [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>] -> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-MetaVars-Occurs.html#performKill" class="link">Source</a></p></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
