4

I stumbled upon what seems to be a strange behavior for Idris.

I'm using Emacs 25.3 on Ubuntu 17.04 and Idris 1.0.

Consider the following module:

module Strange

%default total

fun : Int -> Int -> Int
fun 0 0 = 0
fun 0 n = 10
fun n 0 = 20

When I load this (C-c C-l), I do not get a non-total function warning, and when I try it on the REPL I get this:

λΠ> fun 100 200
20 : Int

... as if Idris is not matching the literal 0 in the third clause. This behavior occurs also when loading the module in a normal shell (idris Strange.idr).

Shouldn't I get some kind of error about non-totality? Is this some bug in this version of Idris?

Thales MG
  • 761
  • 5
  • 15
  • 1
    This is really strange indeed. When I load your file in Idris REPL I see compilation error about non-totality: `Strange.idr:6:1:Strange.fun is not total as there are missing cases`. – Shersh Dec 17 '17 at 17:47
  • @Shersh Is your Idris version newer than 1.0? Like 1.1.1? – Thales MG Dec 17 '17 at 21:11
  • I don't think so. When I execute `idris --version` I see `1.0`. – Shersh Dec 18 '17 at 01:46

0 Answers0