diff --git a/mini-egison.cabal b/mini-egison.cabal
--- a/mini-egison.cabal
+++ b/mini-egison.cabal
@@ -1,7 +1,7 @@
 cabal-version: 1.12
 
 name:           mini-egison
-version:        0.1.4
+version:        0.1.5
 synopsis:    Template Haskell Implementation of Egison Pattern Matching
 description: This package provides the pattern-matching facility that fulfills the following three criteria for practical pattern matching for non-free data types\: (i) non-linear pattern matching with backtracking; (ii) extensibility of pattern-matching algorithms; (iii) ad-hoc polymorphism of patterns.
   Non-free data types are data types whose data have no standard forms.
@@ -44,6 +44,17 @@
     , regex-compat
     , template-haskell
   default-language: Haskell2010
+  default-extensions:
+      TemplateHaskell
+    , QuasiQuotes
+    , GADTs
+    , ExistentialQuantification
+    , DataKinds
+    , MultiParamTypeClasses
+    , TypeFamilies
+    , TypeOperators
+    , FlexibleInstances
+    , TupleSections
   ghc-options:  -O3
   
 test-suite mini-egison-test
@@ -54,13 +65,16 @@
       Paths_mini_egison
   hs-source-dirs:
       test
-  ghc-options: -O3
   build-depends:
       base >=4.7 && <5
     , mini-egison
     , hspec
     , primes
   default-language: Haskell2010
+  default-extensions:
+      QuasiQuotes
+    , GADTs
+  ghc-options: -O3
 
 Executable cdcl
   Main-is:             cdcl.hs
diff --git a/sample/cdcl.hs b/sample/cdcl.hs
--- a/sample/cdcl.hs
+++ b/sample/cdcl.hs
@@ -1,8 +1,7 @@
-{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE QuasiQuotes           #-}
-{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeOperators         #-}
 
 import           Data.List
diff --git a/src/Control/Egison/Core.hs b/src/Control/Egison/Core.hs
--- a/src/Control/Egison/Core.hs
+++ b/src/Control/Egison/Core.hs
@@ -1,10 +1,3 @@
-{-# LANGUAGE DataKinds                 #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE MultiParamTypeClasses     #-}
-{-# LANGUAGE TypeFamilies              #-}
-{-# LANGUAGE TypeOperators             #-}
-
 -- | Definitions of data types for patterns, matchers, match clauses, matching states, and matching atoms.
 
 module Control.Egison.Core (
@@ -39,20 +32,34 @@
 -- @ctx@ is an intermediate pattern-matching result that is a type of a list of data bound in the left-side of the pattern.
 -- @vs@ is a list of types bound to the pattern variables in this pattern.
 data Pattern a m ctx vs where
-  Wildcard :: Pattern a m ctx '[]
-  PatVar :: String -> Pattern a m ctx '[a]
-  AndPat :: Pattern a m ctx vs -> Pattern a m (ctx :++: vs) vs' -> Pattern a m ctx (vs :++: vs')
-  OrPat  :: Pattern a m ctx vs -> Pattern a m ctx vs -> Pattern a m ctx vs
-  NotPat :: Pattern a m ctx '[] -> Pattern a m ctx '[]
-  PredicatePat :: (HList ctx -> a -> Bool) -> Pattern a m ctx '[]
+  Wildcard     :: (Matcher m a) => Pattern a m ctx '[]
+  PatVar       :: (Matcher m a) => String -> Pattern a m ctx '[a]
+  AndPat       :: (Matcher m a) => Pattern a m ctx vs -> Pattern a m (ctx :++: vs) vs' -> Pattern a m ctx (vs :++: vs')
+  OrPat        :: (Matcher m a) => Pattern a m ctx vs -> Pattern a m ctx vs -> Pattern a m ctx vs
+  NotPat       :: (Matcher m a) => Pattern a m ctx '[] -> Pattern a m ctx '[]
+  PredicatePat :: (Matcher m a) => (HList ctx -> a -> Bool) -> Pattern a m ctx '[]
   -- | User-defined pattern; pattern is a function that takes a target, an intermediate pattern-matching result, and a matcher and returns a list of lists of matching atoms.
-  Pattern :: Matcher m a => (HList ctx -> m -> a -> [MList ctx vs]) -> Pattern a m ctx vs
+  Pattern      :: (Matcher m a) => (HList ctx -> m -> a -> [MList ctx vs]) -> Pattern a m ctx vs
 
 -- | The @Matcher@ class is used to declare that @m@ is a matcher for data of a type @a@.
+-- For example,
+-- 
+-- > instance (Matcher m a) => Matcher (Multiset m) [a]
+-- 
+-- declares that "let @m@ be a matcher for @a@, @(Multiset m)@ is a matcher for @[a]@".
 class Matcher m a
 
 -- | A match clause of a match expression whose target data is @a@ and matcher is @m@.
 -- The body of the match clause is evaluated to @b@.
+-- 
+-- The first argument of @MatchClause@ is a pattern for @a@ with a matcher @m@.
+-- This pattern makes a binding whose type is @vs@.
+-- The second argument of @MatchClause@ is a function that takes a heterogeneous list containing @vs@ and returns @b@.
+-- 
+-- @vs@ is existentially quantified because generally each pattern of the list of match clauses in a pattern-matching expression makes different bindings.
+-- 
+-- Several samples of @MatchClause@s are found in "Control.Egison.QQ".
+-- The 'Control.Egison.QQ.mc' quasiquoter allows us to describe a match clause in user-friendly syntax.
 data MatchClause a m b = forall vs. (Matcher m a) => MatchClause (Pattern a m '[] vs) (HList vs -> b)
 
 ---
@@ -61,15 +68,18 @@
 
 -- | A matching state.
 -- A matching state consists of an intermediate pattern-matching result and a stack of matching atoms.
+-- @vs@ is a list of types bound to the pattern variables in the pattern after processing @MState@.
 data MState vs where
   MState :: vs ~ (xs :++: ys) => HList xs -> MList xs ys -> MState vs
 
 -- | A matching atom.
 -- @ctx@ is a intermediate pattern-matching result.
 -- @vs@ is a list of types bound to the pattern variables by processing this matching atom.
+-- The types of a target @a@ and a matcher @m@ are existentially quantified each matching atom in a stack of matching atoms contains a pattern, matcher, and target for a different type.
 data MAtom ctx vs = forall a m. (Matcher m a) => MAtom (Pattern a m ctx vs) m a
 
--- | A stack of matching atoms
+-- | A list of matching atoms.
+-- It is used to represent a stack of matching atoms in a matching state.
 data MList ctx vs where
   MNil :: MList ctx '[]
   MCons :: MAtom ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys)
diff --git a/src/Control/Egison/Match.hs b/src/Control/Egison/Match.hs
--- a/src/Control/Egison/Match.hs
+++ b/src/Control/Egison/Match.hs
@@ -1,7 +1,3 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs     #-}
-{-# LANGUAGE TypeOperators             #-}
-
 -- | Pattern-matching expressions.
 
 module Control.Egison.Match (
@@ -88,7 +84,7 @@
     NotPat p ->
       [MState rs atoms | null $ processMStatesAll [[MState rs $ MCons (MAtom p m tgt) MNil]]]
     PredicatePat f -> [MState rs atoms | f rs tgt]
-processMState (MState rs MNil) = [MState rs MNil] -- TODO: shold not reach here but reaches here.
+processMState (MState rs MNil) = undefined -- or [MState rs MNil] -- TODO: shold not reach here but reaches here.
 
 patVarProof :: HList xs -> HList '[a] -> MList (xs :++: '[a]) ys -> ((xs :++: '[a]) :++: ys) :~: (xs :++: ('[a] :++: ys))
 patVarProof HNil _ _ = Refl
diff --git a/src/Control/Egison/Matcher.hs b/src/Control/Egison/Matcher.hs
--- a/src/Control/Egison/Matcher.hs
+++ b/src/Control/Egison/Matcher.hs
@@ -42,7 +42,7 @@
 -- | A matcher for data types that are instances of @Eq@.
 -- The @Eql@ matcher can handle a pattern variable, a wildcard, and a value pattern.
 data Eql = Eql
-instance Matcher Eql a
+instance (Eq a) => Matcher Eql a
 
 instance Eq a => ValuePat Eql a where
   valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])
@@ -86,7 +86,7 @@
        -> Pattern a m (ctx :++: xs) ys
        -> Pattern a m ctx (xs :++: ys)
 
--- | a matcher for a list.
+-- | A matcher for a list.
 newtype List m = List m
 instance (Matcher m a) => Matcher (List m) [a]
 
@@ -110,7 +110,7 @@
 splits []     = [([], [])]
 splits (x:xs) = ([], x:xs) : [(x:ys, zs) | (ys, zs) <- splits xs]
 
--- | a matcher for a multiset.
+-- | A matcher for a multiset.
 -- When we regard a collection as a multiset, the order of elements is ignored but the number of times an element appears in the collection is counted.
 newtype Multiset m = Multiset m
 instance (Matcher m a) => Matcher (Multiset m) [a]
@@ -130,7 +130,7 @@
                                                    (matchAll tgt (List m) [[mc| join $hs (cons $x $ts) => (x, hs ++ ts) |]]))
   join p1 p2 = undefined
 
--- | a matcher for a set.
+-- | A matcher for a set. Both the order and the repetition of elements are ignored.
 newtype Set m = Set m
 instance (Matcher m a) => Matcher (Set m) [a]
 
diff --git a/src/Control/Egison/QQ.hs b/src/Control/Egison/QQ.hs
--- a/src/Control/Egison/QQ.hs
+++ b/src/Control/Egison/QQ.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TupleSections   #-}
-
 -- | Quasiquotation for rewriting a match clause.
 
 module Control.Egison.QQ (
@@ -19,59 +16,60 @@
 import           Text.Regex
 
 -- | A quasiquoter for rewriting a match clause.
---
--- * /Wildcards/
---
+-- This quasiquoter is useful for generating a 'MatchClause' in user-friendly syntax.
+-- 
+-- === Wildcards
+-- 
 -- A match clause that contains a wildcard
---
+-- 
 -- > [mc| _ => "Matched" |]
---
--- is rewrited to
---
+-- 
+-- is rewritten to
+-- 
 -- > MatchClause Wildcard
 -- >             (\HNil -> "Matched")
---
--- * /Pattern variables/
---
+-- 
+-- === Pattern variables
+-- 
 -- A match clause that contains a pattern variable
---
+-- 
 -- > [mc| $x => x |]
---
--- is rewrited to
---
+-- 
+-- is rewritten to
+-- 
 -- > MatchClause (PatVar "x")
 -- >             (\HCons x HNil -> x)
---
--- * /Value patterns/
---
+-- 
+-- === Value patterns
+-- 
 -- A match clause that contains a value pattern
---
+-- 
 -- > [mc| cons $x (cons $y (cons #(x + 1) (cons $z nil))) => (x, y, z) |]
---
--- is rewrited to
---
+-- 
+-- is rewritten to
+-- 
 -- > MatchClause (cons (PatVar "x") (cons (PatVar "y") (cons (ValuePat (\HCons x (HCons (y HNil)) -> x + 1)) (cons (PatVar "z") nil))))
 -- >             (\HCons x (HCons (y (HCons z HNil))) -> (x, y, z))
---
--- * /And-patterns/
---
+-- 
+-- === And-patterns
+-- 
 -- A match clause that contains an and-pattern
---
+-- 
 -- > [mc| (& (cons _ _) $x) => x |]
---
--- is rewrited to
---
+-- 
+-- is rewritten to
+-- 
 -- > MatchClause (AndPat (cons Wildcard Wildcard) (PatVar "x"))
 -- >             (\HCons x HNil -> x)
---
--- * /Or-patterns/
---
+-- 
+-- === Or-patterns
+-- 
 -- A match clause that contains an or-pattern
---
+-- 
 -- > [mc| (| nil (cons _ _)) => "Matched" |]
---
--- is rewrited to
---
+-- 
+-- is rewritten to
+-- 
 -- > MatchClause (OrPat nil (cons Wildcard Wildcard))
 -- >             (\HNil -> "Matched")
 mc :: QuasiQuoter
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE GADTs       #-}
-{-# LANGUAGE QuasiQuotes #-}
-
 module Spec (spec) where
 
 import           Control.Egison