%include lhs2TeX.fmt

%if anyMath

%format .     = ".~"
%format alpha = "\alpha"
%format beta  = "\beta"
%format gamma = "\gamma"
%format delta = "\delta"
%format phi   = "\phi"
%format psi   = "\psi"
%format Set   = "\SET"
%format |-    = "\vdash"
%format ?     = "~{?}"

%format when  = "\mathbf{when}"

%endif


%However, when adding meta-variables things get more complicated.
%The convertibility of $A$ and $B$ might now be unknown until some of the meta
%variables have been instantiated.We will give an example illustrating the problem. Given 
%the set of natural numbers, |Nat|, and the set of booleans, |Bool|. Given also a function, |F : Bool -> Set|. The problem we consider is checking if the term 
%|\g. g 0| has type|((x : F ?) -> F (not x)) -> Nat|
%, where the term |?| is a meta-variable of type |Bool| and |0| is a natural number. We now get the constraints |F ? = Bool|, |F ? = Nat|,
% and |F (not 0) = Nat|. We can now see that we have a problem since |F (not 0)|
% is ill-typed. 


When adding meta-variables equality checking gets more complicated, since we cannot
always decide the validity of an equality, and we may be forced to keep it as a
constraint. This is well-known in higher order
unification\cite{huet:unification}: the constraint $?~0 = 0$ has two solutions
$? = \lambda x.x$ and $? = \lambda x.0$. This appears also in type theory with
constraints of the form |F ? = Bool| where $F$ is defined by computation rules.
The fact that we type check modulo yet unsolved constraints can lead to
ill-typed terms.
For instance, 
consider the type-checking problem
|\g. g 0:((x : F ?) -> F (not x)) -> Nat|\footnote{The notation |(x:A) -> B x| should be read as $\forall x:A. B ~x$.}
where the term ? is a meta-variable of type |Bool|, |0:Nat|, and |F:Bool->Set| where |F false = Nat| and |F true = Bool|.
First we check that |((x : F ?) -> F (not x)) -> Nat| is a well-formed type, which
generates the constraint |F ? = Bool|, since the term |not x| forces |x| to be
of type |Bool|. Checking |\g.g 0| against the type |((x : F ?) -> F (not x)) -> Nat|
generate then the constraints |F ? = Nat| and then |F (not 0) = Nat|, which contains
an ill-typed term\footnote{In fact we will also get the constraint |Bool = Bool| which is trivially 
valid and therefore left out.}.