Evaluation of partial functions during conversion

[zanzix]

I seem to have found a bug in how Idris evaluates case trees.

Steps to Reproduce

Take the code from here: https://gist.github.com/zanzix/d5e5642e4aef80bd02ccf5d97116f3b7
Uncomment out the line eval Set (MapFst t) = ?zzz

Expected Behavior

Idris evaluates the case tree

Observed Behavior

Idris hangs forever

[gallais]

You are explicitly trying to evaluate a partial function at the type level. It's bound to end badly.

EvalTy (ProdK k1 k2) p = (EvalTy k1 (Fst p), EvalTy k2 (Snd p))
EvalTy s (Fst {k1=s, k2} a) = fst (EvalTy (ProdK s k2) a)

Agda is careful to turn off unfolding of partial functions however I am not sure it would be
appropriate for Idris given its goal to be more fast-and-loose with these questions.