diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index dc66a8b..25f151b 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -22,7 +22,7 @@ data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
 %name Telescope tel
 
 public export
-Telescope' : Type -> (from, to : Nat) -> Type
+Telescope' : (a : Type) -> (from, to : Nat) -> Type
 Telescope' a = Telescope (\_ => a)
 
 ||| a global context is actually just a telescope over no existing bindings
@@ -31,7 +31,7 @@ Context : (tm : Nat -> Type) -> (len : Nat) -> Type
 Context tm len = Telescope tm 0 len
 
 public export
-Context' : Type -> (len : Nat) -> Type
+Context' : (a : Type) -> (len : Nat) -> Type
 Context' a = Context (\_ => a)