pattern-matchingidristypecase

Pattern matching on Type in Idris

Probably it's elementary but I don't understand why the following function answers 1 for fnc Nat and also, for fnc Integer, which is not even included as a pattern.

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2
Solution

  • You can't pattern match on type and you shouldn't. When I compile your code I receive next error:

    warning - Unreachable case: fnc Nat

    This was already discussed earlier:

    1. Old discussion.
    2. Some similar question.
    3. Some similar issue on GitHub.

    UPDATE:

    Finally found more relevant question with answer:

    Why is typecase a bad thing?