When (exactly) can equality be proposed between different types using '='?

Question

In the documentation, it says:

Equality in Idris is heterogeneous, meaning that we can even propose equalities between values in different types:
idris_not_php : 2 = "2"

That particular example compiles, but the hole is presented as being of type fromInteger 2 = "2". Given that fromInteger 2 can belong to any type that is an instance of Num, maybe the compiler isn't quite clever enough to deduce that the value of 2 is not a String?

In comparison, the following slightly different code fails to compile:

idris_not_php : S (S Z) = "2"

The compiler reports a type mismatch between Nat and String.

Also, the following does compile successfully:

Num String where
  (+) x y = y
  (*) x y = y
  fromInteger n = "2"

idris_not_php : 2 = "2"
idris_not_php = the (the String 2 = "2") Refl

And these two compile:

idris_not_php : S (S Z) ~=~ "2"
idris_not_php = ?hole

two_is_two : 2 ~=~ 2
two_is_two = Refl

Is there any particular rule about when = can be used between things that are of different types, or is it just a matter of using ~=~ when = doesn't work? Are ~=~ and = semantically identical, and if so, why is ~=~ even necessary?

Shersh Shersh · Accepted Answer · 2017-07-22T10:28:47

This answer have some theoretical notes about heterogeneous equality in Idris. And this answer has example of why you may need (~=~).

I just want to add a little about idris_not_php : 2 = "2" example. This can be type checked if you have Num instance for String type just as you did. Integral constants in Idris are polymorphic. Though, any reasonable program wouldn't have such instance for String because it doesn't make sense.

When (exactly) can equality be proposed between different types using '='?

1 Answers