{-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
{-# Language OverloadedStrings #-}
{-# Language Safe #-}
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 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)
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. [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
_ TVar
x Type
_) (Range
_,NotForAll TypeSource
_ TVar
y Type
_) = TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y
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
                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    = 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 Type Type
                -- ^ Expected type, inferred type

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

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

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

              | UndefinedExistVar Name
              | TypeShadowing String Name String
              | MissingModTParam (Located Ident)
              | MissingModVParam (Located Ident)
                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)

-- | 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
    KindMismatch {}                                  -> Int
10
    TyVarWithParams {}                               -> Int
9
    TypeMismatch {}                                  -> Int
8
    RecursiveType {}                                 -> Int
7
    NotForAll {}                                     -> Int
6
    TypeVariableEscaped {}                           -> Int
5

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


    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



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)

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

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
      TypeMismatch TypeSource
src Type
t1 Type
t2    -> TypeSource -> Type -> Type -> Error
TypeMismatch TypeSource
src (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 Type
t1 Type
t2   -> TypeSource -> Type -> Type -> Error
RecursiveType TypeSource
src (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 Type
t [TParam]
xs ->
                                 TypeSource -> Type -> [TParam] -> Error
TypeVariableEscaped TypeSource
src (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 TVar
x Type
t         -> TypeSource -> TVar -> Type -> Error
NotForAll TypeSource
src 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

      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)


      UndefinedExistVar {} -> Error
err
      TypeShadowing {}     -> Error
err
      MissingModTParam {}  -> Error
err
      MissingModVParam {}  -> 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
      TypeMismatch TypeSource
_ Type
t1 Type
t2      -> (Type, Type) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type
t1,Type
t2)
      RecursiveType TypeSource
_ 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
_ 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
_ 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

      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

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

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

      RecursiveType TypeSource
src 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
"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
"(e.g., they cannot be used in type synonyms)."

      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
"Expected:" Doc -> Doc -> Doc
<+> Kind -> Doc
cppKind Kind
k1
              , Doc
"Inferred:" Doc -> Doc -> Doc
<+> Kind -> Doc
cppKind Kind
k2
              , Kind -> Kind -> Doc
kindMismatchHint Kind
k1 Kind
k2
              , Doc -> (TypeSource -> Doc) -> Maybe TypeSource -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\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
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 TypeSource
src 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
"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
             , Type -> Type -> Doc
mismatchHint Type
t1 Type
t2
             , Doc
"When checking" Doc -> Doc -> Doc
<+> TypeSource -> Doc
forall a. PP a => a -> Doc
pp TypeSource
src
             ]

      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 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
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))
               , Doc
"When checking" Doc -> Doc -> Doc
<+> TypeSource -> Doc
forall a. PP a => a -> Doc
pp TypeSource
src
               ]

      NotForAll TypeSource
src 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
"When checking" Doc -> Doc -> Doc
<+> TypeSource -> Doc
forall a. PP a => a -> Doc
pp TypeSource
src
               ]

      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
$
        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
$$ Int -> Doc -> Doc
nest Int
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))

      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 -> Doc
empty
         in NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc
"Ambiguous numeric type:" Doc -> Doc -> Doc
<+> TypeSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
tvarDesc TVarInfo
x) Doc -> Doc -> Doc
$$ Doc
sizeMsg)

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




    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 = Doc
x Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 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) -> Doc
"Possibly due to a missing `=>`"
        (Kind, Kind)
_ -> Doc
empty

    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
$$ 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
_ []  = Doc
forall a. Monoid a => a
mempty
        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
_ = 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))



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
"Unsolvable constraint:" Doc -> Doc -> Doc
$$
                  Int -> Doc -> Doc
nest 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 ]
            Doc
doc1 : [Doc]
_ = [Doc]
tys
            custom :: Doc -> Doc
custom Doc
msg = Doc
msg Doc -> Doc -> Doc
$$
                         Int -> Doc -> Doc
nest 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. [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. [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
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. [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
"Unsupported floating point parameters:" Doc -> Doc -> Doc
$$
                     Int -> Doc -> Doc
nest 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 reordred
     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 ]