[ fix ] compile time typecase for functions

[dunhamsteve]

Description

Compile time typecase gets stuck when comparing a type constructor case alt to either a Pi type or Type. This is happening because the code path for the happy case is present:

    tryAlt {more}
           env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN (Basic "->")) tag [s,t] sc)

but the non-matching case falls back to GotStuck. I've added cases for NoMatch for both Pi types and Type.

This issue was reported in the idrus-help-forum on discord.

Previously, given the code from the discord discussion:

data The : (a : Type) -> a -> Type where
  Is : (x : a) -> The a x

tcase : Type -> Type
tcase (The a _) = a
tcase a = a

the REPL would evaluate tcase (Int -> Int) to tcase (Int -> Int). Getting stuck at:

LOG eval.casetree.stuck:5: Got stuck matching ({arg:8} : [closure]) -> [closure] against Main.The {e:0} {e:1} => [0] {e:0}[0]

With the fix, it now reduces to Int -> Int. The case for Type is similar.