Debugging a universe inconsistency

[Dominic Mulligan]

Hi,

What is the best way to debug a universe inconsistency? Through trial
and error I have got the exact line (or rather, choice of exact lines)
that are causing the inconsistency, but I'm at a loss as to how to
proceed to understand where the inconsistency is creeping in (both
lines look innocuous to me). In particular, turning Idris' log level
up does not seem to help in diagnosing the problem. Is there a
principled way to proceed?

Thanks,
Dom

[Edwin Brady]

Hi Dom,
To be honest I've never come across one before that I haven't contrived so I'm not sure what to suggest either. I think there probably isn't enough logging - maybe showing all the lines that lead to the cycle would help.

If it makes sense to send me the code, I'd be interested to know what sort of thing you're doing that leads to the problem (and might be able to help debug it).

(In the meantime, if you're feeling unsound and want to be less stuck, --typeintype is there :))

Edwin.

[Dominic Mulligan]

Hi Edwin,

OK, thanks. I was trying to port Haskell's Data.Map to Idris, making
everything total using dependent types. I'll send you the code and
proceed using --typeintype for the time being.

Thanks,
Dom

[Edwin Brady]

This turns out to have been a bug in the elaborator, which is now fixed in git.

(If anyone's interested: the problem was not keeping the set of universe variables up to date when definitions contained metavariables, resulting in too many constraints being generated.)

Edwin.