{-# LANGUAGE CPP                 #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}

module GHC.Tc.Errors(
       reportUnsolved, reportAllUnsolved, warnAllUnsolved,
       warnDefaulting,

       solverDepthErrorTcS
  ) where

#include "HsVersions.h"

import GHC.Prelude

import GHC.Tc.Types
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.Env( tcInitTidyEnv )
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Unify ( checkTyVarEq )
import GHC.Tc.Types.Origin
import GHC.Rename.Unbound ( unknownNameSuggestions )
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr  ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon, pprWithTYPE )
import GHC.Core.Unify     ( tcMatchTys, flattenTys )
import GHC.Unit.Module
import GHC.Tc.Instance.Family
import GHC.Tc.Utils.Instantiate
import GHC.Core.InstEnv
import GHC.Core.TyCon
import GHC.Core.Class
import GHC.Core.DataCon
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.EvTerm
import GHC.Hs.Binds ( PatSynBind(..) )
import GHC.Types.Name
import GHC.Types.Name.Reader ( lookupGRE_Name, GlobalRdrEnv, mkRdrUnqual )
import GHC.Builtin.Names ( typeableClassName )
import GHC.Types.Id
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Name.Set
import GHC.Data.Bag
import GHC.Utils.Error  ( pprLocMsgEnvelope )
import GHC.Types.Basic
import GHC.Types.Error
import GHC.Types.Unique.Set ( nonDetEltsUniqSet )
import GHC.Core.ConLike ( ConLike(..))
import GHC.Utils.Misc
import GHC.Data.FastString
import GHC.Utils.Outputable as O
import GHC.Utils.Panic
import GHC.Types.SrcLoc
import GHC.Driver.Session
import GHC.Driver.Ppr
import GHC.Data.List.SetOps ( equivClasses )
import GHC.Data.Maybe
import qualified GHC.LanguageExtensions as LangExt
import GHC.Utils.FV ( fvVarList, unionFV )

import Control.Monad    ( when, unless )
import Data.Foldable    ( toList )
import Data.List        ( partition, mapAccumL, sortBy, unfoldr )

import {-# SOURCE #-} GHC.Tc.Errors.Hole ( findValidHoleFits )

-- import Data.Semigroup   ( Semigroup )
import qualified Data.Semigroup as Semigroup


{-
************************************************************************
*                                                                      *
\section{Errors and contexts}
*                                                                      *
************************************************************************

ToDo: for these error messages, should we note the location as coming
from the insts, or just whatever seems to be around in the monad just
now?

Note [Deferring coercion errors to runtime]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
While developing, sometimes it is desirable to allow compilation to succeed even
if there are type errors in the code. Consider the following case:

  module Main where

  a :: Int
  a = 'a'

  main = print "b"

Even though `a` is ill-typed, it is not used in the end, so if all that we're
interested in is `main` it is handy to be able to ignore the problems in `a`.

Since we treat type equalities as evidence, this is relatively simple. Whenever
we run into a type mismatch in GHC.Tc.Utils.Unify, we normally just emit an error. But it
is always safe to defer the mismatch to the main constraint solver. If we do
that, `a` will get transformed into

  co :: Int ~ Char
  co = ...

  a :: Int
  a = 'a' `cast` co

The constraint solver would realize that `co` is an insoluble constraint, and
emit an error with `reportUnsolved`. But we can also replace the right-hand side
of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
to compile, and it will run fine unless we evaluate `a`. This is what
`deferErrorsToRuntime` does.

It does this by keeping track of which errors correspond to which coercion
in GHC.Tc.Errors. GHC.Tc.Errors.reportTidyWanteds does not print the errors
and does not fail if -fdefer-type-errors is on, so that we can continue
compilation. The errors are turned into warnings in `reportUnsolved`.
-}

-- | Report unsolved goals as errors or warnings. We may also turn some into
-- deferred run-time errors if `-fdefer-type-errors` is on.
reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
reportUnsolved WantedConstraints
wanted
  = do { EvBindsVar
binds_var <- TcM EvBindsVar
newTcEvBinds
       ; Bool
defer_errors <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_DeferTypeErrors
       ; Bool
warn_errors <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnDeferredTypeErrors -- implement #10283
       ; let type_errors :: TypeErrorChoice
type_errors | Bool -> Bool
not Bool
defer_errors = TypeErrorChoice
TypeError
                         | Bool
warn_errors      = WarnReason -> TypeErrorChoice
TypeWarn (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnDeferredTypeErrors)
                         | Bool
otherwise        = TypeErrorChoice
TypeDefer

       ; Bool
defer_holes <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_DeferTypedHoles
       ; Bool
warn_holes  <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnTypedHoles
       ; let expr_holes :: HoleChoice
expr_holes | Bool -> Bool
not Bool
defer_holes = HoleChoice
HoleError
                        | Bool
warn_holes      = HoleChoice
HoleWarn
                        | Bool
otherwise       = HoleChoice
HoleDefer

       ; Bool
partial_sigs      <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.PartialTypeSignatures
       ; Bool
warn_partial_sigs <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnPartialTypeSignatures
       ; let type_holes :: HoleChoice
type_holes | Bool -> Bool
not Bool
partial_sigs  = HoleChoice
HoleError
                        | Bool
warn_partial_sigs = HoleChoice
HoleWarn
                        | Bool
otherwise         = HoleChoice
HoleDefer

       ; Bool
defer_out_of_scope <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_DeferOutOfScopeVariables
       ; Bool
warn_out_of_scope <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnDeferredOutOfScopeVariables
       ; let out_of_scope_holes :: HoleChoice
out_of_scope_holes | Bool -> Bool
not Bool
defer_out_of_scope = HoleChoice
HoleError
                                | Bool
warn_out_of_scope      = HoleChoice
HoleWarn
                                | Bool
otherwise              = HoleChoice
HoleDefer

       ; TypeErrorChoice
-> HoleChoice
-> HoleChoice
-> HoleChoice
-> EvBindsVar
-> WantedConstraints
-> TcM ()
report_unsolved TypeErrorChoice
type_errors HoleChoice
expr_holes
                         HoleChoice
type_holes HoleChoice
out_of_scope_holes
                         EvBindsVar
binds_var WantedConstraints
wanted

       ; EvBindMap
ev_binds <- EvBindsVar -> TcM EvBindMap
getTcEvBindsMap EvBindsVar
binds_var
       ; Bag EvBind -> TcM (Bag EvBind)
forall (m :: * -> *) a. Monad m => a -> m a
return (EvBindMap -> Bag EvBind
evBindMapBinds EvBindMap
ev_binds)}

-- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
-- However, do not make any evidence bindings, because we don't
-- have any convenient place to put them.
-- NB: Type-level holes are OK, because there are no bindings.
-- See Note [Deferring coercion errors to runtime]
-- Used by solveEqualities for kind equalities
--      (see Note [Fail fast on kind errors] in "GHC.Tc.Solver")
reportAllUnsolved :: WantedConstraints -> TcM ()
reportAllUnsolved :: WantedConstraints -> TcM ()
reportAllUnsolved WantedConstraints
wanted
  = do { EvBindsVar
ev_binds <- TcM EvBindsVar
newNoTcEvBinds

       ; Bool
partial_sigs      <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.PartialTypeSignatures
       ; Bool
warn_partial_sigs <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnPartialTypeSignatures
       ; let type_holes :: HoleChoice
type_holes | Bool -> Bool
not Bool
partial_sigs  = HoleChoice
HoleError
                        | Bool
warn_partial_sigs = HoleChoice
HoleWarn
                        | Bool
otherwise         = HoleChoice
HoleDefer

       ; TypeErrorChoice
-> HoleChoice
-> HoleChoice
-> HoleChoice
-> EvBindsVar
-> WantedConstraints
-> TcM ()
report_unsolved TypeErrorChoice
TypeError HoleChoice
HoleError HoleChoice
type_holes HoleChoice
HoleError
                         EvBindsVar
ev_binds WantedConstraints
wanted }

-- | Report all unsolved goals as warnings (but without deferring any errors to
-- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
-- "GHC.Tc.Solver"
warnAllUnsolved :: WantedConstraints -> TcM ()
warnAllUnsolved :: WantedConstraints -> TcM ()
warnAllUnsolved WantedConstraints
wanted
  = do { EvBindsVar
ev_binds <- TcM EvBindsVar
newTcEvBinds
       ; TypeErrorChoice
-> HoleChoice
-> HoleChoice
-> HoleChoice
-> EvBindsVar
-> WantedConstraints
-> TcM ()
report_unsolved (WarnReason -> TypeErrorChoice
TypeWarn WarnReason
NoReason) HoleChoice
HoleWarn HoleChoice
HoleWarn HoleChoice
HoleWarn
                         EvBindsVar
ev_binds WantedConstraints
wanted }

-- | Report unsolved goals as errors or warnings.
report_unsolved :: TypeErrorChoice   -- Deferred type errors
                -> HoleChoice        -- Expression holes
                -> HoleChoice        -- Type holes
                -> HoleChoice        -- Out of scope holes
                -> EvBindsVar        -- cec_binds
                -> WantedConstraints -> TcM ()
report_unsolved :: TypeErrorChoice
-> HoleChoice
-> HoleChoice
-> HoleChoice
-> EvBindsVar
-> WantedConstraints
-> TcM ()
report_unsolved TypeErrorChoice
type_errors HoleChoice
expr_holes
    HoleChoice
type_holes HoleChoice
out_of_scope_holes EvBindsVar
binds_var WantedConstraints
wanted
  | WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { String -> SDoc -> TcM ()
traceTc String
"reportUnsolved {" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"type errors:" SDoc -> SDoc -> SDoc
<+> TypeErrorChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr TypeErrorChoice
type_errors
              , String -> SDoc
text String
"expr holes:" SDoc -> SDoc -> SDoc
<+> HoleChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleChoice
expr_holes
              , String -> SDoc
text String
"type holes:" SDoc -> SDoc -> SDoc
<+> HoleChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleChoice
type_holes
              , String -> SDoc
text String
"scope holes:" SDoc -> SDoc -> SDoc
<+> HoleChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleChoice
out_of_scope_holes ]
       ; String -> SDoc -> TcM ()
traceTc String
"reportUnsolved (before zonking and tidying)" (WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanted)

       ; WantedConstraints
wanted <- WantedConstraints -> TcM WantedConstraints
zonkWC WantedConstraints
wanted   -- Zonk to reveal all information
       ; let tidy_env :: TidyEnv
tidy_env = TidyEnv -> [TcId] -> TidyEnv
tidyFreeTyCoVars TidyEnv
emptyTidyEnv [TcId]
free_tvs
             free_tvs :: [TcId]
free_tvs = (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filterOut TcId -> Bool
isCoVar ([TcId] -> [TcId]) -> [TcId] -> [TcId]
forall a b. (a -> b) -> a -> b
$
                        WantedConstraints -> [TcId]
tyCoVarsOfWCList WantedConstraints
wanted
                        -- tyCoVarsOfWC returns free coercion *holes*, even though
                        -- they are "bound" by other wanted constraints. They in
                        -- turn may mention variables bound further in, which makes
                        -- no sense. Really we should not return those holes at all;
                        -- for now we just filter them out.

       ; String -> SDoc -> TcM ()
traceTc String
"reportUnsolved (after zonking):" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Free tyvars:" SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
pprTyVars [TcId]
free_tvs
              , String -> SDoc
text String
"Tidy env:" SDoc -> SDoc -> SDoc
<+> TidyEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TidyEnv
tidy_env
              , String -> SDoc
text String
"Wanted:" SDoc -> SDoc -> SDoc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanted ]

       ; Bool
warn_redundant <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnRedundantConstraints
       ; Bool
exp_syns <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_PrintExpandedSynonyms
       ; let err_ctxt :: ReportErrCtxt
err_ctxt = CEC { cec_encl :: [Implication]
cec_encl  = []
                            , cec_tidy :: TidyEnv
cec_tidy  = TidyEnv
tidy_env
                            , cec_defer_type_errors :: TypeErrorChoice
cec_defer_type_errors = TypeErrorChoice
type_errors
                            , cec_expr_holes :: HoleChoice
cec_expr_holes = HoleChoice
expr_holes
                            , cec_type_holes :: HoleChoice
cec_type_holes = HoleChoice
type_holes
                            , cec_out_of_scope_holes :: HoleChoice
cec_out_of_scope_holes = HoleChoice
out_of_scope_holes
                            , cec_suppress :: Bool
cec_suppress = WantedConstraints -> Bool
insolubleWC WantedConstraints
wanted
                                 -- See Note [Suppressing error messages]
                                 -- Suppress low-priority errors if there
                                 -- are insoluble errors anywhere;
                                 -- See #15539 and c.f. setting ic_status
                                 -- in GHC.Tc.Solver.setImplicationStatus
                            , cec_warn_redundant :: Bool
cec_warn_redundant = Bool
warn_redundant
                            , cec_expand_syns :: Bool
cec_expand_syns = Bool
exp_syns
                            , cec_binds :: EvBindsVar
cec_binds    = EvBindsVar
binds_var }

       ; TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
       ; ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds ReportErrCtxt
err_ctxt TcLevel
tc_lvl WantedConstraints
wanted
       ; String -> SDoc -> TcM ()
traceTc String
"reportUnsolved }" SDoc
empty }

--------------------------------------------
--      Internal functions
--------------------------------------------

-- | An error Report collects messages categorised by their importance.
-- See Note [Error report] for details.
data Report
  = Report { Report -> [SDoc]
report_important :: [SDoc]
           , Report -> [SDoc]
report_relevant_bindings :: [SDoc]
           , Report -> [SDoc]
report_valid_hole_fits :: [SDoc]
           }

instance Outputable Report where   -- Debugging only
  ppr :: Report -> SDoc
ppr (Report { report_important :: Report -> [SDoc]
report_important = [SDoc]
imp
              , report_relevant_bindings :: Report -> [SDoc]
report_relevant_bindings = [SDoc]
rel
              , report_valid_hole_fits :: Report -> [SDoc]
report_valid_hole_fits = [SDoc]
val })
    = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"important:" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [SDoc]
imp
           , String -> SDoc
text String
"relevant:"  SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [SDoc]
rel
           , String -> SDoc
text String
"valid:"  SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [SDoc]
val ]

{- Note [Error report]
The idea is that error msgs are divided into three parts: the main msg, the
context block (\"In the second argument of ...\"), and the relevant bindings
block, which are displayed in that order, with a mark to divide them.  The
idea is that the main msg ('report_important') varies depending on the error
in question, but context and relevant bindings are always the same, which
should simplify visual parsing.

The context is added when the Report is passed off to 'mkErrorReport'.
Unfortunately, unlike the context, the relevant bindings are added in
multiple places so they have to be in the Report.
-}

instance Semigroup Report where
    Report [SDoc]
a1 [SDoc]
b1 [SDoc]
c1 <> :: Report -> Report -> Report
<> Report [SDoc]
a2 [SDoc]
b2 [SDoc]
c2 = [SDoc] -> [SDoc] -> [SDoc] -> Report
Report ([SDoc]
a1 [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
a2) ([SDoc]
b1 [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
b2) ([SDoc]
c1 [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
c2)

instance Monoid Report where
    mempty :: Report
mempty = [SDoc] -> [SDoc] -> [SDoc] -> Report
Report [] [] []
    mappend :: Report -> Report -> Report
mappend = Report -> Report -> Report
forall a. Semigroup a => a -> a -> a
(Semigroup.<>)

-- | Put a doc into the important msgs block.
important :: SDoc -> Report
important :: SDoc -> Report
important SDoc
doc = Report
forall a. Monoid a => a
mempty { report_important :: [SDoc]
report_important = [SDoc
doc] }

-- | Put a doc into the relevant bindings block.
mk_relevant_bindings :: SDoc -> Report
mk_relevant_bindings :: SDoc -> Report
mk_relevant_bindings SDoc
doc = Report
forall a. Monoid a => a
mempty { report_relevant_bindings :: [SDoc]
report_relevant_bindings = [SDoc
doc] }

-- | Put a doc into the valid hole fits block.
valid_hole_fits :: SDoc -> Report
valid_hole_fits :: SDoc -> Report
valid_hole_fits SDoc
docs = Report
forall a. Monoid a => a
mempty { report_valid_hole_fits :: [SDoc]
report_valid_hole_fits = [SDoc
docs] }

data TypeErrorChoice   -- What to do for type errors found by the type checker
  = TypeError     -- A type error aborts compilation with an error message
  | TypeWarn WarnReason
                  -- A type error is deferred to runtime, plus a compile-time warning
                  -- The WarnReason should usually be (Reason Opt_WarnDeferredTypeErrors)
                  -- but it isn't for the Safe Haskell Overlapping Instances warnings
                  -- see warnAllUnsolved
  | TypeDefer     -- A type error is deferred to runtime; no error or warning at compile time

data HoleChoice
  = HoleError     -- A hole is a compile-time error
  | HoleWarn      -- Defer to runtime, emit a compile-time warning
  | HoleDefer     -- Defer to runtime, no warning

instance Outputable HoleChoice where
  ppr :: HoleChoice -> SDoc
ppr HoleChoice
HoleError = String -> SDoc
text String
"HoleError"
  ppr HoleChoice
HoleWarn  = String -> SDoc
text String
"HoleWarn"
  ppr HoleChoice
HoleDefer = String -> SDoc
text String
"HoleDefer"

instance Outputable TypeErrorChoice  where
  ppr :: TypeErrorChoice -> SDoc
ppr TypeErrorChoice
TypeError         = String -> SDoc
text String
"TypeError"
  ppr (TypeWarn WarnReason
reason) = String -> SDoc
text String
"TypeWarn" SDoc -> SDoc -> SDoc
<+> WarnReason -> SDoc
forall a. Outputable a => a -> SDoc
ppr WarnReason
reason
  ppr TypeErrorChoice
TypeDefer         = String -> SDoc
text String
"TypeDefer"

data ReportErrCtxt
    = CEC { ReportErrCtxt -> [Implication]
cec_encl :: [Implication]  -- Enclosing implications
                                       --   (innermost first)
                                       -- ic_skols and givens are tidied, rest are not
          , ReportErrCtxt -> TidyEnv
cec_tidy  :: TidyEnv

          , ReportErrCtxt -> EvBindsVar
cec_binds :: EvBindsVar    -- Make some errors (depending on cec_defer)
                                       -- into warnings, and emit evidence bindings
                                       -- into 'cec_binds' for unsolved constraints

          , ReportErrCtxt -> TypeErrorChoice
cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime

          -- cec_expr_holes is a union of:
          --   cec_type_holes - a set of typed holes: '_', '_a', '_foo'
          --   cec_out_of_scope_holes - a set of variables which are
          --                            out of scope: 'x', 'y', 'bar'
          , ReportErrCtxt -> HoleChoice
cec_expr_holes :: HoleChoice           -- Holes in expressions
          , ReportErrCtxt -> HoleChoice
cec_type_holes :: HoleChoice           -- Holes in types
          , ReportErrCtxt -> HoleChoice
cec_out_of_scope_holes :: HoleChoice   -- Out of scope holes

          , ReportErrCtxt -> Bool
cec_warn_redundant :: Bool    -- True <=> -Wredundant-constraints
          , ReportErrCtxt -> Bool
cec_expand_syns    :: Bool    -- True <=> -fprint-expanded-synonyms

          , ReportErrCtxt -> Bool
cec_suppress :: Bool    -- True <=> More important errors have occurred,
                                    --          so create bindings if need be, but
                                    --          don't issue any more errors/warnings
                                    -- See Note [Suppressing error messages]
      }

instance Outputable ReportErrCtxt where
  ppr :: ReportErrCtxt -> SDoc
ppr (CEC { cec_binds :: ReportErrCtxt -> EvBindsVar
cec_binds              = EvBindsVar
bvar
           , cec_defer_type_errors :: ReportErrCtxt -> TypeErrorChoice
cec_defer_type_errors  = TypeErrorChoice
dte
           , cec_expr_holes :: ReportErrCtxt -> HoleChoice
cec_expr_holes         = HoleChoice
eh
           , cec_type_holes :: ReportErrCtxt -> HoleChoice
cec_type_holes         = HoleChoice
th
           , cec_out_of_scope_holes :: ReportErrCtxt -> HoleChoice
cec_out_of_scope_holes = HoleChoice
osh
           , cec_warn_redundant :: ReportErrCtxt -> Bool
cec_warn_redundant     = Bool
wr
           , cec_expand_syns :: ReportErrCtxt -> Bool
cec_expand_syns        = Bool
es
           , cec_suppress :: ReportErrCtxt -> Bool
cec_suppress           = Bool
sup })
    = String -> SDoc
text String
"CEC" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
vcat
         [ String -> SDoc
text String
"cec_binds"              SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> EvBindsVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvBindsVar
bvar
         , String -> SDoc
text String
"cec_defer_type_errors"  SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> TypeErrorChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr TypeErrorChoice
dte
         , String -> SDoc
text String
"cec_expr_holes"         SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> HoleChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleChoice
eh
         , String -> SDoc
text String
"cec_type_holes"         SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> HoleChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleChoice
th
         , String -> SDoc
text String
"cec_out_of_scope_holes" SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> HoleChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleChoice
osh
         , String -> SDoc
text String
"cec_warn_redundant"     SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
wr
         , String -> SDoc
text String
"cec_expand_syns"        SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
es
         , String -> SDoc
text String
"cec_suppress"           SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
sup ])

-- | Returns True <=> the ReportErrCtxt indicates that something is deferred
deferringAnyBindings :: ReportErrCtxt -> Bool
  -- Don't check cec_type_holes, as these don't cause bindings to be deferred
deferringAnyBindings :: ReportErrCtxt -> Bool
deferringAnyBindings (CEC { cec_defer_type_errors :: ReportErrCtxt -> TypeErrorChoice
cec_defer_type_errors  = TypeErrorChoice
TypeError
                          , cec_expr_holes :: ReportErrCtxt -> HoleChoice
cec_expr_holes         = HoleChoice
HoleError
                          , cec_out_of_scope_holes :: ReportErrCtxt -> HoleChoice
cec_out_of_scope_holes = HoleChoice
HoleError }) = Bool
False
deferringAnyBindings ReportErrCtxt
_                                            = Bool
True

maybeSwitchOffDefer :: EvBindsVar -> ReportErrCtxt -> ReportErrCtxt
-- Switch off defer-type-errors inside CoEvBindsVar
-- See Note [Failing equalities with no evidence bindings]
maybeSwitchOffDefer :: EvBindsVar -> ReportErrCtxt -> ReportErrCtxt
maybeSwitchOffDefer EvBindsVar
evb ReportErrCtxt
ctxt
 | CoEvBindsVar{} <- EvBindsVar
evb
 = ReportErrCtxt
ctxt { cec_defer_type_errors :: TypeErrorChoice
cec_defer_type_errors  = TypeErrorChoice
TypeError
        , cec_expr_holes :: HoleChoice
cec_expr_holes         = HoleChoice
HoleError
        , cec_out_of_scope_holes :: HoleChoice
cec_out_of_scope_holes = HoleChoice
HoleError }
 | Bool
otherwise
 = ReportErrCtxt
ctxt

{- Note [Failing equalities with no evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we go inside an implication that has no term evidence
(e.g. unifying under a forall), we can't defer type errors.  You could
imagine using the /enclosing/ bindings (in cec_binds), but that may
not have enough stuff in scope for the bindings to be well typed.  So
we just switch off deferred type errors altogether.  See #14605.

This is done by maybeSwitchOffDefer.  It's also useful in one other
place: see Note [Wrapping failing kind equalities] in GHC.Tc.Solver.

Note [Suppressing error messages]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The cec_suppress flag says "don't report any errors".  Instead, just create
evidence bindings (as usual).  It's used when more important errors have occurred.

Specifically (see reportWanteds)
  * If there are insoluble Givens, then we are in unreachable code and all bets
    are off.  So don't report any further errors.
  * If there are any insolubles (eg Int~Bool), here or in a nested implication,
    then suppress errors from the simple constraints here.  Sometimes the
    simple-constraint errors are a knock-on effect of the insolubles.

This suppression behaviour is controlled by the Bool flag in
ReportErrorSpec, as used in reportWanteds.

But we need to take care: flags can turn errors into warnings, and we
don't want those warnings to suppress subsequent errors (including
suppressing the essential addTcEvBind for them: #15152). So in
tryReporter we use askNoErrs to see if any error messages were
/actually/ produced; if not, we don't switch on suppression.

A consequence is that warnings never suppress warnings, so turning an
error into a warning may allow subsequent warnings to appear that were
previously suppressed.   (e.g. partial-sigs/should_fail/T14584)
-}

reportImplic :: ReportErrCtxt -> Implication -> TcM ()
reportImplic :: ReportErrCtxt -> Implication -> TcM ()
reportImplic ReportErrCtxt
ctxt implic :: Implication
implic@(Implic { ic_skols :: Implication -> [TcId]
ic_skols = [TcId]
tvs
                                 , ic_given :: Implication -> [TcId]
ic_given = [TcId]
given
                                 , ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted, ic_binds :: Implication -> EvBindsVar
ic_binds = EvBindsVar
evb
                                 , ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
status, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
info
                                 , ic_tclvl :: Implication -> TcLevel
ic_tclvl = TcLevel
tc_lvl })
  | SkolemInfo
BracketSkol <- SkolemInfo
info
  , Bool -> Bool
not Bool
insoluble
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()        -- For Template Haskell brackets report only
                     -- definite errors. The whole thing will be re-checked
                     -- later when we plug it in, and meanwhile there may
                     -- certainly be un-satisfied constraints

  | Bool
otherwise
  = do { String -> SDoc -> TcM ()
traceTc String
"reportImplic" (Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr Implication
implic')
       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
bad_telescope (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcId] -> TcM ()
reportBadTelescope ReportErrCtxt
ctxt TcLclEnv
tcl_env SkolemInfo
info [TcId]
tvs
               -- Do /not/ use the tidied tvs because then are in the
               -- wrong order, so tidying will rename things wrongly
       ; ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds ReportErrCtxt
ctxt' TcLevel
tc_lvl WantedConstraints
wanted
       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReportErrCtxt -> Bool
cec_warn_redundant ReportErrCtxt
ctxt) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
         ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcId] -> TcM ()
warnRedundantConstraints ReportErrCtxt
ctxt' TcLclEnv
tcl_env SkolemInfo
info' [TcId]
dead_givens }
  where
    tcl_env :: TcLclEnv
tcl_env      = Implication -> TcLclEnv
ic_env Implication
implic
    insoluble :: Bool
insoluble    = ImplicStatus -> Bool
isInsolubleStatus ImplicStatus
status
    (TidyEnv
env1, [TcId]
tvs') = (TidyEnv -> TcId -> (TidyEnv, TcId))
-> TidyEnv -> [TcId] -> (TidyEnv, [TcId])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> TcId -> (TidyEnv, TcId)
tidyVarBndr (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt) ([TcId] -> (TidyEnv, [TcId])) -> [TcId] -> (TidyEnv, [TcId])
forall a b. (a -> b) -> a -> b
$
                   [TcId] -> [TcId]
scopedSort [TcId]
tvs
        -- scopedSort: the ic_skols may not be in dependency order
        -- (see Note [Skolems in an implication] in GHC.Tc.Types.Constraint)
        -- but tidying goes wrong on out-of-order constraints;
        -- so we sort them here before tidying
    info' :: SkolemInfo
info'   = TidyEnv -> SkolemInfo -> SkolemInfo
tidySkolemInfo TidyEnv
env1 SkolemInfo
info
    implic' :: Implication
implic' = Implication
implic { ic_skols :: [TcId]
ic_skols = [TcId]
tvs'
                     , ic_given :: [TcId]
ic_given = (TcId -> TcId) -> [TcId] -> [TcId]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> TcId -> TcId
tidyEvVar TidyEnv
env1) [TcId]
given
                     , ic_info :: SkolemInfo
ic_info  = SkolemInfo
info' }

    ctxt1 :: ReportErrCtxt
ctxt1 = EvBindsVar -> ReportErrCtxt -> ReportErrCtxt
maybeSwitchOffDefer EvBindsVar
evb ReportErrCtxt
ctxt
    ctxt' :: ReportErrCtxt
ctxt' = ReportErrCtxt
ctxt1 { cec_tidy :: TidyEnv
cec_tidy     = TidyEnv
env1
                  , cec_encl :: [Implication]
cec_encl     = Implication
implic' Implication -> [Implication] -> [Implication]
forall a. a -> [a] -> [a]
: ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt

                  , cec_suppress :: Bool
cec_suppress = Bool
insoluble Bool -> Bool -> Bool
|| ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt
                        -- Suppress inessential errors if there
                        -- are insolubles anywhere in the
                        -- tree rooted here, or we've come across
                        -- a suppress-worthy constraint higher up (#11541)

                  , cec_binds :: EvBindsVar
cec_binds    = EvBindsVar
evb }

    dead_givens :: [TcId]
dead_givens = case ImplicStatus
status of
                    IC_Solved { ics_dead :: ImplicStatus -> [TcId]
ics_dead = [TcId]
dead } -> [TcId]
dead
                    ImplicStatus
_                             -> []

    bad_telescope :: Bool
bad_telescope = case ImplicStatus
status of
              ImplicStatus
IC_BadTelescope -> Bool
True
              ImplicStatus
_               -> Bool
False

warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
-- See Note [Tracking redundant constraints] in GHC.Tc.Solver
warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcId] -> TcM ()
warnRedundantConstraints ReportErrCtxt
ctxt TcLclEnv
env SkolemInfo
info [TcId]
ev_vars
 | [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
redundant_evs
 = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

 | SigSkol {} <- SkolemInfo
info
 = TcLclEnv -> TcM () -> TcM ()
forall lcl' gbl a lcl.
lcl' -> TcRnIf gbl lcl' a -> TcRnIf gbl lcl a
setLclEnv TcLclEnv
env (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$  -- We want to add "In the type signature for f"
                    -- to the error context, which is a bit tiresome
   SDoc -> TcM () -> TcM ()
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (String -> SDoc
text String
"In" SDoc -> SDoc -> SDoc
<+> SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
info) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
   do { TcLclEnv
env <- TcRnIf TcGblEnv TcLclEnv TcLclEnv
forall gbl lcl. TcRnIf gbl lcl lcl
getLclEnv
      ; MsgEnvelope DecoratedSDoc
msg <- ReportErrCtxt
-> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
env (SDoc -> Report
important SDoc
doc)
      ; WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnRedundantConstraints) MsgEnvelope DecoratedSDoc
msg }

 | Bool
otherwise  -- But for InstSkol there already *is* a surrounding
              -- "In the instance declaration for Eq [a]" context
              -- and we don't want to say it twice. Seems a bit ad-hoc
 = do { MsgEnvelope DecoratedSDoc
msg <- ReportErrCtxt
-> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
env (SDoc -> Report
important SDoc
doc)
      ; WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnRedundantConstraints) MsgEnvelope DecoratedSDoc
msg }
 where
   doc :: SDoc
doc = String -> SDoc
text String
"Redundant constraint" SDoc -> SDoc -> SDoc
<> [TcId] -> SDoc
forall a. [a] -> SDoc
plural [TcId]
redundant_evs SDoc -> SDoc -> SDoc
<> SDoc
colon
         SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
pprEvVarTheta [TcId]
redundant_evs

   redundant_evs :: [TcId]
redundant_evs =
       (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filterOut TcId -> Bool
is_type_error ([TcId] -> [TcId]) -> [TcId] -> [TcId]
forall a b. (a -> b) -> a -> b
$
       case SkolemInfo
info of -- See Note [Redundant constraints in instance decls]
         SkolemInfo
InstSkol -> (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TcType -> Bool
improving (TcType -> Bool) -> (TcId -> TcType) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcId -> TcType
idType) [TcId]
ev_vars
         SkolemInfo
_        -> [TcId]
ev_vars

   -- See #15232
   is_type_error :: TcId -> Bool
is_type_error = Maybe TcType -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TcType -> Bool) -> (TcId -> Maybe TcType) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> Maybe TcType
userTypeError_maybe (TcType -> Maybe TcType)
-> (TcId -> TcType) -> TcId -> Maybe TcType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcId -> TcType
idType

   improving :: TcType -> Bool
improving TcType
pred -- (transSuperClasses p) does not include p
     = (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcType -> Bool
isImprovementPred (TcType
pred TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: TcType -> [TcType]
transSuperClasses TcType
pred)

reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcTyVar] -> TcM ()
reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcId] -> TcM ()
reportBadTelescope ReportErrCtxt
ctxt TcLclEnv
env (ForAllSkol SDoc
telescope) [TcId]
skols
  = do { MsgEnvelope DecoratedSDoc
msg <- ReportErrCtxt
-> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
env (SDoc -> Report
important SDoc
doc)
       ; MsgEnvelope DecoratedSDoc -> TcM ()
reportError MsgEnvelope DecoratedSDoc
msg }
  where
    doc :: SDoc
doc = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"These kind and type variables:" SDoc -> SDoc -> SDoc
<+> SDoc
telescope SDoc -> SDoc -> SDoc
$$
                String -> SDoc
text String
"are out of dependency order. Perhaps try this ordering:")
             Int
2 ([TcId] -> SDoc
pprTyVars [TcId]
sorted_tvs)

    sorted_tvs :: [TcId]
sorted_tvs = [TcId] -> [TcId]
scopedSort [TcId]
skols

reportBadTelescope ReportErrCtxt
_ TcLclEnv
_ SkolemInfo
skol_info [TcId]
skols
  = String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"reportBadTelescope" (SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info SDoc -> SDoc -> SDoc
$$ [TcId] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcId]
skols)

{- Note [Redundant constraints in instance decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For instance declarations, we don't report unused givens if
they can give rise to improvement.  Example (#10100):
    class Add a b ab | a b -> ab, a ab -> b
    instance Add Zero b b
    instance Add a b ab => Add (Succ a) b (Succ ab)
The context (Add a b ab) for the instance is clearly unused in terms
of evidence, since the dictionary has no fields.  But it is still
needed!  With the context, a wanted constraint
   Add (Succ Zero) beta (Succ Zero)
we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
But without the context we won't find beta := Zero.

This only matters in instance declarations..
-}

reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds ReportErrCtxt
ctxt TcLevel
tc_lvl (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics
                              , wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
  = do { String -> SDoc -> TcM ()
traceTc String
"reportWanteds" ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Simples =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
simples
                                       , String -> SDoc
text String
"Suppress =" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt)
                                       , String -> SDoc
text String
"tidy_cts =" SDoc -> SDoc -> SDoc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
tidy_cts
                                       , String -> SDoc
text String
"tidy_holes = " SDoc -> SDoc -> SDoc
<+> [Hole] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Hole]
tidy_holes ])

         -- First, deal with any out-of-scope errors:
       ; let ([Hole]
out_of_scope, [Hole]
other_holes) = (Hole -> Bool) -> [Hole] -> ([Hole], [Hole])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Hole -> Bool
isOutOfScopeHole [Hole]
tidy_holes
               -- don't suppress out-of-scope errors
             ctxt_for_scope_errs :: ReportErrCtxt
ctxt_for_scope_errs = ReportErrCtxt
ctxt { cec_suppress :: Bool
cec_suppress = Bool
False }
       ; (()
_, Bool
no_out_of_scope) <- TcM () -> TcRn ((), Bool)
forall a. TcRn a -> TcRn (a, Bool)
askNoErrs (TcM () -> TcRn ((), Bool)) -> TcM () -> TcRn ((), Bool)
forall a b. (a -> b) -> a -> b
$
                                 [Ct] -> ReportErrCtxt -> [Hole] -> TcM ()
reportHoles [Ct]
tidy_cts ReportErrCtxt
ctxt_for_scope_errs [Hole]
out_of_scope

         -- Next, deal with things that are utterly wrong
         -- Like Int ~ Bool (incl nullary TyCons)
         -- or  Int ~ t a   (AppTy on one side)
         -- These /ones/ are not suppressed by the incoming context
         -- (but will be by out-of-scope errors)
       ; let ctxt_for_insols :: ReportErrCtxt
ctxt_for_insols = ReportErrCtxt
ctxt { cec_suppress :: Bool
cec_suppress = Bool -> Bool
not Bool
no_out_of_scope }
       ; [Ct] -> ReportErrCtxt -> [Hole] -> TcM ()
reportHoles [Ct]
tidy_cts ReportErrCtxt
ctxt_for_insols [Hole]
other_holes
          -- holes never suppress

       ; (ReportErrCtxt
ctxt1, [Ct]
cts1) <- ReportErrCtxt
-> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporters ReportErrCtxt
ctxt_for_insols [ReporterSpec]
report1 [Ct]
tidy_cts

         -- Now all the other constraints.  We suppress errors here if
         -- any of the first batch failed, or if the enclosing context
         -- says to suppress
       ; let ctxt2 :: ReportErrCtxt
ctxt2 = ReportErrCtxt
ctxt { cec_suppress :: Bool
cec_suppress = ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt Bool -> Bool -> Bool
|| ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt1 }
       ; (ReportErrCtxt
_, [Ct]
leftovers) <- ReportErrCtxt
-> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporters ReportErrCtxt
ctxt2 [ReporterSpec]
report2 [Ct]
cts1
       ; MASSERT2( null leftovers, ppr leftovers )

            -- All the Derived ones have been filtered out of simples
            -- by the constraint solver. This is ok; we don't want
            -- to report unsolved Derived goals as errors
            -- See Note [Do not report derived but soluble errors]

     ; (Implication -> TcM ()) -> Bag Implication -> TcM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> Bag a -> m ()
mapBagM_ (ReportErrCtxt -> Implication -> TcM ()
reportImplic ReportErrCtxt
ctxt2) Bag Implication
implics }
            -- NB ctxt2: don't suppress inner insolubles if there's only a
            -- wanted insoluble here; but do suppress inner insolubles
            -- if there's a *given* insoluble here (= inaccessible code)
 where
    env :: TidyEnv
env = ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt
    tidy_cts :: [Ct]
tidy_cts   = Cts -> [Ct]
forall a. Bag a -> [a]
bagToList ((Ct -> Ct) -> Cts -> Cts
forall a b. (a -> b) -> Bag a -> Bag b
mapBag (TidyEnv -> Ct -> Ct
tidyCt TidyEnv
env)   Cts
simples)
    tidy_holes :: [Hole]
tidy_holes = Bag Hole -> [Hole]
forall a. Bag a -> [a]
bagToList ((Hole -> Hole) -> Bag Hole -> Bag Hole
forall a b. (a -> b) -> Bag a -> Bag b
mapBag (TidyEnv -> Hole -> Hole
tidyHole TidyEnv
env) Bag Hole
holes)

    -- report1: ones that should *not* be suppressed by
    --          an insoluble somewhere else in the tree
    -- It's crucial that anything that is considered insoluble
    -- (see GHC.Tc.Utils.insolubleCt) is caught here, otherwise
    -- we might suppress its error message, and proceed on past
    -- type checking to get a Lint error later
    report1 :: [ReporterSpec]
report1 = [ (String
"custom_error", (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
forall {p}. Ct -> p -> Bool
is_user_type_error, Bool
True,  Reporter
mkUserTypeErrorReporter)

              , ReporterSpec
given_eq_spec
              , (String
"insoluble2",   (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
forall {p}. p -> Pred -> Bool
utterly_wrong,  Bool
True, (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr)
              , (String
"skolem eq1",   (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
very_wrong,     Bool
True, Reporter
mkSkolReporter)
              , (String
"skolem eq2",   (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
skolem_eq,      Bool
True, Reporter
mkSkolReporter)
              , (String
"non-tv eq",    (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
forall {p}. p -> Pred -> Bool
non_tv_eq,      Bool
True, Reporter
mkSkolReporter)

                  -- The only remaining equalities are alpha ~ ty,
                  -- where alpha is untouchable; and representational equalities
                  -- Prefer homogeneous equalities over hetero, because the
                  -- former might be holding up the latter.
                  -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
              , (String
"Homo eqs",      (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
forall {p}. p -> Pred -> Bool
is_homo_equality, Bool
True,  (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr)
              , (String
"Other eqs",     (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
is_equality,      Bool
True,  (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr)
              , (String
"Blocked eqs",   Ct -> Pred -> Bool
is_equality,           Bool
False, (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkSuppressReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkBlockedEqErr)]

    -- report2: we suppress these if there are insolubles elsewhere in the tree
    report2 :: [ReporterSpec]
report2 = [ (String
"Implicit params", Ct -> Pred -> Bool
is_ip,           Bool
False, (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkIPErr)
              , (String
"Irreds",          Ct -> Pred -> Bool
is_irred,        Bool
False, (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkIrredErr)
              , (String
"Dicts",           Ct -> Pred -> Bool
is_dict,         Bool
False, (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkDictErr) ]

    -- also checks to make sure the constraint isn't HoleBlockerReason
    -- See TcCanonical Note [Equalities with incompatible kinds], (4)
    unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
    unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
_ (CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = HoleBlockerReason {}}) Pred
_ = Bool
False
    unblocked Ct -> Pred -> Bool
checker Ct
ct Pred
pred = Ct -> Pred -> Bool
checker Ct
ct Pred
pred

    -- rigid_nom_eq, rigid_nom_tv_eq,
    is_dict, is_equality, is_ip, is_irred :: Ct -> Pred -> Bool

    is_given_eq :: Ct -> Pred -> Bool
is_given_eq Ct
ct Pred
pred
       | EqPred {} <- Pred
pred = Ct -> Bool
arisesFromGivens Ct
ct
       | Bool
otherwise         = Bool
False
       -- I think all given residuals are equalities

    -- Things like (Int ~N Bool)
    utterly_wrong :: p -> Pred -> Bool
utterly_wrong p
_ (EqPred EqRel
NomEq TcType
ty1 TcType
ty2) = TcType -> Bool
isRigidTy TcType
ty1 Bool -> Bool -> Bool
&& TcType -> Bool
isRigidTy TcType
ty2
    utterly_wrong p
_ Pred
_                      = Bool
False

    -- Things like (a ~N Int)
    very_wrong :: Ct -> Pred -> Bool
very_wrong Ct
_ (EqPred EqRel
NomEq TcType
ty1 TcType
ty2) = TcLevel -> TcType -> Bool
isSkolemTy TcLevel
tc_lvl TcType
ty1 Bool -> Bool -> Bool
&& TcType -> Bool
isRigidTy TcType
ty2
    very_wrong Ct
_ Pred
_                      = Bool
False

    -- Things like (a ~N b) or (a  ~N  F Bool)
    skolem_eq :: Ct -> Pred -> Bool
skolem_eq Ct
_ (EqPred EqRel
NomEq TcType
ty1 TcType
_) = TcLevel -> TcType -> Bool
isSkolemTy TcLevel
tc_lvl TcType
ty1
    skolem_eq Ct
_ Pred
_                    = Bool
False

    -- Things like (F a  ~N  Int)
    non_tv_eq :: p -> Pred -> Bool
non_tv_eq p
_ (EqPred EqRel
NomEq TcType
ty1 TcType
_) = Bool -> Bool
not (TcType -> Bool
isTyVarTy TcType
ty1)
    non_tv_eq p
_ Pred
_                    = Bool
False

    is_user_type_error :: Ct -> p -> Bool
is_user_type_error Ct
ct p
_ = Ct -> Bool
isUserTypeErrorCt Ct
ct

    is_homo_equality :: p -> Pred -> Bool
is_homo_equality p
_ (EqPred EqRel
_ TcType
ty1 TcType
ty2) = HasDebugCallStack => TcType -> TcType
TcType -> TcType
tcTypeKind TcType
ty1 HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` HasDebugCallStack => TcType -> TcType
TcType -> TcType
tcTypeKind TcType
ty2
    is_homo_equality p
_ Pred
_                  = Bool
False

    is_equality :: Ct -> Pred -> Bool
is_equality Ct
_ (EqPred {}) = Bool
True
    is_equality Ct
_ Pred
_           = Bool
False

    is_dict :: Ct -> Pred -> Bool
is_dict Ct
_ (ClassPred {}) = Bool
True
    is_dict Ct
_ Pred
_              = Bool
False

    is_ip :: Ct -> Pred -> Bool
is_ip Ct
_ (ClassPred Class
cls [TcType]
_) = Class -> Bool
isIPClass Class
cls
    is_ip Ct
_ Pred
_                 = Bool
False

    is_irred :: Ct -> Pred -> Bool
is_irred Ct
_ (IrredPred {}) = Bool
True
    is_irred Ct
_ Pred
_              = Bool
False

    given_eq_spec :: ReporterSpec
given_eq_spec  -- See Note [Given errors]
      | [Implication] -> Bool
has_gadt_match (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt)
      = (String
"insoluble1a", Ct -> Pred -> Bool
is_given_eq, Bool
True,  Reporter
mkGivenErrorReporter)
      | Bool
otherwise
      = (String
"insoluble1b", Ct -> Pred -> Bool
is_given_eq, Bool
False, Reporter
ignoreErrorReporter)
          -- False means don't suppress subsequent errors
          -- Reason: we don't report all given errors
          --         (see mkGivenErrorReporter), and we should only suppress
          --         subsequent errors if we actually report this one!
          --         #13446 is an example

    -- See Note [Given errors]
    has_gadt_match :: [Implication] -> Bool
has_gadt_match [] = Bool
False
    has_gadt_match (Implication
implic : [Implication]
implics)
      | PatSkol {} <- Implication -> SkolemInfo
ic_info Implication
implic
      , Implication -> HasGivenEqs
ic_given_eqs Implication
implic HasGivenEqs -> HasGivenEqs -> Bool
forall a. Eq a => a -> a -> Bool
/= HasGivenEqs
NoGivenEqs
      , Implication -> Bool
ic_warn_inaccessible Implication
implic
          -- Don't bother doing this if -Winaccessible-code isn't enabled.
          -- See Note [Avoid -Winaccessible-code when deriving] in GHC.Tc.TyCl.Instance.
      = Bool
True
      | Bool
otherwise
      = [Implication] -> Bool
has_gadt_match [Implication]
implics

---------------
isSkolemTy :: TcLevel -> Type -> Bool
-- The type is a skolem tyvar
isSkolemTy :: TcLevel -> TcType -> Bool
isSkolemTy TcLevel
tc_lvl TcType
ty
  | Just TcId
tv <- TcType -> Maybe TcId
getTyVar_maybe TcType
ty
  =  TcId -> Bool
isSkolemTyVar TcId
tv
  Bool -> Bool -> Bool
|| (TcId -> Bool
isTyVarTyVar TcId
tv Bool -> Bool -> Bool
&& TcLevel -> TcId -> Bool
isTouchableMetaTyVar TcLevel
tc_lvl TcId
tv)
     -- The last case is for touchable TyVarTvs
     -- we postpone untouchables to a latter test (too obscure)

  | Bool
otherwise
  = Bool
False

isTyFun_maybe :: Type -> Maybe TyCon
isTyFun_maybe :: TcType -> Maybe TyCon
isTyFun_maybe TcType
ty = case HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty of
                      Just (TyCon
tc,[TcType]
_) | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tc
                      Maybe (TyCon, [TcType])
_ -> Maybe TyCon
forall a. Maybe a
Nothing

--------------------------------------------
--      Reporters
--------------------------------------------

type Reporter
  = ReportErrCtxt -> [Ct] -> TcM ()
type ReporterSpec
  = ( String                     -- Name
    , Ct -> Pred -> Bool         -- Pick these ones
    , Bool                       -- True <=> suppress subsequent reporters
    , Reporter)                  -- The reporter itself

mkSkolReporter :: Reporter
-- Suppress duplicates with either the same LHS, or same location
mkSkolReporter :: Reporter
mkSkolReporter ReportErrCtxt
ctxt [Ct]
cts
  = ([Ct] -> TcM ()) -> [[Ct]] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr ReportErrCtxt
ctxt) ([Ct] -> [[Ct]]
group [Ct]
cts)
  where
     group :: [Ct] -> [[Ct]]
group [] = []
     group (Ct
ct:[Ct]
cts) = (Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
yeses) [Ct] -> [[Ct]] -> [[Ct]]
forall a. a -> [a] -> [a]
: [Ct] -> [[Ct]]
group [Ct]
noes
        where
          ([Ct]
yeses, [Ct]
noes) = (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Ct -> Ct -> Bool
group_with Ct
ct) [Ct]
cts

     group_with :: Ct -> Ct -> Bool
group_with Ct
ct1 Ct
ct2
       | Ordering
EQ <- Ct -> Ct -> Ordering
cmp_loc Ct
ct1 Ct
ct2 = Bool
True
       | Ct -> Ct -> Bool
eq_lhs_type   Ct
ct1 Ct
ct2 = Bool
True
       | Bool
otherwise             = Bool
False

reportHoles :: [Ct]  -- other (tidied) constraints
            -> ReportErrCtxt -> [Hole] -> TcM ()
reportHoles :: [Ct] -> ReportErrCtxt -> [Hole] -> TcM ()
reportHoles [Ct]
tidy_cts ReportErrCtxt
ctxt
  = (Hole -> TcM ()) -> [Hole] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Hole -> TcM ()) -> [Hole] -> TcM ())
-> (Hole -> TcM ()) -> [Hole] -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Hole
hole -> Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportErrCtxt -> Hole -> Bool
ignoreThisHole ReportErrCtxt
ctxt Hole
hole) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
                     do { MsgEnvelope DecoratedSDoc
err <- [Ct] -> ReportErrCtxt -> Hole -> TcM (MsgEnvelope DecoratedSDoc)
mkHoleError [Ct]
tidy_cts ReportErrCtxt
ctxt Hole
hole
                        ; ReportErrCtxt -> Hole -> MsgEnvelope DecoratedSDoc -> TcM ()
maybeReportHoleError ReportErrCtxt
ctxt Hole
hole MsgEnvelope DecoratedSDoc
err
                        ; ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Hole -> TcM ()
maybeAddDeferredHoleBinding ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err Hole
hole }

ignoreThisHole :: ReportErrCtxt -> Hole -> Bool
-- See Note [Skip type holes rapidly]
ignoreThisHole :: ReportErrCtxt -> Hole -> Bool
ignoreThisHole ReportErrCtxt
ctxt Hole
hole
  = case Hole -> HoleSort
hole_sort Hole
hole of
       ExprHole {}    -> Bool
False
       HoleSort
TypeHole       -> Bool
ignore_type_hole
       HoleSort
ConstraintHole -> Bool
ignore_type_hole
  where
    ignore_type_hole :: Bool
ignore_type_hole = case ReportErrCtxt -> HoleChoice
cec_type_holes ReportErrCtxt
ctxt of
                         HoleChoice
HoleDefer -> Bool
True
                         HoleChoice
_         -> Bool
False

{- Note [Skip type holes rapidly]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have module with a /lot/ of partial type signatures, and we
compile it while suppressing partial-type-signature warnings.  Then
we don't want to spend ages constructing error messages and lists of
relevant bindings that we never display! This happened in #14766, in
which partial type signatures in a Happy-generated parser cause a huge
increase in compile time.

The function ignoreThisHole short-circuits the error/warning generation
machinery, in cases where it is definitely going to be a no-op.
-}

mkUserTypeErrorReporter :: Reporter
mkUserTypeErrorReporter :: Reporter
mkUserTypeErrorReporter ReportErrCtxt
ctxt
  = (Ct -> TcM ()) -> [Ct] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Ct -> TcM ()) -> [Ct] -> TcM ())
-> (Ct -> TcM ()) -> [Ct] -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Ct
ct -> do { MsgEnvelope DecoratedSDoc
err <- ReportErrCtxt -> Ct -> TcM (MsgEnvelope DecoratedSDoc)
mkUserTypeError ReportErrCtxt
ctxt Ct
ct
                      ; ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> TcM ()
maybeReportError ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err
                      ; ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err Ct
ct }

mkUserTypeError :: ReportErrCtxt -> Ct -> TcM (MsgEnvelope DecoratedSDoc)
mkUserTypeError :: ReportErrCtxt -> Ct -> TcM (MsgEnvelope DecoratedSDoc)
mkUserTypeError ReportErrCtxt
ctxt Ct
ct = ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct
                        (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$ SDoc -> Report
important
                        (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ TcType -> SDoc
pprUserTypeErrorTy
                        (TcType -> SDoc) -> TcType -> SDoc
forall a b. (a -> b) -> a -> b
$ case Ct -> Maybe TcType
getUserTypeErrorMsg Ct
ct of
                            Just TcType
msg -> TcType
msg
                            Maybe TcType
Nothing  -> String -> SDoc -> TcType
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkUserTypeError" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)


mkGivenErrorReporter :: Reporter
-- See Note [Given errors]
mkGivenErrorReporter :: Reporter
mkGivenErrorReporter ReportErrCtxt
ctxt [Ct]
cts
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg, Ct
ct) <- Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
True ReportErrCtxt
ctxt Ct
ct
       ; DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let (Implication
implic:[Implication]
_) = ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt
                 -- Always non-empty when mkGivenErrorReporter is called
             ct' :: Ct
ct' = Ct -> CtLoc -> Ct
setCtLoc Ct
ct (CtLoc -> TcLclEnv -> CtLoc
setCtLocEnv (Ct -> CtLoc
ctLoc Ct
ct) (Implication -> TcLclEnv
ic_env Implication
implic))
                   -- For given constraints we overwrite the env (and hence src-loc)
                   -- with one from the immediately-enclosing implication.
                   -- See Note [Inaccessible code]

             inaccessible_msg :: SDoc
inaccessible_msg = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Inaccessible code in")
                                   Int
2 (SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Implication -> SkolemInfo
ic_info Implication
implic))
             report :: Report
report = SDoc -> Report
important SDoc
inaccessible_msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend`
                      SDoc -> Report
mk_relevant_bindings SDoc
binds_msg

       ; MsgEnvelope DecoratedSDoc
err <- DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcType
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct' TcType
ty1 TcType
ty2

       ; String -> SDoc -> TcM ()
traceTc String
"mkGivenErrorReporter" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
       ; WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnInaccessibleCode) MsgEnvelope DecoratedSDoc
err }
  where
    (Ct
ct : [Ct]
_ )  = [Ct]
cts    -- Never empty
    (TcType
ty1, TcType
ty2) = TcType -> (TcType, TcType)
getEqPredTys (Ct -> TcType
ctPred Ct
ct)

ignoreErrorReporter :: Reporter
-- Discard Given errors that don't come from
-- a pattern match; maybe we should warn instead?
ignoreErrorReporter :: Reporter
ignoreErrorReporter ReportErrCtxt
ctxt [Ct]
cts
  = do { String -> SDoc -> TcM ()
traceTc String
"mkGivenErrorReporter no" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts SDoc -> SDoc -> SDoc
$$ [Implication] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt))
       ; () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }


{- Note [Given errors]
~~~~~~~~~~~~~~~~~~~~~~
Given constraints represent things for which we have (or will have)
evidence, so they aren't errors.  But if a Given constraint is
insoluble, this code is inaccessible, and we might want to at least
warn about that.  A classic case is

   data T a where
     T1 :: T Int
     T2 :: T a
     T3 :: T Bool

   f :: T Int -> Bool
   f T1 = ...
   f T2 = ...
   f T3 = ...  -- We want to report this case as inaccessible

We'd like to point out that the T3 match is inaccessible. It
will have a Given constraint [G] Int ~ Bool.

But we don't want to report ALL insoluble Given constraints.  See Trac
#12466 for a long discussion.  For example, if we aren't careful
we'll complain about
   f :: ((Int ~ Bool) => a -> a) -> Int
which arguably is OK.  It's more debatable for
   g :: (Int ~ Bool) => Int -> Int
but it's tricky to distinguish these cases so we don't report
either.

The bottom line is this: has_gadt_match looks for an enclosing
pattern match which binds some equality constraints.  If we
find one, we report the insoluble Given.
-}

mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
                             -- Make error message for a group
                -> Reporter  -- Deal with lots of constraints
-- Group together errors from same location,
-- and report only the first (to avoid a cascade)
mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt [Ct]
cts
  = (NonEmpty Ct -> TcM ()) -> [NonEmpty Ct] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt ([Ct] -> TcM ()) -> (NonEmpty Ct -> [Ct]) -> NonEmpty Ct -> TcM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Ct -> [Ct]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList) ((Ct -> Ct -> Ordering) -> [Ct] -> [NonEmpty Ct]
forall a. (a -> a -> Ordering) -> [a] -> [NonEmpty a]
equivClasses Ct -> Ct -> Ordering
cmp_loc [Ct]
cts)

-- Like mkGroupReporter, but doesn't actually print error messages
mkSuppressReporter :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)) -> Reporter
mkSuppressReporter :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
mkSuppressReporter ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt [Ct]
cts
  = (NonEmpty Ct -> TcM ()) -> [NonEmpty Ct] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
suppressGroup ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt ([Ct] -> TcM ()) -> (NonEmpty Ct -> [Ct]) -> NonEmpty Ct -> TcM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Ct -> [Ct]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList) ((Ct -> Ct -> Ordering) -> [Ct] -> [NonEmpty Ct]
forall a. (a -> a -> Ordering) -> [a] -> [NonEmpty a]
equivClasses Ct -> Ct -> Ordering
cmp_loc [Ct]
cts)

eq_lhs_type :: Ct -> Ct -> Bool
eq_lhs_type :: Ct -> Ct -> Bool
eq_lhs_type Ct
ct1 Ct
ct2
  = case (TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct1), TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct2)) of
       (EqPred EqRel
eq_rel1 TcType
ty1 TcType
_, EqPred EqRel
eq_rel2 TcType
ty2 TcType
_) ->
         (EqRel
eq_rel1 EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
eq_rel2) Bool -> Bool -> Bool
&& (TcType
ty1 TcType -> TcType -> Bool
`eqType` TcType
ty2)
       (Pred, Pred)
_ -> String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkSkolReporter" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct1 SDoc -> SDoc -> SDoc
$$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct2)

cmp_loc :: Ct -> Ct -> Ordering
cmp_loc :: Ct -> Ct -> Ordering
cmp_loc Ct
ct1 Ct
ct2 = Ct -> RealSrcLoc
get Ct
ct1 RealSrcLoc -> RealSrcLoc -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Ct -> RealSrcLoc
get Ct
ct2
  where
    get :: Ct -> RealSrcLoc
get Ct
ct = RealSrcSpan -> RealSrcLoc
realSrcSpanStart (CtLoc -> RealSrcSpan
ctLocSpan (Ct -> CtLoc
ctLoc Ct
ct))
             -- Reduce duplication by reporting only one error from each
             -- /starting/ location even if the end location differs

reportGroup :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)) -> Reporter
reportGroup :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt [Ct]
cts =
  ASSERT( not (null cts))
  do { MsgEnvelope DecoratedSDoc
err <- ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt [Ct]
cts
     ; String -> SDoc -> TcM ()
traceTc String
"About to maybeReportErr" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
       [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Constraint:"             SDoc -> SDoc -> SDoc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts
            , String -> SDoc
text String
"cec_suppress ="          SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt)
            , String -> SDoc
text String
"cec_defer_type_errors =" SDoc -> SDoc -> SDoc
<+> TypeErrorChoice -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ReportErrCtxt -> TypeErrorChoice
cec_defer_type_errors ReportErrCtxt
ctxt) ]
     ; ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> TcM ()
maybeReportError ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err
         -- But see Note [Always warn with -fdefer-type-errors]
     ; String -> SDoc -> TcM ()
traceTc String
"reportGroup" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts)
     ; (Ct -> TcM ()) -> [Ct] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err) [Ct]
cts }
         -- Add deferred bindings for all
         -- Redundant if we are going to abort compilation,
         -- but that's hard to know for sure, and if we don't
         -- abort, we need bindings for all (e.g. #12156)

-- like reportGroup, but does not actually report messages. It still adds
-- -fdefer-type-errors bindings, though.
suppressGroup :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)) -> Reporter
suppressGroup :: (ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc))
-> Reporter
suppressGroup ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt [Ct]
cts
 = do { MsgEnvelope DecoratedSDoc
err <- ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mk_err ReportErrCtxt
ctxt [Ct]
cts
      ; String -> SDoc -> TcM ()
traceTc String
"Suppressing errors for" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts)
      ; (Ct -> TcM ()) -> [Ct] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err) [Ct]
cts }

maybeReportHoleError :: ReportErrCtxt -> Hole -> MsgEnvelope DecoratedSDoc -> TcM ()
maybeReportHoleError :: ReportErrCtxt -> Hole -> MsgEnvelope DecoratedSDoc -> TcM ()
maybeReportHoleError ReportErrCtxt
ctxt Hole
hole MsgEnvelope DecoratedSDoc
err
  | Hole -> Bool
isOutOfScopeHole Hole
hole
  -- Always report an error for out-of-scope variables
  -- Unless -fdefer-out-of-scope-variables is on,
  -- in which case the messages are discarded.
  -- See #12170, #12406
  = -- If deferring, report a warning only if -Wout-of-scope-variables is on
    case ReportErrCtxt -> HoleChoice
cec_out_of_scope_holes ReportErrCtxt
ctxt of
      HoleChoice
HoleError -> MsgEnvelope DecoratedSDoc -> TcM ()
reportError MsgEnvelope DecoratedSDoc
err
      HoleChoice
HoleWarn  ->
        WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnDeferredOutOfScopeVariables) MsgEnvelope DecoratedSDoc
err
      HoleChoice
HoleDefer -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- Unlike maybeReportError, these "hole" errors are
-- /not/ suppressed by cec_suppress.  We want to see them!
maybeReportHoleError ReportErrCtxt
ctxt (Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
hole_sort }) MsgEnvelope DecoratedSDoc
err
  | case HoleSort
hole_sort of HoleSort
TypeHole       -> Bool
True
                      HoleSort
ConstraintHole -> Bool
True
                      HoleSort
_              -> Bool
False
  -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
  -- generated for holes in partial type signatures.
  -- Unless -fwarn-partial-type-signatures is not on,
  -- in which case the messages are discarded.
  = -- For partial type signatures, generate warnings only, and do that
    -- only if -fwarn-partial-type-signatures is on
    case ReportErrCtxt -> HoleChoice
cec_type_holes ReportErrCtxt
ctxt of
       HoleChoice
HoleError -> MsgEnvelope DecoratedSDoc -> TcM ()
reportError MsgEnvelope DecoratedSDoc
err
       HoleChoice
HoleWarn  -> WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnPartialTypeSignatures) MsgEnvelope DecoratedSDoc
err
       HoleChoice
HoleDefer -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

maybeReportHoleError ReportErrCtxt
ctxt Hole
hole MsgEnvelope DecoratedSDoc
err
  -- Otherwise this is a typed hole in an expression,
  -- but not for an out-of-scope variable (because that goes through a
  -- different function)
  = -- If deferring, report a warning only if -Wtyped-holes is on
    ASSERT( not (isOutOfScopeHole hole) )
    case ReportErrCtxt -> HoleChoice
cec_expr_holes ReportErrCtxt
ctxt of
       HoleChoice
HoleError -> MsgEnvelope DecoratedSDoc -> TcM ()
reportError MsgEnvelope DecoratedSDoc
err
       HoleChoice
HoleWarn  -> WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnTypedHoles) MsgEnvelope DecoratedSDoc
err
       HoleChoice
HoleDefer -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

maybeReportError :: ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> TcM ()
-- Report the error and/or make a deferred binding for it
maybeReportError :: ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> TcM ()
maybeReportError ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err
  | ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt    -- Some worse error has occurred;
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()            -- so suppress this error/warning

  | Bool
otherwise
  = case ReportErrCtxt -> TypeErrorChoice
cec_defer_type_errors ReportErrCtxt
ctxt of
      TypeErrorChoice
TypeDefer       -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      TypeWarn WarnReason
reason -> WarnReason -> MsgEnvelope DecoratedSDoc -> TcM ()
reportWarning WarnReason
reason MsgEnvelope DecoratedSDoc
err
      TypeErrorChoice
TypeError       -> MsgEnvelope DecoratedSDoc -> TcM ()
reportError MsgEnvelope DecoratedSDoc
err

addDeferredBinding :: ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Ct -> TcM ()
-- See Note [Deferring coercion errors to runtime]
addDeferredBinding :: ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err Ct
ct
  | ReportErrCtxt -> Bool
deferringAnyBindings ReportErrCtxt
ctxt
  , CtWanted { ctev_pred :: CtEvidence -> TcType
ctev_pred = TcType
pred, ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } <- Ct -> CtEvidence
ctEvidence Ct
ct
    -- Only add deferred bindings for Wanted constraints
  = do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let err_tm :: EvTerm
err_tm       = DynFlags -> TcType -> MsgEnvelope DecoratedSDoc -> EvTerm
mkErrorTerm DynFlags
dflags TcType
pred MsgEnvelope DecoratedSDoc
err
             ev_binds_var :: EvBindsVar
ev_binds_var = ReportErrCtxt -> EvBindsVar
cec_binds ReportErrCtxt
ctxt

       ; case TcEvDest
dest of
           EvVarDest TcId
evar
             -> EvBindsVar -> EvBind -> TcM ()
addTcEvBind EvBindsVar
ev_binds_var (EvBind -> TcM ()) -> EvBind -> TcM ()
forall a b. (a -> b) -> a -> b
$ TcId -> EvTerm -> EvBind
mkWantedEvBind TcId
evar EvTerm
err_tm
           HoleDest CoercionHole
hole
             -> do { -- See Note [Deferred errors for coercion holes]
                     let co_var :: TcId
co_var = CoercionHole -> TcId
coHoleCoVar CoercionHole
hole
                   ; EvBindsVar -> EvBind -> TcM ()
addTcEvBind EvBindsVar
ev_binds_var (EvBind -> TcM ()) -> EvBind -> TcM ()
forall a b. (a -> b) -> a -> b
$ TcId -> EvTerm -> EvBind
mkWantedEvBind TcId
co_var EvTerm
err_tm
                   ; CoercionHole -> Coercion -> TcM ()
fillCoercionHole CoercionHole
hole (TcId -> Coercion
mkTcCoVarCo TcId
co_var) }}

  | Bool
otherwise   -- Do not set any evidence for Given/Derived
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

mkErrorTerm :: DynFlags -> Type  -- of the error term
            -> MsgEnvelope DecoratedSDoc -> EvTerm
mkErrorTerm :: DynFlags -> TcType -> MsgEnvelope DecoratedSDoc -> EvTerm
mkErrorTerm DynFlags
dflags TcType
ty MsgEnvelope DecoratedSDoc
err = TcType -> FastString -> EvTerm
evDelayedError TcType
ty FastString
err_fs
  where
    err_msg :: SDoc
err_msg = MsgEnvelope DecoratedSDoc -> SDoc
forall e. RenderableDiagnostic e => MsgEnvelope e -> SDoc
pprLocMsgEnvelope MsgEnvelope DecoratedSDoc
err
    err_fs :: FastString
err_fs  = String -> FastString
mkFastString (String -> FastString) -> String -> FastString
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags (SDoc -> String) -> SDoc -> String
forall a b. (a -> b) -> a -> b
$
              SDoc
err_msg SDoc -> SDoc -> SDoc
$$ String -> SDoc
text String
"(deferred type error)"

maybeAddDeferredHoleBinding :: ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Hole -> TcM ()
maybeAddDeferredHoleBinding :: ReportErrCtxt -> MsgEnvelope DecoratedSDoc -> Hole -> TcM ()
maybeAddDeferredHoleBinding ReportErrCtxt
ctxt MsgEnvelope DecoratedSDoc
err (Hole { hole_sort :: Hole -> HoleSort
hole_sort = ExprHole (HER IORef EvTerm
ref TcType
ref_ty Unique
_) })
-- Only add bindings for holes in expressions
-- not for holes in partial type signatures
-- cf. addDeferredBinding
  | ReportErrCtxt -> Bool
deferringAnyBindings ReportErrCtxt
ctxt
  = do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let err_tm :: EvTerm
err_tm = DynFlags -> TcType -> MsgEnvelope DecoratedSDoc -> EvTerm
mkErrorTerm DynFlags
dflags TcType
ref_ty MsgEnvelope DecoratedSDoc
err
           -- NB: ref_ty, not hole_ty. hole_ty might be rewritten.
           -- See Note [Holes] in GHC.Tc.Types.Constraint
       ; IORef EvTerm -> EvTerm -> TcM ()
forall a env. IORef a -> a -> IOEnv env ()
writeMutVar IORef EvTerm
ref EvTerm
err_tm }
  | Bool
otherwise
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
maybeAddDeferredHoleBinding ReportErrCtxt
_ MsgEnvelope DecoratedSDoc
_ (Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
TypeHole })
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
maybeAddDeferredHoleBinding ReportErrCtxt
_ MsgEnvelope DecoratedSDoc
_ (Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
ConstraintHole })
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
-- Use the first reporter in the list whose predicate says True
tryReporters :: ReportErrCtxt
-> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporters ReportErrCtxt
ctxt [ReporterSpec]
reporters [Ct]
cts
  = do { let ([Ct]
vis_cts, [Ct]
invis_cts) = (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (CtOrigin -> Bool
isVisibleOrigin (CtOrigin -> Bool) -> (Ct -> CtOrigin) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtOrigin
ctOrigin) [Ct]
cts
       ; String -> SDoc -> TcM ()
traceTc String
"tryReporters {" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
vis_cts SDoc -> SDoc -> SDoc
$$ [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
invis_cts)
       ; (ReportErrCtxt
ctxt', [Ct]
cts') <- ReportErrCtxt
-> [ReporterSpec] -> [Ct] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
go ReportErrCtxt
ctxt [ReporterSpec]
reporters [Ct]
vis_cts [Ct]
invis_cts
       ; String -> SDoc -> TcM ()
traceTc String
"tryReporters }" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts')
       ; (ReportErrCtxt, [Ct]) -> TcM (ReportErrCtxt, [Ct])
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt', [Ct]
cts') }
  where
    go :: ReportErrCtxt
-> [ReporterSpec] -> [Ct] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
go ReportErrCtxt
ctxt [] [Ct]
vis_cts [Ct]
invis_cts
      = (ReportErrCtxt, [Ct]) -> TcM (ReportErrCtxt, [Ct])
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, [Ct]
vis_cts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
invis_cts)

    go ReportErrCtxt
ctxt (ReporterSpec
r : [ReporterSpec]
rs) [Ct]
vis_cts [Ct]
invis_cts
       -- always look at *visible* Origins before invisible ones
       -- this is the whole point of isVisibleOrigin
      = do { (ReportErrCtxt
ctxt', [Ct]
vis_cts') <- ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporter ReportErrCtxt
ctxt ReporterSpec
r [Ct]
vis_cts
           ; (ReportErrCtxt
ctxt'', [Ct]
invis_cts') <- ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporter ReportErrCtxt
ctxt' ReporterSpec
r [Ct]
invis_cts
           ; ReportErrCtxt
-> [ReporterSpec] -> [Ct] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
go ReportErrCtxt
ctxt'' [ReporterSpec]
rs [Ct]
vis_cts' [Ct]
invis_cts' }
                -- Carry on with the rest, because we must make
                -- deferred bindings for them if we have -fdefer-type-errors
                -- But suppress their error messages

tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
tryReporter ReportErrCtxt
ctxt (String
str, Ct -> Pred -> Bool
keep_me,  Bool
suppress_after, Reporter
reporter) [Ct]
cts
  | [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
yeses
  = (ReportErrCtxt, [Ct]) -> TcM (ReportErrCtxt, [Ct])
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, [Ct]
cts)
  | Bool
otherwise
  = do { String -> SDoc -> TcM ()
traceTc String
"tryReporter{ " (String -> SDoc
text String
str SDoc -> SDoc -> SDoc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
yeses)
       ; (()
_, Bool
no_errs) <- TcM () -> TcRn ((), Bool)
forall a. TcRn a -> TcRn (a, Bool)
askNoErrs (Reporter
reporter ReportErrCtxt
ctxt [Ct]
yeses)
       ; let suppress_now :: Bool
suppress_now = Bool -> Bool
not Bool
no_errs Bool -> Bool -> Bool
&& Bool
suppress_after
                            -- See Note [Suppressing error messages]
             ctxt' :: ReportErrCtxt
ctxt' = ReportErrCtxt
ctxt { cec_suppress :: Bool
cec_suppress = Bool
suppress_now Bool -> Bool -> Bool
|| ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt }
       ; String -> SDoc -> TcM ()
traceTc String
"tryReporter end }" (String -> SDoc
text String
str SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ReportErrCtxt -> Bool
cec_suppress ReportErrCtxt
ctxt) SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
suppress_after)
       ; (ReportErrCtxt, [Ct]) -> TcM (ReportErrCtxt, [Ct])
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt', [Ct]
nos) }
  where
    ([Ct]
yeses, [Ct]
nos) = (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\Ct
ct -> Ct -> Pred -> Bool
keep_me Ct
ct (TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct))) [Ct]
cts

pprArising :: CtOrigin -> SDoc
-- Used for the main, top-level error message
-- We've done special processing for TypeEq, KindEq, givens
pprArising :: CtOrigin -> SDoc
pprArising (TypeEqOrigin {})         = SDoc
empty
pprArising (KindEqOrigin {})         = SDoc
empty
pprArising CtOrigin
orig | CtOrigin -> Bool
isGivenOrigin CtOrigin
orig = SDoc
empty
                | Bool
otherwise          = CtOrigin -> SDoc
pprCtOrigin CtOrigin
orig

-- Add the "arising from..." part to a message about bunch of dicts
addArising :: CtOrigin -> SDoc -> SDoc
addArising :: CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig SDoc
msg = SDoc -> Int -> SDoc -> SDoc
hang SDoc
msg Int
2 (CtOrigin -> SDoc
pprArising CtOrigin
orig)

pprWithArising :: [Ct] -> (CtLoc, SDoc)
-- Print something like
--    (Eq a) arising from a use of x at y
--    (Show a) arising from a use of p at q
-- Also return a location for the error message
-- Works for Wanted/Derived only
pprWithArising :: [Ct] -> (CtLoc, SDoc)
pprWithArising []
  = String -> (CtLoc, SDoc)
forall a. String -> a
panic String
"pprWithArising"
pprWithArising (Ct
ct:[Ct]
cts)
  | [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
cts
  = (CtLoc
loc, CtOrigin -> SDoc -> SDoc
addArising (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc)
                     ([TcType] -> SDoc
pprTheta [Ct -> TcType
ctPred Ct
ct]))
  | Bool
otherwise
  = (CtLoc
loc, [SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
ppr_one (Ct
ctCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
cts)))
  where
    loc :: CtLoc
loc = Ct -> CtLoc
ctLoc Ct
ct
    ppr_one :: Ct -> SDoc
ppr_one Ct
ct' = SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> SDoc
parens (TcType -> SDoc
pprType (Ct -> TcType
ctPred Ct
ct')))
                     Int
2 (CtLoc -> SDoc
pprCtLoc (Ct -> CtLoc
ctLoc Ct
ct'))

mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct Report
report
  = ReportErrCtxt
-> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport ReportErrCtxt
ctxt (CtLoc -> TcLclEnv
ctLocEnv (Ct -> CtLoc
ctLoc Ct
ct)) Report
report

mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport :: ReportErrCtxt
-> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
tcl_env (Report [SDoc]
important [SDoc]
relevant_bindings [SDoc]
valid_subs)
  = do { SDoc
context <- TidyEnv -> [ErrCtxt] -> TcM SDoc
mkErrInfo (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt) (TcLclEnv -> [ErrCtxt]
tcl_ctxt TcLclEnv
tcl_env)
       ; SrcSpan -> SDoc -> SDoc -> SDoc -> TcM (MsgEnvelope DecoratedSDoc)
mkDecoratedSDocAt (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan (TcLclEnv -> RealSrcSpan
tcl_loc TcLclEnv
tcl_env) Maybe BufSpan
forall a. Maybe a
Nothing)
                           ([SDoc] -> SDoc
vcat [SDoc]
important)
                           SDoc
context
                           ([SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc]
relevant_bindings [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
valid_subs)
       }

type UserGiven = Implication

getUserGivens :: ReportErrCtxt -> [UserGiven]
-- One item for each enclosing implication
getUserGivens :: ReportErrCtxt -> [Implication]
getUserGivens (CEC {cec_encl :: ReportErrCtxt -> [Implication]
cec_encl = [Implication]
implics}) = [Implication] -> [Implication]
getUserGivensFromImplics [Implication]
implics

getUserGivensFromImplics :: [Implication] -> [UserGiven]
getUserGivensFromImplics :: [Implication] -> [Implication]
getUserGivensFromImplics [Implication]
implics
  = [Implication] -> [Implication]
forall a. [a] -> [a]
reverse ((Implication -> Bool) -> [Implication] -> [Implication]
forall a. (a -> Bool) -> [a] -> [a]
filterOut ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TcId] -> Bool) -> (Implication -> [TcId]) -> Implication -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Implication -> [TcId]
ic_given) [Implication]
implics)

{- Note [Always warn with -fdefer-type-errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When -fdefer-type-errors is on we warn about *all* type errors, even
if cec_suppress is on.  This can lead to a lot more warnings than you
would get errors without -fdefer-type-errors, but if we suppress any of
them you might get a runtime error that wasn't warned about at compile
time.

This is an easy design choice to change; just flip the order of the
first two equations for maybeReportError

To be consistent, we should also report multiple warnings from a single
location in mkGroupReporter, when -fdefer-type-errors is on.  But that
is perhaps a bit *over*-consistent! Again, an easy choice to change.

With #10283, you can now opt out of deferred type error warnings.

Note [Deferred errors for coercion holes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we need to defer a type error where the destination for the evidence
is a coercion hole. We can't just put the error in the hole, because we can't
make an erroneous coercion. (Remember that coercions are erased for runtime.)
Instead, we invent a new EvVar, bind it to an error and then make a coercion
from that EvVar, filling the hole with that coercion. Because coercions'
types are unlifted, the error is guaranteed to be hit before we get to the
coercion.

Note [Do not report derived but soluble errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The wc_simples include Derived constraints that have not been solved,
but are not insoluble (in that case they'd be reported by 'report1').
We do not want to report these as errors:

* Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
  an unsolved [D] Eq a, and we do not want to report that; it's just noise.

* Functional dependencies.  For givens, consider
      class C a b | a -> b
      data T a where
         MkT :: C a d => [d] -> T a
      f :: C a b => T a -> F Int
      f (MkT xs) = length xs
  Then we get a [D] b~d.  But there *is* a legitimate call to
  f, namely   f (MkT [True]) :: T Bool, in which b=d.  So we should
  not reject the program.

  For wanteds, something similar
      data T a where
        MkT :: C Int b => a -> b -> T a
      g :: C Int c => c -> ()
      f :: T a -> ()
      f (MkT x y) = g x
  Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
  But again f (MkT True True) is a legitimate call.

(We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
derived superclasses between iterations of the solver.)

For functional dependencies, here is a real example,
stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs

  class C a b | a -> b
  g :: C a b => a -> b -> ()
  f :: C a b => a -> b -> ()
  f xa xb =
      let loop = g xa
      in loop xb

We will first try to infer a type for loop, and we will succeed:
    C a b' => b' -> ()
Subsequently, we will type check (loop xb) and all is good. But,
recall that we have to solve a final implication constraint:
    C a b => (C a b' => .... cts from body of loop .... ))
And now we have a problem as we will generate an equality b ~ b' and fail to
solve it.


************************************************************************
*                                                                      *
                Irreducible predicate errors
*                                                                      *
************************************************************************
-}

mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkIrredErr ReportErrCtxt
ctxt [Ct]
cts
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg, Ct
ct1) <- Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
True ReportErrCtxt
ctxt Ct
ct1
       ; let orig :: CtOrigin
orig = Ct -> CtOrigin
ctOrigin Ct
ct1
             msg :: Report
msg  = [Implication] -> ([TcType], CtOrigin) -> Report
couldNotDeduce (ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt) ((Ct -> TcType) -> [Ct] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> TcType
ctPred [Ct]
cts, CtOrigin
orig)
       ; ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct1 (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$
         Report
msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend` SDoc -> Report
mk_relevant_bindings SDoc
binds_msg }
  where
    (Ct
ct1:[Ct]
_) = [Ct]
cts

----------------
mkHoleError :: [Ct] -> ReportErrCtxt -> Hole -> TcM (MsgEnvelope DecoratedSDoc)
mkHoleError :: [Ct] -> ReportErrCtxt -> Hole -> TcM (MsgEnvelope DecoratedSDoc)
mkHoleError [Ct]
_tidy_simples ReportErrCtxt
_ctxt hole :: Hole
hole@(Hole { hole_occ :: Hole -> OccName
hole_occ = OccName
occ
                                           , hole_ty :: Hole -> TcType
hole_ty = TcType
hole_ty
                                           , hole_loc :: Hole -> CtLoc
hole_loc = CtLoc
ct_loc })
  | Hole -> Bool
isOutOfScopeHole Hole
hole
  = do { DynFlags
dflags  <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; GlobalRdrEnv
rdr_env <- TcRn GlobalRdrEnv
getGlobalRdrEnv
       ; ImportAvails
imp_info <- TcRn ImportAvails
getImports
       ; Module
curr_mod <- IOEnv (Env TcGblEnv TcLclEnv) Module
forall (m :: * -> *). HasModule m => m Module
getModule
       ; HomePackageTable
hpt <- TcRnIf TcGblEnv TcLclEnv HomePackageTable
forall gbl lcl. TcRnIf gbl lcl HomePackageTable
getHpt
       ; SrcSpan -> SDoc -> SDoc -> SDoc -> TcM (MsgEnvelope DecoratedSDoc)
mkDecoratedSDocAt (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan (TcLclEnv -> RealSrcSpan
tcl_loc TcLclEnv
lcl_env) Maybe BufSpan
forall a. Maybe a
Nothing)
                           SDoc
out_of_scope_msg SDoc
O.empty
                           (DynFlags
-> HomePackageTable
-> Module
-> GlobalRdrEnv
-> LocalRdrEnv
-> ImportAvails
-> RdrName
-> SDoc
unknownNameSuggestions DynFlags
dflags HomePackageTable
hpt Module
curr_mod GlobalRdrEnv
rdr_env
                            (TcLclEnv -> LocalRdrEnv
tcl_rdr TcLclEnv
lcl_env) ImportAvails
imp_info (OccName -> RdrName
mkRdrUnqual OccName
occ)) }
  where
    herald :: SDoc
herald | OccName -> Bool
isDataOcc OccName
occ = String -> SDoc
text String
"Data constructor not in scope:"
           | Bool
otherwise     = String -> SDoc
text String
"Variable not in scope:"

    out_of_scope_msg :: SDoc
out_of_scope_msg -- Print v :: ty only if the type has structure
      | Bool
boring_type = SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald Int
2 (OccName -> SDoc
forall a. Outputable a => a -> SDoc
ppr OccName
occ)
      | Bool
otherwise   = SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald Int
2 (OccName -> TcType -> SDoc
pp_occ_with_type OccName
occ TcType
hole_ty)

    lcl_env :: TcLclEnv
lcl_env     = CtLoc -> TcLclEnv
ctLocEnv CtLoc
ct_loc
    boring_type :: Bool
boring_type = TcType -> Bool
isTyVarTy TcType
hole_ty

 -- general case: not an out-of-scope error
mkHoleError [Ct]
tidy_simples ReportErrCtxt
ctxt hole :: Hole
hole@(Hole { hole_occ :: Hole -> OccName
hole_occ = OccName
occ
                                         , hole_ty :: Hole -> TcType
hole_ty = TcType
hole_ty
                                         , hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
sort
                                         , hole_loc :: Hole -> CtLoc
hole_loc = CtLoc
ct_loc })
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg)
           <- Bool
-> ReportErrCtxt
-> TcLclEnv
-> TyCoVarSet
-> TcM (ReportErrCtxt, SDoc)
relevant_bindings Bool
False ReportErrCtxt
ctxt TcLclEnv
lcl_env (TcType -> TyCoVarSet
tyCoVarsOfType TcType
hole_ty)
               -- The 'False' means "don't filter the bindings"; see Trac #8191

       ; Bool
show_hole_constraints <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowHoleConstraints
       ; let constraints_msg :: SDoc
constraints_msg
               | ExprHole HoleExprRef
_ <- HoleSort
sort, Bool
show_hole_constraints
               = ReportErrCtxt -> SDoc
givenConstraintsMsg ReportErrCtxt
ctxt
               | Bool
otherwise
               = SDoc
empty

       ; Bool
show_valid_hole_fits <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowValidHoleFits
       ; (ReportErrCtxt
ctxt, SDoc
sub_msg) <- if Bool
show_valid_hole_fits
                            then ReportErrCtxt -> [Ct] -> Hole -> TcM (ReportErrCtxt, SDoc)
validHoleFits ReportErrCtxt
ctxt [Ct]
tidy_simples Hole
hole
                            else (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, SDoc
empty)

       ; ReportErrCtxt
-> TcLclEnv -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
lcl_env (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$
            SDoc -> Report
important SDoc
hole_msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend`
            SDoc -> Report
mk_relevant_bindings (SDoc
binds_msg SDoc -> SDoc -> SDoc
$$ SDoc
constraints_msg) Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend`
            SDoc -> Report
valid_hole_fits SDoc
sub_msg }

  where
    lcl_env :: TcLclEnv
lcl_env     = CtLoc -> TcLclEnv
ctLocEnv CtLoc
ct_loc
    hole_kind :: TcType
hole_kind   = HasDebugCallStack => TcType -> TcType
TcType -> TcType
tcTypeKind TcType
hole_ty
    tyvars :: [TcId]
tyvars      = TcType -> [TcId]
tyCoVarsOfTypeList TcType
hole_ty

    hole_msg :: SDoc
hole_msg = case HoleSort
sort of
      ExprHole HoleExprRef
_ -> [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Found hole:")
                            Int
2 (OccName -> TcType -> SDoc
pp_occ_with_type OccName
occ TcType
hole_ty)
                         , SDoc
tyvars_msg, SDoc
expr_hole_hint ]
      HoleSort
TypeHole -> [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Found type wildcard" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (OccName -> SDoc
forall a. Outputable a => a -> SDoc
ppr OccName
occ))
                            Int
2 (String -> SDoc
text String
"standing for" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes SDoc
pp_hole_type_with_kind)
                       , SDoc
tyvars_msg, SDoc
type_hole_hint ]
      HoleSort
ConstraintHole -> [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Found extra-constraints wildcard standing for")
                                  Int
2 (SDoc -> SDoc
quotes (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ TcType -> SDoc
pprType TcType
hole_ty)  -- always kind constraint
                             , SDoc
tyvars_msg, SDoc
type_hole_hint ]

    pp_hole_type_with_kind :: SDoc
pp_hole_type_with_kind
      | TcType -> Bool
isLiftedTypeKind TcType
hole_kind
        Bool -> Bool -> Bool
|| TcType -> Bool
isCoVarType TcType
hole_ty -- Don't print the kind of unlifted
                               -- equalities (#15039)
      = TcType -> SDoc
pprType TcType
hole_ty
      | Bool
otherwise
      = TcType -> SDoc
pprType TcType
hole_ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprKind TcType
hole_kind

    tyvars_msg :: SDoc
tyvars_msg = Bool -> SDoc -> SDoc
ppUnless ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
tyvars) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                 String -> SDoc
text String
"Where:" SDoc -> SDoc -> SDoc
<+> ([SDoc] -> SDoc
vcat ((TcId -> SDoc) -> [TcId] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map TcId -> SDoc
loc_msg [TcId]
other_tvs)
                                    SDoc -> SDoc -> SDoc
$$ ReportErrCtxt -> [TcId] -> SDoc
pprSkols ReportErrCtxt
ctxt [TcId]
skol_tvs)
       where
         ([TcId]
skol_tvs, [TcId]
other_tvs) = (TcId -> Bool) -> [TcId] -> ([TcId], [TcId])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition TcId -> Bool
is_skol [TcId]
tyvars
         is_skol :: TcId -> Bool
is_skol TcId
tv = TcId -> Bool
isTcTyVar TcId
tv Bool -> Bool -> Bool
&& TcId -> Bool
isSkolemTyVar TcId
tv
                      -- Coercion variables can be free in the
                      -- hole, via kind casts

    type_hole_hint :: SDoc
type_hole_hint
         | HoleChoice
HoleError <- ReportErrCtxt -> HoleChoice
cec_type_holes ReportErrCtxt
ctxt
         = String -> SDoc
text String
"To use the inferred type, enable PartialTypeSignatures"
         | Bool
otherwise
         = SDoc
empty

    expr_hole_hint :: SDoc
expr_hole_hint                       -- Give hint for, say,   f x = _x
         | FastString -> Int
lengthFS (OccName -> FastString
occNameFS OccName
occ) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1  -- Don't give this hint for plain "_"
         = String -> SDoc
text String
"Or perhaps" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (OccName -> SDoc
forall a. Outputable a => a -> SDoc
ppr OccName
occ)
           SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is mis-spelled, or not in scope"
         | Bool
otherwise
         = SDoc
empty

    loc_msg :: TcId -> SDoc
loc_msg TcId
tv
       | TcId -> Bool
isTyVar TcId
tv
       = case TcId -> TcTyVarDetails
tcTyVarDetails TcId
tv of
           MetaTv {} -> SDoc -> SDoc
quotes (TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is an ambiguous type variable"
           TcTyVarDetails
_         -> SDoc
empty  -- Skolems dealt with already
       | Bool
otherwise  -- A coercion variable can be free in the hole type
       = (SDocContext -> Bool) -> SDoc -> SDoc
ppWhenOption SDocContext -> Bool
sdocPrintExplicitCoercions (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
           SDoc -> SDoc
quotes (TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is a coercion variable"

pp_occ_with_type :: OccName -> Type -> SDoc
pp_occ_with_type :: OccName -> TcType -> SDoc
pp_occ_with_type OccName
occ TcType
hole_ty = SDoc -> Int -> SDoc -> SDoc
hang (OccName -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc OccName
occ) Int
2 (SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprType TcType
hole_ty)

-- We unwrap the ReportErrCtxt here, to avoid introducing a loop in module
-- imports
validHoleFits :: ReportErrCtxt -- The context we're in, i.e. the
                                        -- implications and the tidy environment
                       -> [Ct]          -- Unsolved simple constraints
                       -> Hole          -- The hole
                       -> TcM (ReportErrCtxt, SDoc) -- We return the new context
                                                    -- with a possibly updated
                                                    -- tidy environment, and
                                                    -- the message.
validHoleFits :: ReportErrCtxt -> [Ct] -> Hole -> TcM (ReportErrCtxt, SDoc)
validHoleFits ctxt :: ReportErrCtxt
ctxt@(CEC {cec_encl :: ReportErrCtxt -> [Implication]
cec_encl = [Implication]
implics
                             , cec_tidy :: ReportErrCtxt -> TidyEnv
cec_tidy = TidyEnv
lcl_env}) [Ct]
simps Hole
hole
  = do { (TidyEnv
tidy_env, SDoc
msg) <- TidyEnv -> [Implication] -> [Ct] -> Hole -> TcM (TidyEnv, SDoc)
findValidHoleFits TidyEnv
lcl_env [Implication]
implics [Ct]
simps Hole
hole
       ; (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt {cec_tidy :: TidyEnv
cec_tidy = TidyEnv
tidy_env}, SDoc
msg) }

-- See Note [Constraints include ...]
givenConstraintsMsg :: ReportErrCtxt -> SDoc
givenConstraintsMsg :: ReportErrCtxt -> SDoc
givenConstraintsMsg ReportErrCtxt
ctxt =
    let constraints :: [(Type, RealSrcSpan)]
        constraints :: [(TcType, RealSrcSpan)]
constraints =
          do { implic :: Implication
implic@Implic{ ic_given :: Implication -> [TcId]
ic_given = [TcId]
given } <- ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt
             ; TcId
constraint <- [TcId]
given
             ; (TcType, RealSrcSpan) -> [(TcType, RealSrcSpan)]
forall (m :: * -> *) a. Monad m => a -> m a
return (TcId -> TcType
varType TcId
constraint, TcLclEnv -> RealSrcSpan
tcl_loc (Implication -> TcLclEnv
ic_env Implication
implic)) }

        pprConstraint :: (a, a) -> SDoc
pprConstraint (a
constraint, a
loc) =
          a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
constraint SDoc -> SDoc -> SDoc
<+> Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc
parens (String -> SDoc
text String
"from" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
loc))

    in Bool -> SDoc -> SDoc
ppUnless ([(TcType, RealSrcSpan)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TcType, RealSrcSpan)]
constraints) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
         SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Constraints include")
            Int
2 ([SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ ((TcType, RealSrcSpan) -> SDoc)
-> [(TcType, RealSrcSpan)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TcType, RealSrcSpan) -> SDoc
forall {a} {a}. (Outputable a, Outputable a) => (a, a) -> SDoc
pprConstraint [(TcType, RealSrcSpan)]
constraints)

----------------
mkIPErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkIPErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkIPErr ReportErrCtxt
ctxt [Ct]
cts
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg, Ct
ct1) <- Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
True ReportErrCtxt
ctxt Ct
ct1
       ; let orig :: CtOrigin
orig    = Ct -> CtOrigin
ctOrigin Ct
ct1
             preds :: [TcType]
preds   = (Ct -> TcType) -> [Ct] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> TcType
ctPred [Ct]
cts
             givens :: [Implication]
givens  = ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt
             msg :: Report
msg | [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
givens
                 = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                   [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Unbound implicit parameter" SDoc -> SDoc -> SDoc
<> [Ct] -> SDoc
forall a. [a] -> SDoc
plural [Ct]
cts
                       , Int -> SDoc -> SDoc
nest Int
2 ([TcType] -> SDoc
pprParendTheta [TcType]
preds) ]
                 | Bool
otherwise
                 = [Implication] -> ([TcType], CtOrigin) -> Report
couldNotDeduce [Implication]
givens ([TcType]
preds, CtOrigin
orig)

       ; ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct1 (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$
         Report
msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend` SDoc -> Report
mk_relevant_bindings SDoc
binds_msg }
  where
    (Ct
ct1:[Ct]
_) = [Ct]
cts

{-
Note [Constraints include ...]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
-fshow-hole-constraints. For example, the following hole:

    foo :: (Eq a, Show a) => a -> String
    foo x = _

would generate the message:

    Constraints include
      Eq a (from foo.hs:1:1-36)
      Show a (from foo.hs:1:1-36)

Constraints are displayed in order from innermost (closest to the hole) to
outermost. There's currently no filtering or elimination of duplicates.

************************************************************************
*                                                                      *
                Equality errors
*                                                                      *
************************************************************************

Note [Inaccessible code]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   data T a where
     T1 :: T a
     T2 :: T Bool

   f :: (a ~ Int) => T a -> Int
   f T1 = 3
   f T2 = 4   -- Unreachable code

Here the second equation is unreachable. The original constraint
(a~Int) from the signature gets rewritten by the pattern-match to
(Bool~Int), so the danger is that we report the error as coming from
the *signature* (#7293).  So, for Given errors we replace the
env (and hence src-loc) on its CtLoc with that from the immediately
enclosing implication.

Note [Error messages for untouchables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#9109)
  data G a where { GBool :: G Bool }
  foo x = case x of GBool -> True

Here we can't solve (t ~ Bool), where t is the untouchable result
meta-var 't', because of the (a ~ Bool) from the pattern match.
So we infer the type
   f :: forall a t. G a -> t
making the meta-var 't' into a skolem.  So when we come to report
the unsolved (t ~ Bool), t won't look like an untouchable meta-var
any more.  So we don't assert that it is.
-}

-- Don't have multiple equality errors from the same location
-- E.g.   (Int,Bool) ~ (Bool,Int)   one error will do!
mkEqErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr ReportErrCtxt
ctxt (Ct
ct:[Ct]
_) = ReportErrCtxt -> Ct -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr1 ReportErrCtxt
ctxt Ct
ct
mkEqErr ReportErrCtxt
_ [] = String -> TcM (MsgEnvelope DecoratedSDoc)
forall a. String -> a
panic String
"mkEqErr"

mkEqErr1 :: ReportErrCtxt -> Ct -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr1 ReportErrCtxt
ctxt Ct
ct   -- Wanted or derived;
                   -- givens handled in mkGivenErrorReporter
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg, Ct
ct) <- Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
True ReportErrCtxt
ctxt Ct
ct
       ; GlobalRdrEnv
rdr_env <- TcRn GlobalRdrEnv
getGlobalRdrEnv
       ; FamInstEnvs
fam_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
       ; let coercible_msg :: SDoc
coercible_msg = case Ct -> EqRel
ctEqRel Ct
ct of
               EqRel
NomEq  -> SDoc
empty
               EqRel
ReprEq -> GlobalRdrEnv -> FamInstEnvs -> TcType -> TcType -> SDoc
mkCoercibleExplanation GlobalRdrEnv
rdr_env FamInstEnvs
fam_envs TcType
ty1 TcType
ty2
       ; DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; String -> SDoc -> TcM ()
traceTc String
"mkEqErr1" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
$$ CtOrigin -> SDoc
pprCtOrigin (Ct -> CtOrigin
ctOrigin Ct
ct))
       ; let report :: Report
report = [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [ SDoc -> Report
important SDoc
coercible_msg
                              , SDoc -> Report
mk_relevant_bindings SDoc
binds_msg]
       ; DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcType
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcType
ty1 TcType
ty2 }
  where
    (TcType
ty1, TcType
ty2) = TcType -> (TcType, TcType)
getEqPredTys (Ct -> TcType
ctPred Ct
ct)

-- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
-- is left over.
mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
                       -> TcType -> TcType -> SDoc
mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs -> TcType -> TcType -> SDoc
mkCoercibleExplanation GlobalRdrEnv
rdr_env FamInstEnvs
fam_envs TcType
ty1 TcType
ty2
  | Just (TyCon
tc, [TcType]
tys) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty1
  , (TyCon
rep_tc, [TcType]
_, Coercion
_) <- FamInstEnvs -> TyCon -> [TcType] -> (TyCon, [TcType], Coercion)
tcLookupDataFamInst FamInstEnvs
fam_envs TyCon
tc [TcType]
tys
  , Just SDoc
msg <- TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
rep_tc
  = SDoc
msg
  | Just (TyCon
tc, [TcType]
tys) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
splitTyConApp_maybe TcType
ty2
  , (TyCon
rep_tc, [TcType]
_, Coercion
_) <- FamInstEnvs -> TyCon -> [TcType] -> (TyCon, [TcType], Coercion)
tcLookupDataFamInst FamInstEnvs
fam_envs TyCon
tc [TcType]
tys
  , Just SDoc
msg <- TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
rep_tc
  = SDoc
msg
  | Just (TcType
s1, TcType
_) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty1
  , Just (TcType
s2, TcType
_) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty2
  , TcType
s1 TcType -> TcType -> Bool
`eqType` TcType
s2
  , TcType -> Bool
has_unknown_roles TcType
s1
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"NB: We cannot know what roles the parameters to" SDoc -> SDoc -> SDoc
<+>
          SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
s1) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"have;")
       Int
2 (String -> SDoc
text String
"we must assume that the role is nominal")
  | Bool
otherwise
  = SDoc
empty
  where
    coercible_msg_for_tycon :: TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
tc
        | TyCon -> Bool
isAbstractTyCon TyCon
tc
        = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (SDoc -> Maybe SDoc) -> SDoc -> Maybe SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
hsep [ String -> SDoc
text String
"NB: The type constructor"
                      , SDoc -> SDoc
quotes (TyCon -> SDoc
pprSourceTyCon TyCon
tc)
                      , String -> SDoc
text String
"is abstract" ]
        | TyCon -> Bool
isNewTyCon TyCon
tc
        , [DataCon
data_con] <- TyCon -> [DataCon]
tyConDataCons TyCon
tc
        , let dc_name :: Name
dc_name = DataCon -> Name
dataConName DataCon
data_con
        , Maybe GlobalRdrElt -> Bool
forall a. Maybe a -> Bool
isNothing (GlobalRdrEnv -> Name -> Maybe GlobalRdrElt
lookupGRE_Name GlobalRdrEnv
rdr_env Name
dc_name)
        = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (SDoc -> Maybe SDoc) -> SDoc -> Maybe SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"The data constructor" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
dc_name))
                    Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"of newtype" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
pprSourceTyCon TyCon
tc)
                           , String -> SDoc
text String
"is not in scope" ])
        | Bool
otherwise = Maybe SDoc
forall a. Maybe a
Nothing

    has_unknown_roles :: TcType -> Bool
has_unknown_roles TcType
ty
      | Just (TyCon
tc, [TcType]
tys) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty
      = [TcType]
tys [TcType] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` TyCon -> Int
tyConArity TyCon
tc  -- oversaturated tycon
      | Just (TcType
s, TcType
_) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty
      = TcType -> Bool
has_unknown_roles TcType
s
      | TcType -> Bool
isTyVarTy TcType
ty
      = Bool
True
      | Bool
otherwise
      = Bool
False

mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
             -> Ct
             -> TcType -> TcType -> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr_help :: DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcType
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcType
ty1 TcType
ty2
  | Just (TcId
tv1, Coercion
_) <- TcType -> Maybe (TcId, Coercion)
tcGetCastedTyVar_maybe TcType
ty1
  = DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcId
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 TcType
ty2
  | Just (TcId
tv2, Coercion
_) <- TcType -> Maybe (TcId, Coercion)
tcGetCastedTyVar_maybe TcType
ty2
  = DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcId
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv2 TcType
ty1
  | Bool
otherwise
  = ReportErrCtxt
-> Report
-> Ct
-> TcType
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct TcType
ty1 TcType
ty2

reportEqErr :: ReportErrCtxt -> Report
            -> Ct
            -> TcType -> TcType -> TcM (MsgEnvelope DecoratedSDoc)
reportEqErr :: ReportErrCtxt
-> Report
-> Ct
-> TcType
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct TcType
ty1 TcType
ty2
  = ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct ([Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [Report
misMatch, Report
report, Report
eqInfo])
  where
    misMatch :: Report
misMatch = Bool -> ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchOrCND Bool
False ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
    eqInfo :: Report
eqInfo   = Ct -> TcType -> TcType -> Report
mkEqInfoMsg Ct
ct TcType
ty1 TcType
ty2

mkTyVarEqErr, mkTyVarEqErr'
  :: DynFlags -> ReportErrCtxt -> Report -> Ct
             -> TcTyVar -> TcType -> TcM (MsgEnvelope DecoratedSDoc)
-- tv1 and ty2 are already tidied
mkTyVarEqErr :: DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcId
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 TcType
ty2
  = do { String -> SDoc -> TcM ()
traceTc String
"mkTyVarEqErr" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
$$ TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv1 SDoc -> SDoc -> SDoc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
       ; DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcId
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkTyVarEqErr' DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 TcType
ty2 }

mkTyVarEqErr' :: DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> TcId
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
mkTyVarEqErr' DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 TcType
ty2
     -- impredicativity is a simple error to understand; try it first
  | CheckTyEqResult
check_eq_result CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
cteImpredicative
  = let msg :: SDoc
msg = [SDoc] -> SDoc
vcat [ (if TcId -> Bool
isSkolemTyVar TcId
tv1
                      then String -> SDoc
text String
"Cannot equate type variable"
                      else String -> SDoc
text String
"Cannot instantiate unification variable")
                     SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv1)
                   , SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"with a" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"involving polytypes:") Int
2 (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2) ]
    in
       -- Unlike the other reports, this discards the old 'report_important'
       -- instead of augmenting it.  This is because the details are not likely
       -- to be helpful since this is just an unimplemented feature.
    ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat
        [ Report
headline_msg
        , SDoc -> Report
important SDoc
msg
        , if TcId -> Bool
isSkolemTyVar TcId
tv1 then ReportErrCtxt -> TcId -> TcType -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 TcType
ty2 else Report
forall a. Monoid a => a
mempty
        , Report
report ]

  | TcId -> Bool
isSkolemTyVar TcId
tv1  -- ty2 won't be a meta-tyvar; we would have
                       -- swapped in Solver.Canonical.canEqTyVarHomo
    Bool -> Bool -> Bool
|| TcId -> Bool
isTyVarTyVar TcId
tv1 Bool -> Bool -> Bool
&& Bool -> Bool
not (TcType -> Bool
isTyVarTy TcType
ty2)
    Bool -> Bool -> Bool
|| Ct -> EqRel
ctEqRel Ct
ct EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
ReprEq
     -- The cases below don't really apply to ReprEq (except occurs check)
  = ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat
        [ Report
headline_msg
        , ReportErrCtxt -> TcId -> TcType -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 TcType
ty2
        , ReportErrCtxt -> TcType -> TcType -> Report
suggestAddSig ReportErrCtxt
ctxt TcType
ty1 TcType
ty2
        , Report
report
        ]

  | CheckTyEqResult -> Bool
cterHasOccursCheck CheckTyEqResult
check_eq_result
    -- We report an "occurs check" even for  a ~ F t a, where F is a type
    -- function; it's not insoluble (because in principle F could reduce)
    -- but we have certainly been unable to solve it
    -- See Note [Occurs check error] in GHC.Tc.Solver.Canonical
  = do { let extra2 :: Report
extra2   = Ct -> TcType -> TcType -> Report
mkEqInfoMsg Ct
ct TcType
ty1 TcType
ty2

             interesting_tyvars :: [TcId]
interesting_tyvars = (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TcId -> Bool) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> Bool
noFreeVarsOfType (TcType -> Bool) -> (TcId -> TcType) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcId -> TcType
tyVarKind) ([TcId] -> [TcId]) -> [TcId] -> [TcId]
forall a b. (a -> b) -> a -> b
$
                                  (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filter TcId -> Bool
isTyVar ([TcId] -> [TcId]) -> [TcId] -> [TcId]
forall a b. (a -> b) -> a -> b
$
                                  FV -> [TcId]
fvVarList (FV -> [TcId]) -> FV -> [TcId]
forall a b. (a -> b) -> a -> b
$
                                  TcType -> FV
tyCoFVsOfType TcType
ty1 FV -> FV -> FV
`unionFV` TcType -> FV
tyCoFVsOfType TcType
ty2
             extra3 :: Report
extra3 = SDoc -> Report
mk_relevant_bindings (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$
                      Bool -> SDoc -> SDoc
ppWhen (Bool -> Bool
not ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
interesting_tyvars)) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                      SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Type variable kinds:") Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                      [SDoc] -> SDoc
vcat ((TcId -> SDoc) -> [TcId] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TcId -> SDoc
tyvar_binding (TcId -> SDoc) -> (TcId -> TcId) -> TcId -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TidyEnv -> TcId -> TcId
tidyTyCoVarOcc (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt))
                                [TcId]
interesting_tyvars)

             tyvar_binding :: TcId -> SDoc
tyvar_binding TcId
tv = TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcId -> TcType
tyVarKind TcId
tv)
       ; ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$
         [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [Report
headline_msg, Report
extra2, Report
extra3, Report
report] }

  -- If the immediately-enclosing implication has 'tv' a skolem, and
  -- we know by now its an InferSkol kind of skolem, then presumably
  -- it started life as a TyVarTv, else it'd have been unified, given
  -- that there's no occurs-check or forall problem
  | (Implication
implic:[Implication]
_) <- ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt
  , Implic { ic_skols :: Implication -> [TcId]
ic_skols = [TcId]
skols } <- Implication
implic
  , TcId
tv1 TcId -> [TcId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TcId]
skols
  = ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat
        [ ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
        , ReportErrCtxt -> TcId -> TcType -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 TcType
ty2
        , Report
report
        ]

  -- Check for skolem escape
  | (Implication
implic:[Implication]
_) <- ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt   -- Get the innermost context
  , Implic { ic_skols :: Implication -> [TcId]
ic_skols = [TcId]
skols, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info } <- Implication
implic
  , let esc_skols :: [TcId]
esc_skols = (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filter (TcId -> TyCoVarSet -> Bool
`elemVarSet` (TcType -> TyCoVarSet
tyCoVarsOfType TcType
ty2)) [TcId]
skols
  , Bool -> Bool
not ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
esc_skols)
  = do { let msg :: Report
msg = ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
             esc_doc :: SDoc
esc_doc = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"because" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"variable" SDoc -> SDoc -> SDoc
<> [TcId] -> SDoc
forall a. [a] -> SDoc
plural [TcId]
esc_skols
                             SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TcId]
esc_skols
                           , String -> SDoc
text String
"would escape" SDoc -> SDoc -> SDoc
<+>
                             if [TcId] -> Bool
forall a. [a] -> Bool
isSingleton [TcId]
esc_skols then String -> SDoc
text String
"its scope"
                                                      else String -> SDoc
text String
"their scope" ]
             tv_extra :: Report
tv_extra = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$
                        [SDoc] -> SDoc
vcat [ Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
esc_doc
                             , [SDoc] -> SDoc
sep [ (if [TcId] -> Bool
forall a. [a] -> Bool
isSingleton [TcId]
esc_skols
                                      then String -> SDoc
text String
"This (rigid, skolem)" SDoc -> SDoc -> SDoc
<+>
                                           SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"variable is"
                                      else String -> SDoc
text String
"These (rigid, skolem)" SDoc -> SDoc -> SDoc
<+>
                                           SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"variables are")
                               SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"bound by"
                             , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info
                             , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+>
                               RealSrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcLclEnv -> RealSrcSpan
tcl_loc (Implication -> TcLclEnv
ic_env Implication
implic)) ] ]
       ; ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct ([Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [Report
msg, Report
tv_extra, Report
report]) }

  -- Nastiest case: attempt to unify an untouchable variable
  -- So tv is a meta tyvar (or started that way before we
  -- generalised it).  So presumably it is an *untouchable*
  -- meta tyvar or a TyVarTv, else it'd have been unified
  -- See Note [Error messages for untouchables]
  | (Implication
implic:[Implication]
_) <- ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt   -- Get the innermost context
  , Implic { ic_given :: Implication -> [TcId]
ic_given = [TcId]
given, ic_tclvl :: Implication -> TcLevel
ic_tclvl = TcLevel
lvl, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info } <- Implication
implic
  = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
           , ppr tv1 $$ ppr lvl )  -- See Note [Error messages for untouchables]
    do { let msg :: Report
msg = ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
             tclvl_extra :: Report
tclvl_extra = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$
                  Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                  [SDoc] -> SDoc
sep [ SDoc -> SDoc
quotes (TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv1) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is untouchable"
                      , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"inside the constraints:" SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
pprEvVarTheta [TcId]
given
                      , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"bound by" SDoc -> SDoc -> SDoc
<+> SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info
                      , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+>
                        RealSrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcLclEnv -> RealSrcSpan
tcl_loc (Implication -> TcLclEnv
ic_env Implication
implic)) ]
             tv_extra :: Report
tv_extra = ReportErrCtxt -> TcId -> TcType -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 TcType
ty2
             add_sig :: Report
add_sig  = ReportErrCtxt -> TcType -> TcType -> Report
suggestAddSig ReportErrCtxt
ctxt TcType
ty1 TcType
ty2
       ; ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM (MsgEnvelope DecoratedSDoc))
-> Report -> TcM (MsgEnvelope DecoratedSDoc)
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat
            [Report
msg, Report
tclvl_extra, Report
tv_extra, Report
add_sig, Report
report] }

  | Bool
otherwise
  = ReportErrCtxt
-> Report
-> Ct
-> TcType
-> TcType
-> TcM (MsgEnvelope DecoratedSDoc)
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct (TcId -> TcType
mkTyVarTy TcId
tv1) TcType
ty2
        -- This *can* happen (#6123)
        -- Consider an ambiguous top-level constraint (a ~ F a)
        -- Not an occurs check, because F is a type function.
  where
    headline_msg :: Report
headline_msg = Bool -> ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchOrCND Bool
insoluble_occurs_check ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2

    ty1 :: TcType
ty1 = TcId -> TcType
mkTyVarTy TcId
tv1

    check_eq_result :: CheckTyEqResult
check_eq_result = case Ct
ct of
      CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = NonCanonicalReason CheckTyEqResult
result } -> CheckTyEqResult
result
      CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = HoleBlockerReason {} }      -> CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteHoleBlocker
      Ct
_ -> DynFlags -> TcId -> TcType -> CheckTyEqResult
checkTyVarEq DynFlags
dflags TcId
tv1 TcType
ty2
        -- in T2627b, we report an error for F (F a0) ~ a0. Note that the type
        -- variable is on the right, so we don't get useful info for the CIrredCan,
        -- and have to compute the result of checkTyVarEq here.


    insoluble_occurs_check :: Bool
insoluble_occurs_check = CheckTyEqResult
check_eq_result CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
cteInsolubleOccurs

    what :: SDoc
what = String -> SDoc
text (String -> SDoc) -> String -> SDoc
forall a b. (a -> b) -> a -> b
$ TypeOrKind -> String
levelString (TypeOrKind -> String) -> TypeOrKind -> String
forall a b. (a -> b) -> a -> b
$
           CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe (Ct -> CtLoc
ctLoc Ct
ct) Maybe TypeOrKind -> TypeOrKind -> TypeOrKind
forall a. Maybe a -> a -> a
`orElse` TypeOrKind
TypeLevel

levelString :: TypeOrKind -> String
levelString :: TypeOrKind -> String
levelString TypeOrKind
TypeLevel = String
"type"
levelString TypeOrKind
KindLevel = String
"kind"

mkEqInfoMsg :: Ct -> TcType -> TcType -> Report
-- Report (a) ambiguity if either side is a type function application
--            e.g. F a0 ~ Int
--        (b) warning about injectivity if both sides are the same
--            type function application   F a ~ F b
--            See Note [Non-injective type functions]
mkEqInfoMsg :: Ct -> TcType -> TcType -> Report
mkEqInfoMsg Ct
ct TcType
ty1 TcType
ty2
  = SDoc -> Report
important (SDoc
tyfun_msg SDoc -> SDoc -> SDoc
$$ SDoc
ambig_msg)
  where
    mb_fun1 :: Maybe TyCon
mb_fun1 = TcType -> Maybe TyCon
isTyFun_maybe TcType
ty1
    mb_fun2 :: Maybe TyCon
mb_fun2 = TcType -> Maybe TyCon
isTyFun_maybe TcType
ty2

    ambig_msg :: SDoc
ambig_msg | Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust Maybe TyCon
mb_fun1 Bool -> Bool -> Bool
|| Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust Maybe TyCon
mb_fun2
              = (Bool, SDoc) -> SDoc
forall a b. (a, b) -> b
snd (Bool -> Ct -> (Bool, SDoc)
mkAmbigMsg Bool
False Ct
ct)
              | Bool
otherwise = SDoc
empty

    tyfun_msg :: SDoc
tyfun_msg | Just TyCon
tc1 <- Maybe TyCon
mb_fun1
              , Just TyCon
tc2 <- Maybe TyCon
mb_fun2
              , TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
              , Bool -> Bool
not (TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
Nominal)
              = String -> SDoc
text String
"NB:" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1)
                SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is a non-injective type family"
              | Bool
otherwise = SDoc
empty

misMatchOrCND :: Bool -> ReportErrCtxt -> Ct
              -> TcType -> TcType -> Report
-- If oriented then ty1 is actual, ty2 is expected
misMatchOrCND :: Bool -> ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchOrCND Bool
insoluble_occurs_check ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
  | Bool
insoluble_occurs_check  -- See Note [Insoluble occurs check]
    Bool -> Bool -> Bool
|| (TcType -> Bool
isRigidTy TcType
ty1 Bool -> Bool -> Bool
&& TcType -> Bool
isRigidTy TcType
ty2)
    Bool -> Bool -> Bool
|| Ct -> Bool
isGivenCt Ct
ct
    Bool -> Bool -> Bool
|| [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
givens
  = -- If the equality is unconditionally insoluble
    -- or there is no context, don't report the context
    ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2

  | Bool
otherwise
  = [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [ [Implication] -> ([TcType], CtOrigin) -> Report
couldNotDeduce [Implication]
givens ([TcType
eq_pred], CtOrigin
orig)
            , SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> TypeOrKind -> TcType -> TcType -> CtOrigin -> SDoc
mk_supplementary_ea_msg ReportErrCtxt
ctxt TypeOrKind
level TcType
ty1 TcType
ty2 CtOrigin
orig ]
  where
    ev :: CtEvidence
ev      = Ct -> CtEvidence
ctEvidence Ct
ct
    eq_pred :: TcType
eq_pred = CtEvidence -> TcType
ctEvPred CtEvidence
ev
    orig :: CtOrigin
orig    = CtEvidence -> CtOrigin
ctEvOrigin CtEvidence
ev
    level :: TypeOrKind
level   = CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) Maybe TypeOrKind -> TypeOrKind -> TypeOrKind
forall a. Maybe a -> a -> a
`orElse` TypeOrKind
TypeLevel
    givens :: [Implication]
givens  = [ Implication
given | Implication
given <- ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt, Implication -> HasGivenEqs
ic_given_eqs Implication
given HasGivenEqs -> HasGivenEqs -> Bool
forall a. Eq a => a -> a -> Bool
/= HasGivenEqs
NoGivenEqs ]
              -- Keep only UserGivens that have some equalities.
              -- See Note [Suppress redundant givens during error reporting]

couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> Report
couldNotDeduce :: [Implication] -> ([TcType], CtOrigin) -> Report
couldNotDeduce [Implication]
givens ([TcType]
wanteds, CtOrigin
orig)
  = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$
    [SDoc] -> SDoc
vcat [ CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (String -> SDoc
text String
"Could not deduce:" SDoc -> SDoc -> SDoc
<+> [TcType] -> SDoc
pprTheta [TcType]
wanteds)
         , [SDoc] -> SDoc
vcat ([Implication] -> [SDoc]
pp_givens [Implication]
givens)]

pp_givens :: [UserGiven] -> [SDoc]
pp_givens :: [Implication] -> [SDoc]
pp_givens [Implication]
givens
   = case [Implication]
givens of
         []     -> []
         (Implication
g:[Implication]
gs) ->      SDoc -> Implication -> SDoc
ppr_given (String -> SDoc
text String
"from the context:") Implication
g
                 SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: (Implication -> SDoc) -> [Implication] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SDoc -> Implication -> SDoc
ppr_given (String -> SDoc
text String
"or from:")) [Implication]
gs
    where
       ppr_given :: SDoc -> Implication -> SDoc
ppr_given SDoc
herald implic :: Implication
implic@(Implic { ic_given :: Implication -> [TcId]
ic_given = [TcId]
gs, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info })
           = SDoc -> Int -> SDoc -> SDoc
hang (SDoc
herald SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
pprEvVarTheta ((TcId -> TcType) -> [TcId] -> [TcId]
forall a. (a -> TcType) -> [a] -> [a]
mkMinimalBySCs TcId -> TcType
evVarPred [TcId]
gs))
             -- See Note [Suppress redundant givens during error reporting]
             -- for why we use mkMinimalBySCs above.
                Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"bound by" SDoc -> SDoc -> SDoc
<+> SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info
                       , String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+> RealSrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcLclEnv -> RealSrcSpan
tcl_loc (Implication -> TcLclEnv
ic_env Implication
implic)) ])

-- These are for the "blocked" equalities, as described in TcCanonical
-- Note [Equalities with incompatible kinds], wrinkle (2). There should
-- always be another unsolved wanted around, which will ordinarily suppress
-- this message. But this can still be printed out with -fdefer-type-errors
-- (sigh), so we must produce a message.
mkBlockedEqErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkBlockedEqErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkBlockedEqErr ReportErrCtxt
ctxt (Ct
ct:[Ct]
_) = ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct Report
report
  where
    report :: Report
report = SDoc -> Report
important SDoc
msg
    msg :: SDoc
msg = [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Cannot use equality for substitution:")
                   Int
2 (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct -> TcType
ctPred Ct
ct))
               , String -> SDoc
text String
"Doing so would be ill-kinded." ]
          -- This is a terrible message. Perhaps worse, if the user
          -- has -fprint-explicit-kinds on, they will see that the two
          -- sides have the same kind, as there is an invisible cast.
          -- I really don't know how to do better.
mkBlockedEqErr ReportErrCtxt
_ [] = String -> TcM (MsgEnvelope DecoratedSDoc)
forall a. String -> a
panic String
"mkBlockedEqErr no constraints"

{-
Note [Suppress redundant givens during error reporting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When GHC is unable to solve a constraint and prints out an error message, it
will print out what given constraints are in scope to provide some context to
the programmer. But we shouldn't print out /every/ given, since some of them
are not terribly helpful to diagnose type errors. Consider this example:

  foo :: Int :~: Int -> a :~: b -> a :~: c
  foo Refl Refl = Refl

When reporting that GHC can't solve (a ~ c), there are two givens in scope:
(Int ~ Int) and (a ~ b). But (Int ~ Int) is trivially soluble (i.e.,
redundant), so it's not terribly useful to report it in an error message.
To accomplish this, we discard any Implications that do not bind any
equalities by filtering the `givens` selected in `misMatchOrCND` (based on
the `ic_given_eqs` field of the Implication). Note that we discard givens
that have no equalities whatsoever, but we want to keep ones with only *local*
equalities, as these may be helpful to the user in understanding what went
wrong.

But this is not enough to avoid all redundant givens! Consider this example,
from #15361:

  goo :: forall (a :: Type) (b :: Type) (c :: Type).
         a :~~: b -> a :~~: c
  goo HRefl = HRefl

Matching on HRefl brings the /single/ given (* ~ *, a ~ b) into scope.
The (* ~ *) part arises due the kinds of (:~~:) being unified. More
importantly, (* ~ *) is redundant, so we'd like not to report it. However,
the Implication (* ~ *, a ~ b) /does/ bind an equality (as reported by its
ic_given_eqs field), so the test above will keep it wholesale.

To refine this given, we apply mkMinimalBySCs on it to extract just the (a ~ b)
part. This works because mkMinimalBySCs eliminates reflexive equalities in
addition to superclasses (see Note [Remove redundant provided dicts]
in GHC.Tc.TyCl.PatSyn).
-}

extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> Report
-- Add on extra info about skolem constants
-- NB: The types themselves are already tidied
extraTyVarEqInfo :: ReportErrCtxt -> TcId -> TcType -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 TcType
ty2
  = SDoc -> Report
important (ReportErrCtxt -> TcId -> SDoc
extraTyVarInfo ReportErrCtxt
ctxt TcId
tv1 SDoc -> SDoc -> SDoc
$$ TcType -> SDoc
ty_extra TcType
ty2)
  where
    ty_extra :: TcType -> SDoc
ty_extra TcType
ty = case TcType -> Maybe (TcId, Coercion)
tcGetCastedTyVar_maybe TcType
ty of
                    Just (TcId
tv, Coercion
_) -> ReportErrCtxt -> TcId -> SDoc
extraTyVarInfo ReportErrCtxt
ctxt TcId
tv
                    Maybe (TcId, Coercion)
Nothing      -> SDoc
empty

extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
extraTyVarInfo :: ReportErrCtxt -> TcId -> SDoc
extraTyVarInfo ReportErrCtxt
ctxt TcId
tv
  = ASSERT2( isTyVar tv, ppr tv )
    case TcId -> TcTyVarDetails
tcTyVarDetails TcId
tv of
          SkolemTv {}   -> ReportErrCtxt -> [TcId] -> SDoc
pprSkols ReportErrCtxt
ctxt [TcId
tv]
          RuntimeUnk {} -> SDoc -> SDoc
quotes (TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
tv) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is an interactive-debugger skolem"
          MetaTv {}     -> SDoc
empty

suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report
-- See Note [Suggest adding a type signature]
suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report
suggestAddSig ReportErrCtxt
ctxt TcType
ty1 TcType
_ty2
  | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
inferred_bndrs   -- No let-bound inferred binders in context
  = Report
forall a. Monoid a => a
mempty
  | [Name
bndr] <- [Name]
inferred_bndrs
  = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Possible fix: add a type signature for" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
bndr)
  | Bool
otherwise
  = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Possible fix: add type signatures for some or all of" SDoc -> SDoc -> SDoc
<+> ([Name] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Name]
inferred_bndrs)
  where
    inferred_bndrs :: [Name]
inferred_bndrs = case TcType -> Maybe TcId
tcGetTyVar_maybe TcType
ty1 of
                       Just TcId
tv | TcId -> Bool
isSkolemTyVar TcId
tv -> [Implication] -> Bool -> TcId -> [Name]
find (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt) Bool
False TcId
tv
                       Maybe TcId
_                          -> []

    -- 'find' returns the binders of an InferSkol for 'tv',
    -- provided there is an intervening implication with
    -- ic_given_eqs /= NoGivenEqs (i.e. a GADT match)
    find :: [Implication] -> Bool -> TcId -> [Name]
find [] Bool
_ TcId
_ = []
    find (Implication
implic:[Implication]
implics) Bool
seen_eqs TcId
tv
       | TcId
tv TcId -> [TcId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Implication -> [TcId]
ic_skols Implication
implic
       , InferSkol [(Name, TcType)]
prs <- Implication -> SkolemInfo
ic_info Implication
implic
       , Bool
seen_eqs
       = ((Name, TcType) -> Name) -> [(Name, TcType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TcType) -> Name
forall a b. (a, b) -> a
fst [(Name, TcType)]
prs
       | Bool
otherwise
       = [Implication] -> Bool -> TcId -> [Name]
find [Implication]
implics (Bool
seen_eqs Bool -> Bool -> Bool
|| Implication -> HasGivenEqs
ic_given_eqs Implication
implic HasGivenEqs -> HasGivenEqs -> Bool
forall a. Eq a => a -> a -> Bool
/= HasGivenEqs
NoGivenEqs) TcId
tv

--------------------
misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report
-- Types are already tidy
-- If oriented then ty1 is actual, ty2 is expected
misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
  = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$
    CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
    TcType -> TcType -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch TcType
ty1 TcType
ty2 CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
    [SDoc] -> SDoc
sep [ case CtOrigin
orig of
            TypeEqOrigin {} -> ReportErrCtxt -> Ct -> TcType -> TcType -> CtOrigin -> SDoc
tk_eq_msg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2 CtOrigin
orig
            KindEqOrigin {} -> ReportErrCtxt -> Ct -> TcType -> TcType -> CtOrigin -> SDoc
tk_eq_msg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2 CtOrigin
orig
            CtOrigin
_ -> Bool -> Ct -> TcType -> TcType -> SDoc
headline_eq_msg Bool
False Ct
ct TcType
ty1 TcType
ty2
        , TcType -> TcType -> SDoc
sameOccExtra TcType
ty2 TcType
ty1 ]
  where
    orig :: CtOrigin
orig = Ct -> CtOrigin
ctOrigin Ct
ct

headline_eq_msg :: Bool -> Ct -> Type -> Type -> SDoc
-- Generates the main "Could't match 't1' against 't2'
-- headline message
headline_eq_msg :: Bool -> Ct -> TcType -> TcType -> SDoc
headline_eq_msg Bool
add_ea Ct
ct TcType
ty1 TcType
ty2

  | (TcType -> Bool
isLiftedRuntimeRep TcType
ty1 Bool -> Bool -> Bool
&& TcType -> Bool
isUnliftedRuntimeRep TcType
ty2) Bool -> Bool -> Bool
||
    (TcType -> Bool
isLiftedRuntimeRep TcType
ty2 Bool -> Bool -> Bool
&& TcType -> Bool
isUnliftedRuntimeRep TcType
ty1) Bool -> Bool -> Bool
||
    (TcType -> Bool
isLiftedLevity TcType
ty1 Bool -> Bool -> Bool
&& TcType -> Bool
isUnliftedLevity TcType
ty2) Bool -> Bool -> Bool
||
    (TcType -> Bool
isLiftedLevity TcType
ty2 Bool -> Bool -> Bool
&& TcType -> Bool
isUnliftedLevity TcType
ty1)
  = String -> SDoc
text String
"Couldn't match a lifted type with an unlifted type"

  | TcType -> Bool
isAtomicTy TcType
ty1 Bool -> Bool -> Bool
|| TcType -> Bool
isAtomicTy TcType
ty2
  = -- Print with quotes
    [SDoc] -> SDoc
sep [ String -> SDoc
text String
herald1 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1)
        , Int -> SDoc -> SDoc
nest Int
padding (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
          String -> SDoc
text String
herald2 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2) ]

  | Bool
otherwise
  = -- Print with vertical layout
    [SDoc] -> SDoc
vcat [ String -> SDoc
text String
herald1 SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1
         , Int -> SDoc -> SDoc
nest Int
padding (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
           String -> SDoc
text String
herald2 SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2 ]
  where
    herald1 :: String
herald1 = [String] -> String
conc [ String
"Couldn't match"
                   , if Bool
is_repr then String
"representation of" else String
""
                   , if Bool
add_ea then String
"expected"          else String
""
                   , String
what ]
    herald2 :: String
herald2 = [String] -> String
conc [ String
"with"
                   , if Bool
is_repr then String
"that of"          else String
""
                   , if Bool
add_ea then (String
"actual " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what) else String
"" ]

    padding :: Int
padding = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
herald1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
herald2

    is_repr :: Bool
is_repr = case Ct -> EqRel
ctEqRel Ct
ct of { EqRel
ReprEq -> Bool
True; EqRel
NomEq -> Bool
False }

    what :: String
what = TypeOrKind -> String
levelString (CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe (Ct -> CtLoc
ctLoc Ct
ct) Maybe TypeOrKind -> TypeOrKind -> TypeOrKind
forall a. Maybe a -> a -> a
`orElse` TypeOrKind
TypeLevel)

    conc :: [String] -> String
    conc :: [String] -> String
conc = (String -> String -> String) -> [String] -> String
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 String -> String -> String
add_space

    add_space :: String -> String -> String
    add_space :: String -> String -> String
add_space String
s1 String
s2 | String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s1   = String
s2
                    | String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s2   = String
s1
                    | Bool
otherwise = String
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char
' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s2)


tk_eq_msg :: ReportErrCtxt
          -> Ct -> Type -> Type -> CtOrigin -> SDoc
tk_eq_msg :: ReportErrCtxt -> Ct -> TcType -> TcType -> CtOrigin -> SDoc
tk_eq_msg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2 orig :: CtOrigin
orig@(TypeEqOrigin { uo_actual :: CtOrigin -> TcType
uo_actual = TcType
act
                                             , uo_expected :: CtOrigin -> TcType
uo_expected = TcType
exp
                                             , uo_thing :: CtOrigin -> Maybe SDoc
uo_thing = Maybe SDoc
mb_thing })
  -- We can use the TypeEqOrigin to
  -- improve the error message quite a lot

  | TcType -> Bool
isUnliftedTypeKind TcType
act, TcType -> Bool
isLiftedTypeKind TcType
exp
  = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Expecting a lifted type, but"
        , Maybe SDoc -> SDoc -> SDoc -> SDoc
thing_msg Maybe SDoc
mb_thing (String -> SDoc
text String
"an") (String -> SDoc
text String
"unlifted") ]

  | TcType -> Bool
isLiftedTypeKind TcType
act, TcType -> Bool
isUnliftedTypeKind TcType
exp
  = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Expecting an unlifted type, but"
        , Maybe SDoc -> SDoc -> SDoc -> SDoc
thing_msg Maybe SDoc
mb_thing (String -> SDoc
text String
"a") (String -> SDoc
text String
"lifted") ]

  | TcType -> Bool
tcIsLiftedTypeKind TcType
exp
  = SDoc
maybe_num_args_msg SDoc -> SDoc -> SDoc
$$
    [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Expected a type, but"
        , case Maybe SDoc
mb_thing of
            Maybe SDoc
Nothing    -> String -> SDoc
text String
"found something with kind"
            Just SDoc
thing -> SDoc -> SDoc
quotes SDoc
thing SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"has kind"
        , SDoc -> SDoc
quotes (TcType -> SDoc
pprWithTYPE TcType
act) ]

  | Just SDoc
nargs_msg <- Maybe SDoc
num_args_msg
  = SDoc
nargs_msg SDoc -> SDoc -> SDoc
$$
    ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
mk_ea_msg ReportErrCtxt
ctxt (Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct) TypeOrKind
level CtOrigin
orig

  | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $
    TcType -> TcType -> TcType -> TcType -> Bool
ea_looks_same TcType
ty1 TcType
ty2 TcType
exp TcType
act
  = ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
mk_ea_msg ReportErrCtxt
ctxt (Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct) TypeOrKind
level CtOrigin
orig

  | Bool
otherwise  -- The mismatched types are /inside/ exp and act
  = [SDoc] -> SDoc
vcat [ Bool -> Ct -> TcType -> TcType -> SDoc
headline_eq_msg Bool
False Ct
ct TcType
ty1 TcType
ty2
         , ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
mk_ea_msg ReportErrCtxt
ctxt Maybe Ct
forall a. Maybe a
Nothing TypeOrKind
level CtOrigin
orig ]

  where
    ct_loc :: CtLoc
ct_loc = Ct -> CtLoc
ctLoc Ct
ct
    level :: TypeOrKind
level  = CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe CtLoc
ct_loc Maybe TypeOrKind -> TypeOrKind -> TypeOrKind
forall a. Maybe a -> a -> a
`orElse` TypeOrKind
TypeLevel

    thing_msg :: Maybe SDoc -> SDoc -> SDoc -> SDoc
thing_msg (Just SDoc
thing) SDoc
_  SDoc
levity = SDoc -> SDoc
quotes SDoc
thing SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is" SDoc -> SDoc -> SDoc
<+> SDoc
levity
    thing_msg Maybe SDoc
Nothing      SDoc
an SDoc
levity = String -> SDoc
text String
"got" SDoc -> SDoc -> SDoc
<+> SDoc
an SDoc -> SDoc -> SDoc
<+> SDoc
levity SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"type"

    num_args_msg :: Maybe SDoc
num_args_msg = case TypeOrKind
level of
      TypeOrKind
KindLevel
        | Bool -> Bool
not (TcType -> Bool
isMetaTyVarTy TcType
exp) Bool -> Bool -> Bool
&& Bool -> Bool
not (TcType -> Bool
isMetaTyVarTy TcType
act)
           -- if one is a meta-tyvar, then it's possible that the user
           -- has asked for something impredicative, and we couldn't unify.
           -- Don't bother with counting arguments.
        -> let n_act :: Int
n_act = TcType -> Int
count_args TcType
act
               n_exp :: Int
n_exp = TcType -> Int
count_args TcType
exp in
           case Int
n_act Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n_exp of
             Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0   -- we don't know how many args there are, so don't
                         -- recommend removing args that aren't
               , Just SDoc
thing <- Maybe SDoc
mb_thing
               -> SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (SDoc -> Maybe SDoc) -> SDoc -> Maybe SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Expecting" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
speakN (Int -> Int
forall a. Num a => a -> a
abs Int
n) SDoc -> SDoc -> SDoc
<+>
                         SDoc
more SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes SDoc
thing
               where
                 more :: SDoc
more
                  | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1    = String -> SDoc
text String
"more argument to"
                  | Bool
otherwise = String -> SDoc
text String
"more arguments to"  -- n > 1
             Int
_ -> Maybe SDoc
forall a. Maybe a
Nothing

      TypeOrKind
_ -> Maybe SDoc
forall a. Maybe a
Nothing

    maybe_num_args_msg :: SDoc
maybe_num_args_msg = Maybe SDoc
num_args_msg Maybe SDoc -> SDoc -> SDoc
forall a. Maybe a -> a -> a
`orElse` SDoc
empty

    count_args :: TcType -> Int
count_args TcType
ty = (TyCoBinder -> Bool) -> [TyCoBinder] -> Int
forall a. (a -> Bool) -> [a] -> Int
count TyCoBinder -> Bool
isVisibleBinder ([TyCoBinder] -> Int) -> [TyCoBinder] -> Int
forall a b. (a -> b) -> a -> b
$ ([TyCoBinder], TcType) -> [TyCoBinder]
forall a b. (a, b) -> a
fst (([TyCoBinder], TcType) -> [TyCoBinder])
-> ([TyCoBinder], TcType) -> [TyCoBinder]
forall a b. (a -> b) -> a -> b
$ TcType -> ([TyCoBinder], TcType)
splitPiTys TcType
ty

tk_eq_msg ReportErrCtxt
ctxt Ct
ct TcType
ty1 TcType
ty2
          (KindEqOrigin TcType
cty1 TcType
cty2 CtOrigin
sub_o Maybe TypeOrKind
mb_sub_t_or_k)
  = [SDoc] -> SDoc
vcat [ Bool -> Ct -> TcType -> TcType -> SDoc
headline_eq_msg Bool
False Ct
ct TcType
ty1 TcType
ty2
         , SDoc
supplementary_msg ]
  where
    sub_t_or_k :: TypeOrKind
sub_t_or_k = Maybe TypeOrKind
mb_sub_t_or_k Maybe TypeOrKind -> TypeOrKind -> TypeOrKind
forall a. Maybe a -> a -> a
`orElse` TypeOrKind
TypeLevel
    sub_whats :: SDoc
sub_whats  = String -> SDoc
text (TypeOrKind -> String
levelString TypeOrKind
sub_t_or_k) SDoc -> SDoc -> SDoc
<> Char -> SDoc
char Char
's'
                 -- "types" or "kinds"

    supplementary_msg :: SDoc
supplementary_msg
      = (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocPrintExplicitCoercions ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \Bool
printExplicitCoercions ->
        if Bool
printExplicitCoercions
           Bool -> Bool -> Bool
|| Bool -> Bool
not (TcType
cty1 TcType -> TcType -> Bool
`pickyEqType` TcType
cty2)
          then [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"When matching" SDoc -> SDoc -> SDoc
<+> SDoc
sub_whats)
                          Int
2 ([SDoc] -> SDoc
vcat [ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
cty1 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>
                                   TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => TcType -> TcType
TcType -> TcType
tcTypeKind TcType
cty1)
                                 , TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
cty2 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>
                                   TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => TcType -> TcType
TcType -> TcType
tcTypeKind TcType
cty2) ])
                    , ReportErrCtxt -> TypeOrKind -> TcType -> TcType -> CtOrigin -> SDoc
mk_supplementary_ea_msg ReportErrCtxt
ctxt TypeOrKind
sub_t_or_k TcType
cty1 TcType
cty2 CtOrigin
sub_o ]
          else String -> SDoc
text String
"When matching the kind of" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
cty1)

tk_eq_msg ReportErrCtxt
_ Ct
_ TcType
_ TcType
_ CtOrigin
_ = String -> SDoc
forall a. String -> a
panic String
"typeeq_mismatch_msg"

ea_looks_same :: Type -> Type -> Type -> Type -> Bool
-- True if the faulting types (ty1, ty2) look the same as
-- the expected/actual types (exp, act).
-- If so, we don't want to redundantly report the latter
ea_looks_same :: TcType -> TcType -> TcType -> TcType -> Bool
ea_looks_same TcType
ty1 TcType
ty2 TcType
exp TcType
act
  = (TcType
act TcType -> TcType -> Bool
`looks_same` TcType
ty1 Bool -> Bool -> Bool
&& TcType
exp TcType -> TcType -> Bool
`looks_same` TcType
ty2) Bool -> Bool -> Bool
||
    (TcType
exp TcType -> TcType -> Bool
`looks_same` TcType
ty1 Bool -> Bool -> Bool
&& TcType
act TcType -> TcType -> Bool
`looks_same` TcType
ty2)
  where
    looks_same :: TcType -> TcType -> Bool
looks_same TcType
t1 TcType
t2 = TcType
t1 TcType -> TcType -> Bool
`pickyEqType` TcType
t2
                    Bool -> Bool -> Bool
|| TcType
t1 TcType -> TcType -> Bool
`eqType` TcType
liftedTypeKind Bool -> Bool -> Bool
&& TcType
t2 TcType -> TcType -> Bool
`eqType` TcType
liftedTypeKind
      -- pickyEqType is sensitive to synonyms, so only replies True
      -- when the types really look the same.  However,
      -- (TYPE 'LiftedRep) and Type both print the same way.

mk_supplementary_ea_msg :: ReportErrCtxt -> TypeOrKind
                        -> Type -> Type -> CtOrigin -> SDoc
mk_supplementary_ea_msg :: ReportErrCtxt -> TypeOrKind -> TcType -> TcType -> CtOrigin -> SDoc
mk_supplementary_ea_msg ReportErrCtxt
ctxt TypeOrKind
level TcType
ty1 TcType
ty2 CtOrigin
orig
  | TypeEqOrigin { uo_expected :: CtOrigin -> TcType
uo_expected = TcType
exp, uo_actual :: CtOrigin -> TcType
uo_actual = TcType
act } <- CtOrigin
orig
  , Bool -> Bool
not (TcType -> TcType -> TcType -> TcType -> Bool
ea_looks_same TcType
ty1 TcType
ty2 TcType
exp TcType
act)
  = ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
mk_ea_msg ReportErrCtxt
ctxt Maybe Ct
forall a. Maybe a
Nothing TypeOrKind
level CtOrigin
orig
  | Bool
otherwise
  = SDoc
empty

mk_ea_msg :: ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
-- Constructs a "Couldn't match" message
-- The (Maybe Ct) says whether this is the main top-level message (Just)
--     or a supplementary message (Nothing)
mk_ea_msg :: ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
mk_ea_msg ReportErrCtxt
ctxt Maybe Ct
at_top TypeOrKind
level
          (TypeEqOrigin { uo_actual :: CtOrigin -> TcType
uo_actual = TcType
act, uo_expected :: CtOrigin -> TcType
uo_expected = TcType
exp, uo_thing :: CtOrigin -> Maybe SDoc
uo_thing = Maybe SDoc
mb_thing })
  | Just SDoc
thing <- Maybe SDoc
mb_thing
  , TypeOrKind
KindLevel <- TypeOrKind
level
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Expected" SDoc -> SDoc -> SDoc
<+> SDoc
kind_desc SDoc -> SDoc -> SDoc
<> SDoc
comma)
       Int
2 (String -> SDoc
text String
"but" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes SDoc
thing SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"has kind" SDoc -> SDoc -> SDoc
<+>
          SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
act))

  | Bool
otherwise
  = [SDoc] -> SDoc
vcat [ case Maybe Ct
at_top of
              Just Ct
ct -> Bool -> Ct -> TcType -> TcType -> SDoc
headline_eq_msg Bool
True Ct
ct TcType
exp TcType
act
              Maybe Ct
Nothing -> SDoc
supplementary_ea_msg
         , Bool -> SDoc -> SDoc
ppWhen Bool
expand_syns SDoc
expandedTys ]

  where
    supplementary_ea_msg :: SDoc
supplementary_ea_msg = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Expected:" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
exp
                                , String -> SDoc
text String
"  Actual:" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
act ]

    kind_desc :: SDoc
kind_desc | TcType -> Bool
tcIsConstraintKind TcType
exp = String -> SDoc
text String
"a constraint"
              | Just TcType
arg <- HasDebugCallStack => TcType -> Maybe TcType
TcType -> Maybe TcType
kindRep_maybe TcType
exp  -- TYPE t0
              , TcType -> Bool
tcIsTyVarTy TcType
arg = (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocPrintExplicitRuntimeReps ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \case
                                   Bool
True  -> String -> SDoc
text String
"kind" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
exp)
                                   Bool
False -> String -> SDoc
text String
"a type"
              | Bool
otherwise       = String -> SDoc
text String
"kind" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
exp)

    expand_syns :: Bool
expand_syns = ReportErrCtxt -> Bool
cec_expand_syns ReportErrCtxt
ctxt

    expandedTys :: SDoc
expandedTys = Bool -> SDoc -> SDoc
ppUnless (TcType
expTy1 TcType -> TcType -> Bool
`pickyEqType` TcType
exp Bool -> Bool -> Bool
&& TcType
expTy2 TcType -> TcType -> Bool
`pickyEqType` TcType
act) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
                  [ String -> SDoc
text String
"Type synonyms expanded:"
                  , String -> SDoc
text String
"Expected type:" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
expTy1
                  , String -> SDoc
text String
"  Actual type:" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
expTy2 ]

    (TcType
expTy1, TcType
expTy2) = TcType -> TcType -> (TcType, TcType)
expandSynonymsToMatch TcType
exp TcType
act

mk_ea_msg ReportErrCtxt
_ Maybe Ct
_ TypeOrKind
_ CtOrigin
_ = SDoc
empty

-- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a
-- type mismatch occurs to due invisible kind arguments.
--
-- This function first checks to see if the 'CtOrigin' argument is a
-- 'TypeEqOrigin', and if so, uses the expected/actual types from that to
-- check for a kind mismatch (as these types typically have more surrounding
-- types and are likelier to be able to glean information about whether a
-- mismatch occurred in an invisible argument position or not). If the
-- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types
-- themselves.
pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
                                 -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch :: TcType -> TcType -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch TcType
ty1 TcType
ty2 CtOrigin
ct
  = Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
show_kinds
  where
    (TcType
act_ty, TcType
exp_ty) = case CtOrigin
ct of
      TypeEqOrigin { uo_actual :: CtOrigin -> TcType
uo_actual = TcType
act
                   , uo_expected :: CtOrigin -> TcType
uo_expected = TcType
exp } -> (TcType
act, TcType
exp)
      CtOrigin
_                                  -> (TcType
ty1, TcType
ty2)
    show_kinds :: Bool
show_kinds = TcType -> TcType -> Bool
tcEqTypeVis TcType
act_ty TcType
exp_ty
                 -- True when the visible bit of the types look the same,
                 -- so we want to show the kinds in the displayed type

{- Note [Insoluble occurs check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider [G] a ~ [a],  [W] a ~ [a] (#13674).  The Given is insoluble
so we don't use it for rewriting.  The Wanted is also insoluble, and
we don't solve it from the Given.  It's very confusing to say
    Cannot solve a ~ [a] from given constraints a ~ [a]

And indeed even thinking about the Givens is silly; [W] a ~ [a] is
just as insoluble as Int ~ Bool.

Conclusion: if there's an insoluble occurs check (cteInsolubleOccurs)
then report it directly, not in the "cannot deduce X from Y" form.
This is done in misMatchOrCND (via the insoluble_occurs_check arg)

(NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
want to be as draconian with them.)

Note [Expanding type synonyms to make types similar]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

In type error messages, if -fprint-expanded-types is used, we want to expand
type synonyms to make expected and found types as similar as possible, but we
shouldn't expand types too much to make type messages even more verbose and
harder to understand. The whole point here is to make the difference in expected
and found types clearer.

`expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
only as much as necessary. Given two types t1 and t2:

  * If they're already same, it just returns the types.

  * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
    type constructors), it expands C1 and C2 if they're different type synonyms.
    Then it recursively does the same thing on expanded types. If C1 and C2 are
    same, then it applies the same procedure to arguments of C1 and arguments of
    C2 to make them as similar as possible.

    Most important thing here is to keep number of synonym expansions at
    minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
    Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
    `T (T3, T3, Bool)`.

  * Otherwise types don't have same shapes and so the difference is clearly
    visible. It doesn't do any expansions and show these types.

Note that we only expand top-layer type synonyms. Only when top-layer
constructors are the same we start expanding inner type synonyms.

Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
respectively. If their type-synonym-expanded forms will meet at some point (i.e.
will have same shapes according to `sameShapes` function), it's possible to find
where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
comparisons. We first collect all the top-layer expansions of t1 and t2 in two
lists, then drop the prefix of the longer list so that they have same lengths.
Then we search through both lists in parallel, and return the first pair of
types that have same shapes. Inner types of these two types with same shapes
are then expanded using the same algorithm.

In case they don't meet, we return the last pair of types in the lists, which
has top-layer type synonyms completely expanded. (in this case the inner types
are not expanded at all, as the current form already shows the type error)
-}

-- | Expand type synonyms in given types only enough to make them as similar as
-- possible. Returned types are the same in terms of used type synonyms.
--
-- To expand all synonyms, see 'Type.expandTypeSynonyms'.
--
-- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
-- some examples of how this should work.
expandSynonymsToMatch :: Type -> Type -> (Type, Type)
expandSynonymsToMatch :: TcType -> TcType -> (TcType, TcType)
expandSynonymsToMatch TcType
ty1 TcType
ty2 = (TcType
ty1_ret, TcType
ty2_ret)
  where
    (TcType
ty1_ret, TcType
ty2_ret) = TcType -> TcType -> (TcType, TcType)
go TcType
ty1 TcType
ty2

    -- | Returns (type synonym expanded version of first type,
    --            type synonym expanded version of second type)
    go :: Type -> Type -> (Type, Type)
    go :: TcType -> TcType -> (TcType, TcType)
go TcType
t1 TcType
t2
      | TcType
t1 TcType -> TcType -> Bool
`pickyEqType` TcType
t2 =
        -- Types are same, nothing to do
        (TcType
t1, TcType
t2)

    go (TyConApp TyCon
tc1 [TcType]
tys1) (TyConApp TyCon
tc2 [TcType]
tys2)
      | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
      , [TcType]
tys1 [TcType] -> [TcType] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [TcType]
tys2 =
        -- Type constructors are same. They may be synonyms, but we don't
        -- expand further. The lengths of tys1 and tys2 must be equal;
        -- for example, with type S a = a, we don't want
        -- to zip (S Monad Int) and (S Bool).
        let ([TcType]
tys1', [TcType]
tys2') =
              [(TcType, TcType)] -> ([TcType], [TcType])
forall a b. [(a, b)] -> ([a], [b])
unzip (String
-> (TcType -> TcType -> (TcType, TcType))
-> [TcType]
-> [TcType]
-> [(TcType, TcType)]
forall a b c. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"expandSynonymsToMatch" TcType -> TcType -> (TcType, TcType)
go [TcType]
tys1 [TcType]
tys2)
         in (TyCon -> [TcType] -> TcType
TyConApp TyCon
tc1 [TcType]
tys1', TyCon -> [TcType] -> TcType
TyConApp TyCon
tc2 [TcType]
tys2')

    go (AppTy TcType
t1_1 TcType
t1_2) (AppTy TcType
t2_1 TcType
t2_2) =
      let (TcType
t1_1', TcType
t2_1') = TcType -> TcType -> (TcType, TcType)
go TcType
t1_1 TcType
t2_1
          (TcType
t1_2', TcType
t2_2') = TcType -> TcType -> (TcType, TcType)
go TcType
t1_2 TcType
t2_2
       in (TcType -> TcType -> TcType
mkAppTy TcType
t1_1' TcType
t1_2', TcType -> TcType -> TcType
mkAppTy TcType
t2_1' TcType
t2_2')

    go ty1 :: TcType
ty1@(FunTy AnonArgFlag
_ TcType
w1 TcType
t1_1 TcType
t1_2) ty2 :: TcType
ty2@(FunTy AnonArgFlag
_ TcType
w2 TcType
t2_1 TcType
t2_2) | TcType
w1 TcType -> TcType -> Bool
`eqType` TcType
w2 =
      let (TcType
t1_1', TcType
t2_1') = TcType -> TcType -> (TcType, TcType)
go TcType
t1_1 TcType
t2_1
          (TcType
t1_2', TcType
t2_2') = TcType -> TcType -> (TcType, TcType)
go TcType
t1_2 TcType
t2_2
       in ( TcType
ty1 { ft_arg :: TcType
ft_arg = TcType
t1_1', ft_res :: TcType
ft_res = TcType
t1_2' }
          , TcType
ty2 { ft_arg :: TcType
ft_arg = TcType
t2_1', ft_res :: TcType
ft_res = TcType
t2_2' })

    go (ForAllTy TyCoVarBinder
b1 TcType
t1) (ForAllTy TyCoVarBinder
b2 TcType
t2) =
      -- NOTE: We may have a bug here, but we just can't reproduce it easily.
      -- See D1016 comments for details and our attempts at producing a test
      -- case. Short version: We probably need RnEnv2 to really get this right.
      let (TcType
t1', TcType
t2') = TcType -> TcType -> (TcType, TcType)
go TcType
t1 TcType
t2
       in (TyCoVarBinder -> TcType -> TcType
ForAllTy TyCoVarBinder
b1 TcType
t1', TyCoVarBinder -> TcType -> TcType
ForAllTy TyCoVarBinder
b2 TcType
t2')

    go (CastTy TcType
ty1 Coercion
_) TcType
ty2 = TcType -> TcType -> (TcType, TcType)
go TcType
ty1 TcType
ty2
    go TcType
ty1 (CastTy TcType
ty2 Coercion
_) = TcType -> TcType -> (TcType, TcType)
go TcType
ty1 TcType
ty2

    go TcType
t1 TcType
t2 =
      -- See Note [Expanding type synonyms to make types similar] for how this
      -- works
      let
        t1_exp_tys :: [TcType]
t1_exp_tys = TcType
t1 TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: TcType -> [TcType]
tyExpansions TcType
t1
        t2_exp_tys :: [TcType]
t2_exp_tys = TcType
t2 TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: TcType -> [TcType]
tyExpansions TcType
t2
        t1_exps :: Int
t1_exps    = [TcType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcType]
t1_exp_tys
        t2_exps :: Int
t2_exps    = [TcType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcType]
t2_exp_tys
        dif :: Int
dif        = Int -> Int
forall a. Num a => a -> a
abs (Int
t1_exps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
t2_exps)
      in
        [(TcType, TcType)] -> (TcType, TcType)
followExpansions ([(TcType, TcType)] -> (TcType, TcType))
-> [(TcType, TcType)] -> (TcType, TcType)
forall a b. (a -> b) -> a -> b
$
          String -> [TcType] -> [TcType] -> [(TcType, TcType)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"expandSynonymsToMatch.go"
            (if Int
t1_exps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
t2_exps then Int -> [TcType] -> [TcType]
forall a. Int -> [a] -> [a]
drop Int
dif [TcType]
t1_exp_tys else [TcType]
t1_exp_tys)
            (if Int
t2_exps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
t1_exps then Int -> [TcType] -> [TcType]
forall a. Int -> [a] -> [a]
drop Int
dif [TcType]
t2_exp_tys else [TcType]
t2_exp_tys)

    -- | Expand the top layer type synonyms repeatedly, collect expansions in a
    -- list. The list does not include the original type.
    --
    -- Example, if you have:
    --
    --   type T10 = T9
    --   type T9  = T8
    --   ...
    --   type T0  = Int
    --
    -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
    --
    -- This only expands the top layer, so if you have:
    --
    --   type M a = Maybe a
    --
    -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
    tyExpansions :: Type -> [Type]
    tyExpansions :: TcType -> [TcType]
tyExpansions = (TcType -> Maybe (TcType, TcType)) -> TcType -> [TcType]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (\TcType
t -> (\TcType
x -> (TcType
x, TcType
x)) (TcType -> (TcType, TcType))
-> Maybe TcType -> Maybe (TcType, TcType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` TcType -> Maybe TcType
tcView TcType
t)

    -- | Drop the type pairs until types in a pair look alike (i.e. the outer
    -- constructors are the same).
    followExpansions :: [(Type, Type)] -> (Type, Type)
    followExpansions :: [(TcType, TcType)] -> (TcType, TcType)
followExpansions [] = String -> SDoc -> (TcType, TcType)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"followExpansions" SDoc
empty
    followExpansions [(TcType
t1, TcType
t2)]
      | TcType -> TcType -> Bool
sameShapes TcType
t1 TcType
t2 = TcType -> TcType -> (TcType, TcType)
go TcType
t1 TcType
t2 -- expand subtrees
      | Bool
otherwise        = (TcType
t1, TcType
t2) -- the difference is already visible
    followExpansions ((TcType
t1, TcType
t2) : [(TcType, TcType)]
tss)
      -- Traverse subtrees when the outer shapes are the same
      | TcType -> TcType -> Bool
sameShapes TcType
t1 TcType
t2 = TcType -> TcType -> (TcType, TcType)
go TcType
t1 TcType
t2
      -- Otherwise follow the expansions until they look alike
      | Bool
otherwise = [(TcType, TcType)] -> (TcType, TcType)
followExpansions [(TcType, TcType)]
tss

    sameShapes :: Type -> Type -> Bool
    sameShapes :: TcType -> TcType -> Bool
sameShapes AppTy{}          AppTy{}          = Bool
True
    sameShapes (TyConApp TyCon
tc1 [TcType]
_) (TyConApp TyCon
tc2 [TcType]
_) = TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
    sameShapes (FunTy {})       (FunTy {})       = Bool
True
    sameShapes (ForAllTy {})    (ForAllTy {})    = Bool
True
    sameShapes (CastTy TcType
ty1 Coercion
_)   TcType
ty2              = TcType -> TcType -> Bool
sameShapes TcType
ty1 TcType
ty2
    sameShapes TcType
ty1              (CastTy TcType
ty2 Coercion
_)   = TcType -> TcType -> Bool
sameShapes TcType
ty1 TcType
ty2
    sameShapes TcType
_                TcType
_                = Bool
False

sameOccExtra :: TcType -> TcType -> SDoc
-- See Note [Disambiguating (X ~ X) errors]
sameOccExtra :: TcType -> TcType -> SDoc
sameOccExtra TcType
ty1 TcType
ty2
  | Just (TyCon
tc1, [TcType]
_) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty1
  , Just (TyCon
tc2, [TcType]
_) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty2
  , let n1 :: Name
n1 = TyCon -> Name
tyConName TyCon
tc1
        n2 :: Name
n2 = TyCon -> Name
tyConName TyCon
tc2
        same_occ :: Bool
same_occ = Name -> OccName
nameOccName Name
n1                   OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> OccName
nameOccName Name
n2
        same_pkg :: Bool
same_pkg = Module -> Unit
forall unit. GenModule unit -> unit
moduleUnit (HasDebugCallStack => Name -> Module
Name -> Module
nameModule Name
n1) Unit -> Unit -> Bool
forall a. Eq a => a -> a -> Bool
== Module -> Unit
forall unit. GenModule unit -> unit
moduleUnit (HasDebugCallStack => Name -> Module
Name -> Module
nameModule Name
n2)
  , Name
n1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n2   -- Different Names
  , Bool
same_occ   -- but same OccName
  = String -> SDoc
text String
"NB:" SDoc -> SDoc -> SDoc
<+> (Bool -> Name -> SDoc
ppr_from Bool
same_pkg Name
n1 SDoc -> SDoc -> SDoc
$$ Bool -> Name -> SDoc
ppr_from Bool
same_pkg Name
n2)
  | Bool
otherwise
  = SDoc
empty
  where
    ppr_from :: Bool -> Name -> SDoc
ppr_from Bool
same_pkg Name
nm
      | SrcSpan -> Bool
isGoodSrcSpan SrcSpan
loc
      = SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
nm) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is defined at")
           Int
2 (SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
loc)
      | Bool
otherwise  -- Imported things have an UnhelpfulSrcSpan
      = SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
nm))
           Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"is defined in" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (ModuleName -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Module -> ModuleName
forall unit. GenModule unit -> ModuleName
moduleName Module
mod))
                  , Bool -> SDoc -> SDoc
ppUnless (Bool
same_pkg Bool -> Bool -> Bool
|| Unit
pkg Unit -> Unit -> Bool
forall a. Eq a => a -> a -> Bool
== Unit
mainUnit) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                    Int -> SDoc -> SDoc
nest Int
4 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"in package" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Unit -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unit
pkg) ])
       where
         pkg :: Unit
pkg = Module -> Unit
forall unit. GenModule unit -> unit
moduleUnit Module
mod
         mod :: Module
mod = HasDebugCallStack => Name -> Module
Name -> Module
nameModule Name
nm
         loc :: SrcSpan
loc = Name -> SrcSpan
nameSrcSpan Name
nm

{- Note [Suggest adding a type signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The OutsideIn algorithm rejects GADT programs that don't have a principal
type, and indeed some that do.  Example:
   data T a where
     MkT :: Int -> T Int

   f (MkT n) = n

Does this have type f :: T a -> a, or f :: T a -> Int?
The error that shows up tends to be an attempt to unify an
untouchable type variable.  So suggestAddSig sees if the offending
type variable is bound by an *inferred* signature, and suggests
adding a declared signature instead.

More specifically, we suggest adding a type sig if we have p ~ ty, and
p is a skolem bound by an InferSkol.  Those skolems were created from
unification variables in simplifyInfer.  Why didn't we unify?  It must
have been because of an intervening GADT or existential, making it
untouchable. Either way, a type signature would help.  For GADTs, it
might make it typeable; for existentials the attempt to write a
signature will fail -- or at least will produce a better error message
next time

This initially came up in #8968, concerning pattern synonyms.

Note [Disambiguating (X ~ X) errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See #8278

Note [Reporting occurs-check errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
type signature, then the best thing is to report that we can't unify
a with [a], because a is a skolem variable.  That avoids the confusing
"occur-check" error message.

But nowadays when inferring the type of a function with no type signature,
even if there are errors inside, we still generalise its signature and
carry on. For example
   f x = x:x
Here we will infer something like
   f :: forall a. a -> [a]
with a deferred error of (a ~ [a]).  So in the deferred unsolved constraint
'a' is now a skolem, but not one bound by the programmer in the context!
Here we really should report an occurs check.

So isUserSkolem distinguishes the two.

Note [Non-injective type functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's very confusing to get a message like
     Couldn't match expected type `Depend s'
            against inferred type `Depend s1'
so mkTyFunInfoMsg adds:
       NB: `Depend' is type function, and hence may not be injective

Warn of loopy local equalities that were dropped.


************************************************************************
*                                                                      *
                 Type-class errors
*                                                                      *
************************************************************************
-}

mkDictErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkDictErr :: ReportErrCtxt -> [Ct] -> TcM (MsgEnvelope DecoratedSDoc)
mkDictErr ReportErrCtxt
ctxt [Ct]
cts
  = ASSERT( not (null cts) )
    do { InstEnvs
inst_envs <- TcM InstEnvs
tcGetInstEnvs
       ; let (Ct
ct1:[Ct]
_) = [Ct]
cts  -- ct1 just for its location
             min_cts :: [Ct]
min_cts = [Ct] -> [Ct]
elim_superclasses [Ct]
cts
             lookups :: [(Ct, ClsInstLookupResult)]
lookups = (Ct -> (Ct, ClsInstLookupResult))
-> [Ct] -> [(Ct, ClsInstLookupResult)]
forall a b. (a -> b) -> [a] -> [b]
map (InstEnvs -> Ct -> (Ct, ClsInstLookupResult)
lookup_cls_inst InstEnvs
inst_envs) [Ct]
min_cts
             ([(Ct, ClsInstLookupResult)]
no_inst_cts, [(Ct, ClsInstLookupResult)]
overlap_cts) = ((Ct, ClsInstLookupResult) -> Bool)
-> [(Ct, ClsInstLookupResult)]
-> ([(Ct, ClsInstLookupResult)], [(Ct, ClsInstLookupResult)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Ct, ClsInstLookupResult) -> Bool
is_no_inst [(Ct, ClsInstLookupResult)]
lookups

       -- Report definite no-instance errors,
       -- or (iff there are none) overlap errors
       -- But we report only one of them (hence 'head') because they all
       -- have the same source-location origin, to try avoid a cascade
       -- of error from one location
       ; (ReportErrCtxt
ctxt, SDoc
err) <- ReportErrCtxt
-> (Ct, ClsInstLookupResult) -> TcM (ReportErrCtxt, SDoc)
mk_dict_err ReportErrCtxt
ctxt ([(Ct, ClsInstLookupResult)] -> (Ct, ClsInstLookupResult)
forall a. [a] -> a
head ([(Ct, ClsInstLookupResult)]
no_inst_cts [(Ct, ClsInstLookupResult)]
-> [(Ct, ClsInstLookupResult)] -> [(Ct, ClsInstLookupResult)]
forall a. [a] -> [a] -> [a]
++ [(Ct, ClsInstLookupResult)]
overlap_cts))
       ; ReportErrCtxt -> Ct -> Report -> TcM (MsgEnvelope DecoratedSDoc)
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct1 (SDoc -> Report
important SDoc
err) }
  where
    no_givens :: Bool
no_givens = [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt)

    is_no_inst :: (Ct, ClsInstLookupResult) -> Bool
is_no_inst (Ct
ct, ([InstMatch]
matches, [ClsInst]
unifiers, [InstMatch]
_))
      =  Bool
no_givens
      Bool -> Bool -> Bool
&& [InstMatch] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [InstMatch]
matches
      Bool -> Bool -> Bool
&& ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
unifiers Bool -> Bool -> Bool
|| (TcId -> Bool) -> [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (TcId -> Bool) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcId -> Bool
isAmbiguousTyVar) (Ct -> [TcId]
tyCoVarsOfCtList Ct
ct))

    lookup_cls_inst :: InstEnvs -> Ct -> (Ct, ClsInstLookupResult)
lookup_cls_inst InstEnvs
inst_envs Ct
ct
                -- Note [Flattening in error message generation]
      = (Ct
ct, Bool -> InstEnvs -> Class -> [TcType] -> ClsInstLookupResult
lookupInstEnv Bool
True InstEnvs
inst_envs Class
clas (InScopeSet -> [TcType] -> [TcType]
flattenTys InScopeSet
emptyInScopeSet [TcType]
tys))
      where
        (Class
clas, [TcType]
tys) = HasDebugCallStack => TcType -> (Class, [TcType])
TcType -> (Class, [TcType])
getClassPredTys (Ct -> TcType
ctPred Ct
ct)


    -- When simplifying [W] Ord (Set a), we need
    --    [W] Eq a, [W] Ord a
    -- but we really only want to report the latter
    elim_superclasses :: [Ct] -> [Ct]
elim_superclasses [Ct]
cts = (Ct -> TcType) -> [Ct] -> [Ct]
forall a. (a -> TcType) -> [a] -> [a]
mkMinimalBySCs Ct -> TcType
ctPred [Ct]
cts

-- [Note: mk_dict_err]
-- ~~~~~~~~~~~~~~~~~~~
-- Different dictionary error messages are reported depending on the number of
-- matches and unifiers:
--
--   - No matches, regardless of unifiers: report "No instance for ...".
--   - Two or more matches, regardless of unifiers: report "Overlapping instances for ...",
--     and show the matching and unifying instances.
--   - One match, one or more unifiers: report "Overlapping instances for", show the
--     matching and unifying instances, and say "The choice depends on the instantion of ...,
--     and the result of evaluating ...".
mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
            -> TcM (ReportErrCtxt, SDoc)
-- Report an overlap error if this class constraint results
-- from an overlap (returning Left clas), otherwise return (Right pred)
mk_dict_err :: ReportErrCtxt
-> (Ct, ClsInstLookupResult) -> TcM (ReportErrCtxt, SDoc)
mk_dict_err ctxt :: ReportErrCtxt
ctxt@(CEC {cec_encl :: ReportErrCtxt -> [Implication]
cec_encl = [Implication]
implics}) (Ct
ct, ([InstMatch]
matches, [ClsInst]
unifiers, [InstMatch]
unsafe_overlapped))
  | [InstMatch] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [InstMatch]
matches  -- No matches but perhaps several unifiers
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg, Ct
ct) <- Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
True ReportErrCtxt
ctxt Ct
ct
       ; [ClsInst]
candidate_insts <- TcM [ClsInst]
get_candidate_instances
       ; (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, Ct -> [ClsInst] -> SDoc -> SDoc
cannot_resolve_msg Ct
ct [ClsInst]
candidate_insts SDoc
binds_msg) }

  | [InstMatch] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [InstMatch]
unsafe_overlapped   -- Some matches => overlap errors
  = (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, SDoc
overlap_msg)

  | Bool
otherwise
  = (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, SDoc
safe_haskell_msg)
  where
    orig :: CtOrigin
orig          = Ct -> CtOrigin
ctOrigin Ct
ct
    pred :: TcType
pred          = Ct -> TcType
ctPred Ct
ct
    (Class
clas, [TcType]
tys)   = HasDebugCallStack => TcType -> (Class, [TcType])
TcType -> (Class, [TcType])
getClassPredTys TcType
pred
    ispecs :: [ClsInst]
ispecs        = [ClsInst
ispec | (ClsInst
ispec, [Maybe TcType]
_) <- [InstMatch]
matches]
    unsafe_ispecs :: [ClsInst]
unsafe_ispecs = [ClsInst
ispec | (ClsInst
ispec, [Maybe TcType]
_) <- [InstMatch]
unsafe_overlapped]
    useful_givens :: [Implication]
useful_givens = CtOrigin -> [Implication] -> [Implication]
discardProvCtxtGivens CtOrigin
orig ([Implication] -> [Implication]
getUserGivensFromImplics [Implication]
implics)
         -- useful_givens are the enclosing implications with non-empty givens,
         -- modulo the horrid discardProvCtxtGivens

    get_candidate_instances :: TcM [ClsInst]
    -- See Note [Report candidate instances]
    get_candidate_instances :: TcM [ClsInst]
get_candidate_instances
      | [TcType
ty] <- [TcType]
tys   -- Only try for single-parameter classes
      = do { InstEnvs
instEnvs <- TcM InstEnvs
tcGetInstEnvs
           ; [ClsInst] -> TcM [ClsInst]
forall (m :: * -> *) a. Monad m => a -> m a
return ((ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> Bool) -> [a] -> [a]
filter (TcType -> ClsInst -> Bool
is_candidate_inst TcType
ty)
                            (InstEnvs -> Class -> [ClsInst]
classInstances InstEnvs
instEnvs Class
clas)) }
      | Bool
otherwise = [ClsInst] -> TcM [ClsInst]
forall (m :: * -> *) a. Monad m => a -> m a
return []

    is_candidate_inst :: TcType -> ClsInst -> Bool
is_candidate_inst TcType
ty ClsInst
inst -- See Note [Report candidate instances]
      | [TcType
other_ty] <- ClsInst -> [TcType]
is_tys ClsInst
inst
      , Just (TyCon
tc1, [TcType]
_) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty
      , Just (TyCon
tc2, [TcType]
_) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
other_ty
      = let n1 :: Name
n1 = TyCon -> Name
tyConName TyCon
tc1
            n2 :: Name
n2 = TyCon -> Name
tyConName TyCon
tc2
            different_names :: Bool
different_names = Name
n1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n2
            same_occ_names :: Bool
same_occ_names = Name -> OccName
nameOccName Name
n1 OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> OccName
nameOccName Name
n2
        in Bool
different_names Bool -> Bool -> Bool
&& Bool
same_occ_names
      | Bool
otherwise = Bool
False

    cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc
    cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc
cannot_resolve_msg Ct
ct [ClsInst]
candidate_insts SDoc
binds_msg
      = [SDoc] -> SDoc
vcat [ SDoc
no_inst_msg
             , Int -> SDoc -> SDoc
nest Int
2 SDoc
extra_note
             , [SDoc] -> SDoc
vcat ([Implication] -> [SDoc]
pp_givens [Implication]
useful_givens)
             , Maybe SDoc
mb_patsyn_prov Maybe SDoc -> SDoc -> SDoc
forall a. Maybe a -> a -> a
`orElse` SDoc
empty
             , Bool -> SDoc -> SDoc
ppWhen (Bool
has_ambig_tvs Bool -> Bool -> Bool
&& Bool -> Bool
not ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
unifiers Bool -> Bool -> Bool
&& [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
useful_givens))
               ([SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppUnless Bool
lead_with_ambig SDoc
ambig_msg, SDoc
binds_msg, SDoc
potential_msg ])

             , Bool -> SDoc -> SDoc
ppWhen (Maybe SDoc -> Bool
forall a. Maybe a -> Bool
isNothing Maybe SDoc
mb_patsyn_prov) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                   -- Don't suggest fixes for the provided context of a pattern
                   -- synonym; the right fix is to bind more in the pattern
               [SDoc] -> SDoc
show_fixes (Bool -> TcType -> [Implication] -> [SDoc]
ctxtFixes Bool
has_ambig_tvs TcType
pred [Implication]
implics
                           [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
drv_fixes)
             , Bool -> SDoc -> SDoc
ppWhen (Bool -> Bool
not ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
candidate_insts))
               (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"There are instances for similar types:")
                   Int
2 ([SDoc] -> SDoc
vcat ((ClsInst -> SDoc) -> [ClsInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ClsInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ClsInst]
candidate_insts))) ]
                   -- See Note [Report candidate instances]
      where
        orig :: CtOrigin
orig = Ct -> CtOrigin
ctOrigin Ct
ct
        -- See Note [Highlighting ambiguous type variables]
        lead_with_ambig :: Bool
lead_with_ambig = Bool
has_ambig_tvs Bool -> Bool -> Bool
&& Bool -> Bool
not ((TcId -> Bool) -> [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcId -> Bool
isRuntimeUnkSkol [TcId]
ambig_tvs)
                        Bool -> Bool -> Bool
&& Bool -> Bool
not ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
unifiers) Bool -> Bool -> Bool
&& [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
useful_givens

        (Bool
has_ambig_tvs, SDoc
ambig_msg) = Bool -> Ct -> (Bool, SDoc)
mkAmbigMsg Bool
lead_with_ambig Ct
ct
        ambig_tvs :: [TcId]
ambig_tvs = ([TcId] -> [TcId] -> [TcId]) -> ([TcId], [TcId]) -> [TcId]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [TcId] -> [TcId] -> [TcId]
forall a. [a] -> [a] -> [a]
(++) (Ct -> ([TcId], [TcId])
getAmbigTkvs Ct
ct)

        no_inst_msg :: SDoc
no_inst_msg
          | Bool
lead_with_ambig
          = SDoc
ambig_msg SDoc -> SDoc -> SDoc
<+> CtOrigin -> SDoc
pprArising CtOrigin
orig
              SDoc -> SDoc -> SDoc
$$ String -> SDoc
text String
"prevents the constraint" SDoc -> SDoc -> SDoc
<+>  SDoc -> SDoc
quotes (TcType -> SDoc
pprParendType TcType
pred)
              SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"from being solved."

          | [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
useful_givens
          = CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"No instance for"
            SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
pred

          | Bool
otherwise
          = CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Could not deduce"
            SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
pred

        potential_msg :: SDoc
potential_msg
          = Bool -> SDoc -> SDoc
ppWhen (Bool -> Bool
not ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
unifiers) Bool -> Bool -> Bool
&& CtOrigin -> Bool
want_potential CtOrigin
orig) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocPrintPotentialInstances ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \Bool
print_insts ->
            (PprStyle -> SDoc) -> SDoc
getPprStyle ((PprStyle -> SDoc) -> SDoc) -> (PprStyle -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \PprStyle
sty ->
            PrintPotentialInstances -> PprStyle -> SDoc -> [ClsInst] -> SDoc
pprPotentials (Bool -> PrintPotentialInstances
PrintPotentialInstances Bool
print_insts) PprStyle
sty SDoc
potential_hdr [ClsInst]
unifiers

        potential_hdr :: SDoc
potential_hdr
          = [SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppWhen Bool
lead_with_ambig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                     String -> SDoc
text String
"Probable fix: use a type annotation to specify what"
                     SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TcId]
ambig_tvs SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"should be."
                 , String -> SDoc
text String
"These potential instance" SDoc -> SDoc -> SDoc
<> [ClsInst] -> SDoc
forall a. [a] -> SDoc
plural [ClsInst]
unifiers
                   SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"exist:"]

        mb_patsyn_prov :: Maybe SDoc
        mb_patsyn_prov :: Maybe SDoc
mb_patsyn_prov
          | Bool -> Bool
not Bool
lead_with_ambig
          , ProvCtxtOrigin PSB{ psb_def :: forall idL idR. PatSynBind idL idR -> LPat idR
psb_def = L SrcSpanAnnA
_ Pat GhcRn
pat } <- CtOrigin
orig
          = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"In other words, a successful match on the pattern"
                       , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ Pat GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr Pat GhcRn
pat
                       , String -> SDoc
text String
"does not provide the constraint" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
pred ])
          | Bool
otherwise = Maybe SDoc
forall a. Maybe a
Nothing

    -- Report "potential instances" only when the constraint arises
    -- directly from the user's use of an overloaded function
    want_potential :: CtOrigin -> Bool
want_potential (TypeEqOrigin {}) = Bool
False
    want_potential CtOrigin
_                 = Bool
True

    extra_note :: SDoc
extra_note | (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcType -> Bool
isFunTy (TyCon -> [TcType] -> [TcType]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
clas) [TcType]
tys)
               = String -> SDoc
text String
"(maybe you haven't applied a function to enough arguments?)"
               | Class -> Name
className Class
clas Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeableClassName  -- Avoid mysterious "No instance for (Typeable T)
               , [TcType
_,TcType
ty] <- [TcType]
tys                        -- Look for (Typeable (k->*) (T k))
               , Just (TyCon
tc,[TcType]
_) <- HasCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty
               , Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc)
               = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"GHC can't yet do polykinded")
                    Int
2 (String -> SDoc
text String
"Typeable" SDoc -> SDoc -> SDoc
<+>
                       SDoc -> SDoc
parens (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => TcType -> TcType
TcType -> TcType
tcTypeKind TcType
ty)))
               | Bool
otherwise
               = SDoc
empty

    drv_fixes :: [SDoc]
drv_fixes = case CtOrigin
orig of
                   CtOrigin
DerivClauseOrigin                  -> [Bool -> SDoc
drv_fix Bool
False]
                   CtOrigin
StandAloneDerivOrigin              -> [Bool -> SDoc
drv_fix Bool
True]
                   DerivOriginDC DataCon
_ Int
_       Bool
standalone -> [Bool -> SDoc
drv_fix Bool
standalone]
                   DerivOriginCoerce TcId
_ TcType
_ TcType
_ Bool
standalone -> [Bool -> SDoc
drv_fix Bool
standalone]
                   CtOrigin
_                -> []

    drv_fix :: Bool -> SDoc
drv_fix Bool
standalone_wildcard
      | Bool
standalone_wildcard
      = String -> SDoc
text String
"fill in the wildcard constraint yourself"
      | Bool
otherwise
      = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"use a standalone 'deriving instance' declaration,")
           Int
2 (String -> SDoc
text String
"so you can specify the instance context yourself")

    -- Normal overlap error
    overlap_msg :: SDoc
overlap_msg
      = ASSERT( not (null matches) )
        [SDoc] -> SDoc
vcat [  CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (String -> SDoc
text String
"Overlapping instances for"
                                SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprType (Class -> [TcType] -> TcType
mkClassPred Class
clas [TcType]
tys))

             ,  Bool -> SDoc -> SDoc
ppUnless ([SDoc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SDoc]
matching_givens) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                  [SDoc] -> SDoc
sep [String -> SDoc
text String
"Matching givens (or their superclasses):"
                      , Int -> SDoc -> SDoc
nest Int
2 ([SDoc] -> SDoc
vcat [SDoc]
matching_givens)]

             ,  (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
sdocOption SDocContext -> Bool
sdocPrintPotentialInstances ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \Bool
print_insts ->
                (PprStyle -> SDoc) -> SDoc
getPprStyle ((PprStyle -> SDoc) -> SDoc) -> (PprStyle -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \PprStyle
sty ->
                PrintPotentialInstances -> PprStyle -> SDoc -> [ClsInst] -> SDoc
pprPotentials (Bool -> PrintPotentialInstances
PrintPotentialInstances Bool
print_insts) PprStyle
sty (String -> SDoc
text String
"Matching instances:") ([ClsInst] -> SDoc) -> [ClsInst] -> SDoc
forall a b. (a -> b) -> a -> b
$
                [ClsInst]
ispecs [ClsInst] -> [ClsInst] -> [ClsInst]
forall a. [a] -> [a] -> [a]
++ [ClsInst]
unifiers

             ,  Bool -> SDoc -> SDoc
ppWhen ([SDoc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SDoc]
matching_givens Bool -> Bool -> Bool
&& [InstMatch] -> Bool
forall a. [a] -> Bool
isSingleton [InstMatch]
matches Bool -> Bool -> Bool
&& [ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
unifiers) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                -- Intuitively, some given matched the wanted in their
                -- flattened or rewritten (from given equalities) form
                -- but the matcher can't figure that out because the
                -- constraints are non-flat and non-rewritten so we
                -- simply report back the whole given
                -- context. Accelerate Smart.hs showed this problem.
                  [SDoc] -> SDoc
sep [ String -> SDoc
text String
"There exists a (perhaps superclass) match:"
                      , Int -> SDoc -> SDoc
nest Int
2 ([SDoc] -> SDoc
vcat ([Implication] -> [SDoc]
pp_givens [Implication]
useful_givens))]

             ,  Bool -> SDoc -> SDoc
ppWhen ([InstMatch] -> Bool
forall a. [a] -> Bool
isSingleton [InstMatch]
matches) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                SDoc -> SDoc
parens ([SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppUnless ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
tyCoVars) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                                 String -> SDoc
text String
"The choice depends on the instantiation of" SDoc -> SDoc -> SDoc
<+>
                                   SDoc -> SDoc
quotes ((TcId -> SDoc) -> [TcId] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcId]
tyCoVars)
                             , Bool -> SDoc -> SDoc
ppUnless ([TyCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCon]
famTyCons) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                                 if ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
tyCoVars)
                                   then
                                     String -> SDoc
text String
"The choice depends on the result of evaluating" SDoc -> SDoc -> SDoc
<+>
                                       SDoc -> SDoc
quotes ((TyCon -> SDoc) -> [TyCon] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCon]
famTyCons)
                                   else
                                     String -> SDoc
text String
"and the result of evaluating" SDoc -> SDoc -> SDoc
<+>
                                       SDoc -> SDoc
quotes ((TyCon -> SDoc) -> [TyCon] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCon]
famTyCons)
                             , Bool -> SDoc -> SDoc
ppWhen ([SDoc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([SDoc]
matching_givens)) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                               [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"To pick the first instance above, use IncoherentInstances"
                                    , String -> SDoc
text String
"when compiling the other instance declarations"]
                        ])]
      where
        tyCoVars :: [TcId]
tyCoVars = [TcType] -> [TcId]
tyCoVarsOfTypesList [TcType]
tys
        famTyCons :: [TyCon]
famTyCons = (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter TyCon -> Bool
isFamilyTyCon ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ (TcType -> [TyCon]) -> [TcType] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (UniqSet TyCon -> [TyCon]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet (UniqSet TyCon -> [TyCon])
-> (TcType -> UniqSet TyCon) -> TcType -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> UniqSet TyCon
tyConsOfType) [TcType]
tys

    matching_givens :: [SDoc]
matching_givens = (Implication -> Maybe SDoc) -> [Implication] -> [SDoc]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Implication -> Maybe SDoc
matchable [Implication]
useful_givens

    matchable :: Implication -> Maybe SDoc
matchable implic :: Implication
implic@(Implic { ic_given :: Implication -> [TcId]
ic_given = [TcId]
evvars, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info })
      = case [TcType]
ev_vars_matching of
             [] -> Maybe SDoc
forall a. Maybe a
Nothing
             [TcType]
_  -> SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (SDoc -> Maybe SDoc) -> SDoc -> Maybe SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> Int -> SDoc -> SDoc
hang ([TcType] -> SDoc
pprTheta [TcType]
ev_vars_matching)
                            Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"bound by" SDoc -> SDoc -> SDoc
<+> SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info
                                   , String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+>
                                     RealSrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcLclEnv -> RealSrcSpan
tcl_loc (Implication -> TcLclEnv
ic_env Implication
implic)) ])
        where ev_vars_matching :: [TcType]
ev_vars_matching = [ TcType
pred
                                 | TcId
ev_var <- [TcId]
evvars
                                 , let pred :: TcType
pred = TcId -> TcType
evVarPred TcId
ev_var
                                 , (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcType -> Bool
can_match (TcType
pred TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: TcType -> [TcType]
transSuperClasses TcType
pred) ]
              can_match :: TcType -> Bool
can_match TcType
pred
                 = case TcType -> Maybe (Class, [TcType])
getClassPredTys_maybe TcType
pred of
                     Just (Class
clas', [TcType]
tys') -> Class
clas' Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
clas
                                          Bool -> Bool -> Bool
&& Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust ([TcType] -> [TcType] -> Maybe TCvSubst
tcMatchTys [TcType]
tys [TcType]
tys')
                     Maybe (Class, [TcType])
Nothing -> Bool
False

    -- Overlap error because of Safe Haskell (first
    -- match should be the most specific match)
    safe_haskell_msg :: SDoc
safe_haskell_msg
     = ASSERT( matches `lengthIs` 1 && not (null unsafe_ispecs) )
       [SDoc] -> SDoc
vcat [ CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (String -> SDoc
text String
"Unsafe overlapping instances for"
                       SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprType (Class -> [TcType] -> TcType
mkClassPred Class
clas [TcType]
tys))
            , [SDoc] -> SDoc
sep [String -> SDoc
text String
"The matching instance is:",
                   Int -> SDoc -> SDoc
nest Int
2 (ClsInst -> SDoc
pprInstance (ClsInst -> SDoc) -> ClsInst -> SDoc
forall a b. (a -> b) -> a -> b
$ [ClsInst] -> ClsInst
forall a. [a] -> a
head [ClsInst]
ispecs)]
            , [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"It is compiled in a Safe module and as such can only"
                   , String -> SDoc
text String
"overlap instances from the same module, however it"
                   , String -> SDoc
text String
"overlaps the following instances from different" SDoc -> SDoc -> SDoc
<+>
                     String -> SDoc
text String
"modules:"
                   , Int -> SDoc -> SDoc
nest Int
2 ([SDoc] -> SDoc
vcat [[ClsInst] -> SDoc
pprInstances ([ClsInst] -> SDoc) -> [ClsInst] -> SDoc
forall a b. (a -> b) -> a -> b
$ [ClsInst]
unsafe_ispecs])
                   ]
            ]


ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
ctxtFixes :: Bool -> TcType -> [Implication] -> [SDoc]
ctxtFixes Bool
has_ambig_tvs TcType
pred [Implication]
implics
  | Bool -> Bool
not Bool
has_ambig_tvs
  , TcType -> Bool
isTyVarClassPred TcType
pred
  , (SkolemInfo
skol:[SkolemInfo]
skols) <- [Implication] -> TcType -> [SkolemInfo]
usefulContext [Implication]
implics TcType
pred
  , let what :: SDoc
what | [SkolemInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SkolemInfo]
skols
             , SigSkol (PatSynCtxt {}) TcType
_ [(Name, TcId)]
_ <- SkolemInfo
skol
             = String -> SDoc
text String
"\"required\""
             | Bool
otherwise
             = SDoc
empty
  = [[SDoc] -> SDoc
sep [ String -> SDoc
text String
"add" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
pred
           SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"to the" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"context of"
         , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SkolemInfo -> SDoc
ppr_skol SkolemInfo
skol SDoc -> SDoc -> SDoc
$$
                    [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"or" SDoc -> SDoc -> SDoc
<+> SkolemInfo -> SDoc
ppr_skol SkolemInfo
skol
                         | SkolemInfo
skol <- [SkolemInfo]
skols ] ] ]
  | Bool
otherwise = []
  where
    ppr_skol :: SkolemInfo -> SDoc
ppr_skol (PatSkol (RealDataCon DataCon
dc) HsMatchContext GhcRn
_) = String -> SDoc
text String
"the data constructor" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
dc)
    ppr_skol (PatSkol (PatSynCon PatSyn
ps)   HsMatchContext GhcRn
_) = String -> SDoc
text String
"the pattern synonym"  SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (PatSyn -> SDoc
forall a. Outputable a => a -> SDoc
ppr PatSyn
ps)
    ppr_skol SkolemInfo
skol_info = SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info

discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
discardProvCtxtGivens :: CtOrigin -> [Implication] -> [Implication]
discardProvCtxtGivens CtOrigin
orig [Implication]
givens  -- See Note [discardProvCtxtGivens]
  | ProvCtxtOrigin (PSB {psb_id :: forall idL idR. PatSynBind idL idR -> LIdP idL
psb_id = L SrcSpanAnnN
_ Name
name}) <- CtOrigin
orig
  = (Implication -> Bool) -> [Implication] -> [Implication]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (Name -> Implication -> Bool
discard Name
name) [Implication]
givens
  | Bool
otherwise
  = [Implication]
givens
  where
    discard :: Name -> Implication -> Bool
discard Name
n (Implic { ic_info :: Implication -> SkolemInfo
ic_info = SigSkol (PatSynCtxt Name
n') TcType
_ [(Name, TcId)]
_ }) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    discard Name
_ Implication
_                                                  = Bool
False

usefulContext :: [Implication] -> PredType -> [SkolemInfo]
-- usefulContext picks out the implications whose context
-- the programmer might plausibly augment to solve 'pred'
usefulContext :: [Implication] -> TcType -> [SkolemInfo]
usefulContext [Implication]
implics TcType
pred
  = [Implication] -> [SkolemInfo]
go [Implication]
implics
  where
    pred_tvs :: TyCoVarSet
pred_tvs = TcType -> TyCoVarSet
tyCoVarsOfType TcType
pred
    go :: [Implication] -> [SkolemInfo]
go [] = []
    go (Implication
ic : [Implication]
ics)
       | Implication -> Bool
implausible Implication
ic = [SkolemInfo]
rest
       | Bool
otherwise      = Implication -> SkolemInfo
ic_info Implication
ic SkolemInfo -> [SkolemInfo] -> [SkolemInfo]
forall a. a -> [a] -> [a]
: [SkolemInfo]
rest
       where
          -- Stop when the context binds a variable free in the predicate
          rest :: [SkolemInfo]
rest | (TcId -> Bool) -> [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TcId -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
pred_tvs) (Implication -> [TcId]
ic_skols Implication
ic) = []
               | Bool
otherwise                                 = [Implication] -> [SkolemInfo]
go [Implication]
ics

    implausible :: Implication -> Bool
implausible Implication
ic
      | [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Implication -> [TcId]
ic_skols Implication
ic)            = Bool
True
      | SkolemInfo -> Bool
implausible_info (Implication -> SkolemInfo
ic_info Implication
ic) = Bool
True
      | Bool
otherwise                     = Bool
False

    implausible_info :: SkolemInfo -> Bool
implausible_info (SigSkol (InfSigCtxt {}) TcType
_ [(Name, TcId)]
_) = Bool
True
    implausible_info SkolemInfo
_                             = Bool
False
    -- Do not suggest adding constraints to an *inferred* type signature

{- Note [Report candidate instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
but comes from some other module, then it may be helpful to point out
that there are some similarly named instances elsewhere.  So we get
something like
    No instance for (Num Int) arising from the literal ‘3’
    There are instances for similar types:
      instance Num GHC.Types.Int -- Defined in ‘GHC.Num’
Discussion in #9611.

Note [Highlighting ambiguous type variables]
~-------------------------------------------
When we encounter ambiguous type variables (i.e. type variables
that remain metavariables after type inference), we need a few more
conditions before we can reason that *ambiguity* prevents constraints
from being solved:
  - We can't have any givens, as encountering a typeclass error
    with given constraints just means we couldn't deduce
    a solution satisfying those constraints and as such couldn't
    bind the type variable to a known type.
  - If we don't have any unifiers, we don't even have potential
    instances from which an ambiguity could arise.
  - Lastly, I don't want to mess with error reporting for
    unknown runtime types so we just fall back to the old message there.
Once these conditions are satisfied, we can safely say that ambiguity prevents
the constraint from being solved.

Note [discardProvCtxtGivens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
In most situations we call all enclosing implications "useful". There is one
exception, and that is when the constraint that causes the error is from the
"provided" context of a pattern synonym declaration:

  pattern Pat :: (Num a, Eq a) => Show a   => a -> Maybe a
             --  required      => provided => type
  pattern Pat x <- (Just x, 4)

When checking the pattern RHS we must check that it does actually bind all
the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
bind the (Show a) constraint.  Answer: no!

But the implication we generate for this will look like
   forall a. (Num a, Eq a) => [W] Show a
because when checking the pattern we must make the required
constraints available, since they are needed to match the pattern (in
this case the literal '4' needs (Num a, Eq a)).

BUT we don't want to suggest adding (Show a) to the "required" constraints
of the pattern synonym, thus:
  pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
It would then typecheck but it's silly.  We want the /pattern/ to bind
the alleged "provided" constraints, Show a.

So we suppress that Implication in discardProvCtxtGivens.  It's
painfully ad-hoc but the truth is that adding it to the "required"
constraints would work.  Suppressing it solves two problems.  First,
we never tell the user that we could not deduce a "provided"
constraint from the "required" context. Second, we never give a
possible fix that suggests to add a "provided" constraint to the
"required" context.

For example, without this distinction the above code gives a bad error
message (showing both problems):

  error: Could not deduce (Show a) ... from the context: (Eq a)
         ... Possible fix: add (Show a) to the context of
         the signature for pattern synonym `Pat' ...

-}

show_fixes :: [SDoc] -> SDoc
show_fixes :: [SDoc] -> SDoc
show_fixes []     = SDoc
empty
show_fixes (SDoc
f:[SDoc]
fs) = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Possible fix:"
                        , Int -> SDoc -> SDoc
nest Int
2 ([SDoc] -> SDoc
vcat (SDoc
f SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: (SDoc -> SDoc) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> SDoc
text String
"or" SDoc -> SDoc -> SDoc
<+>) [SDoc]
fs))]


-- Avoid boolean blindness
newtype PrintPotentialInstances = PrintPotentialInstances Bool

pprPotentials :: PrintPotentialInstances -> PprStyle -> SDoc -> [ClsInst] -> SDoc
-- See Note [Displaying potential instances]
pprPotentials :: PrintPotentialInstances -> PprStyle -> SDoc -> [ClsInst] -> SDoc
pprPotentials (PrintPotentialInstances Bool
show_potentials) PprStyle
sty SDoc
herald [ClsInst]
insts
  | [ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
insts
  = SDoc
empty

  | [ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
show_these
  = SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald
       Int
2 ([SDoc] -> SDoc
vcat [ SDoc -> SDoc
not_in_scope_msg SDoc
empty
               , SDoc
flag_hint ])

  | Bool
otherwise
  = SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald
       Int
2 ([SDoc] -> SDoc
vcat [ [ClsInst] -> SDoc
pprInstances [ClsInst]
show_these
               , Bool -> SDoc -> SDoc
ppWhen (Int
n_in_scope_hidden Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                 String -> SDoc
text String
"...plus"
                   SDoc -> SDoc -> SDoc
<+> Int -> SDoc -> SDoc
speakNOf Int
n_in_scope_hidden (String -> SDoc
text String
"other")
               , SDoc -> SDoc
not_in_scope_msg (String -> SDoc
text String
"...plus")
               , SDoc
flag_hint ])
  where
    n_show :: Int
n_show = Int
3 :: Int

    ([ClsInst]
in_scope, [ClsInst]
not_in_scope) = (ClsInst -> Bool) -> [ClsInst] -> ([ClsInst], [ClsInst])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ClsInst -> Bool
inst_in_scope [ClsInst]
insts
    sorted :: [ClsInst]
sorted = (ClsInst -> ClsInst -> Ordering) -> [ClsInst] -> [ClsInst]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ClsInst -> ClsInst -> Ordering
fuzzyClsInstCmp [ClsInst]
in_scope
    show_these :: [ClsInst]
show_these | Bool
show_potentials = [ClsInst]
sorted
               | Bool
otherwise       = Int -> [ClsInst] -> [ClsInst]
forall a. Int -> [a] -> [a]
take Int
n_show [ClsInst]
sorted
    n_in_scope_hidden :: Int
n_in_scope_hidden = [ClsInst] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ClsInst]
sorted Int -> Int -> Int
forall a. Num a => a -> a -> a
- [ClsInst] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ClsInst]
show_these

       -- "in scope" means that all the type constructors
       -- are lexically in scope; these instances are likely
       -- to be more useful
    inst_in_scope :: ClsInst -> Bool
    inst_in_scope :: ClsInst -> Bool
inst_in_scope ClsInst
cls_inst = (Name -> Bool) -> NameSet -> Bool
nameSetAll Name -> Bool
name_in_scope (NameSet -> Bool) -> NameSet -> Bool
forall a b. (a -> b) -> a -> b
$
                             [TcType] -> NameSet
orphNamesOfTypes (ClsInst -> [TcType]
is_tys ClsInst
cls_inst)

    name_in_scope :: Name -> Bool
name_in_scope Name
name
      | Name -> Bool
isBuiltInSyntax Name
name
      = Bool
True -- E.g. (->)
      | Just Module
mod <- Name -> Maybe Module
nameModule_maybe Name
name
      = QualifyName -> Bool
qual_in_scope (PprStyle -> QueryQualifyName
qualName PprStyle
sty Module
mod (Name -> OccName
nameOccName Name
name))
      | Bool
otherwise
      = Bool
True

    qual_in_scope :: QualifyName -> Bool
    qual_in_scope :: QualifyName -> Bool
qual_in_scope QualifyName
NameUnqual    = Bool
True
    qual_in_scope (NameQual {}) = Bool
True
    qual_in_scope QualifyName
_             = Bool
False

    not_in_scope_msg :: SDoc -> SDoc
not_in_scope_msg SDoc
herald
      | [ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
not_in_scope
      = SDoc
empty
      | Bool
otherwise
      = SDoc -> Int -> SDoc -> SDoc
hang (SDoc
herald SDoc -> SDoc -> SDoc
<+> Int -> SDoc -> SDoc
speakNOf ([ClsInst] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ClsInst]
not_in_scope) (String -> SDoc
text String
"instance")
                     SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"involving out-of-scope types")
           Int
2 (Bool -> SDoc -> SDoc
ppWhen Bool
show_potentials ([ClsInst] -> SDoc
pprInstances [ClsInst]
not_in_scope))

    flag_hint :: SDoc
flag_hint = Bool -> SDoc -> SDoc
ppUnless (Bool
show_potentials Bool -> Bool -> Bool
|| [ClsInst] -> [ClsInst] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [ClsInst]
show_these [ClsInst]
insts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                String -> SDoc
text String
"(use -fprint-potential-instances to see them all)"

{- Note [Displaying potential instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When showing a list of instances for
  - overlapping instances (show ones that match)
  - no such instance (show ones that could match)
we want to give it a bit of structure.  Here's the plan

* Say that an instance is "in scope" if all of the
  type constructors it mentions are lexically in scope.
  These are the ones most likely to be useful to the programmer.

* Show at most n_show in-scope instances,
  and summarise the rest ("plus 3 others")

* Summarise the not-in-scope instances ("plus 4 not in scope")

* Add the flag -fshow-potential-instances which replaces the
  summary with the full list
-}

{-
Note [Flattening in error message generation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (C (Maybe (F x))), where F is a type function, and we have
instances
                C (Maybe Int) and C (Maybe a)
Since (F x) might turn into Int, this is an overlap situation, and
indeed the main solver will have refrained
from solving.  But by the time we get to error message generation, we've
un-flattened the constraint.  So we must *re*-flatten it before looking
up in the instance environment, lest we only report one matching
instance when in fact there are two.

Note [Kind arguments in error messages]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It can be terribly confusing to get an error message like (#9171)

    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
                with actual type ‘GetParam Base (GetParam Base Int)’

The reason may be that the kinds don't match up.  Typically you'll get
more useful information, but not when it's as a result of ambiguity.

To mitigate this, GHC attempts to enable the -fprint-explicit-kinds flag
whenever any error message arises due to a kind mismatch. This means that
the above error message would instead be displayed as:

    Couldn't match expected type
                  ‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
                with actual type
                  ‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’

Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
-}

mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
           -> Ct -> (Bool, SDoc)
mkAmbigMsg :: Bool -> Ct -> (Bool, SDoc)
mkAmbigMsg Bool
prepend_msg Ct
ct
  | [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
ambig_kvs Bool -> Bool -> Bool
&& [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
ambig_tvs = (Bool
False, SDoc
empty)
  | Bool
otherwise                        = (Bool
True,  SDoc
msg)
  where
    ([TcId]
ambig_kvs, [TcId]
ambig_tvs) = Ct -> ([TcId], [TcId])
getAmbigTkvs Ct
ct

    msg :: SDoc
msg |  (TcId -> Bool) -> [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcId -> Bool
isRuntimeUnkSkol [TcId]
ambig_kvs  -- See Note [Runtime skolems]
        Bool -> Bool -> Bool
|| (TcId -> Bool) -> [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcId -> Bool
isRuntimeUnkSkol [TcId]
ambig_tvs
        = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Cannot resolve unknown runtime type"
                 SDoc -> SDoc -> SDoc
<> [TcId] -> SDoc
forall a. [a] -> SDoc
plural [TcId]
ambig_tvs SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TcId]
ambig_tvs
               , String -> SDoc
text String
"Use :print or :force to determine these types"]

        | Bool -> Bool
not ([TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
ambig_tvs)
        = SDoc -> [TcId] -> SDoc
pp_ambig (String -> SDoc
text String
"type") [TcId]
ambig_tvs

        | Bool
otherwise
        = SDoc -> [TcId] -> SDoc
pp_ambig (String -> SDoc
text String
"kind") [TcId]
ambig_kvs

    pp_ambig :: SDoc -> [TcId] -> SDoc
pp_ambig SDoc
what [TcId]
tkvs
      | Bool
prepend_msg -- "Ambiguous type variable 't0'"
      = String -> SDoc
text String
"Ambiguous" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"variable"
        SDoc -> SDoc -> SDoc
<> [TcId] -> SDoc
forall a. [a] -> SDoc
plural [TcId]
tkvs SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TcId]
tkvs

      | Bool
otherwise -- "The type variable 't0' is ambiguous"
      = String -> SDoc
text String
"The" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"variable" SDoc -> SDoc -> SDoc
<> [TcId] -> SDoc
forall a. [a] -> SDoc
plural [TcId]
tkvs
        SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TcId]
tkvs SDoc -> SDoc -> SDoc
<+> [TcId] -> SDoc
forall a. [a] -> SDoc
isOrAre [TcId]
tkvs SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"ambiguous"

pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
pprSkols :: ReportErrCtxt -> [TcId] -> SDoc
pprSkols ReportErrCtxt
ctxt [TcId]
tvs
  = [SDoc] -> SDoc
vcat (((SkolemInfo, [TcId]) -> SDoc) -> [(SkolemInfo, [TcId])] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SkolemInfo, [TcId]) -> SDoc
forall {a}.
(Outputable a, NamedThing a) =>
(SkolemInfo, [a]) -> SDoc
pp_one ([Implication] -> [TcId] -> [(SkolemInfo, [TcId])]
getSkolemInfo (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt) [TcId]
tvs))
  where
    pp_one :: (SkolemInfo, [a]) -> SDoc
pp_one (SkolemInfo
UnkSkol, [a]
tvs)
      = SDoc -> Int -> SDoc -> SDoc
hang ([a] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [a]
tvs)
           Int
2 ([a] -> String -> String -> SDoc
forall {a}. [a] -> String -> String -> SDoc
is_or_are [a]
tvs String
"an" String
"unknown")
    pp_one (SkolemInfo
RuntimeUnkSkol, [a]
tvs)
      = SDoc -> Int -> SDoc -> SDoc
hang ([a] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [a]
tvs)
           Int
2 ([a] -> String -> String -> SDoc
forall {a}. [a] -> String -> String -> SDoc
is_or_are [a]
tvs String
"an" String
"unknown runtime")
    pp_one (SkolemInfo
skol_info, [a]
tvs)
      = [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang ([a] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [a]
tvs)
                  Int
2 ([a] -> String -> String -> SDoc
forall {a}. [a] -> String -> String -> SDoc
is_or_are [a]
tvs String
"a"  String
"rigid" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"bound by")
             , Int -> SDoc -> SDoc
nest Int
2 (SkolemInfo -> SDoc
pprSkolInfo SkolemInfo
skol_info)
             , Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+> SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((SrcSpan -> SrcSpan -> SrcSpan) -> [SrcSpan] -> SrcSpan
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SrcSpan -> SrcSpan -> SrcSpan
combineSrcSpans ((a -> SrcSpan) -> [a] -> [SrcSpan]
forall a b. (a -> b) -> [a] -> [b]
map a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan [a]
tvs))) ]

    is_or_are :: [a] -> String -> String -> SDoc
is_or_are [a
_] String
article String
adjective = String -> SDoc
text String
"is" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
article SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
adjective
                                      SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"type variable"
    is_or_are [a]
_   String
_       String
adjective = String -> SDoc
text String
"are" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
adjective
                                      SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"type variables"

getAmbigTkvs :: Ct -> ([Var],[Var])
getAmbigTkvs :: Ct -> ([TcId], [TcId])
getAmbigTkvs Ct
ct
  = (TcId -> Bool) -> [TcId] -> ([TcId], [TcId])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (TcId -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
dep_tkv_set) [TcId]
ambig_tkvs
  where
    tkvs :: [TcId]
tkvs       = Ct -> [TcId]
tyCoVarsOfCtList Ct
ct
    ambig_tkvs :: [TcId]
ambig_tkvs = (TcId -> Bool) -> [TcId] -> [TcId]
forall a. (a -> Bool) -> [a] -> [a]
filter TcId -> Bool
isAmbiguousTyVar [TcId]
tkvs
    dep_tkv_set :: TyCoVarSet
dep_tkv_set = [TcType] -> TyCoVarSet
tyCoVarsOfTypes ((TcId -> TcType) -> [TcId] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map TcId -> TcType
tyVarKind [TcId]
tkvs)

getSkolemInfo :: [Implication] -> [TcTyVar]
              -> [(SkolemInfo, [TcTyVar])]                    -- #14628
-- Get the skolem info for some type variables
-- from the implication constraints that bind them.
--
-- In the returned (skolem, tvs) pairs, the 'tvs' part is non-empty
getSkolemInfo :: [Implication] -> [TcId] -> [(SkolemInfo, [TcId])]
getSkolemInfo [Implication]
_ []
  = []

getSkolemInfo [] [TcId]
tvs
  | (TcId -> Bool) -> [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TcId -> Bool
isRuntimeUnkSkol [TcId]
tvs = [(SkolemInfo
RuntimeUnkSkol, [TcId]
tvs)]        -- #14628
  | Bool
otherwise = String -> SDoc -> [(SkolemInfo, [TcId])]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"No skolem info:" ([TcId] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcId]
tvs)

getSkolemInfo (Implication
implic:[Implication]
implics) [TcId]
tvs
  | [TcId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcId]
tvs_here =                            [Implication] -> [TcId] -> [(SkolemInfo, [TcId])]
getSkolemInfo [Implication]
implics [TcId]
tvs
  | Bool
otherwise   = (Implication -> SkolemInfo
ic_info Implication
implic, [TcId]
tvs_here) (SkolemInfo, [TcId])
-> [(SkolemInfo, [TcId])] -> [(SkolemInfo, [TcId])]
forall a. a -> [a] -> [a]
: [Implication] -> [TcId] -> [(SkolemInfo, [TcId])]
getSkolemInfo [Implication]
implics [TcId]
tvs_other
  where
    ([TcId]
tvs_here, [TcId]
tvs_other) = (TcId -> Bool) -> [TcId] -> ([TcId], [TcId])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (TcId -> [TcId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Implication -> [TcId]
ic_skols Implication
implic) [TcId]
tvs

-----------------------
-- relevantBindings looks at the value environment and finds values whose
-- types mention any of the offending type variables.  It has to be
-- careful to zonk the Id's type first, so it has to be in the monad.
-- We must be careful to pass it a zonked type variable, too.
--
-- We always remove closed top-level bindings, though,
-- since they are never relevant (cf #8233)

relevantBindings :: Bool  -- True <=> filter by tyvar; False <=> no filtering
                          -- See #8191
                 -> ReportErrCtxt -> Ct
                 -> TcM (ReportErrCtxt, SDoc, Ct)
-- Also returns the zonked and tidied CtOrigin of the constraint
relevantBindings :: Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
want_filtering ReportErrCtxt
ctxt Ct
ct
  = do { String -> SDoc -> TcM ()
traceTc String
"relevantBindings" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
       ; (TidyEnv
env1, CtOrigin
tidy_orig) <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt) (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc)

             -- For *kind* errors, report the relevant bindings of the
             -- enclosing *type* equality, because that's more useful for the programmer
       ; let extra_tvs :: TyCoVarSet
extra_tvs = case CtOrigin
tidy_orig of
                             KindEqOrigin TcType
t1 TcType
t2 CtOrigin
_ Maybe TypeOrKind
_ -> [TcType] -> TyCoVarSet
tyCoVarsOfTypes [TcType
t1,TcType
t2]
                             CtOrigin
_                        -> TyCoVarSet
emptyVarSet
             ct_fvs :: TyCoVarSet
ct_fvs = Ct -> TyCoVarSet
tyCoVarsOfCt Ct
ct TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
extra_tvs

             -- Put a zonked, tidied CtOrigin into the Ct
             loc' :: CtLoc
loc'   = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc CtOrigin
tidy_orig
             ct' :: Ct
ct'    = Ct -> CtLoc -> Ct
setCtLoc Ct
ct CtLoc
loc'
             ctxt1 :: ReportErrCtxt
ctxt1  = ReportErrCtxt
ctxt { cec_tidy :: TidyEnv
cec_tidy = TidyEnv
env1 }

       ; (ReportErrCtxt
ctxt2, SDoc
doc) <- Bool
-> ReportErrCtxt
-> TcLclEnv
-> TyCoVarSet
-> TcM (ReportErrCtxt, SDoc)
relevant_bindings Bool
want_filtering ReportErrCtxt
ctxt1 TcLclEnv
lcl_env TyCoVarSet
ct_fvs
       ; (ReportErrCtxt, SDoc, Ct) -> TcM (ReportErrCtxt, SDoc, Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt2, SDoc
doc, Ct
ct') }
  where
    loc :: CtLoc
loc     = Ct -> CtLoc
ctLoc Ct
ct
    lcl_env :: TcLclEnv
lcl_env = CtLoc -> TcLclEnv
ctLocEnv CtLoc
loc

-- slightly more general version, to work also with holes
relevant_bindings :: Bool
                  -> ReportErrCtxt
                  -> TcLclEnv
                  -> TyCoVarSet
                  -> TcM (ReportErrCtxt, SDoc)
relevant_bindings :: Bool
-> ReportErrCtxt
-> TcLclEnv
-> TyCoVarSet
-> TcM (ReportErrCtxt, SDoc)
relevant_bindings Bool
want_filtering ReportErrCtxt
ctxt TcLclEnv
lcl_env TyCoVarSet
ct_tvs
  = do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; String -> SDoc -> TcM ()
traceTc String
"relevant_bindings" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
           [SDoc] -> SDoc
vcat [ TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVarSet
ct_tvs
                , (SDoc -> SDoc) -> [SDoc] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas SDoc -> SDoc
forall a. a -> a
id [ TcId -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcId
id SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcId -> TcType
idType TcId
id)
                                   | TcIdBndr TcId
id TopLevelFlag
_ <- TcLclEnv -> TcBinderStack
tcl_bndrs TcLclEnv
lcl_env ]
                , (SDoc -> SDoc) -> [SDoc] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas SDoc -> SDoc
forall a. a -> a
id
                    [ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
id | TcIdBndr_ExpType Name
id ExpType
_ TopLevelFlag
_ <- TcLclEnv -> TcBinderStack
tcl_bndrs TcLclEnv
lcl_env ] ]

       ; (TidyEnv
tidy_env', [SDoc]
docs, Bool
discards)
              <- DynFlags
-> TidyEnv
-> Maybe Int
-> TyCoVarSet
-> [SDoc]
-> Bool
-> TcBinderStack
-> TcM (TidyEnv, [SDoc], Bool)
go DynFlags
dflags (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt) (DynFlags -> Maybe Int
maxRelevantBinds DynFlags
dflags)
                    TyCoVarSet
emptyVarSet [] Bool
False
                    (TcBinderStack -> TcBinderStack
forall a. HasOccName a => [a] -> [a]
removeBindingShadowing (TcBinderStack -> TcBinderStack) -> TcBinderStack -> TcBinderStack
forall a b. (a -> b) -> a -> b
$ TcLclEnv -> TcBinderStack
tcl_bndrs TcLclEnv
lcl_env)
         -- tcl_bndrs has the innermost bindings first,
         -- which are probably the most relevant ones

       ; let doc :: SDoc
doc = Bool -> SDoc -> SDoc
ppUnless ([SDoc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SDoc]
docs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                   SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Relevant bindings include")
                      Int
2 ([SDoc] -> SDoc
vcat [SDoc]
docs SDoc -> SDoc -> SDoc
$$ Bool -> SDoc -> SDoc
ppWhen Bool
discards SDoc
discardMsg)

             ctxt' :: ReportErrCtxt
ctxt' = ReportErrCtxt
ctxt { cec_tidy :: TidyEnv
cec_tidy = TidyEnv
tidy_env' }

       ; (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt', SDoc
doc) }
  where
    run_out :: Maybe Int -> Bool
    run_out :: Maybe Int -> Bool
run_out Maybe Int
Nothing = Bool
False
    run_out (Just Int
n) = Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0

    dec_max :: Maybe Int -> Maybe Int
    dec_max :: Maybe Int -> Maybe Int
dec_max = (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int
n -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)


    go :: DynFlags -> TidyEnv -> Maybe Int -> TcTyVarSet -> [SDoc]
       -> Bool                          -- True <=> some filtered out due to lack of fuel
       -> [TcBinder]
       -> TcM (TidyEnv, [SDoc], Bool)   -- The bool says if we filtered any out
                                        -- because of lack of fuel
    go :: DynFlags
-> TidyEnv
-> Maybe Int
-> TyCoVarSet
-> [SDoc]
-> Bool
-> TcBinderStack
-> TcM (TidyEnv, [SDoc], Bool)
go DynFlags
_ TidyEnv
tidy_env Maybe Int
_ TyCoVarSet
_ [SDoc]
docs Bool
discards []
      = (TidyEnv, [SDoc], Bool) -> TcM (TidyEnv, [SDoc], Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, [SDoc] -> [SDoc]
forall a. [a] -> [a]
reverse [SDoc]
docs, Bool
discards)
    go DynFlags
dflags TidyEnv
tidy_env Maybe Int
n_left TyCoVarSet
tvs_seen [SDoc]
docs Bool
discards (TcBinder
tc_bndr : TcBinderStack
tc_bndrs)
      = case TcBinder
tc_bndr of
          TcTvBndr {} -> TcM (TidyEnv, [SDoc], Bool)
discard_it
          TcIdBndr TcId
id TopLevelFlag
top_lvl -> Name -> TcType -> TopLevelFlag -> TcM (TidyEnv, [SDoc], Bool)
go2 (TcId -> Name
idName TcId
id) (TcId -> TcType
idType TcId
id) TopLevelFlag
top_lvl
          TcIdBndr_ExpType Name
name ExpType
et TopLevelFlag
top_lvl ->
            do { Maybe TcType
mb_ty <- ExpType -> TcM (Maybe TcType)
readExpType_maybe ExpType
et
                   -- et really should be filled in by now. But there's a chance
                   -- it hasn't, if, say, we're reporting a kind error en route to
                   -- checking a term. See test indexed-types/should_fail/T8129
                   -- Or we are reporting errors from the ambiguity check on
                   -- a local type signature
               ; case Maybe TcType
mb_ty of
                   Just TcType
ty -> Name -> TcType -> TopLevelFlag -> TcM (TidyEnv, [SDoc], Bool)
go2 Name
name TcType
ty TopLevelFlag
top_lvl
                   Maybe TcType
Nothing -> TcM (TidyEnv, [SDoc], Bool)
discard_it  -- No info; discard
               }
      where
        discard_it :: TcM (TidyEnv, [SDoc], Bool)
discard_it = DynFlags
-> TidyEnv
-> Maybe Int
-> TyCoVarSet
-> [SDoc]
-> Bool
-> TcBinderStack
-> TcM (TidyEnv, [SDoc], Bool)
go DynFlags
dflags TidyEnv
tidy_env Maybe Int
n_left TyCoVarSet
tvs_seen [SDoc]
docs
                        Bool
discards TcBinderStack
tc_bndrs
        go2 :: Name -> TcType -> TopLevelFlag -> TcM (TidyEnv, [SDoc], Bool)
go2 Name
id_name TcType
id_type TopLevelFlag
top_lvl
          = do { (TidyEnv
tidy_env', TcType
tidy_ty) <- TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
tidy_env TcType
id_type
               ; String -> SDoc -> TcM ()
traceTc String
"relevantBindings 1" (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
id_name SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
tidy_ty)
               ; let id_tvs :: TyCoVarSet
id_tvs = TcType -> TyCoVarSet
tyCoVarsOfType TcType
tidy_ty
                     doc :: SDoc
doc = [SDoc] -> SDoc
sep [ Name -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc Name
id_name SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
tidy_ty
                               , Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc
parens (String -> SDoc
text String
"bound at"
                                    SDoc -> SDoc -> SDoc
<+> SrcLoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Name -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Name
id_name)))]
                     new_seen :: TyCoVarSet
new_seen = TyCoVarSet
tvs_seen TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
id_tvs

               ; if (Bool
want_filtering Bool -> Bool -> Bool
&& Bool -> Bool
not (DynFlags -> Bool
hasPprDebug DynFlags
dflags)
                                    Bool -> Bool -> Bool
&& TyCoVarSet
id_tvs TyCoVarSet -> TyCoVarSet -> Bool
`disjointVarSet` TyCoVarSet
ct_tvs)
                          -- We want to filter out this binding anyway
                          -- so discard it silently
                 then TcM (TidyEnv, [SDoc], Bool)
discard_it

                 else if TopLevelFlag -> Bool
isTopLevel TopLevelFlag
top_lvl Bool -> Bool -> Bool
&& Bool -> Bool
not (Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Int
n_left)
                          -- It's a top-level binding and we have not specified
                          -- -fno-max-relevant-bindings, so discard it silently
                 then TcM (TidyEnv, [SDoc], Bool)
discard_it

                 else if Maybe Int -> Bool
run_out Maybe Int
n_left Bool -> Bool -> Bool
&& TyCoVarSet
id_tvs TyCoVarSet -> TyCoVarSet -> Bool
`subVarSet` TyCoVarSet
tvs_seen
                          -- We've run out of n_left fuel and this binding only
                          -- mentions already-seen type variables, so discard it
                 then DynFlags
-> TidyEnv
-> Maybe Int
-> TyCoVarSet
-> [SDoc]
-> Bool
-> TcBinderStack
-> TcM (TidyEnv, [SDoc], Bool)
go DynFlags
dflags TidyEnv
tidy_env Maybe Int
n_left TyCoVarSet
tvs_seen [SDoc]
docs
                         Bool
True      -- Record that we have now discarded something
                         TcBinderStack
tc_bndrs

                          -- Keep this binding, decrement fuel
                 else DynFlags
-> TidyEnv
-> Maybe Int
-> TyCoVarSet
-> [SDoc]
-> Bool
-> TcBinderStack
-> TcM (TidyEnv, [SDoc], Bool)
go DynFlags
dflags TidyEnv
tidy_env' (Maybe Int -> Maybe Int
dec_max Maybe Int
n_left) TyCoVarSet
new_seen
                         (SDoc
docSDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
:[SDoc]
docs) Bool
discards TcBinderStack
tc_bndrs }


discardMsg :: SDoc
discardMsg :: SDoc
discardMsg = String -> SDoc
text String
"(Some bindings suppressed;" SDoc -> SDoc -> SDoc
<+>
             String -> SDoc
text String
"use -fmax-relevant-binds=N or -fno-max-relevant-binds)"

-----------------------
warnDefaulting :: [Ct] -> Type -> TcM ()
warnDefaulting :: [Ct] -> TcType -> TcM ()
warnDefaulting [Ct]
wanteds TcType
default_ty
  = do { Bool
warn_default <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnTypeDefaults
       ; TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
       ; let tidy_env :: TidyEnv
tidy_env = TidyEnv -> [TcId] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env0 ([TcId] -> TidyEnv) -> [TcId] -> TidyEnv
forall a b. (a -> b) -> a -> b
$
                        Cts -> [TcId]
tyCoVarsOfCtsList ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
wanteds)
             tidy_wanteds :: [Ct]
tidy_wanteds = (Ct -> Ct) -> [Ct] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> Ct -> Ct
tidyCt TidyEnv
tidy_env) [Ct]
wanteds
             (CtLoc
loc, SDoc
ppr_wanteds) = [Ct] -> (CtLoc, SDoc)
pprWithArising [Ct]
tidy_wanteds
             warn_msg :: SDoc
warn_msg =
                SDoc -> Int -> SDoc -> SDoc
hang ([SDoc] -> SDoc
hsep [ String -> SDoc
text String
"Defaulting the following"
                           , String -> SDoc
text String
"constraint" SDoc -> SDoc -> SDoc
<> [Ct] -> SDoc
forall a. [a] -> SDoc
plural [Ct]
tidy_wanteds
                           , String -> SDoc
text String
"to type"
                           , SDoc -> SDoc
quotes (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
default_ty) ])
                     Int
2
                     SDoc
ppr_wanteds
       ; CtLoc -> TcM () -> TcM ()
forall a. CtLoc -> TcM a -> TcM a
setCtLocM CtLoc
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ WarnReason -> Bool -> SDoc -> TcM ()
warnTc (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnTypeDefaults) Bool
warn_default SDoc
warn_msg }

{-
Note [Runtime skolems]
~~~~~~~~~~~~~~~~~~~~~~
We want to give a reasonably helpful error message for ambiguity
arising from *runtime* skolems in the debugger.  These
are created by in GHC.Runtime.Heap.Inspect.zonkRTTIType.

************************************************************************
*                                                                      *
                 Error from the canonicaliser
         These ones are called *during* constraint simplification
*                                                                      *
************************************************************************
-}

solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
solverDepthErrorTcS :: forall a. CtLoc -> TcType -> TcM a
solverDepthErrorTcS CtLoc
loc TcType
ty
  = CtLoc -> TcM a -> TcM a
forall a. CtLoc -> TcM a -> TcM a
setCtLocM CtLoc
loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
    do { TcType
ty <- TcType -> TcM TcType
zonkTcType TcType
ty
       ; TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
       ; let tidy_env :: TidyEnv
tidy_env     = TidyEnv -> [TcId] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env0 (TcType -> [TcId]
tyCoVarsOfTypeList TcType
ty)
             tidy_ty :: TcType
tidy_ty      = TidyEnv -> TcType -> TcType
tidyType TidyEnv
tidy_env TcType
ty
             msg :: SDoc
msg
               = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Reduction stack overflow; size =" SDoc -> SDoc -> SDoc
<+> SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr SubGoalDepth
depth
                      , SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"When simplifying the following type:")
                           Int
2 (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
tidy_ty)
                      , SDoc
note ]
       ; (TidyEnv, SDoc) -> TcM a
forall a. (TidyEnv, SDoc) -> TcM a
failWithTcM (TidyEnv
tidy_env, SDoc
msg) }
  where
    depth :: SubGoalDepth
depth = CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc
    note :: SDoc
note = [SDoc] -> SDoc
vcat
      [ String -> SDoc
text String
"Use -freduction-depth=0 to disable this check"
      , String -> SDoc
text String
"(any upper bound you could choose might fail unpredictably with"
      , String -> SDoc
text String
" minor updates to GHC, so disabling the check is recommended if"
      , String -> SDoc
text String
" you're sure that type checking should terminate)" ]