{-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Error where


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

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

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

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

  addErrorSize :: (a, b) -> (Int, (a, b))
addErrorSize (r :: a
r,e :: b
e) = (FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Doc -> FilePath
forall a. Show a => a -> FilePath
show (b -> Doc
forall a. PP a => a -> Doc
pp b
e)), (a
r,b
e))
  chooseBestError :: [(a, Error)] -> (a, Error)
chooseBestError    = (Int, (a, Error)) -> (a, Error)
forall a b. (a, b) -> b
snd ((Int, (a, Error)) -> (a, Error))
-> ([(a, Error)] -> (Int, (a, Error)))
-> [(a, Error)]
-> (a, Error)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, (a, Error)) -> (Int, (a, Error)) -> Ordering)
-> [(Int, (a, Error))] -> (Int, (a, Error))
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, (a, Error)) -> Int)
-> (Int, (a, Error))
-> (Int, (a, Error))
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, (a, Error)) -> Int
forall a b. (a, b) -> a
fst) ([(Int, (a, Error))] -> (Int, (a, Error)))
-> ([(a, Error)] -> [(Int, (a, Error))])
-> [(a, Error)]
-> (Int, (a, Error))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Error) -> (Int, (a, Error)))
-> [(a, Error)] -> [(Int, (a, Error))]
forall a b. (a -> b) -> [a] -> [b]
map (a, Error) -> (Int, (a, Error))
forall b a. PP b => (a, b) -> (Int, (a, b))
addErrorSize


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

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

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

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

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

              | KindMismatch Kind Kind
                -- ^ Expected kind, inferred kind

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

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

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

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

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

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

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

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

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

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

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

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

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

              | CannotMixPositionalAndNamedTypeParams

              | UndefinedTypeParameter (Located Ident)

              | RepeatedTypeParameter Ident [Range]

                deriving (Int -> Error -> ShowS
[Error] -> ShowS
Error -> FilePath
(Int -> Error -> ShowS)
-> (Error -> FilePath) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> FilePath
$cshow :: Error -> FilePath
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show, (forall x. Error -> Rep Error x)
-> (forall x. Rep Error x -> Error) -> Generic Error
forall x. Rep Error x -> Error
forall x. Error -> Rep Error x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Error x -> Error
$cfrom :: forall x. Error -> Rep Error x
Generic, Error -> ()
(Error -> ()) -> NFData Error
forall a. (a -> ()) -> NFData a
rnf :: Error -> ()
$crnf :: Error -> ()
NFData)

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

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

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

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


instance FVS Error where
  fvs :: Error -> Set TVar
fvs err :: Error
err =
    case Error
err of
      ErrorMsg {}               -> Set TVar
forall a. Set a
Set.empty
      KindMismatch {}           -> Set TVar
forall a. Set a
Set.empty
      TooManyTypeParams {}      -> Set TVar
forall a. Set a
Set.empty
      TyVarWithParams           -> Set TVar
forall a. Set a
Set.empty
      TooManyTySynParams {}     -> Set TVar
forall a. Set a
Set.empty
      TooFewTyParams {}         -> Set TVar
forall a. Set a
Set.empty
      RecursiveTypeDecls {}     -> Set TVar
forall a. Set a
Set.empty
      TypeMismatch t1 :: Type
t1 t2 :: Type
t2        -> (Type, Type) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type
t1,Type
t2)
      RecursiveType t1 :: Type
t1 t2 :: Type
t2       -> (Type, Type) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type
t1,Type
t2)
      UnsolvedGoals _ gs :: [Goal]
gs        -> [Goal] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Goal]
gs
      UnsolvedDelayedCt g :: DelayedCt
g       -> DelayedCt -> Set TVar
forall t. FVS t => t -> Set TVar
fvs DelayedCt
g
      UnexpectedTypeWildCard    -> Set TVar
forall a. Set a
Set.empty
      TypeVariableEscaped t :: Type
t xs :: [TParam]
xs  -> Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.union`
                                            [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
TVBound [TParam]
xs)
      NotForAll x :: TVar
x t :: Type
t             -> TVar -> Set TVar -> Set TVar
forall a. Ord a => a -> Set a -> Set a
Set.insert TVar
x (Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t)
      TooManyPositionalTypeParams -> Set TVar
forall a. Set a
Set.empty
      CannotMixPositionalAndNamedTypeParams -> Set TVar
forall a. Set a
Set.empty
      UndefinedTypeParameter {}             -> Set TVar
forall a. Set a
Set.empty
      RepeatedTypeParameter {}              -> Set TVar
forall a. Set a
Set.empty



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

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


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

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

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

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

      RecursiveType t1 :: Type
t1 t2 :: Type
t2 ->
        NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested "Matching would result in an infinite type."
          ("The type: " Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t1 Doc -> Doc -> Doc
$$
           "occurs in:" Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t2)

      UnexpectedTypeWildCard ->
        NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested "Wild card types are not allowed in this context"
          "(e.g., they cannot be used in type synonyms)."

      KindMismatch k1 :: Kind
k1 k2 :: Kind
k2 ->
        NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested "Incorrect type form."
          ("Expected:" Doc -> Doc -> Doc
<+> Kind -> Doc
cppKind Kind
k1 Doc -> Doc -> Doc
$$
           "Inferred:" Doc -> Doc -> Doc
<+> Kind -> Doc
cppKind Kind
k2)

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

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

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

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

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

      TypeMismatch t1 :: Type
t1 t2 :: Type
t2 ->
        NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested "Type mismatch:"
          ("Expected type:" Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t1 Doc -> Doc -> Doc
$$
           "Inferred type:" Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t2 Doc -> Doc -> Doc
$$
           Type -> Type -> Doc
mismatchHint Type
t1 Type
t2)

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

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

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

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

      TypeVariableEscaped t :: Type
t xs :: [TParam]
xs ->
        NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested ("The type" Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t Doc -> Doc -> Doc
<+>
                                        "is not sufficiently polymorphic.")
               ("It cannot depend on quantified variables:" Doc -> Doc -> Doc
<+>
                [Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names) [TParam]
xs)))

      NotForAll x :: TVar
x t :: Type
t ->
        NameMap -> Error -> Doc -> Doc
forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
names Error
err (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
nested "Inferred type is not sufficiently polymorphic."
          ("Quantified variable:" Doc -> Doc -> Doc
<+> NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names TVar
x Doc -> Doc -> Doc
$$
           "cannot match type:"   Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t)

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

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

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

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

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

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

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

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

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

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