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

module TcErrors(
       reportUnsolved, reportAllUnsolved, warnAllUnsolved,
       warnDefaulting,

       solverDepthErrorTcS
  ) where

#include "HsVersions.h"

import GhcPrelude

import TcRnTypes
import TcRnMonad
import Constraint
import Predicate
import TcMType
import TcUnify( occCheckForErrors, MetaTyVarUpdateResult(..) )
import TcEnv( tcInitTidyEnv )
import TcType
import TcOrigin
import RnUnbound ( unknownNameSuggestions )
import Type
import TyCoRep
import TyCoPpr          ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon, pprWithTYPE )
import Unify            ( tcMatchTys )
import Module
import FamInst
import FamInstEnv       ( flattenTys )
import Inst
import InstEnv
import TyCon
import Class
import DataCon
import TcEvidence
import TcEvTerm
import GHC.Hs.Expr  ( UnboundVar(..) )
import GHC.Hs.Binds ( PatSynBind(..) )
import Name
import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
               , mkRdrUnqual, isLocalGRE, greSrcSpan )
import PrelNames ( typeableClassName )
import Id
import Var
import VarSet
import VarEnv
import NameSet
import Bag
import ErrUtils         ( ErrMsg, errDoc, pprLocErrMsg )
import BasicTypes
import ConLike          ( ConLike(..))
import Util
import FastString
import Outputable
import SrcLoc
import DynFlags
import ListSetOps       ( equivClasses )
import Maybes
import Pair
import qualified GHC.LanguageExtensions as LangExt
import FV ( fvVarList, unionFV )

import Control.Monad    ( when )
import Data.Foldable    ( toList )
import Data.List        ( partition, mapAccumL, nub, sortBy, unfoldr )
import qualified Data.Set as Set

import {-# SOURCE #-} TcHoleErrors ( 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 TcUnify, 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 TcErrors. TcErrors.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 TcSimplify)
-- 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
-- TcSimplify
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
       ; TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
            -- 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 -> [TyCoVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env0 [TyCoVar]
free_tvs
             free_tvs :: [TyCoVar]
free_tvs = WantedConstraints -> [TyCoVar]
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
<+> [TyCoVar] -> SDoc
pprTyVars [TyCoVar]
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
       ; let err_ctxt :: ReportErrCtxt
err_ctxt = CEC :: [Implication]
-> TidyEnv
-> EvBindsVar
-> TypeErrorChoice
-> HoleChoice
-> HoleChoice
-> HoleChoice
-> 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 insolule errors anywhere;
                                 -- See #15539 and c.f. setting ic_status
                                 -- in TcSimplify.setImplicationStatus
                            , cec_warn_redundant :: Bool
cec_warn_redundant = Bool
warn_redundant
                            , 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.
relevant_bindings :: SDoc -> Report
relevant_bindings :: SDoc -> Report
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_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_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_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 -> [TyCoVar]
ic_skols = [TyCoVar]
tvs, ic_telescope :: Implication -> Maybe SDoc
ic_telescope = Maybe SDoc
m_telescope
                                 , ic_given :: Implication -> [TyCoVar]
ic_given = [TyCoVar]
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')
       ; 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 -> [TyCoVar] -> TcM ()
warnRedundantConstraints ReportErrCtxt
ctxt' TcLclEnv
tcl_env SkolemInfo
info' [TyCoVar]
dead_givens
       ; 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 -> Maybe SDoc -> [TyCoVar] -> TcM ()
reportBadTelescope ReportErrCtxt
ctxt TcLclEnv
tcl_env Maybe SDoc
m_telescope [TyCoVar]
tvs }
  where
    tcl_env :: TcLclEnv
tcl_env      = Implication -> TcLclEnv
ic_env Implication
implic
    insoluble :: Bool
insoluble    = ImplicStatus -> Bool
isInsolubleStatus ImplicStatus
status
    (TidyEnv
env1, [TyCoVar]
tvs') = (TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar))
-> TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt) [TyCoVar]
tvs
    info' :: SkolemInfo
info'        = TidyEnv -> SkolemInfo -> SkolemInfo
tidySkolemInfo TidyEnv
env1 SkolemInfo
info
    implic' :: Implication
implic' = Implication
implic { ic_skols :: [TyCoVar]
ic_skols = [TyCoVar]
tvs'
                     , ic_given :: [TyCoVar]
ic_given = (TyCoVar -> TyCoVar) -> [TyCoVar] -> [TyCoVar]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> TyCoVar -> TyCoVar
tidyEvVar TidyEnv
env1) [TyCoVar]
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 :: [TyCoVar]
dead_givens = case ImplicStatus
status of
                    IC_Solved { ics_dead :: ImplicStatus -> [TyCoVar]
ics_dead = [TyCoVar]
dead } -> [TyCoVar]
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 TcSimplify
warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TyCoVar] -> TcM ()
warnRedundantConstraints ReportErrCtxt
ctxt TcLclEnv
env SkolemInfo
info [TyCoVar]
ev_vars
 | [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
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
<> [TyCoVar] -> SDoc
forall a. [a] -> SDoc
plural [TyCoVar]
redundant_evs SDoc -> SDoc -> SDoc
<> SDoc
colon
         SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
pprEvVarTheta [TyCoVar]
redundant_evs

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

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

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

reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TcTyVar] -> TcM ()
reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TyCoVar] -> TcM ()
reportBadTelescope ReportErrCtxt
ctxt TcLclEnv
env (Just SDoc
telescope) [TyCoVar]
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 ([TyCoVar] -> SDoc
pprTyVars [TyCoVar]
sorted_tvs)

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

reportBadTelescope ReportErrCtxt
_ TcLclEnv
_ Maybe SDoc
Nothing [TyCoVar]
skols
  = String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"reportBadTelescope" ([TyCoVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCoVar]
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 })
  = 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 -> TcM ()
traceTc String
"rw2" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
tidy_cts)

         -- First 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
       ; let ctxt_for_insols :: ReportErrCtxt
ctxt_for_insols = ReportErrCtxt
ctxt { cec_suppress :: Bool
cec_suppress = Bool
False }
       ; (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 ctxt1: 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)

    -- report1: ones that should *not* be suppresed by
    --          an insoluble somewhere else in the tree
    -- It's crucial that anything that is considered insoluble
    -- (see TcRnTypes.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
"Out of scope", Ct -> Pred -> Bool
forall p. Ct -> p -> Bool
is_out_of_scope,    Bool
True,  [Ct] -> Reporter
mkHoleReporter [Ct]
tidy_cts)
              , (String
"Holes",        Ct -> Pred -> Bool
is_hole,            Bool
False, [Ct] -> Reporter
mkHoleReporter [Ct]
tidy_cts)
              , (String
"custom_error", 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
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
forall p. p -> Pred -> Bool
very_wrong,     Bool
True, Reporter
mkSkolReporter)
              , (String
"skolem eq2",   Ct -> Pred -> Bool
forall p. p -> Pred -> Bool
skolem_eq,      Bool
True, Reporter
mkSkolReporter)
              , (String
"non-tv eq",    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 TcCanonical
              , (String
"Homo eqs",      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
is_equality,      Bool
False, (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
mkGroupReporter ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkEqErr) ]

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

    -- rigid_nom_eq, rigid_nom_tv_eq,
    is_hole, 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 Type
ty1 Type
ty2) = Type -> Bool
isRigidTy Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isRigidTy Type
ty2
    utterly_wrong p
_ Pred
_                      = Bool
False

    -- Things like (a ~N Int)
    very_wrong :: p -> Pred -> Bool
very_wrong p
_ (EqPred EqRel
NomEq Type
ty1 Type
ty2) = TcLevel -> Type -> Bool
isSkolemTy TcLevel
tc_lvl Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isRigidTy Type
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 Type
ty1 Type
_) = TcLevel -> Type -> Bool
isSkolemTy TcLevel
tc_lvl Type
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 Type
ty1 Type
_) = Bool -> Bool
not (Type -> Bool
isTyVarTy Type
ty1)
    non_tv_eq p
_ Pred
_                    = Bool
False

    is_out_of_scope :: Ct -> p -> Bool
is_out_of_scope Ct
ct p
_ = Ct -> Bool
isOutOfScopeCt Ct
ct
    is_hole :: Ct -> Pred -> Bool
is_hole         Ct
ct Pred
_ = Ct -> Bool
isHoleCt Ct
ct

    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
_ Type
ty1 Type
ty2) = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
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 [Type]
_) = 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 TcInstDcls.
      = Bool
True
      | Bool
otherwise
      = [Implication] -> Bool
has_gadt_match [Implication]
implics

---------------
isSkolemTy :: TcLevel -> Type -> Bool
-- The type is a skolem tyvar
isSkolemTy :: TcLevel -> Type -> Bool
isSkolemTy TcLevel
tc_lvl Type
ty
  | Just TyCoVar
tv <- Type -> Maybe TyCoVar
getTyVar_maybe Type
ty
  =  TyCoVar -> Bool
isSkolemTyVar TyCoVar
tv
  Bool -> Bool -> Bool
|| (TyCoVar -> Bool
isTyVarTyVar TyCoVar
tv Bool -> Bool -> Bool
&& TcLevel -> TyCoVar -> Bool
isTouchableMetaTyVar TcLevel
tc_lvl TyCoVar
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 :: Type -> Maybe TyCon
isTyFun_maybe Type
ty = case HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty of
                      Just (TyCon
tc,[Type]
_) | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tc
                      Maybe (TyCon, [Type])
_ -> 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

mkHoleReporter :: [Ct] -> Reporter
-- Reports errors one at a time
mkHoleReporter :: [Ct] -> Reporter
mkHoleReporter [Ct]
tidy_simples 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 <- [Ct] -> ReportErrCtxt -> Ct -> TcM ErrMsg
mkHoleError [Ct]
tidy_simples ReportErrCtxt
ctxt Ct
ct
                      ; ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
maybeReportHoleError ReportErrCtxt
ctxt Ct
ct ErrMsg
err
                      ; ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
maybeAddDeferredHoleBinding ReportErrCtxt
ctxt ErrMsg
err Ct
ct }

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
$ Type -> SDoc
pprUserTypeErrorTy
                        (Type -> SDoc) -> Type -> SDoc
forall a b. (a -> b) -> a -> b
$ case Ct -> Maybe Type
getUserTypeErrorMsg Ct
ct of
                            Just Type
msg -> Type
msg
                            Maybe Type
Nothing  -> String -> SDoc -> Type
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
relevant_bindings SDoc
binds_msg

       ; ErrMsg
err <- DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> Type
-> Type
-> TcM ErrMsg
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct'
                             Maybe SwapFlag
forall a. Maybe a
Nothing Type
ty1 Type
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
    (Type
ty1, Type
ty2) = Type -> (Type, Type)
getEqPredTys (Ct -> Type
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)

eq_lhs_type :: Ct -> Ct -> Bool
eq_lhs_type :: Ct -> Ct -> Bool
eq_lhs_type Ct
ct1 Ct
ct2
  = case (Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct1), Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct2)) of
       (EqPred EqRel
eq_rel1 Type
ty1 Type
_, EqPred EqRel
eq_rel2 Type
ty2 Type
_) ->
         (EqRel
eq_rel1 EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
eq_rel2) Bool -> Bool -> Bool
&& (Type
ty1 Type -> Type -> Bool
`eqType` Type
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) -> ReportErrCtxt
            -> [Ct] -> TcM ()
reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
reportGroup ReportErrCtxt -> [Ct] -> TcM ErrMsg
mk_err ReportErrCtxt
ctxt [Ct]
cts =
  case (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Ct -> Bool
isMonadFailInstanceMissing [Ct]
cts of
        -- Only warn about missing MonadFail constraint when
        -- there are no other missing constraints!
        ([Ct]
monadFailCts, []) ->
            do { ErrMsg
err <- ReportErrCtxt -> [Ct] -> TcM ErrMsg
mk_err ReportErrCtxt
ctxt [Ct]
monadFailCts
               ; WarnReason -> ErrMsg -> TcM ()
reportWarning (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnMissingMonadFailInstances) ErrMsg
err }

        ([Ct]
_, [Ct]
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)
  where
    isMonadFailInstanceMissing :: Ct -> Bool
isMonadFailInstanceMissing Ct
ct =
        case CtLoc -> CtOrigin
ctLocOrigin (Ct -> CtLoc
ctLoc Ct
ct) of
            FailablePattern LPat GhcTcId
_pat -> Bool
True
            CtOrigin
_otherwise           -> Bool
False

maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
-- Unlike maybeReportError, these "hole" errors are
-- /not/ suppressed by cec_suppress.  We want to see them!
maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
maybeReportHoleError ReportErrCtxt
ctxt Ct
ct 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.
  | Ct -> Bool
isTypeHoleCt Ct
ct
  = -- 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 ()

  -- 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
  | Ct -> Bool
isOutOfScopeCt Ct
ct
  = -- 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 ()

  -- Otherwise this is a typed hole in an expression,
  -- but not for an out-of-scope variable
  | Bool
otherwise
  = -- If deferring, report a warning only if -Wtyped-holes is on
    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 -> Type
ctev_pred = Type
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_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)"
             err_tm :: EvTerm
err_tm  = Type -> FastString -> EvTerm
evDelayedError Type
pred FastString
err_fs
             ev_binds_var :: EvBindsVar
ev_binds_var = ReportErrCtxt -> EvBindsVar
cec_binds ReportErrCtxt
ctxt

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

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

maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
maybeAddDeferredHoleBinding ReportErrCtxt
ctxt ErrMsg
err Ct
ct
  | Ct -> Bool
isExprHoleCt Ct
ct
  = ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
addDeferredBinding ReportErrCtxt
ctxt ErrMsg
err Ct
ct  -- Only add bindings for holes in expressions
  | Bool
otherwise                       -- not for holes in partial type signatures
  = () -> 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 (Type -> Pred
classifyPredType (Ct -> Type
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)
                     ([Type] -> SDoc
pprTheta [Ct -> Type
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 (Type -> SDoc
pprType (Ct -> Type
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 -> SrcSpan
RealSrcSpan (TcLclEnv -> RealSrcSpan
tcl_loc TcLclEnv
tcl_env))
            ([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 ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyCoVar] -> Bool)
-> (Implication -> [TyCoVar]) -> Implication -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Implication -> [TyCoVar]
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 :: SDoc
msg  = [Implication] -> ([Type], CtOrigin) -> SDoc
couldNotDeduce (ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt) ((Ct -> Type) -> [Ct] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> Type
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
$
            SDoc -> Report
important SDoc
msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend` SDoc -> Report
relevant_bindings SDoc
binds_msg }
  where
    (Ct
ct1:[Ct]
_) = [Ct]
cts

----------------
mkHoleError :: [Ct] -> ReportErrCtxt -> Ct -> TcM ErrMsg
mkHoleError :: [Ct] -> ReportErrCtxt -> Ct -> TcM ErrMsg
mkHoleError [Ct]
_ ReportErrCtxt
_ ct :: Ct
ct@(CHoleCan { cc_hole :: Ct -> Hole
cc_hole = ExprHole (OutOfScope OccName
occ GlobalRdrEnv
rdr_env0) })
  -- Out-of-scope variables, like 'a', where 'a' isn't bound; suggest possible
  -- in-scope variables in the message, and note inaccessible exact matches
  = do { DynFlags
dflags   <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; 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
       ; let suggs_msg :: SDoc
suggs_msg = DynFlags
-> HomePackageTable
-> Module
-> GlobalRdrEnv
-> LocalRdrEnv
-> ImportAvails
-> RdrName
-> SDoc
unknownNameSuggestions DynFlags
dflags HomePackageTable
hpt Module
curr_mod GlobalRdrEnv
rdr_env0
                                                (TcLclEnv -> LocalRdrEnv
tcl_rdr TcLclEnv
lcl_env) ImportAvails
imp_info RdrName
rdr
       ; GlobalRdrEnv
rdr_env     <- TcRn GlobalRdrEnv
getGlobalRdrEnv
       ; Set RealSrcSpan
splice_locs <- TcM (Set RealSrcSpan)
getTopLevelSpliceLocs
       ; let match_msgs :: [SDoc]
match_msgs = GlobalRdrEnv -> Set RealSrcSpan -> [SDoc]
mk_match_msgs GlobalRdrEnv
rdr_env Set RealSrcSpan
splice_locs
       ; SrcSpan -> ErrDoc -> TcM ErrMsg
mkErrDocAt (RealSrcSpan -> SrcSpan
RealSrcSpan RealSrcSpan
err_loc) (ErrDoc -> TcM ErrMsg) -> ErrDoc -> TcM ErrMsg
forall a b. (a -> b) -> a -> b
$
                    [SDoc] -> [SDoc] -> [SDoc] -> ErrDoc
errDoc [SDoc
out_of_scope_msg] [] ([SDoc]
match_msgs [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc
suggs_msg]) }

  where
    rdr :: RdrName
rdr         = OccName -> RdrName
mkRdrUnqual OccName
occ
    ct_loc :: CtLoc
ct_loc      = Ct -> CtLoc
ctLoc Ct
ct
    lcl_env :: TcLclEnv
lcl_env     = CtLoc -> TcLclEnv
ctLocEnv CtLoc
ct_loc
    err_loc :: RealSrcSpan
err_loc     = TcLclEnv -> RealSrcSpan
tcl_loc TcLclEnv
lcl_env
    hole_ty :: Type
hole_ty     = CtEvidence -> Type
ctEvPred (Ct -> CtEvidence
ctEvidence Ct
ct)
    boring_type :: Bool
boring_type = Type -> Bool
isTyVarTy Type
hole_ty

    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 -> Type -> SDoc
pp_with_type OccName
occ Type
hole_ty)

    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:"

    -- Indicate if the out-of-scope variable exactly (and unambiguously) matches
    -- a top-level binding in a later inter-splice group; see Note [OutOfScope
    -- exact matches]
    mk_match_msgs :: GlobalRdrEnv -> Set RealSrcSpan -> [SDoc]
mk_match_msgs GlobalRdrEnv
rdr_env Set RealSrcSpan
splice_locs
      = let gres :: [GlobalRdrElt]
gres = (GlobalRdrElt -> Bool) -> [GlobalRdrElt] -> [GlobalRdrElt]
forall a. (a -> Bool) -> [a] -> [a]
filter GlobalRdrElt -> Bool
isLocalGRE (GlobalRdrEnv -> OccName -> [GlobalRdrElt]
lookupGlobalRdrEnv GlobalRdrEnv
rdr_env OccName
occ)
        in case [GlobalRdrElt]
gres of
             [GlobalRdrElt
gre]
               |  RealSrcSpan RealSrcSpan
bind_loc <- GlobalRdrElt -> SrcSpan
greSrcSpan GlobalRdrElt
gre
                  -- Find splice between the unbound variable and the match; use
                  -- lookupLE, not lookupLT, since match could be in the splice
               ,  Just RealSrcSpan
th_loc <- RealSrcSpan -> Set RealSrcSpan -> Maybe RealSrcSpan
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupLE RealSrcSpan
bind_loc Set RealSrcSpan
splice_locs
               ,  RealSrcSpan
err_loc RealSrcSpan -> RealSrcSpan -> Bool
forall a. Ord a => a -> a -> Bool
< RealSrcSpan
th_loc
               -> [RealSrcSpan -> RealSrcSpan -> SDoc
mk_bind_scope_msg RealSrcSpan
bind_loc RealSrcSpan
th_loc]
             [GlobalRdrElt]
_ -> []

    mk_bind_scope_msg :: RealSrcSpan -> RealSrcSpan -> SDoc
mk_bind_scope_msg RealSrcSpan
bind_loc RealSrcSpan
th_loc
      | Bool
is_th_bind
      = SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> SDoc
quotes (OccName -> SDoc
forall a. Outputable a => a -> SDoc
ppr OccName
occ) SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (String -> SDoc
text String
"splice on" SDoc -> SDoc -> SDoc
<+> SDoc
th_rng))
           Int
2 (String -> SDoc
text String
"is not in scope before line" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
th_start_ln)
      | Bool
otherwise
      = SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> SDoc
quotes (OccName -> SDoc
forall a. Outputable a => a -> SDoc
ppr OccName
occ) SDoc -> SDoc -> SDoc
<+> SDoc
bind_rng SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is not in scope")
           Int
2 (String -> SDoc
text String
"before the splice on" SDoc -> SDoc -> SDoc
<+> SDoc
th_rng)
      where
        bind_rng :: SDoc
bind_rng = SDoc -> SDoc
parens (String -> SDoc
text String
"line" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
bind_ln)
        th_rng :: SDoc
th_rng
          | Int
th_start_ln Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
th_end_ln = SDoc
single
          | Bool
otherwise                = SDoc
multi
        single :: SDoc
single = String -> SDoc
text String
"line"  SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
th_start_ln
        multi :: SDoc
multi  = String -> SDoc
text String
"lines" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
th_start_ln SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
"-" SDoc -> SDoc -> SDoc
<> Int -> SDoc
int Int
th_end_ln
        bind_ln :: Int
bind_ln     = RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
bind_loc
        th_start_ln :: Int
th_start_ln = RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
th_loc
        th_end_ln :: Int
th_end_ln   = RealSrcSpan -> Int
srcSpanEndLine   RealSrcSpan
th_loc
        is_th_bind :: Bool
is_th_bind = RealSrcSpan
th_loc RealSrcSpan -> RealSrcSpan -> Bool
`containsSpan` RealSrcSpan
bind_loc

mkHoleError [Ct]
tidy_simples ReportErrCtxt
ctxt ct :: Ct
ct@(CHoleCan { cc_hole :: Ct -> Hole
cc_hole = Hole
hole })
  -- Explicit holes, like "_" or "_f"
  = do { (ReportErrCtxt
ctxt, SDoc
binds_msg, Ct
ct) <- Bool -> ReportErrCtxt -> Ct -> TcM (ReportErrCtxt, SDoc, Ct)
relevantBindings Bool
False ReportErrCtxt
ctxt Ct
ct
               -- The 'False' means "don't filter the bindings"; see #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
               | Ct -> Bool
isExprHoleCt Ct
ct, 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] -> Ct -> TcM (ReportErrCtxt, SDoc)
validHoleFits ReportErrCtxt
ctxt [Ct]
tidy_simples Ct
ct
                            else (ReportErrCtxt, SDoc) -> TcM (ReportErrCtxt, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ReportErrCtxt
ctxt, SDoc
empty)
       ; 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
hole_msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend`
            SDoc -> Report
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
    occ :: OccName
occ       = Hole -> OccName
holeOcc Hole
hole
    hole_ty :: Type
hole_ty   = CtEvidence -> Type
ctEvPred (Ct -> CtEvidence
ctEvidence Ct
ct)
    hole_kind :: Type
hole_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
hole_ty
    tyvars :: [TyCoVar]
tyvars    = Type -> [TyCoVar]
tyCoVarsOfTypeList Type
hole_ty

    hole_msg :: SDoc
hole_msg = case Hole
hole of
      ExprHole {} -> [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Found hole:")
                               Int
2 (OccName -> Type -> SDoc
pp_with_type OccName
occ Type
hole_ty)
                          , SDoc
tyvars_msg, SDoc
expr_hole_hint ]
      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
      | Type -> Bool
isLiftedTypeKind Type
hole_kind
        Bool -> Bool -> Bool
|| Type -> Bool
isCoVarType Type
hole_ty -- Don't print the kind of unlifted
                               -- equalities (#15039)
      = Type -> SDoc
pprType Type
hole_ty
      | Bool
otherwise
      = Type -> SDoc
pprType Type
hole_ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
pprKind Type
hole_kind

    tyvars_msg :: SDoc
tyvars_msg = Bool -> SDoc -> SDoc
ppUnless ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
tyvars) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                 String -> SDoc
text String
"Where:" SDoc -> SDoc -> SDoc
<+> ([SDoc] -> SDoc
vcat ((TyCoVar -> SDoc) -> [TyCoVar] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVar -> SDoc
loc_msg [TyCoVar]
other_tvs)
                                    SDoc -> SDoc -> SDoc
$$ ReportErrCtxt -> [TyCoVar] -> SDoc
pprSkols ReportErrCtxt
ctxt [TyCoVar]
skol_tvs)
       where
         ([TyCoVar]
skol_tvs, [TyCoVar]
other_tvs) = (TyCoVar -> Bool) -> [TyCoVar] -> ([TyCoVar], [TyCoVar])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition TyCoVar -> Bool
is_skol [TyCoVar]
tyvars
         is_skol :: TyCoVar -> Bool
is_skol TyCoVar
tv = TyCoVar -> Bool
isTcTyVar TyCoVar
tv Bool -> Bool -> Bool
&& TyCoVar -> Bool
isSkolemTyVar TyCoVar
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 :: TyCoVar -> SDoc
loc_msg TyCoVar
tv
       | TyCoVar -> Bool
isTyVar TyCoVar
tv
       = case TyCoVar -> TcTyVarDetails
tcTyVarDetails TyCoVar
tv of
           MetaTv {} -> SDoc -> SDoc
quotes (TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
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
       = (DynFlags -> SDoc) -> SDoc
sdocWithDynFlags ((DynFlags -> SDoc) -> SDoc) -> (DynFlags -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \DynFlags
dflags ->
         if GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_PrintExplicitCoercions DynFlags
dflags
         then SDoc -> SDoc
quotes (TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
tv) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is a coercion variable"
         else SDoc
empty

mkHoleError [Ct]
_ ReportErrCtxt
_ Ct
ct = String -> SDoc -> TcM ErrMsg
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkHoleError" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

-- 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
                       -> Ct            -- The hole constraint.
                       -> TcM (ReportErrCtxt, SDoc) -- We return the new context
                                                    -- with a possibly updated
                                                    -- tidy environment, and
                                                    -- the message.
validHoleFits :: ReportErrCtxt -> [Ct] -> Ct -> 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 Ct
ct
  = do { (TidyEnv
tidy_env, SDoc
msg) <- TidyEnv -> [Implication] -> [Ct] -> Ct -> TcM (TidyEnv, SDoc)
findValidHoleFits TidyEnv
lcl_env [Implication]
implics [Ct]
simps Ct
ct
       ; (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 :: [(Type, RealSrcSpan)]
constraints =
          do { implic :: Implication
implic@Implic{ ic_given :: Implication -> [TyCoVar]
ic_given = [TyCoVar]
given } <- ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt
             ; TyCoVar
constraint <- [TyCoVar]
given
             ; (Type, RealSrcSpan) -> [(Type, RealSrcSpan)]
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCoVar -> Type
varType TyCoVar
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 ([(Type, RealSrcSpan)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, 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
$ ((Type, RealSrcSpan) -> SDoc) -> [(Type, RealSrcSpan)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Type, RealSrcSpan) -> SDoc
forall a a. (Outputable a, Outputable a) => (a, a) -> SDoc
pprConstraint [(Type, RealSrcSpan)]
constraints)

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

----------------
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 :: [Type]
preds   = (Ct -> Type) -> [Ct] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> Type
ctPred [Ct]
cts
             givens :: [Implication]
givens  = ReportErrCtxt -> [Implication]
getUserGivens ReportErrCtxt
ctxt
             msg :: SDoc
msg | [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
givens
                 = 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 ([Type] -> SDoc
pprParendTheta [Type]
preds) ]
                 | Bool
otherwise
                 = [Implication] -> ([Type], CtOrigin) -> SDoc
couldNotDeduce [Implication]
givens ([Type]
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
$
            SDoc -> Report
important SDoc
msg Report -> Report -> Report
forall a. Monoid a => a -> a -> a
`mappend` SDoc -> Report
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.


Note [OutOfScope exact matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When constructing an out-of-scope error message, we not only generate a list of
possible in-scope alternatives but also search for an exact, unambiguous match
in a later inter-splice group.  If we find such a match, we report its presence
(and indirectly, its scope) in the message.  For example, if a module A contains
the following declarations,

   foo :: Int
   foo = x

   $(return [])  -- Empty top-level splice

   x :: Int
   x = 23

we will issue an error similar to

   A.hs:6:7: error:
       • Variable not in scope: x :: Int
       • ‘x’ (line 11) is not in scope before the splice on line 8

By providing information about the match, we hope to clarify why declaring a
variable after a top-level splice but using it before the splice generates an
out-of-scope error (a situation which is often confusing to Haskell newcomers).

Note that if we find multiple exact matches to the out-of-scope variable
(hereafter referred to as x), we report nothing.  Such matches can only be
duplicate record fields, as the presence of any other duplicate top-level
declarations would have already halted compilation.  But if these record fields
are declared in a later inter-splice group, then so too are their corresponding
types.  Thus, these types must not occur in the inter-splice group containing x
(any unknown types would have already been reported), and so the matches to the
record fields are most likely coincidental.

One oddity of the exact match portion of the error message is that we specify
where the match to x is NOT in scope.  Why not simply state where the match IS
in scope?  It most cases, this would be just as easy and perhaps a little
clearer for the user.  But now consider the following example:

    {-# LANGUAGE TemplateHaskell #-}

    module A where

    import Language.Haskell.TH
    import Language.Haskell.TH.Syntax

    foo = x

    $(do -------------------------------------------------
        ds <- [d| ok1 = x
                |]
        addTopDecls ds
        return [])

    bar = $(do
            ds <- [d| x = 23
                      ok2 = x
                    |]
            addTopDecls ds
            litE $ stringL "hello")

    $(return []) -----------------------------------------

    ok3 = x

Here, x is out-of-scope in the declaration of foo, and so we report

    A.hs:8:7: error:
        • Variable not in scope: x
        • ‘x’ (line 16) is not in scope before the splice on lines 10-14

If we instead reported where x IS in scope, we would have to state that it is in
scope after the second top-level splice as well as among all the top-level
declarations added by both calls to addTopDecls.  But doing so would not only
add complexity to the code but also overwhelm the user with unneeded
information.

The logic which determines where x is not in scope is straightforward: it simply
finds the last top-level splice which occurs after x but before (or at) the
match to x (assuming such a splice exists).  In most cases, the check that the
splice occurs after x acts only as a sanity check.  For example, when the match
to x is a non-TH top-level declaration and a splice S occurs before the match,
then x must precede S; otherwise, it would be in scope.  But when dealing with
addTopDecls, this check serves a practical purpose.  Consider the following
declarations:

    $(do
        ds <- [d| ok = x
                  x = 23
                |]
        addTopDecls ds
        return [])

    foo = x

In this case, x is not in scope in the declaration for foo.  Since x occurs
AFTER the splice containing the match, the logic does not find any splices after
x but before or at its match, and so we report nothing about x's scope.  If we
had not checked whether x occurs before the splice, we would have instead
reported that x is not in scope before the splice.  While correct, such an error
message is more likely to confuse than to enlighten.
-}

{-
************************************************************************
*                                                                      *
                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
       ; Bool
exp_syns <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_PrintExpandedSynonyms
       ; let (Bool
keep_going, Maybe SwapFlag
is_oriented, SDoc
wanted_msg)
                           = CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
mk_wanted_extra (Ct -> CtLoc
ctLoc Ct
ct) Bool
exp_syns
             coercible_msg :: SDoc
coercible_msg = case Ct -> EqRel
ctEqRel Ct
ct of
               EqRel
NomEq  -> SDoc
empty
               EqRel
ReprEq -> GlobalRdrEnv -> FamInstEnvs -> Type -> Type -> SDoc
mkCoercibleExplanation GlobalRdrEnv
rdr_env FamInstEnvs
fam_envs Type
ty1 Type
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) SDoc -> SDoc -> SDoc
$$ Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
keep_going)
       ; let report :: Report
report = [Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [SDoc -> Report
important SDoc
wanted_msg, SDoc -> Report
important SDoc
coercible_msg,
                               SDoc -> Report
relevant_bindings SDoc
binds_msg]
       ; if Bool
keep_going
         then DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> Type
-> Type
-> TcM ErrMsg
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
is_oriented Type
ty1 Type
ty2
         else ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct Report
report }
  where
    (Type
ty1, Type
ty2) = Type -> (Type, Type)
getEqPredTys (Ct -> Type
ctPred Ct
ct)

       -- If the types in the error message are the same as the types
       -- we are unifying, don't add the extra expected/actual message
    mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
    mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
mk_wanted_extra CtLoc
loc Bool
expandSyns
      = case CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc of
          orig :: CtOrigin
orig@TypeEqOrigin {} -> Type
-> Type
-> CtOrigin
-> Maybe TypeOrKind
-> Bool
-> (Bool, Maybe SwapFlag, SDoc)
mkExpectedActualMsg Type
ty1 Type
ty2 CtOrigin
orig
                                                      Maybe TypeOrKind
t_or_k Bool
expandSyns
            where
              t_or_k :: Maybe TypeOrKind
t_or_k = CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe CtLoc
loc

          KindEqOrigin Type
cty1 Maybe Type
mb_cty2 CtOrigin
sub_o Maybe TypeOrKind
sub_t_or_k
            -> (Bool
True, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
msg1 SDoc -> SDoc -> SDoc
$$ SDoc
msg2)
            where
              sub_what :: SDoc
sub_what = case Maybe TypeOrKind
sub_t_or_k of Just TypeOrKind
KindLevel -> String -> SDoc
text String
"kinds"
                                            Maybe TypeOrKind
_              -> String -> SDoc
text String
"types"
              msg1 :: SDoc
msg1 = (DynFlags -> SDoc) -> SDoc
sdocWithDynFlags ((DynFlags -> SDoc) -> SDoc) -> (DynFlags -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \DynFlags
dflags ->
                     case Maybe Type
mb_cty2 of
                       Just Type
cty2
                         |  GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_PrintExplicitCoercions DynFlags
dflags
                         Bool -> Bool -> Bool
|| Bool -> Bool
not (Type
cty1 Type -> Type -> Bool
`pickyEqType` Type
cty2)
                         -> SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"When matching" SDoc -> SDoc -> SDoc
<+> SDoc
sub_what)
                               Int
2 ([SDoc] -> SDoc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
cty1 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>
                                         Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
cty1)
                                       , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
cty2 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>
                                         Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
cty2) ])
                       Maybe Type
_ -> String -> SDoc
text String
"When matching the kind of" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
cty1)
              msg2 :: SDoc
msg2 = case CtOrigin
sub_o of
                       TypeEqOrigin {}
                         | Just Type
cty2 <- Maybe Type
mb_cty2 ->
                         (Bool, Maybe SwapFlag, SDoc) -> SDoc
forall a b c. (a, b, c) -> c
thdOf3 (Type
-> Type
-> CtOrigin
-> Maybe TypeOrKind
-> Bool
-> (Bool, Maybe SwapFlag, SDoc)
mkExpectedActualMsg Type
cty1 Type
cty2 CtOrigin
sub_o Maybe TypeOrKind
sub_t_or_k
                                                     Bool
expandSyns)
                       CtOrigin
_ -> SDoc
empty
          CtOrigin
_ -> (Bool
True, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
empty)

-- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
-- is left over.
mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
                       -> TcType -> TcType -> SDoc
mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs -> Type -> Type -> SDoc
mkCoercibleExplanation GlobalRdrEnv
rdr_env FamInstEnvs
fam_envs Type
ty1 Type
ty2
  | Just (TyCon
tc, [Type]
tys) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty1
  , (TyCon
rep_tc, [Type]
_, Coercion
_) <- FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], Coercion)
tcLookupDataFamInst FamInstEnvs
fam_envs TyCon
tc [Type]
tys
  , Just SDoc
msg <- TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
rep_tc
  = SDoc
msg
  | Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2
  , (TyCon
rep_tc, [Type]
_, Coercion
_) <- FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], Coercion)
tcLookupDataFamInst FamInstEnvs
fam_envs TyCon
tc [Type]
tys
  , Just SDoc
msg <- TyCon -> Maybe SDoc
coercible_msg_for_tycon TyCon
rep_tc
  = SDoc
msg
  | Just (Type
s1, Type
_) <- Type -> Maybe (Type, Type)
tcSplitAppTy_maybe Type
ty1
  , Just (Type
s2, Type
_) <- Type -> Maybe (Type, Type)
tcSplitAppTy_maybe Type
ty2
  , Type
s1 Type -> Type -> Bool
`eqType` Type
s2
  , Type -> Bool
has_unknown_roles Type
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 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
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 :: Type -> Bool
has_unknown_roles Type
ty
      | Just (TyCon
tc, [Type]
tys) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty
      = [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` TyCon -> Int
tyConArity TyCon
tc  -- oversaturated tycon
      | Just (Type
s, Type
_) <- Type -> Maybe (Type, Type)
tcSplitAppTy_maybe Type
ty
      = Type -> Bool
has_unknown_roles Type
s
      | Type -> Bool
isTyVarTy Type
ty
      = Bool
True
      | Bool
otherwise
      = Bool
False

{-
-- | Make a listing of role signatures for all the parameterised tycons
-- used in the provided types


-- SLPJ Jun 15: I could not convince myself that these hints were really
-- useful.  Maybe they are, but I think we need more work to make them
-- actually helpful.
mkRoleSigs :: Type -> Type -> SDoc
mkRoleSigs ty1 ty2
  = ppUnless (null role_sigs) $
    hang (text "Relevant role signatures:")
       2 (vcat role_sigs)
  where
    tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
    role_sigs = mapMaybe ppr_role_sig tcs

    ppr_role_sig tc
      | null roles  -- if there are no parameters, don't bother printing
      = Nothing
      | isBuiltInSyntax (tyConName tc)  -- don't print roles for (->), etc.
      = Nothing
      | otherwise
      = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
      where
        roles = tyConRoles tc
-}

mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
             -> Ct
             -> Maybe SwapFlag   -- Nothing <=> not sure
             -> TcType -> TcType -> TcM ErrMsg
mkEqErr_help :: DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> Type
-> Type
-> TcM ErrMsg
mkEqErr_help DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
  | Just (TyCoVar
tv1, Coercion
co1) <- Type -> Maybe (TyCoVar, Coercion)
tcGetCastedTyVar_maybe Type
ty1
  = DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> TyCoVar
-> Coercion
-> Type
-> TcM ErrMsg
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented TyCoVar
tv1 Coercion
co1 Type
ty2
  | Just (TyCoVar
tv2, Coercion
co2) <- Type -> Maybe (TyCoVar, Coercion)
tcGetCastedTyVar_maybe Type
ty2
  = DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> TyCoVar
-> Coercion
-> Type
-> TcM ErrMsg
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
swapped  TyCoVar
tv2 Coercion
co2 Type
ty1
  | Bool
otherwise
  = ReportErrCtxt
-> Report -> Ct -> Maybe SwapFlag -> Type -> Type -> TcM ErrMsg
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
  where
    swapped :: Maybe SwapFlag
swapped = (SwapFlag -> SwapFlag) -> Maybe SwapFlag -> Maybe SwapFlag
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SwapFlag -> SwapFlag
flipSwap Maybe SwapFlag
oriented

reportEqErr :: ReportErrCtxt -> Report
            -> Ct
            -> Maybe SwapFlag   -- Nothing <=> not sure
            -> TcType -> TcType -> TcM ErrMsg
reportEqErr :: ReportErrCtxt
-> Report -> Ct -> Maybe SwapFlag -> Type -> Type -> TcM ErrMsg
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
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 = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchOrCND ReportErrCtxt
ctxt Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
        eqInfo :: Report
eqInfo = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ Ct -> Type -> Type -> SDoc
mkEqInfoMsg Ct
ct Type
ty1 Type
ty2

mkTyVarEqErr, mkTyVarEqErr'
  :: DynFlags -> ReportErrCtxt -> Report -> Ct
             -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
mkTyVarEqErr :: DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> TyCoVar
-> Coercion
-> Type
-> TcM ErrMsg
mkTyVarEqErr DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented TyCoVar
tv1 Coercion
co1 Type
ty2
  = do { String -> SDoc -> TcM ()
traceTc String
"mkTyVarEqErr" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
$$ TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
tv1 SDoc -> SDoc -> SDoc
$$ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co1 SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
       ; DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> TyCoVar
-> Coercion
-> Type
-> TcM ErrMsg
mkTyVarEqErr' DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented TyCoVar
tv1 Coercion
co1 Type
ty2 }

mkTyVarEqErr' :: DynFlags
-> ReportErrCtxt
-> Report
-> Ct
-> Maybe SwapFlag
-> TyCoVar
-> Coercion
-> Type
-> TcM ErrMsg
mkTyVarEqErr' DynFlags
dflags ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented TyCoVar
tv1 Coercion
co1 Type
ty2
  | Bool -> Bool
not Bool
insoluble_occurs_check   -- See Note [Occurs check wins]
  , ReportErrCtxt -> TyCoVar -> Bool
isUserSkolem ReportErrCtxt
ctxt TyCoVar
tv1   -- ty2 won't be a meta-tyvar, or else the thing would
                            -- be oriented the other way round;
                            -- see TcCanonical.canEqTyVarTyVar
    Bool -> Bool -> Bool
|| TyCoVar -> Bool
isTyVarTyVar TyCoVar
tv1 Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isTyVarTy Type
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
        [ SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchOrCND ReportErrCtxt
ctxt Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
        , SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> TyCoVar -> Type -> SDoc
extraTyVarEqInfo ReportErrCtxt
ctxt TyCoVar
tv1 Type
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 TcCanonical
  = do { let main_msg :: SDoc
main_msg = CtOrigin -> SDoc -> SDoc
addArising (Ct -> CtOrigin
ctOrigin Ct
ct) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                        SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Occurs check: cannot construct the infinite" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<> SDoc
colon)
                              Int
2 ([SDoc] -> SDoc
sep [Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1, Char -> SDoc
char Char
'~', Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2])

             extra2 :: Report
extra2 = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ Ct -> Type -> Type -> SDoc
mkEqInfoMsg Ct
ct Type
ty1 Type
ty2

             interesting_tyvars :: [TyCoVar]
interesting_tyvars = (TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TyCoVar -> Bool) -> TyCoVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
noFreeVarsOfType (Type -> Bool) -> (TyCoVar -> Type) -> TyCoVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Type
tyVarKind) ([TyCoVar] -> [TyCoVar]) -> [TyCoVar] -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$
                                  (TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TyCoVar -> Bool
isTyVar ([TyCoVar] -> [TyCoVar]) -> [TyCoVar] -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$
                                  FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$
                                  Type -> FV
tyCoFVsOfType Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
ty2
             extra3 :: Report
extra3 = SDoc -> Report
relevant_bindings (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$
                      Bool -> SDoc -> SDoc
ppWhen (Bool -> Bool
not ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
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 ((TyCoVar -> SDoc) -> [TyCoVar] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TyCoVar -> SDoc
tyvar_binding (TyCoVar -> SDoc) -> (TyCoVar -> TyCoVar) -> TyCoVar -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc (ReportErrCtxt -> TidyEnv
cec_tidy ReportErrCtxt
ctxt))
                                [TyCoVar]
interesting_tyvars)

             tyvar_binding :: TyCoVar -> SDoc
tyvar_binding TyCoVar
tv = TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
tv SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCoVar -> Type
tyVarKind TyCoVar
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 [SDoc -> Report
important SDoc
main_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 (TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
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 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
                        , Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"GHC doesn't yet support impredicative polymorphism") ]
       -- 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 { report_important :: [SDoc]
report_important = [SDoc
msg] } }

   -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds]
   -- in TcCanonical
  | Bool -> Bool
not (Type
k1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
k2)
  = do { let main_msg :: SDoc
main_msg = CtOrigin -> SDoc -> SDoc
addArising (Ct -> CtOrigin
ctOrigin Ct
ct) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                        [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Kind mismatch: cannot unify" SDoc -> SDoc -> SDoc
<+>
                                     SDoc -> SDoc
parens (TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
tv1 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCoVar -> Type
tyVarKind TyCoVar
tv1)) SDoc -> SDoc -> SDoc
<+>
                                     String -> SDoc
text String
"with:")
                                  Int
2 ([SDoc] -> SDoc
sep [Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2, SDoc
dcolon, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k2])
                             , String -> SDoc
text String
"Their kinds differ." ]
             cast_msg :: SDoc
cast_msg
               | Coercion -> Bool
isTcReflexiveCo Coercion
co1 = SDoc
empty
               | Bool
otherwise           = String -> SDoc
text String
"NB:" SDoc -> SDoc -> SDoc
<+> TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
tv1 SDoc -> SDoc -> SDoc
<+>
                                       String -> SDoc
text String
"was casted to have kind" SDoc -> SDoc -> SDoc
<+>
                                       SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k1)

       ; ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
mkErrorMsgFromCt ReportErrCtxt
ctxt Ct
ct ([Report] -> Report
forall a. Monoid a => [a] -> a
mconcat [SDoc -> Report
important SDoc
main_msg, SDoc -> Report
important SDoc
cast_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 -> [TyCoVar]
ic_skols = [TyCoVar]
skols } <- Implication
implic
  , TyCoVar
tv1 TyCoVar -> [TyCoVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCoVar]
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
        [ SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchMsg Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
        , SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> TyCoVar -> Type -> SDoc
extraTyVarEqInfo ReportErrCtxt
ctxt TyCoVar
tv1 Type
ty2
        , Report
report
        ]

  -- Check for skolem escape
  | (Implication
implic:[Implication]
_) <- ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt   -- Get the innermost context
  , Implic { ic_skols :: Implication -> [TyCoVar]
ic_skols = [TyCoVar]
skols, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info } <- Implication
implic
  , let esc_skols :: [TyCoVar]
esc_skols = (TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (TyCoVar -> VarSet -> Bool
`elemVarSet` (Type -> VarSet
tyCoVarsOfType Type
ty2)) [TyCoVar]
skols
  , Bool -> Bool
not ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
esc_skols)
  = do { let msg :: Report
msg = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchMsg Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
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
<> [TyCoVar] -> SDoc
forall a. [a] -> SDoc
plural [TyCoVar]
esc_skols
                             SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TyCoVar]
esc_skols
                           , String -> SDoc
text String
"would escape" SDoc -> SDoc -> SDoc
<+>
                             if [TyCoVar] -> Bool
forall a. [a] -> Bool
isSingleton [TyCoVar]
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 [TyCoVar] -> Bool
forall a. [a] -> Bool
isSingleton [TyCoVar]
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 -> [TyCoVar]
ic_given = [TyCoVar]
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 = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchMsg Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
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 (TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
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
<+> [TyCoVar] -> SDoc
pprEvVarTheta [TyCoVar]
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 = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> TyCoVar -> Type -> SDoc
extraTyVarEqInfo ReportErrCtxt
ctxt TyCoVar
tv1 Type
ty2
             add_sig :: Report
add_sig  = SDoc -> Report
important (SDoc -> Report) -> SDoc -> Report
forall a b. (a -> b) -> a -> b
$ ReportErrCtxt -> Type -> Type -> SDoc
suggestAddSig ReportErrCtxt
ctxt Type
ty1 Type
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 -> Maybe SwapFlag -> Type -> Type -> TcM ErrMsg
reportEqErr ReportErrCtxt
ctxt Report
report Ct
ct Maybe SwapFlag
oriented (TyCoVar -> Type
mkTyVarTy TyCoVar
tv1) Type
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
    Pair Type
_ Type
k1 = Coercion -> Pair Type
tcCoercionKind Coercion
co1
    k2 :: Type
k2        = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty2

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

    what :: SDoc
what = case CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe (Ct -> CtLoc
ctLoc Ct
ct) of
      Just TypeOrKind
KindLevel -> String -> SDoc
text String
"kind"
      Maybe TypeOrKind
_              -> String -> SDoc
text String
"type"

mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
-- 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 -> Type -> Type -> SDoc
mkEqInfoMsg Ct
ct Type
ty1 Type
ty2
  = SDoc
tyfun_msg SDoc -> SDoc -> SDoc
$$ SDoc
ambig_msg
  where
    mb_fun1 :: Maybe TyCon
mb_fun1 = Type -> Maybe TyCon
isTyFun_maybe Type
ty1
    mb_fun2 :: Maybe TyCon
mb_fun2 = Type -> Maybe TyCon
isTyFun_maybe Type
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 -> TyCoVar -> Bool
isUserSkolem ReportErrCtxt
ctxt TyCoVar
tv
  = TyCoVar -> Bool
isSkolemTyVar TyCoVar
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 -> [TyCoVar]
ic_skols = [TyCoVar]
sks, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info })
      = TyCoVar
tv TyCoVar -> [TyCoVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCoVar]
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 :: ReportErrCtxt -> Ct
              -> Maybe SwapFlag -> TcType -> TcType -> SDoc
-- If oriented then ty1 is actual, ty2 is expected
misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchOrCND ReportErrCtxt
ctxt Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
  | [Implication] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Implication]
givens Bool -> Bool -> Bool
||
    (Type -> Bool
isRigidTy Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isRigidTy Type
ty2) Bool -> Bool -> Bool
||
    Ct -> Bool
isGivenCt Ct
ct
       -- If the equality is unconditionally insoluble
       -- or there is no context, don't report the context
  = Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchMsg Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
  | Bool
otherwise
  = [Implication] -> ([Type], CtOrigin) -> SDoc
couldNotDeduce [Implication]
givens ([Type
eq_pred], CtOrigin
orig)
  where
    ev :: CtEvidence
ev      = Ct -> CtEvidence
ctEvidence Ct
ct
    eq_pred :: Type
eq_pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
    orig :: CtOrigin
orig    = CtEvidence -> CtOrigin
ctEvOrigin CtEvidence
ev
    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) -> SDoc
couldNotDeduce :: [Implication] -> ([Type], CtOrigin) -> SDoc
couldNotDeduce [Implication]
givens ([Type]
wanteds, CtOrigin
orig)
  = [SDoc] -> SDoc
vcat [ CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (String -> SDoc
text String
"Could not deduce:" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
pprTheta [Type]
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 -> [TyCoVar]
ic_given = [TyCoVar]
gs, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
skol_info })
           = SDoc -> Int -> SDoc -> SDoc
hang (SDoc
herald SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
pprEvVarTheta ((TyCoVar -> Type) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Type) -> [a] -> [a]
mkMinimalBySCs TyCoVar -> Type
evVarPred [TyCoVar]
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)) ])

{-
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 TcPatSyn).
-}

extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
-- Add on extra info about skolem constants
-- NB: The types themselves are already tidied
extraTyVarEqInfo :: ReportErrCtxt -> TyCoVar -> Type -> SDoc
extraTyVarEqInfo ReportErrCtxt
ctxt TyCoVar
tv1 Type
ty2
  = ReportErrCtxt -> TyCoVar -> SDoc
extraTyVarInfo ReportErrCtxt
ctxt TyCoVar
tv1 SDoc -> SDoc -> SDoc
$$ Type -> SDoc
ty_extra Type
ty2
  where
    ty_extra :: Type -> SDoc
ty_extra Type
ty = case Type -> Maybe TyCoVar
tcGetTyVar_maybe Type
ty of
                    Just TyCoVar
tv -> ReportErrCtxt -> TyCoVar -> SDoc
extraTyVarInfo ReportErrCtxt
ctxt TyCoVar
tv
                    Maybe TyCoVar
Nothing -> SDoc
empty

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

suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
-- See Note [Suggest adding a type signature]
suggestAddSig :: ReportErrCtxt -> Type -> Type -> SDoc
suggestAddSig ReportErrCtxt
ctxt Type
ty1 Type
ty2
  | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
inferred_bndrs
  = SDoc
empty
  | [Name
bndr] <- [Name]
inferred_bndrs
  = 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
  = 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 (Type -> [Name]
get_inf Type
ty1 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Type -> [Name]
get_inf Type
ty2)
    get_inf :: Type -> [Name]
get_inf Type
ty | Just TyCoVar
tv <- Type -> Maybe TyCoVar
tcGetTyVar_maybe Type
ty
               , TyCoVar -> Bool
isSkolemTyVar TyCoVar
tv
               , (Implication
implic, [TyCoVar]
_) : [(Implication, [TyCoVar])]
_ <- [Implication] -> [TyCoVar] -> [(Implication, [TyCoVar])]
getSkolemInfo (ReportErrCtxt -> [Implication]
cec_encl ReportErrCtxt
ctxt) [TyCoVar
tv]
               , InferSkol [(Name, Type)]
prs <- Implication -> SkolemInfo
ic_info Implication
implic
               = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
prs
               | Bool
otherwise
               = []

--------------------
misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
-- Types are already tidy
-- If oriented then ty1 is actual, ty2 is expected
misMatchMsg :: Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchMsg Ct
ct Maybe SwapFlag
oriented Type
ty1 Type
ty2
  | Just SwapFlag
NotSwapped <- Maybe SwapFlag
oriented
  = Ct -> Maybe SwapFlag -> Type -> Type -> SDoc
misMatchMsg Ct
ct (SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
IsSwapped) Type
ty2 Type
ty1

  -- These next two cases are when we're about to report, e.g., that
  -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
  -- lifted vs. unlifted
  | Type -> Bool
isLiftedRuntimeRep Type
ty1
  = SDoc
lifted_vs_unlifted

  | Type -> Bool
isLiftedRuntimeRep Type
ty2
  = SDoc
lifted_vs_unlifted

  | Bool
otherwise  -- So now we have Nothing or (Just IsSwapped)
               -- For some reason we treat Nothing like IsSwapped
  = CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch Type
ty1 Type
ty2 (Ct -> CtOrigin
ctOrigin Ct
ct) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
    [SDoc] -> SDoc
sep [ String -> SDoc
text String
herald1 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
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 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
        , Type -> Type -> SDoc
sameOccExtra Type
ty2 Type
ty1 ]
  where
    herald1 :: String
herald1 = [String] -> String
conc [ String
"Couldn't match"
                   , if Bool
is_repr     then String
"representation of" else String
""
                   , if Bool
is_oriented 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
is_oriented 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 }
    is_oriented :: Bool
is_oriented = Maybe SwapFlag -> Bool
forall a. Maybe a -> Bool
isJust Maybe SwapFlag
oriented

    orig :: CtOrigin
orig = Ct -> CtOrigin
ctOrigin Ct
ct
    what :: String
what = case CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe (Ct -> CtLoc
ctLoc Ct
ct) of
      Just TypeOrKind
KindLevel -> String
"kind"
      Maybe TypeOrKind
_              -> String
"type"

    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)

    lifted_vs_unlifted :: SDoc
lifted_vs_unlifted
      = CtOrigin -> SDoc -> SDoc
addArising CtOrigin
orig (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Couldn't match a lifted type with an unlifted type"

-- | 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 :: Type -> Type -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch Type
ty1 Type
ty2 CtOrigin
ct
  = Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
show_kinds
  where
    (Type
act_ty, Type
exp_ty) = case CtOrigin
ct of
      TypeEqOrigin { uo_actual :: CtOrigin -> Type
uo_actual = Type
act
                   , uo_expected :: CtOrigin -> Type
uo_expected = Type
exp } -> (Type
act, Type
exp)
      CtOrigin
_                                  -> (Type
ty1, Type
ty2)
    show_kinds :: Bool
show_kinds = Type -> Type -> Bool
tcEqTypeVis Type
act_ty Type
exp_ty
                 -- True when the visible bit of the types look the same,
                 -- so we want to show the kinds in the displayed type

mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
                    -> (Bool, Maybe SwapFlag, SDoc)
-- NotSwapped means (actual, expected), IsSwapped is the reverse
-- First return val is whether or not to print a herald above this msg
mkExpectedActualMsg :: Type
-> Type
-> CtOrigin
-> Maybe TypeOrKind
-> Bool
-> (Bool, Maybe SwapFlag, SDoc)
mkExpectedActualMsg Type
ty1 Type
ty2 ct :: CtOrigin
ct@(TypeEqOrigin { uo_actual :: CtOrigin -> Type
uo_actual = Type
act
                                             , uo_expected :: CtOrigin -> Type
uo_expected = Type
exp
                                             , uo_thing :: CtOrigin -> Maybe SDoc
uo_thing = Maybe SDoc
maybe_thing })
                    Maybe TypeOrKind
m_level Bool
printExpanded
  | TypeOrKind
KindLevel <- TypeOrKind
level, Bool
occurs_check_error       = (Bool
True, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
empty)
  | Type -> Bool
isUnliftedTypeKind Type
act, Type -> Bool
isLiftedTypeKind Type
exp = (Bool
False, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
msg2)
  | Type -> Bool
isLiftedTypeKind Type
act, Type -> Bool
isUnliftedTypeKind Type
exp = (Bool
False, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
msg3)
  | Type -> Bool
tcIsLiftedTypeKind Type
exp                       = (Bool
False, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
msg4)
  | Just SDoc
msg <- Maybe SDoc
num_args_msg                     = (Bool
False, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
msg SDoc -> SDoc -> SDoc
$$ SDoc
msg1)
  | TypeOrKind
KindLevel <- TypeOrKind
level, Just SDoc
th <- Maybe SDoc
maybe_thing   = (Bool
False, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc -> SDoc
msg5 SDoc
th)
  | Type
act Type -> Type -> Bool
`pickyEqType` Type
ty1, Type
exp Type -> Type -> Bool
`pickyEqType` Type
ty2 = (Bool
True, SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
NotSwapped, SDoc
empty)
  | Type
exp Type -> Type -> Bool
`pickyEqType` Type
ty1, Type
act Type -> Type -> Bool
`pickyEqType` Type
ty2 = (Bool
True, SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
IsSwapped, SDoc
empty)
  | Bool
otherwise                                    = (Bool
True, Maybe SwapFlag
forall a. Maybe a
Nothing, SDoc
msg1)
  where
    level :: TypeOrKind
level = Maybe TypeOrKind
m_level Maybe TypeOrKind -> TypeOrKind -> TypeOrKind
forall a. Maybe a -> a -> a
`orElse` TypeOrKind
TypeLevel

    occurs_check_error :: Bool
occurs_check_error
      | Just TyCoVar
tv <- Type -> Maybe TyCoVar
tcGetTyVar_maybe Type
ty1
      , TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ty2
      = Bool
True
      | Just TyCoVar
tv <- Type -> Maybe TyCoVar
tcGetTyVar_maybe Type
ty2
      , TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ty1
      = Bool
True
      | Bool
otherwise
      = Bool
False

    sort :: SDoc
sort = case TypeOrKind
level of
      TypeOrKind
TypeLevel -> String -> SDoc
text String
"type"
      TypeOrKind
KindLevel -> String -> SDoc
text String
"kind"

    msg1 :: SDoc
msg1 = case TypeOrKind
level of
      TypeOrKind
KindLevel
        | Just SDoc
th <- Maybe SDoc
maybe_thing
        -> SDoc -> SDoc
msg5 SDoc
th

      TypeOrKind
_ | Bool -> Bool
not (Type
act Type -> Type -> Bool
`pickyEqType` Type
exp)
        -> Type -> Type -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch Type
ty1 Type
ty2 CtOrigin
ct (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
           [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Expected" SDoc -> SDoc -> SDoc
<+> SDoc
sort SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
exp
                , String -> SDoc
text String
"  Actual" SDoc -> SDoc -> SDoc
<+> SDoc
sort SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
act
                , if Bool
printExpanded then SDoc
expandedTys else SDoc
empty ]

        | Bool
otherwise
        -> SDoc
empty

    thing_msg :: Bool -> SDoc -> SDoc
thing_msg = case Maybe SDoc
maybe_thing of
                  Just SDoc
thing -> \Bool
_ SDoc
levity ->
                    SDoc -> SDoc
quotes SDoc
thing SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is" SDoc -> SDoc -> SDoc
<+> SDoc
levity
                  Maybe SDoc
Nothing    -> \Bool
vowel SDoc
levity ->
                    String -> SDoc
text String
"got a" SDoc -> SDoc -> SDoc
<>
                    (if Bool
vowel then Char -> SDoc
char Char
'n' else SDoc
empty) SDoc -> SDoc -> SDoc
<+>
                    SDoc
levity SDoc -> SDoc -> SDoc
<+>
                    String -> SDoc
text String
"type"
    msg2 :: SDoc
msg2 = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Expecting a lifted type, but"
               , Bool -> SDoc -> SDoc
thing_msg Bool
True (String -> SDoc
text String
"unlifted") ]
    msg3 :: SDoc
msg3 = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Expecting an unlifted type, but"
               , Bool -> SDoc -> SDoc
thing_msg Bool
False (String -> SDoc
text String
"lifted") ]
    msg4 :: SDoc
msg4 = SDoc
maybe_num_args_msg SDoc -> SDoc -> SDoc
$$
           [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Expected a type, but"
               , SDoc -> (SDoc -> SDoc) -> Maybe SDoc -> SDoc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> SDoc
text String
"found something with kind")
                       (\SDoc
thing -> SDoc -> SDoc
quotes SDoc
thing SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"has kind")
                       Maybe SDoc
maybe_thing
               , SDoc -> SDoc
quotes (Type -> SDoc
pprWithTYPE Type
act) ]

    msg5 :: SDoc -> SDoc
msg5 SDoc
th = Type -> Type -> CtOrigin -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch Type
ty1 Type
ty2 CtOrigin
ct (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
              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
th SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"has kind" SDoc -> SDoc -> SDoc
<+>
                    SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
act))
      where
        kind_desc :: SDoc
kind_desc | Type -> Bool
tcIsConstraintKind Type
exp = String -> SDoc
text String
"a constraint"

                    -- TYPE t0
                  | Just Type
arg <- HasDebugCallStack => Type -> Maybe Type
Type -> Maybe Type
kindRep_maybe Type
exp
                  , Type -> Bool
tcIsTyVarTy Type
arg = (DynFlags -> SDoc) -> SDoc
sdocWithDynFlags ((DynFlags -> SDoc) -> SDoc) -> (DynFlags -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \DynFlags
dflags ->
                                      if GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_PrintExplicitRuntimeReps DynFlags
dflags
                                      then String -> SDoc
text String
"kind" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
exp)
                                      else String -> SDoc
text String
"a type"

                  | Bool
otherwise       = String -> SDoc
text String
"kind" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
exp)

    num_args_msg :: Maybe SDoc
num_args_msg = case TypeOrKind
level of
      TypeOrKind
KindLevel
        | Bool -> Bool
not (Type -> Bool
isMetaTyVarTy Type
exp) Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isMetaTyVarTy Type
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 = Type -> Int
count_args Type
act
               n_exp :: Int
n_exp = Type -> Int
count_args Type
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
maybe_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 = case Maybe SDoc
num_args_msg of
      Maybe SDoc
Nothing -> SDoc
empty
      Just SDoc
m  -> SDoc
m

    count_args :: Type -> Int
count_args Type
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], Type) -> [TyCoBinder]
forall a b. (a, b) -> a
fst (([TyCoBinder], Type) -> [TyCoBinder])
-> ([TyCoBinder], Type) -> [TyCoBinder]
forall a b. (a -> b) -> a -> b
$ Type -> ([TyCoBinder], Type)
splitPiTys Type
ty

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

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

mkExpectedActualMsg Type
_ Type
_ CtOrigin
_ Maybe TypeOrKind
_ Bool
_ = String -> (Bool, Maybe SwapFlag, SDoc)
forall a. String -> a
panic String
"mkExpectedAcutalMsg"

{- Note [Insoluble occurs check wins]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 first.

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

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

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

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

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

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

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

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

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

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

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

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

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

    go (TyConApp TyCon
tc1 [Type]
tys1) (TyConApp TyCon
tc2 [Type]
tys2)
      | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 =
        -- Type constructors are same. They may be synonyms, but we don't
        -- expand further.
        let ([Type]
tys1', [Type]
tys2') =
              [(Type, Type)] -> ([Type], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Type -> Type -> (Type, Type))
-> [Type] -> [Type] -> [(Type, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Type
ty1 Type
ty2 -> Type -> Type -> (Type, Type)
go Type
ty1 Type
ty2) [Type]
tys1 [Type]
tys2)
         in (TyCon -> [Type] -> Type
TyConApp TyCon
tc1 [Type]
tys1', TyCon -> [Type] -> Type
TyConApp TyCon
tc2 [Type]
tys2')

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

    go ty1 :: Type
ty1@(FunTy AnonArgFlag
_ Type
t1_1 Type
t1_2) ty2 :: Type
ty2@(FunTy AnonArgFlag
_ Type
t2_1 Type
t2_2) =
      let (Type
t1_1', Type
t2_1') = Type -> Type -> (Type, Type)
go Type
t1_1 Type