Thursday 20 November 2008

Type Error

Error:
In environment
ty : type
m : term ty
eq_term_dec :
forall (m' : {m' : term ty | size m' < size m}) (n : term ty),
{`m' = n} + {`m' <> n}
n : term ty
eq_term_dec0 :
forall (ty : type) (m n : term ty),
{[m : (term ty)]= [n : (term ty)]} + {m =/= n}
ty0 : type
m0 : term ty0
n0 : term ty0
uTy : type
vTy : type
u : term (uTy --> vTy)
v : term uTy
uTy' : type
vTy' : type
u' : term (uTy' --> vTy')
v' : term uTy'
vTyEq : vTy = vTy'
filtered_var := eq_type_dec uTy uTy' : {uTy = uTy'} + {uTy <> uTy'}
uTyEq : uTy = uTy'
Heq_anonymous : in_left = filtered_var
u0 : term (uTy --> vTy)
v0 : term uTy
u'0 : term (uTy --> vTy)
v'0 : term uTy
filtered_var0 := eq_term_dec0 (uTy --> vTy) u0 u'0 :
{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}
filtered_var1 := eq_term_dec0 uTy v0 v'0 :
{[v0 : (term uTy)]= [v'0 : (term uTy)]} + {v0 =/= v'0}
branch_0 :=
fun (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
(wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)])
(Heq_anonymous0 : in_left = filtered_var0)
(Heq_anonymous1 : in_left = filtered_var1) => in_left :
forall
(wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
(wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
in_left = filtered_var0 ->
in_left = filtered_var1 ->
{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +
{app u0 v0 =/= app u'0 v'0}
branch_1 :=
fun
(wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +
{u0 =/= u'0})
(wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
{u'0 =/= filtered_var0})
(H : forall
(wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0
: (term (uTy --> vTy))])
(wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
~ (in_left = wildcard' /\ in_left = wildcard'0))
(Heq_anonymous0 : wildcard' = filtered_var0)
(Heq_anonymous1 : wildcard'0 = filtered_var1) => in_right :
forall
(wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +
{u0 =/= u'0})
(wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
{u'0 =/= filtered_var0}),
(forall
(wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
(wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
~ (in_left = wildcard' /\ in_left = wildcard'0)) ->
wildcard' = filtered_var0 ->
wildcard'0 = filtered_var1 ->
{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +
{app u0 v0 =/= app u'0 v'0}
Anonymous : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]
wildcard' := in_left :
{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}
Anonymous0 : u'0 =/= wildcard'
wildcard'0 := in_right :
{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}
The term "wildcard'0" has type
"{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}"
while it is expected to have type
"{[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
{u'0 =/= filtered_var0}".

No comments: