idris-lang / Idris2

A purely functional programming language with first class types

https://idris-lang.org/

Other

2.5k stars 375 forks source link

[ bug ] Buggy `Data.Fin.fromInteger` in the presence of negative integer literals #3266

Closed stefan-hoeck closed 5 months ago

stefan-hoeck commented 5 months ago

This was found by one of my students:

Steps to Reproduce

Typecheck the folloing:

import Data.Fin

%default total

oops : Fin 0
oops = (-1)

boom : Void
boom = uninhabited oops

Expected Behavior

Fails to typecheck.

Observed Behavior

Compiler happy.

The reason is an unhealthy use of believe_me in the implementation of Data.Fin.fromInteger. The fix should not be too hard, so I'll try to come up with a PR soonish.

stefan-hoeck commented 5 months ago

Closed via #3267 .