diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda
index 1ef0a624..8c052e72 100644
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@@ -15,17 +15,17 @@ data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
-  FunctionMismatch : ∀ v w {M N} → (M ≡ val v) → (N ≡ val w) → (function ≢ valueType v) → RuntimeErrorᴱ H (M $ N)
-  BinopMismatch₁ : ∀ op v w {M N} → (M ≡ val v) → (N ≡ val w) → (number ≢ valueType v) → RuntimeErrorᴱ H (binexp M op N)
-  BinopMismatch₂ : ∀ op v w {M N} → (M ≡ val v) → (N ≡ val w) → (number ≢ valueType w) → RuntimeErrorᴱ H (binexp M op N)
-  UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
-  SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
+  FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w)
+  BinopMismatch₁ : ∀ v w {op} → (number ≢ valueType v) → RuntimeErrorᴱ H (binexp (val v) op (val w))
+  BinopMismatch₂ : ∀ v w {op} → (number ≢ valueType w) → RuntimeErrorᴱ H (binexp (val v) op (val w))
+  UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x)
+  SEGV : ∀ {a} → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
   app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
   app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
-  block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
+  block : ∀ {b B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
   bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
   bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)
 
 data RuntimeErrorᴮ H where
-  local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
+  local : ∀ {x M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
   return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda
index b0087f1c..e3522a24 100644
--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@@ -1,30 +1,30 @@
 {-# OPTIONS --rewriting #-}
-{-# OPTIONS --allow-unsolved-metas #-}
 
 module Luau.RuntimeError.ToString where
 
 open import Agda.Builtin.Float using (primShowFloat)
 open import FFI.Data.String using (String; _++_)
-open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
 open import Luau.RuntimeType.ToString using (runtimeTypeToString)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Syntax.ToString using (exprToString)
 open import Luau.Var.ToString using (varToString)
 open import Luau.Value.ToString using (valueToString)
-open import Luau.Syntax using (name; _$_)
+open import Luau.Syntax using (var; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_)
 
-errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
-errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String
+errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String
+errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String
 
--- errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
--- errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
--- errToStringᴱ (app₁ E) = errToStringᴱ E
--- errToStringᴱ (app₂ E) = errToStringᴱ E
--- errToStringᴱ (bin₁ E) = errToStringᴱ E
--- errToStringᴱ (bin₂ E) = errToStringᴱ E
--- errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString (name b)
--- errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t
-errToStringᴱ err = {!!}
+errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound"
+errToStringᴱ (addr a) (SEGV p) = "address " ++ addrToString a ++ " is unallocated"
+errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
+errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
+errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
+errToStringᴱ (binexp M op N) (BinopMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
+errToStringᴱ (binexp M op N) (BinopMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
+errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
+errToStringᴱ (binexp M op N) (bin₂ E) = errToStringᴱ N E
+errToStringᴱ (block b is B end) (block E) = errToStringᴮ B E ++ "\n  in call of function " ++ varToString (name b)
 
-errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
-errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"
+errToStringᴮ (local x ← M ∙ B) (local E) = errToStringᴱ M E ++ "\n  in definition of " ++ varToString (name x) 
+errToStringᴮ (return M ∙ B) (return E) = errToStringᴱ M E ++ "\n  in return statement"