    {-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
    {-# Language FlexibleInstances, FlexibleContexts #-}
    {-# Language PatternGuards #-}
    {-# Language OverloadedStrings #-}
    module Cryptol.TypeCheck.Type
      ( module Cryptol.TypeCheck.Type
      , module Cryptol.TypeCheck.TCon
      ) where

    import GHC.Generics (Generic)
    import Control.DeepSeq

    import qualified Data.IntMap as IntMap
    import           Data.Set (Set)
    import qualified Data.Set as Set
    import           Data.List(sortBy)
    import           Data.Ord(comparing)

    import Cryptol.Parser.Selector
    import Cryptol.Parser.Fixity
    import Cryptol.Parser.Position(Range,emptyRange)
    import Cryptol.ModuleSystem.Name
    import Cryptol.Utils.Ident (Ident)
    import Cryptol.TypeCheck.TCon
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Solver.InfNat
    import Cryptol.Utils.Panic(panic)
    import Prelude

    infix  4 =#=, >==
    infixr 5 `tFun`

    -- | The types of polymorphic values.
    data Schema = Forall { Schema -> [TParam]
    sVars :: [TParam], Schema -> [Prop]
    sProps :: [Prop], Schema -> Prop
    sType :: Type }
                  deriving (Schema -> Schema -> Bool
    (Schema -> Schema -> Bool)
    -> (Schema -> Schema -> Bool) -> Eq Schema
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Schema -> Schema -> Bool
    $c/= :: Schema -> Schema -> Bool
    == :: Schema -> Schema -> Bool
    $c== :: Schema -> Schema -> Bool
    Eq, Int -> Schema -> ShowS
    [Schema] -> ShowS
    Schema -> String
    (Int -> Schema -> ShowS)
    -> (Schema -> String) -> ([Schema] -> ShowS) -> Show Schema
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Schema] -> ShowS
    $cshowList :: [Schema] -> ShowS
    show :: Schema -> String
    $cshow :: Schema -> String
    showsPrec :: Int -> Schema -> ShowS
    $cshowsPrec :: Int -> Schema -> ShowS
    Show, (forall x. Schema -> Rep Schema x)
    -> (forall x. Rep Schema x -> Schema) -> Generic Schema
    forall x. Rep Schema x -> Schema
    forall x. Schema -> Rep Schema x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Schema x -> Schema
    $cfrom :: forall x. Schema -> Rep Schema x
    Generic, Schema -> ()
    (Schema -> ()) -> NFData Schema
    forall a. (a -> ()) -> NFData a
    rnf :: Schema -> ()
    $crnf :: Schema -> ()
    NFData)

    -- | Type parameters.
    data TParam = TParam { TParam -> Int
    tpUnique :: !Int       -- ^ Parameter identifier
                         , TParam -> Kind
    tpKind   :: Kind       -- ^ Kind of parameter
                         , TParam -> TPFlavor
    tpFlav   :: TPFlavor
                            -- ^ What sort of type parameter is this
                         , TParam -> TVarInfo
    tpInfo   :: !TVarInfo
                           -- ^ A description for better messages.
                         }
                  deriving ((forall x. TParam -> Rep TParam x)
    -> (forall x. Rep TParam x -> TParam) -> Generic TParam
    forall x. Rep TParam x -> TParam
    forall x. TParam -> Rep TParam x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TParam x -> TParam
    $cfrom :: forall x. TParam -> Rep TParam x
    Generic, TParam -> ()
    (TParam -> ()) -> NFData TParam
    forall a. (a -> ()) -> NFData a
    rnf :: TParam -> ()
    $crnf :: TParam -> ()
    NFData, Int -> TParam -> ShowS
    [TParam] -> ShowS
    TParam -> String
    (Int -> TParam -> ShowS)
    -> (TParam -> String) -> ([TParam] -> ShowS) -> Show TParam
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TParam] -> ShowS
    $cshowList :: [TParam] -> ShowS
    show :: TParam -> String
    $cshow :: TParam -> String
    showsPrec :: Int -> TParam -> ShowS
    $cshowsPrec :: Int -> TParam -> ShowS
    Show)

    data TPFlavor = TPModParam Name
                  | TPOther (Maybe Name)
                  deriving ((forall x. TPFlavor -> Rep TPFlavor x)
    -> (forall x. Rep TPFlavor x -> TPFlavor) -> Generic TPFlavor
    forall x. Rep TPFlavor x -> TPFlavor
    forall x. TPFlavor -> Rep TPFlavor x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TPFlavor x -> TPFlavor
    $cfrom :: forall x. TPFlavor -> Rep TPFlavor x
    Generic, TPFlavor -> ()
    (TPFlavor -> ()) -> NFData TPFlavor
    forall a. (a -> ()) -> NFData a
    rnf :: TPFlavor -> ()
    $crnf :: TPFlavor -> ()
    NFData, Int -> TPFlavor -> ShowS
    [TPFlavor] -> ShowS
    TPFlavor -> String
    (Int -> TPFlavor -> ShowS)
    -> (TPFlavor -> String) -> ([TPFlavor] -> ShowS) -> Show TPFlavor
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TPFlavor] -> ShowS
    $cshowList :: [TPFlavor] -> ShowS
    show :: TPFlavor -> String
    $cshow :: TPFlavor -> String
    showsPrec :: Int -> TPFlavor -> ShowS
    $cshowsPrec :: Int -> TPFlavor -> ShowS
    Show)

    tMono :: Type -> Schema
    tMono :: Prop -> Schema
    tMono = [TParam] -> [Prop] -> Prop -> Schema
    Forall [] []

    isMono :: Schema -> Maybe Type
    isMono :: Schema -> Maybe Prop
    isMono s :: Schema
    s =
      case Schema
    s of
        Forall [] [] t :: Prop
    t -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t
        _              -> Maybe Prop
    forall a. Maybe a
    Nothing

    schemaParam :: Name -> TPFlavor
    schemaParam :: Name -> TPFlavor
    schemaParam x :: Name
    x = Maybe Name -> TPFlavor
    TPOther (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x)

    tySynParam :: Name -> TPFlavor
    tySynParam :: Name -> TPFlavor
    tySynParam x :: Name
    x = Maybe Name -> TPFlavor
    TPOther (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x)

    propSynParam :: Name -> TPFlavor
    propSynParam :: Name -> TPFlavor
    propSynParam x :: Name
    x = Maybe Name -> TPFlavor
    TPOther (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x)

    newtypeParam :: Name -> TPFlavor
    newtypeParam :: Name -> TPFlavor
    newtypeParam x :: Name
    x = Maybe Name -> TPFlavor
    TPOther (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x)

    modTyParam :: Name -> TPFlavor
    modTyParam :: Name -> TPFlavor
    modTyParam = Name -> TPFlavor
    TPModParam

    tpfName :: TPFlavor -> Maybe Name
    tpfName :: TPFlavor -> Maybe Name
    tpfName f :: TPFlavor
    f =
      case TPFlavor
    f of
        TPModParam x :: Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TPOther x :: Maybe Name
    x -> Maybe Name
    x

    tpName :: TParam -> Maybe Name
    tpName :: TParam -> Maybe Name
    tpName = TPFlavor -> Maybe Name
    tpfName (TPFlavor -> Maybe Name)
    -> (TParam -> TPFlavor) -> TParam -> Maybe Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TPFlavor
    tpFlav

    -- | The internal representation of types.
    -- These are assumed to be kind correct.
    data Type   = TCon !TCon ![Type]
                  -- ^ Type constant with args

                | TVar TVar
                  -- ^ Type variable (free or bound)

                | TUser !Name ![Type] !Type
                  {- ^ This is just a type annotation, for a type that
                  was written as a type synonym.  It is useful so that we
                  can use it to report nicer errors.
                  Example: `TUser T ts t` is really just the type `t` that
                  was written as `T ts` by the user. -}

                | TRec ![(Ident,Type)]
                  -- ^ Record type

                  deriving (Int -> Prop -> ShowS
    [Prop] -> ShowS
    Prop -> String
    (Int -> Prop -> ShowS)
    -> (Prop -> String) -> ([Prop] -> ShowS) -> Show Prop
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Prop] -> ShowS
    $cshowList :: [Prop] -> ShowS
    show :: Prop -> String
    $cshow :: Prop -> String
    showsPrec :: Int -> Prop -> ShowS
    $cshowsPrec :: Int -> Prop -> ShowS
    Show, (forall x. Prop -> Rep Prop x)
    -> (forall x. Rep Prop x -> Prop) -> Generic Prop
    forall x. Rep Prop x -> Prop
    forall x. Prop -> Rep Prop x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Prop x -> Prop
    $cfrom :: forall x. Prop -> Rep Prop x
    Generic, Prop -> ()
    (Prop -> ()) -> NFData Prop
    forall a. (a -> ()) -> NFData a
    rnf :: Prop -> ()
    $crnf :: Prop -> ()
    NFData)

    -- | Type variables.
    data TVar   = TVFree !Int Kind (Set TParam) TVarInfo
                  -- ^ Unique, kind, ids of bound type variables that are in scope
                  -- The last field gives us some infor for nicer warnings/errors.

                | TVBound {-# UNPACK #-} !TParam
                  deriving (Int -> TVar -> ShowS
    [TVar] -> ShowS
    TVar -> String
    (Int -> TVar -> ShowS)
    -> (TVar -> String) -> ([TVar] -> ShowS) -> Show TVar
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TVar] -> ShowS
    $cshowList :: [TVar] -> ShowS
    show :: TVar -> String
    $cshow :: TVar -> String
    showsPrec :: Int -> TVar -> ShowS
    $cshowsPrec :: Int -> TVar -> ShowS
    Show, (forall x. TVar -> Rep TVar x)
    -> (forall x. Rep TVar x -> TVar) -> Generic TVar
    forall x. Rep TVar x -> TVar
    forall x. TVar -> Rep TVar x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TVar x -> TVar
    $cfrom :: forall x. TVar -> Rep TVar x
    Generic, TVar -> ()
    (TVar -> ()) -> NFData TVar
    forall a. (a -> ()) -> NFData a
    rnf :: TVar -> ()
    $crnf :: TVar -> ()
    NFData)

    tvInfo :: TVar -> TVarInfo
    tvInfo :: TVar -> TVarInfo
    tvInfo tv :: TVar
    tv =
      case TVar
    tv of
        TVFree _ _ _ d :: TVarInfo
    d -> TVarInfo
    d
        TVBound tp :: TParam
    tp     -> TParam -> TVarInfo
    tpInfo TParam
    tp

    data TVarInfo = TVarInfo { TVarInfo -> Range
    tvarSource :: Range -- ^ Source code that gave rise
                             , TVarInfo -> TVarSource
    tvarDesc   :: TVarSource -- ^ Description
                             }
                  deriving (Int -> TVarInfo -> ShowS
    [TVarInfo] -> ShowS
    TVarInfo -> String
    (Int -> TVarInfo -> ShowS)
    -> (TVarInfo -> String) -> ([TVarInfo] -> ShowS) -> Show TVarInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TVarInfo] -> ShowS
    $cshowList :: [TVarInfo] -> ShowS
    show :: TVarInfo -> String
    $cshow :: TVarInfo -> String
    showsPrec :: Int -> TVarInfo -> ShowS
    $cshowsPrec :: Int -> TVarInfo -> ShowS
    Show, (forall x. TVarInfo -> Rep TVarInfo x)
    -> (forall x. Rep TVarInfo x -> TVarInfo) -> Generic TVarInfo
    forall x. Rep TVarInfo x -> TVarInfo
    forall x. TVarInfo -> Rep TVarInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TVarInfo x -> TVarInfo
    $cfrom :: forall x. TVarInfo -> Rep TVarInfo x
    Generic, TVarInfo -> ()
    (TVarInfo -> ()) -> NFData TVarInfo
    forall a. (a -> ()) -> NFData a
    rnf :: TVarInfo -> ()
    $crnf :: TVarInfo -> ()
    NFData)

    data TVarSource = TVFromModParam Name     -- ^ Name of module parameter
                    | TVFromSignature Name    -- ^ A variable in a signature
                    | TypeWildCard
                    | TypeOfRecordField Ident
                    | TypeOfTupleField Int
                    | TypeOfSeqElement
                    | LenOfSeq
                    | TypeParamInstNamed {-Fun-}Name {-Param-}Ident
                    | TypeParamInstPos   {-Fun-}Name {-Pos (from 1)-}Int
                    | DefinitionOf Name
                    | LenOfCompGen
                    | TypeOfArg (Maybe Int)
                    | TypeOfRes
                    | TypeErrorPlaceHolder
                      deriving (Int -> TVarSource -> ShowS
    [TVarSource] -> ShowS
    TVarSource -> String
    (Int -> TVarSource -> ShowS)
    -> (TVarSource -> String)
    -> ([TVarSource] -> ShowS)
    -> Show TVarSource
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TVarSource] -> ShowS
    $cshowList :: [TVarSource] -> ShowS
    show :: TVarSource -> String
    $cshow :: TVarSource -> String
    showsPrec :: Int -> TVarSource -> ShowS
    $cshowsPrec :: Int -> TVarSource -> ShowS
    Show, (forall x. TVarSource -> Rep TVarSource x)
    -> (forall x. Rep TVarSource x -> TVarSource) -> Generic TVarSource
    forall x. Rep TVarSource x -> TVarSource
    forall x. TVarSource -> Rep TVarSource x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TVarSource x -> TVarSource
    $cfrom :: forall x. TVarSource -> Rep TVarSource x
    Generic, TVarSource -> ()
    (TVarSource -> ()) -> NFData TVarSource
    forall a. (a -> ()) -> NFData a
    rnf :: TVarSource -> ()
    $crnf :: TVarSource -> ()
    NFData)

    -- | Get the names of something that is related to the tvar.
    tvSourceName :: TVarSource -> Maybe Name
    tvSourceName :: TVarSource -> Maybe Name
    tvSourceName tvs :: TVarSource
    tvs =
      case TVarSource
    tvs of
        TVFromModParam x :: Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TVFromSignature x :: Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TypeParamInstNamed x :: Name
    x _ -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TypeParamInstPos x :: Name
    x _ -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        DefinitionOf x :: Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        _ -> Maybe Name
    forall a. Maybe a
    Nothing

    -- | The type is supposed to be of kind `KProp`
    type Prop   = Type

    -- | Type synonym.
    data TySyn  = TySyn { TySyn -> Name
    tsName        :: Name       -- ^ Name
                        , TySyn -> [TParam]
    tsParams      :: [TParam]   -- ^ Parameters
                        , TySyn -> [Prop]
    tsConstraints :: [Prop]     -- ^ Ensure body is OK
                        , TySyn -> Prop
    tsDef         :: Type       -- ^ Definition
                        , TySyn -> Maybe String
    tsDoc         :: !(Maybe String) -- ^ Documentation
                        }
                  deriving (Int -> TySyn -> ShowS
    [TySyn] -> ShowS
    TySyn -> String
    (Int -> TySyn -> ShowS)
    -> (TySyn -> String) -> ([TySyn] -> ShowS) -> Show TySyn
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TySyn] -> ShowS
    $cshowList :: [TySyn] -> ShowS
    show :: TySyn -> String
    $cshow :: TySyn -> String
    showsPrec :: Int -> TySyn -> ShowS
    $cshowsPrec :: Int -> TySyn -> ShowS
    Show, (forall x. TySyn -> Rep TySyn x)
    -> (forall x. Rep TySyn x -> TySyn) -> Generic TySyn
    forall x. Rep TySyn x -> TySyn
    forall x. TySyn -> Rep TySyn x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TySyn x -> TySyn
    $cfrom :: forall x. TySyn -> Rep TySyn x
    Generic, TySyn -> ()
    (TySyn -> ()) -> NFData TySyn
    forall a. (a -> ()) -> NFData a
    rnf :: TySyn -> ()
    $crnf :: TySyn -> ()
    NFData)

    -- | Named records
    data Newtype  = Newtype { Newtype -> Name
    ntName   :: Name
                            , Newtype -> [TParam]
    ntParams :: [TParam]
                            , Newtype -> [Prop]
    ntConstraints :: [Prop]
                            , Newtype -> [(Ident, Prop)]
    ntFields :: [(Ident,Type)]
                            , Newtype -> Maybe String
    ntDoc :: Maybe String
                            } deriving (Int -> Newtype -> ShowS
    [Newtype] -> ShowS
    Newtype -> String
    (Int -> Newtype -> ShowS)
    -> (Newtype -> String) -> ([Newtype] -> ShowS) -> Show Newtype
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Newtype] -> ShowS
    $cshowList :: [Newtype] -> ShowS
    show :: Newtype -> String
    $cshow :: Newtype -> String
    showsPrec :: Int -> Newtype -> ShowS
    $cshowsPrec :: Int -> Newtype -> ShowS
    Show, (forall x. Newtype -> Rep Newtype x)
    -> (forall x. Rep Newtype x -> Newtype) -> Generic Newtype
    forall x. Rep Newtype x -> Newtype
    forall x. Newtype -> Rep Newtype x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Newtype x -> Newtype
    $cfrom :: forall x. Newtype -> Rep Newtype x
    Generic, Newtype -> ()
    (Newtype -> ()) -> NFData Newtype
    forall a. (a -> ()) -> NFData a
    rnf :: Newtype -> ()
    $crnf :: Newtype -> ()
    NFData)

    -- | Information about an abstract type.
    data AbstractType = AbstractType
      { AbstractType -> Name
    atName    :: Name
      , AbstractType -> Kind
    atKind    :: Kind
      , AbstractType -> ([TParam], [Prop])
    atCtrs    :: ([TParam], [Prop])
      , AbstractType -> Maybe Fixity
    atFixitiy :: Maybe Fixity
      , AbstractType -> Maybe String
    atDoc     :: Maybe String
      } deriving (Int -> AbstractType -> ShowS
    [AbstractType] -> ShowS
    AbstractType -> String
    (Int -> AbstractType -> ShowS)
    -> (AbstractType -> String)
    -> ([AbstractType] -> ShowS)
    -> Show AbstractType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [AbstractType] -> ShowS
    $cshowList :: [AbstractType] -> ShowS
    show :: AbstractType -> String
    $cshow :: AbstractType -> String
    showsPrec :: Int -> AbstractType -> ShowS
    $cshowsPrec :: Int -> AbstractType -> ShowS
    Show, (forall x. AbstractType -> Rep AbstractType x)
    -> (forall x. Rep AbstractType x -> AbstractType)
    -> Generic AbstractType
    forall x. Rep AbstractType x -> AbstractType
    forall x. AbstractType -> Rep AbstractType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep AbstractType x -> AbstractType
    $cfrom :: forall x. AbstractType -> Rep AbstractType x
    Generic, AbstractType -> ()
    (AbstractType -> ()) -> NFData AbstractType
    forall a. (a -> ()) -> NFData a
    rnf :: AbstractType -> ()
    $crnf :: AbstractType -> ()
    NFData)

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

    instance HasKind TVar where
      kindOf :: TVar -> Kind
    kindOf (TVFree  _ k :: Kind
    k _ _) = Kind
    k
      kindOf (TVBound tp :: TParam
    tp) = TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TParam
    tp

    instance HasKind Type where
      kindOf :: Prop -> Kind
    kindOf ty :: Prop
    ty =
        case Prop
    ty of
          TVar a :: TVar
    a      -> TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TVar
    a
          TCon c :: TCon
    c ts :: [Prop]
    ts   -> Kind -> [Prop] -> Kind
    forall a. Kind -> [a] -> Kind
    quickApply (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    c) [Prop]
    ts
          TUser _ _ t :: Prop
    t -> Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Prop
    t
          TRec {}     -> Kind
    KType

    instance HasKind TySyn where
      kindOf :: TySyn -> Kind
    kindOf ts :: TySyn
    ts = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Kind -> Kind -> Kind
    (:->) (Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf (TySyn -> Prop
    tsDef TySyn
    ts)) ((TParam -> Kind) -> [TParam] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf (TySyn -> [TParam]
    tsParams TySyn
    ts))

    instance HasKind Newtype where
      kindOf :: Newtype -> Kind
    kindOf nt :: Newtype
    nt = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Kind -> Kind -> Kind
    (:->) Kind
    KType ((TParam -> Kind) -> [TParam] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf (Newtype -> [TParam]
    ntParams Newtype
    nt))

    instance HasKind TParam where
      kindOf :: TParam -> Kind
    kindOf p :: TParam
    p = TParam -> Kind
    tpKind TParam
    p

    quickApply :: Kind -> [a] -> Kind
    quickApply :: Kind -> [a] -> Kind
    quickApply k :: Kind
    k []               = Kind
    k
    quickApply (_ :-> k :: Kind
    k) (_ : ts :: [a]
    ts) = Kind -> [a] -> Kind
    forall a. Kind -> [a] -> Kind
    quickApply Kind
    k [a]
    ts
    quickApply k :: Kind
    k _                = String -> [String] -> Kind
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.TypeCheck.AST.quickApply"
                                      [ "Applying a non-function kind:", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k ]

    kindResult :: Kind -> Kind
    kindResult :: Kind -> Kind
    kindResult (_ :-> k :: Kind
    k) = Kind -> Kind
    kindResult Kind
    k
    kindResult k :: Kind
    k         = Kind
    k

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

    -- Syntactic equality, ignoring type synonyms and record order
    instance Eq Type where
      TUser _ _ x :: Prop
    x == :: Prop -> Prop -> Bool
    == y :: Prop
    y        = Prop
    x Prop -> Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    == Prop
    y
      x :: Prop
    x == TUser _ _ y :: Prop
    y        = Prop
    y Prop -> Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    == Prop
    x

      TCon x :: TCon
    x xs :: [Prop]
    xs == TCon y :: TCon
    y ys :: [Prop]
    ys  = TCon
    x TCon -> TCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TCon
    y Bool -> Bool -> Bool
    && [Prop]
    xs [Prop] -> [Prop] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Prop]
    ys
      TVar x :: TVar
    x    == TVar y :: TVar
    y     = TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    y

      TRec xs :: [(Ident, Prop)]
    xs   == TRec ys :: [(Ident, Prop)]
    ys    = [(Ident, Prop)] -> [(Ident, Prop)]
    forall b. [(Ident, b)] -> [(Ident, b)]
    norm [(Ident, Prop)]
    xs [(Ident, Prop)] -> [(Ident, Prop)] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [(Ident, Prop)] -> [(Ident, Prop)]
    forall b. [(Ident, b)] -> [(Ident, b)]
    norm [(Ident, Prop)]
    ys
        where norm :: [(Ident, b)] -> [(Ident, b)]
    norm = ((Ident, b) -> (Ident, b) -> Ordering)
    -> [(Ident, b)] -> [(Ident, b)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, b) -> Ident) -> (Ident, b) -> (Ident, b) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, b) -> Ident
    forall a b. (a, b) -> a
    fst)

      _         == _          = Bool
    False

    instance Ord Type where
      compare :: Prop -> Prop -> Ordering
    compare x0 :: Prop
    x0 y0 :: Prop
    y0 =
        case (Prop
    x0,Prop
    y0) of
          (TUser _ _ t :: Prop
    t, _)        -> Prop -> Prop -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Prop
    t Prop
    y0
          (_, TUser _ _ t :: Prop
    t)        -> Prop -> Prop -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Prop
    x0 Prop
    t

          (TVar x :: TVar
    x, TVar y :: TVar
    y)        -> TVar -> TVar -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare TVar
    x TVar
    y
          (TVar {}, _)            -> Ordering
    LT
          (_, TVar {})            -> Ordering
    GT

          (TCon x :: TCon
    x xs :: [Prop]
    xs, TCon y :: TCon
    y ys :: [Prop]
    ys)  -> (TCon, [Prop]) -> (TCon, [Prop]) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (TCon
    x,[Prop]
    xs) (TCon
    y,[Prop]
    ys)
          (TCon {}, _)            -> Ordering
    LT
          (_,TCon {})             -> Ordering
    GT

          (TRec xs :: [(Ident, Prop)]
    xs, TRec ys :: [(Ident, Prop)]
    ys)      -> [(Ident, Prop)] -> [(Ident, Prop)] -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ([(Ident, Prop)] -> [(Ident, Prop)]
    forall b. [(Ident, b)] -> [(Ident, b)]
    norm [(Ident, Prop)]
    xs) ([(Ident, Prop)] -> [(Ident, Prop)]
    forall b. [(Ident, b)] -> [(Ident, b)]
    norm [(Ident, Prop)]
    ys)
            where norm :: [(Ident, b)] -> [(Ident, b)]
    norm = ((Ident, b) -> (Ident, b) -> Ordering)
    -> [(Ident, b)] -> [(Ident, b)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, b) -> Ident) -> (Ident, b) -> (Ident, b) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, b) -> Ident
    forall a b. (a, b) -> a
    fst)

    instance Eq TParam where
      x :: TParam
    x == :: TParam -> TParam -> Bool
    == y :: TParam
    y = TParam -> Int
    tpUnique TParam
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam -> Int
    tpUnique TParam
    y

    instance Ord TParam where
      compare :: TParam -> TParam -> Ordering
    compare x :: TParam
    x y :: TParam
    y = Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (TParam -> Int
    tpUnique TParam
    x) (TParam -> Int
    tpUnique TParam
    y)

    tpVar :: TParam -> TVar
    tpVar :: TParam -> TVar
    tpVar p :: TParam
    p = TParam -> TVar
    TVBound TParam
    p

    -- | The type is "simple" (i.e., it contains no type functions).
    type SType  = Type

    newtypeConType :: Newtype -> Schema
    newtypeConType :: Newtype -> Schema
    newtypeConType nt :: Newtype
    nt =
      [TParam] -> [Prop] -> Prop -> Schema
    Forall [TParam]
    as (Newtype -> [Prop]
    ntConstraints Newtype
    nt)
        (Prop -> Schema) -> Prop -> Schema
    forall a b. (a -> b) -> a -> b
    $ [(Ident, Prop)] -> Prop
    TRec (Newtype -> [(Ident, Prop)]
    ntFields Newtype
    nt) Prop -> Prop -> Prop
    `tFun` TCon -> [Prop] -> Prop
    TCon (Newtype -> TCon
    newtypeTyCon Newtype
    nt) ((TParam -> Prop) -> [TParam] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar -> Prop
    TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TVar
    tpVar) [TParam]
    as)
      where
      as :: [TParam]
    as = Newtype -> [TParam]
    ntParams Newtype
    nt

    abstractTypeTC :: AbstractType -> TCon
    abstractTypeTC :: AbstractType -> TCon
    abstractTypeTC at :: AbstractType
    at =
      case Name -> Maybe TCon
    builtInType (AbstractType -> Name
    atName AbstractType
    at) of
        Just tcon :: TCon
    tcon -> TCon
    tcon
        _         -> TC -> TCon
    TC (TC -> TCon) -> TC -> TCon
    forall a b. (a -> b) -> a -> b
    $ UserTC -> TC
    TCAbstract (UserTC -> TC) -> UserTC -> TC
    forall a b. (a -> b) -> a -> b
    $ Name -> Kind -> UserTC
    UserTC (AbstractType -> Name
    atName AbstractType
    at) (AbstractType -> Kind
    atKind AbstractType
    at)

    instance Eq TVar where
      TVBound x :: TParam
    x       == :: TVar -> TVar -> Bool
    == TVBound y :: TParam
    y       = TParam
    x TParam -> TParam -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam
    y
      TVFree  x :: Int
    x _ _ _ == TVFree  y :: Int
    y _ _ _ = Int
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    y
      _             == _              = Bool
    False

    instance Ord TVar where
      compare :: TVar -> TVar -> Ordering
    compare (TVFree x :: Int
    x _ _ _) (TVFree y :: Int
    y _ _ _) = Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Int
    x Int
    y
      compare (TVFree _ _ _ _) _                = Ordering
    LT
      compare _            (TVFree _ _ _ _)     = Ordering
    GT

      compare (TVBound x :: TParam
    x) (TVBound y :: TParam
    y) = TParam -> TParam -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare TParam
    x TParam
    y

    --------------------------------------------------------------------------------
    -- Queries

    isFreeTV :: TVar -> Bool
    isFreeTV :: TVar -> Bool
    isFreeTV (TVFree {}) = Bool
    True
    isFreeTV _           = Bool
    False

    isBoundTV :: TVar -> Bool
    isBoundTV :: TVar -> Bool
    isBoundTV (TVBound {})  = Bool
    True
    isBoundTV _             = Bool
    False

    tIsError :: Type -> Maybe TCErrorMessage
    tIsError :: Prop -> Maybe TCErrorMessage
    tIsError ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (TError _ x :: TCErrorMessage
    x) _ -> TCErrorMessage -> Maybe TCErrorMessage
    forall a. a -> Maybe a
    Just TCErrorMessage
    x
                    _                   -> Maybe TCErrorMessage
    forall a. Maybe a
    Nothing

    tIsNat' :: Type -> Maybe Nat'
    tIsNat' :: Prop -> Maybe Nat'
    tIsNat' ty :: Prop
    ty =
      case Prop -> Prop
    tNoUser Prop
    ty of
        TCon (TC (TCNum x :: Integer
    x)) [] -> Nat' -> Maybe Nat'
    forall a. a -> Maybe a
    Just (Integer -> Nat'
    Nat Integer
    x)
        TCon (TC TCInf)     [] -> Nat' -> Maybe Nat'
    forall a. a -> Maybe a
    Just Nat'
    Inf
        _                      -> Maybe Nat'
    forall a. Maybe a
    Nothing

    tIsNum :: Type -> Maybe Integer
    tIsNum :: Prop -> Maybe Integer
    tIsNum ty :: Prop
    ty = do Nat x :: Integer
    x <- Prop -> Maybe Nat'
    tIsNat' Prop
    ty
                   Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    x

    tIsInf :: Type -> Bool
    tIsInf :: Prop -> Bool
    tIsInf ty :: Prop
    ty = Prop -> Maybe Nat'
    tIsNat' Prop
    ty Maybe Nat' -> Maybe Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat' -> Maybe Nat'
    forall a. a -> Maybe a
    Just Nat'
    Inf

    tIsVar :: Type -> Maybe TVar
    tIsVar :: Prop -> Maybe TVar
    tIsVar ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TVar x :: TVar
    x -> TVar -> Maybe TVar
    forall a. a -> Maybe a
    Just TVar
    x
                  _      -> Maybe TVar
    forall a. Maybe a
    Nothing

    tIsFun :: Type -> Maybe (Type, Type)
    tIsFun :: Prop -> Maybe (Prop, Prop)
    tIsFun ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TCon (TC TCFun) [a :: Prop
    a, b :: Prop
    b] -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    a, Prop
    b)
                  _                      -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

    tIsSeq :: Type -> Maybe (Type, Type)
    tIsSeq :: Prop -> Maybe (Prop, Prop)
    tIsSeq ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TCon (TC TCSeq) [n :: Prop
    n, a :: Prop
    a] -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    n, Prop
    a)
                  _                      -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

    tIsBit :: Type -> Bool
    tIsBit :: Prop -> Bool
    tIsBit ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TCon (TC TCBit) [] -> Bool
    True
                  _                  -> Bool
    False

    tIsInteger :: Type -> Bool
    tIsInteger :: Prop -> Bool
    tIsInteger ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                      TCon (TC TCInteger) [] -> Bool
    True
                      _                      -> Bool
    False

    tIsIntMod :: Type -> Maybe Type
    tIsIntMod :: Prop -> Maybe Prop
    tIsIntMod ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                     TCon (TC TCIntMod) [n :: Prop
    n] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    n
                     _                      -> Maybe Prop
    forall a. Maybe a
    Nothing

    tIsTuple :: Type -> Maybe [Type]
    tIsTuple :: Prop -> Maybe [Prop]
    tIsTuple ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (TC (TCTuple _)) ts :: [Prop]
    ts -> [Prop] -> Maybe [Prop]
    forall a. a -> Maybe a
    Just [Prop]
    ts
                    _                        -> Maybe [Prop]
    forall a. Maybe a
    Nothing

    tIsRec :: Type -> Maybe [(Ident, Type)]
    tIsRec :: Prop -> Maybe [(Ident, Prop)]
    tIsRec ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TRec fs :: [(Ident, Prop)]
    fs -> [(Ident, Prop)] -> Maybe [(Ident, Prop)]
    forall a. a -> Maybe a
    Just [(Ident, Prop)]
    fs
                  _       -> Maybe [(Ident, Prop)]
    forall a. Maybe a
    Nothing

    tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
    tIsBinFun :: TFun -> Prop -> Maybe (Prop, Prop)
    tIsBinFun f :: TFun
    f ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                       TCon (TF g :: TFun
    g) [a :: Prop
    a,b :: Prop
    b] | TFun
    f TFun -> TFun -> Bool
    forall a. Eq a => a -> a -> Bool
    == TFun
    g -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    a,Prop
    b)
                       _                          -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

    -- | Split up repeated occurances of the given binary type-level function.
    tSplitFun :: TFun -> Type -> [Type]
    tSplitFun :: TFun -> Prop -> [Prop]
    tSplitFun f :: TFun
    f t0 :: Prop
    t0 = Prop -> [Prop] -> [Prop]
    go Prop
    t0 []
      where go :: Prop -> [Prop] -> [Prop]
    go ty :: Prop
    ty xs :: [Prop]
    xs = case TFun -> Prop -> Maybe (Prop, Prop)
    tIsBinFun TFun
    f Prop
    ty of
                         Just (a :: Prop
    a,b :: Prop
    b) -> Prop -> [Prop] -> [Prop]
    go Prop
    a (Prop -> [Prop] -> [Prop]
    go Prop
    b [Prop]
    xs)
                         Nothing    -> Prop
    ty Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : [Prop]
    xs

    pIsFin :: Prop -> Maybe Type
    pIsFin :: Prop -> Maybe Prop
    pIsFin ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TCon (PC PFin) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                  _                   -> Maybe Prop
    forall a. Maybe a
    Nothing

    pIsGeq :: Prop -> Maybe (Type,Type)
    pIsGeq :: Prop -> Maybe (Prop, Prop)
    pIsGeq ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TCon (PC PGeq) [t1 :: Prop
    t1,t2 :: Prop
    t2] -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    t1,Prop
    t2)
                  _                      -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

    pIsEq :: Prop -> Maybe (Type,Type)
    pIsEq :: Prop -> Maybe (Prop, Prop)
    pIsEq ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                 TCon (PC PEqual) [t1 :: Prop
    t1,t2 :: Prop
    t2] -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    t1,Prop
    t2)
                 _                        -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

    pIsZero :: Prop -> Maybe Type
    pIsZero :: Prop -> Maybe Prop
    pIsZero ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                   TCon (PC PZero) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                   _                    -> Maybe Prop
    forall a. Maybe a
    Nothing

    pIsLogic :: Prop -> Maybe Type
    pIsLogic :: Prop -> Maybe Prop
    pIsLogic ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (PC PLogic) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                    _                     -> Maybe Prop
    forall a. Maybe a
    Nothing

    pIsArith :: Prop -> Maybe Type
    pIsArith :: Prop -> Maybe Prop
    pIsArith ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (PC PArith) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                    _                     -> Maybe Prop
    forall a. Maybe a
    Nothing

    pIsCmp :: Prop -> Maybe Type
    pIsCmp :: Prop -> Maybe Prop
    pIsCmp ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TCon (PC PCmp) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                  _                   -> Maybe Prop
    forall a. Maybe a
    Nothing

    pIsSignedCmp :: Prop -> Maybe Type
    pIsSignedCmp :: Prop -> Maybe Prop
    pIsSignedCmp ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                        TCon (PC PSignedCmp) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                        _                         -> Maybe Prop
    forall a. Maybe a
    Nothing

    pIsLiteral :: Prop -> Maybe (Type, Type)
    pIsLiteral :: Prop -> Maybe (Prop, Prop)
    pIsLiteral ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                      TCon (PC PLiteral) [t1 :: Prop
    t1, t2 :: Prop
    t2] -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    t1, Prop
    t2)
                      _                           -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

    pIsTrue :: Prop -> Bool
    pIsTrue :: Prop -> Bool
    pIsTrue ty :: Prop
    ty  = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (PC PTrue) _ -> Bool
    True
                    _                 -> Bool
    False

    pIsWidth :: Prop -> Maybe Type
    pIsWidth :: Prop -> Maybe Prop
    pIsWidth ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (TF TCWidth) [t1 :: Prop
    t1] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t1
                    _                      -> Maybe Prop
    forall a. Maybe a
    Nothing

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

    tNum     :: Integral a => a -> Type
    tNum :: a -> Prop
    tNum n :: a
    n    = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC (Integer -> TC
    TCNum (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n))) []

    tZero     :: Type
    tZero :: Prop
    tZero     = Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (0 :: Int)

    tOne     :: Type
    tOne :: Prop
    tOne      = Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (1 :: Int)

    tTwo     :: Type
    tTwo :: Prop
    tTwo      = Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (2 :: Int)

    tInf     :: Type
    tInf :: Prop
    tInf      = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCInf) []

    tNat'    :: Nat' -> Type
    tNat' :: Nat' -> Prop
    tNat' n' :: Nat'
    n'  = case Nat'
    n' of
                  Inf   -> Prop
    tInf
                  Nat n :: Integer
    n -> Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    n

    tAbstract :: UserTC -> [Type] -> Type
    tAbstract :: UserTC -> [Prop] -> Prop
    tAbstract u :: UserTC
    u ts :: [Prop]
    ts = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC (UserTC -> TC
    TCAbstract UserTC
    u)) [Prop]
    ts

    tBit     :: Type
    tBit :: Prop
    tBit      = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCBit) []

    tInteger :: Type
    tInteger :: Prop
    tInteger  = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCInteger) []

    tIntMod :: Type -> Type
    tIntMod :: Prop -> Prop
    tIntMod n :: Prop
    n = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCIntMod) [Prop
    n]

    tWord    :: Type -> Type
    tWord :: Prop -> Prop
    tWord a :: Prop
    a   = Prop -> Prop -> Prop
    tSeq Prop
    a Prop
    tBit

    tSeq     :: Type -> Type -> Type
    tSeq :: Prop -> Prop -> Prop
    tSeq a :: Prop
    a b :: Prop
    b  = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCSeq) [Prop
    a,Prop
    b]

    tChar :: Type
    tChar :: Prop
    tChar = Prop -> Prop
    tWord (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (8 :: Int))

    tString :: Int -> Type
    tString :: Int -> Prop
    tString len :: Int
    len = Prop -> Prop -> Prop
    tSeq (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum Int
    len) Prop
    tChar

    tRec     :: [(Ident,Type)] -> Type
    tRec :: [(Ident, Prop)] -> Prop
    tRec      = [(Ident, Prop)] -> Prop
    TRec

    tTuple   :: [Type] -> Type
    tTuple :: [Prop] -> Prop
    tTuple ts :: [Prop]
    ts = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC (Int -> TC
    TCTuple ([Prop] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Prop]
    ts))) [Prop]
    ts

    newtypeTyCon :: Newtype -> TCon
    newtypeTyCon :: Newtype -> TCon
    newtypeTyCon nt :: Newtype
    nt = TC -> TCon
    TC (TC -> TCon) -> TC -> TCon
    forall a b. (a -> b) -> a -> b
    $ UserTC -> TC
    TCNewtype (UserTC -> TC) -> UserTC -> TC
    forall a b. (a -> b) -> a -> b
    $ Name -> Kind -> UserTC
    UserTC (Newtype -> Name
    ntName Newtype
    nt) (Newtype -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Newtype
    nt)

    -- | Make a function type.
    tFun     :: Type -> Type -> Type
    tFun :: Prop -> Prop -> Prop
    tFun a :: Prop
    a b :: Prop
    b  = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCFun) [Prop
    a,Prop
    b]

    -- | Eliminate outermost type synonyms.
    tNoUser  :: Type -> Type
    tNoUser :: Prop -> Prop
    tNoUser t :: Prop
    t = case Prop
    t of
                  TUser _ _ a :: Prop
    a -> Prop -> Prop
    tNoUser Prop
    a
                  _           -> Prop
    t

    --------------------------------------------------------------------------------
    -- Construction of type functions

    -- | Make a malformed numeric type.
    tBadNumber :: TCErrorMessage -> Type
    tBadNumber :: TCErrorMessage -> Prop
    tBadNumber = Kind -> TCErrorMessage -> Prop
    tError Kind
    KNum

    -- | Make an error value of the given type.
    tError :: Kind -> TCErrorMessage -> Type
    tError :: Kind -> TCErrorMessage -> Prop
    tError k :: Kind
    k msg :: TCErrorMessage
    msg = TCon -> [Prop] -> Prop
    TCon (Kind -> TCErrorMessage -> TCon
    TError Kind
    k TCErrorMessage
    msg) []

    tf1 :: TFun -> Type -> Type
    tf1 :: TFun -> Prop -> Prop
    tf1 f :: TFun
    f x :: Prop
    x = TCon -> [Prop] -> Prop
    TCon (TFun -> TCon
    TF TFun
    f) [Prop
    x]

    tf2 :: TFun -> Type -> Type -> Type
    tf2 :: TFun -> Prop -> Prop -> Prop
    tf2 f :: TFun
    f x :: Prop
    x y :: Prop
    y = TCon -> [Prop] -> Prop
    TCon (TFun -> TCon
    TF TFun
    f) [Prop
    x,Prop
    y]

    tf3 :: TFun -> Type -> Type -> Type -> Type
    tf3 :: TFun -> Prop -> Prop -> Prop -> Prop
    tf3 f :: TFun
    f x :: Prop
    x y :: Prop
    y z :: Prop
    z = TCon -> [Prop] -> Prop
    TCon (TFun -> TCon
    TF TFun
    f) [Prop
    x,Prop
    y,Prop
    z]

    tSub :: Type -> Type -> Type
    tSub :: Prop -> Prop -> Prop
    tSub = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCSub

    tMul :: Type -> Type -> Type
    tMul :: Prop -> Prop -> Prop
    tMul = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCMul

    tDiv :: Type -> Type -> Type
    tDiv :: Prop -> Prop -> Prop
    tDiv = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCDiv

    tMod :: Type -> Type -> Type
    tMod :: Prop -> Prop -> Prop
    tMod = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCMod

    tExp :: Type -> Type -> Type
    tExp :: Prop -> Prop -> Prop
    tExp = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCExp

    tMin :: Type -> Type -> Type
    tMin :: Prop -> Prop -> Prop
    tMin = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCMin

    tCeilDiv :: Type -> Type -> Type
    tCeilDiv :: Prop -> Prop -> Prop
    tCeilDiv = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCCeilDiv

    tCeilMod :: Type -> Type -> Type
    tCeilMod :: Prop -> Prop -> Prop
    tCeilMod = TFun -> Prop -> Prop -> Prop
    tf2 TFun
    TCCeilMod

    tLenFromThenTo :: Type -> Type -> Type -> Type
    tLenFromThenTo :: Prop -> Prop -> Prop -> Prop
    tLenFromThenTo = TFun -> Prop -> Prop -> Prop -> Prop
    tf3 TFun
    TCLenFromThenTo

    --------------------------------------------------------------------------------
    -- Construction of constraints.

    -- | Equality for numeric types.
    (=#=) :: Type -> Type -> Prop
    x :: Prop
    x =#= :: Prop -> Prop -> Prop
    =#= y :: Prop
    y = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PEqual) [Prop
    x,Prop
    y]

    (=/=) :: Type -> Type -> Prop
    x :: Prop
    x =/= :: Prop -> Prop -> Prop
    =/= y :: Prop
    y = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PNeq) [Prop
    x,Prop
    y]

    pZero :: Type -> Prop
    pZero :: Prop -> Prop
    pZero t :: Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PZero) [Prop
    t]

    pLogic :: Type -> Prop
    pLogic :: Prop -> Prop
    pLogic t :: Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PLogic) [Prop
    t]

    pArith :: Type -> Prop
    pArith :: Prop -> Prop
    pArith t :: Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PArith) [Prop
    t]

    pCmp :: Type -> Prop
    pCmp :: Prop -> Prop
    pCmp t :: Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PCmp) [Prop
    t]

    pSignedCmp :: Type -> Prop
    pSignedCmp :: Prop -> Prop
    pSignedCmp t :: Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PSignedCmp) [Prop
    t]

    pLiteral :: Type -> Type -> Prop
    pLiteral :: Prop -> Prop -> Prop
    pLiteral x :: Prop
    x y :: Prop
    y = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PLiteral) [Prop
    x, Prop
    y]

    -- | Make a greater-than-or-equal-to constraint.
    (>==) :: Type -> Type -> Prop
    x :: Prop
    x >== :: Prop -> Prop -> Prop
    >== y :: Prop
    y = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PGeq) [Prop
    x,Prop
    y]

    -- | A `Has` constraint, used for tuple and record selection.
    pHas :: Selector -> Type -> Type -> Prop
    pHas :: Selector -> Prop -> Prop -> Prop
    pHas l :: Selector
    l ty :: Prop
    ty fi :: Prop
    fi = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC (Selector -> PC
    PHas Selector
    l)) [Prop
    ty,Prop
    fi]

    pTrue :: Prop
    pTrue :: Prop
    pTrue = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PTrue) []

    pAnd :: [Prop] -> Prop
    pAnd :: [Prop] -> Prop
    pAnd []       = Prop
    pTrue
    pAnd [x :: Prop
    x]      = Prop
    x
    pAnd (x :: Prop
    x : xs :: [Prop]
    xs)
      | Just _ <- Prop -> Maybe TCErrorMessage
    tIsError Prop
    x    = Prop
    x
      | Prop -> Bool
    pIsTrue Prop
    x               = Prop
    rest
      | Just _ <- Prop -> Maybe TCErrorMessage
    tIsError Prop
    rest = Prop
    rest
      | Prop -> Bool
    pIsTrue Prop
    rest            = Prop
    x
      | Bool
    otherwise               = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PAnd) [Prop
    x, Prop
    rest]
      where rest :: Prop
    rest = [Prop] -> Prop
    pAnd [Prop]
    xs

    pSplitAnd :: Prop -> [Prop]
    pSplitAnd :: Prop -> [Prop]
    pSplitAnd p0 :: Prop
    p0 = [Prop] -> [Prop]
    go [Prop
    p0]
      where
      go :: [Prop] -> [Prop]
    go [] = []
      go (q :: Prop
    q : qs :: [Prop]
    qs) =
        case Prop -> Prop
    tNoUser Prop
    q of
          TCon (PC PAnd) [l :: Prop
    l,r :: Prop
    r] -> [Prop] -> [Prop]
    go (Prop
    l Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : Prop
    r Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : [Prop]
    qs)
          TCon (PC PTrue) _    -> [Prop] -> [Prop]
    go [Prop]
    qs
          _                    -> Prop
    q Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : [Prop] -> [Prop]
    go [Prop]
    qs

    pFin :: Type -> Prop
    pFin :: Prop -> Prop
    pFin ty :: Prop
    ty =
      case Prop -> Prop
    tNoUser Prop
    ty of
        TCon (TC (TCNum _)) _ -> Prop
    pTrue
        TCon (TC TCInf)     _ -> TCErrorMessage -> Prop
    pError (String -> TCErrorMessage
    TCErrorMessage "`inf` is not finite.")
        _                     -> TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PFin) [Prop
    ty]

    -- | Make a malformed property.
    pError :: TCErrorMessage -> Prop
    pError :: TCErrorMessage -> Prop
    pError msg :: TCErrorMessage
    msg = TCon -> [Prop] -> Prop
    TCon (Kind -> TCErrorMessage -> TCon
    TError Kind
    KProp TCErrorMessage
    msg) []

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

    noFreeVariables :: FVS t => t -> Bool
    noFreeVariables :: t -> Bool
    noFreeVariables = (TVar -> Bool) -> [TVar] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Bool -> Bool
    not (Bool -> Bool) -> (TVar -> Bool) -> TVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TVar -> Bool
    isFreeTV) ([TVar] -> Bool) -> (t -> [TVar]) -> t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList (Set TVar -> [TVar]) -> (t -> Set TVar) -> t -> [TVar]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs

    class FVS t where
      fvs :: t -> Set TVar

    instance FVS Type where
      fvs :: Prop -> Set TVar
    fvs = Prop -> Set TVar
    go
        where
        go :: Prop -> Set TVar
    go ty :: Prop
    ty =
          case Prop
    ty of
            TCon _ ts :: [Prop]
    ts   -> [Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Prop]
    ts
            TVar x :: TVar
    x      -> TVar -> Set TVar
    forall a. a -> Set a
    Set.singleton TVar
    x
            TUser _ _ t :: Prop
    t -> Prop -> Set TVar
    go Prop
    t
            TRec fs :: [(Ident, Prop)]
    fs     -> [Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (((Ident, Prop) -> Prop) -> [(Ident, Prop)] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Prop
    forall a b. (a, b) -> b
    snd [(Ident, Prop)]
    fs)

    instance FVS a => FVS (Maybe a) where
      fvs :: Maybe a -> Set TVar
    fvs Nothing  = Set TVar
    forall a. Set a
    Set.empty
      fvs (Just x :: a
    x) = a -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs a
    x

    instance FVS a => FVS [a] where
      fvs :: [a] -> Set TVar
    fvs xs :: [a]
    xs        = [Set TVar] -> Set TVar
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ((a -> Set TVar) -> [a] -> [Set TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [a]
    xs)

    instance (FVS a, FVS b) => FVS (a,b) where
      fvs :: (a, b) -> Set TVar
    fvs (x :: a
    x,y :: b
    y) = Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (a -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs a
    x) (b -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs b
    y)

    instance FVS Schema where
      fvs :: Schema -> Set TVar
    fvs (Forall as :: [TParam]
    as ps :: [Prop]
    ps t :: Prop
    t) =
          Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    Set.difference (Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union ([Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Prop]
    ps) (Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Prop
    t)) Set TVar
    bound
        where bound :: Set TVar
    bound = [TVar] -> Set TVar
    forall a. Ord a => [a] -> Set a
    Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar [TParam]
    as)

    -- Pretty Printing -------------------------------------------------------------

    instance PP TParam where
      ppPrec :: Int -> TParam -> Doc
    ppPrec = NameMap -> Int -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames TParam) where
      ppPrec :: Int -> WithNames TParam -> Doc
    ppPrec _ (WithNames p :: TParam
    p mp :: NameMap
    mp) = NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    mp (TParam -> TVar
    tpVar TParam
    p)

    addTNames :: [TParam] -> NameMap -> NameMap
    addTNames :: [TParam] -> NameMap -> NameMap
    addTNames as :: [TParam]
    as ns :: NameMap
    ns = ((Int, String) -> NameMap -> NameMap)
    -> NameMap -> [(Int, String)] -> NameMap
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Int -> String -> NameMap -> NameMap)
    -> (Int, String) -> NameMap -> NameMap
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Int -> String -> NameMap -> NameMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert) NameMap
    ns
                    ([(Int, String)] -> NameMap) -> [(Int, String)] -> NameMap
    forall a b. (a -> b) -> a -> b
    $ [(Int, String)]
    named [(Int, String)] -> [(Int, String)] -> [(Int, String)]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [String] -> [(Int, String)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    unnamed_nums [String]
    numNames
                            [(Int, String)] -> [(Int, String)] -> [(Int, String)]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [String] -> [(Int, String)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    unnamed_vals [String]
    valNames

      where avail :: [String] -> [String]
    avail xs :: [String]
    xs = (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [String]
    used) ([String] -> [String]
    nameList [String]
    xs)
            numNames :: [String]
    numNames = [String] -> [String]
    avail ["n","m","i","j","k"]
            valNames :: [String]
    valNames = [String] -> [String]
    avail ["a","b","c","d","e"]

            nm :: TParam -> (Int, Maybe Name, Kind)
    nm x :: TParam
    x = (TParam -> Int
    tpUnique TParam
    x, TParam -> Maybe Name
    tpName TParam
    x, TParam -> Kind
    tpKind TParam
    x)

            named :: [(Int, String)]
    named        = [ (Int
    u,Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n)) | (u :: Int
    u,Just n :: Name
    n,_)  <- (TParam -> (Int, Maybe Name, Kind))
    -> [TParam] -> [(Int, Maybe Name, Kind)]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> (Int, Maybe Name, Kind)
    nm [TParam]
    as ]
            unnamed_nums :: [Int]
    unnamed_nums = [ Int
    u               | (u :: Int
    u,Nothing,KNum)  <- (TParam -> (Int, Maybe Name, Kind))
    -> [TParam] -> [(Int, Maybe Name, Kind)]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> (Int, Maybe Name, Kind)
    nm [TParam]
    as ]
            unnamed_vals :: [Int]
    unnamed_vals = [ Int
    u               | (u :: Int
    u,Nothing,KType) <- (TParam -> (Int, Maybe Name, Kind))
    -> [TParam] -> [(Int, Maybe Name, Kind)]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> (Int, Maybe Name, Kind)
    nm [TParam]
    as ]

            used :: [String]
    used    = ((Int, String) -> String) -> [(Int, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, String) -> String
    forall a b. (a, b) -> b
    snd [(Int, String)]
    named [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ NameMap -> [String]
    forall a. IntMap a -> [a]
    IntMap.elems NameMap
    ns

    ppNewtypeShort :: Newtype -> Doc
    ppNewtypeShort :: Newtype -> Doc
    ppNewtypeShort nt :: Newtype
    nt =
      String -> Doc
    text "newtype" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp (Newtype -> Name
    ntName Newtype
    nt) Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    hsep ((TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Int -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    nm 9) [TParam]
    ps)
      where
      ps :: [TParam]
    ps  = Newtype -> [TParam]
    ntParams Newtype
    nt
      nm :: NameMap
    nm = [TParam] -> NameMap -> NameMap
    addTNames [TParam]
    ps NameMap
    emptyNameMap

    instance PP Schema where
      ppPrec :: Int -> Schema -> Doc
    ppPrec = NameMap -> Int -> Schema -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames Schema) where
      ppPrec :: Int -> WithNames Schema -> Doc
    ppPrec _ (WithNames s :: Schema
    s ns :: NameMap
    ns)
        | [TParam] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Schema -> [TParam]
    sVars Schema
    s) Bool -> Bool -> Bool
    && [Prop] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Schema -> [Prop]
    sProps Schema
    s) = Doc
    body
        | Bool
    otherwise = Doc -> Int -> Doc -> Doc
    hang (Doc
    vars Doc -> Doc -> Doc
    <+> Doc
    props) 2 Doc
    body
        where
        body :: Doc
    body = NameMap -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 (Schema -> Prop
    sType Schema
    s)

        vars :: Doc
    vars = case Schema -> [TParam]
    sVars Schema
    s of
          [] -> Doc
    empty
          vs :: [TParam]
    vs -> Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    commaSep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1) [TParam]
    vs

        props :: Doc
    props = case Schema -> [Prop]
    sProps Schema
    s of
          [] -> Doc
    empty
          ps :: [Prop]
    ps -> Doc -> Doc
    parens ([Doc] -> Doc
    commaSep ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1) [Prop]
    ps)) Doc -> Doc -> Doc
    <+> String -> Doc
    text "=>"

        ns1 :: NameMap
    ns1 = [TParam] -> NameMap -> NameMap
    addTNames (Schema -> [TParam]
    sVars Schema
    s) NameMap
    ns

    instance PP TySyn where
      ppPrec :: Int -> TySyn -> Doc
    ppPrec = NameMap -> Int -> TySyn -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames TySyn) where
      ppPrec :: Int -> WithNames TySyn -> Doc
    ppPrec _ (WithNames ts :: TySyn
    ts ns :: NameMap
    ns) =
        String -> Doc
    text "type" Doc -> Doc -> Doc
    <+> Doc
    ctr Doc -> Doc -> Doc
    <+> Doc
    lhs Doc -> Doc -> Doc
    <+> Char -> Doc
    char '=' Doc -> Doc -> Doc
    <+> NameMap -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 (TySyn -> Prop
    tsDef TySyn
    ts)
        where ns1 :: NameMap
    ns1 = [TParam] -> NameMap -> NameMap
    addTNames (TySyn -> [TParam]
    tsParams TySyn
    ts) NameMap
    ns
              ctr :: Doc
    ctr = case Kind -> Kind
    kindResult (TySyn -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TySyn
    ts) of
                      KProp -> String -> Doc
    text "constraint"
                      _     -> Doc
    empty
              n :: Name
    n = TySyn -> Name
    tsName TySyn
    ts
              lhs :: Doc
    lhs = case (Name -> Maybe Fixity
    nameFixity Name
    n, TySyn -> [TParam]
    tsParams TySyn
    ts) of
                      (Just _, [x :: TParam
    x, y :: TParam
    y]) ->
                        NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 TParam
    x Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall a. PP a => a -> Doc
    pp (Name -> Ident
    nameIdent Name
    n) Doc -> Doc -> Doc
    <+> NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 TParam
    y
                      (_, ps :: [TParam]
    ps) ->
                        Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    sep ((TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1) [TParam]
    ps)

    instance PP Newtype where
      ppPrec :: Int -> Newtype -> Doc
    ppPrec = NameMap -> Int -> Newtype -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP (WithNames Newtype) where
      ppPrec :: Int -> WithNames Newtype -> Doc
    ppPrec _  (WithNames nt :: Newtype
    nt _) = Newtype -> Doc
    ppNewtypeShort Newtype
    nt -- XXX: do the full thing?

    instance PP (WithNames Type) where
      ppPrec :: Int -> WithNames Prop -> Doc
    ppPrec prec :: Int
    prec ty0 :: WithNames Prop
    ty0@(WithNames ty :: Prop
    ty nmMap :: NameMap
    nmMap) =
        case Prop
    ty of
          TVar a :: TVar
    a  -> NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nmMap TVar
    a
          TRec fs :: [(Ident, Prop)]
    fs -> Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma
                        [ Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    l Doc -> Doc -> Doc
    <+> String -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t | (l :: Ident
    l,t :: Prop
    t) <- [(Ident, Prop)]
    fs ]

          _ | Just tinf :: Infix Ident (WithNames Prop)
    tinf <- WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
    isTInfix WithNames Prop
    ty0 -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 2)
                                         (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int
    -> (WithNames Prop -> Maybe (Infix Ident (WithNames Prop)))
    -> Infix Ident (WithNames Prop)
    -> Doc
    forall thing op.
    (PP thing, PP op) =>
    Int -> (thing -> Maybe (Infix op thing)) -> Infix op thing -> Doc
    ppInfix 2 WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
    isTInfix Infix Ident (WithNames Prop)
    tinf

          TUser c :: Name
    c [] _ -> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    c
          TUser c :: Name
    c ts :: [Prop]
    ts _ -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    c Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    fsep ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4) [Prop]
    ts)

          TCon (TC tc :: TC
    tc) ts :: [Prop]
    ts ->
            case (TC
    tc,[Prop]
    ts) of
              (TCNum n :: Integer
    n, [])       -> Integer -> Doc
    integer Integer
    n
              (TCInf,   [])       -> String -> Doc
    text "inf"
              (TCBit,   [])       -> String -> Doc
    text "Bit"
              (TCInteger, [])     -> String -> Doc
    text "Integer"
              (TCIntMod, [n :: Prop
    n])     -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text "Z" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    n

              (TCSeq,   [t1 :: Prop
    t1,TCon (TC TCBit) []]) -> Doc -> Doc
    brackets (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t1)
              (TCSeq,   [t1 :: Prop
    t1,t2 :: Prop
    t2])  -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3)
                                  (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc
    brackets (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t1) Doc -> Doc -> Doc
    <.> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 3 Prop
    t2

              (TCFun,   [t1 :: Prop
    t1,t2 :: Prop
    t2])  -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1)
                                  (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 2 Prop
    t1 Doc -> Doc -> Doc
    <+> String -> Doc
    text "->" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 1 Prop
    t2

              (TCTuple _, fs :: [Prop]
    fs)     -> Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0) [Prop]
    fs

              (_, _)              -> TC -> Doc
    forall a. PP a => a -> Doc
    pp TC
    tc Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    fsep ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4) [Prop]
    ts)

          TCon (PC pc :: PC
    pc) ts :: [Prop]
    ts ->
            case (PC
    pc,[Prop]
    ts) of
              (PEqual, [t1 :: Prop
    t1,t2 :: Prop
    t2])   -> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t1 Doc -> Doc -> Doc
    <+> String -> Doc
    text "==" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t2
              (PNeq ,  [t1 :: Prop
    t1,t2 :: Prop
    t2])   -> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t1 Doc -> Doc -> Doc
    <+> String -> Doc
    text "!=" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t2
              (PGeq,  [t1 :: Prop
    t1,t2 :: Prop
    t2])    -> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t1 Doc -> Doc -> Doc
    <+> String -> Doc
    text ">=" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t2
              (PFin,  [t1 :: Prop
    t1])       -> String -> Doc
    text "fin" Doc -> Doc -> Doc
    <+> (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    t1)
              (PHas x :: Selector
    x, [t1 :: Prop
    t1,t2 :: Prop
    t2])   -> Selector -> Doc
    ppSelector Selector
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "of"
                                   Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t1 Doc -> Doc -> Doc
    <+> String -> Doc
    text "is" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 0 Prop
    t2

              (PArith, [t1 :: Prop
    t1])      -> PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    pc Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    t1
              (PCmp, [t1 :: Prop
    t1])        -> PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    pc Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    t1
              (PSignedCmp, [t1 :: Prop
    t1])  -> PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    pc Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    t1
              (PLiteral, [t1 :: Prop
    t1,t2 :: Prop
    t2]) -> PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    pc Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    t1 Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4 Prop
    t2

              (_, _)              -> PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    pc Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    fsep ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4) [Prop]
    ts)

          TCon f :: TCon
    f ts :: [Prop]
    ts -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 3)
                    (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ TCon -> Doc
    forall a. PP a => a -> Doc
    pp TCon
    f Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    fsep ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall a. PP (WithNames a) => Int -> a -> Doc
    go 4) [Prop]
    ts)

        where
        go :: Int -> a -> Doc
    go p :: Int
    p t :: a
    t = NameMap -> Int -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    nmMap Int
    p a
    t

        isTInfix :: WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
    isTInfix (WithNames (TCon tc :: TCon
    tc [ieLeft' :: Prop
    ieLeft',ieRight' :: Prop
    ieRight']) _) =
          do let ieLeft :: WithNames Prop
    ieLeft  = Prop -> NameMap -> WithNames Prop
    forall a. a -> NameMap -> WithNames a
    WithNames Prop
    ieLeft' NameMap
    nmMap
                 ieRight :: WithNames Prop
    ieRight = Prop -> NameMap -> WithNames Prop
    forall a. a -> NameMap -> WithNames a
    WithNames Prop
    ieRight' NameMap
    nmMap
             (ieOp :: Ident
    ieOp,fi :: Fixity
    fi) <- TCon -> Maybe (Ident, Fixity)
    infixPrimTy TCon
    tc
             let ieAssoc :: Assoc
    ieAssoc = Fixity -> Assoc
    fAssoc Fixity
    fi
                 iePrec :: Int
    iePrec  = Fixity -> Int
    fLevel Fixity
    fi
             Infix Ident (WithNames Prop)
    -> Maybe (Infix Ident (WithNames Prop))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Infix :: forall op thing.
    op -> thing -> thing -> Int -> Assoc -> Infix op thing
    Infix { .. }

        isTInfix (WithNames (TUser n :: Name
    n [ieLeft' :: Prop
    ieLeft',ieRight' :: Prop
    ieRight'] _) _) =
          do let ieLeft :: WithNames Prop
    ieLeft  = Prop -> NameMap -> WithNames Prop
    forall a. a -> NameMap -> WithNames a
    WithNames Prop
    ieLeft' NameMap
    nmMap
                 ieRight :: WithNames Prop
    ieRight = Prop -> NameMap -> WithNames Prop
    forall a. a -> NameMap -> WithNames a
    WithNames Prop
    ieRight' NameMap
    nmMap
             Fixity
    fi <- Name -> Maybe Fixity
    nameFixity Name
    n
             let ieAssoc :: Assoc
    ieAssoc = Fixity -> Assoc
    fAssoc Fixity
    fi
                 iePrec :: Int
    iePrec  = Fixity -> Int
    fLevel Fixity
    fi
                 ieOp :: Ident
    ieOp    = Name -> Ident
    nameIdent Name
    n
             Infix Ident (WithNames Prop)
    -> Maybe (Infix Ident (WithNames Prop))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Infix :: forall op thing.
    op -> thing -> thing -> Int -> Assoc -> Infix op thing
    Infix { .. }

        isTInfix _ = Maybe (Infix Ident (WithNames Prop))
    forall a. Maybe a
    Nothing

    instance PP (WithNames TVar) where

      ppPrec :: Int -> WithNames TVar -> Doc
    ppPrec _ (WithNames (TVBound x :: TParam
    x) mp :: NameMap
    mp) =
        case Int -> NameMap -> Maybe String
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup (TParam -> Int
    tpUnique TParam
    x) NameMap
    mp of
          Just a :: String
    a  -> String -> Doc
    text String
    a
          Nothing ->
            case TParam -> TPFlavor
    tpFlav TParam
    x of
              TPModParam n :: Name
    n     -> Name -> Doc
    forall a. PPName a => a -> Doc
    ppPrefixName Name
    n
              TPOther (Just n :: Name
    n) -> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n Doc -> Doc -> Doc
    <.> "`" Doc -> Doc -> Doc
    <.> Int -> Doc
    int (TParam -> Int
    tpUnique TParam
    x)
              _  -> Kind -> TVarSource -> Int -> Doc
    pickTVarName (TParam -> Kind
    tpKind TParam
    x) (TVarInfo -> TVarSource
    tvarDesc (TParam -> TVarInfo
    tpInfo TParam
    x)) (TParam -> Int
    tpUnique TParam
    x)

      ppPrec _ (WithNames (TVFree x :: Int
    x k :: Kind
    k _ d :: TVarInfo
    d) _) =
        Char -> Doc
    char '?' Doc -> Doc -> Doc
    <.> Kind -> TVarSource -> Int -> Doc
    pickTVarName Kind
    k (TVarInfo -> TVarSource
    tvarDesc TVarInfo
    d) Int
    x

    pickTVarName :: Kind -> TVarSource -> Int -> Doc
    pickTVarName :: Kind -> TVarSource -> Int -> Doc
    pickTVarName k :: Kind
    k src :: TVarSource
    src uni :: Int
    uni =
      String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $
      case TVarSource
    src of
        TVFromModParam n :: Name
    n       -> Name -> String
    forall a. PP a => a -> String
    using Name
    n
        TVFromSignature n :: Name
    n      -> Name -> String
    forall a. PP a => a -> String
    using Name
    n
        TypeWildCard           -> ShowS
    mk ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ case Kind
    k of
                                         KNum -> "n"
                                         _    -> "a"
        TypeOfRecordField i :: Ident
    i    -> Ident -> String
    forall a. PP a => a -> String
    using Ident
    i
        TypeOfTupleField n :: Int
    n     -> ShowS
    mk ("tup_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n)
        TypeOfSeqElement       -> ShowS
    mk "a"
        LenOfSeq               -> ShowS
    mk "n"
        TypeParamInstNamed _ i :: Ident
    i -> Ident -> String
    forall a. PP a => a -> String
    using Ident
    i
        TypeParamInstPos f :: Name
    f n :: Int
    n   -> ShowS
    mk (Name -> String
    forall a. PP a => a -> String
    sh Name
    f String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n)
        DefinitionOf x :: Name
    x         -> Name -> String
    forall a. PP a => a -> String
    using Name
    x
        LenOfCompGen           -> ShowS
    mk "n"
        TypeOfArg mb :: Maybe Int
    mb           -> ShowS
    mk (case Maybe Int
    mb of
                                        Nothing -> "arg"
                                        Just n :: Int
    n  -> "arg_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n)
        TypeOfRes              -> "res"
        TypeErrorPlaceHolder   -> "err"
      where
      sh :: a -> String
    sh a :: a
    a      = Doc -> String
    forall a. Show a => a -> String
    show (a -> Doc
    forall a. PP a => a -> Doc
    pp a
    a)
      using :: a -> String
    using a :: a
    a   = ShowS
    mk (a -> String
    forall a. PP a => a -> String
    sh a
    a)
      mk :: ShowS
    mk a :: String
    a      = String
    a String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "`" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    uni

    instance PP TVar where
      ppPrec :: Int -> TVar -> Doc
    ppPrec = NameMap -> Int -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty

    instance PP Type where
      ppPrec :: Int -> Prop -> Doc
    ppPrec n :: Int
    n t :: Prop
    t = NameMap -> Int -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty Int
    n Prop
    t

    instance PP TVarInfo where
      ppPrec :: Int -> TVarInfo -> Doc
    ppPrec _ tvinfo :: TVarInfo
    tvinfo = TVarSource -> Doc
    forall a. PP a => a -> Doc
    pp (TVarInfo -> TVarSource
    tvarDesc TVarInfo
    tvinfo) Doc -> Doc -> Doc
    <+> Doc
    loc
        where
        loc :: Doc
    loc = if Range
    rng Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    emptyRange then Doc
    empty else "at" Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp Range
    rng
        rng :: Range
    rng = TVarInfo -> Range
    tvarSource TVarInfo
    tvinfo

    instance PP TVarSource where
      ppPrec :: Int -> TVarSource -> Doc
    ppPrec _ tvsrc :: TVarSource
    tvsrc =
        case TVarSource
    tvsrc of
          TVFromModParam m :: Name
    m    -> "module parameter" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    m
          TVFromSignature x :: Name
    x   -> "signature variable" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x)
          TypeWildCard        -> "type wildcard (_)"
          TypeOfRecordField l :: Ident
    l -> "type of field" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    l)
          TypeOfTupleField n :: Int
    n  -> "type of" Doc -> Doc -> Doc
    <+> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    n Doc -> Doc -> Doc
    <+> "tuple field"
          TypeOfSeqElement    -> "type of sequence member"
          LenOfSeq            -> "length of sequence"
          TypeParamInstNamed f :: Name
    f i :: Ident
    i -> "type argument" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i) Doc -> Doc -> Doc
    <+>
                                              "of" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f)
          TypeParamInstPos   f :: Name
    f i :: Int
    i -> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    i Doc -> Doc -> Doc
    <+> "type argument of" Doc -> Doc -> Doc
    <+>
                                                          Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f)
          DefinitionOf x :: Name
    x      -> "the type of" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x)
          LenOfCompGen        -> "length of comprehension generator"
          TypeOfArg mb :: Maybe Int
    mb ->
            case Maybe Int
    mb of
              Nothing -> "type of function argument"
              Just n :: Int
    n -> "type of" Doc -> Doc -> Doc
    <+> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    n Doc -> Doc -> Doc
    <+> "function argument"
          TypeOfRes             -> "type of function result"
          TypeErrorPlaceHolder  -> "type error place-holder"