Fix issue in case eval

newt/Debug.newt

@@ -22,15 +22,9 @@ Val : Type -> U
 Val ι = A
 Val (x ~> y) = Val x -> Val y
 
-id : {a : U} -> a -> a
-id x = x
-
 -- can't get Val to expand here.
-#check (\ x => \ y => \ z => id (Val (x ~> y ~> z))) : Type -> Type -> Type -> U
+#check (\ x => \ y => \ z => (Val (x ~> y ~> z))) : Type -> Type -> Type -> U
 
--- NOW something really strange here, the arrow in the goal type is backwards...
--- I think case eval is broken.
-
-foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> ξ))
-foo {σ} {τ} {ξ} = ? -- \ x y => x
+foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> σ))
+foo {σ} {τ} {σ} = \ x => \ y => x
 

src/Lib/Elab.idr

@@ -673,8 +673,6 @@ checkDone ctx [] body ty = do
   debug "DONE-> check body \{show body} at \{show ty}"
   -- TODO dump context function
   debugM $ dumpCtx ctx
-  debug "ENV \{show ctx.env}"
-  debug "TY \{show ctx.types}"
   -- I'm running an eval here to run case statements that are
   -- unblocked by lets in the env. (Tree.newt:cmp)
   -- The case eval code only works in the Tm -> Val case at the moment.

src/Lib/Eval.idr

@@ -45,15 +45,17 @@ vappSpine t [<] = pure t
 vappSpine t (xs :< x) = vapp !(vappSpine t xs) x
 
 evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
-evalCase env mode sc@(VRef _ nm y sp) (cc@(CaseCons name nms t) :: xs) =
+evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) =
   if nm == name
-    then go env sp nms
+    then do
+      debug "ECase \{nm} \{show sp} \{show nms} \{showTm t}"
+      go env (sp <>> []) nms
     else evalCase env mode sc xs
   where
-    go : Env -> SnocList Val -> List String -> M (Maybe Val)
-    go env (args :< arg) (nm :: nms) = go (arg :: env) args nms
-    go env args [] = Just <$> vappSpine !(eval env mode t) args
-    go env [<] rest = pure Nothing
+    go : Env -> List Val -> List String -> M (Maybe Val)
+    go env (arg :: args) (nm :: nms) = go (arg :: env) args nms
+    go env args [] = Just <$> vappSpine !(eval env mode t) ([<] <>< args)
+    go env [] rest = pure Nothing
 
 evalCase env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u)
 evalCase env mode sc cc = do

tests/black/CaseEval.newt

@@ -19,3 +19,14 @@ three = Refl
 
 addZero : {n : Nat} -> Eq (plus Z n) n
 addZero {n} = Refl
+
+infixr 1 _,_
+data Pair : U -> U -> U where
+  _,_ : {A B : U} -> A -> B -> Pair A B
+
+fst : {A B : U} -> Pair A B -> A
+fst (a,b) = a
+
+-- I had an ordering issue, but it didn't show up with only one constructor argument
+test : Eq (fst (Z, S Z)) Z
+test = Refl