    {-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
    {-# Language OverloadedStrings #-}
    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,minimumBy)
    import Data.Function(on)

    import qualified Cryptol.Parser.AST as P
    import Cryptol.Parser.Position(Located(..), Range(..))
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.InferTypes
    import Cryptol.TypeCheck.Subst
    import Cryptol.ModuleSystem.Name(Name)
    import Cryptol.Utils.Ident(Ident)

    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)]
    forall a. [(a, Error)] -> [(a, Error)]
    dropSumbsumed
      where

      -- pick shortest error from each location.
      dropErrorsFromSameLoc :: [(Range, Error)] -> [(Range, Error)]
    dropErrorsFromSameLoc = ([(Range, Error)] -> (Range, Error))
    -> [[(Range, Error)]] -> [(Range, Error)]
    forall a b. (a -> b) -> [a] -> [b]
    map [(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)

      addErrorSize :: (a, b) -> (Int, (a, b))
    addErrorSize (r :: a
    r,e :: b
    e) = (FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (b -> Doc
    forall a. PP a => a -> Doc
    pp b
    e)), (a
    r,b
    e))
      chooseBestError :: [(a, Error)] -> (a, Error)
    chooseBestError    = (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)) -> Ordering)
    -> [(Int, (a, Error))] -> (Int, (a, Error))
    forall (t :: * -> *) a.
    Foldable t =>
    (a -> a -> Ordering) -> t a -> a
    minimumBy (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 b a. PP b => (a, b) -> (Int, (a, b))
    addErrorSize

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

      dropSumbsumed :: [(a, Error)] -> [(a, Error)]
    dropSumbsumed xs :: [(a, Error)]
    xs =
        case [(a, Error)]
    xs of
          (r :: a
    r,e :: Error
    e) : rest :: [(a, Error)]
    rest -> (a
    r,Error
    e) (a, Error) -> [(a, Error)] -> [(a, Error)]
    forall a. a -> [a] -> [a]
    :
                            [(a, Error)] -> [(a, Error)]
    dropSumbsumed (((a, Error) -> Bool) -> [(a, Error)] -> [(a, Error)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> ((a, Error) -> Bool) -> (a, Error) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .Error -> Error -> Bool
    subsumes Error
    e (Error -> Bool) -> ((a, Error) -> Error) -> (a, Error) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a, Error) -> Error
    forall a b. (a, b) -> b
    snd) [(a, Error)]
    rest)
          [] -> []

    -- | Should the first error suppress the next one.
    subsumes :: Error -> Error -> Bool
    subsumes :: Error -> Error -> Bool
    subsumes (NotForAll x :: TVar
    x _) (NotForAll y :: TVar
    y _) = TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    y
    subsumes _ _ = Bool
    False

    data Warning  = DefaultingKind (P.TParam Name) P.Kind
                  | DefaultingWildType P.Kind
                  | DefaultingTo TVarInfo Type
                    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
    showList :: [Warning] -> ShowS
    $cshowList :: [Warning] -> ShowS
    show :: Warning -> FilePath
    $cshow :: Warning -> FilePath
    showsPrec :: Int -> Warning -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep Warning x -> Warning
    $cfrom :: forall x. Warning -> Rep Warning x
    Generic, Warning -> ()
    (Warning -> ()) -> NFData Warning
    forall a. (a -> ()) -> NFData a
    rnf :: Warning -> ()
    $crnf :: Warning -> ()
    NFData)

    -- | Various errors that might happen during type checking/inference
    data Error    = ErrorMsg Doc
                    -- ^ Just say this

                  | KindMismatch 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 Type Type
                    -- ^ Expected type, inferred type

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

                  | UnsolvedGoals Bool [Goal]
                    -- ^ A constraint that we could not solve
                    -- The boolean indicates if we know that this constraint
                    -- is impossible.

                  | 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 Type [TParam]
                    -- ^ Unification variable depends on quantified variables
                    -- that are not in scope.

                  | NotForAll 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

                  | CannotMixPositionalAndNamedTypeParams

                  | UndefinedTypeParameter (Located Ident)

                  | RepeatedTypeParameter Ident [Range]

                    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
    showList :: [Error] -> ShowS
    $cshowList :: [Error] -> ShowS
    show :: Error -> FilePath
    $cshow :: Error -> FilePath
    showsPrec :: Int -> Error -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep Error x -> Error
    $cfrom :: forall x. Error -> Rep Error x
    Generic, Error -> ()
    (Error -> ()) -> NFData Error
    forall a. (a -> ()) -> NFData a
    rnf :: Error -> ()
    $crnf :: Error -> ()
    NFData)

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

    instance FVS Warning where
      fvs :: Warning -> Set TVar
    fvs warn :: 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 _ ty :: Type
    ty     -> Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    ty

    instance TVars Error where
      apSubst :: Subst -> Error -> Error
    apSubst su :: Subst
    su err :: Error
    err =
        case Error
    err of
          ErrorMsg _                -> Error
    err
          KindMismatch {}           -> Error
    err
          TooManyTypeParams {}      -> Error
    err
          TyVarWithParams           -> Error
    err
          TooManyTySynParams {}     -> Error
    err
          TooFewTyParams {}         -> Error
    err
          RecursiveTypeDecls {}     -> Error
    err
          TypeMismatch t1 :: Type
    t1 t2 :: Type
    t2        -> Type -> Type -> Error
    TypeMismatch (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t1) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t2)
          RecursiveType t1 :: Type
    t1 t2 :: Type
    t2       -> Type -> Type -> Error
    RecursiveType (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t1) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t2)
          UnsolvedGoals x :: Bool
    x gs :: [Goal]
    gs        -> Bool -> [Goal] -> Error
    UnsolvedGoals Bool
    x (Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Goal]
    gs)
          UnsolvedDelayedCt g :: DelayedCt
    g       -> DelayedCt -> Error
    UnsolvedDelayedCt (Subst -> DelayedCt -> DelayedCt
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su DelayedCt
    g)
          UnexpectedTypeWildCard    -> Error
    err
          TypeVariableEscaped t :: Type
    t xs :: [TParam]
    xs  -> Type -> [TParam] -> Error
    TypeVariableEscaped (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) [TParam]
    xs
          NotForAll x :: TVar
    x t :: Type
    t             -> TVar -> Type -> Error
    NotForAll TVar
    x (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
          TooManyPositionalTypeParams -> Error
    err
          CannotMixPositionalAndNamedTypeParams -> Error
    err

          UndefinedTypeParameter {} -> Error
    err
          RepeatedTypeParameter {} -> Error
    err

    instance FVS Error where
      fvs :: Error -> Set TVar
    fvs err :: Error
    err =
        case Error
    err of
          ErrorMsg {}               -> Set TVar
    forall a. Set a
    Set.empty
          KindMismatch {}           -> Set TVar
    forall a. Set a
    Set.empty
          TooManyTypeParams {}      -> Set TVar
    forall a. Set a
    Set.empty
          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
          TypeMismatch t1 :: Type
    t1 t2 :: Type
    t2        -> (Type, Type) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Type
    t1,Type
    t2)
          RecursiveType t1 :: Type
    t1 t2 :: Type
    t2       -> (Type, Type) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Type
    t1,Type
    t2)
          UnsolvedGoals _ gs :: [Goal]
    gs        -> [Goal] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Goal]
    gs
          UnsolvedDelayedCt g :: DelayedCt
    g       -> DelayedCt -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs DelayedCt
    g
          UnexpectedTypeWildCard    -> Set TVar
    forall a. Set a
    Set.empty
          TypeVariableEscaped t :: Type
    t xs :: [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 x :: TVar
    x t :: 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)
          TooManyPositionalTypeParams -> Set TVar
    forall a. Set a
    Set.empty
          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

    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 _ (WithNames warn :: Warning
    warn names :: 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 x :: TParam Name
    x k :: Kind
    k ->
            FilePath -> Doc
    text "Assuming " Doc -> Doc -> Doc
    <+> TParam Name -> Doc
    forall a. PP a => a -> Doc
    pp TParam Name
    x Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "to have" Doc -> Doc -> Doc
    <+> Kind -> Doc
    P.cppKind Kind
    k

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

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

    instance PP (WithNames Error) where
      ppPrec :: Int -> WithNames Error -> Doc
    ppPrec _ (WithNames err :: Error
    err names :: NameMap
    names) =
        case Error
    err of
          ErrorMsg msg :: Doc
    msg ->
            NameMap -> Error -> Doc -> Doc
    forall t. FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter NameMap
    names Error
    err
            Doc
    msg

          RecursiveType t1 :: Type
    t1 t2 :: 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 "Matching would result in an infinite type."
              ("The type: " Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t1 Doc -> Doc -> Doc
    $$
               "occurs in:" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t2)

          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 "Wild card types are not allowed in this context"
              "(e.g., they cannot be used in type synonyms)."

          KindMismatch k1 :: Kind
    k1 k2 :: 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 "Incorrect type form."
              ("Expected:" Doc -> Doc -> Doc
    <+> Kind -> Doc
    cppKind Kind
    k1 Doc -> Doc -> Doc
    $$
               "Inferred:" Doc -> Doc -> Doc
    <+> Kind -> Doc
    cppKind Kind
    k2)

          TooManyTypeParams extra :: Int
    extra k :: 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 "Malformed type."
              ("Kind" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k) Doc -> Doc -> Doc
    <+> "is not a function," 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 "parameter" Doc -> Doc -> Doc
    <.> ".")

          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 "Malformed type."
                   "Type variables cannot be applied to parameters."

          TooManyTySynParams t :: Name
    t extra :: 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 "Malformed type."
              ("Type synonym" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    nm Name
    t 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 "extra parameters" Doc -> Doc -> Doc
    <.> FilePath -> Doc
    text ".")

          TooFewTyParams t :: Name
    t few :: 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 "Malformed type."
              ("Type" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    nm Name
    t Doc -> Doc -> Doc
    <+> "is missing" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    few Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "parameters.")

          RecursiveTypeDecls ts :: [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 "Recursive type declarations:"
                   ([Doc] -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. PP a => a -> Doc
    nm [Name]
    ts)

          TypeMismatch t1 :: Type
    t1 t2 :: 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 "Type mismatch:"
              ("Expected type:" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t1 Doc -> Doc -> 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
    $$
               Type -> Type -> Doc
    mismatchHint Type
    t1 Type
    t2)

          UnsolvedGoals imp :: Bool
    imp gs :: [Goal]
    gs
            | Bool
    imp ->
              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 "Unsolvable 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
    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 "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 "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 g :: 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 "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 "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 t :: Type
    t xs :: [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 ("The type" Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t Doc -> Doc -> Doc
    <+>
                                            "is not sufficiently polymorphic.")
                   ("It cannot depend on quantified variables:" Doc -> Doc -> Doc
    <+>
                    [Doc] -> Doc
    sep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ((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)))

          NotForAll x :: TVar
    x t :: 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 "Inferred type is not sufficiently polymorphic."
              ("Quantified variable:" Doc -> Doc -> Doc
    <+> NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names TVar
    x Doc -> Doc -> Doc
    $$
               "cannot match type:"   Doc -> Doc -> Doc
    <+> NameMap -> Type -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names Type
    t)

          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
    $
            "Too many positional type-parameters in explicit type application"

          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
    $
            "Named and positional type applications may not be mixed."

          UndefinedTypeParameter x :: 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
    $
            "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
    $$ "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 x :: Ident
    x rs :: [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
    $
            "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
    $$ Int -> Doc -> Doc
    nest 2 ([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))

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

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

        pl :: a -> FilePath -> Doc
    pl 1 x :: FilePath
    x     = FilePath -> Doc
    text "1" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    x
        pl n :: a
    n x :: 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 "s"

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

        mismatchHint :: Type -> Type -> Doc
    mismatchHint (TRec fs1 :: [(Ident, Type)]
    fs1) (TRec fs2 :: [(Ident, Type)]
    fs2) =
          FilePath -> [Ident] -> Doc
    forall a. PP a => FilePath -> [a] -> Doc
    hint "Missing" [Ident]
    missing Doc -> Doc -> Doc
    $$ FilePath -> [Ident] -> Doc
    forall a. PP a => FilePath -> [a] -> Doc
    hint "Unexpected" [Ident]
    extra
          where
            missing :: [Ident]
    missing = ((Ident, Type) -> Ident) -> [(Ident, Type)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Type) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Type)]
    fs1 [Ident] -> [Ident] -> [Ident]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ ((Ident, Type) -> Ident) -> [(Ident, Type)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Type) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Type)]
    fs2
            extra :: [Ident]
    extra   = ((Ident, Type) -> Ident) -> [(Ident, Type)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Type) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Type)]
    fs2 [Ident] -> [Ident] -> [Ident]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ ((Ident, Type) -> Ident) -> [(Ident, Type)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Type) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Type)]
    fs1
            hint :: FilePath -> [a] -> Doc
    hint _ []  = Doc
    forall a. Monoid a => a
    mempty
            hint s :: FilePath
    s [x :: a
    x] = FilePath -> Doc
    text FilePath
    s Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "field" Doc -> Doc -> Doc
    <+> a -> Doc
    forall a. PP a => a -> Doc
    pp a
    x
            hint s :: FilePath
    s xs :: [a]
    xs  = FilePath -> Doc
    text FilePath
    s Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "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 _ _ = Doc
    forall a. Monoid a => a
    mempty

        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))