diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies     #-}
-{-# LANGUAGE TypeOperators, TypeSynonymInstances                       #-}
+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies          #-}
+{-# LANGUAGE TypeOperators, TypeSynonymInstances, KindSignatures            #-}
 module Proof.Equational (
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
                          (:~:)(..), (:=:)
@@ -166,7 +166,7 @@
 coerce' Refl a = unsafeCoerce a
 {-# INLINE coerce' #-}
 
-class Proposition f where
+class Proposition (f :: k -> *) where
   type OriginalProp f n :: *
   unWrap :: f n -> OriginalProp f n
   wrap   :: OriginalProp f n -> f n
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.2.0.0
+version:             0.2.0.1
 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
 description:         A simple convenient library to write equational / preorder proof as in Agda.
 license:             BSD3