    -- |
    -- Module      :  Cryptol.TypeCheck.Solver.Class
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- Solving class constraints.
    -- If you make changes to this file, please update the documenation in RefMan.md

    {-# LANGUAGE PatternGuards #-}
    module Cryptol.TypeCheck.Solver.Class
      ( solveZeroInst
      , solveLogicInst
      , solveRingInst
      , solveFieldInst
      , solveIntegralInst
      , solveRoundInst
      , solveEqInst
      , solveCmpInst
      , solveSignedCmpInst
      , solveLiteralInst
      , solveLiteralLessThanInst
      , solveFLiteralInst
      , solveValidFloat
      ) where

    import qualified LibBF as FP

    import Cryptol.TypeCheck.Type hiding (tSub)
    import Cryptol.TypeCheck.SimpType (tAdd,tSub,tWidth,tMax)
    import Cryptol.TypeCheck.Solver.Types
    import Cryptol.Utils.RecordMap

    {- | This places constraints on the floating point numbers that
    we can work with.  This is a bit of an odd check, as it is really
    a limitiation of the backend, and not the language itself.

    On the other hand, it helps us give sane results if one accidentally
    types a polymorphic float at the REPL.  Hopefully, most users will
    stick to particular FP sizes, so this should be quite transparent.
    -}
    solveValidFloat :: Type -> Type -> Solved
    solveValidFloat :: Type -> Type -> Solved
    solveValidFloat Type
    e Type
    p
      | Just BFOpts
    _ <- Type -> Type -> Maybe BFOpts
    knownSupportedFloat Type
    e Type
    p = [Type] -> Solved
    SolvedIf []
      | Bool
    otherwise = Solved
    Unsolved

    -- | Check that the type parameters correspond to a float that
    -- we support, and if so make the precision settings for the BigFloat library.
    knownSupportedFloat :: Type -> Type -> Maybe FP.BFOpts
    knownSupportedFloat :: Type -> Type -> Maybe BFOpts
    knownSupportedFloat Type
    et Type
    pt
      | Just Integer
    e <- Type -> Maybe Integer
    tIsNum Type
    et, Just Integer
    p <- Type -> Maybe Integer
    tIsNum Type
    pt
      , Integer
    minExp Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    e Bool -> Bool -> Bool
    && Integer
    e Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    maxExp Bool -> Bool -> Bool
    && Integer
    minPrec Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    p Bool -> Bool -> Bool
    && Integer
    p Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    maxPrec =
        BFOpts -> Maybe BFOpts
    forall a. a -> Maybe a
    Just (Int -> BFOpts
    FP.expBits (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    e) BFOpts -> BFOpts -> BFOpts
    forall a. Semigroup a => a -> a -> a
    <> Word -> BFOpts
    FP.precBits (Integer -> Word
    forall a. Num a => Integer -> a
    fromInteger Integer
    p)
                                         BFOpts -> BFOpts -> BFOpts
    forall a. Semigroup a => a -> a -> a
    <> BFOpts
    FP.allowSubnormal)
      | Bool
    otherwise = Maybe BFOpts
    forall a. Maybe a
    Nothing
      where
      minExp :: Integer
    minExp  = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    2 (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    FP.expBitsMin)
      maxExp :: Integer
    maxExp  = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    FP.expBitsMax

      minPrec :: Integer
    minPrec = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    2 (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    FP.precBitsMin)
      maxPrec :: Integer
    maxPrec = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    FP.precBitsMax

    -- | Solve a Zero constraint by instance, if possible.
    solveZeroInst :: Type -> Solved
    solveZeroInst :: Type -> Solved
    solveZeroInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Zero Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Zero Bit
      TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf []

      -- Zero Integer
      TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf []

      -- Zero (Z n)
      TCon (TC TC
    TCIntMod) [Type
    n] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type
    n Type -> Type -> Type
    >== Type
    tOne ]

      -- Zero Real

      -- Zero Rational
      TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf []

      -- ValidVloat e p => Zero (Float e p)
      TCon (TC TC
    TCFloat) [Type
    e,Type
    p] -> [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p ]

      -- Zero a => Zero [n]a
      TCon (TC TC
    TCSeq) [Type
    _, Type
    a] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pZero Type
    a ]

      -- Zero b => Zero (a -> b)
      TCon (TC TC
    TCFun) [Type
    _, Type
    b] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pZero Type
    b ]

      -- (Zero a, Zero b) => Zero (a,b)
      TCon (TC (TCTuple Int
    _)) [Type]
    es -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pZero Type
    e | Type
    e <- [Type]
    es ]

      -- (Zero a, Zero b) => Zero { x1 : a, x2 : b }
      TRec RecordMap Ident Type
    fs -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pZero Type
    ety | Type
    ety <- RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs ]

      -- Zero <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve a Logic constraint by instance, if possible.
    solveLogicInst :: Type -> Solved
    solveLogicInst :: Type -> Solved
    solveLogicInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Logic Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Logic Bit
      TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf []

      -- Logic Integer fails
      TCon (TC TC
    TCInteger) [] -> Solved
    Unsolvable

      -- Logic (Z n) fails
      TCon (TC TC
    TCIntMod) [Type
    _] -> Solved
    Unsolvable

      -- Logic Rational fails
      TCon (TC TC
    TCRational) [] -> Solved
    Unsolvable

      -- Logic (Float e p) fails
      TCon (TC TC
    TCFloat) [Type
    _, Type
    _] -> Solved
    Unsolvable

      -- Logic a => Logic [n]a
      TCon (TC TC
    TCSeq) [Type
    _, Type
    a] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pLogic Type
    a ]

      -- Logic b => Logic (a -> b)
      TCon (TC TC
    TCFun) [Type
    _, Type
    b] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pLogic Type
    b ]

      -- (Logic a, Logic b) => Logic (a,b)
      TCon (TC (TCTuple Int
    _)) [Type]
    es -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pLogic Type
    e | Type
    e <- [Type]
    es ]

      -- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
      TRec RecordMap Ident Type
    fs -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pLogic Type
    ety | Type
    ety <- RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs ]

      -- Logic <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve a Ring constraint by instance, if possible.
    solveRingInst :: Type -> Solved
    solveRingInst :: Type -> Solved
    solveRingInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Ring Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Ring [n]e
      TCon (TC TC
    TCSeq) [Type
    n, Type
    e] -> Type -> Type -> Solved
    solveRingSeq Type
    n Type
    e

      -- Ring b => Ring (a -> b)
      TCon (TC TC
    TCFun) [Type
    _,Type
    b] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pRing Type
    b ]

      -- (Ring a, Ring b) => Arith (a,b)
      TCon (TC (TCTuple Int
    _)) [Type]
    es -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pRing Type
    e | Type
    e <- [Type]
    es ]

      -- Ring Bit fails
      TCon (TC TC
    TCBit) [] -> Solved
    Unsolvable

      -- Ring Integer
      TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf []

      -- Ring (Z n)
      TCon (TC TC
    TCIntMod) [Type
    n] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type
    n Type -> Type -> Type
    >== Type
    tOne ]

      -- Ring Rational
      TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf []

      -- ValidFloat e p => Ring (Float e p)
      TCon (TC TC
    TCFloat) [Type
    e,Type
    p] -> [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p ]

      -- (Ring a, Ring b) => Ring { x1 : a, x2 : b }
      TRec RecordMap Ident Type
    fs -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pRing Type
    ety | Type
    ety <- RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs ]

      -- Ring <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve a Ring constraint for a sequence.  The type passed here is the
    -- element type of the sequence.
    solveRingSeq :: Type -> Type -> Solved
    solveRingSeq :: Type -> Type -> Solved
    solveRingSeq Type
    n Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- fin n => Ring [n]Bit
      TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n ]

      -- variables are not solvable.
      TVar {} -> case Type -> Type
    tNoUser Type
    n of
                    {- We are sure that the lenght is not `fin`, so the
                    special case for `Bit` does not apply.
                    Arith ty => Arith [n]ty -}
                    TCon (TC TC
    TCInf) [] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pRing Type
    ty ]
                    Type
    _                  -> Solved
    Unsolved

      -- Ring ty => Ring [n]ty
      Type
    _ -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pRing Type
    ty ]

    -- | Solve an Integral constraint by instance, if possible.
    solveIntegralInst :: Type -> Solved
    solveIntegralInst :: Type -> Solved
    solveIntegralInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Integral Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Integral Bit fails
      TCon (TC TC
    TCBit) [] -> Solved
    Unsolvable

      -- Integral Integer
      TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf []

      -- fin n => Integral [n]
      TCon (TC TC
    TCSeq) [Type
    n, Type
    elTy] ->
        case Type -> Type
    tNoUser Type
    elTy of
          TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n ]
          TVar TVar
    _ -> Solved
    Unsolved
          Type
    _ -> Solved
    Unsolvable

      TVar TVar
    _ -> Solved
    Unsolved

      Type
    _ -> Solved
    Unsolvable

    -- | Solve a Field constraint by instance, if possible.
    solveFieldInst :: Type -> Solved
    solveFieldInst :: Type -> Solved
    solveFieldInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Field Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Field Bit fails
      TCon (TC TC
    TCBit) [] -> Solved
    Unsolvable

      -- Field Integer fails
      TCon (TC TC
    TCInteger) [] -> Solved
    Unsolvable

      -- Field Rational
      TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf []

      -- ValidFloat e p => Field (Float e p)
      TCon (TC TC
    TCFloat) [Type
    e,Type
    p] -> [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p ]

      -- Field Real

      -- Field (Z n)
      TCon (TC TC
    TCIntMod) [Type
    n] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pPrime Type
    n ]

      -- Field ([n]a) fails
      TCon (TC TC
    TCSeq) [Type
    _, Type
    _] -> Solved
    Unsolvable

      -- Field (a -> b) fails
      TCon (TC TC
    TCFun) [Type
    _, Type
    _] -> Solved
    Unsolvable

      -- Field (a, b, ...) fails
      TCon (TC (TCTuple Int
    _)) [Type]
    _ -> Solved
    Unsolvable

      -- Field {x : a, y : b, ...} fails
      TRec RecordMap Ident Type
    _ -> Solved
    Unsolvable

      -- Field <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve a Round constraint by instance, if possible.
    solveRoundInst :: Type -> Solved
    solveRoundInst :: Type -> Solved
    solveRoundInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Round Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Round Bit fails
      TCon (TC TC
    TCBit) [] -> Solved
    Unsolvable

      -- Round Integer fails
      TCon (TC TC
    TCInteger) [] -> Solved
    Unsolvable

      -- Round (Z n) fails
      TCon (TC TC
    TCIntMod) [Type
    _] -> Solved
    Unsolvable

      -- Round Rational
      TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf []

      -- ValidFloat e p => Round (Float e p)
      TCon (TC TC
    TCFloat) [Type
    e,Type
    p] -> [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p ]

      -- Round Real

      -- Round ([n]a) fails
      TCon (TC TC
    TCSeq) [Type
    _, Type
    _] -> Solved
    Unsolvable

      -- Round (a -> b) fails
      TCon (TC TC
    TCFun) [Type
    _, Type
    _] -> Solved
    Unsolvable

      -- Round (a, b, ...) fails
      TCon (TC (TCTuple Int
    _)) [Type]
    _ -> Solved
    Unsolvable

      -- Round {x : a, y : b, ...} fails
      TRec RecordMap Ident Type
    _ -> Solved
    Unsolvable

      -- Round <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve Eq constraints.
    solveEqInst :: Type -> Solved
    solveEqInst :: Type -> Solved
    solveEqInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Eq Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- eq Bit
      TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf []

      -- Eq Integer
      TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf []

      -- Eq Rational
      TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf []

      -- ValidFloat e p => Eq (Float e p)
      TCon (TC TC
    TCFloat) [Type
    e,Type
    p] -> [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p ]

      -- Eq (Z n)
      TCon (TC TC
    TCIntMod) [Type
    n] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type
    n Type -> Type -> Type
    >== Type
    tOne ]

      -- (fin n, Eq a) => Eq [n]a
      TCon (TC TC
    TCSeq) [Type
    n,Type
    a] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type -> Type
    pEq Type
    a ]

      -- (Eq a, Eq b) => Eq (a,b)
      TCon (TC (TCTuple Int
    _)) [Type]
    es -> [Type] -> Solved
    SolvedIf ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    pEq [Type]
    es)

      -- Eq (a -> b) fails
      TCon (TC TC
    TCFun) [Type
    _,Type
    _] -> Solved
    Unsolvable

      -- (Eq a, Eq b) => Eq { x:a, y:b }
      TRec RecordMap Ident Type
    fs -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pEq Type
    e | Type
    e <- RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs ]

      -- Eq <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve Cmp constraints.
    solveCmpInst :: Type -> Solved
    solveCmpInst :: Type -> Solved
    solveCmpInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- Cmp Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- Cmp Bit
      TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf []

      -- Cmp Integer
      TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf []

      -- Cmp Rational
      TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf []

      -- Cmp (Z n) fails
      TCon (TC TC
    TCIntMod) [Type
    _] -> Solved
    Unsolvable

      -- ValidFloat e p => Cmp (Float e p)
      TCon (TC TC
    TCFloat) [Type
    e,Type
    p] -> [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p ]

      -- (fin n, Cmp a) => Cmp [n]a
      TCon (TC TC
    TCSeq) [Type
    n,Type
    a] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type -> Type
    pCmp Type
    a ]

      -- (Cmp a, Cmp b) => Cmp (a,b)
      TCon (TC (TCTuple Int
    _)) [Type]
    es -> [Type] -> Solved
    SolvedIf ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    pCmp [Type]
    es)

      -- Cmp (a -> b) fails
      TCon (TC TC
    TCFun) [Type
    _,Type
    _] -> Solved
    Unsolvable

      -- (Cmp a, Cmp b) => Cmp { x:a, y:b }
      TRec RecordMap Ident Type
    fs -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pCmp Type
    e | Type
    e <- RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs ]

      -- Cmp <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solve a SignedCmp constraint for a sequence.  The type passed here is the
    -- element type of the sequence.
    solveSignedCmpSeq :: Type -> Type -> Solved
    solveSignedCmpSeq :: Type -> Type -> Solved
    solveSignedCmpSeq Type
    n Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- (fin n, n >=1 ) => SignedCmp [n]Bit
      TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type
    n Type -> Type -> Type
    >== Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    1 :: Integer) ]

      -- variables are not solvable.
      TVar {} -> Solved
    Unsolved

      -- (fin n, SignedCmp ty) => SignedCmp [n]ty, when ty != Bit
      Type
    _ -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    n, Type -> Type
    pSignedCmp Type
    ty ]

    -- | Solve SignedCmp constraints.
    solveSignedCmpInst :: Type -> Solved
    solveSignedCmpInst :: Type -> Solved
    solveSignedCmpInst Type
    ty = case Type -> Type
    tNoUser Type
    ty of

      -- SignedCmp Error -> fails
      TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

      -- SignedCmp Bit fails
      TCon (TC TC
    TCBit) [] -> Solved
    Unsolvable

      -- SignedCmp Integer fails
      TCon (TC TC
    TCInteger) [] -> Solved
    Unsolvable

      -- SignedCmp (Z n) fails
      TCon (TC TC
    TCIntMod) [Type
    _] -> Solved
    Unsolvable

      -- SignedCmp Rational fails
      TCon (TC TC
    TCRational) [] -> Solved
    Unsolvable

      -- SignedCmp (Float e p) fails
      TCon (TC TC
    TCFloat) [Type
    _, Type
    _] -> Solved
    Unsolvable

      -- SignedCmp for sequences
      TCon (TC TC
    TCSeq) [Type
    n,Type
    a] -> Type -> Type -> Solved
    solveSignedCmpSeq Type
    n Type
    a

      -- (SignedCmp a, SignedCmp b) => SignedCmp (a,b)
      TCon (TC (TCTuple Int
    _)) [Type]
    es -> [Type] -> Solved
    SolvedIf ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    pSignedCmp [Type]
    es)

      -- SignedCmp (a -> b) fails
      TCon (TC TC
    TCFun) [Type
    _,Type
    _] -> Solved
    Unsolvable

      -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
      TRec RecordMap Ident Type
    fs -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pSignedCmp Type
    e | Type
    e <- RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs ]

      -- SignedCmp <newtype> -> fails
      TNewtype{} -> Solved
    Unsolvable

      Type
    _ -> Solved
    Unsolved

    -- | Solving fractional literal constraints.
    solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved
    solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved
    solveFLiteralInst Type
    numT Type
    denT Type
    rndT Type
    ty
      | TCon (TError {}) [Type]
    _ <- Type -> Type
    tNoUser Type
    numT = Solved
    Unsolvable
      | TCon (TError {}) [Type]
    _ <- Type -> Type
    tNoUser Type
    denT = Solved
    Unsolvable
      | Type -> Bool
    tIsInf Type
    numT Bool -> Bool -> Bool
    || Type -> Bool
    tIsInf Type
    denT Bool -> Bool -> Bool
    || Type -> Bool
    tIsInf Type
    rndT = Solved
    Unsolvable
      | Just Integer
    0 <- Type -> Maybe Integer
    tIsNum Type
    denT = Solved
    Unsolvable

      | Bool
    otherwise =
        case Type -> Type
    tNoUser Type
    ty of
          TVar {} -> Solved
    Unsolved

          TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

          TCon (TC TC
    TCRational) [] ->
            [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    numT, Type -> Type
    pFin Type
    denT, Type
    denT Type -> Type -> Type
    >== Type
    tOne ]

          TCon (TC TC
    TCFloat) [Type
    e,Type
    p]
            | Just Integer
    0    <- Type -> Maybe Integer
    tIsNum Type
    rndT ->
              [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    pValidFloat Type
    e Type
    p
                       , Type -> Type
    pFin Type
    numT, Type -> Type
    pFin Type
    denT, Type
    denT Type -> Type -> Type
    >== Type
    tOne ]

            | Just Integer
    _    <- Type -> Maybe Integer
    tIsNum Type
    rndT
            , Just BFOpts
    opts <- Type -> Type -> Maybe BFOpts
    knownSupportedFloat Type
    e Type
    p
            , Just Integer
    n    <- Type -> Maybe Integer
    tIsNum Type
    numT
            , Just Integer
    d    <- Type -> Maybe Integer
    tIsNum Type
    denT
             -> case BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfDiv BFOpts
    opts (Integer -> BigFloat
    FP.bfFromInteger Integer
    n) (Integer -> BigFloat
    FP.bfFromInteger Integer
    d) of
                  (BigFloat
    _, Status
    FP.Ok) -> [Type] -> Solved
    SolvedIf []
                  (BigFloat, Status)
    _ -> Solved
    Unsolvable

            | Bool
    otherwise -> Solved
    Unsolved

          Type
    _ -> Solved
    Unsolvable

    -- | Solve Literal constraints.
    solveLiteralInst :: Type -> Type -> Solved
    solveLiteralInst :: Type -> Type -> Solved
    solveLiteralInst Type
    val Type
    ty
      | TCon (TError {}) [Type]
    _ <- Type -> Type
    tNoUser Type
    val = Solved
    Unsolvable
      | Bool
    otherwise =
        case Type -> Type
    tNoUser Type
    ty of

          -- Literal n Error -> fails
          TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

          -- (1 >= val) => Literal val Bit
          TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf [ Type
    tOne Type -> Type -> Type
    >== Type
    val ]

          -- (fin val) => Literal val Integer
          TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    val ]

          -- (fin val) => Literal val Rational
          TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    val ]

          -- ValidFloat e p => Literal val (Float e p)   if `val` is representable
          TCon (TC TC
    TCFloat) [Type
    e,Type
    p]
            | Just Integer
    n    <- Type -> Maybe Integer
    tIsNum Type
    val
            , Just BFOpts
    opts <- Type -> Type -> Maybe BFOpts
    knownSupportedFloat Type
    e Type
    p ->
              let bf :: BigFloat
    bf = Integer -> BigFloat
    FP.bfFromInteger Integer
    n
              in case BFOpts -> BigFloat -> (BigFloat, Status)
    FP.bfRoundFloat BFOpts
    opts BigFloat
    bf of
                   (BigFloat
    bf1,Status
    FP.Ok) | BigFloat
    bf BigFloat -> BigFloat -> Bool
    forall a. Eq a => a -> a -> Bool
    == BigFloat
    bf1 -> [Type] -> Solved
    SolvedIf []
                   (BigFloat, Status)
    _ -> Solved
    Unsolvable

            | Bool
    otherwise -> Solved
    Unsolved

          -- (fin val, fin m, m >= val + 1) => Literal val (Z m)
          TCon (TC TC
    TCIntMod) [Type
    modulus] ->
            [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    val, Type -> Type
    pFin Type
    modulus, Type
    modulus Type -> Type -> Type
    >== Type -> Type -> Type
    tAdd Type
    val Type
    tOne ]

          -- (fin bits, bits >= width n) => Literal n [bits]
          TCon (TC TC
    TCSeq) [Type
    bits, Type
    elTy]
            | TCon (TC TC
    TCBit) [] <- Type
    ety ->
                [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    val, Type -> Type
    pFin Type
    bits, Type
    bits Type -> Type -> Type
    >== Type -> Type
    tWidth Type
    val ]
            | TVar TVar
    _ <- Type
    ety -> Solved
    Unsolved
            where ety :: Type
    ety = Type -> Type
    tNoUser Type
    elTy

          TVar TVar
    _ -> Solved
    Unsolved

          Type
    _ -> Solved
    Unsolvable

    -- | Solve Literal constraints.
    solveLiteralLessThanInst :: Type -> Type -> Solved
    solveLiteralLessThanInst :: Type -> Type -> Solved
    solveLiteralLessThanInst Type
    val Type
    ty
      | TCon (TError {}) [Type]
    _ <- Type -> Type
    tNoUser Type
    val = Solved
    Unsolvable
      | Bool
    otherwise =
        case Type -> Type
    tNoUser Type
    ty of

          -- Literal n Error -> fails
          TCon (TError {}) [Type]
    _ -> Solved
    Unsolvable

          -- (2 >= val) => LiteralLessThan val Bit
          TCon (TC TC
    TCBit) [] -> [Type] -> Solved
    SolvedIf [ Type
    tTwo Type -> Type -> Type
    >== Type
    val ]

          -- LiteralLessThan val Integer
          TCon (TC TC
    TCInteger) [] -> [Type] -> Solved
    SolvedIf [ ]

          -- LiteralLessThan val Rational
          TCon (TC TC
    TCRational) [] -> [Type] -> Solved
    SolvedIf [ ]

          -- ValidFloat e p => LiteralLessThan val (Float e p)   if `val-1` is representable
          -- RWD Should we remove this instance for floats?
          TCon (TC TC
    TCFloat) [Type
    e, Type
    p]
            | Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    val
            , Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0
            , Just BFOpts
    opts  <- Type -> Type -> Maybe BFOpts
    knownSupportedFloat Type
    e Type
    p ->
              let bf :: BigFloat
    bf = Integer -> BigFloat
    FP.bfFromInteger (Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
              in case BFOpts -> BigFloat -> (BigFloat, Status)
    FP.bfRoundFloat BFOpts
    opts BigFloat
    bf of
                   (BigFloat
    bf1,Status
    FP.Ok) | BigFloat
    bf BigFloat -> BigFloat -> Bool
    forall a. Eq a => a -> a -> Bool
    == BigFloat
    bf1 -> [Type] -> Solved
    SolvedIf []
                   (BigFloat, Status)
    _ -> Solved
    Unsolvable

            | Bool
    otherwise -> Solved
    Unsolved

          -- (fin val, fin m, m >= val) => LiteralLessThan val (Z m)
          TCon (TC TC
    TCIntMod) [Type
    modulus] ->
            [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    val, Type -> Type
    pFin Type
    modulus, Type
    modulus Type -> Type -> Type
    >== Type
    val ]

          -- (fin bits, bits >= lg2 n) => LiteralLessThan n [bits]
          TCon (TC TC
    TCSeq) [Type
    bits, Type
    elTy]
            | TCon (TC TC
    TCBit) [] <- Type
    ety ->
                [Type] -> Solved
    SolvedIf [ Type -> Type
    pFin Type
    val, Type -> Type
    pFin Type
    bits, Type
    bits Type -> Type -> Type
    >== Type -> Type
    tWidth Type
    val' ]
            | TVar TVar
    _ <- Type
    ety -> Solved
    Unsolved
            where ety :: Type
    ety  = Type -> Type
    tNoUser Type
    elTy
                  val' :: Type
    val' = Type -> Type -> Type
    tSub (Type -> Type -> Type
    tMax Type
    val Type
    tOne) Type
    tOne

          TVar TVar
    _ -> Solved
    Unsolved

          Type
    _ -> Solved
    Unsolvable