Browse thread
Perplexing type error.
- Michael Jones
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Michael Jones <Michael.Jones@c...> |
| Subject: | Perplexing type error. |
Tres petit(e) abstract en Francais: Il y a une "type error" que je ne comprende pas. While tweaking a preterm parser for type expressions in a proof assistant written in caml, I came across the following perplexing type error. At first, it looked like a type inference problem so I specified the types in the generic function definitions and got a new error: #Toplevel input: > and parse_pretypepred src = P_APPLY Pred (parse_preterm) src > ^^^^^^^^^^^^^ This expression has type lexcode list -> preterm * lexcode list, but is used with type lexcode list -> preterm * lexcode list. # _ So. Any ideas why this is an error and how I can fix it? I'm stumped. The line with the error in it is part of a larger mutualy recursive function. I am using caml-light-0.71 on a sun workstation and didn't see anything similar in the known bugs file. Some more detail about the line of code: P_APPLY is a parser combinater that takes a function (Pred in this case) and applies it to the parser result. Pred is a type constructor for making pretypes out of preterms. parse_preterm is the parser and src is the output of the lex. analyzer. regards, mike.