Made EVal more specific & fixed evaluation

2 files changed, 3 insertions, 3 deletions

diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs
index a9c16de..ada273a 100644
--- a/events/src/Events/Spec/Eval.hs
+++ b/events/src/Events/Spec/Eval.hs
@@ -16,7 +16,7 @@ shift = shift' LZ
     shift'  l     (EVar v)   = EVar $ shiftElem l v
     shift'  l     (ELam b)   = ELam $ shift' (LS l) b
     shift'  l     (EApp f x) = EApp (shift' l f) (shift' l x)
-    shift'  l     (EVal _)   = undefined
+    shift'  _     (EVal v)   = EVal v
   
     shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2)
     shiftElem LZ e = ES e
@@ -35,7 +35,7 @@ beta = flip beta' LZ
     beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v)
     beta' e  l     (ELam b)      = ELam $ beta' e (LS l) b
     beta' e  l     (EApp f a)    = EApp (beta' e l f) (beta' e l a)
-    beta' _  l     (EVal _)      = undefined
+    beta' _  _     (EVal v)      = EVal v
 
 evalExpr :: Expr m '[] t -> Val m t
 evalExpr (EVal a)                 = a
diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs
index d9d1ef1..1f319c7 100644
--- a/events/src/Events/Spec/Types.hs
+++ b/events/src/Events/Spec/Types.hs
@@ -18,7 +18,7 @@ import Events.Types
 -- | A functional language reminiscent of typed lambda calculus with monadic
 -- side-effects and foreign primitives
 data Expr :: (* -> *) -> [*] -> * -> * where
-  EVal :: Val m a -> Expr m ctx a
+  EVal :: Val m a ~ m a => Val m a -> Expr m ctx a
   EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b
   EVar :: Elem a ctx -> Expr m ctx a
   ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res)