diff options
Diffstat (limited to 'compiler/typecheck/TcRnTypes.hs')
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 2339 |
1 files changed, 36 insertions, 2303 deletions
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index a66143bf57..8895593698 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -26,6 +26,8 @@ module TcRnTypes( -- The environment types Env(..), TcGblEnv(..), TcLclEnv(..), + setLclEnvTcLevel, getLclEnvTcLevel, + setLclEnvLoc, getLclEnvLoc, IfGblEnv(..), IfLclEnv(..), tcVisibleOrphanMods, @@ -33,7 +35,7 @@ module TcRnTypes( FrontendResult(..), -- Renamer types - ErrCtxt, RecFieldEnv, + ErrCtxt, RecFieldEnv, pushErrCtxt, pushErrCtxtSameOrigin, ImportAvails(..), emptyImportAvails, plusImportAvails, WhereFrom(..), mkModDeps, modDepsElts, @@ -64,59 +66,9 @@ module TcRnTypes( TcIdSigInst(..), TcPatSynInfo(..), isPartialSig, hasCompleteSig, - -- QCInst - QCInst(..), isPendingScInst, - - -- Canonical constraints - Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts, - singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, - isEmptyCts, isCTyEqCan, isCFunEqCan, - isPendingScDict, superClassesMightHelp, getPendingWantedScs, - isCDictCan_Maybe, isCFunEqCan_maybe, - isCNonCanonical, isWantedCt, isDerivedCt, - isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt, - isUserTypeErrorCt, getUserTypeErrorMsg, - ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, - ctEvId, mkTcEqPredLikeEv, - mkNonCanonical, mkNonCanonicalCt, mkGivens, - mkIrredCt, mkInsolubleCt, - ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel, - ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId, - tyCoVarsOfCt, tyCoVarsOfCts, - tyCoVarsOfCtList, tyCoVarsOfCtsList, - - WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, - isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC, - addInsols, insolublesOnly, addSimples, addImplics, - tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, - tyCoVarsOfWCList, insolubleCt, insolubleEqCt, - isDroppableCt, insolubleImplic, - arisesFromGivens, - - Implication(..), newImplication, implicationPrototype, - implicLclEnv, implicDynFlags, - ImplicStatus(..), isInsolubleStatus, isSolvedStatus, - SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth, - bumpSubGoalDepth, subGoalDepthExceeded, - CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin, - ctLocTypeOrKind_maybe, - ctLocDepth, bumpCtLocDepth, isGivenLoc, - setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan, - CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin, - isVisibleOrigin, toInvisibleOrigin, - TypeOrKind(..), isTypeLevel, isKindLevel, - pprCtOrigin, pprCtLoc, - pushErrCtxt, pushErrCtxtSameOrigin, - - - SkolemInfo(..), pprSigSkolInfo, pprSkolInfo, - - CtEvidence(..), TcEvDest(..), - mkKindLoc, toKindLoc, mkGivenLoc, - isWanted, isGiven, isDerived, isGivenOrWDeriv, - ctEvRole, - - wrapType, wrapTypeWithImplication, + -- Misc other types + TcId, TcIdSet, + NameShape(..), removeBindingShadowing, -- Constraint solver plugins @@ -124,25 +76,9 @@ module TcRnTypes( TcPluginM, runTcPluginM, unsafeTcPluginTcM, getEvBindsTcPluginM, - CtFlavour(..), ShadowInfo(..), ctEvFlavour, - CtFlavourRole, ctEvFlavourRole, ctFlavourRole, - eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR, - eqCanDischargeFR, - funEqCanDischarge, funEqCanDischargeF, - - -- Pretty printing - pprEvVarTheta, - pprEvVars, pprEvVarWithType, - - -- Misc other types - TcId, TcIdSet, - Hole(..), holeOcc, - NameShape(..), - -- Role annotations RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv, - lookupRoleAnnot, getRoleAnnots, - + lookupRoleAnnot, getRoleAnnots ) where #include "HsVersions.h" @@ -150,20 +86,16 @@ module TcRnTypes( import GhcPrelude import GHC.Hs -import CoreSyn import HscTypes import TcEvidence import Type -import Class ( Class ) -import TyCon ( TyCon, TyConFlavour, tyConKind ) -import TyCoRep ( coHoleCoVar ) -import Coercion ( Coercion, mkHoleCo ) -import ConLike ( ConLike(..) ) -import DataCon ( DataCon, dataConUserType, dataConOrigArgTys ) -import PatSyn ( PatSyn, pprPatSynType ) +import TyCon ( TyCon, tyConKind ) +import PatSyn ( PatSyn ) import Id ( idType, idName ) import FieldLabel ( FieldLabel ) import TcType +import Constraint +import TcOrigin import Annotations import InstEnv import FamInstEnv @@ -175,7 +107,6 @@ import NameEnv import NameSet import Avail import Var -import FV import VarEnv import Module import SrcLoc @@ -188,14 +119,12 @@ import Bag import DynFlags import Outputable import ListSetOps -import FastString -import qualified GHC.LanguageExtensions as LangExt import Fingerprint import Util import PrelNames ( isUnboundName ) import CostCentreState -import Control.Monad (ap, msum) +import Control.Monad (ap) import qualified Control.Monad.Fail as MonadFail import Data.Set ( Set ) import qualified Data.Set as S @@ -834,6 +763,18 @@ data TcLclEnv -- Changes as we move inside an expression tcl_errs :: TcRef Messages -- Place to accumulate errors } +setLclEnvTcLevel :: TcLclEnv -> TcLevel -> TcLclEnv +setLclEnvTcLevel env lvl = env { tcl_tclvl = lvl } + +getLclEnvTcLevel :: TcLclEnv -> TcLevel +getLclEnvTcLevel = tcl_tclvl + +setLclEnvLoc :: TcLclEnv -> RealSrcSpan -> TcLclEnv +setLclEnvLoc env loc = env { tcl_loc = loc } + +getLclEnvLoc :: TcLclEnv -> RealSrcSpan +getLclEnvLoc = tcl_loc + type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc)) -- Monadic so that we have a chance -- to deal with bound type variables just before error @@ -842,6 +783,18 @@ type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc)) -- Bool: True <=> this is a landmark context; do not -- discard it when trimming for display +-- These are here to avoid module loops: one might expect them +-- in Constraint, but they refer to ErrCtxt which refers to TcM. +-- Easier to just keep these definitions here, alongside TcM. +pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc +pushErrCtxt o err loc@(CtLoc { ctl_env = lcl }) + = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } } + +pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc +-- Just add information w/o updating the origin! +pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl }) + = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } } + type TcTypeEnv = NameEnv TcTyThing type ThBindEnv = NameEnv (TopLevelFlag, ThLevel) @@ -1655,2226 +1608,6 @@ hasCompleteSig sig_fn name {- -************************************************************************ -* * -* Canonical constraints * -* * -* These are the constraints the low-level simplifier works with * -* * -************************************************************************ --} - --- The syntax of xi (ξ) types: --- xi ::= a | T xis | xis -> xis | ... | forall a. tau --- Two important notes: --- (i) No type families, unless we are under a ForAll --- (ii) Note that xi types can contain unexpanded type synonyms; --- however, the (transitive) expansions of those type synonyms --- will not contain any type functions, unless we are under a ForAll. --- We enforce the structure of Xi types when we flatten (TcCanonical) - -type Xi = Type -- In many comments, "xi" ranges over Xi - -type Cts = Bag Ct - -data Ct - -- Atomic canonical constraints - = CDictCan { -- e.g. Num xi - cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] - - cc_class :: Class, - cc_tyargs :: [Xi], -- cc_tyargs are function-free, hence Xi - - cc_pend_sc :: Bool -- See Note [The superclass story] in TcCanonical - -- True <=> (a) cc_class has superclasses - -- (b) we have not (yet) added those - -- superclasses as Givens - } - - | CIrredCan { -- These stand for yet-unusable predicates - cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] - cc_insol :: Bool -- True <=> definitely an error, can never be solved - -- False <=> might be soluble - - -- For the might-be-soluble case, the ctev_pred of the evidence is - -- of form (tv xi1 xi2 ... xin) with a tyvar at the head - -- or (tv1 ~ ty2) where the CTyEqCan kind invariant fails - -- or (F tys ~ ty) where the CFunEqCan kind invariant fails - -- See Note [CIrredCan constraints] - - -- The definitely-insoluble case is for things like - -- Int ~ Bool tycons don't match - -- a ~ [a] occurs check - } - - | CTyEqCan { -- tv ~ rhs - -- Invariants: - -- * See Note [Applying the inert substitution] in TcFlatten - -- * tv not in tvs(rhs) (occurs check) - -- * If tv is a TauTv, then rhs has no foralls - -- (this avoids substituting a forall for the tyvar in other types) - -- * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant] - -- * rhs may have at most one top-level cast - -- * rhs (perhaps under the one cast) is not necessarily function-free, - -- but it has no top-level function. - -- E.g. a ~ [F b] is fine - -- but a ~ F b is not - -- * If the equality is representational, rhs has no top-level newtype - -- See Note [No top-level newtypes on RHS of representational - -- equalities] in TcCanonical - -- * If rhs (perhaps under the cast) is also a tv, then it is oriented - -- to give best chance of - -- unification happening; eg if rhs is touchable then lhs is too - cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] - cc_tyvar :: TcTyVar, - cc_rhs :: TcType, -- Not necessarily function-free (hence not Xi) - -- See invariants above - - cc_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev - } - - | CFunEqCan { -- F xis ~ fsk - -- Invariants: - -- * isTypeFamilyTyCon cc_fun - -- * tcTypeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant] - -- * always Nominal role - cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] - cc_fun :: TyCon, -- A type function - - cc_tyargs :: [Xi], -- cc_tyargs are function-free (hence Xi) - -- Either under-saturated or exactly saturated - -- *never* over-saturated (because if so - -- we should have decomposed) - - cc_fsk :: TcTyVar -- [G] always a FlatSkolTv - -- [W], [WD], or [D] always a FlatMetaTv - -- See Note [The flattening story] in TcFlatten - } - - | CNonCanonical { -- See Note [NonCanonical Semantics] in TcSMonad - cc_ev :: CtEvidence - } - - | CHoleCan { -- See Note [Hole constraints] - -- Treated as an "insoluble" constraint - -- See Note [Insoluble constraints] - cc_ev :: CtEvidence, - cc_hole :: Hole - } - - | CQuantCan QCInst -- A quantified constraint - -- NB: I expect to make more of the cases in Ct - -- look like this, with the payload in an - -- auxiliary type - ------------- -data QCInst -- A much simplified version of ClsInst - -- See Note [Quantified constraints] in TcCanonical - = QCI { qci_ev :: CtEvidence -- Always of type forall tvs. context => ty - -- Always Given - , qci_tvs :: [TcTyVar] -- The tvs - , qci_pred :: TcPredType -- The ty - , qci_pend_sc :: Bool -- Same as cc_pend_sc flag in CDictCan - -- Invariant: True => qci_pred is a ClassPred - } - -instance Outputable QCInst where - ppr (QCI { qci_ev = ev }) = ppr ev - ------------- --- | An expression or type hole -data Hole = ExprHole UnboundVar - -- ^ Either an out-of-scope variable or a "true" hole in an - -- expression (TypedHoles) - | TypeHole OccName - -- ^ A hole in a type (PartialTypeSignatures) - -instance Outputable Hole where - ppr (ExprHole ub) = ppr ub - ppr (TypeHole occ) = text "TypeHole" <> parens (ppr occ) - -holeOcc :: Hole -> OccName -holeOcc (ExprHole uv) = unboundVarOcc uv -holeOcc (TypeHole occ) = occ - -{- Note [Hole constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -CHoleCan constraints are used for two kinds of holes, -distinguished by cc_hole: - - * For holes in expressions (including variables not in scope) - e.g. f x = g _ x - - * For holes in type signatures - e.g. f :: _ -> _ - f x = [x,True] - -Note [CIrredCan constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -CIrredCan constraints are used for constraints that are "stuck" - - we can't solve them (yet) - - we can't use them to solve other constraints - - but they may become soluble if we substitute for some - of the type variables in the constraint - -Example 1: (c Int), where c :: * -> Constraint. We can't do anything - with this yet, but if later c := Num, *then* we can solve it - -Example 2: a ~ b, where a :: *, b :: k, where k is a kind variable - We don't want to use this to substitute 'b' for 'a', in case - 'k' is subsequently unifed with (say) *->*, because then - we'd have ill-kinded types floating about. Rather we want - to defer using the equality altogether until 'k' get resolved. - -Note [Ct/evidence invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field -of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan, - ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct) -This holds by construction; look at the unique place where CDictCan is -built (in TcCanonical). - -In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in -the evidence may *not* be fully zonked; we are careful not to look at it -during constraint solving. See Note [Evidence field of CtEvidence]. - -Note [Ct kind invariant] -~~~~~~~~~~~~~~~~~~~~~~~~ -CTyEqCan and CFunEqCan both require that the kind of the lhs matches the kind -of the rhs. This is necessary because both constraints are used for substitutions -during solving. If the kinds differed, then the substitution would take a well-kinded -type to an ill-kinded one. - --} - -mkNonCanonical :: CtEvidence -> Ct -mkNonCanonical ev = CNonCanonical { cc_ev = ev } - -mkNonCanonicalCt :: Ct -> Ct -mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct } - -mkIrredCt :: CtEvidence -> Ct -mkIrredCt ev = CIrredCan { cc_ev = ev, cc_insol = False } - -mkInsolubleCt :: CtEvidence -> Ct -mkInsolubleCt ev = CIrredCan { cc_ev = ev, cc_insol = True } - -mkGivens :: CtLoc -> [EvId] -> [Ct] -mkGivens loc ev_ids - = map mk ev_ids - where - mk ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id - , ctev_pred = evVarPred ev_id - , ctev_loc = loc }) - -ctEvidence :: Ct -> CtEvidence -ctEvidence (CQuantCan (QCI { qci_ev = ev })) = ev -ctEvidence ct = cc_ev ct - -ctLoc :: Ct -> CtLoc -ctLoc = ctEvLoc . ctEvidence - -setCtLoc :: Ct -> CtLoc -> Ct -setCtLoc ct loc = ct { cc_ev = (cc_ev ct) { ctev_loc = loc } } - -ctOrigin :: Ct -> CtOrigin -ctOrigin = ctLocOrigin . ctLoc - -ctPred :: Ct -> PredType --- See Note [Ct/evidence invariant] -ctPred ct = ctEvPred (ctEvidence ct) - -ctEvId :: Ct -> EvVar --- The evidence Id for this Ct -ctEvId ct = ctEvEvId (ctEvidence ct) - --- | Makes a new equality predicate with the same role as the given --- evidence. -mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType -mkTcEqPredLikeEv ev - = case predTypeEqRel pred of - NomEq -> mkPrimEqPred - ReprEq -> mkReprPrimEqPred - where - pred = ctEvPred ev - --- | Get the flavour of the given 'Ct' -ctFlavour :: Ct -> CtFlavour -ctFlavour = ctEvFlavour . ctEvidence - --- | Get the equality relation for the given 'Ct' -ctEqRel :: Ct -> EqRel -ctEqRel = ctEvEqRel . ctEvidence - -instance Outputable Ct where - ppr ct = ppr (ctEvidence ct) <+> parens pp_sort - where - pp_sort = case ct of - CTyEqCan {} -> text "CTyEqCan" - CFunEqCan {} -> text "CFunEqCan" - CNonCanonical {} -> text "CNonCanonical" - CDictCan { cc_pend_sc = pend_sc } - | pend_sc -> text "CDictCan(psc)" - | otherwise -> text "CDictCan" - CIrredCan { cc_insol = insol } - | insol -> text "CIrredCan(insol)" - | otherwise -> text "CIrredCan(sol)" - CHoleCan { cc_hole = hole } -> text "CHoleCan:" <+> ppr hole - CQuantCan (QCI { qci_pend_sc = pend_sc }) - | pend_sc -> text "CQuantCan(psc)" - | otherwise -> text "CQuantCan" - -{- -************************************************************************ -* * - Simple functions over evidence variables -* * -************************************************************************ --} - ----------------- Getting free tyvars ------------------------- - --- | Returns free variables of constraints as a non-deterministic set -tyCoVarsOfCt :: Ct -> TcTyCoVarSet -tyCoVarsOfCt = fvVarSet . tyCoFVsOfCt - --- | Returns free variables of constraints as a deterministically ordered. --- list. See Note [Deterministic FV] in FV. -tyCoVarsOfCtList :: Ct -> [TcTyCoVar] -tyCoVarsOfCtList = fvVarList . tyCoFVsOfCt - --- | Returns free variables of constraints as a composable FV computation. --- See Note [Deterministic FV] in FV. -tyCoFVsOfCt :: Ct -> FV -tyCoFVsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) - = tyCoFVsOfType xi `unionFV` FV.unitFV tv - `unionFV` tyCoFVsOfType (tyVarKind tv) -tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk }) - = tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk - `unionFV` tyCoFVsOfType (tyVarKind fsk) -tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys -tyCoFVsOfCt ct = tyCoFVsOfType (ctPred ct) - --- | Returns free variables of a bag of constraints as a non-deterministic --- set. See Note [Deterministic FV] in FV. -tyCoVarsOfCts :: Cts -> TcTyCoVarSet -tyCoVarsOfCts = fvVarSet . tyCoFVsOfCts - --- | Returns free variables of a bag of constraints as a deterministically --- odered list. See Note [Deterministic FV] in FV. -tyCoVarsOfCtsList :: Cts -> [TcTyCoVar] -tyCoVarsOfCtsList = fvVarList . tyCoFVsOfCts - --- | Returns free variables of a bag of constraints as a composable FV --- computation. See Note [Deterministic FV] in FV. -tyCoFVsOfCts :: Cts -> FV -tyCoFVsOfCts = foldr (unionFV . tyCoFVsOfCt) emptyFV - --- | Returns free variables of WantedConstraints as a non-deterministic --- set. See Note [Deterministic FV] in FV. -tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet --- Only called on *zonked* things, hence no need to worry about flatten-skolems -tyCoVarsOfWC = fvVarSet . tyCoFVsOfWC - --- | Returns free variables of WantedConstraints as a deterministically --- ordered list. See Note [Deterministic FV] in FV. -tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar] --- Only called on *zonked* things, hence no need to worry about flatten-skolems -tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC - --- | Returns free variables of WantedConstraints as a composable FV --- computation. See Note [Deterministic FV] in FV. -tyCoFVsOfWC :: WantedConstraints -> FV --- Only called on *zonked* things, hence no need to worry about flatten-skolems -tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic }) - = tyCoFVsOfCts simple `unionFV` - tyCoFVsOfBag tyCoFVsOfImplic implic - --- | Returns free variables of Implication as a composable FV computation. --- See Note [Deterministic FV] in FV. -tyCoFVsOfImplic :: Implication -> FV --- Only called on *zonked* things, hence no need to worry about flatten-skolems -tyCoFVsOfImplic (Implic { ic_skols = skols - , ic_given = givens - , ic_wanted = wanted }) - | isEmptyWC wanted - = emptyFV - | otherwise - = tyCoFVsVarBndrs skols $ - tyCoFVsVarBndrs givens $ - tyCoFVsOfWC wanted - -tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV -tyCoFVsOfBag tvs_of = foldr (unionFV . tvs_of) emptyFV - ---------------------------- -dropDerivedWC :: WantedConstraints -> WantedConstraints --- See Note [Dropping derived constraints] -dropDerivedWC wc@(WC { wc_simple = simples }) - = wc { wc_simple = dropDerivedSimples simples } - -- The wc_impl implications are already (recursively) filtered - --------------------------- -dropDerivedSimples :: Cts -> Cts --- Drop all Derived constraints, but make [W] back into [WD], --- so that if we re-simplify these constraints we will get all --- the right derived constraints re-generated. Forgetting this --- step led to #12936 -dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples - -dropDerivedCt :: Ct -> Maybe Ct -dropDerivedCt ct - = case ctEvFlavour ev of - Wanted WOnly -> Just (ct' { cc_ev = ev_wd }) - Wanted _ -> Just ct' - _ | isDroppableCt ct -> Nothing - | otherwise -> Just ct - where - ev = ctEvidence ct - ev_wd = ev { ctev_nosh = WDeriv } - ct' = setPendingScDict ct -- See Note [Resetting cc_pend_sc] - -{- Note [Resetting cc_pend_sc] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we discard Derived constraints, in dropDerivedSimples, we must -set the cc_pend_sc flag to True, so that if we re-process this -CDictCan we will re-generate its derived superclasses. Otherwise -we might miss some fundeps. #13662 showed this up. - -See Note [The superclass story] in TcCanonical. --} - -isDroppableCt :: Ct -> Bool -isDroppableCt ct - = isDerived ev && not keep_deriv - -- Drop only derived constraints, and then only if they - -- obey Note [Dropping derived constraints] - where - ev = ctEvidence ct - loc = ctEvLoc ev - orig = ctLocOrigin loc - - keep_deriv - = case ct of - CHoleCan {} -> True - CIrredCan { cc_insol = insoluble } - -> keep_eq insoluble - _ -> keep_eq False - - keep_eq definitely_insoluble - | isGivenOrigin orig -- Arising only from givens - = definitely_insoluble -- Keep only definitely insoluble - | otherwise - = case orig of - KindEqOrigin {} -> True -- See Note [Dropping derived constraints] - - -- See Note [Dropping derived constraints] - -- For fundeps, drop wanted/wanted interactions - FunDepOrigin2 {} -> True -- Top-level/Wanted - FunDepOrigin1 _ loc1 _ loc2 - | g1 || g2 -> True -- Given/Wanted errors: keep all - | otherwise -> False -- Wanted/Wanted errors: discard - where - g1 = isGivenLoc loc1 - g2 = isGivenLoc loc2 - - _ -> False - -arisesFromGivens :: Ct -> Bool -arisesFromGivens ct - = case ctEvidence ct of - CtGiven {} -> True - CtWanted {} -> False - CtDerived { ctev_loc = loc } -> isGivenLoc loc - -isGivenLoc :: CtLoc -> Bool -isGivenLoc loc = isGivenOrigin (ctLocOrigin loc) - -isGivenOrigin :: CtOrigin -> Bool -isGivenOrigin (GivenOrigin {}) = True -isGivenOrigin (FunDepOrigin1 _ l1 _ l2) = isGivenLoc l1 && isGivenLoc l2 -isGivenOrigin (FunDepOrigin2 _ o1 _ _) = isGivenOrigin o1 -isGivenOrigin _ = False - -{- Note [Dropping derived constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In general we discard derived constraints at the end of constraint solving; -see dropDerivedWC. For example - - * Superclasses: if we have an unsolved [W] (Ord a), we don't want to - complain about an unsolved [D] (Eq a) as well. - - * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate - [D] Int ~ Bool, and we don't want to report that because it's - incomprehensible. That is why we don't rewrite wanteds with wanteds! - - * We might float out some Wanteds from an implication, leaving behind - their insoluble Deriveds. For example: - - forall a[2]. [W] alpha[1] ~ Int - [W] alpha[1] ~ Bool - [D] Int ~ Bool - - The Derived is insoluble, but we very much want to drop it when floating - out. - -But (tiresomely) we do keep *some* Derived constraints: - - * Type holes are derived constraints, because they have no evidence - and we want to keep them, so we get the error report - - * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with - KindEqOrigin, may arise from a type equality a ~ Int#, say. See - Note [Equalities with incompatible kinds] in TcCanonical. - Keeping these around produces better error messages, in practice. - E.g., test case dependent/should_fail/T11471 - - * We keep most derived equalities arising from functional dependencies - - Given/Given interactions (subset of FunDepOrigin1): - The definitely-insoluble ones reflect unreachable code. - - Others not-definitely-insoluble ones like [D] a ~ Int do not - reflect unreachable code; indeed if fundeps generated proofs, it'd - be a useful equality. See #14763. So we discard them. - - - Given/Wanted interacGiven or Wanted interacting with an - instance declaration (FunDepOrigin2) - - - Given/Wanted interactions (FunDepOrigin1); see #9612 - - - But for Wanted/Wanted interactions we do /not/ want to report an - error (#13506). Consider [W] C Int Int, [W] C Int Bool, with - a fundep on class C. We don't want to report an insoluble Int~Bool; - c.f. "wanteds do not rewrite wanteds". - -To distinguish these cases we use the CtOrigin. - -NB: we keep *all* derived insolubles under some circumstances: - - * They are looked at by simplifyInfer, to decide whether to - generalise. Example: [W] a ~ Int, [W] a ~ Bool - We get [D] Int ~ Bool, and indeed the constraints are insoluble, - and we want simplifyInfer to see that, even though we don't - ultimately want to generate an (inexplicable) error message from it - - -************************************************************************ -* * - CtEvidence - The "flavor" of a canonical constraint -* * -************************************************************************ --} - -isWantedCt :: Ct -> Bool -isWantedCt = isWanted . ctEvidence - -isGivenCt :: Ct -> Bool -isGivenCt = isGiven . ctEvidence - -isDerivedCt :: Ct -> Bool -isDerivedCt = isDerived . ctEvidence - -isCTyEqCan :: Ct -> Bool -isCTyEqCan (CTyEqCan {}) = True -isCTyEqCan (CFunEqCan {}) = False -isCTyEqCan _ = False - -isCDictCan_Maybe :: Ct -> Maybe Class -isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls -isCDictCan_Maybe _ = Nothing - -isCFunEqCan_maybe :: Ct -> Maybe (TyCon, [Type]) -isCFunEqCan_maybe (CFunEqCan { cc_fun = tc, cc_tyargs = xis }) = Just (tc, xis) -isCFunEqCan_maybe _ = Nothing - -isCFunEqCan :: Ct -> Bool -isCFunEqCan (CFunEqCan {}) = True -isCFunEqCan _ = False - -isCNonCanonical :: Ct -> Bool -isCNonCanonical (CNonCanonical {}) = True -isCNonCanonical _ = False - -isHoleCt:: Ct -> Bool -isHoleCt (CHoleCan {}) = True -isHoleCt _ = False - -isOutOfScopeCt :: Ct -> Bool --- We treat expression holes representing out-of-scope variables a bit --- differently when it comes to error reporting -isOutOfScopeCt (CHoleCan { cc_hole = ExprHole (OutOfScope {}) }) = True -isOutOfScopeCt _ = False - -isExprHoleCt :: Ct -> Bool -isExprHoleCt (CHoleCan { cc_hole = ExprHole {} }) = True -isExprHoleCt _ = False - -isTypeHoleCt :: Ct -> Bool -isTypeHoleCt (CHoleCan { cc_hole = TypeHole {} }) = True -isTypeHoleCt _ = False - - -{- Note [Custom type errors in constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -When GHC reports a type-error about an unsolved-constraint, we check -to see if the constraint contains any custom-type errors, and if so -we report them. Here are some examples of constraints containing type -errors: - -TypeError msg -- The actual constraint is a type error - -TypError msg ~ Int -- Some type was supposed to be Int, but ended up - -- being a type error instead - -Eq (TypeError msg) -- A class constraint is stuck due to a type error - -F (TypeError msg) ~ a -- A type function failed to evaluate due to a type err - -It is also possible to have constraints where the type error is nested deeper, -for example see #11990, and also: - -Eq (F (TypeError msg)) -- Here the type error is nested under a type-function - -- call, which failed to evaluate because of it, - -- and so the `Eq` constraint was unsolved. - -- This may happen when one function calls another - -- and the called function produced a custom type error. --} - --- | A constraint is considered to be a custom type error, if it contains --- custom type errors anywhere in it. --- See Note [Custom type errors in constraints] -getUserTypeErrorMsg :: Ct -> Maybe Type -getUserTypeErrorMsg ct = findUserTypeError (ctPred ct) - where - findUserTypeError t = msum ( userTypeError_maybe t - : map findUserTypeError (subTys t) - ) - - subTys t = case splitAppTys t of - (t,[]) -> - case splitTyConApp_maybe t of - Nothing -> [] - Just (_,ts) -> ts - (t,ts) -> t : ts - - - - -isUserTypeErrorCt :: Ct -> Bool -isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of - Just _ -> True - _ -> False - -isPendingScDict :: Ct -> Maybe Ct --- Says whether this is a CDictCan with cc_pend_sc is True, --- AND if so flips the flag -isPendingScDict ct@(CDictCan { cc_pend_sc = True }) - = Just (ct { cc_pend_sc = False }) -isPendingScDict _ = Nothing - -isPendingScInst :: QCInst -> Maybe QCInst --- Same as isPrendinScDict, but for QCInsts -isPendingScInst qci@(QCI { qci_pend_sc = True }) - = Just (qci { qci_pend_sc = False }) -isPendingScInst _ = Nothing - -setPendingScDict :: Ct -> Ct --- Set the cc_pend_sc flag to True -setPendingScDict ct@(CDictCan { cc_pend_sc = False }) - = ct { cc_pend_sc = True } -setPendingScDict ct = ct - -superClassesMightHelp :: WantedConstraints -> Bool --- ^ True if taking superclasses of givens, or of wanteds (to perhaps --- expose more equalities or functional dependencies) might help to --- solve this constraint. See Note [When superclasses help] -superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics }) - = anyBag might_help_ct simples || anyBag might_help_implic implics - where - might_help_implic ic - | IC_Unsolved <- ic_status ic = superClassesMightHelp (ic_wanted ic) - | otherwise = False - - might_help_ct ct = isWantedCt ct && not (is_ip ct) - - is_ip (CDictCan { cc_class = cls }) = isIPClass cls - is_ip _ = False - -getPendingWantedScs :: Cts -> ([Ct], Cts) -getPendingWantedScs simples - = mapAccumBagL get [] simples - where - get acc ct | Just ct' <- isPendingScDict ct - = (ct':acc, ct') - | otherwise - = (acc, ct) - -{- Note [When superclasses help] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -First read Note [The superclass story] in TcCanonical. - -We expand superclasses and iterate only if there is at unsolved wanted -for which expansion of superclasses (e.g. from given constraints) -might actually help. The function superClassesMightHelp tells if -doing this superclass expansion might help solve this constraint. -Note that - - * We look inside implications; maybe it'll help to expand the Givens - at level 2 to help solve an unsolved Wanted buried inside an - implication. E.g. - forall a. Ord a => forall b. [W] Eq a - - * Superclasses help only for Wanted constraints. Derived constraints - are not really "unsolved" and we certainly don't want them to - trigger superclass expansion. This was a good part of the loop - in #11523 - - * Even for Wanted constraints, we say "no" for implicit parameters. - we have [W] ?x::ty, expanding superclasses won't help: - - Superclasses can't be implicit parameters - - If we have a [G] ?x:ty2, then we'll have another unsolved - [D] ty ~ ty2 (from the functional dependency) - which will trigger superclass expansion. - - It's a bit of a special case, but it's easy to do. The runtime cost - is low because the unsolved set is usually empty anyway (errors - aside), and the first non-imlicit-parameter will terminate the search. - - The special case is worth it (#11480, comment:2) because it - applies to CallStack constraints, which aren't type errors. If we have - f :: (C a) => blah - f x = ...undefined... - we'll get a CallStack constraint. If that's the only unsolved - constraint it'll eventually be solved by defaulting. So we don't - want to emit warnings about hitting the simplifier's iteration - limit. A CallStack constraint really isn't an unsolved - constraint; it can always be solved by defaulting. --} - -singleCt :: Ct -> Cts -singleCt = unitBag - -andCts :: Cts -> Cts -> Cts -andCts = unionBags - -listToCts :: [Ct] -> Cts -listToCts = listToBag - -ctsElts :: Cts -> [Ct] -ctsElts = bagToList - -consCts :: Ct -> Cts -> Cts -consCts = consBag - -snocCts :: Cts -> Ct -> Cts -snocCts = snocBag - -extendCtsList :: Cts -> [Ct] -> Cts -extendCtsList cts xs | null xs = cts - | otherwise = cts `unionBags` listToBag xs - -andManyCts :: [Cts] -> Cts -andManyCts = unionManyBags - -emptyCts :: Cts -emptyCts = emptyBag - -isEmptyCts :: Cts -> Bool -isEmptyCts = isEmptyBag - -pprCts :: Cts -> SDoc -pprCts cts = vcat (map ppr (bagToList cts)) - -{- -************************************************************************ -* * - Wanted constraints - These are forced to be in TcRnTypes because - TcLclEnv mentions WantedConstraints - WantedConstraint mentions CtLoc - CtLoc mentions ErrCtxt - ErrCtxt mentions TcM -* * -v%************************************************************************ --} - -data WantedConstraints - = WC { wc_simple :: Cts -- Unsolved constraints, all wanted - , wc_impl :: Bag Implication - } - -emptyWC :: WantedConstraints -emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag } - -mkSimpleWC :: [CtEvidence] -> WantedConstraints -mkSimpleWC cts - = WC { wc_simple = listToBag (map mkNonCanonical cts) - , wc_impl = emptyBag } - -mkImplicWC :: Bag Implication -> WantedConstraints -mkImplicWC implic - = WC { wc_simple = emptyBag, wc_impl = implic } - -isEmptyWC :: WantedConstraints -> Bool -isEmptyWC (WC { wc_simple = f, wc_impl = i }) - = isEmptyBag f && isEmptyBag i - - --- | Checks whether a the given wanted constraints are solved, i.e. --- that there are no simple constraints left and all the implications --- are solved. -isSolvedWC :: WantedConstraints -> Bool -isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl} = - isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl - -andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints -andWC (WC { wc_simple = f1, wc_impl = i1 }) - (WC { wc_simple = f2, wc_impl = i2 }) - = WC { wc_simple = f1 `unionBags` f2 - , wc_impl = i1 `unionBags` i2 } - -unionsWC :: [WantedConstraints] -> WantedConstraints -unionsWC = foldr andWC emptyWC - -addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints -addSimples wc cts - = wc { wc_simple = wc_simple wc `unionBags` cts } - -- Consider: Put the new constraints at the front, so they get solved first - -addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints -addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic } - -addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints -addInsols wc cts - = wc { wc_simple = wc_simple wc `unionBags` cts } - -insolublesOnly :: WantedConstraints -> WantedConstraints --- Keep only the definitely-insoluble constraints -insolublesOnly (WC { wc_simple = simples, wc_impl = implics }) - = WC { wc_simple = filterBag insolubleCt simples - , wc_impl = mapBag implic_insols_only implics } - where - implic_insols_only implic - = implic { ic_wanted = insolublesOnly (ic_wanted implic) } - -isSolvedStatus :: ImplicStatus -> Bool -isSolvedStatus (IC_Solved {}) = True -isSolvedStatus _ = False - -isInsolubleStatus :: ImplicStatus -> Bool -isInsolubleStatus IC_Insoluble = True -isInsolubleStatus IC_BadTelescope = True -isInsolubleStatus _ = False - -insolubleImplic :: Implication -> Bool -insolubleImplic ic = isInsolubleStatus (ic_status ic) - -insolubleWC :: WantedConstraints -> Bool -insolubleWC (WC { wc_impl = implics, wc_simple = simples }) - = anyBag insolubleCt simples - || anyBag insolubleImplic implics - -insolubleCt :: Ct -> Bool --- Definitely insoluble, in particular /excluding/ type-hole constraints --- Namely: a) an equality constraint --- b) that is insoluble --- c) and does not arise from a Given -insolubleCt ct - | isHoleCt ct = isOutOfScopeCt ct -- See Note [Insoluble holes] - | not (insolubleEqCt ct) = False - | arisesFromGivens ct = False -- See Note [Given insolubles] - | otherwise = True - -insolubleEqCt :: Ct -> Bool --- Returns True of /equality/ constraints --- that are /definitely/ insoluble --- It won't detect some definite errors like --- F a ~ T (F a) --- where F is a type family, which actually has an occurs check --- --- The function is tuned for application /after/ constraint solving --- i.e. assuming canonicalisation has been done --- E.g. It'll reply True for a ~ [a] --- but False for [a] ~ a --- and --- True for Int ~ F a Int --- but False for Maybe Int ~ F a Int Int --- (where F is an arity-1 type function) -insolubleEqCt (CIrredCan { cc_insol = insol }) = insol -insolubleEqCt _ = False - -instance Outputable WantedConstraints where - ppr (WC {wc_simple = s, wc_impl = i}) - = text "WC" <+> braces (vcat - [ ppr_bag (text "wc_simple") s - , ppr_bag (text "wc_impl") i ]) - -ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc -ppr_bag doc bag - | isEmptyBag bag = empty - | otherwise = hang (doc <+> equals) - 2 (foldr (($$) . ppr) empty bag) - -{- Note [Given insolubles] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider (#14325, comment:) - class (a~b) => C a b - - foo :: C a c => a -> c - foo x = x - - hm3 :: C (f b) b => b -> f b - hm3 x = foo x - -In the RHS of hm3, from the [G] C (f b) b we get the insoluble -[G] f b ~# b. Then we also get an unsolved [W] C b (f b). -Residual implication looks like - forall b. C (f b) b => [G] f b ~# b - [W] C f (f b) - -We do /not/ want to set the implication status to IC_Insoluble, -because that'll suppress reports of [W] C b (f b). But we -may not report the insoluble [G] f b ~# b either (see Note [Given errors] -in TcErrors), so we may fail to report anything at all! Yikes. - -The same applies to Derived constraints that /arise from/ Givens. -E.g. f :: (C Int [a]) => blah -where a fundep means we get - [D] Int ~ [a] -By the same reasoning we must not suppress other errors (#15767) - -Bottom line: insolubleWC (called in TcSimplify.setImplicationStatus) - should ignore givens even if they are insoluble. - -Note [Insoluble holes] -~~~~~~~~~~~~~~~~~~~~~~ -Hole constraints that ARE NOT treated as truly insoluble: - a) type holes, arising from PartialTypeSignatures, - b) "true" expression holes arising from TypedHoles - -An "expression hole" or "type hole" constraint isn't really an error -at all; it's a report saying "_ :: Int" here. But an out-of-scope -variable masquerading as expression holes IS treated as truly -insoluble, so that it trumps other errors during error reporting. -Yuk! - -************************************************************************ -* * - Implication constraints -* * -************************************************************************ --} - -data Implication - = Implic { -- Invariants for a tree of implications: - -- see TcType Note [TcLevel and untouchable type variables] - - ic_tclvl :: TcLevel, -- TcLevel of unification variables - -- allocated /inside/ this implication - - ic_skols :: [TcTyVar], -- Introduced skolems - ic_info :: SkolemInfo, -- See Note [Skolems in an implication] - -- See Note [Shadowing in a constraint] - - ic_telescope :: Maybe SDoc, -- User-written telescope, if there is one - -- See Note [Checking telescopes] - - ic_given :: [EvVar], -- Given evidence variables - -- (order does not matter) - -- See Invariant (GivenInv) in TcType - - ic_no_eqs :: Bool, -- True <=> ic_givens have no equalities, for sure - -- False <=> ic_givens might have equalities - - ic_env :: Env TcGblEnv TcLclEnv, - -- Records the Env at the time of creation. - -- - -- This is primarly needed for the enclosed - -- TcLclEnv, which gives the source location - -- and error context for the implication, and - -- hence for all the given evidence variables. - -- - -- The enclosed DynFlags also influences error - -- reporting. See Note [Avoid - -- -Winaccessible-code when deriving] in - -- TcInstDcls. - - ic_wanted :: WantedConstraints, -- The wanteds - -- See Invariang (WantedInf) in TcType - - ic_binds :: EvBindsVar, -- Points to the place to fill in the - -- abstraction and bindings. - - -- The ic_need fields keep track of which Given evidence - -- is used by this implication or its children - -- NB: including stuff used by nested implications that have since - -- been discarded - ic_need_inner :: VarSet, -- Includes all used Given evidence - ic_need_outer :: VarSet, -- Includes only the free Given evidence - -- i.e. ic_need_inner after deleting - -- (a) givens (b) binders of ic_binds - - ic_status :: ImplicStatus - } - --- | Create a new 'Implication' with as many sensible defaults for its fields --- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do --- /not/ have sensible defaults, so they are initialized with lazy thunks that --- will 'panic' if forced, so one should take care to initialize these fields --- after creation. --- --- This is monadic purely to look up the 'Env', which is used to initialize --- 'ic_env'. -newImplication :: TcM Implication -newImplication - = do env <- getEnv - return (implicationPrototype { ic_env = env }) - -implicationPrototype :: Implication -implicationPrototype - = Implic { -- These fields must be initialised - ic_tclvl = panic "newImplic:tclvl" - , ic_binds = panic "newImplic:binds" - , ic_info = panic "newImplic:info" - , ic_env = panic "newImplic:env" - - -- The rest have sensible default values - , ic_skols = [] - , ic_telescope = Nothing - , ic_given = [] - , ic_wanted = emptyWC - , ic_no_eqs = False - , ic_status = IC_Unsolved - , ic_need_inner = emptyVarSet - , ic_need_outer = emptyVarSet } - --- | Retrieve the enclosed 'TcLclEnv' from an 'Implication'. -implicLclEnv :: Implication -> TcLclEnv -implicLclEnv = env_lcl . ic_env - --- | Retrieve the enclosed 'DynFlags' from an 'Implication'. -implicDynFlags :: Implication -> DynFlags -implicDynFlags = hsc_dflags . env_top . ic_env - -data ImplicStatus - = IC_Solved -- All wanteds in the tree are solved, all the way down - { ics_dead :: [EvVar] } -- Subset of ic_given that are not needed - -- See Note [Tracking redundant constraints] in TcSimplify - - | IC_Insoluble -- At least one insoluble constraint in the tree - - | IC_BadTelescope -- solved, but the skolems in the telescope are out of - -- dependency order - - | IC_Unsolved -- Neither of the above; might go either way - -instance Outputable Implication where - ppr (Implic { ic_tclvl = tclvl, ic_skols = skols - , ic_given = given, ic_no_eqs = no_eqs - , ic_wanted = wanted, ic_status = status - , ic_binds = binds - , ic_need_inner = need_in, ic_need_outer = need_out - , ic_info = info }) - = hang (text "Implic" <+> lbrace) - 2 (sep [ text "TcLevel =" <+> ppr tclvl - , text "Skolems =" <+> pprTyVars skols - , text "No-eqs =" <+> ppr no_eqs - , text "Status =" <+> ppr status - , hang (text "Given =") 2 (pprEvVars given) - , hang (text "Wanted =") 2 (ppr wanted) - , text "Binds =" <+> ppr binds - , whenPprDebug (text "Needed inner =" <+> ppr need_in) - , whenPprDebug (text "Needed outer =" <+> ppr need_out) - , pprSkolInfo info ] <+> rbrace) - -instance Outputable ImplicStatus where - ppr IC_Insoluble = text "Insoluble" - ppr IC_BadTelescope = text "Bad telescope" - ppr IC_Unsolved = text "Unsolved" - ppr (IC_Solved { ics_dead = dead }) - = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead)) - -{- Note [Checking telescopes] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When kind-checking a /user-written/ type, we might have a "bad telescope" -like this one: - data SameKind :: forall k. k -> k -> Type - type Foo :: forall a k (b :: k). SameKind a b -> Type - -The kind of 'a' mentions 'k' which is bound after 'a'. Oops. - -Knowing this means that unification etc must have happened, so it's -convenient to detect it in the constraint solver: - -* We make a single implication constraint when kind-checking - the 'forall' in Foo's kind, something like - forall a k (b::k). { wanted constraints } - -* Having solved {wanted}, before discarding the now-solved implication, - the costraint solver checks the dependency order of the skolem - variables (ic_skols). This is done in setImplicationStatus. - -* This check is only necessary if the implication was born from a - user-written signature. If, say, it comes from checking a pattern - match that binds existentials, where the type of the data constructor - is known to be valid (it in tcConPat), no need for the check. - - So the check is done if and only if ic_telescope is (Just blah). - -* If ic_telesope is (Just d), the d::SDoc displays the original, - user-written type variables. - -* Be careful /NOT/ to discard an implication with non-Nothing - ic_telescope, even if ic_wanted is empty. We must give the - constraint solver a chance to make that bad-telesope test! Hence - the extra guard in emitResidualTvConstraint; see #16247 - -See also TcHsTYpe Note [Keeping scoped variables in order: Explicit] - -Note [Needed evidence variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Th ic_need_evs field holds the free vars of ic_binds, and all the -ic_binds in nested implications. - - * Main purpose: if one of the ic_givens is not mentioned in here, it - is redundant. - - * solveImplication may drop an implication altogether if it has no - remaining 'wanteds'. But we still track the free vars of its - evidence binds, even though it has now disappeared. - -Note [Shadowing in a constraint] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We assume NO SHADOWING in a constraint. Specifically - * The unification variables are all implicitly quantified at top - level, and are all unique - * The skolem variables bound in ic_skols are all freah when the - implication is created. -So we can safely substitute. For example, if we have - forall a. a~Int => ...(forall b. ...a...)... -we can push the (a~Int) constraint inwards in the "givens" without -worrying that 'b' might clash. - -Note [Skolems in an implication] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The skolems in an implication are not there to perform a skolem escape -check. That happens because all the environment variables are in the -untouchables, and therefore cannot be unified with anything at all, -let alone the skolems. - -Instead, ic_skols is used only when considering floating a constraint -outside the implication in TcSimplify.floatEqualities or -TcSimplify.approximateImplications - -Note [Insoluble constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Some of the errors that we get during canonicalization are best -reported when all constraints have been simplified as much as -possible. For instance, assume that during simplification the -following constraints arise: - - [Wanted] F alpha ~ uf1 - [Wanted] beta ~ uf1 beta - -When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail -we will simply see a message: - 'Can't construct the infinite type beta ~ uf1 beta' -and the user has no idea what the uf1 variable is. - -Instead our plan is that we will NOT fail immediately, but: - (1) Record the "frozen" error in the ic_insols field - (2) Isolate the offending constraint from the rest of the inerts - (3) Keep on simplifying/canonicalizing - -At the end, we will hopefully have substituted uf1 := F alpha, and we -will be able to report a more informative error: - 'Can't construct the infinite type beta ~ F alpha beta' - -Insoluble constraints *do* include Derived constraints. For example, -a functional dependency might give rise to [D] Int ~ Bool, and we must -report that. If insolubles did not contain Deriveds, reportErrors would -never see it. - - -************************************************************************ -* * - Pretty printing -* * -************************************************************************ --} - -pprEvVars :: [EvVar] -> SDoc -- Print with their types -pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars) - -pprEvVarTheta :: [EvVar] -> SDoc -pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars) - -pprEvVarWithType :: EvVar -> SDoc -pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v) - - - --- | Wraps the given type with the constraints (via ic_given) in the given --- implication, according to the variables mentioned (via ic_skols) --- in the implication, but taking care to only wrap those variables --- that are mentioned in the type or the implication. -wrapTypeWithImplication :: Type -> Implication -> Type -wrapTypeWithImplication ty impl = wrapType ty mentioned_skols givens - where givens = map idType $ ic_given impl - skols = ic_skols impl - freeVars = fvVarSet $ tyCoFVsOfTypes (ty:givens) - mentioned_skols = filter (`elemVarSet` freeVars) skols - -wrapType :: Type -> [TyVar] -> [PredType] -> Type -wrapType ty skols givens = mkSpecForAllTys skols $ mkPhiTy givens ty - - -{- -************************************************************************ -* * - CtEvidence -* * -************************************************************************ - -Note [Evidence field of CtEvidence] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -During constraint solving we never look at the type of ctev_evar/ctev_dest; -instead we look at the ctev_pred field. The evtm/evar field -may be un-zonked. - -Note [Bind new Givens immediately] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For Givens we make new EvVars and bind them immediately. Two main reasons: - * Gain sharing. E.g. suppose we start with g :: C a b, where - class D a => C a b - class (E a, F a) => D a - If we generate all g's superclasses as separate EvTerms we might - get selD1 (selC1 g) :: E a - selD2 (selC1 g) :: F a - selC1 g :: D a - which we could do more economically as: - g1 :: D a = selC1 g - g2 :: E a = selD1 g1 - g3 :: F a = selD2 g1 - - * For *coercion* evidence we *must* bind each given: - class (a~b) => C a b where .... - f :: C a b => .... - Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b. - But that superclass selector can't (yet) appear in a coercion - (see evTermCoercion), so the easy thing is to bind it to an Id. - -So a Given has EvVar inside it rather than (as previously) an EvTerm. - --} - --- | A place for type-checking evidence to go after it is generated. --- Wanted equalities are always HoleDest; other wanteds are always --- EvVarDest. -data TcEvDest - = EvVarDest EvVar -- ^ bind this var to the evidence - -- EvVarDest is always used for non-type-equalities - -- e.g. class constraints - - | HoleDest CoercionHole -- ^ fill in this hole with the evidence - -- HoleDest is always used for type-equalities - -- See Note [Coercion holes] in TyCoRep - -data CtEvidence - = CtGiven -- Truly given, not depending on subgoals - { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] - , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence] - , ctev_loc :: CtLoc } - - - | CtWanted -- Wanted goal - { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] - , ctev_dest :: TcEvDest - , ctev_nosh :: ShadowInfo -- See Note [Constraint flavours] - , ctev_loc :: CtLoc } - - | CtDerived -- A goal that we don't really have to solve and can't - -- immediately rewrite anything other than a derived - -- (there's no evidence!) but if we do manage to solve - -- it may help in solving other goals. - { ctev_pred :: TcPredType - , ctev_loc :: CtLoc } - -ctEvPred :: CtEvidence -> TcPredType --- The predicate of a flavor -ctEvPred = ctev_pred - -ctEvLoc :: CtEvidence -> CtLoc -ctEvLoc = ctev_loc - -ctEvOrigin :: CtEvidence -> CtOrigin -ctEvOrigin = ctLocOrigin . ctEvLoc - --- | Get the equality relation relevant for a 'CtEvidence' -ctEvEqRel :: CtEvidence -> EqRel -ctEvEqRel = predTypeEqRel . ctEvPred - --- | Get the role relevant for a 'CtEvidence' -ctEvRole :: CtEvidence -> Role -ctEvRole = eqRelRole . ctEvEqRel - -ctEvTerm :: CtEvidence -> EvTerm -ctEvTerm ev = EvExpr (ctEvExpr ev) - -ctEvExpr :: CtEvidence -> EvExpr -ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) - = Coercion $ ctEvCoercion ev -ctEvExpr ev = evId (ctEvEvId ev) - -ctEvCoercion :: HasDebugCallStack => CtEvidence -> Coercion -ctEvCoercion (CtGiven { ctev_evar = ev_id }) - = mkTcCoVarCo ev_id -ctEvCoercion (CtWanted { ctev_dest = dest }) - | HoleDest hole <- dest - = -- ctEvCoercion is only called on type equalities - -- and they always have HoleDests - mkHoleCo hole -ctEvCoercion ev - = pprPanic "ctEvCoercion" (ppr ev) - -ctEvEvId :: CtEvidence -> EvVar -ctEvEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev -ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h -ctEvEvId (CtGiven { ctev_evar = ev }) = ev -ctEvEvId ctev@(CtDerived {}) = pprPanic "ctEvId:" (ppr ctev) - -instance Outputable TcEvDest where - ppr (HoleDest h) = text "hole" <> ppr h - ppr (EvVarDest ev) = ppr ev - -instance Outputable CtEvidence where - ppr ev = ppr (ctEvFlavour ev) - <+> pp_ev - <+> braces (ppr (ctl_depth (ctEvLoc ev))) <> dcolon - -- Show the sub-goal depth too - <+> ppr (ctEvPred ev) - where - pp_ev = case ev of - CtGiven { ctev_evar = v } -> ppr v - CtWanted {ctev_dest = d } -> ppr d - CtDerived {} -> text "_" - -isWanted :: CtEvidence -> Bool -isWanted (CtWanted {}) = True -isWanted _ = False - -isGiven :: CtEvidence -> Bool -isGiven (CtGiven {}) = True -isGiven _ = False - -isDerived :: CtEvidence -> Bool -isDerived (CtDerived {}) = True -isDerived _ = False - -{- -%************************************************************************ -%* * - CtFlavour -%* * -%************************************************************************ - -Note [Constraint flavours] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -Constraints come in four flavours: - -* [G] Given: we have evidence - -* [W] Wanted WOnly: we want evidence - -* [D] Derived: any solution must satisfy this constraint, but - we don't need evidence for it. Examples include: - - superclasses of [W] class constraints - - equalities arising from functional dependencies - or injectivity - -* [WD] Wanted WDeriv: a single constraint that represents - both [W] and [D] - We keep them paired as one both for efficiency, and because - when we have a finite map F tys -> CFunEqCan, it's inconvenient - to have two CFunEqCans in the range - -The ctev_nosh field of a Wanted distinguishes between [W] and [WD] - -Wanted constraints are born as [WD], but are split into [W] and its -"shadow" [D] in TcSMonad.maybeEmitShadow. - -See Note [The improvement story and derived shadows] in TcSMonad --} - -data CtFlavour -- See Note [Constraint flavours] - = Given - | Wanted ShadowInfo - | Derived - deriving Eq - -data ShadowInfo - = WDeriv -- [WD] This Wanted constraint has no Derived shadow, - -- so it behaves like a pair of a Wanted and a Derived - | WOnly -- [W] It has a separate derived shadow - -- See Note [Derived shadows] - deriving( Eq ) - -isGivenOrWDeriv :: CtFlavour -> Bool -isGivenOrWDeriv Given = True -isGivenOrWDeriv (Wanted WDeriv) = True -isGivenOrWDeriv _ = False - -instance Outputable CtFlavour where - ppr Given = text "[G]" - ppr (Wanted WDeriv) = text "[WD]" - ppr (Wanted WOnly) = text "[W]" - ppr Derived = text "[D]" - -ctEvFlavour :: CtEvidence -> CtFlavour -ctEvFlavour (CtWanted { ctev_nosh = nosh }) = Wanted nosh -ctEvFlavour (CtGiven {}) = Given -ctEvFlavour (CtDerived {}) = Derived - --- | Whether or not one 'Ct' can rewrite another is determined by its --- flavour and its equality relation. See also --- Note [Flavours with roles] in TcSMonad -type CtFlavourRole = (CtFlavour, EqRel) - --- | Extract the flavour, role, and boxity from a 'CtEvidence' -ctEvFlavourRole :: CtEvidence -> CtFlavourRole -ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev) - --- | Extract the flavour and role from a 'Ct' -ctFlavourRole :: Ct -> CtFlavourRole --- Uses short-cuts to role for special cases -ctFlavourRole (CDictCan { cc_ev = ev }) - = (ctEvFlavour ev, NomEq) -ctFlavourRole (CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel }) - = (ctEvFlavour ev, eq_rel) -ctFlavourRole (CFunEqCan { cc_ev = ev }) - = (ctEvFlavour ev, NomEq) -ctFlavourRole (CHoleCan { cc_ev = ev }) - = (ctEvFlavour ev, NomEq) -- NomEq: CHoleCans can be rewritten by - -- by nominal equalities but empahatically - -- not by representational equalities -ctFlavourRole ct - = ctEvFlavourRole (ctEvidence ct) - -{- Note [eqCanRewrite] -~~~~~~~~~~~~~~~~~~~~~~ -(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form -tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of -a can-rewrite relation, see Definition [Can-rewrite relation] in -TcSMonad. - -With the solver handling Coercible constraints like equality constraints, -the rewrite conditions must take role into account, never allowing -a representational equality to rewrite a nominal one. - -Note [Wanteds do not rewrite Wanteds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We don't allow Wanteds to rewrite Wanteds, because that can give rise -to very confusing type error messages. A good example is #8450. -Here's another - f :: a -> Bool - f x = ( [x,'c'], [x,True] ) `seq` True -Here we get - [W] a ~ Char - [W] a ~ Bool -but we do not want to complain about Bool ~ Char! - -Note [Deriveds do rewrite Deriveds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -However we DO allow Deriveds to rewrite Deriveds, because that's how -improvement works; see Note [The improvement story] in TcInteract. - -However, for now at least I'm only letting (Derived,NomEq) rewrite -(Derived,NomEq) and not doing anything for ReprEq. If we have - eqCanRewriteFR (Derived, NomEq) (Derived, _) = True -then we lose property R2 of Definition [Can-rewrite relation] -in TcSMonad - R2. If f1 >= f, and f2 >= f, - then either f1 >= f2 or f2 >= f1 -Consider f1 = (Given, ReprEq) - f2 = (Derived, NomEq) - f = (Derived, ReprEq) - -I thought maybe we could never get Derived ReprEq constraints, but -we can; straight from the Wanteds during improvement. And from a Derived -ReprEq we could conceivably get a Derived NomEq improvement (by decomposing -a type constructor with Nomninal role), and hence unify. --} - -eqCanRewrite :: EqRel -> EqRel -> Bool -eqCanRewrite NomEq _ = True -eqCanRewrite ReprEq ReprEq = True -eqCanRewrite ReprEq NomEq = False - -eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool --- Can fr1 actually rewrite fr2? --- Very important function! --- See Note [eqCanRewrite] --- See Note [Wanteds do not rewrite Wanteds] --- See Note [Deriveds do rewrite Deriveds] -eqCanRewriteFR (Given, r1) (_, r2) = eqCanRewrite r1 r2 -eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True -eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True -eqCanRewriteFR _ _ = False - -eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool --- Is it /possible/ that fr1 can rewrite fr2? --- This is used when deciding which inerts to kick out, --- at which time a [WD] inert may be split into [W] and [D] -eqMayRewriteFR (Wanted WDeriv, NomEq) (Wanted WDeriv, NomEq) = True -eqMayRewriteFR (Derived, NomEq) (Wanted WDeriv, NomEq) = True -eqMayRewriteFR fr1 fr2 = eqCanRewriteFR fr1 fr2 - ------------------ -{- Note [funEqCanDischarge] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have two CFunEqCans with the same LHS: - (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2) -Can we drop x2 in favour of x1, either unifying -f2 (if it's a flatten meta-var) or adding a new Given -(f1 ~ f2), if x2 is a Given? - -Answer: yes if funEqCanDischarge is true. --} - -funEqCanDischarge - :: CtEvidence -> CtEvidence - -> ( SwapFlag -- NotSwapped => lhs can discharge rhs - -- Swapped => rhs can discharge lhs - , Bool) -- True <=> upgrade non-discharded one - -- from [W] to [WD] --- See Note [funEqCanDischarge] -funEqCanDischarge ev1 ev2 - = ASSERT2( ctEvEqRel ev1 == NomEq, ppr ev1 ) - ASSERT2( ctEvEqRel ev2 == NomEq, ppr ev2 ) - -- CFunEqCans are all Nominal, hence asserts - funEqCanDischargeF (ctEvFlavour ev1) (ctEvFlavour ev2) - -funEqCanDischargeF :: CtFlavour -> CtFlavour -> (SwapFlag, Bool) -funEqCanDischargeF Given _ = (NotSwapped, False) -funEqCanDischargeF _ Given = (IsSwapped, False) -funEqCanDischargeF (Wanted WDeriv) _ = (NotSwapped, False) -funEqCanDischargeF _ (Wanted WDeriv) = (IsSwapped, True) -funEqCanDischargeF (Wanted WOnly) (Wanted WOnly) = (NotSwapped, False) -funEqCanDischargeF (Wanted WOnly) Derived = (NotSwapped, True) -funEqCanDischargeF Derived (Wanted WOnly) = (IsSwapped, True) -funEqCanDischargeF Derived Derived = (NotSwapped, False) - - -{- Note [eqCanDischarge] -~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have two identical CTyEqCan equality constraints -(i.e. both LHS and RHS are the same) - (x1:a~t) `eqCanDischarge` (xs:a~t) -Can we just drop x2 in favour of x1? - -Answer: yes if eqCanDischarge is true. - -Note that we do /not/ allow Wanted to discharge Derived. -We must keep both. Why? Because the Derived may rewrite -other Deriveds in the model whereas the Wanted cannot. - -However a Wanted can certainly discharge an identical Wanted. So -eqCanDischarge does /not/ define a can-rewrite relation in the -sense of Definition [Can-rewrite relation] in TcSMonad. - -We /do/ say that a [W] can discharge a [WD]. In evidence terms it -certainly can, and the /caller/ arranges that the otherwise-lost [D] -is spat out as a new Derived. -} - -eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool --- See Note [eqCanDischarge] -eqCanDischargeFR (f1,r1) (f2, r2) = eqCanRewrite r1 r2 - && eqCanDischargeF f1 f2 - -eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool -eqCanDischargeF Given _ = True -eqCanDischargeF (Wanted _) (Wanted _) = True -eqCanDischargeF (Wanted WDeriv) Derived = True -eqCanDischargeF Derived Derived = True -eqCanDischargeF _ _ = False - - -{- -************************************************************************ -* * - SubGoalDepth -* * -************************************************************************ - -Note [SubGoalDepth] -~~~~~~~~~~~~~~~~~~~ -The 'SubGoalDepth' takes care of stopping the constraint solver from looping. - -The counter starts at zero and increases. It includes dictionary constraints, -equality simplification, and type family reduction. (Why combine these? Because -it's actually quite easy to mistake one for another, in sufficiently involved -scenarios, like ConstraintKinds.) - -The flag -fcontext-stack=n (not very well named!) fixes the maximium -level. - -* The counter includes the depth of type class instance declarations. Example: - [W] d{7} : Eq [Int] - That is d's dictionary-constraint depth is 7. If we use the instance - $dfEqList :: Eq a => Eq [a] - to simplify it, we get - d{7} = $dfEqList d'{8} - where d'{8} : Eq Int, and d' has depth 8. - - For civilised (decidable) instance declarations, each increase of - depth removes a type constructor from the type, so the depth never - gets big; i.e. is bounded by the structural depth of the type. - -* The counter also increments when resolving -equalities involving type functions. Example: - Assume we have a wanted at depth 7: - [W] d{7} : F () ~ a - If there is a type function equation "F () = Int", this would be rewritten to - [W] d{8} : Int ~ a - and remembered as having depth 8. - - Again, without UndecidableInstances, this counter is bounded, but without it - can resolve things ad infinitum. Hence there is a maximum level. - -* Lastly, every time an equality is rewritten, the counter increases. Again, - rewriting an equality constraint normally makes progress, but it's possible - the "progress" is just the reduction of an infinitely-reducing type family. - Hence we need to track the rewrites. - -When compiling a program requires a greater depth, then GHC recommends turning -off this check entirely by setting -freduction-depth=0. This is because the -exact number that works is highly variable, and is likely to change even between -minor releases. Because this check is solely to prevent infinite compilation -times, it seems safe to disable it when a user has ascertained that their program -doesn't loop at the type level. - --} - --- | See Note [SubGoalDepth] -newtype SubGoalDepth = SubGoalDepth Int - deriving (Eq, Ord, Outputable) - -initialSubGoalDepth :: SubGoalDepth -initialSubGoalDepth = SubGoalDepth 0 - -bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth -bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1) - -maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth -maxSubGoalDepth (SubGoalDepth n) (SubGoalDepth m) = SubGoalDepth (n `max` m) - -subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool -subGoalDepthExceeded dflags (SubGoalDepth d) - = mkIntWithInf d > reductionDepth dflags - -{- -************************************************************************ -* * - CtLoc -* * -************************************************************************ - -The 'CtLoc' gives information about where a constraint came from. -This is important for decent error message reporting because -dictionaries don't appear in the original source code. -type will evolve... - --} - -data CtLoc = CtLoc { ctl_origin :: CtOrigin - , ctl_env :: TcLclEnv - , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure - , ctl_depth :: !SubGoalDepth } - - -- The TcLclEnv includes particularly - -- source location: tcl_loc :: RealSrcSpan - -- context: tcl_ctxt :: [ErrCtxt] - -- binder stack: tcl_bndrs :: TcBinderStack - -- level: tcl_tclvl :: TcLevel - -mkKindLoc :: TcType -> TcType -- original *types* being compared - -> CtLoc -> CtLoc -mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc) - (KindEqOrigin s1 (Just s2) (ctLocOrigin loc) - (ctLocTypeOrKind_maybe loc)) - --- | Take a CtLoc and moves it to the kind level -toKindLoc :: CtLoc -> CtLoc -toKindLoc loc = loc { ctl_t_or_k = Just KindLevel } - -mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc -mkGivenLoc tclvl skol_info env - = CtLoc { ctl_origin = GivenOrigin skol_info - , ctl_env = env { tcl_tclvl = tclvl } - , ctl_t_or_k = Nothing -- this only matters for error msgs - , ctl_depth = initialSubGoalDepth } - -ctLocEnv :: CtLoc -> TcLclEnv -ctLocEnv = ctl_env - -ctLocLevel :: CtLoc -> TcLevel -ctLocLevel loc = tcl_tclvl (ctLocEnv loc) - -ctLocDepth :: CtLoc -> SubGoalDepth -ctLocDepth = ctl_depth - -ctLocOrigin :: CtLoc -> CtOrigin -ctLocOrigin = ctl_origin - -ctLocSpan :: CtLoc -> RealSrcSpan -ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl - -ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind -ctLocTypeOrKind_maybe = ctl_t_or_k - -setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc -setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (lcl { tcl_loc = loc }) - -bumpCtLocDepth :: CtLoc -> CtLoc -bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d } - -setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc -setCtLocOrigin ctl orig = ctl { ctl_origin = orig } - -updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc -updateCtLocOrigin ctl@(CtLoc { ctl_origin = orig }) upd - = ctl { ctl_origin = upd orig } - -setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc -setCtLocEnv ctl env = ctl { ctl_env = env } - -pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc -pushErrCtxt o err loc@(CtLoc { ctl_env = lcl }) - = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } } - -pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc --- Just add information w/o updating the origin! -pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl }) - = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } } - -{- -************************************************************************ -* * - SkolemInfo -* * -************************************************************************ --} - --- SkolemInfo gives the origin of *given* constraints --- a) type variables are skolemised --- b) an implication constraint is generated -data SkolemInfo - = SigSkol -- A skolem that is created by instantiating - -- a programmer-supplied type signature - -- Location of the binding site is on the TyVar - -- See Note [SigSkol SkolemInfo] - UserTypeCtxt -- What sort of signature - TcType -- Original type signature (before skolemisation) - [(Name,TcTyVar)] -- Maps the original name of the skolemised tyvar - -- to its instantiated version - - | SigTypeSkol UserTypeCtxt - -- like SigSkol, but when we're kind-checking the *type* - -- hence, we have less info - - | ForAllSkol SDoc -- Bound by a user-written "forall". - - | DerivSkol Type -- Bound by a 'deriving' clause; - -- the type is the instance we are trying to derive - - | InstSkol -- Bound at an instance decl - | InstSC TypeSize -- A "given" constraint obtained by superclass selection. - -- If (C ty1 .. tyn) is the largest class from - -- which we made a superclass selection in the chain, - -- then TypeSize = sizeTypes [ty1, .., tyn] - -- See Note [Solving superclass constraints] in TcInstDcls - - | FamInstSkol -- Bound at a family instance decl - | PatSkol -- An existential type variable bound by a pattern for - ConLike -- a data constructor with an existential type. - (HsMatchContext Name) - -- e.g. data T = forall a. Eq a => MkT a - -- f (MkT x) = ... - -- The pattern MkT x will allocate an existential type - -- variable for 'a'. - - | ArrowSkol -- An arrow form (see TcArrows) - - | IPSkol [HsIPName] -- Binding site of an implicit parameter - - | RuleSkol RuleName -- The LHS of a RULE - - | InferSkol [(Name,TcType)] - -- We have inferred a type for these (mutually-recursivive) - -- polymorphic Ids, and are now checking that their RHS - -- constraints are satisfied. - - | BracketSkol -- Template Haskell bracket - - | UnifyForAllSkol -- We are unifying two for-all types - TcType -- The instantiated type *inside* the forall - - | TyConSkol TyConFlavour Name -- bound in a type declaration of the given flavour - - | DataConSkol Name -- bound as an existential in a Haskell98 datacon decl or - -- as any variable in a GADT datacon decl - - | ReifySkol -- Bound during Template Haskell reification - - | QuantCtxtSkol -- Quantified context, e.g. - -- f :: forall c. (forall a. c a => c [a]) => blah - - | UnkSkol -- Unhelpful info (until I improve it) - -instance Outputable SkolemInfo where - ppr = pprSkolInfo - -pprSkolInfo :: SkolemInfo -> SDoc --- Complete the sentence "is a rigid type variable bound by..." -pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty -pprSkolInfo (SigTypeSkol cx) = pprUserTypeCtxt cx -pprSkolInfo (ForAllSkol doc) = quotes doc -pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for" - <+> pprWithCommas ppr ips -pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred) -pprSkolInfo InstSkol = text "the instance declaration" -pprSkolInfo (InstSC n) = text "the instance declaration" <> whenPprDebug (parens (ppr n)) -pprSkolInfo FamInstSkol = text "a family instance declaration" -pprSkolInfo BracketSkol = text "a Template Haskell bracket" -pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name -pprSkolInfo ArrowSkol = text "an arrow form" -pprSkolInfo (PatSkol cl mc) = sep [ pprPatSkolInfo cl - , text "in" <+> pprMatchContext mc ] -pprSkolInfo (InferSkol ids) = hang (text "the inferred type" <> plural ids <+> text "of") - 2 (vcat [ ppr name <+> dcolon <+> ppr ty - | (name,ty) <- ids ]) -pprSkolInfo (UnifyForAllSkol ty) = text "the type" <+> ppr ty -pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaration for" <+> quotes (ppr name) -pprSkolInfo (DataConSkol name)= text "the data constructor" <+> quotes (ppr name) -pprSkolInfo ReifySkol = text "the type being reified" - -pprSkolInfo (QuantCtxtSkol {}) = text "a quantified context" - --- UnkSkol --- For type variables the others are dealt with by pprSkolTvBinding. --- For Insts, these cases should not happen -pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) text "UnkSkol" - -pprSigSkolInfo :: UserTypeCtxt -> TcType -> SDoc --- The type is already tidied -pprSigSkolInfo ctxt ty - = case ctxt of - FunSigCtxt f _ -> vcat [ text "the type signature for:" - , nest 2 (pprPrefixOcc f <+> dcolon <+> ppr ty) ] - PatSynCtxt {} -> pprUserTypeCtxt ctxt -- See Note [Skolem info for pattern synonyms] - _ -> vcat [ pprUserTypeCtxt ctxt <> colon - , nest 2 (ppr ty) ] - -pprPatSkolInfo :: ConLike -> SDoc -pprPatSkolInfo (RealDataCon dc) - = sep [ text "a pattern with constructor:" - , nest 2 $ ppr dc <+> dcolon - <+> pprType (dataConUserType dc) <> comma ] - -- pprType prints forall's regardless of -fprint-explicit-foralls - -- which is what we want here, since we might be saying - -- type variable 't' is bound by ... - -pprPatSkolInfo (PatSynCon ps) - = sep [ text "a pattern with pattern synonym:" - , nest 2 $ ppr ps <+> dcolon - <+> pprPatSynType ps <> comma ] - -{- Note [Skolem info for pattern synonyms] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For pattern synonym SkolemInfo we have - SigSkol (PatSynCtxt p) ty _ -but the type 'ty' is not very helpful. The full pattern-synonym type -has the provided and required pieces, which it is inconvenient to -record and display here. So we simply don't display the type at all, -contenting outselves with just the name of the pattern synonym, which -is fine. We could do more, but it doesn't seem worth it. - -Note [SigSkol SkolemInfo] -~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we (deeply) skolemise a type - f :: forall a. a -> forall b. b -> a -Then we'll instantiate [a :-> a', b :-> b'], and with the instantiated - a' -> b' -> a. -But when, in an error message, we report that "b is a rigid type -variable bound by the type signature for f", we want to show the foralls -in the right place. So we proceed as follows: - -* In SigSkol we record - - the original signature forall a. a -> forall b. b -> a - - the instantiation mapping [a :-> a', b :-> b'] - -* Then when tidying in TcMType.tidySkolemInfo, we first tidy a' to - whatever it tidies to, say a''; and then we walk over the type - replacing the binder a by the tidied version a'', to give - forall a''. a'' -> forall b''. b'' -> a'' - We need to do this under function arrows, to match what deeplySkolemise - does. - -* Typically a'' will have a nice pretty name like "a", but the point is - that the foral-bound variables of the signature we report line up with - the instantiated skolems lying around in other types. - - -************************************************************************ -* * - CtOrigin -* * -************************************************************************ --} - -data CtOrigin - = GivenOrigin SkolemInfo - - -- All the others are for *wanted* constraints - | OccurrenceOf Name -- Occurrence of an overloaded identifier - | OccurrenceOfRecSel RdrName -- Occurrence of a record selector - | AppOrigin -- An application of some kind - - | SpecPragOrigin UserTypeCtxt -- Specialisation pragma for - -- function or instance - - | TypeEqOrigin { uo_actual :: TcType - , uo_expected :: TcType - , uo_thing :: Maybe SDoc - -- ^ The thing that has type "actual" - , uo_visible :: Bool - -- ^ Is at least one of the three elements above visible? - -- (Errors from the polymorphic subsumption check are considered - -- visible.) Only used for prioritizing error messages. - } - - | KindEqOrigin -- See Note [Equalities with incompatible kinds] in TcCanonical. - TcType (Maybe TcType) -- A kind equality arising from unifying these two types - CtOrigin -- originally arising from this - (Maybe TypeOrKind) -- the level of the eq this arises from - - | IPOccOrigin HsIPName -- Occurrence of an implicit parameter - | OverLabelOrigin FastString -- Occurrence of an overloaded label - - | LiteralOrigin (HsOverLit GhcRn) -- Occurrence of a literal - | NegateOrigin -- Occurrence of syntactic negation - - | ArithSeqOrigin (ArithSeqInfo GhcRn) -- [x..], [x..y] etc - | AssocFamPatOrigin -- When matching the patterns of an associated - -- family instance with that of its parent class - | SectionOrigin - | TupleOrigin -- (..,..) - | ExprSigOrigin -- e :: ty - | PatSigOrigin -- p :: ty - | PatOrigin -- Instantiating a polytyped pattern at a constructor - | ProvCtxtOrigin -- The "provided" context of a pattern synonym signature - (PatSynBind GhcRn GhcRn) -- Information about the pattern synonym, in - -- particular the name and the right-hand side - | RecordUpdOrigin - | ViewPatOrigin - - | ScOrigin TypeSize -- Typechecking superclasses of an instance declaration - -- If the instance head is C ty1 .. tyn - -- then TypeSize = sizeTypes [ty1, .., tyn] - -- See Note [Solving superclass constraints] in TcInstDcls - - | DerivClauseOrigin -- Typechecking a deriving clause (as opposed to - -- standalone deriving). - | DerivOriginDC DataCon Int Bool - -- Checking constraints arising from this data con and field index. The - -- Bool argument in DerivOriginDC and DerivOriginCoerce is True if - -- standalong deriving (with a wildcard constraint) is being used. This - -- is used to inform error messages on how to recommended fixes (e.g., if - -- the argument is True, then don't recommend "use standalone deriving", - -- but rather "fill in the wildcard constraint yourself"). - -- See Note [Inferring the instance context] in TcDerivInfer - | DerivOriginCoerce Id Type Type Bool - -- DerivOriginCoerce id ty1 ty2: Trying to coerce class method `id` from - -- `ty1` to `ty2`. - | StandAloneDerivOrigin -- Typechecking stand-alone deriving. Useful for - -- constraints coming from a wildcard constraint, - -- e.g., deriving instance _ => Eq (Foo a) - -- See Note [Inferring the instance context] - -- in TcDerivInfer - | DefaultOrigin -- Typechecking a default decl - | DoOrigin -- Arising from a do expression - | DoPatOrigin (LPat GhcRn) -- Arising from a failable pattern in - -- a do expression - | MCompOrigin -- Arising from a monad comprehension - | MCompPatOrigin (LPat GhcRn) -- Arising from a failable pattern in a - -- monad comprehension - | IfOrigin -- Arising from an if statement - | ProcOrigin -- Arising from a proc expression - | AnnOrigin -- An annotation - - | FunDepOrigin1 -- A functional dependency from combining - PredType CtLoc -- This constraint arising from ... - PredType CtLoc -- and this constraint arising from ... - - | FunDepOrigin2 -- A functional dependency from combining - PredType CtOrigin -- This constraint arising from ... - PredType SrcSpan -- and this top-level instance - -- We only need a CtOrigin on the first, because the location - -- is pinned on the entire error message - - | HoleOrigin - | UnboundOccurrenceOf OccName - | ListOrigin -- An overloaded list - | StaticOrigin -- A static form - | FailablePattern (LPat GhcTcId) -- A failable pattern in do-notation for the - -- MonadFail Proposal (MFP). Obsolete when - -- actual desugaring to MonadFail.fail is - -- live. - | Shouldn'tHappenOrigin String - -- the user should never see this one, - -- unless ImpredicativeTypes is on, where all - -- bets are off - | InstProvidedOrigin Module ClsInst - -- Skolem variable arose when we were testing if an instance - -- is solvable or not. - --- | Flag to see whether we're type-checking terms or kind-checking types -data TypeOrKind = TypeLevel | KindLevel - deriving Eq - -instance Outputable TypeOrKind where - ppr TypeLevel = text "TypeLevel" - ppr KindLevel = text "KindLevel" - -isTypeLevel :: TypeOrKind -> Bool -isTypeLevel TypeLevel = True -isTypeLevel KindLevel = False - -isKindLevel :: TypeOrKind -> Bool -isKindLevel TypeLevel = False -isKindLevel KindLevel = True - --- An origin is visible if the place where the constraint arises is manifest --- in user code. Currently, all origins are visible except for invisible --- TypeEqOrigins. This is used when choosing which error of --- several to report -isVisibleOrigin :: CtOrigin -> Bool -isVisibleOrigin (TypeEqOrigin { uo_visible = vis }) = vis -isVisibleOrigin (KindEqOrigin _ _ sub_orig _) = isVisibleOrigin sub_orig -isVisibleOrigin _ = True - --- Converts a visible origin to an invisible one, if possible. Currently, --- this works only for TypeEqOrigin -toInvisibleOrigin :: CtOrigin -> CtOrigin -toInvisibleOrigin orig@(TypeEqOrigin {}) = orig { uo_visible = False } -toInvisibleOrigin orig = orig - -instance Outputable CtOrigin where - ppr = pprCtOrigin - -ctoHerald :: SDoc -ctoHerald = text "arising from" - --- | Extract a suitable CtOrigin from a HsExpr -lexprCtOrigin :: LHsExpr GhcRn -> CtOrigin -lexprCtOrigin (L _ e) = exprCtOrigin e - -exprCtOrigin :: HsExpr GhcRn -> CtOrigin -exprCtOrigin (HsVar _ (L _ name)) = OccurrenceOf name -exprCtOrigin (HsUnboundVar _ uv) = UnboundOccurrenceOf (unboundVarOcc uv) -exprCtOrigin (HsConLikeOut {}) = panic "exprCtOrigin HsConLikeOut" -exprCtOrigin (HsRecFld _ f) = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f) -exprCtOrigin (HsOverLabel _ _ l) = OverLabelOrigin l -exprCtOrigin (HsIPVar _ ip) = IPOccOrigin ip -exprCtOrigin (HsOverLit _ lit) = LiteralOrigin lit -exprCtOrigin (HsLit {}) = Shouldn'tHappenOrigin "concrete literal" -exprCtOrigin (HsLam _ matches) = matchesCtOrigin matches -exprCtOrigin (HsLamCase _ ms) = matchesCtOrigin ms -exprCtOrigin (HsApp _ e1 _) = lexprCtOrigin e1 -exprCtOrigin (HsAppType _ e1 _) = lexprCtOrigin e1 -exprCtOrigin (OpApp _ _ op _) = lexprCtOrigin op -exprCtOrigin (NegApp _ e _) = lexprCtOrigin e -exprCtOrigin (HsPar _ e) = lexprCtOrigin e -exprCtOrigin (SectionL _ _ _) = SectionOrigin -exprCtOrigin (SectionR _ _ _) = SectionOrigin -exprCtOrigin (ExplicitTuple {}) = Shouldn'tHappenOrigin "explicit tuple" -exprCtOrigin ExplicitSum{} = Shouldn'tHappenOrigin "explicit sum" -exprCtOrigin (HsCase _ _ matches) = matchesCtOrigin matches -exprCtOrigin (HsIf _ (Just syn) _ _ _) = exprCtOrigin (syn_expr syn) -exprCtOrigin (HsIf {}) = Shouldn'tHappenOrigin "if expression" -exprCtOrigin (HsMultiIf _ rhs) = lGRHSCtOrigin rhs -exprCtOrigin (HsLet _ _ e) = lexprCtOrigin e -exprCtOrigin (HsDo {}) = DoOrigin -exprCtOrigin (ExplicitList {}) = Shouldn'tHappenOrigin "list" -exprCtOrigin (RecordCon {}) = Shouldn'tHappenOrigin "record construction" -exprCtOrigin (RecordUpd {}) = Shouldn'tHappenOrigin "record update" -exprCtOrigin (ExprWithTySig {}) = ExprSigOrigin -exprCtOrigin (ArithSeq {}) = Shouldn'tHappenOrigin "arithmetic sequence" -exprCtOrigin (HsSCC _ _ _ e) = lexprCtOrigin e -exprCtOrigin (HsCoreAnn _ _ _ e) = lexprCtOrigin e -exprCtOrigin (HsBracket {}) = Shouldn'tHappenOrigin "TH bracket" -exprCtOrigin (HsRnBracketOut {})= Shouldn'tHappenOrigin "HsRnBracketOut" -exprCtOrigin (HsTcBracketOut {})= panic "exprCtOrigin HsTcBracketOut" -exprCtOrigin (HsSpliceE {}) = Shouldn'tHappenOrigin "TH splice" -exprCtOrigin (HsProc {}) = Shouldn'tHappenOrigin "proc" -exprCtOrigin (HsStatic {}) = Shouldn'tHappenOrigin "static expression" -exprCtOrigin (HsTick _ _ e) = lexprCtOrigin e -exprCtOrigin (HsBinTick _ _ _ e) = lexprCtOrigin e -exprCtOrigin (HsTickPragma _ _ _ _ e) = lexprCtOrigin e -exprCtOrigin (HsWrap {}) = panic "exprCtOrigin HsWrap" -exprCtOrigin (XExpr nec) = noExtCon nec - --- | Extract a suitable CtOrigin from a MatchGroup -matchesCtOrigin :: MatchGroup GhcRn (LHsExpr GhcRn) -> CtOrigin -matchesCtOrigin (MG { mg_alts = alts }) - | L _ [L _ match] <- alts - , Match { m_grhss = grhss } <- match - = grhssCtOrigin grhss - - | otherwise - = Shouldn'tHappenOrigin "multi-way match" -matchesCtOrigin (XMatchGroup nec) = noExtCon nec - --- | Extract a suitable CtOrigin from guarded RHSs -grhssCtOrigin :: GRHSs GhcRn (LHsExpr GhcRn) -> CtOrigin -grhssCtOrigin (GRHSs { grhssGRHSs = lgrhss }) = lGRHSCtOrigin lgrhss -grhssCtOrigin (XGRHSs nec) = noExtCon nec - --- | Extract a suitable CtOrigin from a list of guarded RHSs -lGRHSCtOrigin :: [LGRHS GhcRn (LHsExpr GhcRn)] -> CtOrigin -lGRHSCtOrigin [L _ (GRHS _ _ (L _ e))] = exprCtOrigin e -lGRHSCtOrigin [L _ (XGRHS nec)] = noExtCon nec -lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS" - -pprCtLoc :: CtLoc -> SDoc --- "arising from ... at ..." --- Not an instance of Outputable because of the "arising from" prefix -pprCtLoc (CtLoc { ctl_origin = o, ctl_env = lcl}) - = sep [ pprCtOrigin o - , text "at" <+> ppr (tcl_loc lcl)] - -pprCtOrigin :: CtOrigin -> SDoc --- "arising from ..." --- Not an instance of Outputable because of the "arising from" prefix -pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk - -pprCtOrigin (SpecPragOrigin ctxt) - = case ctxt of - FunSigCtxt n _ -> text "a SPECIALISE pragma for" <+> quotes (ppr n) - SpecInstCtxt -> text "a SPECIALISE INSTANCE pragma" - _ -> text "a SPECIALISE pragma" -- Never happens I think - -pprCtOrigin (FunDepOrigin1 pred1 loc1 pred2 loc2) - = hang (ctoHerald <+> text "a functional dependency between constraints:") - 2 (vcat [ hang (quotes (ppr pred1)) 2 (pprCtLoc loc1) - , hang (quotes (ppr pred2)) 2 (pprCtLoc loc2) ]) - -pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2) - = hang (ctoHerald <+> text "a functional dependency between:") - 2 (vcat [ hang (text "constraint" <+> quotes (ppr pred1)) - 2 (pprCtOrigin orig1 ) - , hang (text "instance" <+> quotes (ppr pred2)) - 2 (text "at" <+> ppr loc2) ]) - -pprCtOrigin (KindEqOrigin t1 (Just t2) _ _) - = hang (ctoHerald <+> text "a kind equality arising from") - 2 (sep [ppr t1, char '~', ppr t2]) - -pprCtOrigin AssocFamPatOrigin - = text "when matching a family LHS with its class instance head" - -pprCtOrigin (KindEqOrigin t1 Nothing _ _) - = hang (ctoHerald <+> text "a kind equality when matching") - 2 (ppr t1) - -pprCtOrigin (UnboundOccurrenceOf name) - = ctoHerald <+> text "an undeclared identifier" <+> quotes (ppr name) - -pprCtOrigin (DerivOriginDC dc n _) - = hang (ctoHerald <+> text "the" <+> speakNth n - <+> text "field of" <+> quotes (ppr dc)) - 2 (parens (text "type" <+> quotes (ppr ty))) - where - ty = dataConOrigArgTys dc !! (n-1) - -pprCtOrigin (DerivOriginCoerce meth ty1 ty2 _) - = hang (ctoHerald <+> text "the coercion of the method" <+> quotes (ppr meth)) - 2 (sep [ text "from type" <+> quotes (ppr ty1) - , nest 2 $ text "to type" <+> quotes (ppr ty2) ]) - -pprCtOrigin (DoPatOrigin pat) - = ctoHerald <+> text "a do statement" - $$ - text "with the failable pattern" <+> quotes (ppr pat) - -pprCtOrigin (MCompPatOrigin pat) - = ctoHerald <+> hsep [ text "the failable pattern" - , quotes (ppr pat) - , text "in a statement in a monad comprehension" ] -pprCtOrigin (FailablePattern pat) - = ctoHerald <+> text "the failable pattern" <+> quotes (ppr pat) - $$ - text "(this will become an error in a future GHC release)" - -pprCtOrigin (Shouldn'tHappenOrigin note) - = sdocWithDynFlags $ \dflags -> - if xopt LangExt.ImpredicativeTypes dflags - then text "a situation created by impredicative types" - else - vcat [ text "<< This should not appear in error messages. If you see this" - , text "in an error message, please report a bug mentioning" <+> quotes (text note) <+> text "at" - , text "https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug >>" ] - -pprCtOrigin (ProvCtxtOrigin PSB{ psb_id = (L _ name) }) - = hang (ctoHerald <+> text "the \"provided\" constraints claimed by") - 2 (text "the signature of" <+> quotes (ppr name)) - -pprCtOrigin (InstProvidedOrigin mod cls_inst) - = vcat [ text "arising when attempting to show that" - , ppr cls_inst - , text "is provided by" <+> quotes (ppr mod)] - -pprCtOrigin simple_origin - = ctoHerald <+> pprCtO simple_origin - --- | Short one-liners -pprCtO :: CtOrigin -> SDoc -pprCtO (OccurrenceOf name) = hsep [text "a use of", quotes (ppr name)] -pprCtO (OccurrenceOfRecSel name) = hsep [text "a use of", quotes (ppr name)] -pprCtO AppOrigin = text "an application" -pprCtO (IPOccOrigin name) = hsep [text "a use of implicit parameter", quotes (ppr name)] -pprCtO (OverLabelOrigin l) = hsep [text "the overloaded label" - ,quotes (char '#' <> ppr l)] -pprCtO RecordUpdOrigin = text "a record update" -pprCtO ExprSigOrigin = text "an expression type signature" -pprCtO PatSigOrigin = text "a pattern type signature" -pprCtO PatOrigin = text "a pattern" -pprCtO ViewPatOrigin = text "a view pattern" -pprCtO IfOrigin = text "an if expression" -pprCtO (LiteralOrigin lit) = hsep [text "the literal", quotes (ppr lit)] -pprCtO (ArithSeqOrigin seq) = hsep [text "the arithmetic sequence", quotes (ppr seq)] -pprCtO SectionOrigin = text "an operator section" -pprCtO AssocFamPatOrigin = text "the LHS of a famly instance" -pprCtO TupleOrigin = text "a tuple" -pprCtO NegateOrigin = text "a use of syntactic negation" -pprCtO (ScOrigin n) = text "the superclasses of an instance declaration" - <> whenPprDebug (parens (ppr n)) -pprCtO DerivClauseOrigin = text "the 'deriving' clause of a data type declaration" -pprCtO StandAloneDerivOrigin = text "a 'deriving' declaration" -pprCtO DefaultOrigin = text "a 'default' declaration" -pprCtO DoOrigin = text "a do statement" -pprCtO MCompOrigin = text "a statement in a monad comprehension" -pprCtO ProcOrigin = text "a proc expression" -pprCtO (TypeEqOrigin t1 t2 _ _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2] -pprCtO AnnOrigin = text "an annotation" -pprCtO HoleOrigin = text "a use of" <+> quotes (text "_") -pprCtO ListOrigin = text "an overloaded list" -pprCtO StaticOrigin = text "a static form" -pprCtO _ = panic "pprCtOrigin" - -{- Constraint Solver Plugins ------------------------- -} |