HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

Kind2 hanging on file check #400

Closed Danfs64 closed 4 months ago

Danfs64 commented 2 years ago

If I try to check this:

Flat_map <x> <y> (f : x -> List y) (l : List x) : List y
Flat_map f  List.nil        = List.nil
Flat_map f (List.cons x xs) =
  let app = (f x)
  List.concat app (Flat_map f xs)

Main {
  (Flat_map (n => [n, n]) [1,5,4])
}

The kind2 check <file> command hangs indefinitely. If I try to run said file, it runs correctly. Also, if I change the Main to:

Main {
  (Flat_map (n => [n]) [1,5,4])
}

It checks appropriately

developedby commented 2 years ago

It's failing to infer the type of n. If you annotate the lambda it type checks fine: ((n: U60) => [n, n])