idris-lang/Idris2

Pattern matching 0 on numbers

maheshkronecker opened this issue · 2 comments

maheshkronecker commented

Hello. I often stumble on this kind of error when attempting to pattern match on numbers. I'm not sure whether it is an issue or not. Could you please let me know if this is a real issue or normal behavior (and then possibly why) ?

Steps to Reproduce

null : Num a => a -> Bool
null 0 = True
null _ = False

Expected Behavior

I would expect it to type check. In Haskell, we would have to add the class constraint Eq a for null to be accepted by the compiler. However, this still does not work in Idris 2.

Observed Behavior

Type checking error :

Patterns for null require matching on different types.
buzden commented

I would expect this to not to typecheck, because what you are effectively trying to match on is a function application. 0 is in fact an application of fromInteger to an interger 0, thus you have fromInteger 0 on the LHS.

Since the clause of your function is typechecked for any type a before knowing any particular a, this function whould never reduce to any expression, thus it is impossible to match on this abstract value.

  • 👍1
maheshkronecker commented

OK, got it, thank you. I'll close the issue.

  • 👍1