    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE Safe #-}
    -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    module Cryptol.TypeCheck.SimpType where

    import Control.Applicative((<|>))
    import Cryptol.TypeCheck.Type hiding
      (tSub,tMul,tDiv,tMod,tExp,tMin,tCeilDiv,tCeilMod,tLenFromThenTo)
    import Cryptol.TypeCheck.TypePat
    import Cryptol.TypeCheck.Solver.InfNat
    import Control.Monad(msum,guard)

    tRebuild' :: Bool -> Type -> Type
    tRebuild' :: Bool -> Type -> Type
    tRebuild' Bool
    withUser = Type -> Type
    go
      where
      go :: Type -> Type
    go Type
    ty =
        case Type
    ty of
          TUser Name
    x [Type]
    xs Type
    t
            | Bool
    withUser  -> Name -> [Type] -> Type -> Type
    TUser Name
    x [Type]
    xs (Type -> Type
    go Type
    t)
            | Bool
    otherwise -> Type -> Type
    go Type
    t
          TVar TVar
    _        -> Type
    ty
          TRec RecordMap Ident Type
    xs       -> RecordMap Ident Type -> Type
    TRec ((Type -> Type) -> RecordMap Ident Type -> RecordMap Ident Type
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Type -> Type
    go RecordMap Ident Type
    xs)
          TNewtype Newtype
    nt [Type]
    xs -> Newtype -> [Type] -> Type
    TNewtype Newtype
    nt ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    go [Type]
    xs)
          TCon TCon
    tc [Type]
    ts    -> TCon -> [Type] -> Type
    tCon TCon
    tc ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    go [Type]
    ts)

    tRebuild :: Type -> Type
    tRebuild :: Type -> Type
    tRebuild = Bool -> Type -> Type
    tRebuild' Bool
    True

    tCon :: TCon -> [Type] -> Type
    tCon :: TCon -> [Type] -> Type
    tCon TCon
    tc [Type]
    ts =
      case TCon
    tc of
        TF TFun
    f ->
          case (TFun
    f, [Type]
    ts) of
            (TFun
    TCAdd, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tAdd Type
    x Type
    y
            (TFun
    TCSub, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tSub Type
    x Type
    y
            (TFun
    TCMul, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tMul Type
    x Type
    y
            (TFun
    TCExp, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tExp Type
    x Type
    y
            (TFun
    TCDiv, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tDiv Type
    x Type
    y
            (TFun
    TCMod, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tMod Type
    x Type
    y
            (TFun
    TCMin, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tMin Type
    x Type
    y
            (TFun
    TCMax, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tMax Type
    x Type
    y
            (TFun
    TCWidth, [Type
    x]) -> Type -> Type
    tWidth Type
    x
            (TFun
    TCCeilDiv, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tCeilDiv Type
    x Type
    y
            (TFun
    TCCeilMod, [Type
    x, Type
    y]) -> Type -> Type -> Type
    tCeilMod Type
    x Type
    y
            (TFun
    TCLenFromThenTo, [Type
    x, Type
    y, Type
    z]) -> Type -> Type -> Type -> Type
    tLenFromThenTo Type
    x Type
    y Type
    z
            (TFun, [Type])
    _ -> TCon -> [Type] -> Type
    TCon TCon
    tc [Type]
    ts
        TCon
    _ -> TCon -> [Type] -> Type
    TCon TCon
    tc [Type]
    ts

    -- Normal: constants to the left
    tAdd :: Type -> Type -> Type
    tAdd :: Type -> Type -> Type
    tAdd Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCAdd (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Nat'
    nAdd)) [Type
    x,Type
    y] = Type
    t
      | Type -> Bool
    tIsInf Type
    x            = Type
    tInf
      | Type -> Bool
    tIsInf Type
    y            = Type
    tInf
      | Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    x  = Integer -> Type -> Type
    addK Integer
    n Type
    y
      | Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    y  = Integer -> Type -> Type
    addK Integer
    n Type
    x
      | Just (Integer
    n,Type
    x1) <- Type -> Maybe (Integer, Type)
    isSumK Type
    x = Integer -> Type -> Type
    addK Integer
    n (Type -> Type -> Type
    tAdd Type
    x1 Type
    y)
      | Just (Integer
    n,Type
    y1) <- Type -> Maybe (Integer, Type)
    isSumK Type
    y = Integer -> Type -> Type
    addK Integer
    n (Type -> Type -> Type
    tAdd Type
    x Type
    y1)
      | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    (|-|) Type
    y
                                 Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    x Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    b)
                                 Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    a) = Type
    v
      | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    (|-|) Type
    x
                                 Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    b Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    y)
                                 Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    a) = Type
    v

      | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (Match Type
    factor Match Type -> Match Type -> Match Type
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Match Type
    same Match Type -> Match Type -> Match Type
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Match Type
    swapVars) = Type
    v

      | Bool
    otherwise           = TFun -> Type -> Type -> Type
    tf2 TFun
    TCAdd Type
    x Type
    y
      where
      isSumK :: Type -> Maybe (Integer, Type)
    isSumK Type
    t = case Type -> Type
    tNoUser Type
    t of
                   TCon (TF TFun
    TCAdd) [ Type
    l, Type
    r ] ->
                     do Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    l
                        (Integer, Type) -> Maybe (Integer, Type)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    n, Type
    r)
                   Type
    _ -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing

      addK :: Integer -> Type -> Type
    addK Integer
    0 Type
    t = Type
    t
      addK Integer
    n Type
    t | Just (Integer
    m,Type
    b) <- Type -> Maybe (Integer, Type)
    isSumK Type
    t = TFun -> Type -> Type -> Type
    tf2 TFun
    TCAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    m)) Type
    b
               | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe
                         (Match Type -> Maybe Type) -> Match Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    (|-|) Type
    t
                              (do Integer
    m <- Pat Type Integer
    aNat Type
    b
                                  Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Match Type) -> Type -> Match Type
    forall a b. (a -> b) -> a -> b
    $ case Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    n Integer
    m of
                                             Ordering
    GT -> Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    m)) Type
    a
                                             Ordering
    EQ -> Type
    a
                                             Ordering
    LT -> Type -> Type -> Type
    tSub Type
    a (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    mInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    n)))
                                Match Type -> Match Type -> Match Type
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
                                (do Integer
    m <- Pat Type Integer
    aNat Type
    a
                                    Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Type -> Type
    tSub (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    mInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    n)) Type
    b))
                          = Type
    v
               -- K + min a b ~> min (K + a) (K + b)
               | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe
                        (Match Type -> Maybe Type) -> Match Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    aMin Type
    t
                             Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Match Type) -> Type -> Match Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    tMin (Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) Type
    a) (Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) Type
    b)
                  = Type
    v

               | Bool
    otherwise              = TFun -> Type -> Type -> Type
    tf2 TFun
    TCAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) Type
    t

      factor :: Match Type
    factor = do (Type
    a,Type
    b1)  <- Pat Type (Type, Type)
    aMul Type
    x
                  (Type
    a',Type
    b2) <- Pat Type (Type, Type)
    aMul Type
    y
                  Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    a Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    a')
                  Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Type -> Type
    tMul Type
    a (Type -> Type -> Type
    tAdd Type
    b1 Type
    b2))

      same :: Match Type
    same = do Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    x Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    y)
                Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Type -> Type
    tMul (Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    2 :: Int)) Type
    x)

      swapVars :: Match Type
    swapVars = do TVar
    a <- Pat Type TVar
    aTVar Type
    x
                    TVar
    b <- Pat Type TVar
    aTVar Type
    y
                    Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar
    b TVar -> TVar -> Bool
    forall a. Ord a => a -> a -> Bool
    < TVar
    a)
                    Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TFun -> Type -> Type -> Type
    tf2 TFun
    TCAdd Type
    y Type
    x)

    tSub :: Type -> Type -> Type
    tSub :: Type -> Type -> Type
    tSub Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCSub ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Maybe Nat'
    nSub) [Type
    x,Type
    y] = Type
    t
      | Type -> Bool
    tIsInf Type
    y  = Type -> Type
    tError (TFun -> Type -> Type -> Type
    tf2 TFun
    TCSub Type
    x Type
    y)
      | Just Integer
    0 <- Maybe Integer
    yNum = Type
    x
      | Just Integer
    k <- Maybe Integer
    yNum
      , TCon (TF TFun
    TCAdd) [Type
    a,Type
    b] <- Type -> Type
    tNoUser Type
    x
      , Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    a = case Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    k Integer
    n of
                               Ordering
    EQ -> Type
    b
                               Ordering
    LT -> TFun -> Type -> Type -> Type
    tf2 TFun
    TCAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    k)) Type
    b
                               Ordering
    GT -> Type -> Type -> Type
    tSub Type
    b (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    n))

      | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    anAdd Type
    x
                                 (Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    a Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    y) Match () -> Match Type -> Match Type
    forall a b. Match a -> Match b -> Match b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    b)
                                    Match Type -> Match Type -> Match Type
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    b Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    y) Match () -> Match Type -> Match Type
    forall a b. Match a -> Match b -> Match b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    a))
                           = Type
    v

      | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    (|-|) Type
    y
                                 Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Type -> Type
    tSub (Type -> Type -> Type
    tAdd Type
    x Type
    b) Type
    a)) = Type
    v

      | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCSub Type
    x Type
    y
      where
      yNum :: Maybe Integer
    yNum = Type -> Maybe Integer
    tIsNum Type
    y

    -- Normal: constants to the left
    tMul :: Type -> Type -> Type
    tMul :: Type -> Type -> Type
    tMul Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCMul (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Nat'
    nMul)) [Type
    x,Type
    y] = Type
    t
      | Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    x  = Integer -> Type -> Type
    mulK Integer
    n Type
    y
      | Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    y  = Integer -> Type -> Type
    mulK Integer
    n Type
    x
      | Just Type
    v <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe Match Type
    swapVars = Type
    v
      | Bool
    otherwise           = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMul Type
    x Type
    y
      where
      mulK :: Integer -> Type -> Type
    mulK Integer
    0 Type
    _ = Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0 :: Int)
      mulK Integer
    1 Type
    t = Type
    t
      mulK Integer
    n Type
    t | TCon (TF TFun
    TCMul) [Type
    a,Type
    b] <- Type
    t'
               , Just Nat'
    a' <- Type -> Maybe Nat'
    tIsNat' Type
    a = case Nat'
    a' of
                                         Nat'
    Inf   -> Type
    t
                                         Nat Integer
    m -> TFun -> Type -> Type -> Type
    tf2 TFun
    TCMul (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    m)) Type
    b
               | TCon (TF TFun
    TCDiv) [Type
    a,Type
    b] <- Type
    t'
               , Just Integer
    b' <- Type -> Maybe Integer
    tIsNum Type
    b
               -- XXX: similar for a = b * k?
               , Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    b' = Type -> Type -> Type
    tSub Type
    a (Type -> Type -> Type
    tMod Type
    a Type
    b)

               | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMul (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) Type
    t
        where t' :: Type
    t' = Type -> Type
    tNoUser Type
    t

      swapVars :: Match Type
    swapVars = do TVar
    a <- Pat Type TVar
    aTVar Type
    x
                    TVar
    b <- Pat Type TVar
    aTVar Type
    y
                    Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar
    b TVar -> TVar -> Bool
    forall a. Ord a => a -> a -> Bool
    < TVar
    a)
                    Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TFun -> Type -> Type -> Type
    tf2 TFun
    TCMul Type
    y Type
    x)

    tDiv :: Type -> Type -> Type
    tDiv :: Type -> Type -> Type
    tDiv Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCDiv ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Maybe Nat'
    nDiv) [Type
    x,Type
    y] = Type
    t
      | Type -> Bool
    tIsInf Type
    x = Type
    bad
      | Just Integer
    0 <- Type -> Maybe Integer
    tIsNum Type
    y = Type
    bad
      | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCDiv Type
    x Type
    y
        where bad :: Type
    bad = Type -> Type
    tError (TFun -> Type -> Type -> Type
    tf2 TFun
    TCDiv Type
    x Type
    y)

    tMod :: Type -> Type -> Type
    tMod :: Type -> Type -> Type
    tMod Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCMod ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Maybe Nat'
    nMod) [Type
    x,Type
    y] = Type
    t
      | Type -> Bool
    tIsInf Type
    x = Type
    bad
      | Just Integer
    0 <- Type -> Maybe Integer
    tIsNum Type
    y = Type
    bad
      | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMod Type
    x Type
    y
        where bad :: Type
    bad = Type -> Type
    tError (TFun -> Type -> Type -> Type
    tf2 TFun
    TCMod Type
    x Type
    y)

    tCeilDiv :: Type -> Type -> Type
    tCeilDiv :: Type -> Type -> Type
    tCeilDiv Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCCeilDiv ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Maybe Nat'
    nCeilDiv) [Type
    x,Type
    y] = Type
    t
      | Type -> Bool
    tIsInf Type
    y = Type
    bad
      | Just Integer
    0 <- Type -> Maybe Integer
    tIsNum Type
    y = Type
    bad
      | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCCeilDiv Type
    x Type
    y
        where bad :: Type
    bad = Type -> Type
    tError (TFun -> Type -> Type -> Type
    tf2 TFun
    TCCeilDiv Type
    x Type
    y)

    tCeilMod :: Type -> Type -> Type
    tCeilMod :: Type -> Type -> Type
    tCeilMod Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCCeilMod ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Maybe Nat'
    nCeilMod) [Type
    x,Type
    y] = Type
    t
      | Type -> Bool
    tIsInf Type
    y = Type
    bad
      | Just Integer
    0 <- Type -> Maybe Integer
    tIsNum Type
    x = Type
    bad
      | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCCeilMod Type
    x Type
    y
        where bad :: Type
    bad = Type -> Type
    tError (TFun -> Type -> Type -> Type
    tf2 TFun
    TCCeilMod Type
    x Type
    y)

    tExp :: Type -> Type -> Type
    tExp :: Type -> Type -> Type
    tExp Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCExp (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Nat'
    nExp)) [Type
    x,Type
    y] = Type
    t
      | Just Integer
    0 <- Type -> Maybe Integer
    tIsNum Type
    y = Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    1 :: Int)
      | TCon (TF TFun
    TCExp) [Type
    a,Type
    b] <- Type -> Type
    tNoUser Type
    y = Type -> Type -> Type
    tExp Type
    x (Type -> Type -> Type
    tMul Type
    a Type
    b)
      | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCExp Type
    x Type
    y

    -- Normal: constants to the left
    tMin :: Type -> Type -> Type
    tMin :: Type -> Type -> Type
    tMin Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCMin (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Nat'
    nMin)) [Type
    x,Type
    y] = Type
    t
      | Just Nat'
    n <- Type -> Maybe Nat'
    tIsNat' Type
    x = Nat' -> Type -> Type
    minK Nat'
    n Type
    y
      | Just Nat'
    n <- Type -> Maybe Nat'
    tIsNat' Type
    y = Nat' -> Type -> Type
    minK Nat'
    n Type
    x
      | Just Type
    n <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (Type -> Type -> Match Type
    minPlusK Type
    x Type
    y Match Type -> Match Type -> Match Type
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Type
    minPlusK Type
    y Type
    x) = Type
    n
      | Just Type
    n <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (Match Type -> Maybe Type) -> Match Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ do (Nat'
    k,Type
    a) <- Type -> Match (Nat', Type)
    isMinK Type
    x
                                  Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Match Type) -> Type -> Match Type
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Type -> Type
    minK Nat'
    k (Type -> Type -> Type
    tMin Type
    a Type
    y)
                              Match Type -> Match Type -> Match Type
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
                              do (Nat'
    k,Type
    a) <- Type -> Match (Nat', Type)
    isMinK Type
    y
                                 Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Match Type) -> Type -> Match Type
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Type -> Type
    minK Nat'
    k (Type -> Type -> Type
    tMin Type
    x Type
    a)
        = Type
    n

      | Just Type
    n <- Match Type -> Maybe Type
    forall a. Match a -> Maybe a
    matchMaybe (Match Type -> Maybe Type) -> Match Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ do (Integer
    k1,Type
    a) <- Type -> Match (Integer, Type)
    isAddK Type
    x
                                  (Integer
    k2,Type
    b) <- Type -> Match (Integer, Type)
    isAddK Type
    y
                                  Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    a Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    b)
                                  Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Match Type) -> Type -> Match Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    k1 Integer
    k2)) Type
    a
        = Type
    n

      | Type
    x Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    y              = Type
    x
      -- XXX: min (k + t) t -> t
      | Bool
    otherwise           = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMin Type
    x Type
    y
      where
      isAddK :: Type -> Match (Integer, Type)
    isAddK Type
    ty = do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    anAdd Type
    ty
                     Integer
    k     <- Pat Type Integer
    aNat Type
    a
                     (Integer, Type) -> Match (Integer, Type)
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k,Type
    b)

      isMinK :: Type -> Match (Nat', Type)
    isMinK Type
    ty = do (Type
    a,Type
    b) <- Pat Type (Type, Type)
    aMin Type
    ty
                     Nat'
    k     <- Pat Type Nat'
    aNat' Type
    a
                     (Nat', Type) -> Match (Nat', Type)
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Nat'
    k,Type
    b)

      minPlusK :: Type -> Type -> Match Type
    minPlusK Type
    a Type
    b = do (Integer
    k,Type
    r) <- Type -> Match (Integer, Type)
    isAddK Type
    a
                        Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    1 Bool -> Bool -> Bool
    && Type
    b Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    r)
                        Type -> Match Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    b

      minK :: Nat' -> Type -> Type
    minK Nat'
    Inf Type
    t      = Type
    t
      minK (Nat Integer
    0) Type
    _  = Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0 :: Int)
      minK (Nat Integer
    k) Type
    t
        | TCon (TF TFun
    TCMin) [Type
    a,Type
    b] <- Type
    t'
        , Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    a   = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMin (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    k Integer
    n)) Type
    b

        | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMin (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    k) Type
    t
        where t' :: Type
    t' = Type -> Type
    tNoUser Type
    t

    -- Normal: constants to the left
    tMax :: Type -> Type -> Type
    tMax :: Type -> Type -> Type
    tMax Type
    x Type
    y
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCMax (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
    forall a b. (a -> a -> b) -> [a] -> b
    op2 Nat' -> Nat' -> Nat'
    nMax)) [Type
    x,Type
    y] = Type
    t
      | Just Nat'
    n <- Type -> Maybe Nat'
    tIsNat' Type
    x = Nat' -> Type -> Type
    maxK Nat'
    n Type
    y
      | Just Nat'
    n <- Type -> Maybe Nat'
    tIsNat' Type
    y = Nat' -> Type -> Type
    maxK Nat'
    n Type
    x
      | Bool
    otherwise           = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMax Type
    x Type
    y
      where
      maxK :: Nat' -> Type -> Type
    maxK Nat'
    Inf Type
    _     = Type
    tInf
      maxK (Nat Integer
    0) Type
    t = Type
    t
      maxK (Nat Integer
    k) Type
    t

        -- max 1 t ~> t,   if t = a ^ b && a >= 1
        | Integer
    k Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1
        , TCon (TF TFun
    TCExp) [Type
    a,Type
    _] <- Type
    t'
        , Just Nat'
    base <- Type -> Maybe Nat'
    tIsNat' Type
    a
        , Nat'
    base Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer -> Nat'
    Nat Integer
    1 = Type
    t

        | TCon (TF TFun
    TCAdd) [Type
    a,Type
    b] <- Type
    t'
        , Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    a = if Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n
                                 then Type
    t
                                 else Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) (Type -> Type -> Type
    tMax (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    n)) Type
    b)

        | TCon (TF TFun
    TCSub) [Type
    a,Type
    b] <- Type
    t'
        , Just Nat'
    n <- Type -> Maybe Nat'
    tIsNat' Type
    a =
          case Nat'
    n of
            Nat'
    Inf   -> Type
    t
            Nat Integer
    m -> if Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    m then Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    k else Type -> Type -> Type
    tSub Type
    a (Type -> Type -> Type
    tMin (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    k)) Type
    b)

        | TCon (TF TFun
    TCMax) [Type
    a,Type
    b] <- Type
    t'
        , Just Integer
    n <- Type -> Maybe Integer
    tIsNum Type
    a  = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMax (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    k Integer
    n)) Type
    b

        | Bool
    otherwise = TFun -> Type -> Type -> Type
    tf2 TFun
    TCMax (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    k) Type
    t
        where t' :: Type
    t' = Type -> Type
    tNoUser Type
    t

    tWidth :: Type -> Type
    tWidth :: Type -> Type
    tWidth Type
    x
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCWidth (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total ((Nat' -> Nat') -> [Nat'] -> Nat'
    forall a b. (a -> b) -> [a] -> b
    op1 Nat' -> Nat'
    nWidth)) [Type
    x] = Type
    t

      -- width (2^n - 1) = n
      | TCon (TF TFun
    TCSub) [Type
    a,Type
    b] <- Type -> Type
    tNoUser Type
    x
      , Just Integer
    1 <- Type -> Maybe Integer
    tIsNum Type
    b
      , TCon (TF TFun
    TCExp) [Type
    p,Type
    q] <- Type -> Type
    tNoUser Type
    a
      , Just Integer
    2 <- Type -> Maybe Integer
    tIsNum Type
    p = Type
    q

      | Bool
    otherwise = TFun -> Type -> Type
    tf1 TFun
    TCWidth Type
    x

    tLenFromThenTo :: Type -> Type -> Type -> Type
    tLenFromThenTo :: Type -> Type -> Type -> Type
    tLenFromThenTo Type
    x Type
    y Type
    z
      | Just Type
    t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    TCLenFromThenTo ((Nat' -> Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
    forall a b. (a -> a -> a -> b) -> [a] -> b
    op3 Nat' -> Nat' -> Nat' -> Maybe Nat'
    nLenFromThenTo) [Type
    x,Type
    y,Type
    z] = Type
    t
      | Bool
    otherwise = TFun -> Type -> Type -> Type -> Type
    tf3 TFun
    TCLenFromThenTo Type
    x Type
    y Type
    z

    total :: ([Nat'] -> Nat') -> ([Nat'] -> Maybe Nat')
    total :: ([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
    total [Nat'] -> Nat'
    f [Nat']
    xs = Nat' -> Maybe Nat'
    forall a. a -> Maybe a
    Just ([Nat'] -> Nat'
    f [Nat']
    xs)

    op1 :: (a -> b) -> [a] -> b
    op1 :: forall a b. (a -> b) -> [a] -> b
    op1 a -> b
    f ~[a
    x] = a -> b
    f a
    x

    op2 :: (a -> a -> b) -> [a] -> b
    op2 :: forall a b. (a -> a -> b) -> [a] -> b
    op2 a -> a -> b
    f ~[a
    x,a
    y] = a -> a -> b
    f a
    x a
    y

    op3 :: (a -> a -> a -> b) -> [a] -> b
    op3 :: forall a b. (a -> a -> a -> b) -> [a] -> b
    op3 a -> a -> a -> b
    f ~[a
    x,a
    y,a
    z] = a -> a -> a -> b
    f a
    x a
    y a
    z

    -- | Common checks: check for error, or simple full evaluation.
    -- We assume that input kinds and the result kind are the same (i.e., Nat)
    tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
    tOp TFun
    tf [Nat'] -> Maybe Nat'
    f [Type]
    ts
      | Just Type
    t <- [Maybe Type] -> Maybe Type
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ((Type -> Maybe Type) -> [Type] -> [Maybe Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Maybe Type
    tIsError [Type]
    ts) = Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Type
    tError Type
    t)
        -- assumes result kind the same as input kind

      | Just [Nat']
    xs <- (Type -> Maybe Nat') -> [Type] -> Maybe [Nat']
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Type -> Maybe Nat'
    tIsNat' [Type]
    ts =
          Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ case [Nat'] -> Maybe Nat'
    f [Nat']
    xs of
                   Maybe Nat'
    Nothing -> Type -> Type
    tError (TCon -> [Type] -> Type
    TCon (TFun -> TCon
    TF TFun
    tf) ((Nat' -> Type) -> [Nat'] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat' -> Type
    tNat' [Nat']
    xs))
                   Just Nat'
    n  -> Nat' -> Type
    tNat' Nat'
    n
      | Bool
    otherwise = Maybe Type
    forall a. Maybe a
    Nothing