How to Compare Types for Equality?

Question

I attempted to compare a String and String, expecting True.

Idris> String == String
Can't find implementation for Eq Type

Then I expected False when comparing a String to a Bool.

Idris> String /= Bool
Can't find implementation for Eq Type

Am I missing an import?

Answer 1

You can't as it would break parametricity, which we have in Idris. We can't pattern match on types. But this would be necessary to write the Eq implementation, for example:

{- Doesn't work!
eqNat : Type -> Bool
eqNat Nat = True
eqNat _ = False -}

Also, if one could pattern match on types, they would be needed in the run-time. Right now types get erased when compiling.