diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index 07b4937..b21d3cc 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -18,6 +18,7 @@
 module Data.Vec where
 
 import Relation.Equality (gcastWith)
+import Data.Kind         (Type)
 import Data.Nat
 import Data.Bool
 import Data.Char         (Char)
@@ -31,7 +32,7 @@ import qualified Data.TypeClass as T
 infixr 5 :-
 
 -- | The 'Vec' datatype
-data Vec ∷ ★ → ℕ → ★ where
+data Vec ∷ Type → ℕ → Type where
   Nil  ∷ Vec a Z                   -- ^ empty 'Vec', length 0
   (:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator
 
@@ -197,27 +198,27 @@ permutations xs@(_:-_) = concatMap (\(y,ys) → map (y:-) (permutations ys)) (se
 -- and a 'Vec' reduces the vector to a single value obtained
 -- by sequentially applying the operation from the left to the right.
 foldl ∷ (a → b → a) → a → Vec b n → a
-foldl _ x Nil       = x
+foldl  _  x Nil       = x
 foldl (⊗) x (y :- ys) = foldl (⊗) (x ⊗ y) ys
 
 
 -- | Same as "fold" but reduces the vector in the opposite
 -- direction: from the right to the left.
 foldr ∷ (a → b → b) → b → Vec a n → b
-foldr _ x Nil     = x
+foldr  _  x Nil     = x
 foldr (⊗) x (y:-ys) = y ⊗ (foldr (⊗) x ys)
 
 
 -- | Variant of 'foldl' which requires no starting value but
 -- applies only on nonempty 'Vec'
 foldl₁ ∷ (a → a → a) → Vec a (S n) → a
-foldl₁ _   (x :- Nil)     = x
+foldl₁  _  (x :- Nil)     = x
 foldl₁ (⊗) (x :- y :- ys) = foldl₁ (⊗) (x ⊗ y :- ys)
 
 
 -- | As for 'foldl', a variant of 'foldr' with no starting point
 foldr₁ ∷ (a → a → a) → Vec a (S n) → a
-foldr₁ _   (x :- Nil)     = x
+foldr₁  _  (x :- Nil)     = x
 foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys))