Sorry about the explosion surrounding my implementation of a simple reverse function in class. Working with theorem provers can be humbling as undoubtedly you are discovering.
The problem was quite subtle. Will discovered the issue after he and I poked around a bit after class. Here is the definition we were working with:
Fixpoint rev (T:Type) (l:list T) : list T :=
match l with
| nil _ => nil T
| (cons _ h t) => (app T (rev T t) (cons T h (nil T)))
end.
Other than the wildcards for type variables, this definition should make pretty good sense to you. It did when I was working with it, but I could not get it to type check much less execute.
As Will discovered, the problem is not in the definition of rev but un the
definition of app. nil and cons are both defined by our new definition of
polymorphic lists. rev is the function under consideration. We’ve written
a version of app previously that is still in scope. However, that app was
written before our polymorphic list definition in Lists.v. When we tried to
use it in the definition of rev, of course it did not type check. If type
checking had thrown an error that app did not exist we would have caught it
immediately.
I’m happy to go through this in class if anyone is interested in seeing it, but
if you simply write a polymorphic version of app before the polymorphic
version of rev, everything works perfectly.