Error Messages Unclear wrt Theorem type instantiation

import List
import Nat

theorem l_one : length(node(1, empty)) = 1
proof
  // length_one[1]
  // length_one[Nat][1]
  // length_one[Nat, 1]
  length_one<Nat>[1]
end

Error messages here for the commented errors are unclear as to what the problem is. Working on fixing this.

Ex In Order: expected type but the call returns Nat

/home/calvin/Documents/Programming/343/deduce/test.pf:6.3-6.18: to instantiate:
        length_one : (all U:type. (all x:U. length([x]) = 1))
with type arguments, instead write:
        length_one<Nat>

/home/calvin/Documents/Programming/343/deduce/test.pf:6.3-6.21: to instantiate:
        length_one : (all U:type. (all x:U. length([x]) = 1))
with type arguments, instead write:
        length_one<Nat, 1>

jsiek / deduce

Error Messages Unclear wrt Theorem type instantiation #27