Matching on constructor function

[Victor-Savu]

Hi, I'm new to Idris, so I apologise in advance for not using the correct terms. I will just post the TD&DR; version here and explain below how I got to this problem to avoid cluttering the report. Also, thanks a lot for Idris!

TL&DR: I inserted the Int on the first line when refactoring and to my surprise the code still compiled but baz turned into a constant function returning "Hello":

data FooBar = MkFoo Int | MkBar

baz : FooBar -> String
baz MkFoo = "Hello"
baz MkBar = "World"

Steps to Reproduce

1. Install Idris 1.3.2

2. Load a script containing the above code (in my case the file was named unif.idr):

   idris unif.idr
   

Expected Behavior

The error that idris2 produces:

     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.0.0-ab98b4d3c
  _/ // /_/ / /  / (__  )   / __/      http://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/

Welcome to Idris 2.  Enjoy yourself!
1/1: Building unif (unif.idr)
unif.idr:4:5--4:11:While processing left hand side of Main.baz at unif.idr:4:1--5:1:
When unifying (1 {arg:158} : Int) -> FooBar and FooBar
Mismatch between:
        (1 {arg:158} : Int) -> FooBar
and
        FooBar
Main>

Observed Behavior

No error:

     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.3.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
*unif>

Background

The example above is distilled from some more verbose code I've been writing while learning Idris. I ran into the problem when refactoring the (correspondent of the) first line in the example above from

data FooBar = MkFoo | MkBar

to

data FooBar = MkFoo Int | MkBar

while forgetting to update function baz. The most worrying part is that the program compiles fine and baz always returns "Hello". This can lead to very difficult to trace down logical errors as a result of refactoring. I was happy to see that idris2 has spotted the problem right away :tada: but I am not ready to learn Idris using idris2 since I noticed a lot of parsing issues in idris2 that, as a novice, confuse me.