    {-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
    {-# Language FlexibleInstances, FlexibleContexts #-}
    {-# Language PatternGuards #-}
    {-# Language OverloadedStrings #-}
    {-| This module contains types related to typechecking and the output of the
    typechecker.  In particular, it should contain the types needed by
    interface files (see 'Crytpol.ModuleSystem.Interface'), which are (kind of)
    the output of the typechker.
    -}
    module Cryptol.TypeCheck.Type
      ( module Cryptol.TypeCheck.Type
      , module Cryptol.TypeCheck.TCon
      ) where

    import GHC.Generics (Generic)
    import Control.DeepSeq

    import           Data.Map(Map)
    import qualified Data.Map as Map
    import qualified Data.IntMap as IntMap
    import           Data.Maybe (fromMaybe)
    import           Data.Set (Set)
    import qualified Data.Set as Set
    import           Data.Text (Text)

    import Cryptol.Parser.Selector
    import Cryptol.Parser.Position(Located,thing,Range,emptyRange)
    import Cryptol.Parser.AST(ImpName(..))
    import Cryptol.ModuleSystem.Name
    import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName, ogModule, ModName)
    import Cryptol.TypeCheck.TCon
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Solver.InfNat
    import Cryptol.Utils.Fixity
    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.RecordMap
    import Prelude

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

    --------------------------------------------------------------------------------
    -- Module parameters

    type FunctorParams = Map Ident ModParam

    -- | Compute the names from all functor parameters
    allParamNames :: FunctorParams -> ModParamNames
    allParamNames :: FunctorParams -> ModParamNames
    allParamNames FunctorParams
    mps =
      ModParamNames
        { mpnTypes :: Map Name ModTParam
    mpnTypes       = [Map Name ModTParam] -> Map Name ModTParam
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((ModParamNames -> Map Name ModTParam)
    -> [ModParamNames] -> [Map Name ModTParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModParamNames -> Map Name ModTParam
    mpnTypes [ModParamNames]
    ps)
        , mpnConstraints :: [Located Prop]
    mpnConstraints = (ModParamNames -> [Located Prop])
    -> [ModParamNames] -> [Located Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ModParamNames -> [Located Prop]
    mpnConstraints [ModParamNames]
    ps
        , mpnFuns :: Map Name ModVParam
    mpnFuns        = [Map Name ModVParam] -> Map Name ModVParam
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((ModParamNames -> Map Name ModVParam)
    -> [ModParamNames] -> [Map Name ModVParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModParamNames -> Map Name ModVParam
    mpnFuns [ModParamNames]
    ps)
        , mpnTySyn :: Map Name TySyn
    mpnTySyn       = [Map Name TySyn] -> Map Name TySyn
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((ModParamNames -> Map Name TySyn)
    -> [ModParamNames] -> [Map Name TySyn]
    forall a b. (a -> b) -> [a] -> [b]
    map ModParamNames -> Map Name TySyn
    mpnTySyn [ModParamNames]
    ps)
        , mpnDoc :: Maybe Text
    mpnDoc         = Maybe Text
    forall a. Maybe a
    Nothing
        }
      where
      ps :: [ModParamNames]
    ps = (ModParam -> ModParamNames) -> [ModParam] -> [ModParamNames]
    forall a b. (a -> b) -> [a] -> [b]
    map ModParam -> ModParamNames
    mpParameters (FunctorParams -> [ModParam]
    forall k a. Map k a -> [a]
    Map.elems FunctorParams
    mps)

    -- | A module parameter.  Corresponds to a "signature import".
    -- A single module parameter can bring multiple things in scope.
    data ModParam = ModParam
      { ModParam -> Ident
    mpName        :: Ident
        -- ^ The name of a functor parameter.

      , ModParam -> Maybe ModName
    mpQual        :: !(Maybe ModName)
        -- ^ This is the qualifier for the parameter.  We use it to
        -- derive parameter names when doing `_` imports.

      , ModParam -> ImpName Name
    mpIface       :: ImpName Name
        -- ^ The interface corresponding to this parameter.
        -- This is thing in `import interface`

      , ModParam -> ModParamNames
    mpParameters  :: ModParamNames
        {- ^ These are the actual parameters, not the ones in the interface
          For example if the same interface is used for multiple parameters
          the `ifmpParameters` would all be different. -}
      } deriving (Int -> ModParam -> ShowS
    [ModParam] -> ShowS
    ModParam -> [Char]
    (Int -> ModParam -> ShowS)
    -> (ModParam -> [Char]) -> ([ModParam] -> ShowS) -> Show ModParam
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ModParam -> ShowS
    showsPrec :: Int -> ModParam -> ShowS
    $cshow :: ModParam -> [Char]
    show :: ModParam -> [Char]
    $cshowList :: [ModParam] -> ShowS
    showList :: [ModParam] -> ShowS
    Show, (forall x. ModParam -> Rep ModParam x)
    -> (forall x. Rep ModParam x -> ModParam) -> Generic ModParam
    forall x. Rep ModParam x -> ModParam
    forall x. ModParam -> Rep ModParam x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ModParam -> Rep ModParam x
    from :: forall x. ModParam -> Rep ModParam x
    $cto :: forall x. Rep ModParam x -> ModParam
    to :: forall x. Rep ModParam x -> ModParam
    Generic, ModParam -> ()
    (ModParam -> ()) -> NFData ModParam
    forall a. (a -> ()) -> NFData a
    $crnf :: ModParam -> ()
    rnf :: ModParam -> ()
    NFData)

    -- | Information about the names brought in through an "interface import".
    -- This is also used to keep information about.
    data ModParamNames = ModParamNames
      { ModParamNames -> Map Name ModTParam
    mpnTypes       :: Map Name ModTParam
        -- ^ Type parameters

      , ModParamNames -> Map Name TySyn
    mpnTySyn      :: !(Map Name TySyn)
        -- ^ Type synonyms

      , ModParamNames -> [Located Prop]
    mpnConstraints :: [Located Prop]
        -- ^ Constraints on param. types

      , ModParamNames -> Map Name ModVParam
    mpnFuns        :: Map.Map Name ModVParam
        -- ^ Value parameters

      , ModParamNames -> Maybe Text
    mpnDoc         :: !(Maybe Text)
        -- ^ Documentation about the interface.
      } deriving (Int -> ModParamNames -> ShowS
    [ModParamNames] -> ShowS
    ModParamNames -> [Char]
    (Int -> ModParamNames -> ShowS)
    -> (ModParamNames -> [Char])
    -> ([ModParamNames] -> ShowS)
    -> Show ModParamNames
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ModParamNames -> ShowS
    showsPrec :: Int -> ModParamNames -> ShowS
    $cshow :: ModParamNames -> [Char]
    show :: ModParamNames -> [Char]
    $cshowList :: [ModParamNames] -> ShowS
    showList :: [ModParamNames] -> ShowS
    Show, (forall x. ModParamNames -> Rep ModParamNames x)
    -> (forall x. Rep ModParamNames x -> ModParamNames)
    -> Generic ModParamNames
    forall x. Rep ModParamNames x -> ModParamNames
    forall x. ModParamNames -> Rep ModParamNames x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ModParamNames -> Rep ModParamNames x
    from :: forall x. ModParamNames -> Rep ModParamNames x
    $cto :: forall x. Rep ModParamNames x -> ModParamNames
    to :: forall x. Rep ModParamNames x -> ModParamNames
    Generic, ModParamNames -> ()
    (ModParamNames -> ()) -> NFData ModParamNames
    forall a. (a -> ()) -> NFData a
    $crnf :: ModParamNames -> ()
    rnf :: ModParamNames -> ()
    NFData)

    -- | A type parameter of a module.
    data ModTParam = ModTParam
      { ModTParam -> Name
    mtpName   :: Name
      , ModTParam -> Kind
    mtpKind   :: Kind
      , ModTParam -> Maybe Text
    mtpDoc    :: Maybe Text
      } deriving (Int -> ModTParam -> ShowS
    [ModTParam] -> ShowS
    ModTParam -> [Char]
    (Int -> ModTParam -> ShowS)
    -> (ModTParam -> [Char])
    -> ([ModTParam] -> ShowS)
    -> Show ModTParam
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ModTParam -> ShowS
    showsPrec :: Int -> ModTParam -> ShowS
    $cshow :: ModTParam -> [Char]
    show :: ModTParam -> [Char]
    $cshowList :: [ModTParam] -> ShowS
    showList :: [ModTParam] -> ShowS
    Show,(forall x. ModTParam -> Rep ModTParam x)
    -> (forall x. Rep ModTParam x -> ModTParam) -> Generic ModTParam
    forall x. Rep ModTParam x -> ModTParam
    forall x. ModTParam -> Rep ModTParam x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ModTParam -> Rep ModTParam x
    from :: forall x. ModTParam -> Rep ModTParam x
    $cto :: forall x. Rep ModTParam x -> ModTParam
    to :: forall x. Rep ModTParam x -> ModTParam
    Generic,ModTParam -> ()
    (ModTParam -> ()) -> NFData ModTParam
    forall a. (a -> ()) -> NFData a
    $crnf :: ModTParam -> ()
    rnf :: ModTParam -> ()
    NFData)

    -- | This is how module parameters appear in actual types.
    mtpParam :: ModTParam -> TParam
    mtpParam :: ModTParam -> TParam
    mtpParam ModTParam
    mtp = TParam { tpUnique :: Int
    tpUnique = Name -> Int
    nameUnique (ModTParam -> Name
    mtpName ModTParam
    mtp)
                          , tpKind :: Kind
    tpKind   = ModTParam -> Kind
    mtpKind ModTParam
    mtp
                          , tpFlav :: TPFlavor
    tpFlav   = Name -> TPFlavor
    TPModParam (ModTParam -> Name
    mtpName ModTParam
    mtp)
                          , tpInfo :: TVarInfo
    tpInfo   = TVarInfo
    desc
                          }
      where desc :: TVarInfo
    desc = TVarInfo { tvarDesc :: TypeSource
    tvarDesc   = Name -> TypeSource
    TVFromModParam (ModTParam -> Name
    mtpName ModTParam
    mtp)
                            , tvarSource :: Range
    tvarSource = Name -> Range
    nameLoc (ModTParam -> Name
    mtpName ModTParam
    mtp)
                            }

    -- | A value parameter of a module.
    data ModVParam = ModVParam
      { ModVParam -> Name
    mvpName   :: Name
      , ModVParam -> Schema
    mvpType   :: Schema
      , ModVParam -> Maybe Text
    mvpDoc    :: Maybe Text
      , ModVParam -> Maybe Fixity
    mvpFixity :: Maybe Fixity       -- XXX: This should be in the name?
      } deriving (Int -> ModVParam -> ShowS
    [ModVParam] -> ShowS
    ModVParam -> [Char]
    (Int -> ModVParam -> ShowS)
    -> (ModVParam -> [Char])
    -> ([ModVParam] -> ShowS)
    -> Show ModVParam
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ModVParam -> ShowS
    showsPrec :: Int -> ModVParam -> ShowS
    $cshow :: ModVParam -> [Char]
    show :: ModVParam -> [Char]
    $cshowList :: [ModVParam] -> ShowS
    showList :: [ModVParam] -> ShowS
    Show,(forall x. ModVParam -> Rep ModVParam x)
    -> (forall x. Rep ModVParam x -> ModVParam) -> Generic ModVParam
    forall x. Rep ModVParam x -> ModVParam
    forall x. ModVParam -> Rep ModVParam x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ModVParam -> Rep ModVParam x
    from :: forall x. ModVParam -> Rep ModVParam x
    $cto :: forall x. Rep ModVParam x -> ModVParam
    to :: forall x. Rep ModVParam x -> ModVParam
    Generic,ModVParam -> ()
    (ModVParam -> ()) -> NFData ModVParam
    forall a. (a -> ()) -> NFData a
    $crnf :: ModVParam -> ()
    rnf :: ModVParam -> ()
    NFData)
    --------------------------------------------------------------------------------

    -- | 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
    $c== :: Schema -> Schema -> Bool
    == :: Schema -> Schema -> Bool
    $c/= :: Schema -> Schema -> Bool
    /= :: Schema -> Schema -> Bool
    Eq, Int -> Schema -> ShowS
    [Schema] -> ShowS
    Schema -> [Char]
    (Int -> Schema -> ShowS)
    -> (Schema -> [Char]) -> ([Schema] -> ShowS) -> Show Schema
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Schema -> ShowS
    showsPrec :: Int -> Schema -> ShowS
    $cshow :: Schema -> [Char]
    show :: Schema -> [Char]
    $cshowList :: [Schema] -> ShowS
    showList :: [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
    $cfrom :: forall x. Schema -> Rep Schema x
    from :: forall x. Schema -> Rep Schema x
    $cto :: forall x. Rep Schema x -> Schema
    to :: forall x. Rep Schema x -> Schema
    Generic, Schema -> ()
    (Schema -> ()) -> NFData Schema
    forall a. (a -> ()) -> NFData a
    $crnf :: Schema -> ()
    rnf :: 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
    $cfrom :: forall x. TParam -> Rep TParam x
    from :: forall x. TParam -> Rep TParam x
    $cto :: forall x. Rep TParam x -> TParam
    to :: forall x. Rep TParam x -> TParam
    Generic, TParam -> ()
    (TParam -> ()) -> NFData TParam
    forall a. (a -> ()) -> NFData a
    $crnf :: TParam -> ()
    rnf :: TParam -> ()
    NFData, Int -> TParam -> ShowS
    [TParam] -> ShowS
    TParam -> [Char]
    (Int -> TParam -> ShowS)
    -> (TParam -> [Char]) -> ([TParam] -> ShowS) -> Show TParam
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TParam -> ShowS
    showsPrec :: Int -> TParam -> ShowS
    $cshow :: TParam -> [Char]
    show :: TParam -> [Char]
    $cshowList :: [TParam] -> ShowS
    showList :: [TParam] -> ShowS
    Show)

    data TPFlavor = TPModParam Name
                  | TPUnifyVar
                  | TPSchemaParam Name
                  | TPTySynParam Name
                  | TPPropSynParam Name
                  | TPNewtypeParam Name
                  | TPPrimParam 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
    $cfrom :: forall x. TPFlavor -> Rep TPFlavor x
    from :: forall x. TPFlavor -> Rep TPFlavor x
    $cto :: forall x. Rep TPFlavor x -> TPFlavor
    to :: forall x. Rep TPFlavor x -> TPFlavor
    Generic, TPFlavor -> ()
    (TPFlavor -> ()) -> NFData TPFlavor
    forall a. (a -> ()) -> NFData a
    $crnf :: TPFlavor -> ()
    rnf :: TPFlavor -> ()
    NFData, Int -> TPFlavor -> ShowS
    [TPFlavor] -> ShowS
    TPFlavor -> [Char]
    (Int -> TPFlavor -> ShowS)
    -> (TPFlavor -> [Char]) -> ([TPFlavor] -> ShowS) -> Show TPFlavor
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TPFlavor -> ShowS
    showsPrec :: Int -> TPFlavor -> ShowS
    $cshow :: TPFlavor -> [Char]
    show :: TPFlavor -> [Char]
    $cshowList :: [TPFlavor] -> ShowS
    showList :: [TPFlavor] -> ShowS
    Show)

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

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

    schemaParam :: Name -> TPFlavor
    schemaParam :: Name -> TPFlavor
    schemaParam = Name -> TPFlavor
    TPSchemaParam

    tySynParam :: Name -> TPFlavor
    tySynParam :: Name -> TPFlavor
    tySynParam = Name -> TPFlavor
    TPTySynParam

    propSynParam :: Name -> TPFlavor
    propSynParam :: Name -> TPFlavor
    propSynParam = Name -> TPFlavor
    TPPropSynParam

    newtypeParam :: Name -> TPFlavor
    newtypeParam :: Name -> TPFlavor
    newtypeParam = Name -> TPFlavor
    TPNewtypeParam

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

    tpfName :: TPFlavor -> Maybe Name
    tpfName :: TPFlavor -> Maybe Name
    tpfName TPFlavor
    f =
      case TPFlavor
    f of
        TPFlavor
    TPUnifyVar       -> Maybe Name
    forall a. Maybe a
    Nothing
        TPModParam Name
    x     -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TPSchemaParam Name
    x  -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TPTySynParam Name
    x   -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TPPropSynParam Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TPNewtypeParam Name
    x -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x
        TPPrimParam Name
    x    -> Name -> Maybe Name
    forall a. a -> Maybe a
    Just 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 !(RecordMap Ident Type)
                  -- ^ Record type

                | TNewtype !Newtype ![Type]
                  -- ^ A newtype

                  deriving (Int -> Prop -> ShowS
    [Prop] -> ShowS
    Prop -> [Char]
    (Int -> Prop -> ShowS)
    -> (Prop -> [Char]) -> ([Prop] -> ShowS) -> Show Prop
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Prop -> ShowS
    showsPrec :: Int -> Prop -> ShowS
    $cshow :: Prop -> [Char]
    show :: Prop -> [Char]
    $cshowList :: [Prop] -> ShowS
    showList :: [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
    $cfrom :: forall x. Prop -> Rep Prop x
    from :: forall x. Prop -> Rep Prop x
    $cto :: forall x. Rep Prop x -> Prop
    to :: forall x. Rep Prop x -> Prop
    Generic, Prop -> ()
    (Prop -> ()) -> NFData Prop
    forall a. (a -> ()) -> NFData a
    $crnf :: Prop -> ()
    rnf :: 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 info for nicer warnings/errors.

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

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

    tvUnique :: TVar -> Int
    tvUnique :: TVar -> Int
    tvUnique (TVFree Int
    u Kind
    _ Set TParam
    _ TVarInfo
    _) = Int
    u
    tvUnique (TVBound TParam { tpUnique :: TParam -> Int
    tpUnique = Int
    u }) = Int
    u

    data TVarInfo = TVarInfo { TVarInfo -> Range
    tvarSource :: !Range -- ^ Source code that gave rise
                             , TVarInfo -> TypeSource
    tvarDesc   :: !TypeSource -- ^ Description
                             }
                  deriving (Int -> TVarInfo -> ShowS
    [TVarInfo] -> ShowS
    TVarInfo -> [Char]
    (Int -> TVarInfo -> ShowS)
    -> (TVarInfo -> [Char]) -> ([TVarInfo] -> ShowS) -> Show TVarInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TVarInfo -> ShowS
    showsPrec :: Int -> TVarInfo -> ShowS
    $cshow :: TVarInfo -> [Char]
    show :: TVarInfo -> [Char]
    $cshowList :: [TVarInfo] -> ShowS
    showList :: [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
    $cfrom :: forall x. TVarInfo -> Rep TVarInfo x
    from :: forall x. TVarInfo -> Rep TVarInfo x
    $cto :: forall x. Rep TVarInfo x -> TVarInfo
    to :: forall x. Rep TVarInfo x -> TVarInfo
    Generic, TVarInfo -> ()
    (TVarInfo -> ()) -> NFData TVarInfo
    forall a. (a -> ()) -> NFData a
    $crnf :: TVarInfo -> ()
    rnf :: TVarInfo -> ()
    NFData)

    -- | Explains how this type came to be, for better error messages.
    data TypeSource = 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 ArgDescr
                    | TypeOfRes
                    | FunApp
                    | TypeOfIfCondExpr
                    | TypeFromUserAnnotation
                    | GeneratorOfListComp
                    | TypeErrorPlaceHolder
                      deriving (Int -> TypeSource -> ShowS
    [TypeSource] -> ShowS
    TypeSource -> [Char]
    (Int -> TypeSource -> ShowS)
    -> (TypeSource -> [Char])
    -> ([TypeSource] -> ShowS)
    -> Show TypeSource
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TypeSource -> ShowS
    showsPrec :: Int -> TypeSource -> ShowS
    $cshow :: TypeSource -> [Char]
    show :: TypeSource -> [Char]
    $cshowList :: [TypeSource] -> ShowS
    showList :: [TypeSource] -> ShowS
    Show, (forall x. TypeSource -> Rep TypeSource x)
    -> (forall x. Rep TypeSource x -> TypeSource) -> Generic TypeSource
    forall x. Rep TypeSource x -> TypeSource
    forall x. TypeSource -> Rep TypeSource x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TypeSource -> Rep TypeSource x
    from :: forall x. TypeSource -> Rep TypeSource x
    $cto :: forall x. Rep TypeSource x -> TypeSource
    to :: forall x. Rep TypeSource x -> TypeSource
    Generic, TypeSource -> ()
    (TypeSource -> ()) -> NFData TypeSource
    forall a. (a -> ()) -> NFData a
    $crnf :: TypeSource -> ()
    rnf :: TypeSource -> ()
    NFData)

    data ArgDescr = ArgDescr
      { ArgDescr -> Maybe Name
    argDescrFun    :: Maybe Name
      , ArgDescr -> Maybe Int
    argDescrNumber :: Maybe Int
      }
      deriving (Int -> ArgDescr -> ShowS
    [ArgDescr] -> ShowS
    ArgDescr -> [Char]
    (Int -> ArgDescr -> ShowS)
    -> (ArgDescr -> [Char]) -> ([ArgDescr] -> ShowS) -> Show ArgDescr
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ArgDescr -> ShowS
    showsPrec :: Int -> ArgDescr -> ShowS
    $cshow :: ArgDescr -> [Char]
    show :: ArgDescr -> [Char]
    $cshowList :: [ArgDescr] -> ShowS
    showList :: [ArgDescr] -> ShowS
    Show,(forall x. ArgDescr -> Rep ArgDescr x)
    -> (forall x. Rep ArgDescr x -> ArgDescr) -> Generic ArgDescr
    forall x. Rep ArgDescr x -> ArgDescr
    forall x. ArgDescr -> Rep ArgDescr x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ArgDescr -> Rep ArgDescr x
    from :: forall x. ArgDescr -> Rep ArgDescr x
    $cto :: forall x. Rep ArgDescr x -> ArgDescr
    to :: forall x. Rep ArgDescr x -> ArgDescr
    Generic,ArgDescr -> ()
    (ArgDescr -> ()) -> NFData ArgDescr
    forall a. (a -> ()) -> NFData a
    $crnf :: ArgDescr -> ()
    rnf :: ArgDescr -> ()
    NFData)

    noArgDescr :: ArgDescr
    noArgDescr :: ArgDescr
    noArgDescr = ArgDescr { argDescrFun :: Maybe Name
    argDescrFun = Maybe Name
    forall a. Maybe a
    Nothing, argDescrNumber :: Maybe Int
    argDescrNumber = Maybe Int
    forall a. Maybe a
    Nothing }

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

    -- | A type annotated with information on how it came about.
    data TypeWithSource = WithSource
      { TypeWithSource -> Prop
    twsType   :: Type
      , TypeWithSource -> TypeSource
    twsSource :: TypeSource
      , TypeWithSource -> Maybe Range
    twsRange  :: !(Maybe Range)
      }

    -- | 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 Text
    tsDoc         :: !(Maybe Text) -- ^ Documentation
                        }
                  deriving (Int -> TySyn -> ShowS
    [TySyn] -> ShowS
    TySyn -> [Char]
    (Int -> TySyn -> ShowS)
    -> (TySyn -> [Char]) -> ([TySyn] -> ShowS) -> Show TySyn
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TySyn -> ShowS
    showsPrec :: Int -> TySyn -> ShowS
    $cshow :: TySyn -> [Char]
    show :: TySyn -> [Char]
    $cshowList :: [TySyn] -> ShowS
    showList :: [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
    $cfrom :: forall x. TySyn -> Rep TySyn x
    from :: forall x. TySyn -> Rep TySyn x
    $cto :: forall x. Rep TySyn x -> TySyn
    to :: forall x. Rep TySyn x -> TySyn
    Generic, TySyn -> ()
    (TySyn -> ()) -> NFData TySyn
    forall a. (a -> ()) -> NFData a
    $crnf :: TySyn -> ()
    rnf :: TySyn -> ()
    NFData)

    -- | Named records
    data Newtype  = Newtype { Newtype -> Name
    ntName   :: Name
                            , Newtype -> [TParam]
    ntParams :: [TParam]
                            , Newtype -> [Prop]
    ntConstraints :: [Prop]
                            , Newtype -> Name
    ntConName :: !Name
                            , Newtype -> RecordMap Ident Prop
    ntFields :: RecordMap Ident Type
                            , Newtype -> Maybe Text
    ntDoc :: Maybe Text
                            } deriving (Int -> Newtype -> ShowS
    [Newtype] -> ShowS
    Newtype -> [Char]
    (Int -> Newtype -> ShowS)
    -> (Newtype -> [Char]) -> ([Newtype] -> ShowS) -> Show Newtype
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Newtype -> ShowS
    showsPrec :: Int -> Newtype -> ShowS
    $cshow :: Newtype -> [Char]
    show :: Newtype -> [Char]
    $cshowList :: [Newtype] -> ShowS
    showList :: [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
    $cfrom :: forall x. Newtype -> Rep Newtype x
    from :: forall x. Newtype -> Rep Newtype x
    $cto :: forall x. Rep Newtype x -> Newtype
    to :: forall x. Rep Newtype x -> Newtype
    Generic, Newtype -> ()
    (Newtype -> ()) -> NFData Newtype
    forall a. (a -> ()) -> NFData a
    $crnf :: Newtype -> ()
    rnf :: Newtype -> ()
    NFData)

    instance Eq Newtype where
      Newtype
    x == :: Newtype -> Newtype -> Bool
    == Newtype
    y = Newtype -> Name
    ntName Newtype
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Newtype -> Name
    ntName Newtype
    y

    instance Ord Newtype where
      compare :: Newtype -> Newtype -> Ordering
    compare Newtype
    x Newtype
    y = Name -> Name -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Newtype -> Name
    ntName Newtype
    x) (Newtype -> Name
    ntName Newtype
    y)

    -- | 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 Text
    atDoc     :: Maybe Text
      } deriving (Int -> AbstractType -> ShowS
    [AbstractType] -> ShowS
    AbstractType -> [Char]
    (Int -> AbstractType -> ShowS)
    -> (AbstractType -> [Char])
    -> ([AbstractType] -> ShowS)
    -> Show AbstractType
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> AbstractType -> ShowS
    showsPrec :: Int -> AbstractType -> ShowS
    $cshow :: AbstractType -> [Char]
    show :: AbstractType -> [Char]
    $cshowList :: [AbstractType] -> ShowS
    showList :: [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
    $cfrom :: forall x. AbstractType -> Rep AbstractType x
    from :: forall x. AbstractType -> Rep AbstractType x
    $cto :: forall x. Rep AbstractType x -> AbstractType
    to :: forall x. Rep AbstractType x -> AbstractType
    Generic, AbstractType -> ()
    (AbstractType -> ()) -> NFData AbstractType
    forall a. (a -> ()) -> NFData a
    $crnf :: AbstractType -> ()
    rnf :: AbstractType -> ()
    NFData)

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

    instance HasKind AbstractType where
      kindOf :: AbstractType -> Kind
    kindOf AbstractType
    at = (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
    (:->) (AbstractType -> Kind
    atKind AbstractType
    at) ((TParam -> Kind) -> [TParam] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf (([TParam], [Prop]) -> [TParam]
    forall a b. (a, b) -> a
    fst (AbstractType -> ([TParam], [Prop])
    atCtrs AbstractType
    at)))

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

    instance HasKind Type where
      kindOf :: Prop -> Kind
    kindOf Prop
    ty =
        case Prop
    ty of
          TVar TVar
    a      -> TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TVar
    a
          TCon TCon
    c [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 Name
    _ [Prop]
    _ Prop
    t -> Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Prop
    t
          TRec {}     -> Kind
    KType
          TNewtype{}  -> Kind
    KType

    instance HasKind TySyn where
      kindOf :: TySyn -> Kind
    kindOf TySyn
    ts = (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
    (:->) (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 Newtype
    nt = (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 ((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 TParam
    p = TParam -> Kind
    tpKind TParam
    p

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

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

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

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

      TCon TCon
    x [Prop]
    xs == TCon TCon
    y [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 TVar
    x    == TVar TVar
    y     = TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    y
      TRec RecordMap Ident Prop
    xs   == TRec RecordMap Ident Prop
    ys    = RecordMap Ident Prop
    xs RecordMap Ident Prop -> RecordMap Ident Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    == RecordMap Ident Prop
    ys
      TNewtype Newtype
    ntx [Prop]
    xs == TNewtype Newtype
    nty [Prop]
    ys = Newtype
    ntx Newtype -> Newtype -> Bool
    forall a. Eq a => a -> a -> Bool
    == Newtype
    nty Bool -> Bool -> Bool
    && [Prop]
    xs [Prop] -> [Prop] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Prop]
    ys

      Prop
    _         == Prop
    _          = Bool
    False

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

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

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

          (TRec RecordMap Ident Prop
    xs, TRec RecordMap Ident Prop
    ys)      -> RecordMap Ident Prop -> RecordMap Ident Prop -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare RecordMap Ident Prop
    xs RecordMap Ident Prop
    ys
          (TRec{}, Prop
    _)             -> Ordering
    LT
          (Prop
    _, TRec{})             -> Ordering
    GT

          (TNewtype Newtype
    x [Prop]
    xs, TNewtype Newtype
    y [Prop]
    ys) -> (Newtype, [Prop]) -> (Newtype, [Prop]) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Newtype
    x,[Prop]
    xs) (Newtype
    y,[Prop]
    ys)

    instance Eq TParam where
      TParam
    x == :: TParam -> TParam -> Bool
    == 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 TParam
    x 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 TParam
    p = TParam -> TVar
    TVBound TParam
    p

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

    --------------------------------------------------------------------
    -- Superclass

    -- | Compute the set of all @Prop@s that are implied by the
    --   given prop via superclass constraints.
    superclassSet :: Prop -> Set Prop

    superclassSet :: Prop -> Set Prop
    superclassSet (TCon (PC PC
    PPrime) [Prop
    n]) =
      [Prop] -> Set Prop
    forall a. Ord a => [a] -> Set a
    Set.fromList [ Prop -> Prop
    pFin Prop
    n, Prop
    n Prop -> Prop -> Prop
    >== Prop
    tTwo ]

    superclassSet (TCon (PC PC
    p0) [Prop
    t]) = PC -> Set Prop
    go PC
    p0
      where
      super :: PC -> Set Prop
    super PC
    p = Prop -> Set Prop -> Set Prop
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    p) [Prop
    t]) (PC -> Set Prop
    go PC
    p)

      go :: PC -> Set Prop
    go PC
    PRing      = PC -> Set Prop
    super PC
    PZero
      go PC
    PLogic     = PC -> Set Prop
    super PC
    PZero
      go PC
    PField     = PC -> Set Prop
    super PC
    PRing
      go PC
    PIntegral  = PC -> Set Prop
    super PC
    PRing
      go PC
    PRound     = PC -> Set Prop
    super PC
    PField Set Prop -> Set Prop -> Set Prop
    forall a. Semigroup a => a -> a -> a
    <> PC -> Set Prop
    super PC
    PCmp
      go PC
    PCmp       = PC -> Set Prop
    super PC
    PEq
      go PC
    PSignedCmp = PC -> Set Prop
    super PC
    PEq
      go PC
    _ = Set Prop
    forall a. Monoid a => a
    mempty

    superclassSet Prop
    _ = Set Prop
    forall a. Monoid a => a
    mempty

    newtypeConType :: Newtype -> Schema
    newtypeConType :: Newtype -> Schema
    newtypeConType 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
    $ RecordMap Ident Prop -> Prop
    TRec (Newtype -> RecordMap Ident Prop
    ntFields Newtype
    nt) Prop -> Prop -> Prop
    `tFun` Newtype -> [Prop] -> Prop
    TNewtype 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 AbstractType
    at =
      case Name -> Maybe TCon
    builtInType (AbstractType -> Name
    atName AbstractType
    at) of
        Just TCon
    tcon
          | TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tcon Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == AbstractType -> Kind
    atKind AbstractType
    at -> TCon
    tcon
          | Bool
    otherwise ->
            [Char] -> [[Char]] -> TCon
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "abstractTypeTC"
              [ [Char]
    "Mismatch between built-in and declared type."
              , [Char]
    "Name: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Name -> [Char]
    forall a. PP a => a -> [Char]
    pretty (AbstractType -> Name
    atName AbstractType
    at)
              , [Char]
    "Declared: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> [Char]
    forall a. PP a => a -> [Char]
    pretty (AbstractType -> Kind
    atKind AbstractType
    at)
              , [Char]
    "Built-in: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> [Char]
    forall a. PP a => a -> [Char]
    pretty (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tcon)
              ]
        Maybe 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 TParam
    x       == :: TVar -> TVar -> Bool
    == TVBound TParam
    y       = TParam
    x TParam -> TParam -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam
    y
      TVFree  Int
    x Kind
    _ Set TParam
    _ TVarInfo
    _ == TVFree  Int
    y Kind
    _ Set TParam
    _ TVarInfo
    _ = Int
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    y
      TVar
    _             == TVar
    _              = Bool
    False

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

      compare (TVBound TParam
    x) (TVBound 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 TVar
    _           = Bool
    False

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

    tIsError :: Type -> Maybe Type
    tIsError :: Prop -> Maybe Prop
    tIsError Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                    TCon (TError Kind
    _) [Prop
    t] -> Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t
                    TCon (TError Kind
    _) [Prop]
    _   -> [Char] -> [[Char]] -> Maybe Prop
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "tIsError" [[Char]
    "Malformed error"]
                    Prop
    _                   -> Maybe Prop
    forall a. Maybe a
    Nothing

    tHasErrors :: Type -> Bool
    tHasErrors :: Prop -> Bool
    tHasErrors Prop
    ty =
      case Prop -> Prop
    tNoUser Prop
    ty of
        TCon (TError Kind
    _) [Prop]
    _   -> Bool
    True
        TCon TCon
    _ [Prop]
    ts           -> (Prop -> Bool) -> [Prop] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Prop -> Bool
    tHasErrors [Prop]
    ts
        TRec RecordMap Ident Prop
    mp             -> (Prop -> Bool) -> RecordMap Ident Prop -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Prop -> Bool
    tHasErrors RecordMap Ident Prop
    mp
        Prop
    _                   -> Bool
    False

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

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

    tIsInf :: Type -> Bool
    tIsInf :: Prop -> Bool
    tIsInf 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 Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                  TVar TVar
    x -> TVar -> Maybe TVar
    forall a. a -> Maybe a
    Just TVar
    x
                  Prop
    _      -> Maybe TVar
    forall a. Maybe a
    Nothing

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

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

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

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

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

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

    tIsFloat :: Type -> Maybe (Type, Type)
    tIsFloat :: Prop -> Maybe (Prop, Prop)
    tIsFloat Prop
    ty =
      case Prop -> Prop
    tNoUser Prop
    ty of
        TCon (TC TC
    TCFloat) [Prop
    e, Prop
    p] -> (Prop, Prop) -> Maybe (Prop, Prop)
    forall a. a -> Maybe a
    Just (Prop
    e, Prop
    p)
        Prop
    _                        -> Maybe (Prop, Prop)
    forall a. Maybe a
    Nothing

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

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

    tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
    tIsBinFun :: TFun -> Prop -> Maybe (Prop, Prop)
    tIsBinFun TFun
    f Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of
                       TCon (TF TFun
    g) [Prop
    a,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)
                       Prop
    _                          -> 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 TFun
    f Prop
    t0 = Prop -> [Prop] -> [Prop]
    go Prop
    t0 []
      where go :: Prop -> [Prop] -> [Prop]
    go Prop
    ty [Prop]
    xs = case TFun -> Prop -> Maybe (Prop, Prop)
    tIsBinFun TFun
    f Prop
    ty of
                         Just (Prop
    a,Prop
    b) -> Prop -> [Prop] -> [Prop]
    go Prop
    a (Prop -> [Prop] -> [Prop]
    go Prop
    b [Prop]
    xs)
                         Maybe (Prop, Prop)
    Nothing    -> Prop
    ty Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : [Prop]
    xs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    tNum     :: Integral a => a -> Type
    tNum :: forall a. Integral a => a -> Prop
    tNum 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 (Int
    0 :: Int)

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

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

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

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

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

    tNewtype :: Newtype -> [Type] -> Type
    tNewtype :: Newtype -> [Prop] -> Prop
    tNewtype Newtype
    nt [Prop]
    ts = Newtype -> [Prop] -> Prop
    TNewtype Newtype
    nt [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) []

    tRational :: Type
    tRational :: Prop
    tRational  = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCRational) []

    tFloat   :: Type -> Type -> Type
    tFloat :: Prop -> Prop -> Prop
    tFloat Prop
    e Prop
    p = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCFloat) [ Prop
    e, Prop
    p ]

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

    tArray :: Type -> Type -> Type
    tArray :: Prop -> Prop -> Prop
    tArray Prop
    a Prop
    b = TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCArray) [Prop
    a, Prop
    b]

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

    tSeq     :: Type -> Type -> Type
    tSeq :: Prop -> Prop -> Prop
    tSeq Prop
    a 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 (Int
    8 :: Int))

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

    tRec     :: RecordMap Ident Type -> Type
    tRec :: RecordMap Ident Prop -> Prop
    tRec      = RecordMap Ident Prop -> Prop
    TRec

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

    -- | Make a function type.
    tFun     :: Type -> Type -> Type
    tFun :: Prop -> Prop -> Prop
    tFun Prop
    a 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 Prop
    t = case Prop
    t of
                  TUser Name
    _ [Prop]
    _ Prop
    a -> Prop -> Prop
    tNoUser Prop
    a
                  Prop
    _           -> Prop
    t

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

    -- | Make an error value of the given type to replace
    -- the given malformed type (the argument to the error function)
    tError :: Type -> Type
    tError :: Prop -> Prop
    tError Prop
    t = TCon -> [Prop] -> Prop
    TCon (Kind -> TCon
    TError (Kind
    k Kind -> Kind -> Kind
    :-> Kind
    k)) [Prop
    t]
      where k :: Kind
    k = Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Prop
    t

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

    tf2 :: TFun -> Type -> Type -> Type
    tf2 :: TFun -> Prop -> Prop -> Prop
    tf2 TFun
    f Prop
    x 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 TFun
    f Prop
    x Prop
    y 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
    Prop
    x =#= :: Prop -> Prop -> Prop
    =#= Prop
    y = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PEqual) [Prop
    x,Prop
    y]

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

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

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

    pRing :: Type -> Prop
    pRing :: Prop -> Prop
    pRing Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PRing) [Prop
    t]

    pIntegral :: Type -> Prop
    pIntegral :: Prop -> Prop
    pIntegral Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PIntegral) [Prop
    t]

    pField :: Type -> Prop
    pField :: Prop -> Prop
    pField Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PField) [Prop
    t]

    pRound :: Type -> Prop
    pRound :: Prop -> Prop
    pRound Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PRound) [Prop
    t]

    pEq :: Type -> Prop
    pEq :: Prop -> Prop
    pEq Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PEq) [Prop
    t]

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

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

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

    pLiteralLessThan :: Type -> Type -> Prop
    pLiteralLessThan :: Prop -> Prop -> Prop
    pLiteralLessThan Prop
    x Prop
    y = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PLiteralLessThan) [Prop
    x, Prop
    y]

    -- | Make a greater-than-or-equal-to constraint.
    (>==) :: Type -> Type -> Prop
    Prop
    x >== :: Prop -> Prop -> Prop
    >== 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 Selector
    l Prop
    ty 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 [Prop
    x]      = Prop
    x
    pAnd (Prop
    x : [Prop]
    xs)
      | Just Prop
    _ <- Prop -> Maybe Prop
    tIsError Prop
    x    = Prop
    x
      | Prop -> Bool
    pIsTrue Prop
    x               = Prop
    rest
      | Just Prop
    _ <- Prop -> Maybe Prop
    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 Prop
    p0 = [Prop] -> [Prop]
    go [Prop
    p0]
      where
      go :: [Prop] -> [Prop]
    go [] = []
      go (Prop
    q : [Prop]
    qs) =
        case Prop -> Prop
    tNoUser Prop
    q of
          TCon (PC PC
    PAnd) [Prop
    l,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 PC
    PTrue) [Prop]
    _    -> [Prop] -> [Prop]
    go [Prop]
    qs
          Prop
    _                    -> Prop
    q Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : [Prop] -> [Prop]
    go [Prop]
    qs

    pFin :: Type -> Prop
    pFin :: Prop -> Prop
    pFin Prop
    ty =
      case Prop -> Prop
    tNoUser Prop
    ty of
        TCon (TC (TCNum Integer
    _)) [Prop]
    _ -> Prop
    pTrue
        TCon (TC TC
    TCInf)     [Prop]
    _ -> Prop -> Prop
    tError Prop
    prop -- XXX: should we be doing this here??
        Prop
    _                     -> Prop
    prop
      where
      prop :: Prop
    prop = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PFin) [Prop
    ty]

    pValidFloat :: Type -> Type -> Type
    pValidFloat :: Prop -> Prop -> Prop
    pValidFloat Prop
    e Prop
    p = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PValidFloat) [Prop
    e,Prop
    p]

    pPrime :: Type -> Prop
    pPrime :: Prop -> Prop
    pPrime Prop
    ty =
      case Prop -> Prop
    tNoUser Prop
    ty of
        TCon (TC TC
    TCInf) [Prop]
    _ -> Prop -> Prop
    tError Prop
    prop
        Prop
    _ -> Prop
    prop
      where
      prop :: Prop
    prop = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PPrime) [Prop
    ty]

    -- Negation --------------------------------------------------------------------

    {-| `pNegNumeric` negates a simple (i.e., not And, not prime, etc) prop
    over numeric type vars.  The result is a conjunction of properties.  -}
    pNegNumeric :: Prop -> [Prop]
    pNegNumeric :: Prop -> [Prop]
    pNegNumeric Prop
    prop =
      case Prop -> Prop
    tNoUser Prop
    prop of
        TCon TCon
    tcon [Prop]
    tys ->
          case TCon
    tcon of
            PC PC
    pc ->
              case PC
    pc of

                -- not (x == y)  <=>  x /= y
                PC
    PEqual -> [TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PNeq) [Prop]
    tys]

                -- not (x /= y)  <=>  x == y
                PC
    PNeq -> [TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PEqual) [Prop]
    tys]

                -- not (x >= y)  <=>  x /= y and y >= x
                PC
    PGeq -> [TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PNeq) [Prop]
    tys, TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PGeq) ([Prop] -> [Prop]
    forall a. [a] -> [a]
    reverse [Prop]
    tys)]

                -- not (fin x)  <=>  x == Inf
                PC
    PFin | [Prop
    ty] <- [Prop]
    tys -> [Prop
    ty Prop -> Prop -> Prop
    =#= Prop
    tInf]
                     | Bool
    otherwise -> [Prop]
    forall {a}. a
    bad

                -- not True  <=>  0 == 1
                PC
    PTrue -> [TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PEqual) [Prop
    tZero, Prop
    tOne]]

                PC
    _ -> [Prop]
    forall {a}. a
    bad

            TError Kind
    _ki -> [Prop
    prop] -- propogates `TError`

            TC TC
    _tc -> [Prop]
    forall {a}. a
    bad
            TF TFun
    _tf -> [Prop]
    forall {a}. a
    bad

        Prop
    _ -> [Prop]
    forall {a}. a
    bad

      where
      bad :: a
    bad = [Char] -> [[Char]] -> a
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "pNegNumeric"
              [ [Char]
    "Unexpeceted numeric constraint:"
              , Prop -> [Char]
    forall a. PP a => a -> [Char]
    pretty Prop
    prop
              ]

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

    noFreeVariables :: FVS t => t -> Bool
    noFreeVariables :: forall t. FVS t => 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

    freeParams :: FVS t => t -> Set TParam
    freeParams :: forall t. FVS t => t -> Set TParam
    freeParams t
    x = [Set TParam] -> Set TParam
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ((TVar -> Set TParam) -> [TVar] -> [Set TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map TVar -> Set TParam
    params (Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList (t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs t
    x)))
      where
        params :: TVar -> Set TParam
    params (TVFree Int
    _ Kind
    _ Set TParam
    tps TVarInfo
    _) = Set TParam
    tps
        params (TVBound TParam
    tp) = TParam -> Set TParam
    forall a. a -> Set a
    Set.singleton TParam
    tp

    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 Prop
    ty =
          case Prop
    ty of
            TCon TCon
    _ [Prop]
    ts   -> [Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Prop]
    ts
            TVar TVar
    x      -> TVar -> Set TVar
    forall a. a -> Set a
    Set.singleton TVar
    x
            TUser Name
    _ [Prop]
    _ Prop
    t -> Prop -> Set TVar
    go Prop
    t
            TRec RecordMap Ident Prop
    fs     -> [Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (RecordMap Ident Prop -> [Prop]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Prop
    fs)
            TNewtype Newtype
    _nt [Prop]
    ts -> [Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Prop]
    ts

    -- | Find the abstract types mentioned in a type.
    class FreeAbstract t where
      freeAbstract :: t -> Set UserTC

    instance FreeAbstract a => FreeAbstract [a] where
      freeAbstract :: [a] -> Set UserTC
    freeAbstract = [Set UserTC] -> Set UserTC
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set UserTC] -> Set UserTC)
    -> ([a] -> [Set UserTC]) -> [a] -> Set UserTC
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Set UserTC) -> [a] -> [Set UserTC]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract

    instance (FreeAbstract a, FreeAbstract b) => FreeAbstract (a,b) where
      freeAbstract :: (a, b) -> Set UserTC
    freeAbstract (a
    a,b
    b) = Set UserTC -> Set UserTC -> Set UserTC
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (a -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract a
    a) (b -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract b
    b)

    instance FreeAbstract TCon where
      freeAbstract :: TCon -> Set UserTC
    freeAbstract TCon
    tc =
        case TCon
    tc of
          TC (TCAbstract UserTC
    ut) -> UserTC -> Set UserTC
    forall a. a -> Set a
    Set.singleton UserTC
    ut
          TCon
    _                  -> Set UserTC
    forall a. Set a
    Set.empty

    instance FreeAbstract Type where
      freeAbstract :: Prop -> Set UserTC
    freeAbstract Prop
    ty =
        case Prop
    ty of
          TCon TCon
    tc [Prop]
    ts      -> (TCon, [Prop]) -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract (TCon
    tc,[Prop]
    ts)
          TVar {}         -> Set UserTC
    forall a. Set a
    Set.empty
          TUser Name
    _ [Prop]
    _ Prop
    t     -> Prop -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract Prop
    t
          TRec RecordMap Ident Prop
    fs         -> [Prop] -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract (RecordMap Ident Prop -> [Prop]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Prop
    fs)
          TNewtype Newtype
    _nt [Prop]
    ts -> [Prop] -> Set UserTC
    forall t. FreeAbstract t => t -> Set UserTC
    freeAbstract [Prop]
    ts

    instance FVS a => FVS (Maybe a) where
      fvs :: Maybe a -> Set TVar
    fvs Maybe a
    Nothing  = Set TVar
    forall a. Set a
    Set.empty
      fvs (Just 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 [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 (a
    x,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 [TParam]
    as [Prop]
    ps 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 Int
    _ (WithNames TParam
    p 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 [TParam]
    as NameMap
    ns = ((Int, [Char]) -> NameMap -> NameMap)
    -> NameMap -> [(Int, [Char])] -> NameMap
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Int -> [Char] -> NameMap -> NameMap)
    -> (Int, [Char]) -> NameMap -> NameMap
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Int -> [Char] -> NameMap -> NameMap
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert) NameMap
    ns
                    ([(Int, [Char])] -> NameMap) -> [(Int, [Char])] -> NameMap
    forall a b. (a -> b) -> a -> b
    $ [(Int, [Char])]
    named [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [[Char]] -> [(Int, [Char])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    unnamed_nums [[Char]]
    numNames
                            [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [[Char]] -> [(Int, [Char])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    unnamed_vals [[Char]]
    valNames

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

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

            named :: [(Int, [Char])]
    named        = [ (Int
    u,Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n)) | (Int
    u,Just Name
    n,Kind
    _)  <- (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               | (Int
    u,Maybe Name
    Nothing,Kind
    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               | (Int
    u,Maybe Name
    Nothing,Kind
    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 :: [[Char]]
    used    = ((Int, [Char]) -> [Char]) -> [(Int, [Char])] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd [(Int, [Char])]
    named [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ NameMap -> [[Char]]
    forall a. IntMap a -> [a]
    IntMap.elems NameMap
    ns

    ppNewtypeShort :: Newtype -> Doc
    ppNewtypeShort :: Newtype -> Doc
    ppNewtypeShort Newtype
    nt =
      [Char] -> Doc
    text [Char]
    "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 Int
    9) [TParam]
    ps)
      where
      ps :: [TParam]
    ps  = Newtype -> [TParam]
    ntParams Newtype
    nt
      nm :: NameMap
    nm = [TParam] -> NameMap -> NameMap
    addTNames [TParam]
    ps NameMap
    emptyNameMap

    ppNewtypeFull :: Newtype -> Doc
    ppNewtypeFull :: Newtype -> Doc
    ppNewtypeFull Newtype
    nt =
      [Char] -> Doc
    text [Char]
    "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 Int
    9) [TParam]
    ps)
      Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    2 (Doc
    cs Doc -> Doc -> Doc
    $$ (Doc
    "=" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp (Newtype -> Name
    ntConName Newtype
    nt) Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    2 Doc
    fs))
      where
      ps :: [TParam]
    ps = Newtype -> [TParam]
    ntParams Newtype
    nt
      nm :: NameMap
    nm = [TParam] -> NameMap -> NameMap
    addTNames [TParam]
    ps NameMap
    emptyNameMap
      fs :: Doc
    fs = [Doc] -> Doc
    vcat [ Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    f Doc -> Doc -> Doc
    <.> Doc
    ":" Doc -> Doc -> Doc
    <+> Prop -> Doc
    forall a. PP a => a -> Doc
    pp Prop
    t | (Ident
    f,Prop
    t) <- RecordMap Ident Prop -> [(Ident, Prop)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields (Newtype -> RecordMap Ident Prop
    ntFields Newtype
    nt) ]
      cs :: Doc
    cs = [Doc] -> Doc
    vcat ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Doc
    forall a. PP a => a -> Doc
    pp (Newtype -> [Prop]
    ntConstraints Newtype
    nt))

    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 Int
    _ (WithNames Schema
    s NameMap
    ns)
        | [TParam] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Schema -> [TParam]
    sVars Schema
    s) Bool -> Bool -> Bool
    && [Prop] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Schema -> [Prop]
    sProps Schema
    s) = Doc
    body
        | Bool
    otherwise = Int -> Doc -> Doc
    nest Int
    2 ([Doc] -> Doc
    sep ([Doc]
    vars [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    props [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [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
          [] -> []
          [TParam]
    vs -> [Int -> Doc -> Doc
    nest Int
    1 (Doc -> Doc
    braces ([Doc] -> Doc
    commaSepFill ((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
          [] -> []
          [Prop]
    ps -> [Int -> Doc -> Doc
    nest Int
    1 (Doc -> Doc
    parens ([Doc] -> Doc
    commaSepFill ((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
    <+> [Char] -> Doc
    text [Char]
    "=>"]

        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 Int
    _ (WithNames TySyn
    ts NameMap
    ns) =
        Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep
          [ [Doc] -> Doc
    fsep ([[Char] -> Doc
    text [Char]
    "type"] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    ctr [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    lhs [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char -> Doc
    char Char
    '='])
          , 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
                      Kind
    KProp -> [[Char] -> Doc
    text [Char]
    "constraint"]
                      Kind
    _     -> []
              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 Fixity
    _, [TParam
    x, TParam
    y]) ->
                        [NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 TParam
    x, Ident -> Doc
    forall a. PP a => a -> Doc
    pp (Name -> Ident
    nameIdent Name
    n), NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 TParam
    y]
                      (Maybe Fixity
    _, [TParam]
    ps) ->
                        [Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (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 Int
    _  (WithNames Newtype
    nt NameMap
    _) = Newtype -> Doc
    ppNewtypeShort Newtype
    nt -- XXX: do the full thing?

    -- | The precedence levels used by this pretty-printing instance
    -- correspond with parser non-terminals as follows:
    --
    --   * 0-1: @type@
    --
    --   * 2: @infix_type@
    --
    --   * 3: @app_type@
    --
    --   * 4: @dimensions atype@
    --
    --   * 5: @atype@
    instance PP (WithNames Type) where
      ppPrec :: Int -> WithNames Prop -> Doc
    ppPrec Int
    prec ty0 :: WithNames Prop
    ty0@(WithNames Prop
    ty NameMap
    nmMap) =
        case Prop
    ty of
          TVar TVar
    a  -> NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nmMap TVar
    a
          TNewtype Newtype
    nt [Prop]
    ts -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep (Name -> Doc
    forall a. PP a => a -> Doc
    pp (Newtype -> Name
    ntName Newtype
    nt) Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5) [Prop]
    ts)
          TRec RecordMap Ident Prop
    fs -> [Doc] -> Doc
    ppRecord
                        [ Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    l Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    ":" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t | (Ident
    l,Prop
    t) <- RecordMap Ident Prop -> [(Ident, Prop)]
    forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
    displayFields RecordMap Ident Prop
    fs ]

          Prop
    _ | Just 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
    > Int
    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 Int
    2 WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
    isTInfix Infix Ident (WithNames Prop)
    tinf

          TUser Name
    c [Prop]
    ts Prop
    t ->
            (NameDisp -> Doc) -> Doc
    withNameDisp ((NameDisp -> Doc) -> Doc) -> (NameDisp -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ \NameDisp
    disp ->
            case Name -> Maybe OrigName
    asOrigName Name
    c of
              Just OrigName
    og | NameFormat
    NotInScope <- OrigName -> NameDisp -> NameFormat
    getNameFormat OrigName
    og NameDisp
    disp ->
                  Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    prec Prop
    t -- unfold type synonym if not in scope
              Maybe OrigName
    _ ->
                case [Prop]
    ts of
                  [] -> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    c
                  [Prop]
    _ -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    c Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5) [Prop]
    ts)

          TCon (TC TC
    tc) [Prop]
    ts ->
            case (TC
    tc,[Prop]
    ts) of
              (TCNum Integer
    n, [])       -> Integer -> Doc
    integer Integer
    n
              (TC
    TCInf,   [])       -> [Char] -> Doc
    text [Char]
    "inf"
              (TC
    TCBit,   [])       -> [Char] -> Doc
    text [Char]
    "Bit"
              (TC
    TCInteger, [])     -> [Char] -> Doc
    text [Char]
    "Integer"
              (TC
    TCRational, [])    -> [Char] -> Doc
    text [Char]
    "Rational"

              (TC
    TCIntMod, [Prop
    n])     -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    text [Char]
    "Z" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5 Prop
    n

              (TC
    TCSeq,   [Prop
    t1,TCon (TC TC
    TCBit) []]) -> Doc -> Doc
    brackets (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t1)
              (TC
    TCSeq,   [Prop
    t1,Prop
    t2])  -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    4)
                                  (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 Int
    0 Prop
    t1) Doc -> Doc -> Doc
    <.> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    4 Prop
    t2

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

              (TCTuple Int
    _, [Prop]
    fs)     -> [Doc] -> Doc
    ppTuple ([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 Int
    0) [Prop]
    fs

              (TC
    _, [Prop]
    _)              -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep (TC -> Doc
    forall a. PP a => a -> Doc
    pp TC
    tc Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5) [Prop]
    ts))

          TCon (PC PC
    pc) [Prop]
    ts ->
            case (PC
    pc,[Prop]
    ts) of
              (PC
    PEqual, [Prop
    t1,Prop
    t2])   -> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t1 Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    "==" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t2
              (PC
    PNeq ,  [Prop
    t1,Prop
    t2])   -> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t1 Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    "!=" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t2
              (PC
    PGeq,  [Prop
    t1,Prop
    t2])    -> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t1 Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    ">=" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t2
              (PC
    PFin,  [Prop
    t1])       -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    text [Char]
    "fin" Doc -> Doc -> Doc
    <+> (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5 Prop
    t1)
              (PC
    PPrime,  [Prop
    t1])     -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    text [Char]
    "prime" Doc -> Doc -> Doc
    <+> (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5 Prop
    t1)
              (PHas Selector
    x, [Prop
    t1,Prop
    t2])   -> Selector -> Doc
    ppSelector Selector
    x Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    "of"
                                   Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t1 Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    "is" Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0 Prop
    t2
              (PC
    PAnd, [Prop
    t1,Prop
    t2])     -> Int -> Doc -> Doc
    nest Int
    1 (Doc -> Doc
    parens ([Doc] -> Doc
    commaSepFill ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    0) (Prop
    t1 Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : Prop -> [Prop]
    pSplitAnd Prop
    t2))))

              (PC
    PRing, [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 Int
    5 Prop
    t1
              (PC
    PField, [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 Int
    5 Prop
    t1
              (PC
    PIntegral, [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 Int
    5 Prop
    t1
              (PC
    PRound, [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 Int
    5 Prop
    t1

              (PC
    PCmp, [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 Int
    5 Prop
    t1
              (PC
    PSignedCmp, [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 Int
    5 Prop
    t1
              (PC
    PLiteral, [Prop
    t1,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 Int
    5 Prop
    t1 Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5 Prop
    t2
              (PC
    PLiteralLessThan, [Prop
    t1,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 Int
    5 Prop
    t1 Doc -> Doc -> Doc
    <+> Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5 Prop
    t2

              (PC
    _, [Prop]
    _)              -> Bool -> Doc -> Doc
    optParens (Int
    prec Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    3) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep (PC -> Doc
    forall a. PP a => a -> Doc
    pp PC
    pc Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Prop -> Doc
    forall {a}. PP (WithNames a) => Int -> a -> Doc
    go Int
    5) [Prop]
    ts)

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

        where
        go :: Int -> a -> Doc
    go Int
    p 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 TCon
    tc [Prop
    ieLeft',Prop
    ieRight']) NameMap
    _) =
          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
             (Ident
    ieOp, Fixity
    ieFixity) <- TCon -> Maybe (Ident, Fixity)
    infixPrimTy TCon
    tc
             Infix Ident (WithNames Prop)
    -> Maybe (Infix Ident (WithNames Prop))
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Infix { Fixity
    Ident
    WithNames Prop
    ieLeft :: WithNames Prop
    ieRight :: WithNames Prop
    ieOp :: Ident
    ieFixity :: Fixity
    ieOp :: Ident
    ieLeft :: WithNames Prop
    ieRight :: WithNames Prop
    ieFixity :: Fixity
    .. }

        isTInfix (WithNames (TUser Name
    n [Prop
    ieLeft',Prop
    ieRight'] Prop
    _) NameMap
    _)
          | Ident -> Bool
    isInfixIdent (Name -> Ident
    nameIdent Name
    n) =
          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
                 ieFixity :: Fixity
    ieFixity = Fixity -> Maybe Fixity -> Fixity
    forall a. a -> Maybe a -> a
    fromMaybe Fixity
    defaultFixity (Name -> Maybe Fixity
    nameFixity Name
    n)
                 ieOp :: Ident
    ieOp     = Name -> Ident
    nameIdent Name
    n
             Infix Ident (WithNames Prop)
    -> Maybe (Infix Ident (WithNames Prop))
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Infix { Fixity
    Ident
    WithNames Prop
    ieOp :: Ident
    ieLeft :: WithNames Prop
    ieRight :: WithNames Prop
    ieFixity :: Fixity
    ieLeft :: WithNames Prop
    ieRight :: WithNames Prop
    ieFixity :: Fixity
    ieOp :: Ident
    .. }

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

    instance PP (WithNames TVar) where

      ppPrec :: Int -> WithNames TVar -> Doc
    ppPrec Int
    _ (WithNames TVar
    tv NameMap
    mp) =
        case TVar
    tv of
          TVBound {} -> Doc
    nmTxt
          TVFree {} -> Doc
    "?" Doc -> Doc -> Doc
    <.> Doc
    nmTxt
        where
        nmTxt :: Doc
    nmTxt
          | Just [Char]
    a <- Int -> NameMap -> Maybe [Char]
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup (TVar -> Int
    tvUnique TVar
    tv) NameMap
    mp = [Char] -> Doc
    text [Char]
    a
          | Bool
    otherwise =
              case TVar
    tv of
                TVBound TParam
    x ->
                  let declNm :: a -> Doc
    declNm a
    n = a -> Doc
    forall a. PP a => a -> Doc
    pp a
    n Doc -> Doc -> Doc
    <.> Doc
    "`" Doc -> Doc -> Doc
    <.> Int -> Doc
    int (TParam -> Int
    tpUnique TParam
    x) in
                  case TParam -> TPFlavor
    tpFlav TParam
    x of
                    TPModParam Name
    n     -> Name -> Doc
    forall a. PPName a => a -> Doc
    ppPrefixName Name
    n
                    TPFlavor
    TPUnifyVar       -> Kind -> TypeSource -> Int -> Doc
    pickTVarName (TParam -> Kind
    tpKind TParam
    x) (TVarInfo -> TypeSource
    tvarDesc (TParam -> TVarInfo
    tpInfo TParam
    x)) (TParam -> Int
    tpUnique TParam
    x)
                    TPSchemaParam Name
    n  -> Name -> Doc
    forall a. PP a => a -> Doc
    declNm Name
    n
                    TPTySynParam Name
    n   -> Name -> Doc
    forall a. PP a => a -> Doc
    declNm Name
    n
                    TPPropSynParam Name
    n -> Name -> Doc
    forall a. PP a => a -> Doc
    declNm Name
    n
                    TPNewtypeParam Name
    n -> Name -> Doc
    forall a. PP a => a -> Doc
    declNm Name
    n
                    TPPrimParam Name
    n    -> Name -> Doc
    forall a. PP a => a -> Doc
    declNm Name
    n

                TVFree Int
    x Kind
    k Set TParam
    _ TVarInfo
    d -> Kind -> TypeSource -> Int -> Doc
    pickTVarName Kind
    k (TVarInfo -> TypeSource
    tvarDesc TVarInfo
    d) Int
    x

    pickTVarName :: Kind -> TypeSource -> Int -> Doc
    pickTVarName :: Kind -> TypeSource -> Int -> Doc
    pickTVarName Kind
    k TypeSource
    src Int
    uni =
      [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $
      case TypeSource
    src of
        TVFromModParam Name
    n       -> Name -> [Char]
    forall a. PP a => a -> [Char]
    using Name
    n
        TVFromSignature Name
    n      -> Name -> [Char]
    forall a. PP a => a -> [Char]
    using Name
    n
        TypeSource
    TypeWildCard           -> ShowS
    mk ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ case Kind
    k of
                                         Kind
    KNum -> [Char]
    "n"
                                         Kind
    _    -> [Char]
    "a"
        TypeOfRecordField Ident
    i    -> Ident -> [Char]
    forall a. PP a => a -> [Char]
    using Ident
    i
        TypeOfTupleField Int
    n     -> ShowS
    mk ([Char]
    "tup_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)
        TypeSource
    TypeOfSeqElement       -> ShowS
    mk [Char]
    "a"
        TypeSource
    LenOfSeq               -> ShowS
    mk [Char]
    "n"
        TypeParamInstNamed Name
    _ Ident
    i -> Ident -> [Char]
    forall a. PP a => a -> [Char]
    using Ident
    i
        TypeParamInstPos Name
    f Int
    n   -> ShowS
    mk (Name -> [Char]
    forall a. PP a => a -> [Char]
    sh Name
    f [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)
        DefinitionOf Name
    x ->
          case Name -> NameInfo
    nameInfo Name
    x of
            GlobalName NameSource
    SystemName OrigName
    og
              | OrigName -> ModPath
    ogModule OrigName
    og ModPath -> ModPath -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName -> ModPath
    TopModule ModName
    exprModName -> ShowS
    mk [Char]
    "it"
            NameInfo
    _ -> Name -> [Char]
    forall a. PP a => a -> [Char]
    using Name
    x
        TypeSource
    LenOfCompGen           -> ShowS
    mk [Char]
    "n"
        TypeSource
    GeneratorOfListComp    -> [Char]
    "seq"
        TypeSource
    TypeOfIfCondExpr       -> [Char]
    "b"
        TypeOfArg ArgDescr
    ad           -> ShowS
    mk (case ArgDescr -> Maybe Int
    argDescrNumber ArgDescr
    ad of
                                        Maybe Int
    Nothing -> [Char]
    "arg"
                                        Just Int
    n  -> [Char]
    "arg_" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)
        TypeSource
    TypeOfRes              -> [Char]
    "res"
        TypeSource
    FunApp                 -> [Char]
    "fun"
        TypeSource
    TypeFromUserAnnotation -> [Char]
    "user"
        TypeSource
    TypeErrorPlaceHolder   -> [Char]
    "err"
      where
      sh :: a -> [Char]
    sh a
    a      = Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (a -> Doc
    forall a. PP a => a -> Doc
    pp a
    a)
      using :: a -> [Char]
    using a
    a   = ShowS
    mk (a -> [Char]
    forall a. PP a => a -> [Char]
    sh a
    a)
      mk :: ShowS
    mk [Char]
    a      = [Char]
    a [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "`" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    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 Int
    n 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 Int
    _ TVarInfo
    tvinfo = [Doc] -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp (TVarInfo -> TypeSource
    tvarDesc TVarInfo
    tvinfo)] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    loc
        where
        loc :: [Doc]
    loc = if Range
    rng Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    emptyRange then [] else [Doc
    "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 ArgDescr where
      ppPrec :: Int -> ArgDescr -> Doc
    ppPrec Int
    _ ArgDescr
    ad = [Doc] -> Doc
    hsep ([Doc
    which, Doc
    "argument"] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    ofFun)
            where
            which :: Doc
    which = Doc -> (Int -> Doc) -> Maybe Int -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    "function" Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal (ArgDescr -> Maybe Int
    argDescrNumber ArgDescr
    ad)
            ofFun :: [Doc]
    ofFun = case ArgDescr -> Maybe Name
    argDescrFun ArgDescr
    ad of
                      Maybe Name
    Nothing -> []
                      Just Name
    f  -> [Doc
    "of" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f]

    instance PP TypeSource where
      ppPrec :: Int -> TypeSource -> Doc
    ppPrec Int
    _ TypeSource
    tvsrc =
        case TypeSource
    tvsrc of
          TVFromModParam Name
    m    -> Doc
    "module parameter" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    m
          TVFromSignature Name
    x   -> Doc
    "signature variable" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x)
          TypeSource
    TypeWildCard        -> Doc
    "type wildcard (_)"
          TypeOfRecordField Ident
    l -> Doc
    "type of field" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    l)
          TypeOfTupleField Int
    n  -> Doc
    "type of" Doc -> Doc -> Doc
    <+> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    n Doc -> Doc -> Doc
    <+> Doc
    "tuple field"
          TypeSource
    TypeOfSeqElement    -> Doc
    "type of sequence member"
          TypeSource
    LenOfSeq            -> Doc
    "length of sequence"
          TypeParamInstNamed Name
    f Ident
    i -> Doc
    "type argument" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i) Doc -> Doc -> Doc
    <+>
                                              Doc
    "of" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f)
          TypeParamInstPos   Name
    f Int
    i -> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    i Doc -> Doc -> Doc
    <+> Doc
    "type argument of" Doc -> Doc -> Doc
    <+>
                                                          Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f)
          DefinitionOf Name
    x      -> Doc
    "the type of" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x)
          TypeSource
    LenOfCompGen        -> Doc
    "length of comprehension generator"
          TypeOfArg ArgDescr
    ad        -> Doc
    "type of" Doc -> Doc -> Doc
    <+> ArgDescr -> Doc
    forall a. PP a => a -> Doc
    pp ArgDescr
    ad
          TypeSource
    TypeOfRes             -> Doc
    "type of function result"
          TypeSource
    TypeOfIfCondExpr      -> Doc
    "type of `if` condition"
          TypeSource
    TypeFromUserAnnotation -> Doc
    "user annotation"
          TypeSource
    GeneratorOfListComp    -> Doc
    "generator in a list comprehension"
          TypeSource
    FunApp                -> Doc
    "function call"
          TypeSource
    TypeErrorPlaceHolder  -> Doc
    "type error place-holder"

    instance PP ModParamNames where
      ppPrec :: Int -> ModParamNames -> Doc
    ppPrec Int
    _ ModParamNames
    ps =
        let tps :: [ModTParam]
    tps = Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems (ModParamNames -> Map Name ModTParam
    mpnTypes ModParamNames
    ps)
        in
        [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (ModTParam -> Doc) -> [ModTParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> Doc
    forall a. PP a => a -> Doc
    pp [ModTParam]
    tps [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
              if [Located Prop] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (ModParamNames -> [Located Prop]
    mpnConstraints ModParamNames
    ps) then [] else
                [ Doc
    "type constraint" Doc -> Doc -> Doc
    <+>
                    Doc -> Doc
    parens ([Doc] -> Doc
    commaSep ((Located Prop -> Doc) -> [Located Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Prop -> Doc
    forall a. PP a => a -> Doc
    pp (Prop -> Doc) -> (Located Prop -> Prop) -> Located Prop -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Located Prop -> Prop
    forall a. Located a -> a
    thing) (ModParamNames -> [Located Prop]
    mpnConstraints ModParamNames
    ps)))
                ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
               [ TySyn -> Doc
    forall a. PP a => a -> Doc
    pp TySyn
    t | TySyn
    t <- Map Name TySyn -> [TySyn]
    forall k a. Map k a -> [a]
    Map.elems (ModParamNames -> Map Name TySyn
    mpnTySyn ModParamNames
    ps) ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
               (ModVParam -> Doc) -> [ModVParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ModVParam -> Doc
    forall a. PP a => a -> Doc
    pp (Map Name ModVParam -> [ModVParam]
    forall k a. Map k a -> [a]
    Map.elems (ModParamNames -> Map Name ModVParam
    mpnFuns ModParamNames
    ps))

    instance PP ModTParam where
      ppPrec :: Int -> ModTParam -> Doc
    ppPrec Int
    _ ModTParam
    p =
        Doc
    "type" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp (ModTParam -> Name
    mtpName ModTParam
    p) Doc -> Doc -> Doc
    <+> Doc
    ":" Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp (ModTParam -> Kind
    mtpKind ModTParam
    p)

    instance PP ModVParam where
      ppPrec :: Int -> ModVParam -> Doc
    ppPrec Int
    _ ModVParam
    p = Name -> Doc
    forall a. PP a => a -> Doc
    pp (ModVParam -> Name
    mvpName ModVParam
    p) Doc -> Doc -> Doc
    <+> Doc
    ":" Doc -> Doc -> Doc
    <+> Schema -> Doc
    forall a. PP a => a -> Doc
    pp (ModVParam -> Schema
    mvpType ModVParam
    p)