    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 (Int -> Solved -> ShowS
    [Solved] -> ShowS
    Solved -> String
    (Int -> Solved -> ShowS)
    -> (Solved -> String) -> ([Solved] -> ShowS) -> Show Solved
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Solved] -> ShowS
    $cshowList :: [Solved] -> ShowS
    show :: Solved -> String
    $cshow :: Solved -> String
    showsPrec :: Int -> Solved -> ShowS
    $cshowsPrec :: Int -> Solved -> ShowS
    Show)

    elseTry :: Solved -> Solved -> Solved
    Unsolved elseTry :: Solved -> Solved -> Solved
    `elseTry` x :: Solved
    x = Solved
    x
    x :: Solved
    x        `elseTry` _ = Solved
    x

    solveOpts :: [Solved] -> Solved
    solveOpts :: [Solved] -> Solved
    solveOpts [] = Solved
    Unsolved
    solveOpts (x :: Solved
    x : xs :: [Solved]
    xs) = Solved
    x Solved -> Solved -> Solved
    `elseTry` [Solved] -> Solved
    solveOpts [Solved]
    xs

    matchThen :: Maybe a -> (a -> Solved) -> Solved
    matchThen :: Maybe a -> (a -> Solved) -> Solved
    matchThen Nothing _  = Solved
    Unsolved
    matchThen (Just a :: a
    a) f :: a -> Solved
    f = a -> Solved
    f a
    a

    guarded :: Bool -> Solved -> Solved
    guarded :: Bool -> Solved -> Solved
    guarded True x :: Solved
    x = Solved
    x
    guarded False _ = Solved
    Unsolved

    instance PP Solved where
      ppPrec :: Int -> Solved -> Doc
    ppPrec _ res :: Solved
    res =
        case Solved
    res of
          SolvedIf ps :: [Prop]
    ps  -> String -> Doc
    text "solved" Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Doc
    forall a. PP a => a -> Doc
    pp [Prop]
    ps))
          Unsolved     -> String -> Doc
    text "unsolved"
          Unsolvable e :: TCErrorMessage
    e -> String -> Doc
    text "unsolvable" Doc -> Doc -> Doc
    <.> Doc
    colon Doc -> Doc -> Doc
    <+> String -> Doc
    text (TCErrorMessage -> String
    tcErrorMessage TCErrorMessage
    e)