diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr
index d8c2572..585231a 100644
--- a/Data/Profunctor/Types.idr
+++ b/Data/Profunctor/Types.idr
@@ -44,7 +44,7 @@ Functor f => Profunctor (Kleislimorphism f) where
 -- Examples of profunctors
 
 public export
-record Star (f : k -> Type) a (b : k) where
+record Star {0 k : Type} (f : k -> Type) a (b : k) where
   constructor MkStar
   applyStar : a -> f b
 
@@ -76,7 +76,7 @@ Functor f => Profunctor (Star f) where
 
 
 public export
-record Costar (f : k -> Type) (a : k) b where
+record Costar {0 k : Type} (f : k -> Type) (a : k) b where
   constructor MkCostar
   applyCostar : f a -> b
 
@@ -101,7 +101,7 @@ Functor f => Profunctor (Costar f) where
 
 
 public export
-record Tagged (a : k) b where
+record Tagged {0 k : Type} (a : k) b where
   constructor Tag
   getTagged : b