diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -19,7 +19,7 @@
   | matchDFS e e [C, ...]      -- match expression
   | Something                  -- Something built-in matcher
 
-C = [mc| p => e]               -- match clause
+C = [mc| p => e |]             -- match clause
 
 p = _                          -- wildcard
   | $x                         -- pattern variable
@@ -38,7 +38,7 @@
 This expression returns a list of a single element because there is only one decomposition.
 
 ```
-matchAll [1,2,3] (List Integer) [[mc| cons $x $xs => (x, xs)]]
+matchAll [1,2,3] (List Integer) [[mc| cons $x $xs => (x, xs)|]]
 -- [(1,[2,3])]
 ```
 
@@ -50,7 +50,7 @@
 For example, by changing the matcher of the above `matchAll` from `List Integer` to `Multiset Integer`, the evaluation result changes as follows:
 
 ```
-matchAll [1,2,3] (Multiset Integer) [[mc| cons $x $xs => (x, xs)]]
+matchAll [1,2,3] (Multiset Integer) [[mc| cons $x $xs => (x, xs)|]]
 -- [(1,[2,3]),(2,[1,3]),(3,[1,2])]
 ```
 
@@ -71,17 +71,86 @@
 A non-linear pattern is effectively used for expressing the pattern.
 
 ```
-matchAll [1,2,5,9,4] (Multiset Integer) [[mc| cons $x (cons #(x+1) _) => x]]
+matchAll [1,2,5,9,4] (Multiset Integer) [[mc| cons $x (cons #(x+1) _) => x|]]
 -- [1,4]
 ```
 
 ### The `match` expression
 
-preparing...
+The `match` expression takes a target, a matcher, and match-clauses as the `matchAll` expression.
+The `match` expression returns only the evaluation result of the first pattern-matching result.
 
+```
+match [1,2,5,9,4] (Multiset Integer) [[mc| cons $x (cons #(x+1) _) => x|]]
+-- 1
+```
+
+The `match` expression is simply implemented using `matchAll` as follows:
+
+```
+match tgt m cs = head $ matchAll tgt m cs
+```
+
 ### `matchAllDFS` and `matchDFS`
 
-preparing...
+The `matchAll` and `match` expressions traverse a search tree for pattern matching in breadth-first order.
+The reason of the default breadth-first traversal is because to enumerate all the successful pattern-matching results even when they are infinitely many.
+For example, all the pairs of natural numbers can be enumerated by the following `matchAll` expression:
+
+```
+take 10 (matchAll [1..] (Set Integer)
+           [[mc| cons $x (cons $y _) => (x, y) |]])
+-- [(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(1,4),(2,3),(3,2),(4,1)]
+```
+
+If we change the above `matchAll` to `matchAllDFS`, the order of the pattern-matching results changes as follows:
+
+```
+take 10 (matchAllDFS [1..] (Set Integer)
+           [[mc| cons $x (cons $y _) => (x, y) |]])
+-- [(1,1),(1,2),(1,3),(1,4),(1,5),(1,6),(1,7),(1,8),(1,9),(1,10)]
+```
+
+There are cases where depth-first traversal is suitable because the depth-first order of pattern-matching results is preferable.
+Furthermore, `matchAllDFS` is more efficient than `matchAll`.
+It would be better to use `matchAllDFS` instead of `matchAll` when the both expressions can be used.
+
+### Matcher definitions
+
+preparing
+
+```
+matchAll (1,2) UnorderedEqlPair [[mc| uepair #2 $x => x |]]
+-- [1]
+matchAll (1,2) (UnorderedPair Eql) [[mc| upair #2 $x => x |]]
+-- [1]
+```
+
+```
+data UnorderedEqlPair = UnorderedEqlPair
+instance (Eq a) => Matcher UnorderedEqlPair (a, a)
+
+uepair :: (Eq a)
+       => Pattern a Eql ctx xs
+       -> Pattern a Eql (ctx :++: xs) ys
+       -> Pattern (a, a) UnorderedEqlPair ctx (xs :++: ys)
+uepair p1 p2 = Pattern (\_ UnorderedEqlPair (t1, t2) ->
+                          [twoMAtoms (MAtom p1 Eql t1) (MAtom p2 Eql t2)
+                          ,twoMAtoms (MAtom p1 Eql t2) (MAtom p2 Eql t1)])
+```
+
+```
+data UnorderedPair m = UnorderedPair m
+instance Matcher m a => Matcher (UnorderedPair m) (a, a)
+
+upair :: (Matcher m a , a ~ (b, b), m ~ (UnorderedPair m'), Matcher m' b)
+      => Pattern b m' ctx xs
+      -> Pattern b m' (ctx :++: xs) ys
+      -> Pattern a m ctx (xs :++: ys)
+upair p1 p2 = Pattern (\_ (UnorderedPair m') (t1, t2) ->
+                         [twoMAtoms (MAtom p1 m' t1) (MAtom p2 m' t2)
+                         ,twoMAtoms (MAtom p1 m' t2) (MAtom p2 m' t1)])
+```
 
 ## Samples
 
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.1
+version:        0.1.2
 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,7 +44,8 @@
     , regex-compat
     , template-haskell
   default-language: Haskell2010
-
+  ghc-options:  -O3
+  
 test-suite mini-egison-test
   type: exitcode-stdio-1.0
   main-is: Test.hs
@@ -53,10 +54,20 @@
       Paths_mini_egison
   hs-source-dirs:
       test
-  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -O3
   build-depends:
       base >=4.7 && <5
     , mini-egison
     , hspec
     , primes
   default-language: Haskell2010
+
+Executable cdcl
+  Main-is:             cdcl.hs
+  Build-depends:
+      base >=4.7 && <5
+    , mini-egison
+    , sort
+  Hs-Source-Dirs:      sample
+  default-language: Haskell2010
+  ghc-options:  -O3
diff --git a/sample/cdcl.hs b/sample/cdcl.hs
new file mode 100644
--- /dev/null
+++ b/sample/cdcl.hs
@@ -0,0 +1,202 @@
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuasiQuotes           #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE TypeOperators         #-}
+
+import           Data.List
+import           Data.Sort
+import           Control.Egison hiding (Integer)
+import qualified Control.Egison as M
+import           Debug.Trace
+
+
+
+-- Literal matcher = Integer matcher
+data Literal = Literal
+instance Integral a => Matcher Literal a
+
+instance Integral a => ValuePat Literal a where
+  valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])
+
+-- Stage matcher = Integer matcher
+data Stage = Stage
+instance Integral a => Matcher Stage a
+
+instance Integral a => ValuePat Stage a where
+  valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])
+
+-- Matchers for assignments
+type TaggedLiteral = (Integer, Integer) -- a tuple of a variable and a stage
+
+data Assign = Deduced TaggedLiteral [TaggedLiteral]
+            | Guessed TaggedLiteral
+  deriving (Show)
+
+data Assignment = Assignment
+instance Matcher Assignment Assign
+
+deduced :: Pattern TaggedLiteral (Pair Literal Stage) ctx xs
+        -> Pattern [TaggedLiteral] (Multiset (Pair Literal Stage)) (ctx :++: xs) ys
+        -> Pattern Assign Assignment ctx (xs :++: ys)
+deduced p1 p2 = Pattern (\_ _ tgt -> case tgt of
+                                       Deduced l ls -> [twoMAtoms (MAtom p1 (Pair Literal Stage) l)
+                                                                  (MAtom p2 (Multiset (Pair Literal Stage)) ls)]
+                                       _ -> [])
+
+guessed :: Pattern TaggedLiteral (Pair Literal Stage) ctx xs
+        -> Pattern Assign Assignment ctx xs
+guessed p1 = Pattern (\_ _ tgt -> case tgt of
+                                    Guessed l -> [oneMAtom (MAtom p1 (Pair Literal Stage) l)]
+                                    _ -> [])
+
+whichever :: Pattern TaggedLiteral (Pair Literal Stage) ctx xs
+          -> Pattern Assign Assignment ctx xs
+whichever p1 = Pattern (\_ _ tgt -> case tgt of
+                                      Deduced l _ -> [oneMAtom (MAtom p1 (Pair Literal Stage) l)]
+                                      Guessed l -> [oneMAtom (MAtom p1 (Pair Literal Stage) l)])
+
+--
+-- VSIDS
+--
+toCNF :: [[Integer]] -> [([Integer], [Integer])]
+toCNF cs = map (\c -> (c, c)) cs
+
+fromCNF ::  [([Integer], [Integer])] -> [[Integer]]
+fromCNF cnf = map (\(c1, _) -> c1) cnf
+
+initVars :: [Integer] -> [(Integer, Integer)]
+initVars vs = map (\v -> (negate v, 0)) vs ++ map (\v -> (v, 0)) vs
+
+addVars :: [Integer] -> [(Integer, Integer)] -> [(Integer, Integer)]
+addVars vs vars =
+  matchDFS (vs, vars) (Pair (List Literal) (List (Pair Literal M.Integer)))
+    [[mc| pair nil _ => sortBy (\(_, c1) (_, c2) -> opposite (compare c1 c2)) vars |],
+     [mc| pair (cons $v $vs2) (join $hs (cons (pair #v $c) $ts)) =>
+          addVars vs2 (hs ++ (v, c + 1) : ts) |]]
+ where
+   opposite LT = GT
+   opposite GT = LT
+   opposite EQ = EQ
+
+deleteVar :: Integer -> [(Integer, Integer)] -> [(Integer, Integer)]
+deleteVar v vars =
+  matchDFS vars (Multiset (Pair Literal M.Integer))
+    [[mc| cons (pair #v _) (cons (pair #(negate v) _) $vars2) => vars2 |]]
+
+--
+-- Utility functions for literals and cnfs
+--
+getStage :: Integer -> [Assign] -> Integer
+getStage l trail =
+  matchDFS trail (List Assignment)
+    [[mc| join _ (cons (whichever (pair #(negate l) $s)) _) => s |]]
+
+deleteLiteral :: Integer -> [([Integer], [Integer])] -> [([Integer], [Integer])]
+deleteLiteral l cnf =
+  map (\(c1, c2) -> (matchAll c1 (Multiset Literal)
+                       [[mc| cons (& (not #l) $m) _ => m |]],
+                     c2))
+      cnf
+
+deleteClausesWith :: Integer -> [([Integer], [Integer])] -> [([Integer], [Integer])]
+deleteClausesWith l cnf =
+  matchAll cnf (Multiset (Pair (Multiset Literal) (Multiset Literal)))
+    [[mc| cons (& (pair (not (cons #l _)) _) $c) _ => c |]]
+
+assignTrue :: Integer -> [([Integer], [Integer])] -> [([Integer], [Integer])]
+assignTrue l cnf =
+  deleteLiteral (negate l) (deleteClausesWith l cnf)
+
+--
+-- Unit propagation
+--
+unitPropagate :: Integer -> [([Integer], [Integer])] -> [Assign] -> ([([Integer], [Integer])], [Assign])
+unitPropagate stage cnf trail = unitPropagate' stage cnf trail trail
+
+unitPropagate' :: Integer -> [([Integer], [Integer])] -> [Assign] -> [Assign] -> ([([Integer], [Integer])], [Assign])
+unitPropagate' stage cnf trail otrail =
+  matchDFS trail (List Assignment)
+    [[mc| cons (whichever (pair $l _)) $trail2 => unitPropagate' stage (assignTrue l cnf) trail2 otrail |],
+     [mc| _ => unitPropagate'' stage cnf otrail |]]
+   
+unitPropagate'' :: Integer -> [([Integer], [Integer])] -> [Assign] -> ([([Integer], [Integer])], [Assign])
+unitPropagate'' stage cnf trail =
+  matchDFS cnf (Multiset (Pair (Multiset Literal) (Multiset Literal)))
+    [[mc| cons (pair nil _) _ => (cnf, trail) |],
+     [mc| cons (pair (cons $l nil) (cons #l $rs)) _ =>
+          unitPropagate'' stage (assignTrue l cnf) 
+                          ([(Deduced (l, stage) (map (\r -> (r, (getStage r trail))) rs))] ++ trail) |],
+     [mc| _ => (cnf, trail) |]]
+
+--
+-- Learning
+--
+
+learn :: Integer -> [(Integer, Integer)] -> [Assign] -> (Integer, [Integer])
+learn stage cl trail =
+  matchDFS (trail, cl) (Pair (List Assignment) (Multiset (Pair Literal M.Integer))) -- must be matchDFS
+    [[mc| pair _ (not (cons (pair _ #stage) (cons (pair _ #stage) _))) =>
+          (minimum (map (\(_, c) -> c) cl), map (\(l, _) -> l) cl) |],
+     [mc| pair (join _ (cons (deduced (pair $l #stage) $ds) $trail2))
+               (cons (pair #(negate l) #stage) $rs) =>
+          learn stage (union rs ds) trail2 |]]
+
+--
+-- Backjumping
+--
+
+backjump :: Integer -> [Assign] -> [Assign]
+backjump stage trail =
+  matchDFS trail (List Assignment)
+    [[mc| join _ (& (cons (guessed (pair _ #stage)) _) $trail2) => trail2 |],
+     [mc| _ => [] |]]
+
+--
+-- Guess
+--
+
+guess vars trail =
+  matchDFS (vars, trail) (Pair (List (Pair Literal M.Integer)) (List Assignment)) -- must be matchDFS
+    [[mc| pair (join _ (cons (pair $l _) _))
+               (not (join _ (cons (whichever (pair (| #l #(negate l)) _)) _))) =>
+          negate l |]]
+
+--
+-- CDCL main
+--
+
+cdcl :: [Integer] -> [[Integer]] -> Bool
+cdcl vars cnf = cdcl' 0 0 (initVars vars) (toCNF cnf) []
+
+cdcl' :: Integer -> Integer -> [(Integer, Integer)] -> [([Integer], [Integer])] -> [Assign] -> Bool
+cdcl' count stage vars cnf trail =
+  let (cnf2, trail2) = unitPropagate stage cnf trail in
+--  let (cnf2, trail2) = unitPropagate stage cnf (trace (show trail) trail) in -- debug
+    matchDFS (cnf2, trail2) (Pair (Multiset (Pair (Multiset Literal) (Multiset Literal))) (List Assignment))
+      [[mc| pair nil _ => True |],
+       [mc| pair (cons (pair nil $cc) _) (join _ (cons (guessed (pair $l #stage)) $trail3)) =>
+            let (s, lc) = learn stage (map (\l -> (l, (getStage l trail2))) cc) trail2 in
+            let trail4 = backjump s trail3 in
+              cdcl' (count + 1) s (addVars lc vars) ((lc, lc):cnf) trail4 |],
+       [mc| pair (cons (pair nil $cc) _) _ => False |],
+       [mc| _ =>
+            let g = guess vars trail2 in
+              cdcl' (count + 1) (stage + 1) vars cnf (Guessed (g, stage + 1):trail2) |]]
+
+main = do
+--  putStrLn $ show $ cdcl [] []
+--  putStrLn $ show $ cdcl [] [[]]
+--  putStrLn $ show $ cdcl [1] [[1]]
+--  putStrLn $ show $ cdcl [1,2] [[1],[1,2]]
+--  putStrLn $ "Problem 20"
+--  putStrLn $ show $ cdcl [1..20] problem20 -- 0.293 sec
+  putStrLn $ "Problem 50"
+  putStrLn $ show $ cdcl [1..50] problem50 -- 2.570 sec
+
+problem20 =
+  [[4,-18,19],[3,18,-5],[-5,-8,-15],[-20,7,-16],[10,-13,-7],[-12,-9,17],[17,19,5],[-16,9,15],[11,-5,-14],[18,-10,13],[-3,11,12],[-6,-17,-8],[-18,14,1],[-19,-15,10],[12,18,-19],[-8,4,7],[-8,-9,4],[7,17,-15],[12,-7,-14],[-10,-11,8],[2,-15,-11],[9,6,1],[-11,20,-17],[9,-15,13],[12,-7,-17],[-18,-2,20],[20,12,4],[19,11,14],[-16,18,-4],[-1,-17,-19],[-13,15,10],[-12,-14,-13],[12,-14,-7],[-7,16,10],[6,10,7],[20,14,-16],[-19,17,11],[-7,1,-20],[-5,12,15],[-4,-9,-13],[12,-11,-7],[-5,19,-8],[1,16,17],[20,-14,-15],[13,-4,10],[14,7,10],[-5,9,20],[10,1,-19],[-16,-15,-1],[16,3,-11],[-15,-10,4],[4,-15,-3],[-10,-16,11],[-8,12,-5],[14,-6,12],[1,6,11],[-13,-5,-1],[-7,-2,12],[1,-20,19],[-2,-13,-8],[15,18,4],[-11,14,9],[-6,-15,-2],[5,-12,-15],[-6,17,5],[-13,5,-19],[20,-1,14],[9,-17,15],[-5,19,-18],[-12,8,-10],[-18,14,-4],[15,-9,13],[9,-5,-1],[10,-19,-14],[20,9,4],[-9,-2,19],[-5,13,-17],[2,-10,-18],[-18,3,11],[7,-9,17],[-15,-6,-3],[-2,3,-13],[12,3,-2],[-2,-3,17],[20,-15,-16],[-5,-17,-19],[-20,-18,11],[-9,1,-5],[-19,9,17],[12,-2,17],[4,-16,-5]]
+
+problem50 =
+  [[18,-8,29],[-16,3,18],[-36,-11,-30],[-50,20,32],[-6,9,35],[42,-38,29],[43,-15,10],[-48,-47,1],[-45,-16,33],[38,42,22],[-49,41,-34],[12,17,35],[22,-49,7],[-10,-11,-39],[-28,-36,-37],[-13,-46,-41],[21,-4,9],[12,48,10],[24,23,15],[-8,-41,-43],[-44,-2,-35],[-27,18,31],[47,35,6],[-11,-27,41],[-33,-47,-45],[-16,36,-37],[27,-46,2],[15,-28,10],[-38,46,-39],[-33,-4,24],[-12,-45,50],[-32,-21,-15],[8,42,24],[30,-49,4],[45,-9,28],[-33,-47,-1],[1,27,-16],[-11,-17,-35],[-42,-15,45],[-19,-27,30],[3,28,12],[48,-11,-33],[-6,37,-9],[-37,13,-7],[-2,26,16],[46,-24,-38],[-13,-24,-8],[-36,-42,-21],[-37,-19,3],[-31,-50,35],[-7,-26,29],[-42,-45,29],[33,25,-6],[-45,-5,7],[-7,28,-6],[-48,31,-11],[32,16,-37],[-24,48,1],[18,-46,23],[-30,-50,48],[-21,39,-2],[24,47,42],[-36,30,4],[-5,28,-1],[-47,32,-42],[16,37,-22],[-43,42,-34],[-40,39,-20],[-49,29,6],[-41,-3,39],[-16,-12,43],[24,22,3],[47,-45,43],[45,-37,46],[-9,26,5],[-3,23,-13],[5,-34,13],[12,39,13],[22,50,37],[19,9,46],[-24,8,-27],[-28,7,21],[8,-25,50],[20,50,4],[27,36,13],[26,31,-25],[39,-44,-32],[-20,41,-10],[49,-28,35],[1,44,34],[39,35,-11],[-50,-42,-7],[-24,7,47],[-13,5,-48],[-9,-20,-23],[2,17,-19],[11,23,21],[-45,30,15],[11,26,-24],[38,33,-13],[44,-27,-7],[41,49,2],[-18,12,-37],[-2,12,-26],[-19,7,32],[-22,11,33],[8,12,-20],[16,40,-48],[-2,-24,-11],[26,-17,37],[-14,-19,46],[5,47,36],[-29,-9,19],[32,4,28],[-34,20,-46],[-4,-36,-13],[-15,-37,45],[-21,29,23],[-6,-40,7],[-42,31,-29],[-36,24,31],[-45,-37,-1],[3,-6,-29],[-28,-50,27],[44,26,5],[-17,-48,49],[12,-40,-7],[-12,31,-48],[27,32,-42],[-27,-10,1],[6,-49,10],[-24,8,43],[23,31,1],[11,-47,38],[-28,26,-13],[-40,12,-42],[-3,39,46],[17,41,46],[23,21,13],[-14,-1,-38],[20,18,6],[-50,20,-9],[10,-32,-18],[-21,49,-34],[44,23,-35],[40,-19,34],[-1,6,-12],[6,-2,-7],[32,-20,34],[-12,43,-29],[24,2,-49],[10,-4,40],[11,5,12],[-3,47,-31],[43,-23,21],[-41,-36,-50],[-8,-42,-24],[39,45,7],[7,37,-45],[41,40,8],[-50,-10,-8],[-5,-39,-14],[-22,-24,-43],[-36,40,35],[17,49,41],[-32,7,24],[-30,-8,-9],[-41,-13,-10],[31,26,-33],[17,-22,-39],[-21,28,3],[-14,46,23],[29,16,19],[42,-32,-44],[-24,10,23],[-1,-32,-21],[-8,-44,-39],[39,11,9],[19,14,-46],[46,44,-42],[37,23,-29],[32,25,20],[14,-43,-12],[-36,-18,46],[14,-26,-10],[-2,-30,5],[6,-18,46],[-26,2,-44],[20,-8,-11],[-31,3,16],[-22,-9,39],[-49,44,-42],[-45,-44,31],[-31,50,-11],[-32,-46,2],[-6,-7,17],[19,-32,48],[39,20,-10],[-22,-37,38],[-31,9,-48],[40,12,7],[-24,-4,9],[-22,49,33],[-12,43,10],[25,-30,-10],[46,47,31],[13,27,-7],[-45,32,-35],[-50,34,9],[2,34,30],[3,16,2],[-18,45,-12],[33,37,10],[43,7,-18],[-22,44,-19],[-31,-27,-42],[-3,-40,8],[-23,-31,38]]
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
@@ -14,13 +14,20 @@
   MState(..),
   MAtom(..),
   MList(..),
+  mappend,
+  oneMAtom,
+  twoMAtoms,
+  threeMAtoms,
   -- Heterogeneous list
   HList(..),
   happend,
   (:++:),
   ) where
 
+import           Prelude hiding (mappend)
 import           Data.Maybe
+import           Data.Type.Equality
+import           Unsafe.Coerce
 
 ---
 --- Pattern
@@ -38,11 +45,11 @@
   NotPat :: Pattern a m ctx '[] -> Pattern a m ctx '[]
   PredicatePat :: (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 => (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
 
-class Matcher a
+class Matcher m a
 
-data MatchClause a m b = forall vs. (Matcher m) => MatchClause (Pattern a m '[] vs) (HList vs -> b)
+data MatchClause a m b = forall vs. (Matcher m a) => MatchClause (Pattern a m '[] vs) (HList vs -> b)
 
 ---
 --- Matching state
@@ -54,7 +61,7 @@
 -- matching atom
 -- ctx: intermediate pattern-matching results
 -- vs: list of types bound to the pattern variables in the pattern.
-data MAtom ctx vs = forall a m. (Matcher m) => MAtom (Pattern a m ctx vs) m a
+data MAtom ctx vs = forall a m. (Matcher m a) => MAtom (Pattern a m ctx vs) m a
 
 -- stack of matching atoms
 data MList ctx vs where
@@ -62,6 +69,24 @@
   MCons :: MAtom ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys)
   MJoin :: MList ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys)
 
+mappend :: MList ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys)
+mappend MNil atoms = atoms
+mappend (MCons atom atoms1) atoms2 =
+  case mconsAssocProof atom atoms1 of
+    Refl -> case mappendAssocProof atom atoms1 atoms2 of
+      Refl -> MCons atom (mappend atoms1 atoms2)
+
+oneMAtom :: MAtom ctx xs -> MList ctx xs
+oneMAtom atom1 = MCons atom1 MNil
+
+twoMAtoms :: MAtom ctx xs -> MAtom (ctx :++: xs) ys -> MList ctx (xs :++: ys)
+twoMAtoms atom1 atom2 = MCons atom1 (MCons atom2 MNil)
+
+threeMAtoms :: MAtom ctx xs -> MAtom (ctx :++: xs) ys -> MAtom (ctx :++: xs :++: ys) zs -> MList ctx (xs :++: ys :++: zs)
+threeMAtoms atom1 atom2 atom3 =
+  case threeMConsAssocProof atom1 atom2 atom3 of
+    Refl -> MCons atom1 (MCons atom2 (MCons atom3 MNil))
+
 ---
 --- Heterogeneous list
 ---
@@ -70,19 +95,25 @@
   HNil :: HList '[]
   HCons :: a -> HList as -> HList (a ': as)
 
+type family (as ::[*]) :++: (bs :: [*]) :: [*] where
+  as :++: '[] = as
+  '[] :++: bs = bs
+  (a ': as) :++: bs = a ': (as :++: bs)
+
 happend :: HList as -> HList bs -> HList (as :++: bs)
-happend (HCons x xs) ys = case proof x xs ys of Refl -> HCons x $ happend xs ys
 happend HNil ys         = ys
+happend xs@(HCons x xs') ys = case hconsAssocProof x xs' ys of
+                                Refl -> HCons x $ happend xs' ys
 
-type family as :++: bs :: [*] where
-  bs :++: '[] = bs
-  '[] :++: bs = bs
-  (a ': as) :++: bs = a ': (as :++: bs)
+hconsAssocProof :: a -> HList as -> HList bs -> ((a ': as) :++: bs) :~: (a ': (as :++: bs))
+hconsAssocProof _ _ HNil = Refl
+hconsAssocProof x xs (HCons y ys) = Refl
 
-data (a :: [*]) :~: (b :: [*]) where
-  Refl :: a :~: a
+mconsAssocProof :: MAtom ctx vs -> MList (ctx :++: vs) vs' -> (ctx :++: (vs :++: vs')) :~: ((ctx :++: vs) :++: vs')
+mconsAssocProof _ _ = unsafeCoerce Refl -- Todo: Write proof.
 
-proof :: a -> HList as -> HList bs -> ((a ': as) :++: bs) :~: (a ': (as :++: bs))
-proof _ _ HNil = Refl
-proof x xs (HCons y ys) = Refl
+mappendAssocProof :: MAtom ctx xs -> MList (ctx :++: xs) ys ->  MList (ctx :++: xs :++: ys) zs -> (xs :++: (ys :++: zs)) :~: ((xs :++: ys) :++: zs)
+mappendAssocProof _ _ _ = unsafeCoerce Refl -- Todo: Write proof.
 
+threeMConsAssocProof :: MAtom ctx xs -> MAtom (ctx :++: xs) ys -> MAtom (ctx :++: xs :++: ys) zs -> (xs :++: ys :++: zs) :~: (xs :++: (ys :++: zs))
+threeMConsAssocProof _ _ _ = unsafeCoerce Refl -- Todo: Write proof.
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,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs     #-}
+{-# LANGUAGE TypeOperators             #-}
 
 module Control.Egison.Match (
   matchAll,
@@ -8,25 +9,27 @@
   matchDFS,
   ) where
 
+import           Prelude hiding (mappend)
 import           Control.Egison.Core
 import           Unsafe.Coerce
+import           Data.Type.Equality
 
-matchAll :: (Matcher m) => a -> m -> [MatchClause a m b] -> [b]
+matchAll :: (Matcher m a) => a -> m -> [MatchClause a m b] -> [b]
 matchAll tgt m [] = []
 matchAll tgt m ((MatchClause pat f):cs) =
   let results = processMStatesAll [[MState HNil (MCons (MAtom pat m tgt) MNil)]] in
   map f results ++ matchAll tgt m cs
 
-match :: (Matcher m) => a -> m -> [MatchClause a m b] -> b
+match :: (Matcher m a) => a -> m -> [MatchClause a m b] -> b
 match tgt m cs = head $ matchAll tgt m cs
 
-matchAllDFS :: (Matcher m) => a -> m -> [MatchClause a m b] -> [b]
+matchAllDFS :: (Matcher m a) => a -> m -> [MatchClause a m b] -> [b]
 matchAllDFS tgt m [] = []
 matchAllDFS tgt m ((MatchClause pat f):cs) =
   let results = processMStatesAllDFS [MState HNil (MCons (MAtom pat m tgt) MNil)] in
   map f results ++ matchAllDFS tgt m cs
 
-matchDFS :: (Matcher m) => a -> m -> [MatchClause a m b] -> b
+matchDFS :: (Matcher m a) => a -> m -> [MatchClause a m b] -> b
 matchDFS tgt m cs = head $ matchAllDFS tgt m cs
 
 --
@@ -62,19 +65,27 @@
   case pat of
     Pattern f ->
       let matomss = f rs m tgt in
-      map (\newAtoms -> MState rs (MJoin newAtoms atoms)) matomss
+      map (\newAtoms -> MState rs (mappend newAtoms atoms)) matomss
     Wildcard -> [MState rs atoms]
-    PatVar _ -> [unsafeCoerce $ MState (happend rs (HCons tgt HNil)) atoms]
+    PatVar _ -> case patVarProof rs (HCons tgt HNil) atoms of
+                  Refl -> [MState (happend rs (HCons tgt HNil)) atoms]
     AndPat p1 p2 ->
-      [unsafeCoerce $ MState rs (MCons (MAtom p1 m tgt) (MCons (MAtom p2 m tgt) $ unsafeCoerce atoms))]
+      case (assocProof (MAtom p1 m tgt) (MAtom p2 m tgt)) of
+        Refl -> case (andPatProof (MAtom p1 m tgt) (MAtom p2 m tgt) atoms) of
+          Refl -> [MState rs (MCons (MAtom p1 m tgt) (MCons (MAtom p2 m tgt) $ atoms))]
     OrPat p1 p2 ->
       [MState rs (MCons (MAtom p1 m tgt) atoms), MState rs (MCons (MAtom p2 m tgt) atoms)]
     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 (MJoin MNil matoms2)) = processMState (MState rs matoms2)
-processMState (MState rs (MJoin matoms1 matoms2)) =
-  let mstates = processMState (MState rs matoms1) in
-  map (\(MState rs' ms) -> unsafeCoerce $ MState rs' $ MJoin ms matoms2) mstates
 processMState (MState rs MNil) = [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
+patVarProof (HCons _ xs) ys zs = unsafeCoerce Refl -- Todo: Write proof.
+
+andPatProof :: MAtom ctx vs -> MAtom (ctx :++: vs) vs' -> MList (ctx :++: vs :++: vs') ys -> (ctx :++: ((vs :++: vs') :++: ys)) :~: (ctx :++: (vs :++: (vs' :++: ys)))
+andPatProof _ _ _ = unsafeCoerce Refl -- Todo: Write proof.
+
+assocProof :: MAtom ctx vs -> MAtom (ctx :++: vs) vs' -> (ctx :++: (vs :++: vs')) :~: ((ctx :++: vs) :++: vs')
+assocProof _ _ = unsafeCoerce Refl -- Todo: Write proof.
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
@@ -23,6 +23,7 @@
   ) where
 
 import           Prelude hiding (Integer)
+import           Data.List (tails)
 import           Control.Egison.Core
 import           Control.Egison.Match
 import           Control.Egison.QQ
@@ -32,25 +33,25 @@
 --
 
 data Something = Something
-instance Matcher Something
+instance Matcher Something a
 
 --
 -- Eql and Integer matchers
 --
 
 class ValuePat m a where
-  valuePat :: (Matcher m, Eq a) => (HList ctx -> a) -> Pattern a m ctx '[]
+  valuePat :: (Matcher m a, Eq a) => (HList ctx -> a) -> Pattern a m ctx '[]
 
 -- Eql matcher
 data Eql = Eql
-instance Matcher Eql
+instance Matcher Eql a
 
 instance Eq a => ValuePat Eql a where
   valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])
 
 -- Integer matcher
 data Integer = Integer
-instance Matcher Integer
+instance Integral a => Matcher Integer a
 
 instance Integral a => ValuePat Integer a where
   valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])
@@ -59,75 +60,85 @@
 --- Pair matcher
 ---
 
-data Pair a b = Pair a b
-instance (Matcher a, Matcher b) => Matcher (Pair a b)
+data Pair m1 m2 = Pair m1 m2
+instance (Matcher m1 a1, Matcher m2 a2) => Matcher (Pair m1 m2) (a1, a2)
 
 class PairPat m a where
-  pair :: (Matcher m, a ~ (b1, b2), m ~ (Pair m1 m2)) => Pattern b1 m1 ctx xs -> Pattern b2 m2 (ctx :++: xs) ys -> Pattern a m ctx (xs :++: ys)
+  pair :: (Matcher m a , a ~ (b1, b2), m ~ (Pair m1 m2))
+       => Pattern b1 m1 ctx xs
+       -> Pattern b2 m2 (ctx :++: xs) ys
+       -> Pattern a m ctx (xs :++: ys)
 
-instance (Matcher m1, Matcher m2) => PairPat (Pair m1 m2) (a1, a2) where
-  pair p1 p2 = Pattern (\_ (Pair m1 m2) (t1, t2) -> [MCons (MAtom p1 m1 t1) $ MCons (MAtom p2 m2 t2) MNil])
+instance (Matcher m1 a1, Matcher m2 a2) => PairPat (Pair m1 m2) (a1, a2) where
+  pair p1 p2 = Pattern (\_ (Pair m1 m2) (t1, t2) -> [twoMAtoms (MAtom p1 m1 t1) (MAtom p2 m2 t2)])
 
 ---
 --- Matchers for collections
 ---
 
 class CollectionPat m a where
-  nil  :: (Matcher m, a ~ [a']) => Pattern a m ctx '[]
-  cons :: (Matcher m, a ~ [a'], m ~ (f m')) => Pattern a' m' ctx xs -> Pattern a m (ctx :++: xs) ys -> Pattern a m ctx (xs :++: ys)
-  join :: (Matcher m, a ~ [a']) => Pattern a m ctx xs -> Pattern a m (ctx :++: xs) ys -> Pattern a m ctx (xs :++: ys)
+  nil  :: (Matcher m a) => Pattern a m ctx '[]
+  cons :: (Matcher m a, a ~ [a'], m ~ (f m'))
+       => Pattern a' m' ctx xs
+       -> Pattern a m (ctx :++: xs) ys
+       -> Pattern a m ctx (xs :++: ys)
+  join :: (Matcher m a)
+       => Pattern a m ctx xs
+       -> Pattern a m (ctx :++: xs) ys
+       -> Pattern a m ctx (xs :++: ys)
 
 -- List matcher
-newtype List a = List a
-instance (Matcher a) => Matcher (List a)
+newtype List m = List m
+instance (Matcher m a) => Matcher (List m) [a]
 
-instance (Matcher m, Eq a, ValuePat m a) => ValuePat (List m) [a] where
+instance (Matcher m a, Eq a, ValuePat m a) => ValuePat (List m) [a] where
   valuePat f = Pattern (\ctx (List m) tgt ->
                             match (f ctx, tgt) (Pair (List m) (List m)) $
                               [[mc| pair nil nil => [MNil] |],
                                [mc| pair (cons $x $xs) (cons #x #xs) => [MNil] |],
                                [mc| Wildcard => [] |]])
 
-instance Matcher m => CollectionPat (List m) [a] where
+instance Matcher m a => CollectionPat (List m) [a] where
   nil = Pattern (\_ _ t -> [MNil | null t])
   cons p1 p2 = Pattern (\_ (List m) tgt ->
                               case tgt of
                                 [] -> []
-                                x:xs -> [MCons (MAtom p1 m x) $ MCons (MAtom p2 (List m) xs) MNil])
-  join p1 p2 = Pattern (\_ m tgt -> map (\(hs, ts) -> MCons (MAtom p1 m hs) $ MCons (MAtom p2 m ts) MNil) (splits tgt))
+                                x:xs -> [twoMAtoms (MAtom p1 m x) (MAtom p2 (List m) xs)])
+  join Wildcard p2 = Pattern (\_ m tgt -> map (\ts -> oneMAtom (MAtom p2 m ts)) (tails tgt))
+  join p1 p2 = Pattern (\_ m tgt -> map (\(hs, ts) -> twoMAtoms (MAtom p1 m hs) (MAtom p2 m ts)) (splits tgt))
 
 splits :: [a] -> [([a], [a])]
 splits []     = [([], [])]
 splits (x:xs) = ([], x:xs) : [(x:ys, zs) | (ys, zs) <- splits xs]
 
 -- Multiset matcher
-newtype Multiset a = Multiset a
-instance (Matcher a) => Matcher (Multiset a)
+newtype Multiset m = Multiset m
+instance (Matcher m a) => Matcher (Multiset m) [a]
 
-instance (Matcher m, Eq a, ValuePat m a) => ValuePat (Multiset m) [a] where
+instance (Matcher m a, Eq a, ValuePat m a) => ValuePat (Multiset m) [a] where
   valuePat f = Pattern (\ctx (Multiset m) tgt ->
                             match (f ctx, tgt) (Pair (List m) (Multiset m)) $
                               [[mc| pair nil nil => [MNil] |],
                                [mc| pair (cons $x $xs) (cons #x #xs) => [MNil] |],
                                [mc| Wildcard => [] |]])
 
-instance (Matcher m) => CollectionPat (Multiset m) [a] where
+instance (Matcher m a) => CollectionPat (Multiset m) [a] where
   nil = Pattern (\_ _ tgt -> [MNil | null tgt])
-  cons p Wildcard = Pattern (\_ (Multiset m) tgt -> map (\x -> MCons (MAtom p m x) MNil) tgt)
-  cons p1 p2 = Pattern (\_ (Multiset m) tgt -> map (\(x, xs) -> MCons (MAtom p1 m x) $ MCons (MAtom p2 (Multiset m) xs) MNil)
+  cons p Wildcard = Pattern (\_ (Multiset m) tgt -> map (\x -> oneMAtom (MAtom p m x)) tgt)
+  cons p1 p2 = Pattern (\_ (Multiset m) tgt -> map (\(x, xs) -> twoMAtoms (MAtom p1 m x) (MAtom p2 (Multiset m) xs))
                                                    (matchAll tgt (List m) [[mc| join $hs (cons $x $ts) => (x, hs ++ ts) |]]))
   join p1 p2 = undefined
 
 -- Set matcher
-newtype Set a = Set a
-instance (Matcher a) => Matcher (Set a)
+newtype Set m = Set m
+instance (Matcher m a) => Matcher (Set m) [a]
 
-instance (Matcher m, Eq a,  Ord a, ValuePat m a) => ValuePat (Set m) [a] where
+instance (Matcher m a, Eq a,  Ord a, ValuePat m a) => ValuePat (Set m) [a] where
   valuePat f = undefined
 
-instance Matcher m => CollectionPat (Set m) [a] where
+instance Matcher m a => CollectionPat (Set m) [a] where
   nil = Pattern (\_ _ tgt -> [MNil | null tgt])
   cons p1 p2 = Pattern (\_ (Set m) tgt ->
-                  map (\x -> MCons (MAtom p1 m x) $ MCons (MAtom p2 (Set m) tgt) MNil)
+                  map (\x -> twoMAtoms (MAtom p1 m x) (MAtom p2 (Set m) tgt))
                       (matchAll tgt (List m) [[mc| join Wildcard (cons $x Wildcard) => x |]]))
   join p1 p2 = undefined
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -53,11 +53,26 @@
          [mc| _ => "Not matched" |]]
       `shouldBe` "Matched"
 
+--    it "test" $
+--      match 1 (List Integer)
+--        [[mc| $x => "Matched" |]]
+--      `shouldBe` "Matched"
+
   describe "match-all with infinitely many results" $ do
-    it "Check the order of pattern-matching results" $
+    it "Check the order of pattern-matching results (multiset bfs) " $
       take 10 (matchAll [1..] (Multiset Integer)
                  [[mc| cons $x (cons $y _) => (x, y) |]])
       `shouldBe` [(1,2),(1,3),(2,1),(1,4),(2,3),(3,1),(1,5),(2,4),(3,2),(4,1)]
+
+    it "Check the order of pattern-matching results (set bfs)" $
+      take 10 (matchAll [1..] (Set Integer)
+                 [[mc| cons $x (cons $y _) => (x, y) |]])
+      `shouldBe` [(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(1,4),(2,3),(3,2),(4,1)]
+
+    it "Check the order of pattern-matching results (set dfs)" $
+      take 10 (matchAllDFS [1..] (Set Integer)
+                 [[mc| cons $x (cons $y _) => (x, y) |]])
+      `shouldBe` [(1,1),(1,2),(1,3),(1,4),(1,5),(1,6),(1,7),(1,8),(1,9),(1,10)]
 
   describe "built-in pattern constructs" $ do
     it "Predicate patterns" $