[ fix ] compile time typecase for functions

idris-lang · Jul 2, 2024 · efce152 · efce152
1 parent 22c25e9
commit efce152
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 0 deletions.
diff --git a/src/Core/Normalise/Eval.idr b/src/Core/Normalise/Eval.idr
@@ -368,13 +368,18 @@ parameters (defs : Defs, topopts : EvalOpts)
     -- Type of type matching, in typecase
     tryAlt env loc opts fc stk (NType _ _) (ConCase (UN (Basic "Type")) tag [] sc)
          = evalTree env loc opts fc stk sc
+    tryAlt env loc opts fc stk (NType _ _) (ConCase _ _ _ _)
+         = pure NoMatch
     -- Arrow matching, in typecase
     tryAlt {more}
            env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN (Basic "->")) tag [s,t] sc)
        = evalConAlt {more} env loc opts fc stk [s,t]
                   [aty,
                    MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]
                   sc
+    tryAlt {more}
+           env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase nm tag args sc)
+       = pure NoMatch
     -- Delay matching
     tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)
          = evalTree env (ty :: arg :: loc) opts fc stk sc

diff --git a/tests/idris2/evaluator/evaluator005/TypeCase.idr b/tests/idris2/evaluator/evaluator005/TypeCase.idr
@@ -0,0 +1,7 @@
+data The : (a : Type) -> a -> Type where
+  Is : (x : a) -> The a x
+
+tcase : Type -> Type
+tcase (The a _) = a
+tcase a = a
+
diff --git a/tests/idris2/evaluator/evaluator005/expected b/tests/idris2/evaluator/evaluator005/expected
@@ -0,0 +1,4 @@
+1/1: Building TypeCase (TypeCase.idr)
+Main> Int -> Int
+Main> Type
+Main> Bye for now!
diff --git a/tests/idris2/evaluator/evaluator005/input b/tests/idris2/evaluator/evaluator005/input
@@ -0,0 +1,3 @@
+tcase (Int -> Int)
+tcase Type
+:q
diff --git a/tests/idris2/evaluator/evaluator005/run b/tests/idris2/evaluator/evaluator005/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 TypeCase.idr < input