nunchaku-inria / nunchaku

Model finder for higher-order logic
https://nunchaku-inria.github.io/nunchaku/
BSD 2-Clause "Simplified" License
42 stars 3 forks source link

Type error without line number #28

Closed samuelgruetter closed 5 years ago

samuelgruetter commented 5 years ago

Version: nunchaku 0.5.1 70e510138ab0efd037b3351750b2b428a97c890c

The following example

val K : type.
val V : type.

data tuple := pair K V.

data list :=
  nil
| cons tuple list.

data option :=
  None
| Some V.

rec put : list -> K -> V -> list :=
  fun l k v. cons (pair k v) l.

# correct version:
# rec put : list -> K -> V -> list :=
#   put = (fun l k v. cons (pair k v) l).

yields

Error: type error:
  unification error: incompatible types:
  trying to unify `list -> K -> V -> list` and `prop`

It would be good if a line number was reported.

c-cube commented 5 years ago

I will try to improve that, thank you for the bug report.

samuelgruetter commented 5 years ago

Cool :+1: