{-# 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
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Range -> (String, Position, Position)
cmpR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst))    -- order errors
              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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. [(a, Error)] -> [(a, Error)]
chooseBestError
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==)    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 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    = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a}. (a, Error) -> (Int, (a, Error))
addErrorRating


  cmpR :: Range -> (String, Position, Position)
cmpR Range
r  = ( Range -> String
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 forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (Range, Error) -> Bool
keep [(Range, Error)]
survived) (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 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 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 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Warning] -> ShowS
$cshowList :: [Warning] -> ShowS
show :: Warning -> String
$cshow :: Warning -> String
showsPrec :: Int -> Warning -> ShowS
$cshowsPrec :: Int -> Warning -> ShowS
Show, 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: Warning -> ()
$crnf :: 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 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> String
$cshow :: Error -> String
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show, 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: Error -> ()
$crnf :: Error -> ()
NFData)

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

data BIWhat = BIFunctor | BIInterface | BIPrimitive | BIForeign | BIAbstractType
    deriving (Int -> BIWhat -> ShowS
[BIWhat] -> ShowS
BIWhat -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BIWhat] -> ShowS
$cshowList :: [BIWhat] -> ShowS
show :: BIWhat -> String
$cshow :: BIWhat -> String
showsPrec :: Int -> BIWhat -> ShowS
$cshowsPrec :: Int -> BIWhat -> ShowS
Show, 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
$cto :: forall x. Rep BIWhat x -> BIWhat
$cfrom :: forall x. BIWhat -> Rep BIWhat x
Generic, BIWhat -> ()
forall a. (a -> ()) -> NFData a
rnf :: BIWhat -> ()
$crnf :: 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
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
tHasErrors (forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
g)                  -> Int
0
      | Bool
otherwise                                    -> Int
4

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

    UnsolvedDelayedCt DelayedCt
dt
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
tHasErrors (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 forall a b. (a -> b) -> a -> b
$! (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 {}     -> forall a. Set a
Set.empty
      DefaultingWildType {} -> forall a. Set a
Set.empty
      DefaultingTo TVarInfo
_ Type
ty     -> forall t. FVS t => t -> Set TVar
fvs Type
ty
      NonExhaustivePropGuards {} -> 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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Schema
t1) forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t1) forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t1) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t2)
      UnsolvedGoals [Goal]
gs          -> [Goal] -> Error
UnsolvedGoals forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
gs
      UnsolvableGoals [Goal]
gs        -> [Goal] -> Error
UnsolvableGoals forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
gs
      UnsolvedDelayedCt DelayedCt
g       -> DelayedCt -> Error
UnsolvedDelayedCt forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) 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 forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su FFITypeError
e

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

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

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

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

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

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

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

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

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


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

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

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

      NonExhaustivePropGuards Name
n ->
        String -> Doc
text String
"Could not prove that the constraint guards used in defining" Doc -> Doc -> Doc
<+> 
        forall a. PP a => a -> Doc
pp Name
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"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 ->
        forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested Doc
"Matching would result in an infinite type." forall a b. (a -> b) -> a -> b
$
          [Doc] -> Doc
vcat ( [ Doc
"The type: " Doc -> Doc -> Doc
<+> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t1
                 , Doc
"occurs in:" Doc -> Doc -> Doc
<+> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t2
                 ] forall a. [a] -> [a] -> [a]
++ Path -> [Doc]
ppCtxt Path
pa forall a. [a] -> [a] -> [a]
++
                 [ Doc
"When checking" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp TypeSource
src ] )

      Error
UnexpectedTypeWildCard ->
        forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested Doc
"Wild card types are not allowed in this context" 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 ->
        forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested Doc
"Incorrect type form." forall a b. (a -> b) -> a -> b
$
         [Doc] -> Doc
vcat 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
           ] forall a. [a] -> [a] -> [a]
++ Kind -> Kind -> [Doc]
kindMismatchHint Kind
k1 Kind
k2
             forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\TypeSource
src -> [Doc
"When checking" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp TypeSource
src]) Maybe TypeSource
mbsrc

      TooManyTypeParams Int
extra Kind
k ->
        forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested Doc
"Malformed type."
          (Doc
"Kind" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (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
<+> forall {a}. (Eq a, Num a, Show a) => a -> String -> Doc
pl Int
extra String
"parameter" Doc -> Doc -> Doc
<.> Doc
".")

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

      TooFewTyParams Name
t Int
few ->
        forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested Doc
"Malformed type."
          (Doc
"Type" Doc -> Doc -> 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
<+> String -> Doc
text String
"parameters.")

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

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

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

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

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

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

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

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

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

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

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

      RepeatedTypeParameter Ident
x [Range]
rs ->
        forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$
          Doc
"Multiple definitions for type parameter `" Doc -> Doc -> Doc
<.> forall a. PP a => a -> Doc
pp Ident
x Doc -> Doc -> Doc
<.> Doc
"`:"
          Doc -> Doc -> Doc
$$ [Doc] -> Doc
bullets (forall a b. (a -> b) -> [a] -> [b]
map 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
<+> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t']
                 Maybe Type
Nothing -> []
         in forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err
              ([Doc] -> Doc
vcat ([Doc
"Ambiguous numeric type:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
tvarDesc TVarInfo
x)] 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 (forall a. PP a => a -> Doc
pp Name
x)
      TypeShadowing String
this Name
new String
that ->
        Doc
"Type" Doc -> Doc -> Doc
<+> String -> Doc
text String
this Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Name
new) Doc -> Doc -> Doc
<+>
        Doc
"shadowing an existing" Doc -> Doc -> Doc
<+> String -> Doc
text String
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 (forall a. PP a => a -> Doc
pp (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 (forall a. PP a => a -> Doc
pp (forall a. Located a -> a
thing Located Ident
x))

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

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

      FunctorInstanceBadArgument Ident
i ->
        Doc
"Functor does not have parameter" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (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 (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:" forall a b. (a -> b) -> a -> b
$
              [Doc] -> Doc
bullets
                [ Doc
"Module parameter:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Ident
i
                , Doc
"Value parameter:" Doc -> Doc -> 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:" forall a b. (a -> b) -> a -> b
$
              [Doc] -> Doc
bullets forall a b. (a -> b) -> a -> b
$
                [ Doc
it Doc -> Doc -> 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"
                ] 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:" forall a b. (a -> b) -> a -> b
$
              [Doc] -> Doc
bullets
                [ Doc
"Parameter name:" Doc -> Doc -> 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: " forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
vcat
          [ forall a. PP a => a -> Doc
pp TParam
param Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Kind
k
          , Doc
"Only type variables of kind" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Kind
KNum Doc -> Doc -> Doc
<+> Doc
"are supported"
          , Doc
"When checking" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp TypeSource
src ]

      UnsupportedFFIType TypeSource
src FFITypeError
t -> [Doc] -> Doc
vcat
        [ forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names FFITypeError
t
        , Doc
"When checking" Doc -> Doc -> 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 (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 (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]
_ -> forall a. PP a => a -> Doc
pp TCon
tc
                  Type
_         -> 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 -> String -> Doc
pl a
1 String
x     = String -> Doc
text String
"1" Doc -> Doc -> Doc
<+> String -> Doc
text String
x
    pl a
n String
x     = String -> Doc
text (forall a. Show a => a -> String
show a
n) Doc -> Doc -> Doc
<+> String -> Doc
text String
x Doc -> Doc -> Doc
<.> String -> Doc
text String
"s"

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

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

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

    noUni :: Bool
noUni = forall a. Set a -> Bool
Set.null (forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (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
<+> forall a. PP a => a -> Doc
pp Path
pa ]




explainUnsolvable :: NameMap -> [Goal] -> Doc
explainUnsolvable :: NameMap -> [Goal] -> Doc
explainUnsolvable NameMap
names [Goal]
gs =
  forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names [Goal]
gs ([Doc] -> Doc
bullets (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 (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 (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'
                     [] -> forall a. HasCallStack => String -> a
error String
"explainUnsolvable: Expected TCon to have at least one argument"
            custom :: Doc -> Doc
custom Doc
msg = Doc -> Int -> Doc -> Doc
hang Doc
msg
                            Int
2 (String -> Doc
text String
"arising from" Doc -> Doc -> Doc
$$
                               forall a. PP a => a -> Doc
pp (Goal -> ConstraintSource
goalSource Goal
g)   Doc -> Doc -> Doc
$$
                               String -> Doc
text String
"at" Doc -> Doc -> 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 forall a. [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 (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 forall a. [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 forall a. [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 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 (forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
names Int
4 Type
m forall a. Semigroup a => a -> a -> a
<> Doc
"/" forall a. Semigroup a => a -> a -> a
<>
                                       forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
names Int
4 Type
n)
                     ty :: Doc
ty   = [Doc]
tys forall a. [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
<+> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
e Doc -> Doc -> Doc
$$
                              Doc
"precision =" Doc -> Doc -> 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 =
  [String] -> [TVar] -> NameMap
mkMap [String]
numRoots [TVar]
numVaras forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` [String] -> [TVar] -> NameMap
mkMap [String]
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 :: [String] -> [TVar] -> NameMap
mkMap [String]
roots [TVar]
vs = forall a. [(Int, a)] -> IntMap a
IntMap.fromList (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {b}. TVar -> b -> (Int, b)
mkName [TVar]
vs ([String] -> [String]
variants [String]
roots))

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

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

  useUnicode :: Bool
useUnicode = Bool
True

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

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

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