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

{-# 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.Unify( occCheckForErrors, MetaTyVarUpdateResult(..) )
import GHC.Tc.Utils.Env( tcInitTidyEnv )
import GHC.Tc.Utils.TcType
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 )
import GHC.Unit.Module
import GHC.Tc.Instance.Family
import GHC.Core.FamInstEnv ( flattenTys )
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  ( ErrMsg, errDoc, pprLocErrMsg )
import GHC.Types.Basic
import GHC.Types.Unique.Set ( nonDetEltsUniqSet )
import GHC.Core.ConLike ( ConLike(..))
import GHC.Utils.Misc
import GHC.Data.FastString
import GHC.Utils.Outputable
import GHC.Types.SrcLoc
import GHC.Driver.Session
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, nub, 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")
-- and for simplifyDefault.
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
            -- If we are deferring we are going to need /all/ evidence around,
            -- including the evidence produced by unflattening (zonkWC)
       ; let tidy_env :: TidyEnv
tidy_env = TidyEnv -> [TcId] -> TidyEnv
tidyFreeTyCoVars TidyEnv
emptyTidyEnv [TcId]
free_tvs
             free_tvs :: [TcId]
free_tvs = WantedConstraints -> [TcId]
tyCoVarsOfWCList WantedConstraints
wanted

       ; 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 :: [Implication]
-> TidyEnv
-> EvBindsVar
-> TypeErrorChoice
-> HoleChoice
-> HoleChoice
-> HoleChoice
-> Bool
-> Bool
-> Bool
-> ReportErrCtxt
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

-- | Transforms a 'ReportErrCtxt' into one that does not defer any bindings
-- at all.
noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
noDeferredBindings ReportErrCtxt
ctxt = 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 }

{- 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]
tvs
    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 | CoEvBindsVar{} <- EvBindsVar
evb    = ReportErrCtxt -> ReportErrCtxt
noDeferredBindings ReportErrCtxt
ctxt
          | Bool
otherwise                = ReportErrCtxt
ctxt
          -- 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.

    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
      ; ErrMsg
msg <- ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
env (SDoc -> Report
important SDoc
doc)
      ; WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnRedundantConstraints) ErrMsg
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 { ErrMsg
msg <- ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
env (SDoc -> Report
important SDoc
doc)
      ; WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnRedundantConstraints) ErrMsg
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 (Kind -> Bool
improving (Kind -> Bool) -> (TcId -> Kind) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcId -> Kind
idType) [TcId]
ev_vars
         SkolemInfo
_        -> [TcId]
ev_vars

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

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

reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcTyVar] -> TcM ()
reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcId] -> TcM ()
reportBadTelescope ReportErrCtxt
ctxt TcLclEnv
env (ForAllSkol SDoc
_ SDoc
telescope) [TcId]
skols
  = do { ErrMsg
msg <- ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
env (SDoc -> Report
important SDoc
doc)
       ; ErrMsg -> TcM ()
reportError ErrMsg
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 ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkEqErr)
              , (String
"skolem eq1",   (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
forall {p}. p -> Pred -> Bool
very_wrong,     Bool
True, Reporter
mkSkolReporter)
              , (String
"skolem eq2",   (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
forall {p}. p -> 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 ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkEqErr)
              , (String
"Other eqs",     (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
unblocked Ct -> Pred -> Bool
is_equality,      Bool
True,  (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkEqErr)
              , (String
"Blocked eqs",   Ct -> Pred -> Bool
is_equality,           Bool
False, (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
mkSuppressReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkIPErr)
              , (String
"Irreds",          Ct -> Pred -> Bool
is_irred,        Bool
False, (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkIrredErr)
              , (String
"Dicts",           Ct -> Pred -> Bool
is_dict,         Bool
False, (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkDictErr) ]

    -- also checks to make sure the constraint isn't BlockedCIS
    -- 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_status :: Ct -> CtIrredStatus
cc_status = CtIrredStatus
BlockedCIS }) 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 Kind
ty1 Kind
ty2) = Kind -> Bool
isRigidTy Kind
ty1 Bool -> Bool -> Bool
&& Kind -> Bool
isRigidTy Kind
ty2
    utterly_wrong p
_ Pred
_                      = Bool
False

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

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

    -- Things like (F a  ~N  Int)
    non_tv_eq :: p -> Pred -> Bool
non_tv_eq p
_ (EqPred EqRel
NomEq Kind
ty1 Kind
_) = Bool -> Bool
not (Kind -> Bool
isTyVarTy Kind
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
_ Kind
ty1 Kind
ty2) = HasDebugCallStack => Kind -> Kind
Kind -> Kind
tcTypeKind Kind
ty1 HasDebugCallStack => Kind -> Kind -> Bool
Kind -> Kind -> Bool
`tcEqType` HasDebugCallStack => Kind -> Kind
Kind -> Kind
tcTypeKind Kind
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 [Kind]
_) = 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
      , Bool -> Bool
not (Implication -> Bool
ic_no_eqs Implication
implic)
      , 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 -> Kind -> Bool
isSkolemTy TcLevel
tc_lvl Kind
ty
  | Just TcId
tv <- Kind -> Maybe TcId
getTyVar_maybe Kind
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 :: Kind -> Maybe TyCon
isTyFun_maybe Kind
ty = case HasCallStack => Kind -> Maybe (TyCon, [Kind])
Kind -> Maybe (TyCon, [Kind])
tcSplitTyConApp_maybe Kind
ty of
                      Just (TyCon
tc,[Kind]
_) | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tc
                      Maybe (TyCon, [Kind])
_ -> 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 ErrMsg) -> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 { ErrMsg
err <- [Ct] -> ReportErrCtxt -> Hole -> TcM ErrMsg
mkHoleError [Ct]
tidy_cts ReportErrCtxt
ctxt Hole
hole
                        ; ReportErrCtxt -> Hole -> ErrMsg -> TcM ()
maybeReportHoleError ReportErrCtxt
ctxt Hole
hole ErrMsg
err
                        ; ReportErrCtxt -> ErrMsg -> Hole -> TcM ()
maybeAddDeferredHoleBinding ReportErrCtxt
ctxt ErrMsg
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
  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 { ErrMsg
err <- ReportErrCtxt -> Ct -> TcM ErrMsg
mkUserTypeError ReportErrCtxt
ctxt Ct
ct
                      ; ReportErrCtxt -> ErrMsg -> TcM ()
maybeReportError ReportErrCtxt
ctxt ErrMsg
err
                      ; ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt ErrMsg
err Ct
ct }

mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
mkUserTypeError ReportErrCtxt
ctxt Ct
ct = ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct
                        (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
forall a b. (a -> b) -> a -> b
$ SDoc -> Report
important
                        (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ Kind -> SDoc
pprUserTypeErrorTy
                        (Kind -> SDoc) -> Kind -> SDoc
forall a b. (a -> b) -> a -> b
$ case Ct -> Maybe Kind
getUserTypeErrorMsg Ct
ct of
                            Just Kind
msg -> Kind
msg
                            Maybe Kind
Nothing  -> String -> SDoc -> Kind
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

       ; ErrMsg
err <- DynFlags
-> ReportErrCtxt -> Report -> Ct -> Kind -> Kind -> TcM ErrMsg
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct' Kind
ty1 Kind
ty2

       ; String -> SDoc -> TcM ()
traceTc String
"mkGivenErrorReporter" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
       ; WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnInaccessibleCode) ErrMsg
err }
  where
    (Ct
ct : [Ct]
_ )  = [Ct]
cts    -- Never empty
    (Kind
ty1, Kind
ty2) = Kind -> (Kind, Kind)
getEqPredTys (Ct -> Kind
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 ErrMsg)
                             -- 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 ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 ErrMsg) -> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 ErrMsg) -> Reporter
mkSuppressReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
mkSuppressReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 ErrMsg) -> Reporter
suppressGroup ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 (Kind -> Pred
classifyPredType (Ct -> Kind
ctPred Ct
ct1), Kind -> Pred
classifyPredType (Ct -> Kind
ctPred Ct
ct2)) of
       (EqPred EqRel
eq_rel1 Kind
ty1 Kind
_, EqPred EqRel
eq_rel2 Kind
ty2 Kind
_) ->
         (EqRel
eq_rel1 EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
eq_rel2) Bool -> Bool -> Bool
&& (Kind
ty1 Kind -> Kind -> Bool
`eqType` Kind
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 = CtLoc -> RealSrcSpan
ctLocSpan (Ct -> CtLoc
ctLoc Ct
ct1) RealSrcSpan -> RealSrcSpan -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` CtLoc -> RealSrcSpan
ctLocSpan (Ct -> CtLoc
ctLoc Ct
ct2)

reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM ErrMsg
mk_err ReportErrCtxt
ctxt [Ct]
cts =
  ASSERT( not (null cts))
  do { ErrMsg
err <- ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 -> ErrMsg -> TcM ()
maybeReportError ReportErrCtxt
ctxt ErrMsg
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 -> ErrMsg -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt ErrMsg
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 ErrMsg) -> Reporter
suppressGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
suppressGroup ReportErrCtxt -> [Ct] -> TcM ErrMsg
mk_err ReportErrCtxt
ctxt [Ct]
cts
 = do { ErrMsg
err <- ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 -> ErrMsg -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt ErrMsg
err) [Ct]
cts }

maybeReportHoleError :: ReportErrCtxt -> Hole -> ErrMsg -> TcM ()
maybeReportHoleError :: ReportErrCtxt -> Hole -> ErrMsg -> TcM ()
maybeReportHoleError ReportErrCtxt
ctxt Hole
hole ErrMsg
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 -> ErrMsg -> TcM ()
reportError ErrMsg
err
      HoleChoice
HoleWarn  ->
        WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnDeferredOutOfScopeVariables) ErrMsg
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
TypeHole }) ErrMsg
err
  -- 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 -> ErrMsg -> TcM ()
reportError ErrMsg
err
       HoleChoice
HoleWarn  -> WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnPartialTypeSignatures) ErrMsg
err
       HoleChoice
HoleDefer -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

maybeReportHoleError ReportErrCtxt
ctxt hole :: Hole
hole@(Hole { hole_sort :: Hole -> HoleSort
hole_sort = ExprHole TcId
_ }) ErrMsg
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 -> ErrMsg -> TcM ()
reportError ErrMsg
err
       HoleChoice
HoleWarn  -> WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnTypedHoles) ErrMsg
err
       HoleChoice
HoleDefer -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
-- Report the error and/or make a deferred binding for it
maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
maybeReportError ReportErrCtxt
ctxt ErrMsg
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 -> ErrMsg -> TcM ()
reportWarning WarnReason
reason ErrMsg
err
      TypeErrorChoice
TypeError       -> ErrMsg -> TcM ()
reportError ErrMsg
err

addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
-- See Note [Deferring coercion errors to runtime]
addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt ErrMsg
err Ct
ct
  | ReportErrCtxt -> Bool
deferringAnyBindings ReportErrCtxt
ctxt
  , CtWanted { ctev_pred :: CtEvidence -> Kind
ctev_pred = Kind
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 -> Kind -> ErrMsg -> EvTerm
mkErrorTerm DynFlags
dflags Kind
pred ErrMsg
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
            -> ErrMsg -> EvTerm
mkErrorTerm :: DynFlags -> Kind -> ErrMsg -> EvTerm
mkErrorTerm DynFlags
dflags Kind
ty ErrMsg
err = Kind -> FastString -> EvTerm
evDelayedError Kind
ty FastString
err_fs
  where
    err_msg :: SDoc
err_msg = ErrMsg -> SDoc
pprLocErrMsg ErrMsg
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 -> ErrMsg -> Hole -> TcM ()
maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Hole -> TcM ()
maybeAddDeferredHoleBinding ReportErrCtxt
ctxt ErrMsg
err (Hole { hole_sort :: Hole -> HoleSort
hole_sort = ExprHole TcId
ev_id })
-- 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 -> Kind -> ErrMsg -> EvTerm
mkErrorTerm DynFlags
dflags (TcId -> Kind
idType TcId
ev_id) ErrMsg
err
           -- NB: idType ev_id, not hole_ty. hole_ty might be rewritten.
           -- See Note [Holes] in GHC.Tc.Types.Constraint
       ; EvBindsVar -> EvBind -> TcM ()
addTcEvBind (ReportErrCtxt -> EvBindsVar
cec_binds ReportErrCtxt
ctxt) (EvBind -> TcM ()) -> EvBind -> TcM ()
forall a b. (a -> b) -> a -> b
$ TcId -> EvTerm -> EvBind
mkWantedEvBind TcId
ev_id EvTerm
err_tm }
  | Bool
otherwise
  = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
maybeAddDeferredHoleBinding ReportErrCtxt
_ ErrMsg
_ (Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
TypeHole })
  = () -> 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 (Kind -> Pred
classifyPredType (Ct -> Kind
ctPred Ct
ct))) [Ct]
cts

pprArising :: CtOrigin -> SDoc
-- Used for the main, top-level error message
-- We've done special processing for TypeEq, KindEq, Given
pprArising :: CtOrigin -> SDoc
pprArising (TypeEqOrigin {}) = SDoc
empty
pprArising (KindEqOrigin {}) = SDoc
empty
pprArising (GivenOrigin {})  = SDoc
empty
pprArising CtOrigin
orig              = 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)
                     ([Kind] -> SDoc
pprTheta [Ct -> Kind
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 (Kind -> SDoc
pprType (Ct -> Kind
ctPred Ct
ct')))
                     Int
2 (CtLoc -> SDoc
pprCtLoc (Ct -> CtLoc
ctLoc Ct
ct'))

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

mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
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 -> ErrDoc -> TcM ErrMsg
mkErrDocAt (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan (TcLclEnv -> RealSrcSpan
tcl_loc TcLclEnv
tcl_env) Maybe BufSpan
forall a. Maybe a
Nothing)
            ([SDoc] -> [SDoc] -> [SDoc] -> ErrDoc
errDoc [SDoc]
important [SDoc
context] ([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 ErrMsg
mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
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] -> ([Kind], CtOrigin) -> Report
couldNotDeduce (ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt) ((Ct -> Kind) -> [Ct] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> Kind
ctPred [Ct]
cts, CtOrigin
orig)
       ; ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct1 (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
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 ErrMsg
mkHoleError :: [Ct] -> ReportErrCtxt -> Hole -> TcM ErrMsg
mkHoleError [Ct]
_tidy_simples ReportErrCtxt
_ctxt hole :: Hole
hole@(Hole { hole_occ :: Hole -> OccName
hole_occ = OccName
occ
                                           , hole_ty :: Hole -> Kind
hole_ty = Kind
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 -> ErrDoc -> TcM ErrMsg
mkErrDocAt (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan (TcLclEnv -> RealSrcSpan
tcl_loc TcLclEnv
lcl_env) Maybe BufSpan
forall a. Maybe a
Nothing) (ErrDoc -> TcM ErrMsg) -> ErrDoc -> TcM ErrMsg
forall a b. (a -> b) -> a -> b
$
                    [SDoc] -> [SDoc] -> [SDoc] -> ErrDoc
errDoc [SDoc
out_of_scope_msg] []
                           [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 -> Kind -> SDoc
pp_occ_with_type OccName
occ Kind
hole_ty)

    lcl_env :: TcLclEnv
lcl_env     = CtLoc -> TcLclEnv
ctLocEnv CtLoc
ct_loc
    boring_type :: Bool
boring_type = Kind -> Bool
isTyVarTy Kind
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 -> Kind
hole_ty = Kind
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 (Kind -> TyCoVarSet
tyCoVarsOfType Kind
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 TcId
_ <- 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 ErrMsg
mkErrorReport ReportErrCtxt
ctxt TcLclEnv
lcl_env (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
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 :: Kind
hole_kind   = HasDebugCallStack => Kind -> Kind
Kind -> Kind
tcTypeKind Kind
hole_ty
    tyvars :: [TcId]
tyvars      = Kind -> [TcId]
tyCoVarsOfTypeList Kind
hole_ty

    hole_msg :: SDoc
hole_msg = case HoleSort
sort of
      ExprHole TcId
_ -> [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Found hole:")
                            Int
2 (OccName -> Kind -> SDoc
pp_occ_with_type OccName
occ Kind
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 ]

    pp_hole_type_with_kind :: SDoc
pp_hole_type_with_kind
      | Kind -> Bool
isLiftedTypeKind Kind
hole_kind
        Bool -> Bool -> Bool
|| Kind -> Bool
isCoVarType Kind
hole_ty -- Don't print the kind of unlifted
                               -- equalities (#15039)
      = Kind -> SDoc
pprType Kind
hole_ty
      | Bool
otherwise
      = Kind -> SDoc
pprType Kind
hole_ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Kind -> SDoc
pprKind Kind
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 -> Kind -> SDoc
pp_occ_with_type OccName
occ Kind
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
<+> Kind -> SDoc
pprType Kind
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 :: [(Kind, 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
             ; (Kind, RealSrcSpan) -> [(Kind, RealSrcSpan)]
forall (m :: * -> *) a. Monad m => a -> m a
return (TcId -> Kind
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 ([(Kind, RealSrcSpan)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Kind, 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
$ ((Kind, RealSrcSpan) -> SDoc) -> [(Kind, RealSrcSpan)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Kind, RealSrcSpan) -> SDoc
forall {a} {a}. (Outputable a, Outputable a) => (a, a) -> SDoc
pprConstraint [(Kind, RealSrcSpan)]
constraints)

----------------
mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
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 :: [Kind]
preds   = (Ct -> Kind) -> [Ct] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> Kind
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 ([Kind] -> SDoc
pprParendTheta [Kind]
preds) ]
                 | Bool
otherwise
                 = [Implication] -> ([Kind], CtOrigin) -> Report
couldNotDeduce [Implication]
givens ([Kind]
preds, CtOrigin
orig)

       ; ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct1 (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
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 ErrMsg
mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkEqErr ReportErrCtxt
ctxt (Ct
ct:[Ct]
_) = ReportErrCtxt -> Ct -> TcM ErrMsg
mkEqErr1 ReportErrCtxt
ctxt Ct
ct
mkEqErr ReportErrCtxt
_ [] = String -> TcM ErrMsg
forall a. String -> a
panic String
"mkEqErr"

mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
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 -> Kind -> Kind -> SDoc
mkCoercibleExplanation GlobalRdrEnv
rdr_env FamInstEnvs
fam_envs Kind
ty1 Kind
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 -> Kind -> Kind -> TcM ErrMsg
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Kind
ty1 Kind
ty2 }
  where
    (Kind
ty1, Kind
ty2) = Kind -> (Kind, Kind)
getEqPredTys (Ct -> Kind
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 -> Kind -> Kind -> SDoc
mkCoercibleExplanation GlobalRdrEnv
rdr_env FamInstEnvs
fam_envs Kind
ty1 Kind
ty2
  | Just (TyCon
tc, [Kind]
tys) <- HasCallStack => Kind -> Maybe (TyCon, [Kind])
Kind -> Maybe (TyCon, [Kind])
tcSplitTyConApp_maybe Kind
ty1
  , (TyCon
rep_tc, [Kind]
_, Coercion
_) <- FamInstEnvs -> TyCon -> [Kind] -> (TyCon, [Kind], Coercion)
tcLookupDataFamInst FamInstEnvs
fam_envs TyCon
tc [Kind]
tys
  , Just SDoc
msg <- TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
rep_tc
  = SDoc
msg
  | Just (TyCon
tc, [Kind]
tys) <- HasDebugCallStack => Kind -> Maybe (TyCon, [Kind])
Kind -> Maybe (TyCon, [Kind])
splitTyConApp_maybe Kind
ty2
  , (TyCon
rep_tc, [Kind]
_, Coercion
_) <- FamInstEnvs -> TyCon -> [Kind] -> (TyCon, [Kind], Coercion)
tcLookupDataFamInst FamInstEnvs
fam_envs TyCon
tc [Kind]
tys
  , Just SDoc
msg <- TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
rep_tc
  = SDoc
msg
  | Just (Kind
s1, Kind
_) <- Kind -> Maybe (Kind, Kind)
tcSplitAppTy_maybe Kind
ty1
  , Just (Kind
s2, Kind
_) <- Kind -> Maybe (Kind, Kind)
tcSplitAppTy_maybe Kind
ty2
  , Kind
s1 Kind -> Kind -> Bool
`eqType` Kind
s2
  , Kind -> Bool
has_unknown_roles Kind
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 (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
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 :: Kind -> Bool
has_unknown_roles Kind
ty
      | Just (TyCon
tc, [Kind]
tys) <- HasCallStack => Kind -> Maybe (TyCon, [Kind])
Kind -> Maybe (TyCon, [Kind])
tcSplitTyConApp_maybe Kind
ty
      = [Kind]
tys [Kind] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` TyCon -> Int
tyConArity TyCon
tc  -- oversaturated tycon
      | Just (Kind
s, Kind
_) <- Kind -> Maybe (Kind, Kind)
tcSplitAppTy_maybe Kind
ty
      = Kind -> Bool
has_unknown_roles Kind
s
      | Kind -> Bool
isTyVarTy Kind
ty
      = Bool
True
      | Bool
otherwise
      = Bool
False

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

reportEqErr :: ReportErrCtxt -> Report
            -> Ct
            -> TcType -> TcType -> TcM ErrMsg
reportEqErr :: ReportErrCtxt -> Report -> Ct -> Kind -> Kind -> TcM ErrMsg
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct Kind
ty1 Kind
ty2
  = ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
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 -> Kind -> Kind -> Report
misMatchOrCND Bool
False ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2
    eqInfo :: Report
eqInfo   = Ct -> Kind -> Kind -> Report
mkEqInfoMsg Ct
ct Kind
ty1 Kind
ty2

mkTyVarEqErr, mkTyVarEqErr'
  :: DynFlags -> ReportErrCtxt -> Report -> Ct
             -> TcTyVar -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
mkTyVarEqErr :: DynFlags
-> ReportErrCtxt -> Report -> Ct -> TcId -> Kind -> TcM ErrMsg
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 Kind
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
$$ Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
ty2)
       ; DynFlags
-> ReportErrCtxt -> Report -> Ct -> TcId -> Kind -> TcM ErrMsg
mkTyVarEqErr' DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 Kind
ty2 }

mkTyVarEqErr' :: DynFlags
-> ReportErrCtxt -> Report -> Ct -> TcId -> Kind -> TcM ErrMsg
mkTyVarEqErr' DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct TcId
tv1 Kind
ty2
  | ReportErrCtxt -> TcId -> Bool
isUserSkolem ReportErrCtxt
ctxt 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 (Kind -> Bool
isTyVarTy Kind
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 ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat
        [ Report
headline_msg
        , ReportErrCtxt -> TcId -> Kind -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 Kind
ty2
        , Report
report
        ]

  | MetaTyVarUpdateResult ()
MTVU_Occurs <- MetaTyVarUpdateResult ()
occ_check_expand
    -- 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 -> Kind -> Kind -> Report
mkEqInfoMsg Ct
ct Kind
ty1 Kind
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
. Kind -> Bool
noFreeVarsOfType (Kind -> Bool) -> (TcId -> Kind) -> TcId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcId -> Kind
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
$
                                  Kind -> FV
tyCoFVsOfType Kind
ty1 FV -> FV -> FV
`unionFV` Kind -> FV
tyCoFVsOfType Kind
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
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcId -> Kind
tyVarKind TcId
tv)
       ; ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
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] }

  | MetaTyVarUpdateResult ()
MTVU_Bad <- MetaTyVarUpdateResult ()
occ_check_expand
  = do { let msg :: SDoc
msg = [SDoc] -> SDoc
vcat [ 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 (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
ty2) ]
       -- 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 ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [ Report
headline_msg, SDoc -> Report
important SDoc
msg, 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 ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
forall a b. (a -> b) -> a -> b
$ [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat
        [ ReportErrCtxt -> Ct -> Kind -> Kind -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2
        , ReportErrCtxt -> TcId -> Kind -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 Kind
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` (Kind -> TyCoVarSet
tyCoVarsOfType Kind
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 -> Kind -> Kind -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
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 ErrMsg
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 -> Kind -> Kind -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
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 -> Kind -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 Kind
ty2
             add_sig :: Report
add_sig  = ReportErrCtxt -> Kind -> Kind -> Report
suggestAddSig ReportErrCtxt
ctxt Kind
ty1 Kind
ty2
       ; ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct (Report -> TcM ErrMsg) -> Report -> TcM ErrMsg
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 -> Kind -> Kind -> TcM ErrMsg
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct (TcId -> Kind
mkTyVarTy TcId
tv1) Kind
ty2
        -- This *can* happen (#6123, and test T2627b)
        -- 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 -> Kind -> Kind -> Report
misMatchOrCND Bool
insoluble_occurs_check ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2

    ty1 :: Kind
ty1 = TcId -> Kind
mkTyVarTy TcId
tv1
    occ_check_expand :: MetaTyVarUpdateResult ()
occ_check_expand       = DynFlags -> TcId -> Kind -> MetaTyVarUpdateResult ()
occCheckForErrors DynFlags
dflags TcId
tv1 Kind
ty2
    insoluble_occurs_check :: Bool
insoluble_occurs_check = EqRel -> TcId -> Kind -> Bool
isInsolubleOccursCheck (Ct -> EqRel
ctEqRel Ct
ct) TcId
tv1 Kind
ty2

    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 -> Kind -> Kind -> Report
mkEqInfoMsg Ct
ct Kind
ty1 Kind
ty2
  = SDoc -> Report
important (SDoc
tyfun_msg SDoc -> SDoc -> SDoc
$$ SDoc
ambig_msg)
  where
    mb_fun1 :: Maybe TyCon
mb_fun1 = Kind -> Maybe TyCon
isTyFun_maybe Kind
ty1
    mb_fun2 :: Maybe TyCon
mb_fun2 = Kind -> Maybe TyCon
isTyFun_maybe Kind
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

isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
-- See Note [Reporting occurs-check errors]
isUserSkolem :: ReportErrCtxt -> TcId -> Bool
isUserSkolem ReportErrCtxt
ctxt TcId
tv
  = TcId -> Bool
isSkolemTyVar TcId
tv Bool -> Bool -> Bool
&& (Implication -> Bool) -> [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Implication -> Bool
is_user_skol_tv (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt)
  where
    is_user_skol_tv :: Implication -> Bool
is_user_skol_tv (Implic { ic_skols :: Implication -> [TcId]
ic_skols = [TcId]
sks, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info })
      = TcId
tv TcId -> [TcId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TcId]
sks Bool -> Bool -> Bool
&& SkolemInfo -> Bool
is_user_skol_info SkolemInfo
skol_info

    is_user_skol_info :: SkolemInfo -> Bool
is_user_skol_info (InferSkol {}) = Bool
False
    is_user_skol_info SkolemInfo
_ = Bool
True

misMatchOrCND :: Bool -> ReportErrCtxt -> Ct
              -> TcType -> TcType -> Report
-- If oriented then ty1 is actual, ty2 is expected
misMatchOrCND :: Bool -> ReportErrCtxt -> Ct -> Kind -> Kind -> Report
misMatchOrCND Bool
insoluble_occurs_check ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2
  | Bool
insoluble_occurs_check  -- See Note [Insoluble occurs check]
    Bool -> Bool -> Bool
|| (Kind -> Bool
isRigidTy Kind
ty1 Bool -> Bool -> Bool
&& Kind -> Bool
isRigidTy Kind
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 -> Kind -> Kind -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2

  | Bool
otherwise
  = [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [ [Implication] -> ([Kind], CtOrigin) -> Report
couldNotDeduce [Implication]
givens ([Kind
eq_pred], CtOrigin
orig)
            , SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> TypeOrKind -> Kind -> Kind -> CtOrigin -> SDoc
mk_supplementary_ea_msg ReportErrCtxt
ctxt TypeOrKind
level Kind
ty1 Kind
ty2 CtOrigin
orig ]
  where
    ev :: CtEvidence
ev      = Ct -> CtEvidence
ctEvidence Ct
ct
    eq_pred :: Kind
eq_pred = CtEvidence -> Kind
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, Bool -> Bool
not (Implication -> Bool
ic_no_eqs Implication
given)]
              -- Keep only UserGivens that have some equalities.
              -- See Note [Suppress redundant givens during error reporting]

couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> Report
couldNotDeduce :: [Implication] -> ([Kind], CtOrigin) -> Report
couldNotDeduce [Implication]
givens ([Kind]
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
<+> [Kind] -> SDoc
pprTheta [Kind]
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 -> Kind) -> [TcId] -> [TcId]
forall a. (a -> Kind) -> [a] -> [a]
mkMinimalBySCs TcId -> Kind
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 ErrMsg
mkBlockedEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkBlockedEqErr ReportErrCtxt
ctxt (Ct
ct:[Ct]
_) = ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
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 (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct -> Kind
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 ErrMsg
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_no_eqs` field of the Implication).

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_no_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 -> Kind -> Report
extraTyVarEqInfo ReportErrCtxt
ctxt TcId
tv1 Kind
ty2
  = SDoc -> Report
important (ReportErrCtxt -> TcId -> SDoc
extraTyVarInfo ReportErrCtxt
ctxt TcId
tv1 SDoc -> SDoc -> SDoc
$$ Kind -> SDoc
ty_extra Kind
ty2)
  where
    ty_extra :: Kind -> SDoc
ty_extra Kind
ty = case Kind -> Maybe (TcId, Coercion)
tcGetCastedTyVar_maybe Kind
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 -> Kind -> Kind -> Report
suggestAddSig ReportErrCtxt
ctxt Kind
ty1 Kind
ty2
  | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
inferred_bndrs
  = 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 = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (Kind -> [Name]
get_inf Kind
ty1 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Kind -> [Name]
get_inf Kind
ty2)
    get_inf :: Kind -> [Name]
get_inf Kind
ty | Just TcId
tv <- Kind -> Maybe TcId
tcGetTyVar_maybe Kind
ty
               , TcId -> Bool
isSkolemTyVar TcId
tv
               , ((InferSkol [(Name, Kind)]
prs, [TcId]
_) : [(SkolemInfo, [TcId])]
_) <- [Implication] -> [TcId] -> [(SkolemInfo, [TcId])]
getSkolemInfo (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt) [TcId
tv]
               = ((Name, Kind) -> Name) -> [(Name, Kind)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Kind) -> Name
forall a b. (a, b) -> a
fst [(Name, Kind)]
prs
               | Bool
otherwise
               = []

--------------------
misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report
-- Types are already tidy
-- If oriented then ty1 is actual, ty2 is expected
misMatchMsg :: ReportErrCtxt -> Ct -> Kind -> Kind -> Report
misMatchMsg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
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
$
    Kind -> Kind -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch Kind
ty1 Kind
ty2 CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
    [SDoc] -> SDoc
sep [ case CtOrigin
orig of
            TypeEqOrigin {} -> ReportErrCtxt -> Ct -> Kind -> Kind -> CtOrigin -> SDoc
tk_eq_msg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2 CtOrigin
orig
            KindEqOrigin {} -> ReportErrCtxt -> Ct -> Kind -> Kind -> CtOrigin -> SDoc
tk_eq_msg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2 CtOrigin
orig
            CtOrigin
_ -> Bool -> Ct -> Kind -> Kind -> SDoc
headline_eq_msg Bool
False Ct
ct Kind
ty1 Kind
ty2
        , Kind -> Kind -> SDoc
sameOccExtra Kind
ty2 Kind
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 -> Kind -> Kind -> SDoc
headline_eq_msg Bool
add_ea Ct
ct Kind
ty1 Kind
ty2

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

  | Kind -> Bool
isAtomicTy Kind
ty1 Bool -> Bool -> Bool
|| Kind -> Bool
isAtomicTy Kind
ty2
  = -- Print with quotes
    [SDoc] -> SDoc
sep [ String -> SDoc
text String
herald1 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
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 (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
ty2) ]

  | Bool
otherwise
  = -- Print with vertical layout
    [SDoc] -> SDoc
vcat [ String -> SDoc
text String
herald1 SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
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
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
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 -> Kind -> Kind -> CtOrigin -> SDoc
tk_eq_msg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2 orig :: CtOrigin
orig@(TypeEqOrigin { uo_actual :: CtOrigin -> Kind
uo_actual = Kind
act
                                             , uo_expected :: CtOrigin -> Kind
uo_expected = Kind
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

  | Kind -> Bool
isUnliftedTypeKind Kind
act, Kind -> Bool
isLiftedTypeKind Kind
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") ]

  | Kind -> Bool
isLiftedTypeKind Kind
act, Kind -> Bool
isUnliftedTypeKind Kind
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") ]

  | Kind -> Bool
tcIsLiftedTypeKind Kind
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 (Kind -> SDoc
pprWithTYPE Kind
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) $
    Kind -> Kind -> Kind -> Kind -> Bool
ea_looks_same Kind
ty1 Kind
ty2 Kind
exp Kind
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 -> Kind -> Kind -> SDoc
headline_eq_msg Bool
False Ct
ct Kind
ty1 Kind
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 (Kind -> Bool
isMetaTyVarTy Kind
exp) Bool -> Bool -> Bool
&& Bool -> Bool
not (Kind -> Bool
isMetaTyVarTy Kind
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 = Kind -> Int
count_args Kind
act
               n_exp :: Int
n_exp = Kind -> Int
count_args Kind
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 :: Kind -> Int
count_args Kind
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], Kind) -> [TyCoBinder]
forall a b. (a, b) -> a
fst (([TyCoBinder], Kind) -> [TyCoBinder])
-> ([TyCoBinder], Kind) -> [TyCoBinder]
forall a b. (a -> b) -> a -> b
$ Kind -> ([TyCoBinder], Kind)
splitPiTys Kind
ty

tk_eq_msg ReportErrCtxt
ctxt Ct
ct Kind
ty1 Kind
ty2
          (KindEqOrigin Kind
cty1 Maybe Kind
mb_cty2 CtOrigin
sub_o Maybe TypeOrKind
mb_sub_t_or_k)
  = [SDoc] -> SDoc
vcat [ Bool -> Ct -> Kind -> Kind -> SDoc
headline_eq_msg Bool
False Ct
ct Kind
ty1 Kind
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 ->
        case Maybe Kind
mb_cty2 of
          Just Kind
cty2
            |  Bool
printExplicitCoercions
            Bool -> Bool -> Bool
|| Bool -> Bool
not (Kind
cty1 Kind -> Kind -> Bool
`pickyEqType` Kind
cty2)
            -> [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 [ Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
cty1 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>
                                   Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Kind -> Kind
Kind -> Kind
tcTypeKind Kind
cty1)
                                 , Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
cty2 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>
                                   Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Kind -> Kind
Kind -> Kind
tcTypeKind Kind
cty2) ])
                    , ReportErrCtxt -> TypeOrKind -> Kind -> Kind -> CtOrigin -> SDoc
mk_supplementary_ea_msg ReportErrCtxt
ctxt TypeOrKind
sub_t_or_k Kind
cty1 Kind
cty2 CtOrigin
sub_o ]
          Maybe Kind
_ -> String -> SDoc
text String
"When matching the kind of" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
cty1)

tk_eq_msg ReportErrCtxt
_ Ct
_ Kind
_ Kind
_ 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 :: Kind -> Kind -> Kind -> Kind -> Bool
ea_looks_same Kind
ty1 Kind
ty2 Kind
exp Kind
act
  = (Kind
act Kind -> Kind -> Bool
`looks_same` Kind
ty1 Bool -> Bool -> Bool
&& Kind
exp Kind -> Kind -> Bool
`looks_same` Kind
ty2) Bool -> Bool -> Bool
||
    (Kind
exp Kind -> Kind -> Bool
`looks_same` Kind
ty1 Bool -> Bool -> Bool
&& Kind
act Kind -> Kind -> Bool
`looks_same` Kind
ty2)
  where
    looks_same :: Kind -> Kind -> Bool
looks_same Kind
t1 Kind
t2 = Kind
t1 Kind -> Kind -> Bool
`pickyEqType` Kind
t2
                    Bool -> Bool -> Bool
|| Kind
t1 Kind -> Kind -> Bool
`eqType` Kind
liftedTypeKind Bool -> Bool -> Bool
&& Kind
t2 Kind -> Kind -> Bool
`eqType` Kind
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 -> Kind -> Kind -> CtOrigin -> SDoc
mk_supplementary_ea_msg ReportErrCtxt
ctxt TypeOrKind
level Kind
ty1 Kind
ty2 CtOrigin
orig
  | TypeEqOrigin { uo_expected :: CtOrigin -> Kind
uo_expected = Kind
exp, uo_actual :: CtOrigin -> Kind
uo_actual = Kind
act } <- CtOrigin
orig
  , Bool -> Bool
not (Kind -> Kind -> Kind -> Kind -> Bool
ea_looks_same Kind
ty1 Kind
ty2 Kind
exp Kind
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 -> Kind
uo_actual = Kind
act, uo_expected :: CtOrigin -> Kind
uo_expected = Kind
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 (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
act))

  | Bool
otherwise
  = [SDoc] -> SDoc
vcat [ case Maybe Ct
at_top of
              Just Ct
ct -> Bool -> Ct -> Kind -> Kind -> SDoc
headline_eq_msg Bool
True Ct
ct Kind
exp Kind
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
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
exp
                                , String -> SDoc
text String
"  Actual:" SDoc -> SDoc -> SDoc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
act ]

    kind_desc :: SDoc
kind_desc | Kind -> Bool
tcIsConstraintKind Kind
exp = String -> SDoc
text String
"a constraint"
              | Just Kind
arg <- HasDebugCallStack => Kind -> Maybe Kind
Kind -> Maybe Kind
kindRep_maybe Kind
exp  -- TYPE t0
              , Kind -> Bool
tcIsTyVarTy Kind
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 (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
exp)
                                   Bool
False -> String -> SDoc
text String
"a type"
              | Bool
otherwise       = String -> SDoc
text String
"kind" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
exp)

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

    expandedTys :: SDoc
expandedTys = Bool -> SDoc -> SDoc
ppUnless (Kind
expTy1 Kind -> Kind -> Bool
`pickyEqType` Kind
exp Bool -> Bool -> Bool
&& Kind
expTy2 Kind -> Kind -> Bool
`pickyEqType` Kind
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
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
expTy1
                  , String -> SDoc
text String
"  Actual type:" SDoc -> SDoc -> SDoc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
expTy2 ]

    (Kind
expTy1, Kind
expTy2) = Kind -> Kind -> (Kind, Kind)
expandSynonymsToMatch Kind
exp Kind
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 :: Kind -> Kind -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch Kind
ty1 Kind
ty2 CtOrigin
ct
  = Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
show_kinds
  where
    (Kind
act_ty, Kind
exp_ty) = case CtOrigin
ct of
      TypeEqOrigin { uo_actual :: CtOrigin -> Kind
uo_actual = Kind
act
                   , uo_expected :: CtOrigin -> Kind
uo_expected = Kind
exp } -> (Kind
act, Kind
exp)
      CtOrigin
_                                  -> (Kind
ty1, Kind
ty2)
    show_kinds :: Bool
show_kinds = Kind -> Kind -> Bool
tcEqTypeVis Kind
act_ty Kind
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 (isInsolubleOccursCheck)
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