<!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.Rules.LHS.Unify</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-Rules-LHS-Unify.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Rules-LHS-Unify.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.Rules.LHS.Unify</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"><span class="keyword">newtype</span> <a href="#t:Unify">Unify</a> a = <a href="#v:U">U</a> {<ul class="subs"><li><a href="#v:unUnify">unUnify</a> :: <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader.html#t:ReaderT">ReaderT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyEnv">UnifyEnv</a> (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Writer-Lazy.html#t:WriterT">WriterT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">UnifyOutput</a> (<a href="Agda-TypeChecking-Monad-Exception.html#t:ExceptionT">ExceptionT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException">UnifyException</a> (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Lazy.html#t:StateT">StateT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyState">UnifyState</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a>))) a</li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:UnifyMayPostpone">UnifyMayPostpone</a> <ul class="subs"><li>= <a href="#v:MayPostpone">MayPostpone</a> </li><li>| <a href="#v:MayNotPostpone">MayNotPostpone</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:UnifyEnv">UnifyEnv</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">UnifyMayPostpone</a></li><li class="src short"><a href="#v:emptyUEnv">emptyUEnv</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">UnifyMayPostpone</a></li><li class="src short"><a href="#v:noPostponing">noPostponing</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a</li><li class="src short"><a href="#v:askPostpone">askPostpone</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">UnifyMayPostpone</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:UnifyOutput">UnifyOutput</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unifiable">Unifiable</a></li><li class="src short"><a href="#v:emptyUOutput">emptyUOutput</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">UnifyOutput</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:Unifiable">Unifiable</a> <ul class="subs"><li>= <a href="#v:Definitely">Definitely</a> </li><li>| <a href="#v:Possibly">Possibly</a> </li></ul></li><li class="src short"><a href="#v:reportPostponing">reportPostponing</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:ifClean">ifClean</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a</li><li class="src short"><span class="keyword">data</span> <a href="#t:Equality">Equality</a> = <a href="#v:Equal">Equal</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Sub">Sub</a> = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:UnifyException">UnifyException</a> <ul class="subs"><li>= <a href="#v:ConstructorMismatch">ConstructorMismatch</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> </li><li>| <a href="#v:StronglyRigidOccurrence">StronglyRigidOccurrence</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> </li><li>| <a href="#v:GenericUnifyException">GenericUnifyException</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:UnifyState">UnifyState</a> = <a href="#v:USt">USt</a> {<ul class="subs"><li><a href="#v:uniSub">uniSub</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a></li><li><a href="#v:uniConstr">uniConstr</a> :: [<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</a>]</li></ul>}</li><li class="src short"><a href="#v:emptyUState">emptyUState</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyState">UnifyState</a></li><li class="src short"><a href="#v:constructorMismatch">constructorMismatch</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a</li><li class="src short"><a href="#v:constructorMismatchHH">constructorMismatchHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a</li><li class="src short"><a href="#v:onSub">onSub</a> :: (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a> -> a) -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a</li><li class="src short"><a href="#v:modSub">modSub</a> :: (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a>) -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:checkEqualities">checkEqualities</a> :: [<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</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:checkEquality">checkEquality</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</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/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:checkEqualityHH">checkEqualityHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:forceHom">forceHom</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:addEquality">addEquality</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:addEqualityHH">addEqualityHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:takeEqualities">takeEqualities</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> [<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</a>]</li><li class="src short"><a href="#v:occursCheck">occursCheck</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:-124--45--62-">(|->)</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> (<a href="Agda-Syntax-Internal.html#t:Term">Term</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>) -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:makeSubstitution">makeSubstitution</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><span class="keyword">class</span> <a href="#t:UReduce">UReduce</a> t <span class="keyword">where</span><ul class="subs"><li><a href="#v:ureduce">ureduce</a> :: t -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> t</li></ul></li><li class="src short"><a href="#v:flattenSubstitution">flattenSubstitution</a> :: <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:UnificationResult">UnificationResult</a> <ul class="subs"><li>= <a href="#v:Unifies">Unifies</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a> </li><li>| <a href="#v:NoUnify">NoUnify</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> </li><li>| <a href="#v:DontKnow">DontKnow</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:HomHet">HomHet</a> a<ul class="subs"><li>= <a href="#v:Hom">Hom</a> a </li><li>| <a href="#v:Het">Het</a> a a </li></ul></li><li class="src short"><a href="#v:isHom">isHom</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> 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:fromHom">fromHom</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a -> a</li><li class="src short"><a href="#v:leftHH">leftHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a -> a</li><li class="src short"><a href="#v:rightHH">rightHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a -> a</li><li class="src short"><span class="keyword">type</span> <a href="#t:TermHH">TermHH</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:TypeHH">TypeHH</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:TelHH">TelHH</a> = <a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>)</li><li class="src short"><span class="keyword">type</span> <a href="#t:TelViewHH">TelViewHH</a> = <a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a></li><li class="src short"><a href="#v:absAppHH">absAppHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> t tHH => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> t -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH">TermHH</a> -> tHH</li><li class="src short"><span class="keyword">class</span> <a href="#t:ApplyHH">ApplyHH</a> t <span class="keyword">where</span><ul class="subs"><li><a href="#v:applyHH">applyHH</a> :: t -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> t</li></ul></li><li class="src short"><a href="#v:substHH">substHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> t tHH => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH">TermHH</a> -> t -> tHH</li><li class="src short"><span class="keyword">class</span> <a href="#t:SubstHH">SubstHH</a> t tHH <span class="keyword">where</span><ul class="subs"><li><a href="#v:substUnderHH">substUnderHH</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH">TermHH</a> -> t -> tHH</li><li><a href="#v:trivialHH">trivialHH</a> :: t -> tHH</li></ul></li><li class="src short"><a href="#v:unifyIndices_">unifyIndices_</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:FlexibleVars">FlexibleVars</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> tcm <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:unifyIndices">unifyIndices</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:FlexibleVars">FlexibleVars</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> tcm <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnificationResult">UnificationResult</a></li><li class="src short"><a href="#v:dataOrRecordType">dataOrRecordType</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)</li><li class="src short"><a href="#v:dataOrRecordType-39-">dataOrRecordType'</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>, <a href="Agda-Syntax-Internal.html#t:Args">Args</a>))</li><li class="src short"><a href="#v:dataOrRecordTypeHH">dataOrRecordTypeHH</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</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-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>)</li><li class="src short"><a href="#v:isEtaRecordTypeHH">isEtaRecordTypeHH</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> tcm (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Args">Args</a>))</li><li class="src short"><span class="keyword">data</span> <a href="#t:ShapeView">ShapeView</a> a<ul class="subs"><li>= <a href="#v:PiSh">PiSh</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a) </li><li>| <a href="#v:FunSh">FunSh</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) a </li><li>| <a href="#v:DefSh">DefSh</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> </li><li>| <a href="#v:VarSh">VarSh</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> </li><li>| <a href="#v:LitSh">LitSh</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> </li><li>| <a href="#v:SortSh">SortSh</a> </li><li>| <a href="#v:MetaSh">MetaSh</a> </li><li>| <a href="#v:ElseSh">ElseSh</a> </li></ul></li><li class="src short"><a href="#v:shapeView">shapeView</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> (<a href="Agda-Syntax-Internal.html#t:Type">Type</a>, <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)</li><li class="src short"><a href="#v:shapeViewHH">shapeViewHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>, <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>)</li><li class="src short"><a href="#v:telViewUpToHH">telViewUpToHH</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TelViewHH">TelViewHH</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:Unify" class="def">Unify</a> a <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#Unify" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:U" class="def">U</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:unUnify" class="def">unUnify</a> :: <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader.html#t:ReaderT">ReaderT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyEnv">UnifyEnv</a> (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Writer-Lazy.html#t:WriterT">WriterT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">UnifyOutput</a> (<a href="Agda-TypeChecking-Monad-Exception.html#t:ExceptionT">ExceptionT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException">UnifyException</a> (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Lazy.html#t:StateT">StateT</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyState">UnifyState</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a>))) a</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Unify" class="caption collapser" onclick="toggleSection('i:Unify')">Instances</p><div id="section.i:Unify" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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/Control-Applicative.html#t:Applicative">Applicative</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/transformers-0.3.0.0/Control-Monad-IO-Class.html#t:MonadIO">MonadIO</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader-Class.html#t:MonadReader">MonadReader</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCEnv">TCEnv</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCState">TCState</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Writer-Class.html#t:MonadWriter">MonadWriter</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">UnifyOutput</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Monad-Exception.html#t:MonadException">MonadException</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException">UnifyException</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:UnifyMayPostpone" class="def">UnifyMayPostpone</a> <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UnifyMayPostpone" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:MayPostpone" class="def">MayPostpone</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:MayNotPostpone" class="def">MayNotPostpone</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:UnifyEnv" class="def">UnifyEnv</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">UnifyMayPostpone</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UnifyEnv" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:emptyUEnv" class="def">emptyUEnv</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">UnifyMayPostpone</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#emptyUEnv" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:noPostponing" class="def">noPostponing</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#noPostponing" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:askPostpone" class="def">askPostpone</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">UnifyMayPostpone</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#askPostpone" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:UnifyOutput" class="def">UnifyOutput</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unifiable">Unifiable</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UnifyOutput" class="link">Source</a></p><div class="doc"><p>Output the result of unification (success or maybe).
</p></div></div><div class="top"><p class="src"><a name="v:emptyUOutput" class="def">emptyUOutput</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">UnifyOutput</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#emptyUOutput" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Unifiable" class="def">Unifiable</a> <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#Unifiable" class="link">Source</a></p><div class="doc"><p>Were two terms unifiable or did we have to postpone some equation such that we are not sure?
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Definitely" class="def">Definitely</a></td><td class="doc"><p>Unification succeeded.
</p></td></tr><tr><td class="src"><a name="v:Possibly" class="def">Possibly</a></td><td class="doc"><p>Unification did not fail, but we had to postpone a part.
</p></td></tr></table></div><div class="subs instances"><p id="control.i:Unifiable" class="caption collapser" onclick="toggleSection('i:Unifiable')">Instances</p><div id="section.i:Unifiable" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Monoid.html#t:Monoid">Monoid</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unifiable">Unifiable</a></td><td class="doc"><p>Conjunctive monoid.
</p></td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Writer-Class.html#t:MonadWriter">MonadWriter</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">UnifyOutput</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:reportPostponing" class="def">reportPostponing</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#reportPostponing" class="link">Source</a></p><div class="doc"><p>Tell that something could not be unified right now,
so the unification succeeds only <code><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:Possibly">Possibly</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:ifClean" class="def">ifClean</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#ifClean" class="link">Source</a></p><div class="doc"><p>Check whether unification proceeded without postponement.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Equality" class="def">Equality</a> <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#Equality" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Equal" class="def">Equal</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Equality" class="caption collapser" onclick="toggleSection('i:Equality')">Instances</p><div id="section.i:Equality" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Sub" class="def">Sub</a> = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#Sub" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:UnifyException" class="def">UnifyException</a> <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UnifyException" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ConstructorMismatch" class="def">ConstructorMismatch</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:StronglyRigidOccurrence" class="def">StronglyRigidOccurrence</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:GenericUnifyException" class="def">GenericUnifyException</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:UnifyException" class="caption collapser" onclick="toggleSection('i:UnifyException')">Instances</p><div id="section.i:UnifyException" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Error-Class.html#t:Error">Error</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException">UnifyException</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Monad-Exception.html#t:MonadException">MonadException</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException">UnifyException</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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:UnifyState" class="def">UnifyState</a> <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UnifyState" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:USt" class="def">USt</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:uniSub" class="def">uniSub</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:uniConstr" class="def">uniConstr</a> :: [<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</a>]</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div></div><div class="top"><p class="src"><a name="v:emptyUState" class="def">emptyUState</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyState">UnifyState</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#emptyUState" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:constructorMismatch" class="def">constructorMismatch</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#constructorMismatch" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:constructorMismatchHH" class="def">constructorMismatchHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#constructorMismatchHH" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:onSub" class="def">onSub</a> :: (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a> -> a) -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#onSub" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:modSub" class="def">modSub</a> :: (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a>) -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#modSub" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:checkEqualities" class="def">checkEqualities</a> :: [<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</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-Rules-LHS-Unify.html#checkEqualities" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:checkEquality" class="def">checkEquality</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</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/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#checkEquality" class="link">Source</a></p><div class="doc"><p>Force equality now instead of postponing it using <code><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:addEquality">addEquality</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:checkEqualityHH" class="def">checkEqualityHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#checkEqualityHH" class="link">Source</a></p><div class="doc"><p>Try equality. If constraints remain, postpone (enter unsafe mode).
Heterogeneous equalities cannot be tried nor reawakened,
so we can throw them away and flag <a href="dirty.html">dirty</a>.
</p></div></div><div class="top"><p class="src"><a name="v:forceHom" class="def">forceHom</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#forceHom" class="link">Source</a></p><div class="doc"><p>Check whether heterogeneous situation is really homogeneous.
If not, give up.
</p></div></div><div class="top"><p class="src"><a name="v:addEquality" class="def">addEquality</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#addEquality" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addEqualityHH" class="def">addEqualityHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#addEqualityHH" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:takeEqualities" class="def">takeEqualities</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> [<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</a>]<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#takeEqualities" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:occursCheck" class="def">occursCheck</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#occursCheck" class="link">Source</a></p><div class="doc"><p>Includes flexible occurrences, metas need to be solved. TODO: relax?
TODO: later solutions may remove flexible occurences
</p></div></div><div class="top"><p class="src"><a name="v:-124--45--62-" class="def">(|->)</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> (<a href="Agda-Syntax-Internal.html#t:Term">Term</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>) -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</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-Rules-LHS-Unify.html#%7C-%3E" class="link">Source</a></p><div class="doc"><p>Assignment with preceding occurs check.
</p></div></div><div class="top"><p class="src"><a name="v:makeSubstitution" class="def">makeSubstitution</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub">Sub</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#makeSubstitution" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:UReduce" class="def">UReduce</a> t <span class="keyword">where</span><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UReduce" class="link">Source</a></p><div class="doc"><p>Apply the current substitution on a term and reduce to weak head normal form.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:ureduce" class="def">ureduce</a> :: t -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> t<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#ureduce" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:UReduce" class="caption collapser" onclick="toggleSection('i:UReduce')">Instances</p><div id="section.i:UReduce" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce">UReduce</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-Rules-LHS-Unify.html#t:UReduce">UReduce</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-Rules-LHS-Unify.html#t:UReduce">UReduce</a> t => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce">UReduce</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce">UReduce</a> t => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce">UReduce</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> t)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:flattenSubstitution" class="def">flattenSubstitution</a> :: <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#flattenSubstitution" class="link">Source</a></p><div class="doc"><p>Take a substitution σ and ensure that no variables from the domain appear
in the targets. The context of the targets is not changed.
TODO: can this be expressed using makeSubstitution and applySubst?
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:UnificationResult" class="def">UnificationResult</a> <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#UnificationResult" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Unifies" class="def">Unifies</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:NoUnify" class="def">NoUnify</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DontKnow" class="def">DontKnow</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCErr">TCErr</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:HomHet" class="def">HomHet</a> a <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#HomHet" class="link">Source</a></p><div class="doc"><p>Are we in a homogeneous (one type) or heterogeneous (two types) situation?
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Hom" class="def">Hom</a> a</td><td class="doc"><p>homogeneous
</p></td></tr><tr><td class="src"><a name="v:Het" class="def">Het</a> a a</td><td class="doc"><p>heterogeneous
</p></td></tr></table></div><div class="subs instances"><p id="control.i:HomHet" class="caption collapser" onclick="toggleSection('i:HomHet')">Instances</p><div id="section.i:HomHet" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</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/Data-Typeable-Internal.html#t:Typeable1">Typeable1</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</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/Data-Foldable.html#t:Foldable">Foldable</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</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/Data-Traversable.html#t:Traversable">Traversable</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</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-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</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/Data-Eq.html#t:Eq">Eq</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</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-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</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-Pretty.html#t:PrettyTCM">PrettyTCM</a> a => <a href="Agda-TypeChecking-Pretty.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-Rules-LHS-Unify.html#t:UReduce">UReduce</a> t => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce">UReduce</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a) (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:isHom" class="def">isHom</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> 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-Rules-LHS-Unify.html#isHom" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:fromHom" class="def">fromHom</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a -> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#fromHom" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:leftHH" class="def">leftHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a -> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#leftHH" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:rightHH" class="def">rightHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a -> a<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#rightHH" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:TermHH" class="def">TermHH</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#TermHH" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:TypeHH" class="def">TypeHH</a> = <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#TypeHH" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:TelHH" class="def">TelHH</a> = <a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>)<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#TelHH" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:TelViewHH" class="def">TelViewHH</a> = <a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#TelViewHH" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:absAppHH" class="def">absAppHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> t tHH => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> t -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH">TermHH</a> -> tHH<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#absAppHH" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:ApplyHH" class="def">ApplyHH</a> t <span class="keyword">where</span><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#ApplyHH" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:applyHH" class="def">applyHH</a> :: t -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> t<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#applyHH" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:ApplyHH" class="caption collapser" onclick="toggleSection('i:ApplyHH')">Instances</p><div id="section.i:ApplyHH" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ApplyHH">ApplyHH</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-Rules-LHS-Unify.html#t:ApplyHH">ApplyHH</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:substHH" class="def">substHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> t tHH => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH">TermHH</a> -> t -> tHH<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#substHH" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:SubstHH" class="def">SubstHH</a> t tHH <span class="keyword">where</span><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#SubstHH" class="link">Source</a></p><div class="doc"><p><code>substHH u t</code> substitutes <code>u</code> for the 0th variable in <code>t</code>.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:substUnderHH" class="def">substUnderHH</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH">TermHH</a> -> t -> tHH<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#substUnderHH" class="link">Source</a></p><p class="src"><a name="v:trivialHH" class="def">trivialHH</a> :: t -> tHH<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#trivialHH" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:SubstHH" class="caption collapser" onclick="toggleSection('i:SubstHH')">Instances</p><div id="section.i:SubstHH" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</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-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</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-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a b => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a b => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a b => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> a) (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a b => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a) (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> b)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> 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-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a a', <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> b b') => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (a, b) (a', b')</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:unifyIndices_" class="def">unifyIndices_</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:FlexibleVars">FlexibleVars</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> tcm <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#unifyIndices_" class="link">Source</a></p><div class="doc"><p>Unify indices.
</p></div></div><div class="top"><p class="src"><a name="v:unifyIndices" class="def">unifyIndices</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:FlexibleVars">FlexibleVars</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> tcm <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnificationResult">UnificationResult</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#unifyIndices" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dataOrRecordType" class="def">dataOrRecordType</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#dataOrRecordType" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc"><p>Constructor name.
</p></td></tr><tr><td class="src">-> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc"><p>Type of constructor application (must end in data/record).
</p></td></tr><tr><td class="src">-> <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-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)</td><td class="doc"><p>Type of constructor, applied to pars.
</p></td></tr></table></div><div class="doc"><p>Given the type of a constructor application the corresponding
data or record type, applied to its parameters (extracted from the
given type), is returned.
</p><p>Precondition: The type has to correspond to an application of the
given constructor.
</p></div></div><div class="top"><p class="src"><a name="v:dataOrRecordType-39-" class="def">dataOrRecordType'</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#dataOrRecordType%27" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc"><p>Constructor name.
</p></td></tr><tr><td class="src">-> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc"><p>Type of constructor application (must end in data/record).
</p></td></tr><tr><td class="src">-> <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-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Internal.html#t:Type">Type</a>, <a href="Agda-Syntax-Internal.html#t:Args">Args</a>))</td><td class="doc"><p>Name of data/record type,
type of constructor to be applied, and
data/record parameters
</p></td></tr></table></div></div><div class="top"><p class="src"><a name="v:dataOrRecordTypeHH" class="def">dataOrRecordTypeHH</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#dataOrRecordTypeHH" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc"><p>Constructor name.
</p></td></tr><tr><td class="src">-> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a></td><td class="doc"><p>Type(s) of constructor application (must end in same data/record).
</p></td></tr><tr><td class="src">-> <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-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>)</td><td class="doc"><p>Type of constructor, instantiated possibly heterogeneously to parameters.
</p></td></tr></table></div><div class="doc"><p>Heterogeneous situation.
<code>a1</code> and <code>a2</code> need to end in same datatype/record.
</p></div></div><div class="top"><p class="src"><a name="v:isEtaRecordTypeHH" class="def">isEtaRecordTypeHH</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> tcm (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> <a href="Agda-Syntax-Internal.html#t:Args">Args</a>))<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#isEtaRecordTypeHH" class="link">Source</a></p><div class="doc"><p>Return record type identifier if argument is a record type.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:ShapeView" class="def">ShapeView</a> a <a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#ShapeView" class="link">Source</a></p><div class="doc"><p>Views an expression (pair) as type shape. Fails if not same shape.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:PiSh" class="def">PiSh</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:FunSh" class="def">FunSh</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) a</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DefSh" class="def">DefSh</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc"><p>data/record
</p></td></tr><tr><td class="src"><a name="v:VarSh" class="def">VarSh</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></td><td class="doc"><p>neutral type
</p></td></tr><tr><td class="src"><a name="v:LitSh" class="def">LitSh</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a></td><td class="doc"><p>built-in type
</p></td></tr><tr><td class="src"><a name="v:SortSh" class="def">SortSh</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:MetaSh" class="def">MetaSh</a></td><td class="doc"><p>some meta
</p></td></tr><tr><td class="src"><a name="v:ElseSh" class="def">ElseSh</a></td><td class="doc"><p>not a type or not definitely same shape
</p></td></tr></table></div><div class="subs instances"><p id="control.i:ShapeView" class="caption collapser" onclick="toggleSection('i:ShapeView')">Instances</p><div id="section.i:ShapeView" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</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/Data-Typeable-Internal.html#t:Typeable1">Typeable1</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</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/Data-Eq.html#t:Eq">Eq</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> 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/Data-Ord.html#t:Ord">Ord</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> 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 => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:shapeView" class="def">shapeView</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> (<a href="Agda-Syntax-Internal.html#t:Type">Type</a>, <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a>)<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#shapeView" class="link">Source</a></p><div class="doc"><p>Return the type and its shape. Expects input in (u)reduced form.
</p></div></div><div class="top"><p class="src"><a name="v:shapeViewHH" class="def">shapeViewHH</a> :: <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>, <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView">ShapeView</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a>)<a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#shapeViewHH" class="link">Source</a></p><div class="doc"><p>Return the reduced type(s) and the common shape.
</p></div></div><div class="top"><p class="src"><a name="v:telViewUpToHH" class="def">telViewUpToHH</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH">TypeHH</a> -> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Unify</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TelViewHH">TelViewHH</a><a href="src/Agda-TypeChecking-Rules-LHS-Unify.html#telViewUpToHH" class="link">Source</a></p><div class="doc"><p><code>telViewUpToHH n t</code> takes off the first <code>n</code> function types of <code>t</code>.
Takes off all if $n < 0$.
</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>
