    {-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
    {-# Language OverloadedStrings #-}
    {-# Language Safe #-}
    -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    module Cryptol.TypeCheck.Error where

    import qualified Data.IntMap as IntMap
    import qualified Data.Set as Set
    import Control.DeepSeq(NFData)
    import GHC.Generics(Generic)
    import Data.List((\\),sortBy,groupBy,partition)
    import Data.Function(on)

    import Cryptol.Utils.Ident(Ident,Namespace(..))
    import qualified Cryptol.Parser.AST as P
    import Cryptol.Parser.Position(Located(..), Range(..), rangeWithin)
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.InferTypes
    import Cryptol.TypeCheck.Subst
    import Cryptol.TypeCheck.Unify(Path,isRootPath)
    import Cryptol.TypeCheck.FFI.Error
    import Cryptol.ModuleSystem.Name(Name)
    import Cryptol.Utils.RecordMap

    cleanupErrors :: [(Range,Error)] -> [(Range,Error)]
    cleanupErrors :: [(Range, Error)] -> [(Range, Error)]
    cleanupErrors = [(Range, Error)] -> [(Range, Error)]
    dropErrorsFromSameLoc
                  ([(Range, Error)] -> [(Range, Error)])
    -> ([(Range, Error)] -> [(Range, Error)])
    -> [(Range, Error)]
    -> [(Range, Error)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Range, Error) -> (Range, Error) -> Ordering)
    -> [(Range, Error)] -> [(Range, Error)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy ((FilePath, Position, Position)
    -> (FilePath, Position, Position) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ((FilePath, Position, Position)
     -> (FilePath, Position, Position) -> Ordering)
    -> ((Range, Error) -> (FilePath, Position, Position))
    -> (Range, Error)
    -> (Range, Error)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Range -> (FilePath, Position, Position)
    cmpR (Range -> (FilePath, Position, Position))
    -> ((Range, Error) -> Range)
    -> (Range, Error)
    -> (FilePath, Position, Position)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Range, Error) -> Range
    forall a b. (a, b) -> a
    fst))    -- order errors
                  ([(Range, Error)] -> [(Range, Error)])
    -> ([(Range, Error)] -> [(Range, Error)])
    -> [(Range, Error)]
    -> [(Range, Error)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Range, Error)] -> [(Range, Error)] -> [(Range, Error)]
    dropSubsumed []
      where

      -- pick shortest error from each location.
      dropErrorsFromSameLoc :: [(Range, Error)] -> [(Range, Error)]
    dropErrorsFromSameLoc = ([(Range, Error)] -> [(Range, Error)])
    -> [[(Range, Error)]] -> [(Range, Error)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap [(Range, Error)] -> [(Range, Error)]
    forall {a}. [(a, Error)] -> [(a, Error)]
    chooseBestError
                            ([[(Range, Error)]] -> [(Range, Error)])
    -> ([(Range, Error)] -> [[(Range, Error)]])
    -> [(Range, Error)]
    -> [(Range, Error)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Range, Error) -> (Range, Error) -> Bool)
    -> [(Range, Error)] -> [[(Range, Error)]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    (==)    (Range -> Range -> Bool)
    -> ((Range, Error) -> Range)
    -> (Range, Error)
    -> (Range, Error)
    -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Range, Error) -> Range
    forall a b. (a, b) -> a
    fst)

      addErrorRating :: (a, Error) -> (Int, (a, Error))
    addErrorRating (a
    r,Error
    e) = (Error -> Int
    errorImportance Error
    e, (a
    r,Error
    e))
      chooseBestError :: [(a, Error)] -> [(a, Error)]
    chooseBestError    = ((Int, (a, Error)) -> (a, Error))
    -> [(Int, (a, Error))] -> [(a, Error)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, (a, Error)) -> (a, Error)
    forall a b. (a, b) -> b
    snd
                         ([(Int, (a, Error))] -> [(a, Error)])
    -> ([(a, Error)] -> [(Int, (a, Error))])
    -> [(a, Error)]
    -> [(a, Error)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[(Int, (a, Error))]] -> [(Int, (a, Error))]
    forall a. HasCallStack => [a] -> a
    head
                         ([[(Int, (a, Error))]] -> [(Int, (a, Error))])
    -> ([(a, Error)] -> [[(Int, (a, Error))]])
    -> [(a, Error)]
    -> [(Int, (a, Error))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Int, (a, Error)) -> (Int, (a, Error)) -> Bool)
    -> [(Int, (a, Error))] -> [[(Int, (a, Error))]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Int -> Int -> Bool)
    -> ((Int, (a, Error)) -> Int)
    -> (Int, (a, Error))
    -> (Int, (a, Error))
    -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Int, (a, Error)) -> Int
    forall a b. (a, b) -> a
    fst)
                         ([(Int, (a, Error))] -> [[(Int, (a, Error))]])
    -> ([(a, Error)] -> [(Int, (a, Error))])
    -> [(a, Error)]
    -> [[(Int, (a, Error))]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Int, (a, Error)) -> (Int, (a, Error)) -> Ordering)
    -> [(Int, (a, Error))] -> [(Int, (a, Error))]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy ((Int -> Int -> Ordering) -> Int -> Int -> Ordering
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> ((Int, (a, Error)) -> Int)
    -> (Int, (a, Error))
    -> (Int, (a, Error))
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Int, (a, Error)) -> Int
    forall a b. (a, b) -> a
    fst)
                         ([(Int, (a, Error))] -> [(Int, (a, Error))])
    -> ([(a, Error)] -> [(Int, (a, Error))])
    -> [(a, Error)]
    -> [(Int, (a, Error))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((a, Error) -> (Int, (a, Error)))
    -> [(a, Error)] -> [(Int, (a, Error))]
    forall a b. (a -> b) -> [a] -> [b]
    map (a, Error) -> (Int, (a, Error))
    forall {a}. (a, Error) -> (Int, (a, Error))
    addErrorRating

      cmpR :: Range -> (FilePath, Position, Position)
    cmpR Range
    r  = ( Range -> FilePath
    source Range
    r    -- First by file
                , Range -> Position
    from Range
    r      -- Then starting position
                , Range -> Position
    to Range
    r        -- Finally end position
                )

      dropSubsumed :: [(Range, Error)] -> [(Range, Error)] -> [(Range, Error)]
    dropSubsumed [(Range, Error)]
    survived [(Range, Error)]
    xs =
        case [(Range, Error)]
    xs of
          (Range, Error)
    err : [(Range, Error)]
    rest ->
             let keep :: (Range, Error) -> Bool
    keep (Range, Error)
    e = Bool -> Bool
    not ((Range, Error) -> (Range, Error) -> Bool
    subsumes (Range, Error)
    err (Range, Error)
    e)
             in [(Range, Error)] -> [(Range, Error)] -> [(Range, Error)]
    dropSubsumed ((Range, Error)
    err (Range, Error) -> [(Range, Error)] -> [(Range, Error)]
    forall a. a -> [a] -> [a]
    : ((Range, Error) -> Bool) -> [(Range, Error)] -> [(Range, Error)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Range, Error) -> Bool
    keep [(Range, Error)]
    survived) (((Range, Error) -> Bool) -> [(Range, Error)] -> [(Range, Error)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Range, Error) -> Bool
    keep [(Range, Error)]
    rest)
          [] -> [(Range, Error)]
    survived

    -- | Should the first error suppress the next one.
    subsumes :: (Range,Error) -> (Range,Error) -> Bool
    subsumes :: (Range, Error) -> (Range, Error) -> Bool
    subsumes (Range
    _,NotForAll TypeSource
    _ Path
    _ TVar
    x Type
    _) (Range
    _,NotForAll TypeSource
    _ Path
    _ TVar
    y Type
    _) = TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    y
    subsumes (Range
    r1,Error
    UnexpectedTypeWildCard) (Range
    r2,UnsupportedFFIType{}) =
      Range
    r1 Range -> Range -> Bool
    `rangeWithin` Range
    r2
    subsumes (Range
    r1,KindMismatch {}) (Range
    r2,Error
    err) =
      case Error
    err of
        KindMismatch {} -> Range
    r1 Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    r2
        Error
    _               -> Bool
    True
    subsumes (Range, Error)
    _ (Range, Error)
    _ = Bool
    False

    data Warning  = DefaultingKind (P.TParam Name) P.Kind
                  | DefaultingWildType P.Kind
                  | DefaultingTo !TVarInfo Type
                  | NonExhaustivePropGuards Name
                    deriving (Int -> Warning -> ShowS
    [Warning] -> ShowS
    Warning -> FilePath
    (Int -> Warning -> ShowS)
    -> (Warning -> FilePath) -> ([Warning] -> ShowS) -> Show Warning
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Warning -> ShowS
    showsPrec :: Int -> Warning -> ShowS
    $cshow :: Warning -> FilePath
    show :: Warning -> FilePath
    $cshowList :: [Warning] -> ShowS
    showList :: [Warning] -> ShowS
    Show, (forall x. Warning -> Rep Warning x)
    -> (forall x. Rep Warning x -> Warning) -> Generic Warning
    forall x. Rep Warning x -> Warning
    forall x. Warning -> Rep Warning x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Warning -> Rep Warning x
    from :: forall x. Warning -> Rep Warning x
    $cto :: forall x. Rep Warning x -> Warning
    to :: forall x. Rep Warning x -> Warning
    Generic, Warning -> ()
    (Warning -> ()) -> NFData Warning
    forall a. (a -> ()) -> NFData a
    $crnf :: Warning -> ()
    rnf :: Warning -> ()
    NFData)

    -- | Various errors that might happen during type checking/inference
    data Error    = KindMismatch (Maybe TypeSource) Kind Kind
                    -- ^ Expected kind, inferred kind

                  | TooManyTypeParams Int Kind
                    -- ^ Number of extra parameters, kind of result
                    -- (which should not be of the form @_ -> _@)

                  | TyVarWithParams
                    -- ^ A type variable was applied to some arguments.

                  | TooManyTySynParams Name Int
                    -- ^ Type-synonym, number of extra params

                  | TooFewTyParams Name Int
                    -- ^ Who is missing params, number of missing params

                  | RecursiveTypeDecls [Name]
                    -- ^ The type synonym declarations are recursive

                  | TypeMismatch TypeSource Path Type Type
                    -- ^ Expected type, inferred type

                  | SchemaMismatch Ident Schema Schema
                    -- ^ Name of module parameter, expected scehema, actual schema.
                    -- This may happen when instantiating modules.

                  | RecursiveType TypeSource Path Type Type
                    -- ^ Unification results in a recursive type

                  | UnsolvedGoals [Goal]
                    -- ^ A constraint that we could not solve, usually because
                    -- there are some left-over variables that we could not infer.

                  | UnsolvableGoals [Goal]
                    -- ^ A constraint that we could not solve and we know
                    -- it is impossible to do it.

                  | UnsolvedDelayedCt DelayedCt
                    -- ^ A constraint (with context) that we could not solve

                  | UnexpectedTypeWildCard
                    -- ^ Type wild cards are not allowed in this context
                    -- (e.g., definitions of type synonyms).

                  | TypeVariableEscaped TypeSource Path Type [TParam]
                    -- ^ Unification variable depends on quantified variables
                    -- that are not in scope.

                  | NotForAll TypeSource Path TVar Type
                    -- ^ Quantified type variables (of kind *) need to
                    -- match the given type, so it does not work for all types.

                  | TooManyPositionalTypeParams
                    -- ^ Too many positional type arguments, in an explicit
                    -- type instantiation

                  | BadParameterKind TParam Kind
                    -- ^ Kind other than `*` or `#` given to parameter of
                    --   type synonym, newtype, function signature, etc.

                  | CannotMixPositionalAndNamedTypeParams

                  | UndefinedTypeParameter (Located Ident)

                  | RepeatedTypeParameter Ident [Range]

                  | AmbiguousSize TVarInfo (Maybe Type)
                    -- ^ Could not determine the value of a numeric type variable,
                    --   but we know it must be at least as large as the given type
                    --   (or unconstrained, if Nothing).

                  | BareTypeApp
                    -- ^ Bare expression of the form `{_}

                  | UndefinedExistVar Name
                  | TypeShadowing String Name String
                  | MissingModTParam (Located Ident)
                  | MissingModVParam (Located Ident)
                  | MissingModParam Ident

                  | FunctorInstanceMissingArgument Ident
                  | FunctorInstanceBadArgument Ident
                  | FunctorInstanceMissingName Namespace Ident
                  | FunctorInstanceBadBacktick BadBacktickInstance

                  | UnsupportedFFIKind TypeSource TParam Kind
                    -- ^ Kind is not supported for FFI
                  | UnsupportedFFIType TypeSource FFITypeError
                    -- ^ Type is not supported for FFI

                  | NestedConstraintGuard Ident
                    -- ^ Constraint guards may only apper at the top-level

                  | DeclarationRequiresSignatureCtrGrd Ident
                    -- ^ All declarataions in a recursive group involving
                    -- constraint guards should have signatures

                  | InvalidConstraintGuard Prop
                    -- ^ The given constraint may not be used as a constraint guard

                  | TemporaryError Doc
                    -- ^ This is for errors that don't fit other cateogories.
                    -- We should not use it much, and is generally to be used
                    -- for transient errors, which are due to incomplete
                    -- implementation.
                    deriving (Int -> Error -> ShowS
    [Error] -> ShowS
    Error -> FilePath
    (Int -> Error -> ShowS)
    -> (Error -> FilePath) -> ([Error] -> ShowS) -> Show Error
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Error -> ShowS
    showsPrec :: Int -> Error -> ShowS
    $cshow :: Error -> FilePath
    show :: Error -> FilePath
    $cshowList :: [Error] -> ShowS
    showList :: [Error] -> ShowS
    Show, (forall x. Error -> Rep Error x)
    -> (forall x. Rep Error x -> Error) -> Generic Error
    forall x. Rep Error x -> Error
    forall x. Error -> Rep Error x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Error -> Rep Error x
    from :: forall x. Error -> Rep Error x
    $cto :: forall x. Rep Error x -> Error
    to :: forall x. Rep Error x -> Error
    Generic, Error -> ()
    (Error -> ()) -> NFData Error
    forall a. (a -> ()) -> NFData a
    $crnf :: Error -> ()
    rnf :: Error -> ()
    NFData)

    data BadBacktickInstance =
        BIPolymorphicArgument Ident Ident
      | BINested [(BIWhat, Name)]
      | BIMultipleParams Ident
        deriving (Int -> BadBacktickInstance -> ShowS
    [BadBacktickInstance] -> ShowS
    BadBacktickInstance -> FilePath
    (Int -> BadBacktickInstance -> ShowS)
    -> (BadBacktickInstance -> FilePath)
    -> ([BadBacktickInstance] -> ShowS)
    -> Show BadBacktickInstance
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> BadBacktickInstance -> ShowS
    showsPrec :: Int -> BadBacktickInstance -> ShowS
    $cshow :: BadBacktickInstance -> FilePath
    show :: BadBacktickInstance -> FilePath
    $cshowList :: [BadBacktickInstance] -> ShowS
    showList :: [BadBacktickInstance] -> ShowS
    Show, (forall x. BadBacktickInstance -> Rep BadBacktickInstance x)
    -> (forall x. Rep BadBacktickInstance x -> BadBacktickInstance)
    -> Generic BadBacktickInstance
    forall x. Rep BadBacktickInstance x -> BadBacktickInstance
    forall x. BadBacktickInstance -> Rep BadBacktickInstance x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. BadBacktickInstance -> Rep BadBacktickInstance x
    from :: forall x. BadBacktickInstance -> Rep BadBacktickInstance x
    $cto :: forall x. Rep BadBacktickInstance x -> BadBacktickInstance
    to :: forall x. Rep BadBacktickInstance x -> BadBacktickInstance
    Generic, BadBacktickInstance -> ()
    (BadBacktickInstance -> ()) -> NFData BadBacktickInstance
    forall a. (a -> ()) -> NFData a
    $crnf :: BadBacktickInstance -> ()
    rnf :: BadBacktickInstance -> ()
    NFData)

    data BIWhat = BIFunctor | BIInterface | BIPrimitive | BIForeign | BIAbstractType
        deriving (Int -> BIWhat -> ShowS
    [BIWhat] -> ShowS
    BIWhat -> FilePath
    (Int -> BIWhat -> ShowS)
    -> (BIWhat -> FilePath) -> ([BIWhat] -> ShowS) -> Show BIWhat
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> BIWhat -> ShowS
    showsPrec :: Int -> BIWhat -> ShowS
    $cshow :: BIWhat -> FilePath
    show :: BIWhat -> FilePath
    $cshowList :: [BIWhat] -> ShowS
    showList :: [BIWhat] -> ShowS
    Show, (forall x. BIWhat -> Rep BIWhat x)
    -> (forall x. Rep BIWhat x -> BIWhat) -> Generic BIWhat
    forall x. Rep BIWhat x -> BIWhat
    forall x. BIWhat -> Rep BIWhat x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. BIWhat -> Rep BIWhat x
    from :: forall x. BIWhat -> Rep BIWhat x
    $cto :: forall x. Rep BIWhat x -> BIWhat
    to :: forall x. Rep BIWhat x -> BIWhat
    Generic, BIWhat -> ()
    (BIWhat -> ()) -> NFData BIWhat
    forall a. (a -> ()) -> NFData a
    $crnf :: BIWhat -> ()
    rnf :: BIWhat -> ()
    NFData)

    -- | When we have multiple errors on the same location, we show only the
    -- ones with the has highest rating according to this function.
    errorImportance :: Error -> Int
    errorImportance :: Error -> Int
    errorImportance Error
    err =
      case Error
    err of
        Error
    BareTypeApp                                      -> Int
    11 -- basically a parse error
        TemporaryError {}                                -> Int
    11
        -- show these as usually means the user used something that doesn't work

        FunctorInstanceMissingArgument {}                 -> Int
    10
        MissingModParam {}                                -> Int
    10
        FunctorInstanceBadArgument {}                     -> Int
    10
        FunctorInstanceMissingName {}                     ->  Int
    9
        FunctorInstanceBadBacktick {}                     ->  Int
    9

        KindMismatch {}                                  -> Int
    10
        TyVarWithParams {}                               -> Int
    9
        TypeMismatch {}                                  -> Int
    8
        SchemaMismatch {}                                -> Int
    7
        RecursiveType {}                                 -> Int
    7
        NotForAll {}                                     -> Int
    6
        TypeVariableEscaped {}                           -> Int
    5

        UndefinedExistVar {}                             -> Int
    10
        TypeShadowing {}                                 -> Int
    2
        MissingModTParam {}                              -> Int
    10
        MissingModVParam {}                              -> Int
    10

        BadParameterKind{}                               -> Int
    9
        CannotMixPositionalAndNamedTypeParams {}         -> Int
    8
        TooManyTypeParams {}                             -> Int
    8
        TooFewTyParams {}                                -> Int
    8
        TooManyPositionalTypeParams {}                   -> Int
    8
        UndefinedTypeParameter {}                        -> Int
    8
        RepeatedTypeParameter {}                         -> Int
    8

        TooManyTySynParams {}                            -> Int
    8
        UnexpectedTypeWildCard {}                        -> Int
    8

        RecursiveTypeDecls {}                            -> Int
    9

        UnsolvableGoals [Goal]
    g
          | (Type -> Bool) -> [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Type -> Bool
    tHasErrors ((Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Type
    goal [Goal]
    g)                  -> Int
    0
          | Bool
    otherwise                                    -> Int
    4

        UnsolvedGoals [Goal]
    g
          | (Type -> Bool) -> [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Type -> Bool
    tHasErrors ((Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Type
    goal [Goal]
    g)                  -> Int
    0
          | Bool
    otherwise                                    -> Int
    4

        UnsolvedDelayedCt DelayedCt
    dt
          | (Type -> Bool) -> [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Type -> Bool
    tHasErrors ((Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Type
    goal (DelayedCt -> [Goal]
    dctGoals DelayedCt
    dt))      -> Int
    0
          | Bool
    otherwise                                    -> Int
    3

        AmbiguousSize {}                                 -> Int
    2

        UnsupportedFFIKind {}                            -> Int
    10
        UnsupportedFFIType {}                            -> Int
    7
        -- less than UnexpectedTypeWildCard

        NestedConstraintGuard {}                         -> Int
    10
        DeclarationRequiresSignatureCtrGrd {}            -> Int
    9
        InvalidConstraintGuard {}                        -> Int
    5

    instance TVars Warning where
      apSubst :: Subst -> Warning -> Warning
    apSubst Subst
    su Warning
    warn =
        case Warning
    warn of
          DefaultingKind {}     -> Warning
    warn
          DefaultingWildType {} -> Warning
    warn
          DefaultingTo TVarInfo
    d Type
    ty     -> TVarInfo -> Type -> Warning
    DefaultingTo TVarInfo
    d (Type -> Warning) -> Type -> Warning
    forall a b. (a -> b) -> a -> b
    $! (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    ty)
          NonExhaustivePropGuards {} -> Warning
    warn

    instance FVS Warning where
      fvs :: Warning -> Set TVar
    fvs Warning
    warn =
        case Warning
    warn of
          DefaultingKind {}     -> Set TVar
    forall a. Set a
    Set.empty
          DefaultingWildType {} -> Set TVar
    forall a. Set a
    Set.empty
          DefaultingTo TVarInfo
    _ Type
    ty     -> Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    ty
          NonExhaustivePropGuards {} -> Set TVar
    forall a. Set a
    Set.empty

    instance TVars Error where
      apSubst :: Subst -> Error -> Error
    apSubst Subst
    su Error
    err =
        case Error
    err of
          KindMismatch {}           -> Error
    err
          TooManyTypeParams {}      -> Error
    err
          Error
    TyVarWithParams           -> Error
    err
          TooManyTySynParams {}     -> Error
    err
          TooFewTyParams {}         -> Error
    err
          RecursiveTypeDecls {}     -> Error
    err
          SchemaMismatch Ident
    i Schema
    t1 Schema
    t2  ->
            Ident -> Schema -> Schema -> Error
    SchemaMismatch Ident
    i (Schema -> Schema -> Error) -> Schema -> Schema -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Schema -> Schema
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Schema
    t1) (Schema -> Error) -> Schema -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Schema -> Schema
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Schema
    t2)
          TypeMismatch TypeSource
    src Path
    pa Type
    t1 Type
    t2 -> TypeSource -> Path -> Type -> Type -> Error
    TypeMismatch TypeSource
    src Path
    pa (Type -> Type -> Error) -> Type -> Type -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t1) (Type -> Error) -> Type -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t2)
          RecursiveType TypeSource
    src Path
    pa Type
    t1 Type
    t2   -> TypeSource -> Path -> Type -> Type -> Error
    RecursiveType TypeSource
    src Path
    pa (Type -> Type -> Error) -> Type -> Type -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t1) (Type -> Error) -> Type -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t2)
          UnsolvedGoals [Goal]
    gs          -> [Goal] -> Error
    UnsolvedGoals ([Goal] -> Error) -> [Goal] -> Error
    forall a b. (a -> b) -> a -> b
    !$ Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Goal]
    gs
          UnsolvableGoals [Goal]
    gs        -> [Goal] -> Error
    UnsolvableGoals ([Goal] -> Error) -> [Goal] -> Error
    forall a b. (a -> b) -> a -> b
    !$ Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Goal]
    gs
          UnsolvedDelayedCt DelayedCt
    g       -> DelayedCt -> Error
    UnsolvedDelayedCt (DelayedCt -> Error) -> DelayedCt -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> DelayedCt -> DelayedCt
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su DelayedCt
    g)
          Error
    UnexpectedTypeWildCard    -> Error
    err
          TypeVariableEscaped TypeSource
    src Path
    pa Type
    t [TParam]
    xs ->
                                     TypeSource -> Path -> Type -> [TParam] -> Error
    TypeVariableEscaped TypeSource
    src Path
    pa (Type -> [TParam] -> Error) -> Type -> [TParam] -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) ([TParam] -> Error) -> [TParam] -> Error
    forall a b. (a -> b) -> a -> b
    .$ [TParam]
    xs
          NotForAll TypeSource
    src Path
    pa TVar
    x Type
    t        -> TypeSource -> Path -> TVar -> Type -> Error
    NotForAll TypeSource
    src Path
    pa TVar
    x (Type -> Error) -> Type -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
          Error
    TooManyPositionalTypeParams -> Error
    err
          Error
    CannotMixPositionalAndNamedTypeParams -> Error
    err

          BadParameterKind{} -> Error
    err
          UndefinedTypeParameter {} -> Error
    err
          RepeatedTypeParameter {} -> Error
    err
          AmbiguousSize TVarInfo
    x Maybe Type
    t -> TVarInfo -> Maybe Type -> Error
    AmbiguousSize TVarInfo
    x (Maybe Type -> Error) -> Maybe Type -> Error
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Maybe Type -> Maybe Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Maybe Type
    t)

          Error
    BareTypeApp -> Error
    err

          UndefinedExistVar {} -> Error
    err
          TypeShadowing {}     -> Error
    err
          MissingModTParam {}  -> Error
    err
          MissingModVParam {}  -> Error
    err
          MissingModParam {}   -> Error
    err

          FunctorInstanceMissingArgument {} -> Error
    err
          FunctorInstanceBadArgument {} -> Error
    err
          FunctorInstanceMissingName {} -> Error
    err
          FunctorInstanceBadBacktick {} -> Error
    err

          UnsupportedFFIKind {}    -> Error
    err
          UnsupportedFFIType TypeSource
    src FFITypeError
    e -> TypeSource -> FFITypeError -> Error
    UnsupportedFFIType TypeSource
    src (FFITypeError -> Error) -> FFITypeError -> Error
    forall a b. (a -> b) -> a -> b
    !$ Subst -> FFITypeError -> FFITypeError
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su FFITypeError
    e

          NestedConstraintGuard {} -> Error
    err
          DeclarationRequiresSignatureCtrGrd {} -> Error
    err
          InvalidConstraintGuard Type
    p -> Type -> Error
    InvalidConstraintGuard (Type -> Error) -> Type -> Error
    forall a b. (a -> b) -> a -> b
    $! Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    p

          TemporaryError {} -> Error
    err

    instance FVS Error where
      fvs :: Error -> Set TVar
    fvs Error
    err =
        case Error
    err of
          KindMismatch {}           -> Set TVar
    forall a. Set a
    Set.empty
          TooManyTypeParams {}      -> Set TVar
    forall a. Set a
    Set.empty
          Error
    TyVarWithParams           -> Set TVar
    forall a. Set a
    Set.empty
          TooManyTySynParams {}     -> Set TVar
    forall a. Set a
    Set.empty
          TooFewTyParams {}         -> Set TVar
    forall a. Set a
    Set.empty
          RecursiveTypeDecls {}     -> Set TVar
    forall a. Set a
    Set.empty
          SchemaMismatch Ident
    _ Schema
    t1 Schema
    t2    -> (Schema, Schema) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Schema
    t1,Schema
    t2)
          TypeMismatch TypeSource
    _ Path
    _ Type
    t1 Type
    t2    -> (Type, Type) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Type
    t1,Type
    t2)
          RecursiveType TypeSource
    _ Path
    _ Type
    t1 Type
    t2   -> (Type, Type) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Type
    t1,Type
    t2)
          UnsolvedGoals [Goal]
    gs          -> [Goal] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Goal]
    gs
          UnsolvableGoals [Goal]
    gs        -> [Goal] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Goal]
    gs
          UnsolvedDelayedCt DelayedCt
    g       -> DelayedCt -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs DelayedCt
    g
          Error
    UnexpectedTypeWildCard    -> Set TVar
    forall a. Set a
    Set.empty
          TypeVariableEscaped TypeSource
    _ Path
    _ Type
    t [TParam]
    xs-> Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    t Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union`
                                                [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
    TVBound [TParam]
    xs)
          NotForAll TypeSource
    _ Path
    _ TVar
    x Type
    t             -> TVar -> Set TVar -> Set TVar
    forall a. Ord a => a -> Set a -> Set a
    Set.insert TVar
    x (Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    t)
          Error
    TooManyPositionalTypeParams -> Set TVar
    forall a. Set a
    Set.empty
          Error
    CannotMixPositionalAndNamedTypeParams -> Set TVar
    forall a. Set a
    Set.empty
          UndefinedTypeParameter {}             -> Set TVar
    forall a. Set a
    Set.empty
          RepeatedTypeParameter {}              -> Set TVar
    forall a. Set a
    Set.empty
          AmbiguousSize TVarInfo
    _ Maybe Type
    t -> Maybe Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Maybe Type
    t
          BadParameterKind TParam
    tp Kind
    _ -> TVar -> Set TVar
    forall a. a -> Set a
    Set.singleton (TParam -> TVar
    TVBound TParam
    tp)

          Error
    BareTypeApp -> Set TVar
    forall a. Set a
    Set.empty

          UndefinedExistVar {} -> Set TVar
    forall a. Set a
    Set.empty
          TypeShadowing {}     -> Set TVar
    forall a. Set a
    Set.empty
          MissingModTParam {}  -> Set TVar
    forall a. Set a
    Set.empty
          MissingModVParam {}  -> Set TVar
    forall a. Set a
    Set.empty
          MissingModParam {}   -> Set TVar
    forall a. Set a
    Set.empty

          FunctorInstanceMissingArgument {} -> Set TVar
    forall a. Set a
    Set.empty
          FunctorInstanceBadArgument {} -> Set TVar
    forall a. Set a
    Set.empty
          FunctorInstanceMissingName {} -> Set TVar
    forall a. Set a
    Set.empty
          FunctorInstanceBadBacktick {} -> Set TVar
    forall a. Set a
    Set.empty

          UnsupportedFFIKind {}  -> Set TVar
    forall a. Set a
    Set.empty
          UnsupportedFFIType TypeSource
    _ FFITypeError
    t -> FFITypeError -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs FFITypeError
    t

          NestedConstraintGuard {} -> Set TVar
    forall a. Set a
    Set.empty
          DeclarationRequiresSignatureCtrGrd {} -> Set TVar
    forall a. Set a
    Set.empty
          InvalidConstraintGuard Type
    p -> Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    p

          TemporaryError {} -> Set TVar
    forall a. Set a
    Set.empty

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

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

    instance PP (WithNames Warning) where
      ppPrec :: Int -> WithNames Warning -> Doc
    ppPrec Int
    _ (WithNames Warning
    warn NameMap
    names) =
        NameMap -> Warning -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Warning
    warn (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
        case Warning
    warn of
          DefaultingKind TParam Name
    x Kind
    k ->
            FilePath -> Doc
    text FilePath
    "Assuming " Doc -> Doc -> Doc
    <+> TParam Name -> Doc
    forall a. PP a => a -> Doc
    pp TParam Name
    x Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    "to have" Doc -> Doc -> Doc
    <+> Kind -> Doc
    P.cppKind Kind
    k

          DefaultingWildType Kind
    k ->
            FilePath -> Doc
    text FilePath
    "Assuming _ to have" Doc -> Doc -> Doc
    <+> Kind -> Doc
    P.cppKind Kind
    k

          DefaultingTo TVarInfo
    d Type
    ty ->
            FilePath -> Doc
    text FilePath
    "Defaulting" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp (TVarInfo -> TypeSource
    tvarDesc TVarInfo
    d) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    "to"
                                                  Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    ty

          NonExhaustivePropGuards Name
    n ->
            FilePath -> Doc
    text FilePath
    "Could not prove that the constraint guards used in defining" Doc -> Doc -> Doc
    <+>
            Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    "were exhaustive."

    instance PP (WithNames Error) where
      ppPrec :: Int -> WithNames Error -> Doc
    ppPrec Int
    _ (WithNames Error
    err NameMap
    names) =
        case Error
    err of

          RecursiveType TypeSource
    src Path
    pa Type
    t1 Type
    t2 ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Matching would result in an infinite type." (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    vcat ( [ Doc
    "The type: " Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t1
                     , Doc
    "occurs in:" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t2
                     ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Path -> [Doc]
    ppCtxt Path
    pa [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
                     [ Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src ] )

          Error
    UnexpectedTypeWildCard ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Wild card types are not allowed in this context" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    vcat [ Doc
    "They cannot be used in:"
                   , [Doc] -> Doc
    bullets [ Doc
    "type synonyms"
                             , Doc
    "FFI declarations"
                             , Doc
    "declarations with constraint guards"
                             ]
                   ]

          KindMismatch Maybe TypeSource
    mbsrc Kind
    k1 Kind
    k2 ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Incorrect type form." (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
             [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
               [ Doc
    "Expected:" Doc -> Doc -> Doc
    <+> Kind -> Doc
    cppKind Kind
    k1
               , Doc
    "Inferred:" Doc -> Doc -> Doc
    <+> Kind -> Doc
    cppKind Kind
    k2
               ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Kind -> Kind -> [Doc]
    kindMismatchHint Kind
    k1 Kind
    k2
                 [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc] -> (TypeSource -> [Doc]) -> Maybe TypeSource -> [Doc]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\TypeSource
    src -> [Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src]) Maybe TypeSource
    mbsrc

          TooManyTypeParams Int
    extra Kind
    k ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Malformed type."
              (Doc
    "Kind" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k) Doc -> Doc -> Doc
    <+> Doc
    "is not a function," Doc -> Doc -> Doc
    $$
               Doc
    "but it was applied to" Doc -> Doc -> Doc
    <+> Int -> FilePath -> Doc
    forall {a}. (Eq a, Num a, Show a) => a -> FilePath -> Doc
    pl Int
    extra FilePath
    "parameter" Doc -> Doc -> Doc
    <.> Doc
    ".")

          Error
    TyVarWithParams ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Malformed type."
                   Doc
    "Type variables cannot be applied to parameters."

          TooManyTySynParams Name
    t Int
    extra ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Malformed type."
              (Doc
    "Type synonym" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    nm Name
    t Doc -> Doc -> Doc
    <+> Doc
    "was applied to" Doc -> Doc -> Doc
    <+>
                Int -> FilePath -> Doc
    forall {a}. (Eq a, Num a, Show a) => a -> FilePath -> Doc
    pl Int
    extra FilePath
    "extra parameters" Doc -> Doc -> Doc
    <.> FilePath -> Doc
    text FilePath
    ".")

          TooFewTyParams Name
    t Int
    few ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Malformed type."
              (Doc
    "Type" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    nm Name
    t Doc -> Doc -> Doc
    <+> Doc
    "is missing" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    few Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    "parameters.")

          RecursiveTypeDecls [Name]
    ts ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Recursive type declarations:"
                   ([Doc] -> Doc
    commaSep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. PP a => a -> Doc
    nm [Name]
    ts)

          TypeMismatch TypeSource
    src Path
    pa Type
    t1 Type
    t2 ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Type mismatch:" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [ Doc
    "Expected type:" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t1
              , Doc
    "Inferred type:" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t2
              ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Type -> Type -> [Doc]
    mismatchHint Type
    t1 Type
    t2
                [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Path -> [Doc]
    ppCtxt Path
    pa
                [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src]

          SchemaMismatch Ident
    i Schema
    t1 Schema
    t2 ->
              NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              Doc -> Doc -> Doc
    nested (Doc
    "Type mismatch in module parameter" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i)) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
                [ Doc
    "Expected type:" Doc -> Doc -> Doc
    <+> NameMap -> Schema -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Schema
    t1
                , Doc
    "Actual type:"   Doc -> Doc -> Doc
    <+> NameMap -> Schema -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Schema
    t2
                ]

          UnsolvableGoals [Goal]
    gs -> NameMap -> [Goal] -> Doc
    explainUnsolvable NameMap
    names [Goal]
    gs

          UnsolvedGoals [Goal]
    gs
            | Bool
    noUni ->
              NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              Doc -> Doc -> Doc
    nested Doc
    "Unsolved constraints:" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    bullets ((Goal -> Doc) -> [Goal] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Goal -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names) [Goal]
    gs)

            | Bool
    otherwise ->
              NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsBefore NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              Doc -> Doc -> Doc
    nested Doc
    "subject to the following constraints:" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    bullets ((Goal -> Doc) -> [Goal] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Goal -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names) [Goal]
    gs)

          UnsolvedDelayedCt DelayedCt
    g
            | Bool
    noUni ->
              NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              Doc -> Doc -> Doc
    nested Doc
    "Failed to validate user-specified signature." (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              NameMap -> DelayedCt -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names DelayedCt
    g
            | Bool
    otherwise ->
              NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsBefore NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              Doc -> Doc -> Doc
    nested Doc
    "while validating user-specified signature" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              NameMap -> DelayedCt -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names DelayedCt
    g

          TypeVariableEscaped TypeSource
    src Path
    pa Type
    t [TParam]
    xs ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested (Doc
    "The type" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t Doc -> Doc -> Doc
    <+>
                                            Doc
    "is not sufficiently polymorphic.") (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    vcat ( [ Doc
    "It cannot depend on quantified variables:" Doc -> Doc -> Doc
    <+>
                           ([Doc] -> Doc
    commaSep ((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
    names) [TParam]
    xs))
                     ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Path -> [Doc]
    ppCtxt Path
    pa
                       [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src ]
                   )

          NotForAll TypeSource
    src Path
    pa TVar
    x Type
    t ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc -> Doc -> Doc
    nested Doc
    "Inferred type is not sufficiently polymorphic." (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              [Doc] -> Doc
    vcat ( [ Doc
    "Quantified variable:" Doc -> Doc -> Doc
    <+> NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names TVar
    x
                     , Doc
    "cannot match type:"   Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t
                     ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Path -> [Doc]
    ppCtxt Path
    pa
                       [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src ]
                   )

          BadParameterKind TParam
    tp Kind
    k ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            [Doc] -> Doc
    vcat [ Doc
    "Illegal kind assigned to type variable:" Doc -> Doc -> Doc
    <+> NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names TParam
    tp
                 , Doc
    "Unexpected:" Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k
                 ]

          Error
    TooManyPositionalTypeParams ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc
    "Too many positional type-parameters in explicit type application."

          Error
    CannotMixPositionalAndNamedTypeParams ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc
    "Named and positional type applications may not be mixed."

          UndefinedTypeParameter Located Ident
    x ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            Doc
    "Undefined type parameter `" Doc -> Doc -> Doc
    <.> Ident -> Doc
    forall a. PP a => a -> Doc
    pp (Located Ident -> Ident
    forall a. Located a -> a
    thing Located Ident
    x) Doc -> Doc -> Doc
    <.> Doc
    "`."
              Doc -> Doc -> Doc
    $$ Doc
    "See" Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp (Located Ident -> Range
    forall a. Located a -> Range
    srcRange Located Ident
    x)

          RepeatedTypeParameter Ident
    x [Range]
    rs ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
              Doc
    "Multiple definitions for type parameter `" Doc -> Doc -> Doc
    <.> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    x Doc -> Doc -> Doc
    <.> Doc
    "`:"
              Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    bullets ((Range -> Doc) -> [Range] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Range -> Doc
    forall a. PP a => a -> Doc
    pp [Range]
    rs)

          AmbiguousSize TVarInfo
    x Maybe Type
    t ->
            let sizeMsg :: [Doc]
    sizeMsg =
                   case Maybe Type
    t of
                     Just Type
    t' -> [Doc
    "Must be at least:" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t']
                     Maybe Type
    Nothing -> []
             in NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err
                  ([Doc] -> Doc
    vcat ([Doc
    "Ambiguous numeric type:" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp (TVarInfo -> TypeSource
    tvarDesc TVarInfo
    x)] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    sizeMsg))

          Error
    BareTypeApp ->
            Doc
    "Unexpected bare type application." Doc -> Doc -> Doc
    $$
            Doc
    "Perhaps you meant `( ... ) instead."

          UndefinedExistVar Name
    x -> Doc
    "Undefined type" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x)
          TypeShadowing FilePath
    this Name
    new FilePath
    that ->
            Doc
    "Type" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    this Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    new) Doc -> Doc -> Doc
    <+>
            Doc
    "shadowing an existing" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    that Doc -> Doc -> Doc
    <+> Doc
    "with the same name."
          MissingModTParam Located Ident
    x ->
            Doc
    "Missing definition for type parameter" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp (Located Ident -> Ident
    forall a. Located a -> a
    thing Located Ident
    x))
          MissingModVParam Located Ident
    x ->
            Doc
    "Missing definition for value parameter" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp (Located Ident -> Ident
    forall a. Located a -> a
    thing Located Ident
    x))

          MissingModParam Ident
    x ->
            Doc
    "Missing module parameter" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    x)

          FunctorInstanceMissingArgument Ident
    i ->
            Doc
    "Missing functor argument" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i)

          FunctorInstanceBadArgument Ident
    i ->
            Doc
    "Functor does not have parameter" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i)

          FunctorInstanceMissingName Namespace
    ns Ident
    i ->
            Doc
    "Functor argument does not define" Doc -> Doc -> Doc
    <+> Doc
    sayNS Doc -> Doc -> Doc
    <+> Doc
    "parameter" Doc -> Doc -> Doc
    <+>
                Doc -> Doc
    quotes (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i)
            where
            sayNS :: Doc
    sayNS =
              case Namespace
    ns of
                  Namespace
    NSValue     -> Doc
    "value"
                  Namespace
    NSType      -> Doc
    "type"
                  Namespace
    NSModule    -> Doc
    "module"

          FunctorInstanceBadBacktick BadBacktickInstance
    bad ->
            case BadBacktickInstance
    bad of
              BIPolymorphicArgument Ident
    i Ident
    x ->
                Doc -> Doc -> Doc
    nested Doc
    "Value parameter may not have a polymorphic type:" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                  [Doc] -> Doc
    bullets
                    [ Doc
    "Module parameter:" Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i
                    , Doc
    "Value parameter:" Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    x
                    , Doc
    "When instantiatiating a functor using parameterization,"
                      Doc -> Doc -> Doc
    $$ Doc
    "the value parameters need to have a simple type."
                    ]

              BINested [(BIWhat, Name)]
    what ->
                Doc -> Doc -> Doc
    nested Doc
    "Invalid declarations in parameterized instantiation:" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                  [Doc] -> Doc
    bullets ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
                    [ Doc
    it Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n
                    | (BIWhat
    w,Name
    n) <- [(BIWhat, Name)]
    what
                    , let it :: Doc
    it = case BIWhat
    w of
                                 BIWhat
    BIFunctor -> Doc
    "functor"
                                 BIWhat
    BIInterface -> Doc
    "interface"
                                 BIWhat
    BIPrimitive -> Doc
    "primitive"
                                 BIWhat
    BIAbstractType -> Doc
    "abstract type"
                                 BIWhat
    BIForeign -> Doc
    "foreign import"
                    ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
                    [ Doc
    "A functor instantiated using parameterization," Doc -> Doc -> Doc
    $$
                      Doc
    "may not contain nested functors, interfaces, or primitives."
                    ]
              BIMultipleParams Ident
    x ->
                Doc -> Doc -> Doc
    nested Doc
    "Repeated parameter name in parameterized instantiation:" (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                  [Doc] -> Doc
    bullets
                    [ Doc
    "Parameter name:" Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    x
                    , Doc
    "Parameterized instantiation requires distinct parameter names"
                    ]

          UnsupportedFFIKind TypeSource
    src TParam
    param Kind
    k ->
            Doc -> Doc -> Doc
    nested Doc
    "Kind of type variable unsupported for FFI: " (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            [Doc] -> Doc
    vcat
              [ TParam -> Doc
    forall a. PP a => a -> Doc
    pp TParam
    param Doc -> Doc -> Doc
    <+> Doc
    colon Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k
              , Doc
    "Only type variables of kind" Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    KNum Doc -> Doc -> Doc
    <+> Doc
    "are supported"
              , Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src ]

          UnsupportedFFIType TypeSource
    src FFITypeError
    t -> [Doc] -> Doc
    vcat
            [ NameMap -> FFITypeError -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names FFITypeError
    t
            , Doc
    "When checking" Doc -> Doc -> Doc
    <+> TypeSource -> Doc
    forall a. PP a => a -> Doc
    pp TypeSource
    src ]

          NestedConstraintGuard Ident
    d ->
            [Doc] -> Doc
    vcat [ Doc
    "Local declaration" Doc -> Doc -> Doc
    <+> Doc -> Doc
    backticks (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    d)
                                       Doc -> Doc -> Doc
    <+> Doc
    "may not use constraint guards."
                 , Doc
    "Constraint guards may only appear at the top-level of a module."
                 ]

          DeclarationRequiresSignatureCtrGrd Ident
    d ->
            [Doc] -> Doc
    vcat [ Doc
    "The declaration of" Doc -> Doc -> Doc
    <+> Doc -> Doc
    backticks (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    d) Doc -> Doc -> Doc
    <+>
                                                Doc
    "requires a full type signature,"
                 , Doc
    "because it is part of a recursive group with constraint guards."
                 ]

          InvalidConstraintGuard Type
    p ->
            let d :: Doc
    d = case Type -> Type
    tNoUser Type
    p of
                      TCon TCon
    tc [Type]
    _ -> TCon -> Doc
    forall a. PP a => a -> Doc
    pp TCon
    tc
                      Type
    _         -> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    p
            in
            [Doc] -> Doc
    vcat [ Doc -> Doc
    backticks Doc
    d Doc -> Doc -> Doc
    <+> Doc
    "may not be used in a constraint guard."
                 , Doc
    "Constraint guards support only numeric comparisons and `fin`."
                 ]

          TemporaryError Doc
    doc -> Doc
    doc
        where
        bullets :: [Doc] -> Doc
    bullets [Doc]
    xs = [Doc] -> Doc
    vcat [ Doc
    "•" Doc -> Doc -> Doc
    <+> Doc
    d | Doc
    d <- [Doc]
    xs ]

        nested :: Doc -> Doc -> Doc
    nested Doc
    x Doc
    y = Int -> Doc -> Doc
    nest Int
    2 (Doc
    x Doc -> Doc -> Doc
    $$ Doc
    y)

        pl :: a -> FilePath -> Doc
    pl a
    1 FilePath
    x     = FilePath -> Doc
    text FilePath
    "1" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    x
        pl a
    n FilePath
    x     = FilePath -> Doc
    text (a -> FilePath
    forall a. Show a => a -> FilePath
    show a
    n) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    x Doc -> Doc -> Doc
    <.> FilePath -> Doc
    text FilePath
    "s"

        nm :: a -> Doc
    nm a
    x       = FilePath -> Doc
    text FilePath
    "`" Doc -> Doc -> Doc
    <.> a -> Doc
    forall a. PP a => a -> Doc
    pp a
    x Doc -> Doc -> Doc
    <.> FilePath -> Doc
    text FilePath
    "`"

        kindMismatchHint :: Kind -> Kind -> [Doc]
    kindMismatchHint Kind
    k1 Kind
    k2 =
          case (Kind
    k1,Kind
    k2) of
            (Kind
    KType,Kind
    KProp) -> [FilePath -> Doc
    text FilePath
    "Possibly due to a missing `=>`"]
            (Kind, Kind)
    _ -> []

        mismatchHint :: Type -> Type -> [Doc]
    mismatchHint (TRec RecordMap Ident Type
    fs1) (TRec RecordMap Ident Type
    fs2) =
          FilePath -> [Ident] -> [Doc]
    forall {a}. PP a => FilePath -> [a] -> [Doc]
    hint FilePath
    "Missing" [Ident]
    missing [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> [Ident] -> [Doc]
    forall {a}. PP a => FilePath -> [a] -> [Doc]
    hint FilePath
    "Unexpected" [Ident]
    extra
          where
            missing :: [Ident]
    missing = RecordMap Ident Type -> [Ident]
    forall a b. RecordMap a b -> [a]
    displayOrder RecordMap Ident Type
    fs1 [Ident] -> [Ident] -> [Ident]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ RecordMap Ident Type -> [Ident]
    forall a b. RecordMap a b -> [a]
    displayOrder RecordMap Ident Type
    fs2
            extra :: [Ident]
    extra   = RecordMap Ident Type -> [Ident]
    forall a b. RecordMap a b -> [a]
    displayOrder RecordMap Ident Type
    fs2 [Ident] -> [Ident] -> [Ident]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ RecordMap Ident Type -> [Ident]
    forall a b. RecordMap a b -> [a]
    displayOrder RecordMap Ident Type
    fs1
            hint :: FilePath -> [a] -> [Doc]
    hint FilePath
    _ []  = []
            hint FilePath
    s [a
    x] = [FilePath -> Doc
    text FilePath
    s Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    "field" Doc -> Doc -> Doc
    <+> a -> Doc
    forall a. PP a => a -> Doc
    pp a
    x]
            hint FilePath
    s [a]
    xs  = [FilePath -> Doc
    text FilePath
    s Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    "fields" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep ((a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. PP a => a -> Doc
    pp [a]
    xs)]
        mismatchHint Type
    _ Type
    _ = []

        noUni :: Bool
    noUni = Set TVar -> Bool
    forall a. Set a -> Bool
    Set.null ((TVar -> Bool) -> Set TVar -> Set TVar
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter TVar -> Bool
    isFreeTV (Error -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Error
    err))

        ppCtxt :: Path -> [Doc]
    ppCtxt Path
    pa = if Path -> Bool
    isRootPath Path
    pa then [] else [ Doc
    "Context:" Doc -> Doc -> Doc
    <+> Path -> Doc
    forall a. PP a => a -> Doc
    pp Path
    pa ]

    explainUnsolvable :: NameMap -> [Goal] -> Doc
    explainUnsolvable :: NameMap -> [Goal] -> Doc
    explainUnsolvable NameMap
    names [Goal]
    gs =
      NameMap -> [Goal] -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names [Goal]
    gs ([Doc] -> Doc
    bullets ((Goal -> Doc) -> [Goal] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Doc
    explain [Goal]
    gs))

      where
      bullets :: [Doc] -> Doc
    bullets [Doc]
    xs = [Doc] -> Doc
    vcat [ Doc
    "•" Doc -> Doc -> Doc
    <+> Doc
    d | Doc
    d <- [Doc]
    xs ]

      explain :: Goal -> Doc
    explain Goal
    g =
        let useCtr :: Doc
    useCtr = Doc -> Int -> Doc -> Doc
    hang Doc
    "Unsolvable constraint:" Int
    2 (NameMap -> Goal -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Goal
    g)

        in
        case Type -> Type
    tNoUser (Goal -> Type
    goal Goal
    g) of
          TCon (PC PC
    pc) [Type]
    ts ->
            let tys :: [Doc]
    tys = [ Doc -> Doc
    backticks (NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t) | Type
    t <- [Type]
    ts ]
                doc1 :: Doc
    doc1 = case [Doc]
    tys of
                         (Doc
    doc1' : [Doc]
    _) -> Doc
    doc1'
                         [] -> FilePath -> Doc
    forall a. HasCallStack => FilePath -> a
    error FilePath
    "explainUnsolvable: Expected TCon to have at least one argument"
                custom :: Doc -> Doc
    custom Doc
    msg = Doc -> Int -> Doc -> Doc
    hang Doc
    msg
                                Int
    2 (FilePath -> Doc
    text FilePath
    "arising from" Doc -> Doc -> Doc
    $$
                                   ConstraintSource -> Doc
    forall a. PP a => a -> Doc
    pp (Goal -> ConstraintSource
    goalSource Goal
    g)   Doc -> Doc -> Doc
    $$
                                   FilePath -> Doc
    text FilePath
    "at" Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp (Goal -> Range
    goalRange Goal
    g))
            in
            case PC
    pc of
              PC
    PEqual      -> Doc
    useCtr
              PC
    PNeq        -> Doc
    useCtr
              PC
    PGeq        -> Doc
    useCtr
              PC
    PFin        -> Doc
    useCtr
              PC
    PPrime      -> Doc
    useCtr

              PHas Selector
    sel ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not have field" Doc -> Doc -> Doc
    <+> Doc
    f
                        Doc -> Doc -> Doc
    <+> Doc
    "of type" Doc -> Doc -> Doc
    <+> ([Doc]
    tys [Doc] -> Int -> Doc
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    1))
                where f :: Doc
    f = case Selector
    sel of
                            P.TupleSel Int
    n Maybe Int
    _ -> Int -> Doc
    int Int
    n
                            P.RecordSel Ident
    fl Maybe [Ident]
    _ -> Doc -> Doc
    backticks (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    fl)
                            P.ListSel Int
    n Maybe Int
    _ -> Int -> Doc
    int Int
    n

              PC
    PZero  ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not have `zero`")

              PC
    PLogic ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support logical operations.")

              PC
    PRing ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support ring operations.")

              PC
    PIntegral ->
                Doc -> Doc
    custom (Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "is not an integral type.")

              PC
    PField ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support field operations.")

              PC
    PRound ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support rounding operations.")

              PC
    PEq ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support equality.")

              PC
    PCmp        ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support comparisons.")

              PC
    PSignedCmp  ->
                Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "does not support signed comparisons.")

              PC
    PLiteral ->
                let doc2 :: Doc
    doc2 = [Doc]
    tys [Doc] -> Int -> Doc
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    1
                in Doc -> Doc
    custom (Doc
    doc1 Doc -> Doc -> Doc
    </> Doc
    "is not a valid literal of type" Doc -> Doc -> Doc
    <+> Doc
    doc2)

              PC
    PLiteralLessThan ->
                let doc2 :: Doc
    doc2 = [Doc]
    tys [Doc] -> Int -> Doc
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    1
                in Doc -> Doc
    custom (Doc
    "Type" Doc -> Doc -> Doc
    <+> Doc
    doc2 Doc -> Doc -> Doc
    </> Doc
    "does not contain all literals below" Doc -> Doc -> Doc
    <+> (Doc
    doc1 Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "."))

              PC
    PFLiteral ->
                case [Type]
    ts of
                  ~[Type
    m,Type
    n,Type
    _r,Type
    _a] ->
                     let frac :: Doc
    frac = Doc -> Doc
    backticks (NameMap -> Int -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    names Int
    4 Type
    m Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "/" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <>
                                           NameMap -> Int -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    names Int
    4 Type
    n)
                         ty :: Doc
    ty   = [Doc]
    tys [Doc] -> Int -> Doc
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    3
                     in Doc -> Doc
    custom (Doc
    frac Doc -> Doc -> Doc
    </> Doc
    "is not a valid literal of type" Doc -> Doc -> Doc
    </> Doc
    ty)

              PC
    PValidFloat ->
                case [Type]
    ts of
                  ~[Type
    e,Type
    p] ->
                    Doc -> Doc
    custom (Doc -> Int -> Doc -> Doc
    hang Doc
    "Unsupported floating point parameters:"
                               Int
    2 (Doc
    "exponent =" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    e Doc -> Doc -> Doc
    $$
                                  Doc
    "precision =" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    p))

              PC
    PAnd        -> Doc
    useCtr
              PC
    PTrue       -> Doc
    useCtr

          Type
    _ -> Doc
    useCtr

    -- | This picks the names to use when showing errors and warnings.
    computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap
    computeFreeVarNames :: [(Range, Warning)] -> [(Range, Error)] -> NameMap
    computeFreeVarNames [(Range, Warning)]
    warns [(Range, Error)]
    errs =
      [FilePath] -> [TVar] -> NameMap
    mkMap [FilePath]
    numRoots [TVar]
    numVaras NameMap -> NameMap -> NameMap
    forall a. IntMap a -> IntMap a -> IntMap a
    `IntMap.union` [FilePath] -> [TVar] -> NameMap
    mkMap [FilePath]
    otherRoots [TVar]
    otherVars

      {- XXX: Currently we pick the names based on the unique of the variable:
         smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`)
         This may still lead to changes in the names if the uniques got reordered
         for some reason.  A more stable approach might be to order the variables
         on their location in the error/warning, but that's quite a bit more code
         so for now we just go with the simple approximation. -}

      where
      mkName :: TVar -> b -> (Int, b)
    mkName TVar
    x b
    v = (TVar -> Int
    tvUnique TVar
    x, b
    v)
      mkMap :: [FilePath] -> [TVar] -> NameMap
    mkMap [FilePath]
    roots [TVar]
    vs = [(Int, FilePath)] -> NameMap
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList ((TVar -> FilePath -> (Int, FilePath))
    -> [TVar] -> [FilePath] -> [(Int, FilePath)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TVar -> FilePath -> (Int, FilePath)
    forall {b}. TVar -> b -> (Int, b)
    mkName [TVar]
    vs ([FilePath] -> [FilePath]
    variants [FilePath]
    roots))

      ([TVar]
    numVaras,[TVar]
    otherVars) = (TVar -> Bool) -> [TVar] -> ([TVar], [TVar])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition ((Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KNum) (Kind -> Bool) -> (TVar -> Kind) -> TVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf)
                           ([TVar] -> ([TVar], [TVar])) -> [TVar] -> ([TVar], [TVar])
    forall a b. (a -> b) -> a -> b
    $ Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList
                           (Set TVar -> [TVar]) -> Set TVar -> [TVar]
    forall a b. (a -> b) -> a -> b
    $ (TVar -> Bool) -> Set TVar -> Set TVar
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter TVar -> Bool
    isFreeTV
                           (Set TVar -> Set TVar) -> Set TVar -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ ([Warning], [Error]) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (((Range, Warning) -> Warning) -> [(Range, Warning)] -> [Warning]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range, Warning) -> Warning
    forall a b. (a, b) -> b
    snd [(Range, Warning)]
    warns, ((Range, Error) -> Error) -> [(Range, Error)] -> [Error]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range, Error) -> Error
    forall a b. (a, b) -> b
    snd [(Range, Error)]
    errs)

      otherRoots :: [FilePath]
    otherRoots = [ FilePath
    "a", FilePath
    "b", FilePath
    "c", FilePath
    "d" ]
      numRoots :: [FilePath]
    numRoots   = [ FilePath
    "m", FilePath
    "n", FilePath
    "u", FilePath
    "v" ]

      useUnicode :: Bool
    useUnicode = Bool
    True

      suff :: Int -> FilePath
    suff Int
    n
        | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    10 Bool -> Bool -> Bool
    && Bool
    useUnicode = [Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Int
    0x2080 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n)]
        | Bool
    otherwise = Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    n

      variant :: Int -> ShowS
    variant Int
    n FilePath
    x = if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then FilePath
    x else FilePath
    x FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    suff Int
    n

      variants :: [FilePath] -> [FilePath]
    variants [FilePath]
    roots = [ Int -> ShowS
    variant Int
    n FilePath
    r | Int
    n <- [ Int
    0 .. ], FilePath
    r <- [FilePath]
    roots ]