diff options
66 files changed, 3071 insertions, 2892 deletions
diff --git a/compiler/GHC/StgToCmm/Ticky.hs b/compiler/GHC/StgToCmm/Ticky.hs index 06ef520c0d..7548f3de13 100644 --- a/compiler/GHC/StgToCmm/Ticky.hs +++ b/compiler/GHC/StgToCmm/Ticky.hs @@ -131,8 +131,8 @@ import DynFlags -- Turgid imports for showTypeCategory import PrelNames import TcType -import Type import TyCon +import Predicate import Data.Maybe import qualified Data.Char diff --git a/compiler/basicTypes/BasicTypes.hs b/compiler/basicTypes/BasicTypes.hs index 43ad2cbbba..6e18180d1c 100644 --- a/compiler/basicTypes/BasicTypes.hs +++ b/compiler/basicTypes/BasicTypes.hs @@ -106,7 +106,9 @@ module BasicTypes( IntWithInf, infinity, treatZeroAsInf, mkIntWithInf, intGtLimit, - SpliceExplicitFlag(..) + SpliceExplicitFlag(..), + + TypeOrKind(..), isTypeLevel, isKindLevel ) where import GhcPrelude @@ -1644,3 +1646,25 @@ data SpliceExplicitFlag = ExplicitSplice | -- ^ <=> $(f x y) ImplicitSplice -- ^ <=> f x y, i.e. a naked top level expression deriving Data + +{- ********************************************************************* +* * + Types vs Kinds +* * +********************************************************************* -} + +-- | 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 diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs index 690ed6854f..47eb7a838b 100644 --- a/compiler/basicTypes/DataCon.hs +++ b/compiler/basicTypes/DataCon.hs @@ -73,6 +73,7 @@ import FieldLabel import Class import Name import PrelNames +import Predicate import Var import VarSet( emptyVarSet ) import Outputable diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs index 4dceb4bc03..8c62cc9944 100644 --- a/compiler/basicTypes/Id.hs +++ b/compiler/basicTypes/Id.hs @@ -73,9 +73,6 @@ module Id ( isConLikeId, isBottomingId, idIsFrom, hasNoBinding, - -- ** Evidence variables - DictId, isDictId, isEvVar, - -- ** Join variables JoinId, isJoinId, isJoinId_maybe, idJoinArity, asJoinId, asJoinId_maybe, zapJoinId, @@ -129,7 +126,7 @@ import IdInfo import BasicTypes -- Imported and re-exported -import Var( Id, CoVar, DictId, JoinId, +import Var( Id, CoVar, JoinId, InId, InVar, OutId, OutVar, idInfo, idDetails, setIdDetails, globaliseId, varType, @@ -587,20 +584,6 @@ isDeadBinder bndr | isId bndr = isDeadOcc (idOccInfo bndr) {- ************************************************************************ * * - Evidence variables -* * -************************************************************************ --} - -isEvVar :: Var -> Bool -isEvVar var = isEvVarType (varType var) - -isDictId :: Id -> Bool -isDictId id = isDictTy (idType id) - -{- -************************************************************************ -* * Join variables * * ************************************************************************ diff --git a/compiler/basicTypes/Predicate.hs b/compiler/basicTypes/Predicate.hs new file mode 100644 index 0000000000..dab4e64a52 --- /dev/null +++ b/compiler/basicTypes/Predicate.hs @@ -0,0 +1,228 @@ +{- + +Describes predicates as they are considered by the solver. + +-} + +module Predicate ( + Pred(..), classifyPredType, + isPredTy, isEvVarType, + + -- Equality predicates + EqRel(..), eqRelRole, + isEqPrimPred, isEqPred, + getEqPredTys, getEqPredTys_maybe, getEqPredRole, + predTypeEqRel, + mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole, + mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, + + -- Class predicates + mkClassPred, isDictTy, + isClassPred, isEqPredClass, isCTupleClass, + getClassPredTys, getClassPredTys_maybe, + + -- Implicit parameters + isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, hasIPPred, + + -- Evidence variables + DictId, isEvVar, isDictId + ) where + +import GhcPrelude + +import Type +import Class +import TyCon +import Var +import Coercion + +import PrelNames + +import FastString +import Outputable +import Util + +import Control.Monad ( guard ) + +-- | A predicate in the solver. The solver tries to prove Wanted predicates +-- from Given ones. +data Pred + = ClassPred Class [Type] + | EqPred EqRel Type Type + | IrredPred PredType + | ForAllPred [TyCoVarBinder] [PredType] PredType + -- ForAllPred: see Note [Quantified constraints] in TcCanonical + -- NB: There is no TuplePred case + -- Tuple predicates like (Eq a, Ord b) are just treated + -- as ClassPred, as if we had a tuple class with two superclasses + -- class (c1, c2) => (%,%) c1 c2 + +classifyPredType :: PredType -> Pred +classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of + Just (tc, [_, _, ty1, ty2]) + | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2 + | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2 + + Just (tc, tys) + | Just clas <- tyConClass_maybe tc + -> ClassPred clas tys + + _ | (tvs, rho) <- splitForAllVarBndrs ev_ty + , (theta, pred) <- splitFunTys rho + , not (null tvs && null theta) + -> ForAllPred tvs theta pred + + | otherwise + -> IrredPred ev_ty + +-- --------------------- Dictionary types --------------------------------- + +mkClassPred :: Class -> [Type] -> PredType +mkClassPred clas tys = mkTyConApp (classTyCon clas) tys + +isDictTy :: Type -> Bool +isDictTy = isClassPred + +getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type]) +getClassPredTys ty = case getClassPredTys_maybe ty of + Just (clas, tys) -> (clas, tys) + Nothing -> pprPanic "getClassPredTys" (ppr ty) + +getClassPredTys_maybe :: PredType -> Maybe (Class, [Type]) +getClassPredTys_maybe ty = case splitTyConApp_maybe ty of + Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys) + _ -> Nothing + +-- --------------------- Equality predicates --------------------------------- + +-- | A choice of equality relation. This is separate from the type 'Role' +-- because 'Phantom' does not define a (non-trivial) equality relation. +data EqRel = NomEq | ReprEq + deriving (Eq, Ord) + +instance Outputable EqRel where + ppr NomEq = text "nominal equality" + ppr ReprEq = text "representational equality" + +eqRelRole :: EqRel -> Role +eqRelRole NomEq = Nominal +eqRelRole ReprEq = Representational + +getEqPredTys :: PredType -> (Type, Type) +getEqPredTys ty + = case splitTyConApp_maybe ty of + Just (tc, [_, _, ty1, ty2]) + | tc `hasKey` eqPrimTyConKey + || tc `hasKey` eqReprPrimTyConKey + -> (ty1, ty2) + _ -> pprPanic "getEqPredTys" (ppr ty) + +getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type) +getEqPredTys_maybe ty + = case splitTyConApp_maybe ty of + Just (tc, [_, _, ty1, ty2]) + | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2) + | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2) + _ -> Nothing + +getEqPredRole :: PredType -> Role +getEqPredRole ty = eqRelRole (predTypeEqRel ty) + +-- | Get the equality relation relevant for a pred type. +predTypeEqRel :: PredType -> EqRel +predTypeEqRel ty + | Just (tc, _) <- splitTyConApp_maybe ty + , tc `hasKey` eqReprPrimTyConKey + = ReprEq + | otherwise + = NomEq + +{------------------------------------------- +Predicates on PredType +--------------------------------------------} + +{- +Note [Evidence for quantified constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The superclass mechanism in TcCanonical.makeSuperClasses risks +taking a quantified constraint like + (forall a. C a => a ~ b) +and generate superclass evidence + (forall a. C a => a ~# b) + +This is a funny thing: neither isPredTy nor isCoVarType are true +of it. So we are careful not to generate it in the first place: +see Note [Equality superclasses in quantified constraints] +in TcCanonical. +-} + +isEvVarType :: Type -> Bool +-- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b) +-- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2) +-- See Note [Types for coercions, predicates, and evidence] in TyCoRep +-- See Note [Evidence for quantified constraints] +isEvVarType ty = isCoVarType ty || isPredTy ty + +isEqPredClass :: Class -> Bool +-- True of (~) and (~~) +isEqPredClass cls = cls `hasKey` eqTyConKey + || cls `hasKey` heqTyConKey + +isClassPred, isEqPred, isEqPrimPred, isIPPred :: PredType -> Bool +isClassPred ty = case tyConAppTyCon_maybe ty of + Just tyCon | isClassTyCon tyCon -> True + _ -> False + +isEqPred ty -- True of (a ~ b) and (a ~~ b) + -- ToDo: should we check saturation? + | Just tc <- tyConAppTyCon_maybe ty + , Just cls <- tyConClass_maybe tc + = isEqPredClass cls + | otherwise + = False + +isEqPrimPred ty = isCoVarType ty + -- True of (a ~# b) (a ~R# b) + +isIPPred ty = case tyConAppTyCon_maybe ty of + Just tc -> isIPTyCon tc + _ -> False + +isIPTyCon :: TyCon -> Bool +isIPTyCon tc = tc `hasKey` ipClassKey + -- Class and its corresponding TyCon have the same Unique + +isIPClass :: Class -> Bool +isIPClass cls = cls `hasKey` ipClassKey + +isCTupleClass :: Class -> Bool +isCTupleClass cls = isTupleTyCon (classTyCon cls) + +isIPPred_maybe :: Type -> Maybe (FastString, Type) +isIPPred_maybe ty = + do (tc,[t1,t2]) <- splitTyConApp_maybe ty + guard (isIPTyCon tc) + x <- isStrLitTy t1 + return (x,t2) + +hasIPPred :: PredType -> Bool +hasIPPred pred + = case classifyPredType pred of + ClassPred cls tys + | isIPClass cls -> True + | isCTupleClass cls -> any hasIPPred tys + _other -> False + +{- +************************************************************************ +* * + Evidence variables +* * +************************************************************************ +-} + +isEvVar :: Var -> Bool +isEvVar var = isEvVarType (varType var) + +isDictId :: Id -> Bool +isDictId id = isDictTy (varType id) diff --git a/compiler/coreSyn/CoreArity.hs b/compiler/coreSyn/CoreArity.hs index d8497322a1..d940d9d69c 100644 --- a/compiler/coreSyn/CoreArity.hs +++ b/compiler/coreSyn/CoreArity.hs @@ -30,6 +30,7 @@ import VarEnv import Id import Type import TyCon ( initRecTc, checkRecTc ) +import Predicate ( isDictTy ) import Coercion import BasicTypes import Unique @@ -517,7 +518,7 @@ mk_cheap_fn dflags cheap_app = \e mb_ty -> exprIsCheapX cheap_app e || case mb_ty of Nothing -> False - Just ty -> isDictLikeTy ty + Just ty -> isDictTy ty ---------------------- @@ -624,9 +625,6 @@ The (foo DInt) is floated out, and makes ineffective a RULE One could go further and make exprIsCheap reply True to any dictionary-typed expression, but that's more work. -See Note [Dictionary-like types] in TcType.hs for why we use -isDictLikeTy here rather than isDictTy - Note [Eta expanding thunks] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ We don't eta-expand diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs index 95aae22b58..1ca5a6b438 100644 --- a/compiler/coreSyn/CoreUtils.hs +++ b/compiler/coreSyn/CoreUtils.hs @@ -77,6 +77,7 @@ import Id import IdInfo import PrelNames( absentErrorIdKey ) import Type +import Predicate import TyCoRep( TyCoBinder(..), TyBinder ) import Coercion import TyCon diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index 95c26b90e0..6498ed7f6f 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -41,6 +41,7 @@ import CoreArity ( etaExpand ) import CoreUnfold import CoreFVs import Digraph +import Predicate import PrelNames import TyCon diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index 3ff27ea098..4737d13c0b 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -214,6 +214,7 @@ Library Hooks Id IdInfo + Predicate Lexeme Literal Llvm @@ -505,6 +506,8 @@ Library TcRnExports TcRnMonad TcRnTypes + Constraint + TcOrigin TcRules TcSimplify TcHoleErrors diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs index dc336e3914..d35adf8f4f 100644 --- a/compiler/main/GHC.hs +++ b/compiler/main/GHC.hs @@ -311,6 +311,7 @@ import GhcMonad import TcRnMonad ( finalSafeMode, fixSafeInstances, initIfaceTcRn ) import LoadIface ( loadSysInterface ) import TcRnTypes +import Predicate import Packages import NameSet import RdrName diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs index e7f3947210..04e50ebca8 100644 --- a/compiler/main/InteractiveEval.hs +++ b/compiler/main/InteractiveEval.hs @@ -63,6 +63,9 @@ import TyCon import Type hiding( typeKind ) import RepType import TcType +import Constraint +import TcOrigin +import Predicate import Var import Id import Name hiding ( varName ) diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index 27c7318805..79a30482b0 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -81,6 +81,7 @@ module TysPrim( eqPrimTyCon, -- ty1 ~# ty2 eqReprPrimTyCon, -- ty1 ~R# ty2 (at role Representational) eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom) + equalityTyCon, -- * SIMD #include "primop-vector-tys-exports.hs-incl" @@ -919,6 +920,12 @@ eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName binders res_kind roles res_kind = unboxedTupleKind [] roles = [Nominal, Nominal, Phantom, Phantom] +-- | Given a Role, what TyCon is the type of equality predicates at that role? +equalityTyCon :: Role -> TyCon +equalityTyCon Nominal = eqPrimTyCon +equalityTyCon Representational = eqReprPrimTyCon +equalityTyCon Phantom = eqPhantPrimTyCon + {- ********************************************************************* * * The primitive array types diff --git a/compiler/rename/RnBinds.hs b/compiler/rename/RnBinds.hs index 56caee1a2a..9b93af907b 100644 --- a/compiler/rename/RnBinds.hs +++ b/compiler/rename/RnBinds.hs @@ -49,7 +49,7 @@ import NameSet import RdrName ( RdrName, rdrNameOcc ) import SrcLoc import ListSetOps ( findDupsEq ) -import BasicTypes ( RecFlag(..) ) +import BasicTypes ( RecFlag(..), TypeOrKind(..) ) import Digraph ( SCC(..) ) import Bag import Util diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index ea8cfb5347..791b6a4ceb 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -52,7 +52,7 @@ import NameEnv import Avail import Outputable import Bag -import BasicTypes ( pprRuleName ) +import BasicTypes ( pprRuleName, TypeOrKind(..) ) import FastString import SrcLoc import DynFlags diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index 87f364011e..434ed496f1 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -57,8 +57,9 @@ import FieldLabel import Util import ListSetOps ( deleteBys ) -import BasicTypes ( compareFixity, funTyFixity, negateFixity, - Fixity(..), FixityDirection(..), LexicalFixity(..) ) +import BasicTypes ( compareFixity, funTyFixity, negateFixity + , Fixity(..), FixityDirection(..), LexicalFixity(..) + , TypeOrKind(..) ) import Outputable import FastString import Maybes diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs index e49a40dc0d..75e80d0c46 100644 --- a/compiler/specialise/Specialise.hs +++ b/compiler/specialise/Specialise.hs @@ -16,6 +16,7 @@ import GhcPrelude import Id import TcType hiding( substTy ) import Type hiding( substTy, extendTvSubstList ) +import Predicate import Module( Module, HasModule(..) ) import Coercion( Coercion ) import CoreMonad diff --git a/compiler/stranal/WwLib.hs b/compiler/stranal/WwLib.hs index 5e4d22857a..f8b398fbcd 100644 --- a/compiler/stranal/WwLib.hs +++ b/compiler/stranal/WwLib.hs @@ -30,6 +30,7 @@ import Literal ( absentLiteralOf, rubbishLit ) import VarEnv ( mkInScopeSet ) import VarSet ( VarSet ) import Type +import Predicate ( isClassPred ) import RepType ( isVoidTy, typePrimRep ) import Coercion import FamInstEnv diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs index ee1971345b..d367d1df63 100644 --- a/compiler/typecheck/ClsInst.hs +++ b/compiler/typecheck/ClsInst.hs @@ -17,6 +17,7 @@ import TcType import TcTypeable import TcMType import TcEvidence +import Predicate import RnEnv( addUsedGRE ) import RdrName( lookupGRE_FieldLabel ) import InstEnv diff --git a/compiler/typecheck/Constraint.hs b/compiler/typecheck/Constraint.hs new file mode 100644 index 0000000000..acc335262a --- /dev/null +++ b/compiler/typecheck/Constraint.hs @@ -0,0 +1,1778 @@ +{- + +This module defines types and simple operations over constraints, +as used in the type-checker and constraint solver. + +-} + +{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-} + +module Constraint ( + -- 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(..), implicationPrototype, + ImplicStatus(..), isInsolubleStatus, isSolvedStatus, + SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth, + bumpSubGoalDepth, subGoalDepthExceeded, + CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin, + ctLocTypeOrKind_maybe, + ctLocDepth, bumpCtLocDepth, isGivenLoc, + setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan, + pprCtLoc, + + -- CtEvidence + CtEvidence(..), TcEvDest(..), + mkKindLoc, toKindLoc, mkGivenLoc, + isWanted, isGiven, isDerived, isGivenOrWDeriv, + ctEvRole, + + wrapType, wrapTypeWithImplication, + + CtFlavour(..), ShadowInfo(..), ctEvFlavour, + CtFlavourRole, ctEvFlavourRole, ctFlavourRole, + eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR, + eqCanDischargeFR, + funEqCanDischarge, funEqCanDischargeF, + + -- Pretty printing + pprEvVarTheta, + pprEvVars, pprEvVarWithType, + + -- holes + HoleSort(..), + + ) + where + +#include "HsVersions.h" + +import GhcPrelude + +import {-# SOURCE #-} TcRnTypes ( TcLclEnv, setLclEnvTcLevel, getLclEnvTcLevel + , setLclEnvLoc, getLclEnvLoc ) + +import Predicate +import Type +import Coercion +import Class +import TyCon +import Var +import Id + +import TcType +import TcEvidence +import TcOrigin + +import CoreSyn + +import OccName +import FV +import VarSet +import DynFlags +import BasicTypes + +import Outputable +import SrcLoc +import Bag +import Util + +import Control.Monad ( msum ) + +{- +************************************************************************ +* * +* 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_occ :: OccName, -- The name of this hole + cc_hole :: HoleSort -- The sort of this hole (expr, type, ...) + } + + | 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 + +------------ +-- | Used to indicate which sort of hole we have. +data HoleSort = ExprHole + -- ^ Either an out-of-scope variable or a "true" hole in an + -- expression (TypedHoles) + | TypeHole + -- ^ A hole in a type (PartialTypeSignatures) + +{- Note [Hole constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +CHoleCan constraints are used for two kinds of holes, +distinguished by cc_hole: + + * For holes in expressions + 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_occ = occ } -> text "CHoleCan:" <+> ppr occ + 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 _ orig1 _ _ orig2 _ + | g1 || g2 -> True -- Given/Wanted errors: keep all + | otherwise -> False -- Wanted/Wanted errors: discard + where + g1 = isGivenOrigin orig1 + g2 = isGivenOrigin orig2 + + _ -> 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) + +{- 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 +-- A Hole that does not have a leading underscore is +-- simply an out-of-scope variable, and we treat that +-- a bit differently when it comes to error reporting +isOutOfScopeCt (CHoleCan { cc_occ = occ }) = not (startsWithUnderscore occ) +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_warn_inaccessible :: Bool, + -- True <=> -Winaccessible-code is enabled + -- at construction. See + -- Note [Avoid -Winaccessible-code when deriving] + -- in TcInstDcls + + ic_env :: TcLclEnv, + -- Records the TcLClEnv at the time of creation. + -- + -- The TcLclEnv gives the source location + -- and error context for the implication, and + -- hence for all the given evidence variables. + + 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 + -- See Note [Needed evidence variables] + 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 + } + +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" + , ic_warn_inaccessible = panic "newImplic:warn_inaccessible" + + -- 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 } + +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 -> TcCoercion +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 [The improvement story and derived shadows] in TcSMonad + 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 = setLclEnvTcLevel env 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 = getLclEnvTcLevel (ctLocEnv loc) + +ctLocDepth :: CtLoc -> SubGoalDepth +ctLocDepth = ctl_depth + +ctLocOrigin :: CtLoc -> CtOrigin +ctLocOrigin = ctl_origin + +ctLocSpan :: CtLoc -> RealSrcSpan +ctLocSpan (CtLoc { ctl_env = lcl}) = getLclEnvLoc 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 (setLclEnvLoc lcl 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 } + +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 (getLclEnvLoc lcl)] diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs index 14399df4a6..f8c4124534 100644 --- a/compiler/typecheck/FunDeps.hs +++ b/compiler/typecheck/FunDeps.hs @@ -24,6 +24,7 @@ import GhcPrelude import Name import Var import Class +import Predicate import Type import TcType( transSuperClasses ) import CoAxiom( TypeEqn ) diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 8e180b4cf4..cab0e596c5 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -42,6 +42,9 @@ import FastString import GHC.Hs import TcHsSyn import TcRnMonad +import Constraint +import Predicate +import TcOrigin import TcEnv import TcEvidence import InstEnv @@ -66,6 +69,7 @@ import SrcLoc import DynFlags import Util import Outputable +import BasicTypes ( TypeOrKind(..) ) import qualified GHC.LanguageExtensions as LangExt import Control.Monad( unless ) diff --git a/compiler/typecheck/TcArrows.hs b/compiler/typecheck/TcArrows.hs index 34f1a1fb37..e6c07cf6ba 100644 --- a/compiler/typecheck/TcArrows.hs +++ b/compiler/typecheck/TcArrows.hs @@ -24,6 +24,7 @@ import TcPat import TcUnify import TcRnMonad import TcEnv +import TcOrigin import TcEvidence import Id( mkLocalId ) import Inst diff --git a/compiler/typecheck/TcBackpack.hs b/compiler/typecheck/TcBackpack.hs index bc66834849..17c9ac7e80 100644 --- a/compiler/typecheck/TcBackpack.hs +++ b/compiler/typecheck/TcBackpack.hs @@ -19,7 +19,7 @@ module TcBackpack ( import GhcPrelude -import BasicTypes (defaultFixity) +import BasicTypes (defaultFixity, TypeOrKind(..)) import Packages import TcRnExports import DynFlags @@ -34,6 +34,8 @@ import TcIface import TcMType import TcType import TcSimplify +import Constraint +import TcOrigin import LoadIface import RnNames import ErrUtils diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index e909556e06..dc701d360b 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -27,6 +27,7 @@ import FastString import GHC.Hs import TcSigs import TcRnMonad +import TcOrigin import TcEnv import TcUnify import TcSimplify diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index c2e90c6023..30ea3a9a87 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -13,7 +13,9 @@ module TcCanonical( import GhcPrelude -import TcRnTypes +import Constraint +import Predicate +import TcOrigin import TcUnify( swapOverTyVars, metaTyVarUpdateOK ) import TcType import Type @@ -284,7 +286,7 @@ So here's the plan: Note [Eagerly expand given superclasses]. 3. If we have any remaining unsolved wanteds - (see Note [When superclasses help] in TcRnTypes) + (see Note [When superclasses help] in Constraint) try harder: take both the Givens and Wanteds, and expand superclasses again. See the calls to expandSuperClasses in TcSimplify.simpl_loop and solveWanteds. @@ -617,7 +619,7 @@ case. Instead we have a special case in TcInteract.doTopReactOther, which looks for primitive equalities specially in the quantified constraints. -See also Note [Evidence for quantified constraints] in Type. +See also Note [Evidence for quantified constraints] in Predicate. ************************************************************************ @@ -702,7 +704,7 @@ Here are the moving parts * checkValidType gets some changes to accept forall-constraints only in the right places. - * Type.PredTree gets a new constructor ForAllPred, and + * Predicate.Pred gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forall-constraints @@ -2114,7 +2116,7 @@ Int ~ Int. The user thus sees that GHC can't solve Int ~ Int, which is embarrassing. See #11198 for more tales of destruction. The reason for this odd behavior is much the same as -Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the +Note [Wanteds do not rewrite Wanteds] in Constraint: note that the new `co` is a Wanted. The solution is then not to use `co` to "rewrite" -- that is, cast -- `w`, but diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs index 6f2ef4c292..18e71c8803 100644 --- a/compiler/typecheck/TcClassDcl.hs +++ b/compiler/typecheck/TcClassDcl.hs @@ -30,7 +30,9 @@ import TcBinds import TcUnify import TcHsType import TcMType -import Type ( getClassPredTys_maybe, piResultTys ) +import Type ( piResultTys ) +import Predicate +import TcOrigin import TcType import TcRnMonad import DriverPhases (HscSource(..)) diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 055af76743..ba6dcf773b 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -20,6 +20,8 @@ import DynFlags import TcRnMonad import FamInst +import TcOrigin +import Predicate import TcDerivInfer import TcDerivUtils import TcValidity( allDistinctTyVars ) @@ -617,7 +619,7 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mb_lderiv_strat overlap_mode)) = setSrcSpan loc $ addErrCtxt (standaloneCtxt deriv_ty) $ do { traceTc "Standalone deriving decl for" (ppr deriv_ty) - ; let ctxt = TcType.InstDeclCtxt True + ; let ctxt = TcOrigin.InstDeclCtxt True ; traceTc "Deriving strategy (standalone deriving)" $ vcat [ppr mb_lderiv_strat, ppr deriv_ty] ; (mb_lderiv_strat, via_tvs) <- tcDerivStrategy mb_lderiv_strat diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs index 4bb1c76063..c8ecde4014 100644 --- a/compiler/typecheck/TcDerivInfer.hs +++ b/compiler/typecheck/TcDerivInfer.hs @@ -31,6 +31,9 @@ import TcGenFunctor import TcGenGenerics import TcMType import TcRnMonad +import TcOrigin +import Constraint +import Predicate import TcType import TyCon import Type diff --git a/compiler/typecheck/TcDerivUtils.hs b/compiler/typecheck/TcDerivUtils.hs index ae191f937b..76c42817fd 100644 --- a/compiler/typecheck/TcDerivUtils.hs +++ b/compiler/typecheck/TcDerivUtils.hs @@ -44,6 +44,7 @@ import SrcLoc import TcGenDeriv import TcGenFunctor import TcGenGenerics +import TcOrigin import TcRnMonad import TcType import THNames (liftClassKey) diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 814143103c..62117bc756 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -15,10 +15,13 @@ 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 @@ -415,7 +418,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope warnRedundantConstraints ctxt' tcl_env info' dead_givens ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs } where - tcl_env = implicLclEnv implic + tcl_env = ic_env implic insoluble = isInsolubleStatus status (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) tvs info' = tidySkolemInfo env1 info @@ -580,7 +583,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics }) -- rigid_nom_eq, rigid_nom_tv_eq, is_hole, is_dict, - is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool + is_equality, is_ip, is_irred :: Ct -> Pred -> Bool is_given_eq ct pred | EqPred {} <- pred = arisesFromGivens ct @@ -639,7 +642,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics }) has_gadt_match (implic : implics) | PatSkol {} <- ic_info implic , not (ic_no_eqs implic) - , wopt Opt_WarnInaccessibleCode (implicDynFlags implic) + , ic_warn_inaccessible implic -- Don't bother doing this if -Winaccessible-code isn't enabled. -- See Note [Avoid -Winaccessible-code when deriving] in TcInstDcls. = True @@ -672,7 +675,7 @@ type Reporter = ReportErrCtxt -> [Ct] -> TcM () type ReporterSpec = ( String -- Name - , Ct -> PredTree -> Bool -- Pick these ones + , Ct -> Pred -> Bool -- Pick these ones , Bool -- True <=> suppress subsequent reporters , Reporter) -- The reporter itself @@ -720,7 +723,7 @@ mkGivenErrorReporter ctxt cts ; dflags <- getDynFlags ; let (implic:_) = cec_encl ctxt -- Always non-empty when mkGivenErrorReporter is called - ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (implicLclEnv implic)) + ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic)) -- For given constraints we overwrite the env (and hence src-loc) -- with one from the immediately-enclosing implication. -- See Note [Inaccessible code] @@ -1218,7 +1221,7 @@ givenConstraintsMsg ctxt = constraints = do { implic@Implic{ ic_given = given } <- cec_encl ctxt ; constraint <- given - ; return (varType constraint, tcl_loc (implicLclEnv implic)) } + ; return (varType constraint, tcl_loc (ic_env implic)) } pprConstraint (constraint, loc) = ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc)) @@ -1571,7 +1574,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 <+> text "bound by" , nest 2 $ ppr skol_info , nest 2 $ text "at" <+> - ppr (tcl_loc (implicLclEnv implic)) ] ] + ppr (tcl_loc (ic_env implic)) ] ] ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) } -- Nastiest case: attempt to unify an untouchable variable @@ -1590,7 +1593,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given , nest 2 $ text "bound by" <+> ppr skol_info , nest 2 $ text "at" <+> - ppr (tcl_loc (implicLclEnv implic)) ] + ppr (tcl_loc (ic_env implic)) ] tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2 add_sig = important $ suggestAddSig ctxt ty1 ty2 ; mkErrorMsgFromCt ctxt ct $ mconcat @@ -1685,7 +1688,7 @@ pp_givens givens -- See Note [Suppress redundant givens during error reporting] -- for why we use mkMinimalBySCs above. 2 (sep [ text "bound by" <+> ppr skol_info - , text "at" <+> ppr (tcl_loc (implicLclEnv implic)) ]) + , text "at" <+> ppr (tcl_loc (ic_env implic)) ]) {- Note [Suppress redundant givens during error reporting] @@ -2433,7 +2436,7 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over _ -> Just $ hang (pprTheta ev_vars_matching) 2 (sep [ text "bound by" <+> ppr skol_info , text "at" <+> - ppr (tcl_loc (implicLclEnv implic)) ]) + ppr (tcl_loc (ic_env implic)) ]) where ev_vars_matching = [ pred | ev_var <- evvars , let pred = evVarPred ev_var diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 85175b227a..ee5b72033f 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -64,12 +64,12 @@ import PrelNames import DynFlags ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) ) import VarEnv import VarSet +import Predicate import Name import Pair import CoreSyn import Class ( classSCSelId ) -import Id ( isEvVar ) import CoreFVs ( exprSomeFreeVars ) import Util @@ -118,7 +118,6 @@ mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion mkTcSubCo :: TcCoercionN -> TcCoercionR -maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion @@ -156,7 +155,6 @@ mkTcForAllCos = mkForAllCos mkTcNthCo = mkNthCo mkTcLRCo = mkLRCo mkTcSubCo = mkSubCo -maybeTcSubCo = maybeSubCo tcDowngradeRole = downgradeRole mkTcAxiomRuleCo = mkAxiomRuleCo mkTcGReflRightCo = mkGReflRightCo @@ -177,6 +175,13 @@ isTcReflexiveCo = isReflexiveCo tcCoToMCo :: TcCoercion -> TcMCoercion tcCoToMCo = coToMCo +-- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing. +-- Note that the input coercion should always be nominal. +maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion +maybeTcSubCo NomEq = id +maybeTcSubCo ReprEq = mkTcSubCo + + {- %************************************************************************ %* * @@ -641,7 +646,7 @@ Instead we make a binding g1 :: a~Bool = g |> ax7 a and the constraint [G] g1 :: a~Bool -See #7238 and Note [Bind new Givens immediately] in TcRnTypes +See #7238 and Note [Bind new Givens immediately] in Constraint Note [EvBinds/EvTerm] ~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 31c2ea4298..3c827fba59 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -25,6 +25,7 @@ import {-# SOURCE #-} TcSplice( tcSpliceExpr, tcTypedBracket, tcUntypedBracket import THNames( liftStringName, liftName ) import GHC.Hs +import Constraint ( HoleSort(..) ) import TcHsSyn import TcRnMonad import TcUnify @@ -44,6 +45,7 @@ import TcHsType import TcPatSyn( tcPatSynBuilderOcc, nonBidirectionalErr ) import TcPat import TcMType +import TcOrigin import TcType import Id import IdInfo diff --git a/compiler/typecheck/TcExpr.hs-boot b/compiler/typecheck/TcExpr.hs-boot index efebcdc6e5..3aa9952088 100644 --- a/compiler/typecheck/TcExpr.hs-boot +++ b/compiler/typecheck/TcExpr.hs-boot @@ -2,7 +2,8 @@ module TcExpr where import Name import GHC.Hs ( HsExpr, LHsExpr, SyntaxExpr ) import TcType ( TcRhoType, TcSigmaType, SyntaxOpType, ExpType, ExpRhoType ) -import TcRnTypes( TcM, CtOrigin ) +import TcRnTypes( TcM ) +import TcOrigin ( CtOrigin ) import GHC.Hs.Extension ( GhcRn, GhcTcId ) tcPolyExpr :: diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index c575cb572c..8f271ac444 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -12,6 +12,8 @@ module TcFlatten( import GhcPrelude import TcRnTypes +import Constraint +import Predicate import TcType import Type import TcEvidence @@ -1362,7 +1364,7 @@ flatten_exact_fam_app_fully tc tys ; let xi = fsk_xi `mkCastTy` kind_co co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co `mkTransCo` - maybeSubCo eq_rel (mkSymCo co) + maybeTcSubCo eq_rel (mkSymCo co) `mkTransCo` ret_co ; return (xi, co') } @@ -1397,7 +1399,7 @@ flatten_exact_fam_app_fully tc tys -- the xis are flattened ; let fsk_ty = mkTyVarTy fsk xi = fsk_ty `mkCastTy` kind_co - co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeSubCo eq_rel (mkSymCo co)) + co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeTcSubCo eq_rel (mkSymCo co)) `mkTransCo` ret_co ; return (xi, co') } @@ -1435,7 +1437,7 @@ flatten_exact_fam_app_fully tc tys ] ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty ; eq_rel <- getEqRel - ; let co = maybeSubCo eq_rel norm_co + ; let co = maybeTcSubCo eq_rel norm_co `mkTransCo` mkSymCo final_co ; flavour <- getFlavour -- NB: only extend cache with nominal equalities @@ -1461,7 +1463,7 @@ flatten_exact_fam_app_fully tc tys Just (norm_co, norm_ty) -> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty ; eq_rel <- getEqRel - ; let co = mkSymCo (maybeSubCo eq_rel norm_co + ; let co = mkSymCo (maybeTcSubCo eq_rel norm_co `mkTransCo` mkSymCo final_co) ; return $ Just (xi, co) } Nothing -> pure Nothing } diff --git a/compiler/typecheck/TcHoleErrors.hs b/compiler/typecheck/TcHoleErrors.hs index 3366e5a1ad..a2eee57947 100644 --- a/compiler/typecheck/TcHoleErrors.hs +++ b/compiler/typecheck/TcHoleErrors.hs @@ -18,6 +18,8 @@ import GhcPrelude import TcRnTypes import TcRnMonad +import Constraint +import TcOrigin import TcMType import TcEvidence import TcType diff --git a/compiler/typecheck/TcHoleErrors.hs-boot b/compiler/typecheck/TcHoleErrors.hs-boot index 16e0c953c0..a8f5b81c8c 100644 --- a/compiler/typecheck/TcHoleErrors.hs-boot +++ b/compiler/typecheck/TcHoleErrors.hs-boot @@ -4,7 +4,8 @@ -- + which calls 'TcSimplify.simpl_top' module TcHoleErrors where -import TcRnTypes ( TcM, Ct, Implication ) +import TcRnTypes ( TcM ) +import Constraint ( Ct, Implication ) import Outputable ( SDoc ) import VarEnv ( TidyEnv ) diff --git a/compiler/typecheck/TcHoleFitTypes.hs b/compiler/typecheck/TcHoleFitTypes.hs index fccf47eb54..0748367f43 100644 --- a/compiler/typecheck/TcHoleFitTypes.hs +++ b/compiler/typecheck/TcHoleFitTypes.hs @@ -8,6 +8,7 @@ module TcHoleFitTypes ( import GhcPrelude import TcRnTypes +import Constraint import TcType import RdrName diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index 3e5f7dc1fe..8ae3a8dc18 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -51,6 +51,7 @@ import GhcPrelude import GHC.Hs import Id import IdInfo +import Predicate import TcRnMonad import PrelNames import BuildTyCl ( TcMethInfo, MethInfo ) diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index cd65fc0522..c2776c7b1b 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -71,6 +71,9 @@ import GhcPrelude import GHC.Hs import TcRnMonad +import TcOrigin +import Predicate +import Constraint import TcEvidence import TcEnv import TcMType @@ -1674,7 +1677,7 @@ is correct, choosing ImplicationStatus IC_BadTelescope if they aren't. Then, in TcErrors, we report if there is a bad telescope. This way, we can report a suggested ordering to the user if there is a problem. -See also Note [Checking telescopes] in TcRnTypes +See also Note [Checking telescopes] in Constraint Note [Keeping scoped variables in order: Implicit] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index c047d13cc8..16150dfec7 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -29,6 +29,8 @@ import TcValidity import TcHsSyn import TcMType import TcType +import Constraint +import TcOrigin import BuildTyCl import Inst import ClsInst( AssocInstInfo(..), isNotAssociated ) @@ -1660,10 +1662,8 @@ Instead, we take the much simpler approach of always disabling 1. In tcMethods (which typechecks method bindings), disable -Winaccessible-code. -2. When creating Implications during typechecking, record the Env - (through ic_env) at the time of creation. Since the Env also stores - DynFlags, this will remember that -Winaccessible-code was disabled over - the scope of that implication. +2. When creating Implications during typechecking, record this flag + (in ic_warn_inaccessible) at the time of creation. 3. After typechecking comes error reporting, where GHC must decide how to report inaccessible code to the user, on an Implication-by-Implication basis. If an Implication's DynFlags indicate that -Winaccessible-code was diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 9122a04436..dbc564a9d3 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -35,6 +35,9 @@ import TcEvidence import Outputable import TcRnTypes +import Constraint +import Predicate +import TcOrigin import TcSMonad import Bag import MonadUtils ( concatMapM, foldlM ) @@ -1181,8 +1184,12 @@ addFunDepWork inerts work_ev cls inert_loc = ctEvLoc inert_ev derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth` ctl_depth inert_loc - , ctl_origin = FunDepOrigin1 work_pred work_loc - inert_pred inert_loc } + , ctl_origin = FunDepOrigin1 work_pred + (ctLocOrigin work_loc) + (ctLocSpan work_loc) + inert_pred + (ctLocOrigin inert_loc) + (ctLocSpan inert_loc) } {- ********************************************************************** @@ -1860,7 +1867,7 @@ selection. This avoids having to support quantified constraints whose kind is not Constraint, such as (forall a. F a ~# b) See - * Note [Evidence for quantified constraints] in Type + * Note [Evidence for quantified constraints] in Predicate * Note [Equality superclasses in quantified constraints] in TcCanonical -} @@ -2609,4 +2616,3 @@ matchLocalInst pred loc qtv_set = mkVarSet qtvs this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc (matches, unif) = match_local_inst qcis - diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index ebd531ec13..e0dc5bcfa8 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -48,6 +48,8 @@ module TcMType ( unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, + newImplication, + -------------------------------- -- Instantiation newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, @@ -98,9 +100,12 @@ import TyCon import Coercion import Class import Var +import Predicate +import TcOrigin -- others: import TcRnMonad -- TcType, amongst others +import Constraint import TcEvidence import Id import Name @@ -116,7 +121,9 @@ import FastString import Bag import Pair import UniqSet +import DynFlags import qualified GHC.LanguageExtensions as LangExt +import BasicTypes ( TypeOrKind(..) ) import Control.Monad import Maybes @@ -287,6 +294,22 @@ predTypeOccName ty = case classifyPredType ty of IrredPred {} -> mkVarOccFS (fsLit "irred") ForAllPred {} -> mkVarOccFS (fsLit "df") +-- | 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 to look up the 'TcLclEnv', which is used to initialize +-- 'ic_env', and to set the -Winaccessible-code flag. See +-- Note [Avoid -Winaccessible-code when deriving] in TcInstDcls. +newImplication :: TcM Implication +newImplication + = do env <- getLclEnv + warn_inaccessible <- woptM Opt_WarnInaccessibleCode + return (implicationPrototype { ic_env = env + , ic_warn_inaccessible = warn_inaccessible }) + {- ************************************************************************ * * @@ -2211,10 +2234,10 @@ zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k) Nothing -> return (env1, Nothing) ; (env3, orig') <- zonkTidyOrigin env2 orig ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) } -zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2) +zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2) = do { (env1, p1') <- zonkTidyTcType env p1 ; (env2, p2') <- zonkTidyTcType env1 p2 - ; return (env2, FunDepOrigin1 p1' l1 p2' l2) } + ; return (env2, FunDepOrigin1 p1' o1 l1 p2' o2 l2) } zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2) = do { (env1, p1') <- zonkTidyTcType env p1 ; (env2, p2') <- zonkTidyTcType env1 p2 @@ -2257,7 +2280,7 @@ tidySkolemInfo _ info = info tidySigSkol :: TidyEnv -> UserTypeCtxt -> TcType -> [(Name,TcTyVar)] -> SkolemInfo -- We need to take special care when tidying SigSkol --- See Note [SigSkol SkolemInfo] in TcRnTypes +-- See Note [SigSkol SkolemInfo] in Origin tidySigSkol env cx ty tv_prs = SigSkol cx (tidy_ty env ty) tv_prs' where diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs index f971da2aa3..139f729fea 100644 --- a/compiler/typecheck/TcMatches.hs +++ b/compiler/typecheck/TcMatches.hs @@ -33,6 +33,7 @@ import TcMType import TcType import TcBinds import TcUnify +import TcOrigin import Name import TysWiredIn import Id diff --git a/compiler/typecheck/TcOrigin.hs b/compiler/typecheck/TcOrigin.hs new file mode 100644 index 0000000000..43bf617749 --- /dev/null +++ b/compiler/typecheck/TcOrigin.hs @@ -0,0 +1,660 @@ +{- + +Describes the provenance of types as they flow through the type-checker. +The datatypes here are mainly used for error message generation. + +-} + +{-# LANGUAGE CPP #-} + +module TcOrigin ( + -- UserTypeCtxt + UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe, + + -- SkolemInfo + SkolemInfo(..), pprSigSkolInfo, pprSkolInfo, + + -- CtOrigin + CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin, + isVisibleOrigin, toInvisibleOrigin, + pprCtOrigin, isGivenOrigin + + ) where + +#include "HsVersions.h" + +import GhcPrelude + +import TcType + +import GHC.Hs + +import Id +import DataCon +import ConLike +import TyCon +import InstEnv +import PatSyn + +import Module +import Name +import RdrName +import qualified GHC.LanguageExtensions as LangExt +import DynFlags + +import SrcLoc +import FastString +import Outputable +import BasicTypes + +{- ********************************************************************* +* * + UserTypeCtxt +* * +********************************************************************* -} + +------------------------------------- +-- | UserTypeCtxt describes the origin of the polymorphic type +-- in the places where we need an expression to have that type +data UserTypeCtxt + = FunSigCtxt -- Function type signature, when checking the type + -- Also used for types in SPECIALISE pragmas + Name -- Name of the function + Bool -- True <=> report redundant constraints + -- This is usually True, but False for + -- * Record selectors (not important here) + -- * Class and instance methods. Here + -- the code may legitimately be more + -- polymorphic than the signature + -- generated from the class + -- declaration + + | InfSigCtxt Name -- Inferred type for function + | ExprSigCtxt -- Expression type signature + | KindSigCtxt -- Kind signature + | StandaloneKindSigCtxt -- Standalone kind signature + Name -- Name of the type/class + | TypeAppCtxt -- Visible type application + | ConArgCtxt Name -- Data constructor argument + | TySynCtxt Name -- RHS of a type synonym decl + | PatSynCtxt Name -- Type sig for a pattern synonym + | PatSigCtxt -- Type sig in pattern + -- eg f (x::t) = ... + -- or (x::t, y) = e + | RuleSigCtxt Name -- LHS of a RULE forall + -- RULE "foo" forall (x :: a -> a). f (Just x) = ... + | ResSigCtxt -- Result type sig + -- f x :: t = .... + | ForSigCtxt Name -- Foreign import or export signature + | DefaultDeclCtxt -- Types in a default declaration + | InstDeclCtxt Bool -- An instance declaration + -- True: stand-alone deriving + -- False: vanilla instance declaration + | SpecInstCtxt -- SPECIALISE instance pragma + | ThBrackCtxt -- Template Haskell type brackets [t| ... |] + | GenSigCtxt -- Higher-rank or impredicative situations + -- e.g. (f e) where f has a higher-rank type + -- We might want to elaborate this + | GhciCtxt Bool -- GHCi command :kind <type> + -- The Bool indicates if we are checking the outermost + -- type application. + -- See Note [Unsaturated type synonyms in GHCi] in + -- TcValidity. + + | ClassSCCtxt Name -- Superclasses of a class + | SigmaCtxt -- Theta part of a normal for-all type + -- f :: <S> => a -> a + | DataTyCtxt Name -- The "stupid theta" part of a data decl + -- data <S> => T a = MkT a + | DerivClauseCtxt -- A 'deriving' clause + | TyVarBndrKindCtxt Name -- The kind of a type variable being bound + | DataKindCtxt Name -- The kind of a data/newtype (instance) + | TySynKindCtxt Name -- The kind of the RHS of a type synonym + | TyFamResKindCtxt Name -- The result kind of a type family + +{- +-- Notes re TySynCtxt +-- We allow type synonyms that aren't types; e.g. type List = [] +-- +-- If the RHS mentions tyvars that aren't in scope, we'll +-- quantify over them: +-- e.g. type T = a->a +-- will become type T = forall a. a->a +-- +-- With gla-exts that's right, but for H98 we should complain. +-} + + +pprUserTypeCtxt :: UserTypeCtxt -> SDoc +pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n) +pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n) +pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n) +pprUserTypeCtxt ExprSigCtxt = text "an expression type signature" +pprUserTypeCtxt KindSigCtxt = text "a kind signature" +pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n) +pprUserTypeCtxt TypeAppCtxt = text "a type argument" +pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c) +pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c) +pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]" +pprUserTypeCtxt PatSigCtxt = text "a pattern type signature" +pprUserTypeCtxt ResSigCtxt = text "a result type signature" +pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n) +pprUserTypeCtxt DefaultDeclCtxt = text "a type in a `default' declaration" +pprUserTypeCtxt (InstDeclCtxt False) = text "an instance declaration" +pprUserTypeCtxt (InstDeclCtxt True) = text "a stand-alone deriving instance declaration" +pprUserTypeCtxt SpecInstCtxt = text "a SPECIALISE instance pragma" +pprUserTypeCtxt GenSigCtxt = text "a type expected by the context" +pprUserTypeCtxt (GhciCtxt {}) = text "a type in a GHCi command" +pprUserTypeCtxt (ClassSCCtxt c) = text "the super-classes of class" <+> quotes (ppr c) +pprUserTypeCtxt SigmaCtxt = text "the context of a polymorphic type" +pprUserTypeCtxt (DataTyCtxt tc) = text "the context of the data type declaration for" <+> quotes (ppr tc) +pprUserTypeCtxt (PatSynCtxt n) = text "the signature for pattern synonym" <+> quotes (ppr n) +pprUserTypeCtxt (DerivClauseCtxt) = text "a `deriving' clause" +pprUserTypeCtxt (TyVarBndrKindCtxt n) = text "the kind annotation on the type variable" <+> quotes (ppr n) +pprUserTypeCtxt (DataKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n) +pprUserTypeCtxt (TySynKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n) +pprUserTypeCtxt (TyFamResKindCtxt n) = text "the result kind for" <+> quotes (ppr n) + +isSigMaybe :: UserTypeCtxt -> Maybe Name +isSigMaybe (FunSigCtxt n _) = Just n +isSigMaybe (ConArgCtxt n) = Just n +isSigMaybe (ForSigCtxt n) = Just n +isSigMaybe (PatSynCtxt n) = Just n +isSigMaybe _ = Nothing + +{- +************************************************************************ +* * + 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 CtOrigin RealSrcSpan -- This constraint arising from ... + PredType CtOrigin RealSrcSpan -- 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. +-- 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 + +isGivenOrigin :: CtOrigin -> Bool +isGivenOrigin (GivenOrigin {}) = True +isGivenOrigin (FunDepOrigin1 _ o1 _ _ o2 _) = isGivenOrigin o1 && isGivenOrigin o2 +isGivenOrigin (FunDepOrigin2 _ o1 _ _) = isGivenOrigin o1 +isGivenOrigin _ = False + +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 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" + +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 orig1 loc1 pred2 orig2 loc2) + = hang (ctoHerald <+> text "a functional dependency between constraints:") + 2 (vcat [ hang (quotes (ppr pred1)) 2 (pprCtOrigin orig1 <+> text "at" <+> ppr loc1) + , hang (quotes (ppr pred2)) 2 (pprCtOrigin orig2 <+> text "at" <+> ppr 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" diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index 1a7adde878..39e6dcd3dd 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -39,6 +39,7 @@ import TcUnify import TcHsType import TysWiredIn import TcEvidence +import TcOrigin import TyCon import DataCon import PatSyn diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 28ec8471ff..746b48401b 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -40,10 +40,11 @@ import TcBinds import BasicTypes import TcSimplify import TcUnify -import Type( PredTree(..), EqRel(..), classifyPredType ) +import Predicate import TysWiredIn import TcType import TcEvidence +import TcOrigin import BuildTyCl import VarSet import MkId @@ -300,7 +301,7 @@ have type $bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a and that is bad because (a ~# Maybe b) is not a predicate type -(see Note [Types for coercions, predicates, and evidence] in Type) +(see Note [Types for coercions, predicates, and evidence] in TyCoRep and is not implicitly instantiated. So in mkProvEvidence we lift (a ~# b) to (a ~ b). Tiresome, and @@ -405,7 +406,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details ; let skol_info = SigSkol (PatSynCtxt name) pat_ty [] -- The type here is a bit bogus, but we do not print -- the type for PatSynCtxt, so it doesn't matter - -- See TcRnTypes Note [Skolem info for pattern synonyms] + -- See Note [Skolem info for pattern synonyms] in Origin ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted -- Solve the constraints now, because we are about to make a PatSyn, diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs index f4fe3013a3..d88e25cc87 100644 --- a/compiler/typecheck/TcPluginM.hs +++ b/compiler/typecheck/TcPluginM.hs @@ -61,14 +61,14 @@ import qualified IfaceEnv import qualified Finder import FamInstEnv ( FamInstEnv ) -import TcRnMonad ( TcGblEnv, TcLclEnv, Ct, CtLoc, TcPluginM +import TcRnMonad ( TcGblEnv, TcLclEnv, TcPluginM , unsafeTcPluginTcM, getEvBindsTcPluginM , liftIO, traceTc ) +import Constraint ( Ct, CtLoc, CtEvidence(..), ctLocOrigin ) import TcMType ( TcTyVar, TcType ) import TcEnv ( TcTyThing ) import TcEvidence ( TcCoercion, CoercionHole, EvTerm(..) , EvExpr, EvBind, mkGivenEvBind ) -import TcRnTypes ( CtEvidence(..) ) import Var ( EvVar ) import Module @@ -158,7 +158,7 @@ zonkCt = unsafeTcPluginTcM . TcM.zonkCt -- | Create a new wanted constraint. newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence newWanted loc pty - = unsafeTcPluginTcM (TcM.newWanted (TcM.ctLocOrigin loc) Nothing pty) + = unsafeTcPluginTcM (TcM.newWanted (ctLocOrigin loc) Nothing pty) -- | Create a new derived constraint. newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 22606871aa..000455bd3f 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -76,6 +76,8 @@ import TcExpr import TcRnMonad import TcRnExports import TcEvidence +import Constraint +import TcOrigin import qualified BooleanFormula as BF import PprTyThing( pprTyThingInContext ) import CoreFVs( orphNamesOfFamInst ) diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs index fe3f3e6d4c..c820eb3c20 100644 --- a/compiler/typecheck/TcRnMonad.hs +++ b/compiler/typecheck/TcRnMonad.hs @@ -146,7 +146,9 @@ import GhcPrelude import TcRnTypes -- Re-export all import IOEnv -- Re-export all +import Constraint import TcEvidence +import TcOrigin import GHC.Hs hiding (LIE) import HscTypes @@ -175,7 +177,7 @@ import FastString import Panic import Util import Annotations -import BasicTypes( TopLevelFlag ) +import BasicTypes( TopLevelFlag, TypeOrKind(..) ) import Maybes import CostCentreState diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index f95f853a70..8fa12b28b1 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, - HoleSort(..), - 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,16 +119,14 @@ 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 Data.Set ( Set ) import qualified Data.Set as S import Data.List ( sort ) @@ -856,6 +785,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 @@ -864,6 +805,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) @@ -1677,2220 +1630,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_occ :: OccName, -- The name of this hole - cc_hole :: HoleSort -- The sort of this hole (expr, type, ...) - } - - | 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 - ------------- --- | Used to indicate which sort of hole we have. -data HoleSort = ExprHole - -- ^ Either an out-of-scope variable or a "true" hole in an - -- expression (TypedHoles) - | TypeHole - -- ^ A hole in a type (PartialTypeSignatures) - -{- Note [Hole constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -CHoleCan constraints are used for two kinds of holes, -distinguished by cc_hole: - - * For holes in expressions - 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_occ = occ } -> text "CHoleCan:" <+> ppr occ - 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 --- A Hole that does not have a leading underscore is --- simply an out-of-scope variable, and we treat that --- a bit differently when it comes to error reporting -isOutOfScopeCt (CHoleCan { cc_occ = occ }) = not (startsWithUnderscore occ) -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 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 ------------------------- -} diff --git a/compiler/typecheck/TcRnTypes.hs-boot b/compiler/typecheck/TcRnTypes.hs-boot index b22f5c3ff8..dda9f627fe 100644 --- a/compiler/typecheck/TcRnTypes.hs-boot +++ b/compiler/typecheck/TcRnTypes.hs-boot @@ -1,6 +1,12 @@ module TcRnTypes where --- Build ordering -import GHC.Base() +import TcType +import SrcLoc data TcLclEnv + +setLclEnvTcLevel :: TcLclEnv -> TcLevel -> TcLclEnv +getLclEnvTcLevel :: TcLclEnv -> TcLevel + +setLclEnvLoc :: TcLclEnv -> RealSrcSpan -> TcLclEnv +getLclEnvLoc :: TcLclEnv -> RealSrcSpan diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs index 41a7be18b7..36de540aed 100644 --- a/compiler/typecheck/TcRules.hs +++ b/compiler/typecheck/TcRules.hs @@ -17,6 +17,9 @@ import GHC.Hs import TcRnTypes import TcRnMonad import TcSimplify +import Constraint +import Predicate +import TcOrigin import TcMType import TcType import TcHsType diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 72017d9069..ca6022f23b 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -164,6 +164,9 @@ import Bag import UniqSupply import Util import TcRnTypes +import TcOrigin +import Constraint +import Predicate import Unique import UniqFM @@ -1100,7 +1103,7 @@ instance Outputable InertCans where Note [The improvement story and derived shadows] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not -rewrite Wanteds] in TcRnTypes), we may miss some opportunities for +rewrite Wanteds] in Constraint), we may miss some opportunities for solving. Here's a classic example (indexed-types/should_fail/T4093a) Ambiguity check for f: (Foo e ~ Maybe e) => Foo e @@ -2931,7 +2934,7 @@ checkTvConstraintsTcS skol_info skol_tvs (TcS thing_inside) ; unless (null wanteds) $ do { ev_binds_var <- TcM.newNoTcEvBinds - ; imp <- newImplication + ; imp <- TcM.newImplication ; let wc = emptyWC { wc_simple = wanteds } imp' = imp { ic_tclvl = new_tclvl , ic_skols = skol_tvs @@ -2970,7 +2973,7 @@ checkConstraintsTcS skol_info skol_tvs given (TcS thing_inside) thing_inside new_tcs_env ; ev_binds_var <- TcM.newTcEvBinds - ; imp <- newImplication + ; imp <- TcM.newImplication ; let wc = emptyWC { wc_simple = wanteds } imp' = imp { ic_tclvl = new_tclvl , ic_skols = skol_tvs @@ -3440,7 +3443,7 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence -- Make a new variable of the given PredType, -- immediately bind it to the given term -- and return its CtEvidence --- See Note [Bind new Givens immediately] in TcRnTypes +-- See Note [Bind new Givens immediately] in Constraint newGivenEvVar loc (pred, rhs) = do { new_ev <- newBoundEvVarId pred rhs ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) } diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index 3aa16a83f5..9d03576ae0 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -31,6 +31,7 @@ import GHC.Hs import TcHsType import TcRnTypes import TcRnMonad +import TcOrigin import TcType import TcMType import TcValidity ( checkValidType ) diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 7efaf2f29a..34bc4a8448 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -45,6 +45,9 @@ import TcCanonical ( makeSuperClasses, solveCallStack ) import TcMType as TcM import TcRnMonad as TcM import TcSMonad as TcS +import Constraint +import Predicate +import TcOrigin import TcType import Type import TysWiredIn ( liftedRepTy ) @@ -835,7 +838,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds | psig_theta_var <- psig_theta_vars ] -- Now construct the residual constraint - ; residual_wanted <- mkResidualConstraints rhs_tclvl tc_env ev_binds_var + ; residual_wanted <- mkResidualConstraints rhs_tclvl ev_binds_var name_taus co_vars qtvs bound_theta_vars (wanted_transformed `andWC` mkSimpleWC psig_wanted) @@ -854,13 +857,13 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds partial_sigs = filter isPartialSig sigs -------------------- -mkResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar +mkResidualConstraints :: TcLevel -> EvBindsVar -> [(Name, TcTauType)] -> VarSet -> [TcTyVar] -> [EvVar] -> WantedConstraints -> TcM WantedConstraints -- Emit the remaining constraints from the RHS. -- See Note [Emitting the residual implication in simplifyInfer] -mkResidualConstraints rhs_tclvl tc_env ev_binds_var +mkResidualConstraints rhs_tclvl ev_binds_var name_taus co_vars qtvs full_theta_vars wanteds | isEmptyWC wanteds = return wanteds @@ -873,23 +876,22 @@ mkResidualConstraints rhs_tclvl tc_env ev_binds_var ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple) ; let inner_wanted = wanteds { wc_simple = inner_simple } + ; implics <- if isEmptyWC inner_wanted + then return emptyBag + else do implic1 <- newImplication + return $ unitBag $ + implic1 { ic_tclvl = rhs_tclvl + , ic_skols = qtvs + , ic_telescope = Nothing + , ic_given = full_theta_vars + , ic_wanted = inner_wanted + , ic_binds = ev_binds_var + , ic_no_eqs = False + , ic_info = skol_info } + ; return (WC { wc_simple = outer_simple - , wc_impl = mk_implic inner_wanted })} + , wc_impl = implics })} where - mk_implic inner_wanted - | isEmptyWC inner_wanted - = emptyBag - | otherwise - = unitBag (implicationPrototype { ic_tclvl = rhs_tclvl - , ic_skols = qtvs - , ic_telescope = Nothing - , ic_given = full_theta_vars - , ic_wanted = inner_wanted - , ic_binds = ev_binds_var - , ic_no_eqs = False - , ic_info = skol_info - , ic_env = tc_env }) - full_theta = map idType full_theta_vars skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty) | (name, ty) <- name_taus ] @@ -1663,7 +1665,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -- Solve the nested constraints ; (no_given_eqs, given_insols, residual_wanted) <- nestImplicTcS ev_binds_var tclvl $ - do { let loc = mkGivenLoc tclvl info (implicLclEnv imp) + do { let loc = mkGivenLoc tclvl info (ic_env imp) givens = mkGivens loc given_ids ; solveSimpleGivens givens diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index 05c2b0fd10..aa9e38357e 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -46,6 +46,7 @@ import SrcLoc import THNames import TcUnify import TcEnv +import TcOrigin import Coercion( etaExpandCoAxBranch ) import FileCleanup ( newTempName, TempFileLifetime(..) ) diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 904f80827f..80e220d385 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -47,6 +47,7 @@ import RnEnv( lookupConstructorFields ) import FamInst import FamInstEnv import Coercion +import TcOrigin import Type import TyCoRep -- for checkValidRoles import Class diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index 09a6be7a69..026186c1bd 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -36,6 +36,7 @@ import TcEnv import TcBinds( tcValBinds ) import TyCoRep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) ) import TcType +import Predicate import TysWiredIn( unitTy ) import MkCore( rEC_SEL_ERROR_ID ) import GHC.Hs diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 1d3ec0d568..c116e4fea3 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -36,7 +36,6 @@ module TcType ( promoteSkolem, promoteSkolemX, promoteSkolemsX, -------------------------------- -- MetaDetails - UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe, TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv, MetaDetails(Flexi, Indirect), MetaInfo(..), isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, @@ -141,7 +140,6 @@ module TcType ( isClassPred, isEqPrimPred, isIPPred, isEqPred, isEqPredClass, mkClassPred, - isDictLikeTy, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy, isRuntimeRepVar, isKindLevPoly, isVisibleBinder, isInvisibleBinder, @@ -205,6 +203,7 @@ import ForeignCall import VarSet import Coercion import Type +import Predicate import RepType import TyCon @@ -572,123 +571,6 @@ instance Outputable MetaInfo where {- ********************************************************************* * * - UserTypeCtxt -* * -********************************************************************* -} - -------------------------------------- --- UserTypeCtxt describes the origin of the polymorphic type --- in the places where we need an expression to have that type - -data UserTypeCtxt - = FunSigCtxt -- Function type signature, when checking the type - -- Also used for types in SPECIALISE pragmas - Name -- Name of the function - Bool -- True <=> report redundant constraints - -- This is usually True, but False for - -- * Record selectors (not important here) - -- * Class and instance methods. Here - -- the code may legitimately be more - -- polymorphic than the signature - -- generated from the class - -- declaration - - | InfSigCtxt Name -- Inferred type for function - | ExprSigCtxt -- Expression type signature - | KindSigCtxt -- Kind signature - | StandaloneKindSigCtxt -- Standalone kind signature - Name -- Name of the type/class - | TypeAppCtxt -- Visible type application - | ConArgCtxt Name -- Data constructor argument - | TySynCtxt Name -- RHS of a type synonym decl - | PatSynCtxt Name -- Type sig for a pattern synonym - | PatSigCtxt -- Type sig in pattern - -- eg f (x::t) = ... - -- or (x::t, y) = e - | RuleSigCtxt Name -- LHS of a RULE forall - -- RULE "foo" forall (x :: a -> a). f (Just x) = ... - | ResSigCtxt -- Result type sig - -- f x :: t = .... - | ForSigCtxt Name -- Foreign import or export signature - | DefaultDeclCtxt -- Types in a default declaration - | InstDeclCtxt Bool -- An instance declaration - -- True: stand-alone deriving - -- False: vanilla instance declaration - | SpecInstCtxt -- SPECIALISE instance pragma - | ThBrackCtxt -- Template Haskell type brackets [t| ... |] - | GenSigCtxt -- Higher-rank or impredicative situations - -- e.g. (f e) where f has a higher-rank type - -- We might want to elaborate this - | GhciCtxt Bool -- GHCi command :kind <type> - -- The Bool indicates if we are checking the outermost - -- type application. - -- See Note [Unsaturated type synonyms in GHCi] in - -- TcValidity. - - | ClassSCCtxt Name -- Superclasses of a class - | SigmaCtxt -- Theta part of a normal for-all type - -- f :: <S> => a -> a - | DataTyCtxt Name -- The "stupid theta" part of a data decl - -- data <S> => T a = MkT a - | DerivClauseCtxt -- A 'deriving' clause - | TyVarBndrKindCtxt Name -- The kind of a type variable being bound - | DataKindCtxt Name -- The kind of a data/newtype (instance) - | TySynKindCtxt Name -- The kind of the RHS of a type synonym - | TyFamResKindCtxt Name -- The result kind of a type family - -{- --- Notes re TySynCtxt --- We allow type synonyms that aren't types; e.g. type List = [] --- --- If the RHS mentions tyvars that aren't in scope, we'll --- quantify over them: --- e.g. type T = a->a --- will become type T = forall a. a->a --- --- With gla-exts that's right, but for H98 we should complain. --} - - -pprUserTypeCtxt :: UserTypeCtxt -> SDoc -pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n) -pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n) -pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n) -pprUserTypeCtxt ExprSigCtxt = text "an expression type signature" -pprUserTypeCtxt KindSigCtxt = text "a kind signature" -pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n) -pprUserTypeCtxt TypeAppCtxt = text "a type argument" -pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c) -pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c) -pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]" -pprUserTypeCtxt PatSigCtxt = text "a pattern type signature" -pprUserTypeCtxt ResSigCtxt = text "a result type signature" -pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n) -pprUserTypeCtxt DefaultDeclCtxt = text "a type in a `default' declaration" -pprUserTypeCtxt (InstDeclCtxt False) = text "an instance declaration" -pprUserTypeCtxt (InstDeclCtxt True) = text "a stand-alone deriving instance declaration" -pprUserTypeCtxt SpecInstCtxt = text "a SPECIALISE instance pragma" -pprUserTypeCtxt GenSigCtxt = text "a type expected by the context" -pprUserTypeCtxt (GhciCtxt {}) = text "a type in a GHCi command" -pprUserTypeCtxt (ClassSCCtxt c) = text "the super-classes of class" <+> quotes (ppr c) -pprUserTypeCtxt SigmaCtxt = text "the context of a polymorphic type" -pprUserTypeCtxt (DataTyCtxt tc) = text "the context of the data type declaration for" <+> quotes (ppr tc) -pprUserTypeCtxt (PatSynCtxt n) = text "the signature for pattern synonym" <+> quotes (ppr n) -pprUserTypeCtxt (DerivClauseCtxt) = text "a `deriving' clause" -pprUserTypeCtxt (TyVarBndrKindCtxt n) = text "the kind annotation on the type variable" <+> quotes (ppr n) -pprUserTypeCtxt (DataKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n) -pprUserTypeCtxt (TySynKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n) -pprUserTypeCtxt (TyFamResKindCtxt n) = text "the result kind for" <+> quotes (ppr n) - -isSigMaybe :: UserTypeCtxt -> Maybe Name -isSigMaybe (FunSigCtxt n _) = Just n -isSigMaybe (ConArgCtxt n) = Just n -isSigMaybe (ForSigCtxt n) = Just n -isSigMaybe (PatSynCtxt n) = Just n -isSigMaybe _ = Nothing - - -{- ********************************************************************* -* * Untouchable type variables * * ********************************************************************* -} @@ -1998,7 +1880,7 @@ Note [Lift equality constaints when quantifying] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We can't quantify over a constraint (t1 ~# t2) because that isn't a predicate type; see Note [Types for coercions, predicates, and evidence] -in Type.hs. +in TyCoRep. So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted to Coercible. @@ -2137,14 +2019,6 @@ isCallStackPred cls tys | otherwise = Nothing -hasIPPred :: PredType -> Bool -hasIPPred pred - = case classifyPredType pred of - ClassPred cls tys - | isIPClass cls -> True - | isCTupleClass cls -> any hasIPPred tys - _other -> False - is_tc :: Unique -> Type -> Bool -- Newtypes are opaque to this is_tc uniq ty = case tcSplitTyConApp_maybe ty of diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index 8588576acb..6e5eb94d72 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -29,7 +29,7 @@ import TcType ( TcType, tcEqType ) import TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon , Injectivity(..) ) import Coercion ( Role(..) ) -import TcRnTypes ( Xi ) +import Constraint ( Xi ) import CoAxiom ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn ) import Name ( Name, BuiltInSyntax(..) ) import TysWiredIn diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 37190a63fb..819cc0c2ee 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -48,6 +48,9 @@ import TcType import Type import Coercion import TcEvidence +import Constraint +import Predicate +import TcOrigin import Name( isSystemName ) import Inst import TyCon @@ -1208,7 +1211,7 @@ emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted , isNothing m_telescope || skol_tvs `lengthAtMost` 1 -- If m_telescope is (Just d), we must do the bad-telescope check, -- so we must /not/ discard the implication even if there are no - -- wanted constraints. See Note [Checking telescopes] in TcRnTypes. + -- wanted constraints. See Note [Checking telescopes] in Constraint. -- Lacking this check led to #16247 = return () diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index e72aa7f7b0..e5d0f3ca5e 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -38,6 +38,8 @@ import Coercion import CoAxiom import Class import TyCon +import Predicate +import TcOrigin -- others: import IfaceType( pprIfaceType, pprIfaceTypeApp ) diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index d0000e1e35..7695e31643 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -37,11 +37,13 @@ module Coercion ( mkPhantomCo, mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo, mkAxiomInstCo, mkProofIrrelCo, - downgradeRole, maybeSubCo, mkAxiomRuleCo, + downgradeRole, mkAxiomRuleCo, mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo, mkKindCo, castCoercionKind, castCoercionKindI, mkHeteroCoercionType, + mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole, + mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, -- ** Decomposition instNewTyCon_maybe, @@ -138,7 +140,7 @@ import Unique import Pair import SrcLoc import PrelNames -import TysPrim ( eqPhantPrimTyCon ) +import TysPrim import ListSetOps import Maybes import UniqFM @@ -506,22 +508,6 @@ coVarRole cv Just tc0 -> tc0 Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv) --- | Makes a coercion type from two types: the types whose equality --- is proven by the relevant 'Coercion' -mkCoercionType :: Role -> Type -> Type -> Type -mkCoercionType Nominal = mkPrimEqPred -mkCoercionType Representational = mkReprPrimEqPred -mkCoercionType Phantom = \ty1 ty2 -> - let ki1 = typeKind ty1 - ki2 = typeKind ty2 - in - TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2] - -mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type -mkHeteroCoercionType Nominal = mkHeteroPrimEqPred -mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred -mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType" - -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@, -- produce a coercion @rep_co :: r1 ~ r2@. mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion @@ -1232,13 +1218,6 @@ downgradeRole r1 r2 co Just co' -> co' Nothing -> pprPanic "downgradeRole" (ppr co) --- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing. --- Note that the input coercion should always be nominal. -maybeSubCo :: EqRel -> Coercion -> Coercion -maybeSubCo NomEq = id -maybeSubCo ReprEq = mkSubCo - - mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion mkAxiomRuleCo = AxiomRuleCo @@ -2357,6 +2336,54 @@ cf Type.piResultTys (which in fact we call here). -} +-- | Makes a coercion type from two types: the types whose equality +-- is proven by the relevant 'Coercion' +mkCoercionType :: Role -> Type -> Type -> Type +mkCoercionType Nominal = mkPrimEqPred +mkCoercionType Representational = mkReprPrimEqPred +mkCoercionType Phantom = \ty1 ty2 -> + let ki1 = typeKind ty1 + ki2 = typeKind ty2 + in + TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2] + +mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type +mkHeteroCoercionType Nominal = mkHeteroPrimEqPred +mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred +mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType" + +-- | Creates a primitive type equality predicate. +-- Invariant: the types are not Coercions +mkPrimEqPred :: Type -> Type -> Type +mkPrimEqPred ty1 ty2 + = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2] + where + k1 = typeKind ty1 + k2 = typeKind ty2 + +-- | Makes a lifted equality predicate at the given role +mkPrimEqPredRole :: Role -> Type -> Type -> PredType +mkPrimEqPredRole Nominal = mkPrimEqPred +mkPrimEqPredRole Representational = mkReprPrimEqPred +mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom" + +-- | Creates a primite type equality predicate with explicit kinds +mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type +mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2] + +-- | Creates a primitive representational type equality predicate +-- with explicit kinds +mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type +mkHeteroReprPrimEqPred k1 k2 ty1 ty2 + = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2] + +mkReprPrimEqPred :: Type -> Type -> Type +mkReprPrimEqPred ty1 ty2 + = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2] + where + k1 = typeKind ty1 + k2 = typeKind ty2 + -- | Assuming that two types are the same, ignoring coercions, find -- a nominal coercion between the types. This is useful when optimizing -- transitivity over coercion applications, where splitting two diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index ed94241c5f..51c3679351 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -52,11 +52,14 @@ module Type ( mkLamType, mkLamTypes, piResultTy, piResultTys, applyTysX, dropForAlls, + mkFamilyTyConApp, mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy, isLitTy, + isPredTy, + getRuntimeRep_maybe, kindRep_maybe, kindRep, mkCastTy, mkCoercionTy, splitCastTy_maybe, @@ -65,7 +68,7 @@ module Type ( userTypeError_maybe, pprUserTypeErrorTy, coAxNthLHS, - stripCoercionTy, splitCoercionType_maybe, + stripCoercionTy, splitPiTysInvisible, splitPiTysInvisibleN, invisibleTyBndrCount, @@ -82,23 +85,6 @@ module Type ( -- (Newtypes) newTyConInstRhs, - -- Pred types - mkFamilyTyConApp, - isDictLikeTy, - mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole, - equalityTyCon, - mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, - mkClassPred, - isClassPred, isEqPrimPred, isEqPred, isEqPredClass, - isIPPred, isIPTyCon, isIPClass, - isCTupleClass, - - -- Deconstructing predicate types - PredTree(..), EqRel(..), eqRelRole, classifyPredType, - getClassPredTys, getClassPredTys_maybe, - getEqPredTys, getEqPredTys_maybe, getEqPredRole, - predTypeEqRel, - -- ** Binders sameVis, mkTyCoVarBinder, mkTyCoVarBinders, @@ -117,11 +103,11 @@ module Type ( funTyCon, -- ** Predicates on types - isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy, + isTyVarTy, isFunTy, isCoercionTy, isCoercionTy_maybe, isForAllTy, isForAllTy_ty, isForAllTy_co, isPiTy, isTauTy, isFamFreeTy, - isCoVarType, isEvVarType, + isCoVarType, isValidJoinPointType, tyConAppNeedsKindSig, @@ -253,7 +239,6 @@ import VarEnv import VarSet import UniqSet -import Class import TyCon import TysPrim import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind @@ -1191,6 +1176,18 @@ splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty' splitTyConApp_maybe ty = repSplitTyConApp_maybe ty +-- | Split a type constructor application into its type constructor and +-- applied types. Note that this may fail in the case of a 'FunTy' with an +-- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind +-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your +-- type before using this function. +-- +-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'. +tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type]) +-- Defined here to avoid module loops between Unify and TcType. +tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty' +tcSplitTyConApp_maybe ty = repSplitTyConApp_maybe ty + ------------------- repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) -- ^ Like 'splitTyConApp_maybe', but doesn't look through synonyms. This @@ -1790,320 +1787,6 @@ binderRelevantType_maybe :: TyCoBinder -> Maybe Type binderRelevantType_maybe (Named {}) = Nothing binderRelevantType_maybe (Anon _ ty) = Just ty -{- -%************************************************************************ -%* * - Pred -* * -************************************************************************ - -Predicates on PredType - -Note [Evidence for quantified constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The superclass mechanism in TcCanonical.makeSuperClasses risks -taking a quantified constraint like - (forall a. C a => a ~ b) -and generate superclass evidence - (forall a. C a => a ~# b) - -This is a funny thing: neither isPredTy nor isCoVarType are true -of it. So we are careful not to generate it in the first place: -see Note [Equality superclasses in quantified constraints] -in TcCanonical. --} - --- | Split a type constructor application into its type constructor and --- applied types. Note that this may fail in the case of a 'FunTy' with an --- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind --- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your --- type before using this function. --- --- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'. -tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type]) --- Defined here to avoid module loops between Unify and TcType. -tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty' -tcSplitTyConApp_maybe ty = repSplitTyConApp_maybe ty - --- tcIsConstraintKind stuf only makes sense in the typechecker --- After that Constraint = Type --- See Note [coreView vs tcView] --- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh) -tcIsConstraintKind :: Kind -> Bool -tcIsConstraintKind ty - | Just (tc, args) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here - , isConstraintKindCon tc - = ASSERT2( null args, ppr ty ) True - - | otherwise - = False - --- | Is this kind equivalent to @*@? --- --- This considers 'Constraint' to be distinct from @*@. For a version that --- treats them as the same type, see 'isLiftedTypeKind'. -tcIsLiftedTypeKind :: Kind -> Bool -tcIsLiftedTypeKind ty - | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here - , tc `hasKey` tYPETyConKey - = isLiftedRuntimeRep arg - | otherwise - = False - --- | Is this kind equivalent to @TYPE r@ (for some unknown r)? --- --- This considers 'Constraint' to be distinct from @*@. -tcIsRuntimeTypeKind :: Kind -> Bool -tcIsRuntimeTypeKind ty - | Just (tc, _) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here - , tc `hasKey` tYPETyConKey - = True - | otherwise - = False - -tcReturnsConstraintKind :: Kind -> Bool --- True <=> the Kind ultimately returns a Constraint --- E.g. * -> Constraint --- forall k. k -> Constraint -tcReturnsConstraintKind kind - | Just kind' <- tcView kind = tcReturnsConstraintKind kind' -tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty -tcReturnsConstraintKind (FunTy { ft_res = ty }) = tcReturnsConstraintKind ty -tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc -tcReturnsConstraintKind _ = False - -isEvVarType :: Type -> Bool --- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b) --- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2) --- See Note [Types for coercions, predicates, and evidence] --- See Note [Evidence for quantified constraints] -isEvVarType ty = isCoVarType ty || isPredTy ty - --- | Does this type classify a core (unlifted) Coercion? --- At either role nominal or representational --- (t1 ~# t2) or (t1 ~R# t2) --- See Note [Types for coercions, predicates, and evidence] -isCoVarType :: Type -> Bool -isCoVarType ty = isEqPrimPred ty - -isEqPredClass :: Class -> Bool --- True of (~) and (~~) -isEqPredClass cls = cls `hasKey` eqTyConKey - || cls `hasKey` heqTyConKey - -isClassPred, isEqPred, isEqPrimPred, isIPPred :: PredType -> Bool -isClassPred ty = case tyConAppTyCon_maybe ty of - Just tyCon | isClassTyCon tyCon -> True - _ -> False - -isEqPred ty -- True of (a ~ b) and (a ~~ b) - -- ToDo: should we check saturation? - | Just tc <- tyConAppTyCon_maybe ty - , Just cls <- tyConClass_maybe tc - = isEqPredClass cls - | otherwise - = False - -isEqPrimPred ty -- True of (a ~# b) (a ~R# b) - -- ToDo: should we check saturation? - | Just tc <- tyConAppTyCon_maybe ty - = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey - | otherwise - = False - -isIPPred ty = case tyConAppTyCon_maybe ty of - Just tc -> isIPTyCon tc - _ -> False - -isIPTyCon :: TyCon -> Bool -isIPTyCon tc = tc `hasKey` ipClassKey - -- Class and its corresponding TyCon have the same Unique - -isIPClass :: Class -> Bool -isIPClass cls = cls `hasKey` ipClassKey - -isCTupleClass :: Class -> Bool -isCTupleClass cls = isTupleTyCon (classTyCon cls) - -{- -Make PredTypes - ---------------------- Equality types --------------------------------- --} - --- | Makes a lifted equality predicate at the given role -mkPrimEqPredRole :: Role -> Type -> Type -> PredType -mkPrimEqPredRole Nominal = mkPrimEqPred -mkPrimEqPredRole Representational = mkReprPrimEqPred -mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom" - --- | Creates a primitive type equality predicate. --- Invariant: the types are not Coercions -mkPrimEqPred :: Type -> Type -> Type -mkPrimEqPred ty1 ty2 - = TyConApp eqPrimTyCon [k1, k2, ty1, ty2] - where - k1 = typeKind ty1 - k2 = typeKind ty2 - --- | Creates a primite type equality predicate with explicit kinds -mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type -mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2] - --- | Creates a primitive representational type equality predicate --- with explicit kinds -mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type -mkHeteroReprPrimEqPred k1 k2 ty1 ty2 - = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2] - --- | Try to split up a coercion type into the types that it coerces -splitCoercionType_maybe :: Type -> Maybe (Type, Type) -splitCoercionType_maybe ty - = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty - ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey - ; return (ty1, ty2) } - -mkReprPrimEqPred :: Type -> Type -> Type -mkReprPrimEqPred ty1 ty2 - = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2] - where - k1 = typeKind ty1 - k2 = typeKind ty2 - -equalityTyCon :: Role -> TyCon -equalityTyCon Nominal = eqPrimTyCon -equalityTyCon Representational = eqReprPrimTyCon -equalityTyCon Phantom = eqPhantPrimTyCon - --- --------------------- Dictionary types --------------------------------- - -mkClassPred :: Class -> [Type] -> PredType -mkClassPred clas tys = TyConApp (classTyCon clas) tys - -isDictTy :: Type -> Bool -isDictTy = isClassPred - -isDictLikeTy :: Type -> Bool --- Note [Dictionary-like types] -isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty' -isDictLikeTy ty = case splitTyConApp_maybe ty of - Just (tc, tys) | isClassTyCon tc -> True - | isTupleTyCon tc -> all isDictLikeTy tys - _other -> False - -{- Note [Dictionary-like types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Being "dictionary-like" means either a dictionary type or a tuple thereof. -In GHC 6.10 we build implication constraints which construct such tuples, -and if we land up with a binding - t :: (C [a], Eq [a]) - t = blah -then we want to treat t as cheap under "-fdicts-cheap" for example. -(Implication constraints are normally inlined, but sadly not if the -occurrence is itself inside an INLINE function! Until we revise the -handling of implication constraints, that is.) This turned out to -be important in getting good arities in DPH code. Example: - - class C a - class D a where { foo :: a -> a } - instance C a => D (Maybe a) where { foo x = x } - - bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b) - {-# INLINE bar #-} - bar x y = (foo (Just x), foo (Just y)) - -Then 'bar' should jolly well have arity 4 (two dicts, two args), but -we ended up with something like - bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ... - in \x,y. <blah>) - -This is all a bit ad-hoc; eg it relies on knowing that implication -constraints build tuples. - -ToDo: it would be far easier just to use isPredTy. --} - --- | A choice of equality relation. This is separate from the type 'Role' --- because 'Phantom' does not define a (non-trivial) equality relation. -data EqRel = NomEq | ReprEq - deriving (Eq, Ord) - -instance Outputable EqRel where - ppr NomEq = text "nominal equality" - ppr ReprEq = text "representational equality" - -eqRelRole :: EqRel -> Role -eqRelRole NomEq = Nominal -eqRelRole ReprEq = Representational - -data PredTree - = ClassPred Class [Type] - | EqPred EqRel Type Type - | IrredPred PredType - | ForAllPred [TyCoVarBinder] [PredType] PredType - -- ForAllPred: see Note [Quantified constraints] in TcCanonical - -- NB: There is no TuplePred case - -- Tuple predicates like (Eq a, Ord b) are just treated - -- as ClassPred, as if we had a tuple class with two superclasses - -- class (c1, c2) => (%,%) c1 c2 - -classifyPredType :: PredType -> PredTree -classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of - Just (tc, [_, _, ty1, ty2]) - | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2 - | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2 - - Just (tc, tys) - | Just clas <- tyConClass_maybe tc - -> ClassPred clas tys - - _ | (tvs, rho) <- splitForAllVarBndrs ev_ty - , (theta, pred) <- splitFunTys rho - , not (null tvs && null theta) - -> ForAllPred tvs theta pred - - | otherwise - -> IrredPred ev_ty - -getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type]) -getClassPredTys ty = case getClassPredTys_maybe ty of - Just (clas, tys) -> (clas, tys) - Nothing -> pprPanic "getClassPredTys" (ppr ty) - -getClassPredTys_maybe :: PredType -> Maybe (Class, [Type]) -getClassPredTys_maybe ty = case splitTyConApp_maybe ty of - Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys) - _ -> Nothing - -getEqPredTys :: PredType -> (Type, Type) -getEqPredTys ty - = case splitTyConApp_maybe ty of - Just (tc, [_, _, ty1, ty2]) - | tc `hasKey` eqPrimTyConKey - || tc `hasKey` eqReprPrimTyConKey - -> (ty1, ty2) - _ -> pprPanic "getEqPredTys" (ppr ty) - -getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type) -getEqPredTys_maybe ty - = case splitTyConApp_maybe ty of - Just (tc, [_, _, ty1, ty2]) - | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2) - | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2) - _ -> Nothing - -getEqPredRole :: PredType -> Role -getEqPredRole ty = eqRelRole (predTypeEqRel ty) - --- | Get the equality relation relevant for a pred type. -predTypeEqRel :: PredType -> EqRel -predTypeEqRel ty - | Just (tc, _) <- splitTyConApp_maybe ty - , tc `hasKey` eqReprPrimTyConKey - = ReprEq - | otherwise - = NomEq - ------------- Closing over kinds ----------------- -- | Add the kind variables free in the kinds of the tyvars in the given set. @@ -2187,6 +1870,19 @@ isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty isFamFreeTy (CastTy ty _) = isFamFreeTy ty isFamFreeTy (CoercionTy _) = False -- Not sure about this +-- | Does this type classify a core (unlifted) Coercion? +-- At either role nominal or representational +-- (t1 ~# t2) or (t1 ~R# t2) +-- See Note [Types for coercions, predicates, and evidence] in TyCoRep +isCoVarType :: Type -> Bool + -- ToDo: should we check saturation? +isCoVarType ty + | Just tc <- tyConAppTyCon_maybe ty + = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey + | otherwise + = False + + {- ************************************************************************ * * @@ -2706,7 +2402,10 @@ typeKind ty@(ForAllTy {}) (tvs, body) = splitTyVarForAllTys ty body_kind = typeKind body ------------------------------ +--------------------------------------------- +-- Utilities to be used in Unify, which uses "tc" functions +--------------------------------------------- + tcTypeKind :: HasDebugCallStack => Type -> Kind -- No need to expand synonyms tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys @@ -2749,9 +2448,56 @@ tcTypeKind ty@(ForAllTy {}) isPredTy :: HasDebugCallStack => Type -> Bool --- See Note [Types for coercions, predicates, and evidence] +-- See Note [Types for coercions, predicates, and evidence] in TyCoRep isPredTy ty = tcIsConstraintKind (tcTypeKind ty) +-- tcIsConstraintKind stuff only makes sense in the typechecker +-- After that Constraint = Type +-- See Note [coreView vs tcView] +-- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh) +tcIsConstraintKind :: Kind -> Bool +tcIsConstraintKind ty + | Just (tc, args) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here + , isConstraintKindCon tc + = ASSERT2( null args, ppr ty ) True + + | otherwise + = False + +-- | Is this kind equivalent to @*@? +-- +-- This considers 'Constraint' to be distinct from @*@. For a version that +-- treats them as the same type, see 'isLiftedTypeKind'. +tcIsLiftedTypeKind :: Kind -> Bool +tcIsLiftedTypeKind ty + | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here + , tc `hasKey` tYPETyConKey + = isLiftedRuntimeRep arg + | otherwise + = False + +-- | Is this kind equivalent to @TYPE r@ (for some unknown r)? +-- +-- This considers 'Constraint' to be distinct from @*@. +tcIsRuntimeTypeKind :: Kind -> Bool +tcIsRuntimeTypeKind ty + | Just (tc, _) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here + , tc `hasKey` tYPETyConKey + = True + | otherwise + = False + +tcReturnsConstraintKind :: Kind -> Bool +-- True <=> the Kind ultimately returns a Constraint +-- E.g. * -> Constraint +-- forall k. k -> Constraint +tcReturnsConstraintKind kind + | Just kind' <- tcView kind = tcReturnsConstraintKind kind' +tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty +tcReturnsConstraintKind (FunTy { ft_res = ty }) = tcReturnsConstraintKind ty +tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc +tcReturnsConstraintKind _ = False + -------------------------- typeLiteralKind :: TyLit -> Kind typeLiteralKind (NumTyLit {}) = typeNatKind diff --git a/testsuite/tests/parser/should_run/CountParserDeps.hs b/testsuite/tests/parser/should_run/CountParserDeps.hs index d0de0b9e11..67a2eef8c8 100644 --- a/testsuite/tests/parser/should_run/CountParserDeps.hs +++ b/testsuite/tests/parser/should_run/CountParserDeps.hs @@ -29,7 +29,9 @@ main = do [libdir] <- getArgs modules <- parserDeps libdir let num = sizeUniqSet modules - unless (num < 160) $ exitWith (ExitFailure num) +-- print num +-- print (map moduleNameString $ nonDetEltsUniqSet modules) + unless (num < 165) $ exitWith (ExitFailure num) parserDeps :: FilePath -> IO (UniqSet ModuleName) parserDeps libdir = diff --git a/testsuite/tests/plugins/hole-fit-plugin/HoleFitPlugin.hs b/testsuite/tests/plugins/hole-fit-plugin/HoleFitPlugin.hs index 2a04742a53..2692dbe665 100644 --- a/testsuite/tests/plugins/hole-fit-plugin/HoleFitPlugin.hs +++ b/testsuite/tests/plugins/hole-fit-plugin/HoleFitPlugin.hs @@ -7,7 +7,7 @@ import TcHoleErrors import Data.List (stripPrefix, sortOn) -import TcRnTypes +import Constraint import TcRnMonad |