    {-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass, Safe #-}
    module Cryptol.TypeCheck.TCon where

    import qualified Data.Map as Map
    import GHC.Generics (Generic)
    import Control.DeepSeq

    import Cryptol.Parser.Selector
    import qualified Cryptol.ModuleSystem.Name as M
    import Cryptol.Utils.Fixity
    import Cryptol.Utils.Ident
    import Cryptol.Utils.PP

    -- | This is used for pretty prinitng.
    -- XXX: it would be nice to just rely in the info from the Prelude.
    infixPrimTy :: TCon -> Maybe (Ident,Fixity)
    infixPrimTy :: TCon -> Maybe (Ident, Fixity)
    infixPrimTy = \TCon
    tc -> TCon -> Map TCon (Ident, Fixity) -> Maybe (Ident, Fixity)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TCon
    tc Map TCon (Ident, Fixity)
    mp
      where
      mp :: Map TCon (Ident, Fixity)
    mp = [(TCon, (Ident, Fixity))] -> Map TCon (Ident, Fixity)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
              [ String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix String
    "=="  PC -> TCon
    PC PC
    PEqual    (Int -> Fixity
    n Int
    20)
              , String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix String
    "!="  PC -> TCon
    PC PC
    PNeq      (Int -> Fixity
    n Int
    20)
              , String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix String
    ">="  PC -> TCon
    PC PC
    PGeq      (Int -> Fixity
    n Int
    30)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "+"  TFun -> TCon
    TF TFun
    TCAdd     (Int -> Fixity
    l Int
    80)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "-"  TFun -> TCon
    TF TFun
    TCSub     (Int -> Fixity
    l Int
    80)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "*"  TFun -> TCon
    TF TFun
    TCMul     (Int -> Fixity
    l Int
    90)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "/"  TFun -> TCon
    TF TFun
    TCDiv     (Int -> Fixity
    l Int
    90)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "%"  TFun -> TCon
    TF TFun
    TCMod     (Int -> Fixity
    l Int
    90)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "^^" TFun -> TCon
    TF TFun
    TCExp     (Int -> Fixity
    r Int
    95)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "/^" TFun -> TCon
    TF TFun
    TCCeilDiv (Int -> Fixity
    l Int
    90)
              , String
    -> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
    forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix  String
    "%^" TFun -> TCon
    TF TFun
    TCCeilMod (Int -> Fixity
    l Int
    90)
              ]

      r :: Int -> Fixity
    r Int
    x = Fixity { fAssoc :: Assoc
    fAssoc = Assoc
    RightAssoc, fLevel :: Int
    fLevel = Int
    x }
      l :: Int -> Fixity
    l Int
    x = Fixity { fAssoc :: Assoc
    fAssoc = Assoc
    LeftAssoc,  fLevel :: Int
    fLevel = Int
    x }
      n :: Int -> Fixity
    n Int
    x = Fixity { fAssoc :: Assoc
    fAssoc = Assoc
    NonAssoc,   fLevel :: Int
    fLevel = Int
    x }

      tInfix :: String -> (t -> a) -> t -> b -> (a, (Ident, b))
    tInfix String
    x t -> a
    mk t
    tc b
    f = (t -> a
    mk t
    tc, (String -> Ident
    packIdent String
    x, b
    f))

    builtInType :: M.Name -> Maybe TCon
    builtInType :: Name -> Maybe TCon
    builtInType Name
    nm =
      case Name -> NameInfo
    M.nameInfo Name
    nm of
        M.GlobalName NameSource
    _ OrigName { ogModule :: OrigName -> ModPath
    ogModule = ModPath
    m }
          | ModPath
    m ModPath -> ModPath -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName -> ModPath
    M.TopModule ModName
    preludeName -> Ident -> Map Ident TCon -> Maybe TCon
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Name -> Ident
    M.nameIdent Name
    nm) Map Ident TCon
    builtInTypes
          | ModPath
    m ModPath -> ModPath -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName -> ModPath
    M.TopModule ModName
    floatName   -> Ident -> Map Ident TCon -> Maybe TCon
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Name -> Ident
    M.nameIdent Name
    nm) Map Ident TCon
    builtInFloat
          | ModPath
    m ModPath -> ModPath -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName -> ModPath
    M.TopModule ModName
    arrayName   -> Ident -> Map Ident TCon -> Maybe TCon
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Name -> Ident
    M.nameIdent Name
    nm) Map Ident TCon
    builtInArray
        NameInfo
    _ -> Maybe TCon
    forall a. Maybe a
    Nothing

      where
      String
    x ~> :: String -> b -> (Ident, b)
    ~> b
    y = (String -> Ident
    packIdent String
    x, b
    y)

      -- Built-in types from Float.cry
      builtInFloat :: Map Ident TCon
    builtInFloat = [(Ident, TCon)] -> Map Ident TCon
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
        [ String
    "Float"             String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCFloat
        , String
    "ValidFloat"        String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PValidFloat
        ]

      -- Built-in types from Cryptol.cry
      builtInTypes :: Map Ident TCon
    builtInTypes = [(Ident, TCon)] -> Map Ident TCon
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
        [ -- Types
          String
    "inf"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCInf
        , String
    "Bit"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCBit
        , String
    "Integer"           String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCInteger
        , String
    "Rational"          String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCRational
        , String
    "Z"                 String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCIntMod

          -- Predicate contstructors
        , String
    "=="                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PEqual
        , String
    "!="                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PNeq
        , String
    ">="                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PGeq
        , String
    "fin"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PFin
        , String
    "prime"             String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PPrime
        , String
    "Zero"              String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PZero
        , String
    "Logic"             String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PLogic
        , String
    "Ring"              String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PRing
        , String
    "Integral"          String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PIntegral
        , String
    "Field"             String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PField
        , String
    "Round"             String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PRound
        , String
    "Eq"                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PEq
        , String
    "Cmp"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PCmp
        , String
    "SignedCmp"         String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PSignedCmp
        , String
    "Literal"           String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PLiteral
        , String
    "LiteralLessThan"   String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PLiteralLessThan
        , String
    "FLiteral"          String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> PC -> TCon
    PC PC
    PFLiteral

        -- Type functions
        , String
    "+"                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCAdd
        , String
    "-"                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCSub
        , String
    "*"                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCMul
        , String
    "/"                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCDiv
        , String
    "%"                String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCMod
        , String
    "^^"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCExp
        , String
    "width"            String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCWidth
        , String
    "min"              String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCMin
        , String
    "max"              String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCMax
        , String
    "/^"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCCeilDiv
        , String
    "%^"               String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCCeilMod
        , String
    "lengthFromThenTo" String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TFun -> TCon
    TF TFun
    TCLenFromThenTo
        ]

      -- Built-in types from Array.cry
      builtInArray :: Map Ident TCon
    builtInArray = [(Ident, TCon)] -> Map Ident TCon
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
        [ String
    "Array" String -> TCon -> (Ident, TCon)
    forall {b}. String -> b -> (Ident, b)
    ~> TC -> TCon
    TC TC
    TCArray
        ]

    --------------------------------------------------------------------------------

    infixr 5 :->

    -- | Kinds, classify types.
    data Kind   = KType
                | KNum
                | KProp
                | Kind :-> Kind
                  deriving (Kind -> Kind -> Bool
    (Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Kind -> Kind -> Bool
    == :: Kind -> Kind -> Bool
    $c/= :: Kind -> Kind -> Bool
    /= :: Kind -> Kind -> Bool
    Eq, Eq Kind
    Eq Kind
    -> (Kind -> Kind -> Ordering)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Kind)
    -> (Kind -> Kind -> Kind)
    -> Ord Kind
    Kind -> Kind -> Bool
    Kind -> Kind -> Ordering
    Kind -> Kind -> Kind
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Kind -> Kind -> Ordering
    compare :: Kind -> Kind -> Ordering
    $c< :: Kind -> Kind -> Bool
    < :: Kind -> Kind -> Bool
    $c<= :: Kind -> Kind -> Bool
    <= :: Kind -> Kind -> Bool
    $c> :: Kind -> Kind -> Bool
    > :: Kind -> Kind -> Bool
    $c>= :: Kind -> Kind -> Bool
    >= :: Kind -> Kind -> Bool
    $cmax :: Kind -> Kind -> Kind
    max :: Kind -> Kind -> Kind
    $cmin :: Kind -> Kind -> Kind
    min :: Kind -> Kind -> Kind
    Ord, Int -> Kind -> ShowS
    [Kind] -> ShowS
    Kind -> String
    (Int -> Kind -> ShowS)
    -> (Kind -> String) -> ([Kind] -> ShowS) -> Show Kind
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Kind -> ShowS
    showsPrec :: Int -> Kind -> ShowS
    $cshow :: Kind -> String
    show :: Kind -> String
    $cshowList :: [Kind] -> ShowS
    showList :: [Kind] -> ShowS
    Show, (forall x. Kind -> Rep Kind x)
    -> (forall x. Rep Kind x -> Kind) -> Generic Kind
    forall x. Rep Kind x -> Kind
    forall x. Kind -> Rep Kind x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Kind -> Rep Kind x
    from :: forall x. Kind -> Rep Kind x
    $cto :: forall x. Rep Kind x -> Kind
    to :: forall x. Rep Kind x -> Kind
    Generic, Kind -> ()
    (Kind -> ()) -> NFData Kind
    forall a. (a -> ()) -> NFData a
    $crnf :: Kind -> ()
    rnf :: Kind -> ()
    NFData)

    class HasKind t where
      kindOf :: t -> Kind

    instance HasKind TCon where
      kindOf :: TCon -> Kind
    kindOf (TC TC
    tc)      = TC -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TC
    tc
      kindOf (PC PC
    pc)      = PC -> Kind
    forall t. HasKind t => t -> Kind
    kindOf PC
    pc
      kindOf (TF TFun
    tf)      = TFun -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TFun
    tf
      kindOf (TError Kind
    k)   = Kind
    k

    instance HasKind UserTC where
      kindOf :: UserTC -> Kind
    kindOf (UserTC Name
    _ Kind
    k) = Kind
    k

    instance HasKind TC where
      kindOf :: TC -> Kind
    kindOf TC
    tcon =
        case TC
    tcon of
          TCNum Integer
    _   -> Kind
    KNum
          TC
    TCInf     -> Kind
    KNum
          TC
    TCBit     -> Kind
    KType
          TC
    TCInteger -> Kind
    KType
          TC
    TCRational -> Kind
    KType
          TC
    TCFloat   -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KType
          TC
    TCIntMod  -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KType
          TC
    TCArray   -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KType
          TC
    TCSeq     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KType
          TC
    TCFun     -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KType
          TCTuple Int
    n -> (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Kind -> Kind -> Kind
    (:->) Kind
    KType (Int -> Kind -> [Kind]
    forall a. Int -> a -> [a]
    replicate Int
    n Kind
    KType)
          TCAbstract UserTC
    x -> UserTC -> Kind
    forall t. HasKind t => t -> Kind
    kindOf UserTC
    x

    instance HasKind PC where
      kindOf :: PC -> Kind
    kindOf PC
    pc =
        case PC
    pc of
          PC
    PEqual     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PNeq       -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PGeq       -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PFin       -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PPrime     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KProp
          PHas Selector
    _     -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PZero      -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PLogic     -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PRing      -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PIntegral  -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PField     -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PRound     -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PEq        -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PCmp       -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PSignedCmp -> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PLiteral   -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PLiteralLessThan -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PFLiteral  -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KType Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PValidFloat -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PAnd       -> Kind
    KProp Kind -> Kind -> Kind
    :-> Kind
    KProp Kind -> Kind -> Kind
    :-> Kind
    KProp
          PC
    PTrue      -> Kind
    KProp

    instance HasKind TFun where
      kindOf :: TFun -> Kind
    kindOf TFun
    tfun =
        case TFun
    tfun of
          TFun
    TCWidth   -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum

          TFun
    TCAdd     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCSub     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCMul     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCDiv     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCMod     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCExp     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCMin     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCMax     -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCCeilDiv -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum
          TFun
    TCCeilMod -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum

          TFun
    TCLenFromThenTo -> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum Kind -> Kind -> Kind
    :-> Kind
    KNum

    -- | Type constants.
    data TCon   = TC TC | PC PC | TF TFun | TError Kind
                  deriving (Int -> TCon -> ShowS
    [TCon] -> ShowS
    TCon -> String
    (Int -> TCon -> ShowS)
    -> (TCon -> String) -> ([TCon] -> ShowS) -> Show TCon
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TCon -> ShowS
    showsPrec :: Int -> TCon -> ShowS
    $cshow :: TCon -> String
    show :: TCon -> String
    $cshowList :: [TCon] -> ShowS
    showList :: [TCon] -> ShowS
    Show, TCon -> TCon -> Bool
    (TCon -> TCon -> Bool) -> (TCon -> TCon -> Bool) -> Eq TCon
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TCon -> TCon -> Bool
    == :: TCon -> TCon -> Bool
    $c/= :: TCon -> TCon -> Bool
    /= :: TCon -> TCon -> Bool
    Eq, Eq TCon
    Eq TCon
    -> (TCon -> TCon -> Ordering)
    -> (TCon -> TCon -> Bool)
    -> (TCon -> TCon -> Bool)
    -> (TCon -> TCon -> Bool)
    -> (TCon -> TCon -> Bool)
    -> (TCon -> TCon -> TCon)
    -> (TCon -> TCon -> TCon)
    -> Ord TCon
    TCon -> TCon -> Bool
    TCon -> TCon -> Ordering
    TCon -> TCon -> TCon
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: TCon -> TCon -> Ordering
    compare :: TCon -> TCon -> Ordering
    $c< :: TCon -> TCon -> Bool
    < :: TCon -> TCon -> Bool
    $c<= :: TCon -> TCon -> Bool
    <= :: TCon -> TCon -> Bool
    $c> :: TCon -> TCon -> Bool
    > :: TCon -> TCon -> Bool
    $c>= :: TCon -> TCon -> Bool
    >= :: TCon -> TCon -> Bool
    $cmax :: TCon -> TCon -> TCon
    max :: TCon -> TCon -> TCon
    $cmin :: TCon -> TCon -> TCon
    min :: TCon -> TCon -> TCon
    Ord, (forall x. TCon -> Rep TCon x)
    -> (forall x. Rep TCon x -> TCon) -> Generic TCon
    forall x. Rep TCon x -> TCon
    forall x. TCon -> Rep TCon x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TCon -> Rep TCon x
    from :: forall x. TCon -> Rep TCon x
    $cto :: forall x. Rep TCon x -> TCon
    to :: forall x. Rep TCon x -> TCon
    Generic, TCon -> ()
    (TCon -> ()) -> NFData TCon
    forall a. (a -> ()) -> NFData a
    $crnf :: TCon -> ()
    rnf :: TCon -> ()
    NFData)

    -- | Predicate symbols.
    -- If you add additional user-visible constructors, please update 'primTys'.
    data PC     = PEqual        -- ^ @_ == _@
                | PNeq          -- ^ @_ /= _@
                | PGeq          -- ^ @_ >= _@
                | PFin          -- ^ @fin _@
                | PPrime        -- ^ @prime _@

                -- classes
                | PHas Selector -- ^ @Has sel type field@ does not appear in schemas
                | PZero         -- ^ @Zero _@
                | PLogic        -- ^ @Logic _@
                | PRing         -- ^ @Ring _@
                | PIntegral     -- ^ @Integral _@
                | PField        -- ^ @Field _@
                | PRound        -- ^ @Round _@
                | PEq           -- ^ @Eq _@
                | PCmp          -- ^ @Cmp _@
                | PSignedCmp    -- ^ @SignedCmp _@
                | PLiteral      -- ^ @Literal _ _@
                | PLiteralLessThan -- ^ @LiteralLessThan _ _@
                | PFLiteral     -- ^ @FLiteral _ _ _@

                | PValidFloat   -- ^ @ValidFloat _ _@ constraints on supported
                                -- floating point representaitons

                | PAnd          -- ^ This is useful when simplifying things in place
                | PTrue         -- ^ Ditto
                  deriving (Int -> PC -> ShowS
    [PC] -> ShowS
    PC -> String
    (Int -> PC -> ShowS)
    -> (PC -> String) -> ([PC] -> ShowS) -> Show PC
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PC -> ShowS
    showsPrec :: Int -> PC -> ShowS
    $cshow :: PC -> String
    show :: PC -> String
    $cshowList :: [PC] -> ShowS
    showList :: [PC] -> ShowS
    Show, PC -> PC -> Bool
    (PC -> PC -> Bool) -> (PC -> PC -> Bool) -> Eq PC
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PC -> PC -> Bool
    == :: PC -> PC -> Bool
    $c/= :: PC -> PC -> Bool
    /= :: PC -> PC -> Bool
    Eq, Eq PC
    Eq PC
    -> (PC -> PC -> Ordering)
    -> (PC -> PC -> Bool)
    -> (PC -> PC -> Bool)
    -> (PC -> PC -> Bool)
    -> (PC -> PC -> Bool)
    -> (PC -> PC -> PC)
    -> (PC -> PC -> PC)
    -> Ord PC
    PC -> PC -> Bool
    PC -> PC -> Ordering
    PC -> PC -> PC
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: PC -> PC -> Ordering
    compare :: PC -> PC -> Ordering
    $c< :: PC -> PC -> Bool
    < :: PC -> PC -> Bool
    $c<= :: PC -> PC -> Bool
    <= :: PC -> PC -> Bool
    $c> :: PC -> PC -> Bool
    > :: PC -> PC -> Bool
    $c>= :: PC -> PC -> Bool
    >= :: PC -> PC -> Bool
    $cmax :: PC -> PC -> PC
    max :: PC -> PC -> PC
    $cmin :: PC -> PC -> PC
    min :: PC -> PC -> PC
    Ord, (forall x. PC -> Rep PC x)
    -> (forall x. Rep PC x -> PC) -> Generic PC
    forall x. Rep PC x -> PC
    forall x. PC -> Rep PC x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PC -> Rep PC x
    from :: forall x. PC -> Rep PC x
    $cto :: forall x. Rep PC x -> PC
    to :: forall x. Rep PC x -> PC
    Generic, PC -> ()
    (PC -> ()) -> NFData PC
    forall a. (a -> ()) -> NFData a
    $crnf :: PC -> ()
    rnf :: PC -> ()
    NFData)

    -- | 1-1 constants.
    -- If you add additional user-visible constructors, please update 'primTys'.
    data TC     = TCNum Integer            -- ^ Numbers
                | TCInf                    -- ^ Inf
                | TCBit                    -- ^ Bit
                | TCInteger                -- ^ Integer
                | TCFloat                  -- ^ Float
                | TCIntMod                 -- ^ @Z _@
                | TCRational               -- ^ @Rational@
                | TCArray                  -- ^ @Array _ _@
                | TCSeq                    -- ^ @[_] _@
                | TCFun                    -- ^ @_ -> _@
                | TCTuple Int              -- ^ @(_, _, _)@
                | TCAbstract UserTC        -- ^ An abstract type
                  deriving (Int -> TC -> ShowS
    [TC] -> ShowS
    TC -> String
    (Int -> TC -> ShowS)
    -> (TC -> String) -> ([TC] -> ShowS) -> Show TC
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TC -> ShowS
    showsPrec :: Int -> TC -> ShowS
    $cshow :: TC -> String
    show :: TC -> String
    $cshowList :: [TC] -> ShowS
    showList :: [TC] -> ShowS
    Show, TC -> TC -> Bool
    (TC -> TC -> Bool) -> (TC -> TC -> Bool) -> Eq TC
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TC -> TC -> Bool
    == :: TC -> TC -> Bool
    $c/= :: TC -> TC -> Bool
    /= :: TC -> TC -> Bool
    Eq, Eq TC
    Eq TC
    -> (TC -> TC -> Ordering)
    -> (TC -> TC -> Bool)
    -> (TC -> TC -> Bool)
    -> (TC -> TC -> Bool)
    -> (TC -> TC -> Bool)
    -> (TC -> TC -> TC)
    -> (TC -> TC -> TC)
    -> Ord TC
    TC -> TC -> Bool
    TC -> TC -> Ordering
    TC -> TC -> TC
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: TC -> TC -> Ordering
    compare :: TC -> TC -> Ordering
    $c< :: TC -> TC -> Bool
    < :: TC -> TC -> Bool
    $c<= :: TC -> TC -> Bool
    <= :: TC -> TC -> Bool
    $c> :: TC -> TC -> Bool
    > :: TC -> TC -> Bool
    $c>= :: TC -> TC -> Bool
    >= :: TC -> TC -> Bool
    $cmax :: TC -> TC -> TC
    max :: TC -> TC -> TC
    $cmin :: TC -> TC -> TC
    min :: TC -> TC -> TC
    Ord, (forall x. TC -> Rep TC x)
    -> (forall x. Rep TC x -> TC) -> Generic TC
    forall x. Rep TC x -> TC
    forall x. TC -> Rep TC x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TC -> Rep TC x
    from :: forall x. TC -> Rep TC x
    $cto :: forall x. Rep TC x -> TC
    to :: forall x. Rep TC x -> TC
    Generic, TC -> ()
    (TC -> ()) -> NFData TC
    forall a. (a -> ()) -> NFData a
    $crnf :: TC -> ()
    rnf :: TC -> ()
    NFData)

    data UserTC = UserTC M.Name Kind
                  deriving (Int -> UserTC -> ShowS
    [UserTC] -> ShowS
    UserTC -> String
    (Int -> UserTC -> ShowS)
    -> (UserTC -> String) -> ([UserTC] -> ShowS) -> Show UserTC
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UserTC -> ShowS
    showsPrec :: Int -> UserTC -> ShowS
    $cshow :: UserTC -> String
    show :: UserTC -> String
    $cshowList :: [UserTC] -> ShowS
    showList :: [UserTC] -> ShowS
    Show, (forall x. UserTC -> Rep UserTC x)
    -> (forall x. Rep UserTC x -> UserTC) -> Generic UserTC
    forall x. Rep UserTC x -> UserTC
    forall x. UserTC -> Rep UserTC x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. UserTC -> Rep UserTC x
    from :: forall x. UserTC -> Rep UserTC x
    $cto :: forall x. Rep UserTC x -> UserTC
    to :: forall x. Rep UserTC x -> UserTC
    Generic, UserTC -> ()
    (UserTC -> ()) -> NFData UserTC
    forall a. (a -> ()) -> NFData a
    $crnf :: UserTC -> ()
    rnf :: UserTC -> ()
    NFData)

    instance Eq UserTC where
      UserTC Name
    x Kind
    _ == :: UserTC -> UserTC -> Bool
    == UserTC Name
    y Kind
    _ = Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    y

    instance Ord UserTC where
      compare :: UserTC -> UserTC -> Ordering
    compare (UserTC Name
    x Kind
    _) (UserTC Name
    y Kind
    _) = Name -> Name -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Name
    x Name
    y

    -- | Built-in type functions.
    -- If you add additional user-visible constructors,
    -- please update 'primTys' in "Cryptol.Prims.Types".
    data TFun

      = TCAdd                 -- ^ @ : Num -> Num -> Num @
      | TCSub                 -- ^ @ : Num -> Num -> Num @
      | TCMul                 -- ^ @ : Num -> Num -> Num @
      | TCDiv                 -- ^ @ : Num -> Num -> Num @
      | TCMod                 -- ^ @ : Num -> Num -> Num @
      | TCExp                 -- ^ @ : Num -> Num -> Num @
      | TCWidth               -- ^ @ : Num -> Num @
      | TCMin                 -- ^ @ : Num -> Num -> Num @
      | TCMax                 -- ^ @ : Num -> Num -> Num @
      | TCCeilDiv             -- ^ @ : Num -> Num -> Num @
      | TCCeilMod             -- ^ @ : Num -> Num -> Num @

      -- Computing the lengths of explicit enumerations
      | TCLenFromThenTo       -- ^ @ : Num -> Num -> Num -> Num@
        -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@

        deriving (Int -> TFun -> ShowS
    [TFun] -> ShowS
    TFun -> String
    (Int -> TFun -> ShowS)
    -> (TFun -> String) -> ([TFun] -> ShowS) -> Show TFun
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TFun -> ShowS
    showsPrec :: Int -> TFun -> ShowS
    $cshow :: TFun -> String
    show :: TFun -> String
    $cshowList :: [TFun] -> ShowS
    showList :: [TFun] -> ShowS
    Show, TFun -> TFun -> Bool
    (TFun -> TFun -> Bool) -> (TFun -> TFun -> Bool) -> Eq TFun
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TFun -> TFun -> Bool
    == :: TFun -> TFun -> Bool
    $c/= :: TFun -> TFun -> Bool
    /= :: TFun -> TFun -> Bool
    Eq, Eq TFun
    Eq TFun
    -> (TFun -> TFun -> Ordering)
    -> (TFun -> TFun -> Bool)
    -> (TFun -> TFun -> Bool)
    -> (TFun -> TFun -> Bool)
    -> (TFun -> TFun -> Bool)
    -> (TFun -> TFun -> TFun)
    -> (TFun -> TFun -> TFun)
    -> Ord TFun
    TFun -> TFun -> Bool
    TFun -> TFun -> Ordering
    TFun -> TFun -> TFun
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: TFun -> TFun -> Ordering
    compare :: TFun -> TFun -> Ordering
    $c< :: TFun -> TFun -> Bool
    < :: TFun -> TFun -> Bool
    $c<= :: TFun -> TFun -> Bool
    <= :: TFun -> TFun -> Bool
    $c> :: TFun -> TFun -> Bool
    > :: TFun -> TFun -> Bool
    $c>= :: TFun -> TFun -> Bool
    >= :: TFun -> TFun -> Bool
    $cmax :: TFun -> TFun -> TFun
    max :: TFun -> TFun -> TFun
    $cmin :: TFun -> TFun -> TFun
    min :: TFun -> TFun -> TFun
    Ord, TFun
    TFun -> TFun -> Bounded TFun
    forall a. a -> a -> Bounded a
    $cminBound :: TFun
    minBound :: TFun
    $cmaxBound :: TFun
    maxBound :: TFun
    Bounded, Int -> TFun
    TFun -> Int
    TFun -> [TFun]
    TFun -> TFun
    TFun -> TFun -> [TFun]
    TFun -> TFun -> TFun -> [TFun]
    (TFun -> TFun)
    -> (TFun -> TFun)
    -> (Int -> TFun)
    -> (TFun -> Int)
    -> (TFun -> [TFun])
    -> (TFun -> TFun -> [TFun])
    -> (TFun -> TFun -> [TFun])
    -> (TFun -> TFun -> TFun -> [TFun])
    -> Enum TFun
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: TFun -> TFun
    succ :: TFun -> TFun
    $cpred :: TFun -> TFun
    pred :: TFun -> TFun
    $ctoEnum :: Int -> TFun
    toEnum :: Int -> TFun
    $cfromEnum :: TFun -> Int
    fromEnum :: TFun -> Int
    $cenumFrom :: TFun -> [TFun]
    enumFrom :: TFun -> [TFun]
    $cenumFromThen :: TFun -> TFun -> [TFun]
    enumFromThen :: TFun -> TFun -> [TFun]
    $cenumFromTo :: TFun -> TFun -> [TFun]
    enumFromTo :: TFun -> TFun -> [TFun]
    $cenumFromThenTo :: TFun -> TFun -> TFun -> [TFun]
    enumFromThenTo :: TFun -> TFun -> TFun -> [TFun]
    Enum, (forall x. TFun -> Rep TFun x)
    -> (forall x. Rep TFun x -> TFun) -> Generic TFun
    forall x. Rep TFun x -> TFun
    forall x. TFun -> Rep TFun x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TFun -> Rep TFun x
    from :: forall x. TFun -> Rep TFun x
    $cto :: forall x. Rep TFun x -> TFun
    to :: forall x. Rep TFun x -> TFun
    Generic, TFun -> ()
    (TFun -> ()) -> NFData TFun
    forall a. (a -> ()) -> NFData a
    $crnf :: TFun -> ()
    rnf :: TFun -> ()
    NFData)

    --------------------------------------------------------------------------------
    -- Pretty printing

    instance PP Kind where
      ppPrec :: Int -> Kind -> Doc
    ppPrec Int
    p Kind
    k = case Kind
    k of
        Kind
    KType   -> Char -> Doc
    char Char
    '*'
        Kind
    KNum    -> Char -> Doc
    char Char
    '#'
        Kind
    KProp   -> String -> Doc
    text String
    "Prop"
        Kind
    l :-> Kind
    r -> Bool -> Doc -> Doc
    optParens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    1) ([Doc] -> Doc
    sep [Int -> Kind -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec Int
    1 Kind
    l, String -> Doc
    text String
    "->", Int -> Kind -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec Int
    0 Kind
    r])

    instance PP TCon where
      ppPrec :: Int -> TCon -> Doc
    ppPrec Int
    _ (TC TC
    tc)        = TC -> Doc
    forall a. PP a => a -> Doc
    pp TC
    tc
      ppPrec Int
    _ (PC PC
    tc)        = PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    tc
      ppPrec Int
    _ (TF TFun
    tc)        = TFun -> Doc
    forall a. PP a => a -> Doc
    pp TFun
    tc
      ppPrec Int
    _ (TError Kind
    _)     = Doc
    "Error"

    instance PP PC where
      ppPrec :: Int -> PC -> Doc
    ppPrec Int
    _ PC
    x =
        case PC
    x of
          PC
    PEqual     -> String -> Doc
    text String
    "(==)"
          PC
    PNeq       -> String -> Doc
    text String
    "(/=)"
          PC
    PGeq       -> String -> Doc
    text String
    "(>=)"
          PC
    PFin       -> String -> Doc
    text String
    "fin"
          PC
    PPrime     -> String -> Doc
    text String
    "prime"
          PHas Selector
    sel   -> Doc -> Doc
    parens (Selector -> Doc
    ppSelector Selector
    sel)
          PC
    PZero      -> String -> Doc
    text String
    "Zero"
          PC
    PLogic     -> String -> Doc
    text String
    "Logic"
          PC
    PRing      -> String -> Doc
    text String
    "Ring"
          PC
    PIntegral  -> String -> Doc
    text String
    "Integral"
          PC
    PField     -> String -> Doc
    text String
    "Field"
          PC
    PRound     -> String -> Doc
    text String
    "Round"
          PC
    PEq        -> String -> Doc
    text String
    "Eq"
          PC
    PCmp       -> String -> Doc
    text String
    "Cmp"
          PC
    PSignedCmp -> String -> Doc
    text String
    "SignedCmp"
          PC
    PLiteral   -> String -> Doc
    text String
    "Literal"
          PC
    PLiteralLessThan -> String -> Doc
    text String
    "LiteralLessThan"
          PC
    PFLiteral  -> String -> Doc
    text String
    "FLiteral"
          PC
    PValidFloat -> String -> Doc
    text String
    "ValidFloat"
          PC
    PTrue      -> String -> Doc
    text String
    "True"
          PC
    PAnd       -> String -> Doc
    text String
    "(&&)"

    instance PP TC where
      ppPrec :: Int -> TC -> Doc
    ppPrec Int
    _ TC
    x =
        case TC
    x of
          TCNum Integer
    n   -> Integer -> Doc
    integer Integer
    n
          TC
    TCInf     -> String -> Doc
    text String
    "inf"
          TC
    TCBit     -> String -> Doc
    text String
    "Bit"
          TC
    TCInteger -> String -> Doc
    text String
    "Integer"
          TC
    TCIntMod  -> String -> Doc
    text String
    "Z"
          TC
    TCRational -> String -> Doc
    text String
    "Rational"
          TC
    TCArray   -> String -> Doc
    text String
    "Array"
          TC
    TCFloat   -> String -> Doc
    text String
    "Float"
          TC
    TCSeq     -> String -> Doc
    text String
    "[]"
          TC
    TCFun     -> String -> Doc
    text String
    "(->)"
          TCTuple Int
    0 -> String -> Doc
    text String
    "()"
          TCTuple Int
    1 -> String -> Doc
    text String
    "(one tuple?)"
          TCTuple Int
    n -> Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    hcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Doc -> [Doc]
    forall a. Int -> a -> [a]
    replicate (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Doc
    comma
          TCAbstract UserTC
    u -> UserTC -> Doc
    forall a. PP a => a -> Doc
    pp UserTC
    u

    instance PP UserTC where
      ppPrec :: Int -> UserTC -> Doc
    ppPrec Int
    p (UserTC Name
    x Kind
    _) = Int -> Name -> Doc
    forall a. PP a => Int -> a -> Doc
    ppPrec Int
    p Name
    x

    instance PP TFun where
      ppPrec :: Int -> TFun -> Doc
    ppPrec Int
    _ TFun
    tcon =
        case TFun
    tcon of
          TFun
    TCAdd             -> String -> Doc
    text String
    "+"
          TFun
    TCSub             -> String -> Doc
    text String
    "-"
          TFun
    TCMul             -> String -> Doc
    text String
    "*"
          TFun
    TCDiv             -> String -> Doc
    text String
    "/"
          TFun
    TCMod             -> String -> Doc
    text String
    "%"
          TFun
    TCExp             -> String -> Doc
    text String
    "^^"
          TFun
    TCWidth           -> String -> Doc
    text String
    "width"
          TFun
    TCMin             -> String -> Doc
    text String
    "min"
          TFun
    TCMax             -> String -> Doc
    text String
    "max"
          TFun
    TCCeilDiv         -> String -> Doc
    text String
    "/^"
          TFun
    TCCeilMod         -> String -> Doc
    text String
    "%^"
          TFun
    TCLenFromThenTo   -> String -> Doc
    text String
    "lengthFromThenTo"