Pattern matching on Type in Idris

Question

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

Shersh · Accepted Answer · 2017-08-13T12:12:08.080

3

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:

UPDATE:

Finally found more relevant question with answer:

Why is typecase a bad thing?

edited Aug 13 '17 at 12:12

answered Aug 01 '17 at 17:05

Shersh

9,019
3
33
61

1

@Shersh Thanks for the last link! Could you vote for reopening this perfectly good question? I think it's a shame it has been closed. – Anton Trunov Aug 14 '17 at 15:32
1

@AntonTrunov I also think so. Voted for reopening. – Shersh Aug 14 '17 at 15:51

score 1 · Answer 2 · answered Feb 27 '23 at 11:01

1

You can in fact now do this in Idris 2:

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2
fnc _ = 3

answered Feb 27 '23 at 11:01

Matt R

9,892
10
50
83

Pattern matching on Type in Idris

2 Answers2

Linked