type-checking going slowly

26 views
Skip to first unread message

Robert Watson

unread,
Sep 28, 2022, 10:56:57 AM9/28/22
to Idris Programming Language
Sometimes type-checking gets slowed down to about 4 minutes and when it does this it is just trying to find the type of, or simplify or something, a right hand side hole (all the essentials seem to be checked fine and quickly). I've tested that this is in fact the problem by trying to find the type of such a hole, and indeed the process gets killed (after about 7 minutes in this case). I'm thinking it should be possible to turn off that search or reduce it to 30 seconds or something. 

Is there any way to do that?

It looks something like this: 

example :   (f : Function) -> (c : Value) -> some complicated but valid type
example f c = ?kkkdd
(4 minutes of type checking)

Whereas the following type checks instantly:
example :   (f : Function) -> (c : Value) -> some complicated but valid type
(instant type-checking)

Reply all
Reply to author
Forward
0 new messages