<!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.Errors</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-Errors.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Errors.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.Errors</p></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:prettyError">prettyError</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</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-String.html#t:String">String</a></li><li class="src short"><span class="keyword">class</span> <a href="#t:PrettyTCM">PrettyTCM</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:prettyTCM">prettyTCM</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Pretty.html#t:Doc">Doc</a></li></ul></li><li class="src short"><a href="#v:tcErrString">tcErrString</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:Warnings">Warnings</a> = <a href="#v:Warnings">Warnings</a> {<ul class="subs"><li><a href="#v:terminationProblems">terminationProblems</a> :: [<a href="Agda-TypeChecking-Monad-Base.html#t:TerminationError">TerminationError</a>]</li><li><a href="#v:unsolvedMetaVariables">unsolvedMetaVariables</a> :: [<a href="Agda-Syntax-Position.html#t:Range">Range</a>]</li><li><a href="#v:unsolvedConstraints">unsolvedConstraints</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Constraints">Constraints</a></li></ul>}</li><li class="src short"><a href="#v:warningsToError">warningsToError</a> :: <a href="Agda-TypeChecking-Errors.html#t:Warnings">Warnings</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TypeError">TypeError</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:prettyError" class="def">prettyError</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</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-String.html#t:String">String</a><a href="src/Agda-TypeChecking-Errors.html#prettyError" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:PrettyTCM" class="def">PrettyTCM</a> a <span class="keyword">where</span><a href="src/Agda-TypeChecking-Pretty.html#PrettyTCM" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:prettyTCM" class="def">prettyTCM</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Pretty.html#t:Doc">Doc</a><a href="src/Agda-TypeChecking-Pretty.html#prettyTCM" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:PrettyTCM" class="caption collapser" onclick="toggleSection('i:PrettyTCM')">Instances</p><div id="section.i:PrettyTCM" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</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-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</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-Errors.html#t:PrettyTCM">PrettyTCM</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-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</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-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Internal.html#t:Elim">Elim</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</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-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TypeError">TypeError</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Context">Context</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Call">Call</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayTerm">DisplayTerm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:ProblemConstraint">ProblemConstraint</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:NamedClause">NamedClause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Pretty.html#t:PrettyContext">PrettyContext</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Positivity.html#t:Node">Node</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Positivity.html#t:OccursWhere">OccursWhere</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:AsBinding">AsBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:DotPatternInst">DotPatternInst</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-TypeChecking-Coverage.html#t:SplitError">SplitError</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Termination-TermCheck.html#t:DeBruijnPat">DeBruijnPat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> a => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> [a]</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> a e, <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> e c, <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> c) => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</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-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> a e, <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> e c, <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> c) => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</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-Errors.html#t:PrettyTCM">PrettyTCM</a> a => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-Syntax-Internal.html#t:Blocked">Blocked</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> a => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> a => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> a, <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> b) => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (a, b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> n => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (n, <a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> n => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (n, <a href="Agda-TypeChecking-Positivity.html#t:Edge">Edge</a>)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> n, <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (n, e)) => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-Utils-Graph.html#t:Graph">Graph</a> n e)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> a e, <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> e c, <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> c) => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> a, <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> b) => <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Judgement">Judgement</a> a b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:tcErrString" class="def">tcErrString</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a><a href="src/Agda-TypeChecking-Errors.html#tcErrString" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Warnings" class="def">Warnings</a> <a href="src/Agda-TypeChecking-Errors.html#Warnings" class="link">Source</a></p><div class="doc"><p>Warnings.
</p><p>Invariant: The fields are never empty at the same time.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Warnings" class="def">Warnings</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:terminationProblems" class="def">terminationProblems</a> :: [<a href="Agda-TypeChecking-Monad-Base.html#t:TerminationError">TerminationError</a>]</dt><dd class="doc"><p>Termination checking problems are not reported if
<code>optTerminationCheck</code> is <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#v:False">False</a></code>.
</p></dd><dt class="src"><a name="v:unsolvedMetaVariables" class="def">unsolvedMetaVariables</a> :: [<a href="Agda-Syntax-Position.html#t:Range">Range</a>]</dt><dd class="doc"><p>Meta-variable problems are reported as type errors unless
<code>optAllowUnsolved</code> is <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#v:True">True</a></code>.
</p></dd><dt class="src"><a name="v:unsolvedConstraints" class="def">unsolvedConstraints</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Constraints">Constraints</a></dt><dd class="doc"><p>Same as <code><a href="Agda-TypeChecking-Errors.html#v:unsolvedMetaVariables">unsolvedMetaVariables</a></code>.
</p></dd></dl><div class="clear"></div></div></td></tr></table></div></div><div class="top"><p class="src"><a name="v:warningsToError" class="def">warningsToError</a> :: <a href="Agda-TypeChecking-Errors.html#t:Warnings">Warnings</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TypeError">TypeError</a><a href="src/Agda-TypeChecking-Errors.html#warningsToError" class="link">Source</a></p><div class="doc"><p>Turns warnings into an error. Even if several errors are possible
only one is raised.
</p></div></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>
