diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs
--- a/examples/simple-arith-core.hs
+++ b/examples/simple-arith-core.hs
@@ -10,6 +10,7 @@
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE NoStarIsType #-}
 {-# OPTIONS_GHC -dcore-lint #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
 
@@ -61,7 +62,7 @@
 minusLeq _ _ = Witness
 
 absurdTrueFalse :: ( 'True :~: 'False) -> a
-absurdTrueFalse = \case
+absurdTrueFalse = \case {}
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802
 hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a
@@ -124,4 +125,10 @@
 ghc92NLtToGeq :: (n DTO.<? m) ~ 'True
   => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'False
 ghc92NLtToGeq _ _ = Refl
+
+minLeq :: n <= m => NProxy n -> NProxy m -> DTO.Min n m :~: n
+minLeq _ _ = Refl
+
+maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m
+maxLeq _ _ = Refl
 #endif
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: ebd8f606caa0d36b4fa5c701546d739968ed42ceeba4e62275620799c4e295dc
+-- hash: 321c5fb49fa1a616b17e9d7403d059fae66cceb781b4b2a12f547a6be9636e5d
 
 name:           ghc-typelits-presburger
-version:        0.6.1.0
+version:        0.6.2.0
 synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers.
 description:    @ghc-typelits-presburger@ augments GHC type-system with Presburger
                 Arithmetic Solver for Type-level natural numbers.
diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs
--- a/src/GHC/TypeLits/Presburger/Types.hs
+++ b/src/GHC/TypeLits/Presburger/Types.hs
@@ -601,6 +601,12 @@
 toPresburgerExp :: Given Translation => Type -> Machine Expr
 toPresburgerExp ty = case ty of
   TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t
+  TyConApp tc (lastN 4 -> [cmpNM, l, e, g])
+    | tc `elem` ordCond given
+    , TyConApp cmp (lastN 2 -> [n, m]) <- cmpNM
+    , cmp `elem` natCompare given
+    , all ((`elem` [TypeEq n, TypeEq m]) . TypeEq) [l,e,g]
+    -> decodeMinMax n m l e g
   t@(TyConApp tc ts) ->
     parseExpr given toPresburgerExp ty
       <|> body tc ts
@@ -638,6 +644,18 @@
                   ++ [ step con Max
                      | con <- natMin given
                      ]
+
+decodeMinMax :: Given Translation => Type -> Type -> Type -> Type -> Type -> Machine Expr
+decodeMinMax n m lt eq gt 
+  | lt `eqType`  n && eq `eqType`  n && gt `eqType` m = 
+    Min <$> toPresburgerExp n <*> toPresburgerExp m
+  | lt `eqType`  n && eq `eqType`  m && gt `eqType` m = 
+    Min <$> toPresburgerExp n <*> toPresburgerExp m
+  | lt `eqType` m && eq `eqType`  m && gt `eqType` n = 
+    Max <$> toPresburgerExp n <*> toPresburgerExp m
+  | lt `eqType` m && eq `eqType`  n && gt `eqType` n = 
+    Max <$> toPresburgerExp n <*> toPresburgerExp m
+  | otherwise = mzero
 
 -- simplTypeCmp :: Type -> Type