From 710355176ab6353127812a1eff82cb2efd246b48 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Wed, 8 Feb 2017 15:08:50 -0800
Subject: [PATCH] More rules and things;  external solver disabled;  we can at
 least load ChaCha

---
 cryptol.cabal                                 |   4 +
 src/Cryptol/TypeCheck/Infer.hs                |   2 +-
 src/Cryptol/TypeCheck/Kind.hs                 |  11 +-
 src/Cryptol/TypeCheck/Monad.hs                |   5 +-
 src/Cryptol/TypeCheck/SimpType.hs             | 242 ++++++++++++
 src/Cryptol/TypeCheck/SimpleSolver.hs         | 203 +---------
 src/Cryptol/TypeCheck/Solve.hs                | 188 ++++++---
 src/Cryptol/TypeCheck/Solver/Improve.hs       | 207 ++++++++++
 src/Cryptol/TypeCheck/Solver/Numeric.hs       | 364 +++++++-----------
 .../TypeCheck/Solver/Numeric/ImportExport.hs  |   2 +-
 src/Cryptol/TypeCheck/Solver/Types.hs         |   6 +
 src/Cryptol/TypeCheck/Solver/Utils.hs         |   4 +-
 src/Cryptol/TypeCheck/Subst.hs                |   9 +-
 src/Cryptol/TypeCheck/Type.hs                 |   7 +-
 src/Cryptol/TypeCheck/TypePat.hs              | 171 ++++++++
 src/Cryptol/Utils/Panic.hs                    |   6 +-
 src/Cryptol/Utils/Patterns.hs                 | 136 +++++++
 17 files changed, 1064 insertions(+), 503 deletions(-)
 create mode 100644 src/Cryptol/TypeCheck/SimpType.hs
 create mode 100644 src/Cryptol/TypeCheck/Solver/Improve.hs
 create mode 100644 src/Cryptol/TypeCheck/TypePat.hs
 create mode 100644 src/Cryptol/Utils/Patterns.hs

diff --git a/cryptol.cabal b/cryptol.cabal
index 4070f2b2..b4e6c873 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -94,6 +94,7 @@ library
                        Cryptol.Utils.Panic,
                        Cryptol.Utils.Debug,
                        Cryptol.Utils.Misc,
+                       Cryptol.Utils.Patterns,
                        Cryptol.Version,
 
                        Cryptol.ModuleSystem,
@@ -107,6 +108,8 @@ library
 
                        Cryptol.TypeCheck,
                        Cryptol.TypeCheck.Type,
+                       Cryptol.TypeCheck.TypePat,
+                       Cryptol.TypeCheck.SimpType,
                        Cryptol.TypeCheck.AST,
                        Cryptol.TypeCheck.Monad,
                        Cryptol.TypeCheck.Infer,
@@ -130,6 +133,7 @@ library
                        Cryptol.TypeCheck.Solver.Utils,
 
                        Cryptol.TypeCheck.Solver.Numeric,
+                       Cryptol.TypeCheck.Solver.Improve,
                        Cryptol.TypeCheck.Solver.CrySAT,
                        Cryptol.TypeCheck.Solver.Numeric.AST,
                        Cryptol.TypeCheck.Solver.Numeric.ImportExport,
diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index 0b58f189..2f916aa6 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -22,7 +22,7 @@ import qualified Cryptol.Parser.Names as P
 import           Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp)
 import           Cryptol.TypeCheck.Monad
 import           Cryptol.TypeCheck.Solve
-import           Cryptol.TypeCheck.SimpleSolver(tSub,tMul,tExp)
+import           Cryptol.TypeCheck.SimpType(tSub,tMul,tExp)
 import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
                                           checkNewtype)
 import           Cryptol.TypeCheck.Instantiate
diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs
index f74cb86c..6e62aa0b 100644
--- a/src/Cryptol/TypeCheck/Kind.hs
+++ b/src/Cryptol/TypeCheck/Kind.hs
@@ -20,6 +20,7 @@ import           Cryptol.Parser.AST (Named(..))
 import           Cryptol.Parser.Position
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Monad hiding (withTParams)
+import           Cryptol.TypeCheck.SimpType(tRebuild)
 import           Cryptol.TypeCheck.Solve (simplifyAllConstraints
                                          ,wfTypeFunction)
 import           Cryptol.Utils.PP
@@ -42,7 +43,9 @@ checkSchema (P.Forall xs ps t mb) =
         do ps1 <- mapM checkProp ps
            t1  <- doCheckType t (Just KType)
            return (ps1,t1)
-     return (Forall xs1 ps1 t1, gs)
+     return ( Forall xs1 (map tRebuild ps1) (tRebuild t1)
+            , [ g { goal = tRebuild (goal g) } | g <- gs ]
+            )
 
   where
   rng = case mb of
@@ -59,8 +62,8 @@ checkTySyn (P.TySyn x as t) =
                          return r
      return TySyn { tsName   = thing x
                   , tsParams = as1
-                  , tsConstraints = map goal gs
-                  , tsDef = t1
+                  , tsConstraints = map (tRebuild . goal) gs
+                  , tsDef = tRebuild t1
                   }
 
 -- | Check a newtype declaration.
@@ -89,7 +92,7 @@ checkNewtype (P.Newtype x as fs) =
 checkType :: P.Type Name -> Maybe Kind -> InferM Type
 checkType t k =
   do (_, t1) <- withTParams True [] $ doCheckType t k
-     return t1
+     return (tRebuild t1)
 
 {- | Check something with type parameters.
 
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
index bc690439..1b317563 100644
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -325,10 +325,7 @@ addGoals :: [Goal] -> InferM ()
 addGoals gs0 = doAdd =<< simpGoals gs0
   where
   doAdd [] = return ()
-  doAdd gs =
-    do io $ putStrLn "Adding goals:"
-       io $ mapM_ putStrLn [ "  " ++ show (pp (goal g)) | g <- gs ]
-       IM $ sets_ $ \s -> s { iCts = foldl' (flip insertGoal) (iCts s) gs }
+  doAdd gs = IM $ sets_ $ \s -> s { iCts = foldl' (flip insertGoal) (iCts s) gs }
 
 
 -- | Collect the goals emitted by the given sub-computation.
diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs
new file mode 100644
index 00000000..0fb76faa
--- /dev/null
+++ b/src/Cryptol/TypeCheck/SimpType.hs
@@ -0,0 +1,242 @@
+{-# LANGUAGE PatternGuards #-}
+module Cryptol.TypeCheck.SimpType where
+
+import Control.Applicative((<|>))
+import Cryptol.TypeCheck.Type hiding
+  (tAdd,tSub,tMul,tDiv,tMod,tExp,tMin,tMax,tWidth,tLenFromThen,tLenFromThenTo)
+import Cryptol.TypeCheck.TypePat
+import Cryptol.TypeCheck.Solver.InfNat
+import Control.Monad(msum,guard)
+import Cryptol.TypeCheck.PP(pp)
+
+
+tRebuild :: Type -> Type
+tRebuild = go
+  where
+  go ty =
+    case ty of
+      TUser x xs t -> TUser x xs (go t)
+      TVar _       -> ty
+      TRec xs      -> TRec [ (x,go y) | (x,y) <- xs ]
+      TCon tc ts ->
+        case (tc, map go ts) of
+          (TF f, ts') ->
+            case (f,ts') of
+              (TCAdd,[x,y]) -> tAdd x y
+              (TCSub,[x,y]) -> tSub x y
+              (TCMul,[x,y]) -> tMul x y
+              (TCExp,[x,y]) -> tExp x y
+              (TCDiv,[x,y]) -> tDiv x y
+              (TCMod,[x,y]) -> tMod x y
+              (TCMin,[x,y]) -> tMin x y
+              (TCMax,[x,y]) -> tMax x y
+              (TCWidth,[x]) -> tWidth x
+              (TCLenFromThen,[x,y,z]) -> tLenFromThen x y z
+              (TCLenFromThenTo,[x,y,z]) -> tLenFromThenTo x y z
+              _ -> TCon tc ts
+          (_,ts') -> TCon tc ts'
+
+-- Normal: constants to the left
+tAdd :: Type -> Type -> Type
+tAdd x y
+  | Just t <- tOp TCAdd (total (op2 nAdd)) [x,y] = t
+  | tIsInf x            = tInf
+  | tIsInf y            = tInf
+  | Just n <- tIsNum x  = addK n y
+  | Just n <- tIsNum y  = addK n x
+  | Just (n,x1) <- isSumK x = addK n (tAdd x1 y)
+  | Just (n,y1) <- isSumK y = addK n (tAdd x y1)
+  | Just v <- matchMaybe (do (a,b) <- (|-|) y
+                             guard (x == b)
+                             return a) = v
+  | Just v <- matchMaybe (do (a,b) <- (|-|) x
+                             guard (b == y)
+                             return a) = v
+
+  | otherwise           = tf2 TCAdd x y
+  where
+  isSumK t = case tNoUser t of
+               TCon (TF TCAdd) [ l, r ] ->
+                 do n <- tIsNum l
+                    return (n, r)
+               _ -> Nothing
+
+  addK 0 t = t
+  addK n t | Just (m,b) <- isSumK t = tf2 TCAdd (tNum (n + m)) b
+           | otherwise              = tf2 TCAdd (tNum n) t
+
+tSub :: Type -> Type -> Type
+tSub x y
+  | Just t <- tOp TCSub (op2 nSub) [x,y] = t
+  | tIsInf y  = tBadNumber $ TCErrorMessage "Subtraction of `inf`."
+  | Just 0 <- yNum = x
+  | Just k <- yNum
+  , TCon (TF TCAdd) [a,b] <- tNoUser x
+  , Just n <- tIsNum a = case compare k n of
+                           EQ -> b
+                           LT -> tf2 TCAdd (tNum (n - k)) b
+                           GT -> tSub b (tNum (k - n))
+
+  | Just v <- matchMaybe (do (a,b) <- anAdd x
+                             (guard (a == y) >> return b)
+                                <|> (guard (b == y) >> return a))
+                       = v
+
+  | Just v <- matchMaybe (do (a,b) <- (|-|) y
+                             return (tSub (tAdd x b) a)) = v
+
+  | otherwise = tf2 TCSub x y
+  where
+  yNum = tIsNum y
+
+
+
+-- Normal: constants to the left
+tMul :: Type -> Type -> Type
+tMul x y
+  | Just t <- tOp TCMul (total (op2 nMul)) [x,y] = t
+  | Just n <- tIsNum x  = mulK n y
+  | Just n <- tIsNum y  = mulK n x
+  | otherwise           = tf2 TCMul x y
+  where
+  mulK 0 _ = tNum (0 :: Int)
+  mulK 1 t = t
+  mulK n t | TCon (TF TCMul) [a,b] <- t'
+           , Just a' <- tIsNat' a = case a' of
+                                     Inf   -> t
+                                     Nat m -> tf2 TCMul (tNum (n * m)) b
+           | TCon (TF TCDiv) [a,b] <- t'
+           , Just b' <- tIsNum b
+           -- XXX: similar for a = b * k?
+           , n == b' = tSub a (tMod a b)
+
+
+           | otherwise = tf2 TCMul (tNum n) t
+    where t' = tNoUser t
+
+tDiv :: Type -> Type -> Type
+tDiv x y
+  | Just t <- tOp TCDiv (op2 nDiv) [x,y] = t
+  | tIsInf x = tBadNumber $ TCErrorMessage "Division of `inf`."
+  | Just 0 <- tIsNum y = tBadNumber $ TCErrorMessage "Division by 0."
+  | otherwise = tf2 TCDiv x y
+
+
+tMod :: Type -> Type -> Type
+tMod x y
+  | Just t <- tOp TCMod (op2 nMod) [x,y] = t
+  | tIsInf x = tBadNumber $ TCErrorMessage "Modulus of `inf`."
+  | Just 0 <- tIsNum x = tBadNumber $ TCErrorMessage "Modulus by 0."
+  | otherwise = tf2 TCMod x y
+
+tExp :: Type -> Type -> Type
+tExp x y
+  | Just t <- tOp TCExp (total (op2 nExp)) [x,y] = t
+  | Just 0 <- tIsNum y = tNum (1 :: Int)
+  | TCon (TF TCExp) [a,b] <- tNoUser y = tExp x (tMul a b)
+  | otherwise = tf2 TCExp x y
+
+
+-- Normal: constants to the left
+tMin :: Type -> Type -> Type
+tMin x y
+  | Just t <- tOp TCMin (total (op2 nMin)) [x,y] = t
+  | Just n <- tIsNat' x = minK n y
+  | Just n <- tIsNat' y = minK n x
+  | x == y              = x
+  -- XXX: min (k + t) t -> t
+  | otherwise           = tf2 TCMin x y
+  where
+  minK Inf t      = t
+  minK (Nat 0) _  = tNum (0 :: Int)
+  minK (Nat k) t
+    | TCon (TF TCAdd) [a,b] <- t'
+    , Just n <- tIsNum a   = if k <= n then tNum k
+                                       else tAdd a (tMin (tNum (k - n)) b)
+
+    | TCon (TF TCSub) [a,b] <- t'
+    , Just n <- tIsNum a =
+      if k >= n then t else tSub a (tMax (tNum (n - k)) b)
+
+    | TCon (TF TCMin) [a,b] <- t'
+    , Just n <- tIsNum a   = tf2 TCMin (tNum (min k n)) b
+
+    | otherwise = tf2 TCMin (tNum k) t
+    where t' = tNoUser t
+
+-- Normal: constants to the left
+tMax :: Type -> Type -> Type
+tMax x y
+  | Just t <- tOp TCMax (total (op2 nMax)) [x,y] = t
+  | Just n <- tIsNat' x = maxK n y
+  | Just n <- tIsNat' y = maxK n x
+  | otherwise           = tf2 TCMax x y
+  where
+  maxK Inf _     = tInf
+  maxK (Nat 0) t = t
+  maxK (Nat k) t
+
+    | TCon (TF TCAdd) [a,b] <- t'
+    , Just n <- tIsNum a = if k <= n
+                             then t
+                             else tMax (tNum (k - n)) b
+
+    | TCon (TF TCSub) [a,b] <- t'
+    , Just n <- tIsNat' a =
+      case n of
+        Inf   -> t
+        Nat m -> if k >= m then tNum k else tSub a (tMin (tNum (m - k)) b)
+
+    | TCon (TF TCMax) [a,b] <- t'
+    , Just n <- tIsNum a  = tf2 TCMax (tNum (max k n)) b
+
+    | otherwise = tf2 TCMax (tNum k) t
+    where t' = tNoUser t
+
+
+tWidth :: Type -> Type
+tWidth x
+  | Just t <- tOp TCWidth (total (op1 nWidth)) [x] = t
+  | otherwise = tf1 TCWidth x
+
+tLenFromThen :: Type -> Type -> Type -> Type
+tLenFromThen x y z
+  | Just t <- tOp TCLenFromThen (op3 nLenFromThen) [x,y,z] = t
+  -- XXX: rules?
+  | otherwise = tf3 TCLenFromThen x y z
+
+tLenFromThenTo :: Type -> Type -> Type -> Type
+tLenFromThenTo x y z
+  | Just t <- tOp TCLenFromThen (op3 nLenFromThen) [x,y,z] = t
+  | otherwise = tf3 TCLenFromThenTo x y z
+
+total :: ([Nat'] -> Nat') -> ([Nat'] -> Maybe Nat')
+total f xs = Just (f xs)
+
+op1 :: (a -> b) -> [a] -> b
+op1 f ~[x] = f x
+
+op2 :: (a -> a -> b) -> [a] -> b
+op2 f ~[x,y] = f x y
+
+op3 :: (a -> a -> a -> b) -> [a] -> b
+op3 f ~[x,y,z] = f x y z
+
+-- | Common checks: check for error, or simple full evaluation.
+tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
+tOp tf f ts
+  | Just e  <- msum (map tIsError ts) = Just (tBadNumber e)
+  | Just xs <- mapM tIsNat' ts =
+      Just $ case f xs of
+               Nothing -> tBadNumber (err xs)
+               Just n  -> tNat' n
+  | otherwise = Nothing
+  where
+  err xs = TCErrorMessage $
+              "Invalid applicatoin of " ++ show (pp tf) ++ " to " ++
+                  unwords (map show xs)
+
+
+
+
+
diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs
index 7e9b4c23..b80517e2 100644
--- a/src/Cryptol/TypeCheck/SimpleSolver.hs
+++ b/src/Cryptol/TypeCheck/SimpleSolver.hs
@@ -1,10 +1,5 @@
 {-# LANGUAGE PatternGuards #-}
-module Cryptol.TypeCheck.SimpleSolver
-  ( simplify
-  , simplifyStep
-  , tAdd, tSub, tMul, tDiv, tMod, tExp
-  , tMin, tMax, tWidth, tLenFromThen, tLenFromThenTo
-  ) where
+module Cryptol.TypeCheck.SimpleSolver ( simplify , simplifyStep) where
 
 import Data.Map(Map)
 import Control.Monad(msum)
@@ -20,9 +15,6 @@ import Cryptol.TypeCheck.Solver.Numeric.Interval(Interval)
 import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
 import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst)
 
-type Ctxt = Map TVar Interval
-
-
 simplify :: Ctxt -> Prop -> Prop
 simplify ctxt p =
   case simplifyStep ctxt p of
@@ -49,196 +41,3 @@ simplifyStep ctxt prop =
     _                         -> Unsolved
 
 
-
-
---------------------------------------------------------------------------------
--- Construction of type functions
-
--- Normal: constants to the left
-tAdd :: Type -> Type -> Type
-tAdd x y
-  | Just t <- tOp TCAdd (total (op2 nAdd)) [x,y] = t
-  | tIsInf x            = tInf
-  | tIsInf y            = tInf
-  | Just n <- tIsNum x  = addK n y
-  | Just n <- tIsNum y  = addK n x
-  | Just (n,x1) <- isSumK x = addK n (tAdd x1 y)
-  | Just (n,y1) <- isSumK y = addK n (tAdd x y1)
-  | otherwise           = tf2 TCAdd x y
-  where
-  isSumK t = case tNoUser t of
-               TCon (TF TCAdd) [ l, r ] ->
-                 do n <- tIsNum l
-                    return (n, r)
-               _ -> Nothing
-
-  addK 0 t = t
-  addK n t | Just (m,b) <- isSumK t = tf2 TCAdd (tNum (n + m)) b
-           | otherwise              = tf2 TCAdd (tNum n) t
-
-tSub :: Type -> Type -> Type
-tSub x y
-  | Just t <- tOp TCSub (op2 nSub) [x,y] = t
-  | tIsInf y  = tBadNumber $ TCErrorMessage "Subtraction of `inf`."
-  | Just 0 <- yNum = x
-  | Just k <- yNum
-  , TCon (TF TCAdd) [a,b] <- tNoUser x
-  , Just n <- tIsNum a = case compare k n of
-                           EQ -> b
-                           LT -> tf2 TCAdd (tNum (n - k)) b
-                           GT -> tSub b (tNum (k - n))
-  | otherwise = tf2 TCSub x y
-  where
-  yNum = tIsNum y
-
-
-
--- Normal: constants to the left
-tMul :: Type -> Type -> Type
-tMul x y
-  | Just t <- tOp TCMul (total (op2 nMul)) [x,y] = t
-  | Just n <- tIsNum x  = mulK n y
-  | Just n <- tIsNum y  = mulK n x
-  | otherwise           = tf2 TCMul x y
-  where
-  mulK 0 _ = tNum (0 :: Int)
-  mulK 1 t = t
-  mulK n t | TCon (TF TCMul) [a,b] <- t'
-           , Just a' <- tIsNat' a = case a' of
-                                     Inf   -> t
-                                     Nat m -> tf2 TCMul (tNum (n * m)) b
-           | TCon (TF TCDiv) [a,b] <- t'
-           , Just b' <- tIsNum b
-           -- XXX: similar for a = b * k?
-           , n == b' = tSub a (tMod a b)
-
-
-           | otherwise = tf2 TCMul (tNum n) t
-    where t' = tNoUser t
-
-tDiv :: Type -> Type -> Type
-tDiv x y
-  | Just t <- tOp TCDiv (op2 nDiv) [x,y] = t
-  | tIsInf x = tBadNumber $ TCErrorMessage "Division of `inf`."
-  | Just 0 <- tIsNum y = tBadNumber $ TCErrorMessage "Division by 0."
-  | otherwise = tf2 TCDiv x y
-
-
-tMod :: Type -> Type -> Type
-tMod x y
-  | Just t <- tOp TCMod (op2 nMod) [x,y] = t
-  | tIsInf x = tBadNumber $ TCErrorMessage "Modulus of `inf`."
-  | Just 0 <- tIsNum x = tBadNumber $ TCErrorMessage "Modulus by 0."
-  | otherwise = tf2 TCMod x y
-
-tExp :: Type -> Type -> Type
-tExp x y
-  | Just t <- tOp TCExp (total (op2 nExp)) [x,y] = t
-  | Just 0 <- tIsNum y = tNum (1 :: Int)
-  | TCon (TF TCExp) [a,b] <- tNoUser y = tExp x (tMul a b)
-  | otherwise = tf2 TCExp x y
-
-
--- Normal: constants to the left
-tMin :: Type -> Type -> Type
-tMin x y
-  | Just t <- tOp TCMin (total (op2 nMin)) [x,y] = t
-  | Just n <- tIsNat' x = minK n y
-  | Just n <- tIsNat' y = minK n x
-  | x == y              = x
-  -- XXX: min (k + t) t -> t
-  | otherwise           = tf2 TCMin x y
-  where
-  minK Inf t      = t
-  minK (Nat 0) _  = tNum (0 :: Int)
-  minK (Nat k) t
-    | TCon (TF TCAdd) [a,b] <- t'
-    , Just n <- tIsNum a   = if k <= n then tNum k
-                                       else tAdd a (tMin (tNum (k - n)) b)
-
-    | TCon (TF TCSub) [a,b] <- t'
-    , Just n <- tIsNum a =
-      if k >= n then t else tSub a (tMax (tNum (n - k)) b)
-
-    | TCon (TF TCMin) [a,b] <- t'
-    , Just n <- tIsNum a   = tf2 TCMin (tNum (min k n)) b
-
-    | otherwise = tf2 TCMin (tNum k) t
-    where t' = tNoUser t
-
--- Normal: constants to the left
-tMax :: Type -> Type -> Type
-tMax x y
-  | Just t <- tOp TCMax (total (op2 nMax)) [x,y] = t
-  | Just n <- tIsNat' x = maxK n y
-  | Just n <- tIsNat' y = maxK n x
-  | otherwise           = tf2 TCMax x y
-  where
-  maxK Inf _     = tInf
-  maxK (Nat 0) t = t
-  maxK (Nat k) t
-
-    | TCon (TF TCAdd) [a,b] <- t'
-    , Just n <- tIsNum a = if k <= n
-                             then t
-                             else tMax (tNum (k - n)) b
-
-    | TCon (TF TCSub) [a,b] <- t'
-    , Just n <- tIsNat' a =
-      case n of
-        Inf   -> t
-        Nat m -> if k >= m then tNum k else tSub a (tMin (tNum (m - k)) b)
-
-    | TCon (TF TCMax) [a,b] <- t'
-    , Just n <- tIsNum a  = tf2 TCMax (tNum (max k n)) b
-
-    | otherwise = tf2 TCMax (tNum k) t
-    where t' = tNoUser t
-
-
-tWidth :: Type -> Type
-tWidth x
-  | Just t <- tOp TCWidth (total (op1 nWidth)) [x] = t
-  | otherwise = tf1 TCWidth x
-
-tLenFromThen :: Type -> Type -> Type -> Type
-tLenFromThen x y z
-  | Just t <- tOp TCLenFromThen (op3 nLenFromThen) [x,y,z] = t
-  -- XXX: rules?
-  | otherwise = tf3 TCLenFromThen x y z
-
-tLenFromThenTo :: Type -> Type -> Type -> Type
-tLenFromThenTo x y z
-  | Just t <- tOp TCLenFromThen (op3 nLenFromThen) [x,y,z] = t
-  | otherwise = tf3 TCLenFromThenTo x y z
-
-total :: ([Nat'] -> Nat') -> ([Nat'] -> Maybe Nat')
-total f xs = Just (f xs)
-
-op1 :: (a -> b) -> [a] -> b
-op1 f ~[x] = f x
-
-op2 :: (a -> a -> b) -> [a] -> b
-op2 f ~[x,y] = f x y
-
-op3 :: (a -> a -> a -> b) -> [a] -> b
-op3 f ~[x,y,z] = f x y z
-
--- | Common checks: check for error, or simple full evaluation.
-tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
-tOp tf f ts
-  | Just e  <- msum (map tIsError ts) = Just (tBadNumber e)
-  | Just xs <- mapM tIsNat' ts =
-      Just $ case f xs of
-               Nothing -> tBadNumber (err xs)
-               Just n  -> tNat' n
-  | otherwise = Nothing
-  where
-  err xs = TCErrorMessage $
-              "Invalid applicatoin of " ++ show (pp tf) ++ " to " ++
-                  unwords (map show xs)
-
-
-
-
-
diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs
index b62a4fd6..cba28007 100644
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/src/Cryptol/TypeCheck/Solve.hs
@@ -24,24 +24,29 @@ import           Cryptol.TypeCheck.PP(pp)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Monad
 import           Cryptol.TypeCheck.Subst
-                    (apSubst,fvs,singleSubst, isEmptySubst,
+                    (apSubst,fvs,singleSubst, isEmptySubst, substToList,
                           emptySubst,Subst,listSubst, (@@), Subst,
                            apSubstMaybe, substBinds)
 import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
 import           Cryptol.TypeCheck.Solver.Types
 import           Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
+import           Cryptol.TypeCheck.SimpType(tMax)
 
 
+import           Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
+import           Cryptol.TypeCheck.Solver.Numeric.Interval
 import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
 import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num
 import qualified Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr as Num
 import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
 import           Cryptol.TypeCheck.Solver.CrySAT (debugBlock, DebugLog(..))
-import           Cryptol.Utils.PP (text)
+import           Cryptol.Utils.PP (text,vcat,nest, ($$), (<+>))
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.Misc(anyJust)
+import           Cryptol.Utils.Patterns(matchMaybe)
 
-import           Control.Monad (unless, guard)
+import           Control.Monad (unless, guard, mzero)
+import           Control.Applicative ((<|>))
 import           Data.Either(partitionEithers)
 import           Data.Maybe(catMaybes, fromMaybe)
 import           Data.Map ( Map )
@@ -80,6 +85,65 @@ wfType t =
 
 
 
+--------------------------------------------------------------------------------
+
+
+quickSolverIO :: Ctxt -> [Goal] -> IO (Either Goal (Subst,[Goal]))
+quickSolverIO ctxt [] = return (Right (emptySubst, []))
+quickSolverIO ctxt gs =
+  case quickSolver ctxt gs of
+    Left err ->
+      do msg (text "Contradiction:" <+> pp (goal err))
+         return (Left err)
+    Right (su,gs') ->
+      do msg (vcat (map (pp . goal) gs' ++ [pp su]))
+         return (Right (su,gs'))
+  where
+  shAsmps = case [ pp x <+> text "in" <+> ppInterval i |
+               (x,i) <- Map.toList ctxt ] of
+              [] -> text ""
+              xs -> text "ASMPS:" $$ nest 2 (vcat xs $$ text "===")
+  msg d = return () {-putStrLn $ show (
+             text "quickSolver:" $$ nest 2 (vcat
+                [ shAsmps
+                , vcat (map (pp.goal) gs)
+                , text "==>"
+                , d
+                ]))-}
+
+quickSolver :: Ctxt  -> {- ^ Facts we can know -}
+              [Goal] -> {- ^ Need to solve these -}
+              Either Goal (Subst,[Goal])
+              -- ^ Left: contradiciting goals,
+              --   Right: inferred types, unsolved goals.
+quickSolver ctxt gs0 = go emptySubst [] gs0
+  where
+  go su [] [] = Right (su,[])
+
+  go su unsolved [] =
+    case matchMaybe (findImprovement unsolved) of
+      Nothing            -> Right (su,unsolved)
+      Just (newSu, subs) -> go (newSu @@ su) [] (subs ++ apSubst su unsolved)
+
+  go su unsolved (g : gs) =
+    case Simplify.simplifyStep ctxt (goal g) of
+      Unsolvable _        -> Left g
+      Unsolved            -> go su (g : unsolved) gs
+      SolvedIf subs       ->
+        let cvt x = g { goal = x }
+        in go su unsolved (map cvt subs ++ gs)
+
+  -- Probably better to find more than one.
+  findImprovement []       = mzero
+  findImprovement (g : gs) =
+    do (su,ps) <- improveProp False ctxt (goal g)
+       return (su, [ g { goal = p } | p <- ps ])
+    <|> findImprovement gs
+
+
+
+
+
 --------------------------------------------------------------------------------
 
 simplifyAllConstraints :: InferM ()
@@ -89,11 +153,8 @@ simplifyAllConstraints =
      case gs of
        [] -> return ()
        _ ->
-         do -- r <- curRange
-            io $ putStrLn $ "simplifyAllConstraints " ++ show (length gs)
-            io $ putStrLn $ unlines [ "  " ++ show (pp (goal g), pp (goalSource g)) | g <- gs ]
-            solver <- getSolver
-            (mb,su) <- io (simpGoals' solver gs)
+         do solver <- getSolver
+            (mb,su) <- io (simpGoals' solver Map.empty gs)
             extendSubst su
             case mb of
               Right gs1  -> addGoals gs1
@@ -120,7 +181,35 @@ proveImplicationIO :: Num.Solver
                    -> [Goal]   -- ^ Collected constraints
                    -> IO (Either Error [Warning], Subst)
 proveImplicationIO _   _     _         _  [] [] = return (Right [], emptySubst)
-proveImplicationIO s lname varsInEnv as ps gs =
+proveImplicationIO s f vs ps asmps0 gs0 =
+  do let ctxt = assumptionIntervals Map.empty asmps
+     res <- quickSolverIO ctxt gs
+     case res of
+       Left err -> return (Left (UnsolvedGoal True err), emptySubst)
+       Right (su,[]) -> return (Right [], su)
+       Right (su,gs1) -> proveImplicationIO' s f vs ps asmps gs1
+  where
+  (asmps,gs) =
+    case matchMaybe (improveProps True Map.empty asmps0) of
+     Nothing -> (asmps0,gs0)
+     Just (newSu,newAsmps) ->
+        ( [ TVar x =#= t | (x,t) <- substToList newSu ]
+          ++ newAsmps
+        , [ g { goal = apSubst newSu (goal g) } | g <- gs0 ]
+        )
+
+
+
+
+proveImplicationIO' :: Num.Solver
+                   -> Name     -- ^ Checking this function
+                   -> Set TVar -- ^ These appear in the env., and we should
+                               -- not try to default the
+                   -> [TParam] -- ^ Type parameters
+                   -> [Prop]   -- ^ Assumed constraint
+                   -> [Goal]   -- ^ Collected constraints
+                   -> IO (Either Error [Warning], Subst)
+proveImplicationIO' s lname varsInEnv as ps gs =
   debugBlock s "proveImplicationIO" $
 
   do debugBlock s "assumes" (debugLog s ps)
@@ -154,7 +243,8 @@ proveImplicationIO s lname varsInEnv as ps gs =
             let gs1 = filter ((`notElem` ps) . goal) gs0
 
             debugLog s "3. ---------------------"
-            (mb,su1) <- simpGoals' s (scs ++ gs1)
+            let ctxt = assumptionIntervals Map.empty ps
+            (mb,su1) <- simpGoals' s ctxt (scs ++ gs1)
 
             case mb of
               Left badGs  -> reportUnsolved badGs (su1 @@ su)
@@ -219,15 +309,22 @@ The plan:
   9. Goto 3
 -}
 
-simpGoals' :: Num.Solver -> [Goal] -> IO (Either [Goal] [Goal], Subst)
-simpGoals' s gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
+simpGoals' :: Num.Solver -> Ctxt -> [Goal] -> IO (Either [Goal] [Goal], Subst)
+simpGoals' s asmps gs =
+  do res <- quickSolverIO asmps gs
+     case res of
+       Left err      -> return (Left [err], emptySubst)
+       Right (su,gs) -> return (Right gs, su)
+
+
+simpGoals' s asmps gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
   where
   -- Assumes that the well-formed constraints are themselves well-formed.
   wellFormed gs = [ g { goal = p } | g <- gs, p <- wfType (goal g) ]
 
   go su old [] = return (Right old, su)
   go su old gs =
-    do res  <- solveConstraints s old gs
+    do res  <- solveConstraints s asmps old gs
        case res of
          Left err -> return (Left err, su)
          Right gs2 ->
@@ -264,7 +361,18 @@ want to use the fact that `x >= 1` to simplify `x >= 1` to true.
 
 
 
+
+assumptionIntervals :: Ctxt -> [Prop] -> Ctxt
+assumptionIntervals as ps =
+  case computePropIntervals as ps of
+    NoChange -> as
+    InvalidInterval {} -> as -- XXX: say something
+    NewIntervals bs -> Map.union bs as
+
+
+
 solveConstraints :: Num.Solver ->
+                    Ctxt ->
                     [Goal] {- We may use these, but don't try to solve,
                               we already tried and failed. -} ->
                     [Goal] {- Need to solve these -} ->
@@ -272,22 +380,25 @@ solveConstraints :: Num.Solver ->
                     -- ^ Left: contradiciting goals,
                     --   Right: goals that were not solved, or sub-goals
                     --          for solved goals.  Does not include "old"
-solveConstraints s otherGs gs0 =
-  debugBlock s "Solving constraints" $ go [] gs0
+solveConstraints s asmps otherGs gs0 =
+  debugBlock s "Solving constraints" $ go ctxt0 [] gs0
 
   where
-  go unsolved [] =
+  ctxt0 = assumptionIntervals asmps (map goal otherGs)
+
+
+  go ctxt unsolved [] =
     do let (cs,nums) = partitionEithers (map Num.numericRight unsolved)
        nums' <- solveNumerics s otherNumerics nums
        return (Right (cs ++ nums'))
 
-  go unsolved (g : gs) =
-    case Simplify.simplifyStep Map.empty (goal g) of
+  go ctxt unsolved (g : gs) =
+    case Simplify.simplifyStep ctxt (goal g) of
       Unsolvable _        -> return (Left [g])
-      Unsolved            -> go (g : unsolved) gs
+      Unsolved            -> go ctxt (g : unsolved) gs
       SolvedIf subs       ->
         let cvt x = g { goal = x }
-        in  go unsolved (map cvt subs ++ gs)
+        in  go ctxt unsolved (map cvt subs ++ gs)
 
 
   otherNumerics = [ g | Right g <- map Num.numericRight otherGs ]
@@ -299,6 +410,7 @@ solveNumerics :: Num.Solver ->
                  [(Goal,Num.Prop)] {- ^ Consult these -} ->
                  [(Goal,Num.Prop)] {- ^ Solve these -}   ->
                  IO [Goal]
+solveNumerics _ _ [] = return []
 solveNumerics s consultGs solveGs =
   Num.withScope s $
     do _   <- Num.assumeProps s (map (goal . fst) consultGs)
@@ -439,7 +551,7 @@ improveByDefaultingWith s as ps =
            su                 = listSubst defs
 
        -- Do this to simplify the instantiated "fin" constraints.
-       (mb,su1) <- simpGoals' s (newOthers ++ others ++ apSubst su fins)
+       (mb,su1) <- simpGoals' s Map.empty (newOthers ++ others ++ apSubst su fins)
        case mb of
          Right gs1 ->
            let warn (x,t) =
@@ -536,7 +648,7 @@ defaultReplExpr so e s =
              mbSubst <- tryGetModel so params (sProps s)
              case mbSubst of
                Just su ->
-                 do (res,su1) <- simpGoals' so (map (makeGoal su) (sProps s))
+                 do (res,su1) <- simpGoals' so Map.empty (map (makeGoal su) (sProps s))
                     return $
                       case res of
                         Right [] | isEmptySubst su1 ->
@@ -600,35 +712,3 @@ simpTypeMaybe ty =
 
 
 
---------------------------------------------------------------------------------
-_testSimpGoals :: IO ()
-_testSimpGoals = Num.withSolver cfg $ \s ->
-  do _ <- Num.assumeProps s asmps
-     _mbImps <- Num.check s
-
-
-     (mb,_) <- simpGoals' s gs
-     case mb of
-       Right _  -> debugLog s "End of test"
-       Left _   -> debugLog s "Impossible"
-  where
-  cfg = SolverConfig { solverPath = "z3"
-                     , solverArgs = [ "-smt2", "-in" ]
-                     , solverVerbose = 1
-                     }
-
-  asmps = []
-
-  gs    = map fakeGoal [ tv 0 =#= tMin (num 10) (tv 1)
-                       , tv 1 =#= num 10
-                       ]
-
-
-  fakeGoal p = Goal { goalSource = undefined, goalRange = undefined, goal = p }
-  tv n  = TVar (TVFree n KNum Set.empty (text "test var"))
-  _btv n = TVar (TVBound n KNum)
-  num x = tNum (x :: Int)
-
-
-
-
diff --git a/src/Cryptol/TypeCheck/Solver/Improve.hs b/src/Cryptol/TypeCheck/Solver/Improve.hs
new file mode 100644
index 00000000..55b14863
--- /dev/null
+++ b/src/Cryptol/TypeCheck/Solver/Improve.hs
@@ -0,0 +1,207 @@
+-- | Look for opportunity to solve goals by instantiating variables.
+module Cryptol.TypeCheck.Solver.Improve where
+
+import qualified Data.Set as Set
+import Control.Applicative
+import Control.Monad
+
+import Cryptol.Utils.Patterns
+
+import Cryptol.TypeCheck.Type
+import Cryptol.TypeCheck.SimpType as Mk
+import Cryptol.TypeCheck.Solver.Types
+import Cryptol.TypeCheck.Solver.Numeric.Interval
+import Cryptol.TypeCheck.TypePat
+import Cryptol.TypeCheck.Subst
+
+
+
+improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst,[Prop])
+improveProps impSkol ctxt ps0 = loop emptySubst ps0
+  where
+  loop su props = case go emptySubst [] props of
+                    (newSu,newProps)
+                      | isEmptySubst newSu ->
+                        if isEmptySubst su then mzero else return (su,props)
+                      | otherwise -> loop (newSu @@ su) newProps
+
+  go su subs [] = (su,subs)
+  go su subs (p : ps) =
+    case matchMaybe (improveProp impSkol ctxt p) of
+      Nothing            -> go su (p:subs) ps
+      Just (suNew,psNew) -> go (suNew @@ su) (psNew ++ subs) ps
+
+
+improveProp :: Bool -> Ctxt -> Prop -> Match (Subst,[Prop])
+improveProp impSkol ctxt prop =
+  improveEq impSkol ctxt prop
+  -- XXX: others
+
+
+
+
+improveEq :: Bool -> Ctxt -> Prop -> Match (Subst,[Prop])
+improveEq impSkol fins prop =
+  do (lhs,rhs) <- (|=|) prop
+     rewrite lhs rhs <|> rewrite rhs lhs
+  where
+  rewrite this other =
+    do x <- aTVar this
+       guard (considerVar x && x `Set.notMember` fvs other)
+       return (singleSubst x other, [])
+    <|>
+    do (v,s) <- isSum this
+       guard (v `Set.notMember` fvs other)
+       return (singleSubst v (Mk.tSub other s), [ other >== s ])
+
+  isSum t = do (v,s) <- matches t (anAdd, aTVar, __)
+               valid v s
+        <|> do (s,v) <- matches t (anAdd, __, aTVar)
+               valid v s
+
+  valid v s = do let i = typeInterval fins s
+                 guard (considerVar v && v `Set.notMember` fvs s && iIsFin i)
+                 return (v,s)
+
+  considerVar x = impSkol || isFreeTV x
+
+
+--------------------------------------------------------------------------------
+
+-- XXX
+
+{-
+-- | When given an equality constraint, attempt to rewrite it to the form `?x =
+-- ...`, by moving all occurrences of `?x` to the LHS, and any other variables
+-- to the RHS.  This will only work when there's only one unification variable
+-- present in the prop.
+
+tryRewrteEqAsSubst :: Ctxt -> Type -> Type -> Maybe (TVar,Type)
+tryRewrteEqAsSubst fins t1 t2 =
+  do let vars = Set.toList (Set.filter isFreeTV (fvs (t1,t2)))
+     listToMaybe $ sortBy (flip compare `on` rank)
+                 $ catMaybes [ tryRewriteEq fins var t1 t2 | var <- vars ]
+
+
+-- | Rank a rewrite, favoring expressions that have fewer subtractions than
+-- additions.
+rank :: (TVar,Type) -> Int
+rank (_,ty) = go ty
+  where
+
+  go (TCon (TF TCAdd) ts) = sum (map go ts) + 1
+  go (TCon (TF TCSub) ts) = sum (map go ts) - 1
+  go (TCon (TF TCMul) ts) = sum (map go ts) + 1
+  go (TCon (TF TCDiv) ts) = sum (map go ts) - 1
+  go (TCon _          ts) = sum (map go ts)
+  go _                    = 0
+
+
+-- | Rewrite an equation with respect to a unification variable ?x, into the
+-- form `?x = t`.  There are two interesting cases to consider (four with
+-- symmetry):
+--
+--  * ?x = ty
+--  * expr containing ?x = expr
+--
+-- In the first case, we just return the type variable and the type, but in the
+-- second we try to rewrite the equation until it's in the form of the first
+-- case.
+tryRewriteEq :: Map TVar Interval -> TVar -> Type -> Type -> Maybe (TVar,Type)
+tryRewriteEq fins uvar l r =
+  msum [ do guard (uvarTy == l && uvar `Set.notMember` rfvs)
+            return (uvar, r)
+
+       , do guard (uvarTy == r && uvar `Set.notMember` lfvs)
+            return (uvar, l)
+
+       , do guard (uvar `Set.notMember` rfvs)
+            ty <- rewriteLHS fins uvar l r
+            return (uvar,ty)
+
+       , do guard (uvar `Set.notMember` lfvs)
+            ty <- rewriteLHS fins uvar r l
+            return (uvar,ty)
+       ]
+
+  where
+
+  uvarTy = TVar uvar
+
+  lfvs   = fvs l
+  rfvs   = fvs r
+
+
+-- | Check that a type contains only finite type variables.
+allFin :: Map TVar Interval -> Type -> Bool
+allFin ints ty = iIsFin (typeInterval ints ty)
+
+
+-- | Rewrite an equality until the LHS is just `uvar`. Return the rewritten RHS.
+--
+-- There are a few interesting cases when rewriting the equality:
+--
+--  A o B = R  when `uvar` is only present in A
+--  A o B = R  when `uvar` is only present in B
+--
+-- In the first case, as we only consider addition and subtraction, the
+-- rewriting will continue on the left, after moving the `B` side to the RHS of
+-- the equation.  In the second case, if the operation is addition, the `A` side
+-- will be moved to the RHS, with rewriting continuing in `B`. However, in the
+-- case of subtraction, the `B` side is moved to the RHS, and rewriting
+-- continues on the RHS instead.
+--
+-- In both cases, if the operation is addition, rewriting will only continue if
+-- the operand being moved to the RHS is known to be finite. If this check was
+-- not done, we would end up violating the well-definedness condition for
+-- subtraction (for a, b: well defined (a - b) iff fin b).
+rewriteLHS :: Map TVar Interval -> TVar -> Type -> Type -> Maybe Type
+rewriteLHS fins uvar = go
+  where
+
+  go (TVar tv) rhs | tv == uvar = return rhs
+
+  go (TCon (TF tf) [x,y]) rhs =
+    do let xfvs = fvs x
+           yfvs = fvs y
+
+           inX  = Set.member uvar xfvs
+           inY  = Set.member uvar yfvs
+
+       if | inX && inY -> mzero
+          | inX        -> balanceR x tf y rhs
+          | inY        -> balanceL x tf y rhs
+          | otherwise  -> mzero
+
+
+  -- discard type synonyms, the rewriting will make them no longer apply
+  go (TUser _ _ l) rhs =
+       go l rhs
+
+  -- records won't work here.
+  go _ _ =
+       mzero
+
+
+  -- invert the type function to balance the equation, when the variable occurs
+  -- on the LHS of the expression `x tf y`
+  balanceR x TCAdd y rhs = do guardFin y
+                              go x (tSub rhs y)
+  balanceR x TCSub y rhs = go x (tAdd rhs y)
+  balanceR _ _     _ _   = mzero
+
+
+  -- invert the type function to balance the equation, when the variable occurs
+  -- on the RHS of the expression `x tf y`
+  balanceL x TCAdd y rhs = do guardFin y
+                              go y (tSub rhs x)
+  balanceL x TCSub y rhs = go (tAdd rhs y) x
+  balanceL _ _     _ _   = mzero
+
+
+  -- guard that the type is finite
+  --
+  -- XXX this ignores things like `min x inf` where x is finite, and just
+  -- assumes that it won't work.
+  guardFin ty = guard (allFin fins ty)
+-}
diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs
index a88b452c..92f5d78f 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs
@@ -1,267 +1,177 @@
-{-# LANGUAGE Trustworthy, PatternGuards, MultiWayIf #-}
+{-# LANGUAGE Safe, PatternGuards, MultiWayIf #-}
 module Cryptol.TypeCheck.Solver.Numeric
   ( cryIsEqual, cryIsNotEqual, cryIsGeq
   ) where
 
-import           Control.Monad (msum,guard,mzero)
-import           Data.Function (on)
-import           Data.List (sortBy)
-import           Data.Maybe (catMaybes,listToMaybe)
-import           Data.Map (Map)
-import qualified Data.Map as Map
-import qualified Data.Set as Set
+import           Control.Applicative(Alternative(..))
+import           Control.Monad (guard,mzero)
 
+import Cryptol.Utils.Patterns
 import Cryptol.TypeCheck.PP
 import Cryptol.TypeCheck.Type
+import Cryptol.TypeCheck.TypePat
 import Cryptol.TypeCheck.Solver.Types
 import Cryptol.TypeCheck.Solver.InfNat
 import Cryptol.TypeCheck.Solver.Numeric.Interval
+import Cryptol.TypeCheck.SimpType
 
-import Debug.Trace
 
-cryIsEqual :: Map TVar Interval -> Type -> Type -> Solved
-cryIsEqual fin t1 t2 =
-  solveOpts
-    [ pBin PEqual (==) fin t1 t2
-    , tIsNat' t1 `matchThen` \n -> tryEqK n t2
-    , tIsNat' t2 `matchThen` \n -> tryEqK n t1
-    , tIsVar t1 `matchThen` \tv -> tryEqInf tv t2
-    , tIsVar t2 `matchThen` \tv -> tryEqInf tv t1
-    , guarded (t1 == t2) $ SolvedIf []
-
-    -- x = min (K + x) y --> x = y
-    ]
-
-{-
-  case 
-    Unsolved
-      | Just x <- tIsVar t1, isFreeTV x -> Unsolved
-
-      | Just n <- tIsNat' t1 -> tryEqK n t2
-      | Just n <- tIsNat' t2 -> tryEqK n t1
-
-      | Just (x,t) <- tryRewrteEqAsSubst fin t1 t2 ->
-        let new = show (pp x) ++ " == " ++ show (pp t)
-        in
-          trace ("Rewrote: " ++ sh ++ " -> " ++ new)
-         $ SolvedIf [ TCon (PC PEqual) [TVar x,t] ]
-
-    Unsolved -> trace ("Failed to rewrite eq: " ++ sh) Unsolved
-
-    x -> x
-  where
-  sh = show (pp t1) ++ " == " ++ show (pp t2)
--}
+cryIsEqual :: Ctxt -> Type -> Type -> Solved
+cryIsEqual _ t1 t2 =
+  matchDefault Unsolved $
+        (pBin PEqual (==) t1 t2)
+    <|> (aNat' t1 >>= tryEqK t2)
+    <|> (aNat' t2 >>= tryEqK t1)
+    <|> (aTVar t1 >>= tryEqVar t2)
+    <|> (aTVar t2 >>= tryEqVar t1)
+    <|> ( guard (t1 == t2) >> return (SolvedIf []))
 
 
 
-cryIsNotEqual :: Map TVar Interval -> Type -> Type -> Solved
-cryIsNotEqual = pBin PNeq (/=)
+cryIsNotEqual :: Ctxt -> Type -> Type -> Solved
+cryIsNotEqual _i t1 t2 = matchDefault Unsolved (pBin PNeq (/=) t1 t2)
+
+cryIsGeq :: Ctxt -> Type -> Type -> Solved
+cryIsGeq i t1 t2 =
+  matchDefault Unsolved $
+        (pBin PGeq (>=) t1 t2)
+    <|> (aNat' t1 >>= tryGeqKThan i t2)
+    <|> (aTVar t2 >>= tryGeqThanVar i t1)
+    <|> tryGeqThanSub i t1 t2
+    <|> (geqByInterval i t1 t2)
+    <|> (guard (t1 == t2) >> return (SolvedIf []))
+
 
-cryIsGeq :: Map TVar Interval -> Type -> Type -> Solved
-cryIsGeq = pBin PGeq (>=)
   -- XXX: max a 10 >= 2 --> True
   -- XXX: max a 2 >= 10 --> a >= 10
 
 
-pBin :: PC -> (Nat' -> Nat' -> Bool) -> Map TVar Interval ->
-                                          Type -> Type -> Solved
-pBin tf p _i t1 t2
-  | Just e <- tIsError t1  = Unsolvable e
-  | Just e <- tIsError t2  = Unsolvable e
-  | Just x <- tIsNat' t1
-  , Just y <- tIsNat' t2 =
-      if p x y
-        then SolvedIf []
-        else Unsolvable $ TCErrorMessage
+pBin :: PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
+pBin tf p t1 t2 =
+      Unsolvable <$> anError t1
+  <|> Unsolvable <$> anError t2
+  <|> (do x <- aNat' t1
+          y <- aNat' t2
+          return $ if p x y
+                      then SolvedIf []
+                      else Unsolvable $ TCErrorMessage
                         $ "Predicate " ++ show (pp tf) ++ " does not hold for "
-                              ++ show x ++ " and " ++ show y
-pBin _ _ _ _ _ = Unsolved
+                              ++ show x ++ " and " ++ show y)
+
+
+--------------------------------------------------------------------------------
+-- GEQ
+
+tryGeqKThan :: Ctxt -> Type -> Nat' -> Match Solved
+tryGeqKThan _ _ Inf = return (SolvedIf [])
+tryGeqKThan _ ty (Nat n) =
+  do (a,b) <- aMul ty
+     m     <- aNat' a
+     return $ SolvedIf
+            $ case m of
+                Inf   -> [ b =#= tZero ]
+                Nat 0 -> []
+                Nat k -> [ tNum (div n k) >== b ]
+
+tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved
+tryGeqThanSub _ x y =
+  do (a,_) <- (|-|) y
+     guard (x == a)
+     return (SolvedIf [])
+
+tryGeqThanVar :: Ctxt -> Type -> TVar -> Match Solved
+tryGeqThanVar _ctxt ty x =
+  do (a,b) <- anAdd ty
+     let check y = do x' <- aTVar y
+                      guard (x == x')
+                      return (SolvedIf [])
+     check a <|> check b
+
+geqByInterval :: Ctxt -> Type -> Type -> Match Solved
+geqByInterval ctxt x y =
+  let ix = typeInterval ctxt x
+      iy = typeInterval ctxt y
+  in case (iLower ix, iUpper iy) of
+       (l,Just n) | l >= n -> return (SolvedIf [])
+       _                   -> mzero
 
 --------------------------------------------------------------------------------
 
 
-tryEqInf :: TVar -> Type -> Solved
-tryEqInf tv ty =
-  case tNoUser ty of
-    TCon (TF TCAdd) [a,b]
-      | Just n <- tIsNum a, n >= 1
-      , Just v <- tIsVar b, tv == v -> SolvedIf [ TVar tv =#= tInf ]
-    _ -> Unsolved
 
-tryEqK :: Nat' -> Type -> Solved
-tryEqK lk ty =
-  case tNoUser ty of
-    TCon (TF f) [ a, b ] | Just rk <- tIsNat' a ->
-      case f of
+tryEqVar :: Type -> TVar -> Match Solved
+tryEqVar ty x =
 
-        TCAdd ->
-          case (lk,rk) of
-            (_,Inf) -> Unsolved -- shouldn't happen, as `inf + x ` inf`
-            (Inf, Nat _) -> SolvedIf [ b =#= tInf ]
-            (Nat lk', Nat rk')
-              | lk' >= rk'  -> SolvedIf [ b =#= tNum (lk' - rk') ]
-              | otherwise -> Unsolvable
-                $ TCErrorMessage
-                $ "Adding " ++ show rk' ++ " will always exceed "
-                            ++ show lk'
+  -- x = K + x --> x = inf
+  (do (k,tv) <- matches ty (anAdd, aNat, aTVar)
+      guard (tv == x && k >= 1)
 
-        TCMul ->
-          case (lk,rk) of
-            (Inf,Inf)    -> SolvedIf [ b >== tOne ]
-            (Inf,Nat _)  -> SolvedIf [ b =#= tInf ]
-            (Nat 0, Inf) -> SolvedIf [ b =#= tZero ]
-            (Nat k, Inf) -> Unsolvable
-                          $ TCErrorMessage $ show k ++ " /= inf * anything"
-            (Nat lk', Nat rk')
-              | rk' == 0 -> Unsolved --- shouldn't happen, as `0 * x = x`
-              | (q,0) <- divMod lk' rk' -> SolvedIf [ b =#= tNum q ]
-              | otherwise -> Unsolvable
-                $ TCErrorMessage
-                $ show lk ++ " /= " ++ show rk ++ " * anything"
+      return $ SolvedIf [ TVar x =#= tInf ]
+  )
+  <|>
 
-        -- XXX: Min, Max, etx
-        -- 2  = min (10,y)  --> y = 2
-        -- 2  = min (2,y)   --> y >= 2
-        -- 10 = min (2,y)   --> impossible
-        _ -> Unsolved
-
-
-    _ -> Unsolved
+  -- x = min (K + x) y --> x = y
+  (do (l,r) <- aMin ty
+      let check this other =
+            do (k,x') <- matches this (anAdd, aNat', aTVar)
+               guard (x == x' && k >= Nat 1)
+               return $ SolvedIf [ TVar x =#= other ]
+      check l r <|> check r l
+  )
+  <|>
+  -- x = K + min a x
+  (do (k,(l,r)) <- matches ty (anAdd, aNat, aMin)
+      guard (k >= 1)
+      let check a b = do x' <- aTVar a
+                         guard (x' == x)
+                         return (SolvedIf [ TVar x =#= tAdd (tNum k) b ])
+      check l r <|> check r l
+  )
 
 
 
 
--- | When given an equality constraint, attempt to rewrite it to the form `?x =
--- ...`, by moving all occurrences of `?x` to the LHS, and any other variables
--- to the RHS.  This will only work when there's only one unification variable
--- present in the prop.
-
-tryRewrteEqAsSubst :: Map TVar Interval -> Type -> Type -> Maybe (TVar,Type)
-tryRewrteEqAsSubst fins t1 t2 =
-  do let vars = Set.toList (Set.filter isFreeTV (fvs (t1,t2)))
-     listToMaybe $ sortBy (flip compare `on` rank)
-                 $ catMaybes [ tryRewriteEq fins var t1 t2 | var <- vars ]
 
 
--- | Rank a rewrite, favoring expressions that have fewer subtractions than
--- additions.
-rank :: (TVar,Type) -> Int
-rank (_,ty) = go ty
-  where
 
-  go (TCon (TF TCAdd) ts) = sum (map go ts) + 1
-  go (TCon (TF TCSub) ts) = sum (map go ts) - 1
-  go (TCon (TF TCMul) ts) = sum (map go ts) + 1
-  go (TCon (TF TCDiv) ts) = sum (map go ts) - 1
-  go (TCon _          ts) = sum (map go ts)
-  go _                    = 0
+-- e.g., 10 = t
+tryEqK :: Type -> Nat' -> Match Solved
+tryEqK ty lk =
+
+  do (rk, b) <- matches ty (anAdd, aNat', __)
+     return $
+       case nSub lk rk of
+         -- NOTE: (Inf - Inf) shouldn't be possible
+         Nothing -> Unsolvable
+                      $ TCErrorMessage
+                      $ "Adding " ++ show rk ++ " will always exceed "
+                                  ++ show lk
+
+         Just r -> SolvedIf [ b =#= tNat' r ]
+  <|>
+  do (rk, b) <- matches ty (aMul, aNat', __)
+     return $
+       case (lk,rk) of
+         (Inf,Inf)    -> SolvedIf [ b >== tOne ]
+         (Inf,Nat _)  -> SolvedIf [ b =#= tInf ]
+         (Nat 0, Inf) -> SolvedIf [ b =#= tZero ]
+         (Nat k, Inf) -> Unsolvable
+                       $ TCErrorMessage
+                       $ show k ++ " /= inf * anything"
+         (Nat lk', Nat rk')
+           | rk' == 0 -> SolvedIf [ tNat' lk =#= tZero ]
+              -- shouldn't happen, as `0 * x = x`
+           | (q,0) <- divMod lk' rk' -> SolvedIf [ b =#= tNum q ]
+           | otherwise ->
+               Unsolvable
+             $ TCErrorMessage
+             $ show lk ++ " /= " ++ show rk ++ " * anything"
+
+  -- XXX: Min, Max, etx
+  -- 2  = min (10,y)  --> y = 2
+  -- 2  = min (2,y)   --> y >= 2
+  -- 10 = min (2,y)   --> impossible
 
 
--- | Rewrite an equation with respect to a unification variable ?x, into the
--- form `?x = t`.  There are two interesting cases to consider (four with
--- symmetry):
---
---  * ?x = ty
---  * expr containing ?x = expr
---
--- In the first case, we just return the type variable and the type, but in the
--- second we try to rewrite the equation until it's in the form of the first
--- case.
-tryRewriteEq :: Map TVar Interval -> TVar -> Type -> Type -> Maybe (TVar,Type)
-tryRewriteEq fins uvar l r =
-  msum [ do guard (uvarTy == l && uvar `Set.notMember` rfvs)
-            return (uvar, r)
-
-       , do guard (uvarTy == r && uvar `Set.notMember` lfvs)
-            return (uvar, l)
-
-       , do guard (uvar `Set.notMember` rfvs)
-            ty <- rewriteLHS fins uvar l r
-            return (uvar,ty)
-
-       , do guard (uvar `Set.notMember` lfvs)
-            ty <- rewriteLHS fins uvar r l
-            return (uvar,ty)
-       ]
-
-  where
-
-  uvarTy = TVar uvar
-
-  lfvs   = fvs l
-  rfvs   = fvs r
 
 
--- | Check that a type contains only finite type variables.
-allFin :: Map TVar Interval -> Type -> Bool
-allFin ints ty = iIsFin (typeInterval ints ty)
-
-
--- | Rewrite an equality until the LHS is just `uvar`. Return the rewritten RHS.
---
--- There are a few interesting cases when rewriting the equality:
---
---  A o B = R  when `uvar` is only present in A
---  A o B = R  when `uvar` is only present in B
---
--- In the first case, as we only consider addition and subtraction, the
--- rewriting will continue on the left, after moving the `B` side to the RHS of
--- the equation.  In the second case, if the operation is addition, the `A` side
--- will be moved to the RHS, with rewriting continuing in `B`. However, in the
--- case of subtraction, the `B` side is moved to the RHS, and rewriting
--- continues on the RHS instead.
---
--- In both cases, if the operation is addition, rewriting will only continue if
--- the operand being moved to the RHS is known to be finite. If this check was
--- not done, we would end up violating the well-definedness condition for
--- subtraction (for a, b: well defined (a - b) iff fin b).
-rewriteLHS :: Map TVar Interval -> TVar -> Type -> Type -> Maybe Type
-rewriteLHS fins uvar = go
-  where
-
-  go (TVar tv) rhs | tv == uvar = return rhs
-
-  go (TCon (TF tf) [x,y]) rhs =
-    do let xfvs = fvs x
-           yfvs = fvs y
-
-           inX  = Set.member uvar xfvs
-           inY  = Set.member uvar yfvs
-
-       if | inX && inY -> mzero
-          | inX        -> balanceR x tf y rhs
-          | inY        -> balanceL x tf y rhs
-          | otherwise  -> mzero
-
-
-  -- discard type synonyms, the rewriting will make them no longer apply
-  go (TUser _ _ l) rhs =
-       go l rhs
-
-  -- records won't work here.
-  go _ _ =
-       mzero
-
-
-  -- invert the type function to balance the equation, when the variable occurs
-  -- on the LHS of the expression `x tf y`
-  balanceR x TCAdd y rhs = do guardFin y
-                              go x (tSub rhs y)
-  balanceR x TCSub y rhs = go x (tAdd rhs y)
-  balanceR _ _     _ _   = mzero
-
-
-  -- invert the type function to balance the equation, when the variable occurs
-  -- on the RHS of the expression `x tf y`
-  balanceL x TCAdd y rhs = do guardFin y
-                              go y (tSub rhs x)
-  balanceL x TCSub y rhs = go (tAdd rhs y) x
-  balanceL _ _     _ _   = mzero
-
-
-  -- guard that the type is finite
-  --
-  -- XXX this ignores things like `min x inf` where x is finite, and just
-  -- assumes that it won't work.
-  guardFin ty = guard (allFin fins ty)
diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
index 9cfbc8f7..48766da0 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
@@ -20,7 +20,7 @@ module Cryptol.TypeCheck.Solver.Numeric.ImportExport
 
 import           Cryptol.TypeCheck.Solver.Numeric.AST
 import qualified Cryptol.TypeCheck.AST as Cry
-import qualified Cryptol.TypeCheck.SimpleSolver as SCry
+import qualified Cryptol.TypeCheck.SimpType as SCry
 import           MonadLib
 
 exportProp :: Cry.Prop -> Maybe Prop
diff --git a/src/Cryptol/TypeCheck/Solver/Types.hs b/src/Cryptol/TypeCheck/Solver/Types.hs
index 23c1bf10..bce062fc 100644
--- a/src/Cryptol/TypeCheck/Solver/Types.hs
+++ b/src/Cryptol/TypeCheck/Solver/Types.hs
@@ -1,13 +1,19 @@
 module Cryptol.TypeCheck.Solver.Types where
 
+import Data.Map(Map)
+
 import Cryptol.TypeCheck.Type
 import Cryptol.TypeCheck.PP
+import Cryptol.TypeCheck.Solver.Numeric.Interval
+
+type Ctxt = Map TVar Interval
 
 data Solved = SolvedIf [Prop]           -- ^ Solved, assuming the sub-goals.
             | Unsolved                  -- ^ We could not solve the goal.
             | Unsolvable TCErrorMessage -- ^ The goal can never be solved.
               deriving (Show)
 
+
 elseTry :: Solved -> Solved -> Solved
 Unsolved `elseTry` x = x
 x        `elseTry` _ = x
diff --git a/src/Cryptol/TypeCheck/Solver/Utils.hs b/src/Cryptol/TypeCheck/Solver/Utils.hs
index 546e73ef..0f845af1 100644
--- a/src/Cryptol/TypeCheck/Solver/Utils.hs
+++ b/src/Cryptol/TypeCheck/Solver/Utils.hs
@@ -8,8 +8,8 @@
 
 module Cryptol.TypeCheck.Solver.Utils where
 
-import Cryptol.TypeCheck.AST hiding (tAdd,tMul)
-import Cryptol.TypeCheck.SimpleSolver(tAdd,tMul)
+import Cryptol.TypeCheck.AST hiding (tMul)
+import Cryptol.TypeCheck.SimpType(tAdd,tMul)
 import Control.Monad(mplus,guard)
 import Data.Maybe(listToMaybe)
 
diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs
index aaddbd15..3ddc000e 100644
--- a/src/Cryptol/TypeCheck/Subst.hs
+++ b/src/Cryptol/TypeCheck/Subst.hs
@@ -25,6 +25,7 @@ module Cryptol.TypeCheck.Subst
   , apSubstTypeMapKeys
   , substBinds
   , applySubstToVar
+  , substToList
   ) where
 
 import           Data.Maybe
@@ -37,6 +38,7 @@ import qualified Data.Set as Set
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.PP
 import Cryptol.TypeCheck.TypeMap
+import qualified Cryptol.TypeCheck.SimpType as Simp
 import qualified Cryptol.TypeCheck.SimpleSolver as Simp
 import Cryptol.Utils.Panic(panic)
 import Cryptol.Utils.Misc(anyJust)
@@ -85,6 +87,11 @@ substBinds su
   | suDefaulting su = Set.empty
   | otherwise       = Map.keysSet $ suMap su
 
+substToList :: Subst -> [(TVar,Type)]
+substToList s
+  | suDefaulting s = panic "substToList" ["Defaulting substitution."]
+  | otherwise = Map.toList (suMap s)
+
 instance PP (WithNames Subst) where
   ppPrec _ (WithNames s mp)
     | null els  = text "(empty substitution)"
@@ -123,7 +130,7 @@ apSubstMaybe su ty =
                (TCLenFromThenTo,[t1,t2,t3])  -> Simp.tLenFromThenTo t1 t2 t3
                _ -> panic "apSubstMaybe" ["Unexpected type function", show t]
 
-           PC _ -> Just $! Simp.simplify Map.empty (TCon t ss)
+           PC _ ->Just $! Simp.simplify Map.empty (TCon t ss)
 
            _ -> return (TCon t ss)
 
diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
index 3f62c997..d887d479 100644
--- a/src/Cryptol/TypeCheck/Type.hs
+++ b/src/Cryptol/TypeCheck/Type.hs
@@ -486,12 +486,13 @@ tf2 f x y = TCon (TF f) [x,y]
 tf3 :: TFun -> Type -> Type -> Type -> Type
 tf3 f x y z = TCon (TF f) [x,y,z]
 
-
+{-
 tAdd :: Type -> Type -> Type
 tAdd x y
   | Just x' <- tIsNum x
   , Just y' <- tIsNum y = error (show x' ++ " + " ++ show y')
   | otherwise = tf2 TCAdd x y
+-}
 
 tSub :: Type -> Type -> Type
 tSub = tf2 TCSub
@@ -511,9 +512,6 @@ tExp = tf2 TCExp
 tMin :: Type -> Type -> Type
 tMin = tf2 TCMin
 
-tMax :: Type -> Type -> Type
-tMax = tf2 TCMax
-
 tWidth :: Type -> Type
 tWidth = tf1 TCWidth
 
@@ -682,6 +680,7 @@ instance PP (WithNames Type) where
       TRec fs -> braces $ fsep $ punctuate comma
                     [ pp l <+> text ":" <+> go 0 t | (l,t) <- fs ]
       TUser c ts _ -> optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts)
+      -- TUser _ _ t -> ppPrec prec t -- optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts)
 
       TCon (TC tc) ts ->
         case (tc,ts) of
diff --git a/src/Cryptol/TypeCheck/TypePat.hs b/src/Cryptol/TypeCheck/TypePat.hs
new file mode 100644
index 00000000..03f2f660
--- /dev/null
+++ b/src/Cryptol/TypeCheck/TypePat.hs
@@ -0,0 +1,171 @@
+module Cryptol.TypeCheck.TypePat
+  ( aInf, aNat, aNat'
+
+  , anAdd, (|-|), aMul, (|^|), (|/|), (|%|)
+  , aMin, aMax
+  , aWidth
+  , aLenFromThen, aLenFromThenTo
+
+  , aTVar
+  , aBit
+  , aSeq
+  , aWord
+  , aChar
+  , aTuple
+  , (|->|)
+
+  , aFin, (|=|), (|/=|), (|>=|)
+  , aCmp, aArith
+
+  , aAnd
+  , aTrue
+
+  , anError
+
+  , module Cryptol.Utils.Patterns
+  ) where
+
+import Control.Applicative((<|>))
+import Control.Monad
+import Cryptol.Utils.Patterns
+import Cryptol.TypeCheck.Type
+import Cryptol.TypeCheck.Solver.InfNat
+
+
+tcon :: TCon -> ([Type] -> a) -> Pat Type a
+tcon f p = \ty -> case tNoUser ty of
+                    TCon c ts | f == c -> return (p ts)
+                    _                  -> mzero
+
+ar0 :: [a] -> ()
+ar0 ~[] = ()
+
+ar1 :: [a] -> a
+ar1 ~[a] = a
+
+ar2 :: [a] -> (a,a)
+ar2 ~[a,b] = (a,b)
+
+ar3 :: [a] -> (a,a,a)
+ar3 ~[a,b,c] = (a,b,c)
+
+tf :: TFun -> ([Type] -> a) -> Pat Type a
+tf f ar = tcon (TF f) ar
+
+tc :: TC -> ([Type] -> a) -> Pat Type a
+tc f ar = tcon (TC f) ar
+
+tp :: PC -> ([Type] -> a) -> Pat Prop a
+tp f ar = tcon (PC f) ar
+
+
+--------------------------------------------------------------------------------
+
+aInf :: Pat Type ()
+aInf = tc TCInf ar0
+
+aNat :: Pat Type Integer
+aNat = \a -> case tNoUser a of
+               TCon (TC (TCNum n)) _ -> return n
+               _                     -> mzero
+
+aNat' :: Pat Type Nat'
+aNat' = \a -> (Inf <$  aInf a)
+          <|> (Nat <$> aNat a)
+
+anAdd :: Pat Type (Type,Type)
+anAdd = tf TCAdd ar2
+
+(|-|) :: Pat Type (Type,Type)
+(|-|) = tf TCSub ar2
+
+aMul :: Pat Type (Type,Type)
+aMul = tf TCMul ar2
+
+(|^|) :: Pat Type (Type,Type)
+(|^|) = tf TCExp ar2
+
+(|/|) :: Pat Type (Type,Type)
+(|/|) = tf TCDiv ar2
+
+(|%|) :: Pat Type (Type,Type)
+(|%|) = tf TCMod ar2
+
+aMin :: Pat Type (Type,Type)
+aMin = tf TCMin ar2
+
+aMax :: Pat Type (Type,Type)
+aMax = tf TCMax ar2
+
+aWidth :: Pat Type Type
+aWidth = tf TCWidth ar1
+
+aLenFromThen :: Pat Type (Type,Type,Type)
+aLenFromThen = tf TCLenFromThen ar3
+
+aLenFromThenTo :: Pat Type (Type,Type,Type)
+aLenFromThenTo = tf TCLenFromThenTo ar3
+
+--------------------------------------------------------------------------------
+aTVar :: Pat Type TVar
+aTVar = \a -> case tNoUser a of
+                TVar x -> return x
+                _      -> mzero
+
+aBit :: Pat Type ()
+aBit = tc TCBit ar0
+
+aSeq :: Pat Type (Type,Type)
+aSeq = tc TCSeq ar2
+
+aWord :: Pat Type Type
+aWord = \a -> do (l,t) <- aSeq a
+                 aBit t
+                 return l
+
+aChar :: Pat Type ()
+aChar = \a -> do (l,t) <- aSeq a
+                 n     <- aNat l
+                 guard (n == 8)
+                 aBit t
+
+aTuple :: Pat Type [Type]
+aTuple = \a -> case tNoUser a of
+                 TCon (TC (TCTuple _)) ts -> return ts
+                 _                        -> mzero
+
+(|->|) :: Pat Type (Type,Type)
+(|->|) = tc TCFun ar2
+--------------------------------------------------------------------------------
+
+aFin :: Pat Prop Type
+aFin = tp PFin ar1
+
+(|=|) :: Pat Prop (Type,Type)
+(|=|) = tp PEqual ar2
+
+(|/=|) :: Pat Prop (Type,Type)
+(|/=|) = tp PNeq ar2
+
+(|>=|) :: Pat Prop (Type,Type)
+(|>=|) = tp PGeq ar2
+
+aCmp :: Pat Prop Type
+aCmp = tp PCmp ar1
+
+aArith :: Pat Prop Type
+aArith = tp PArith ar1
+
+aAnd :: Pat Prop (Prop,Prop)
+aAnd = tp PAnd ar2
+
+aTrue :: Pat Prop ()
+aTrue = tp PTrue ar0
+
+--------------------------------------------------------------------------------
+anError :: Pat Type TCErrorMessage
+anError = \a -> case tNoUser a of
+                  TCon (TError _ err) _ -> return err
+                  _                     -> mzero
+
+
diff --git a/src/Cryptol/Utils/Panic.hs b/src/Cryptol/Utils/Panic.hs
index 6c36f4f6..6ce0c6b2 100644
--- a/src/Cryptol/Utils/Panic.hs
+++ b/src/Cryptol/Utils/Panic.hs
@@ -10,7 +10,7 @@
 {-# LANGUAGE DeriveDataTypeable, RecordWildCards #-}
 module Cryptol.Utils.Panic (panic) where
 
-import Cryptol.Version
+-- import Cryptol.Version
 
 import Control.Exception as X
 import Data.Typeable(Typeable)
@@ -29,7 +29,7 @@ instance Show CryptolPanic where
     , "*** Please create an issue at https://github.com/galoisinc/cryptol/issues"
     , ""
     , "%< --------------------------------------------------- "
-    ] ++ rev ++
+    ]{- ++ rev ++
     [ locLab ++ panicLoc p
     , msgLab ++ fromMaybe "" (listToMaybe msgLines)
     ]
@@ -47,7 +47,7 @@ instance Show CryptolPanic where
 
           rev | null commitHash = []
               | otherwise   = [ revLab ++ commitHash
-                              , branchLab ++ commitBranch ++ dirtyLab ]
+                              , branchLab ++ commitBranch ++ dirtyLab ] -}
 
 instance Exception CryptolPanic
 
diff --git a/src/Cryptol/Utils/Patterns.hs b/src/Cryptol/Utils/Patterns.hs
new file mode 100644
index 00000000..f0c01a69
--- /dev/null
+++ b/src/Cryptol/Utils/Patterns.hs
@@ -0,0 +1,136 @@
+{-# Language Safe, RankNTypes, MultiParamTypeClasses #-}
+{-# Language FunctionalDependencies #-}
+{-# Language FlexibleInstances #-}
+{-# Language TypeFamilies, UndecidableInstances #-}
+module Cryptol.Utils.Patterns where
+
+import Control.Monad(liftM,liftM2,ap,MonadPlus(..),guard)
+import Control.Applicative(Alternative(..))
+
+newtype Match b = Match (forall r. r -> (b -> r) -> r)
+
+instance Functor Match where
+  fmap = liftM
+
+instance Applicative Match where
+  pure a = Match $ \_no yes -> yes a
+  (<*>)  = ap
+
+instance Monad Match where
+  fail _ = empty
+  Match m >>= f = Match $ \no yes -> m no $ \a ->
+                                     let Match n = f a in
+                                     n no yes
+
+instance Alternative Match where
+  empty = Match $ \no _ -> no
+  Match m <|> Match n = Match $ \no yes -> m (n no yes) yes
+
+instance MonadPlus Match where
+
+type Pat a b = a -> Match b
+
+
+(|||) :: Pat a b -> Pat a b -> Pat a b
+p ||| q = \a -> p a <|> q a
+
+-- | Check that a value satisfies multiple patterns.
+-- For example, an "as" pattern is @(__ &&& p)@.
+(&&&) :: Pat a b -> Pat a c -> Pat a (b,c)
+p &&& q = \a -> liftM2 (,) (p a) (q a)
+
+-- | Match a value, and modify the result.
+(~>) :: Pat a b -> (b -> c) -> Pat a c
+p ~> f = \a -> f <$> p a
+
+-- | Match a value, and return the given result
+(~~>) :: Pat a b -> c -> Pat a c
+p ~~> f = \a -> f <$ p a
+
+-- | View pattern.
+(<~) :: (a -> b) -> Pat b c -> Pat a c
+f <~ p = \a -> p (f a)
+
+-- | Variable pattern.
+__ :: Pat a a
+__ = return
+
+-- | Constant pattern.
+succeed :: a -> Pat x a
+succeed = const . return
+
+-- | Predicate pattern
+checkThat :: (a -> Bool) -> Pat a ()
+checkThat p = \a -> guard (p a)
+
+-- | Check for exact value.
+lit :: Eq a => a -> Pat a ()
+lit x = checkThat (x ==)
+{-# Inline lit #-}
+
+
+-- | Match a pattern, using the given default if valure.
+matchDefault :: a -> Match a -> a
+matchDefault a (Match m) = m a id
+{-# Inline matchDefault #-}
+
+-- | Match an irrefutable pattern.  Crashes on faliure.
+match :: Match a -> a
+match m = matchDefault (error "Pattern match failure.") m
+{-# Inline match #-}
+
+matchMaybe :: Match a -> Maybe a
+matchMaybe (Match m) = m Nothing Just
+
+
+list :: [Pat a b] -> Pat [a] [b]
+list [] = \a ->
+  case a of
+    [] -> return []
+    _  -> mzero
+list (p : ps) = \as ->
+  case as of
+    []     -> mzero
+    x : xs ->
+      do a  <- p x
+         bs <- list ps xs
+         return (a : bs)
+
+
+(><) :: Pat a b -> Pat x y -> Pat (a,x) (b,y)
+p >< q = \(a,x) -> do b <- p a
+                      y <- q x
+                      return (b,y)
+
+class Matches thing pats res | pats -> thing res where
+  matches :: thing -> pats -> Match res
+
+instance ( f  ~ Pat a a1'
+         , a1 ~ Pat a1' r1
+         ) => Matches a (f,a1) r1 where
+  matches ty (f,a1) = do a1' <- f ty
+                         a1 a1'
+
+instance ( op ~ Pat a (a1',a2')
+         , a1 ~ Pat a1' r1
+         , a2 ~ Pat a2' r2
+         ) => Matches a (op,a1,a2) (r1,r2)
+  where
+  matches ty (f,a1,a2) = do (a1',a2') <- f ty
+                            r1 <- a1 a1'
+                            r2 <- a2 a2'
+                            return (r1,r2)
+
+instance ( op ~ Pat a (a1',a2',a3')
+         , a1 ~ Pat a1' r1
+         , a2 ~ Pat a2' r2
+         , a3 ~ Pat a3' r3
+         ) => Matches a (op,a1,a2,a3) (r1,r2,r3) where
+  matches ty (f,a1,a2,a3) = do (a1',a2',a3') <- f ty
+                               r1 <- a1 a1'
+                               r2 <- a2 a2'
+                               r3 <- a3 a3'
+                               return (r1,r2,r3)
+
+
+