What steps will reproduce the problem?
Run the following code:
prog id : Nat => Nat
id = \x.x
prog bug1 : Nat
bug1 = id (id 2)
What is the expected output?
The expected output should be an error message
conveying that the argument to id should be a value.
or
It could say that the definition of test is in non-linear
form. Either one would suffice. I like the former.
What do you see instead?
When applying to a term with classifier
P, it must be classified Total, but
'(id (Succ (Succ Zero)))'
is not.
when checking the term
'id (id (Succ (Succ Zero)))'
against the signature
'Nat'
In the expression id (id (Succ (Succ Zero)))
The output we get now doesn't really convey to the programmer what the error
is. It makes it sound as
if all arguments to programmatic functions must be total, but this is not
correct. In the programmatic fragment we should be able to pass non-total
functions into non-total functions. So I think this confuses the programmer.
Original issue reported on code.google.com by harley.e...@gmail.com on 2 Mar 2011 at 11:41
Original issue reported on code.google.com by
harley.e...@gmail.comon 2 Mar 2011 at 11:41