diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-07-04 15:17:54 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-07-05 10:44:23 +0100 |
| commit | 45f44e2c9d5db2f25c52abb402f197c20579400f (patch) | |
| tree | f2d09ea5cfa5d0c414e9bff8592595081d2610aa | |
| parent | 14dfdf6a0a3364e2d3ae6f6839ef65bb24df4ebf (diff) | |
| download | haskell-45f44e2c9d5db2f25c52abb402f197c20579400f.tar.gz | |
Refactor validity checking for constraints
There are several changes here.
* TcInteract has gotten too big, so I moved all the class-instance
matching out of TcInteract into a new module ClsInst. It parallels
the FamInst module.
The main export of ClsInst is matchGlobalInst.
This now works in TcM not TcS.
* A big reason to make matchGlobalInst work in TcM is that we can
then use it from TcValidity.checkSimplifiableClassConstraint.
That extends checkSimplifiableClassConstraint to work uniformly
for built-in instances, which means that we now get a warning
if we have givens (Typeable x, KnownNat n); see Trac #15322.
* This change also made me refactor LookupInstResult, in particular
by adding the InstanceWhat field. I also changed the name of the
type to ClsInstResult.
Then instead of matchGlobalInst reporting a staging error (which is
inappropriate for the call from TcValidity), we can do so in
TcInteract.checkInstanceOK.
* In TcValidity, we now check quantified constraints for termination.
For example, this signature should be rejected:
f :: (forall a. Eq (m a) => Eq (m a)) => blah
as discussed in Trac #15316. The main change here is that
TcValidity.check_pred_help now uses classifyPredType, and has a
case for ForAllPred which it didn't before.
This had knock-on refactoring effects in TcValidity.
23 files changed, 881 insertions, 686 deletions
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index 01628dcad1..d4a1dc3c6e 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -437,6 +437,7 @@ Library WorkWrap WwLib FamInst + ClsInst Inst TcAnnotations TcArrows diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs new file mode 100644 index 0000000000..b8ab2bfea2 --- /dev/null +++ b/compiler/typecheck/ClsInst.hs @@ -0,0 +1,586 @@ +{-# LANGUAGE CPP #-} + +module ClsInst ( + matchGlobalInst, + ClsInstResult(..), + InstanceWhat(..), safeOverlap + ) where + +#include "HsVersions.h" + +import GhcPrelude + +import TcEnv +import TcRnMonad +import TcType +import TcMType +import TcEvidence +import RnEnv( addUsedGRE ) +import RdrName( lookupGRE_FieldLabel ) +import InstEnv +import Inst( instDFunType ) +import FamInst( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst ) + +import TysWiredIn +import TysPrim( eqPrimTyCon, eqReprPrimTyCon ) +import PrelNames + +import Id +import Type +import Kind( isConstraintKind ) +import MkCore ( mkStringExprFS, mkNaturalExpr ) + +import Unique ( hasKey ) +import Name ( Name ) +import Var ( DFunId ) +import DataCon +import TyCon +import Class +import DynFlags +import Outputable +import Util( splitAtList, fstOf3 ) +import Data.Maybe + +{- ******************************************************************* +* * + Class lookup +* * +**********************************************************************-} + +-- | Indicates if Instance met the Safe Haskell overlapping instances safety +-- check. +-- +-- See Note [Safe Haskell Overlapping Instances] in TcSimplify +-- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify +type SafeOverlapping = Bool + +data ClsInstResult + = NoInstance -- Definitely no instance + + | OneInst { cir_new_theta :: [TcPredType] + , cir_mk_ev :: [EvExpr] -> EvTerm + , cir_what :: InstanceWhat } + + | NotSure -- Multiple matches and/or one or more unifiers + +data InstanceWhat + = BuiltinInstance + | LocalInstance + | TopLevInstance { iw_dfun_id :: DFunId + , iw_safe_over :: SafeOverlapping } + +instance Outputable ClsInstResult where + ppr NoInstance = text "NoInstance" + ppr NotSure = text "NotSure" + ppr (OneInst { cir_new_theta = ev + , cir_what = what }) + = text "OneInst" <+> vcat [ppr ev, ppr what] + +instance Outputable InstanceWhat where + ppr BuiltinInstance = text "built-in instance" + ppr LocalInstance = text "locally-quantified instance" + ppr (TopLevInstance { iw_safe_over = so }) + = text "top-level instance" <+> (text $ if so then "[safe]" else "[unsafe]") + +safeOverlap :: InstanceWhat -> Bool +safeOverlap (TopLevInstance { iw_safe_over = so }) = so +safeOverlap _ = True + +matchGlobalInst :: DynFlags + -> Bool -- True <=> caller is the short-cut solver + -- See Note [Shortcut solving: overlap] + -> Class -> [Type] -> TcM ClsInstResult +matchGlobalInst dflags short_cut clas tys + | cls_name == knownNatClassName = matchKnownNat clas tys + | cls_name == knownSymbolClassName = matchKnownSymbol clas tys + | isCTupleClass clas = matchCTuple clas tys + | cls_name == typeableClassName = matchTypeable clas tys + | clas `hasKey` heqTyConKey = matchLiftedEquality tys + | clas `hasKey` coercibleTyConKey = matchLiftedCoercible tys + | cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys + | otherwise = matchInstEnv dflags short_cut clas tys + where + cls_name = className clas + + +{- ******************************************************************** +* * + Looking in the instance environment +* * +***********************************************************************-} + + +matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult +matchInstEnv dflags short_cut_solver clas tys + = do { instEnvs <- tcGetInstEnvs + ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy] + (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys + safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps) + ; traceTc "matchInstEnv" $ + vcat [ text "goal:" <+> ppr clas <+> ppr tys + , text "matches:" <+> ppr matches + , text "unify:" <+> ppr unify ] + ; case (matches, unify, safeHaskFail) of + + -- Nothing matches + ([], [], _) + -> do { traceTc "matchClass not matching" (ppr pred) + ; return NoInstance } + + -- A single match (& no safe haskell failure) + ([(ispec, inst_tys)], [], False) + | short_cut_solver -- Called from the short-cut solver + , isOverlappable ispec + -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT + -- then don't let the short-cut solver choose it, because a + -- later instance might overlap it. Trac #14434 is an example + -- See Note [Shortcut solving: overlap] + -> do { traceTc "matchClass: ignoring overlappable" (ppr pred) + ; return NotSure } + + | otherwise + -> do { let dfun_id = instanceDFunId ispec + ; traceTc "matchClass success" $ + vcat [text "dict" <+> ppr pred, + text "witness" <+> ppr dfun_id + <+> ppr (idType dfun_id) ] + -- Record that this dfun is needed + ; match_one (null unsafeOverlaps) dfun_id inst_tys } + + -- More than one matches (or Safe Haskell fail!). Defer any + -- reactions of a multitude until we learn more about the reagent + _ -> do { traceTc "matchClass multiple matches, deferring choice" $ + vcat [text "dict" <+> ppr pred, + text "matches" <+> ppr matches] + ; return NotSure } } + where + pred = mkClassPred clas tys + +match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcM ClsInstResult + -- See Note [DFunInstType: instantiating types] in InstEnv +match_one so dfun_id mb_inst_tys + = do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys) + ; (tys, theta) <- instDFunType dfun_id mb_inst_tys + ; traceTc "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta) + ; return $ OneInst { cir_new_theta = theta + , cir_mk_ev = evDFunApp dfun_id tys + , cir_what = TopLevInstance { iw_dfun_id = dfun_id + , iw_safe_over = so } } } + + +{- ******************************************************************** +* * + Class lookup for CTuples +* * +***********************************************************************-} + +matchCTuple :: Class -> [Type] -> TcM ClsInstResult +matchCTuple clas tys -- (isCTupleClass clas) holds + = return (OneInst { cir_new_theta = tys + , cir_mk_ev = tuple_ev + , cir_what = BuiltinInstance }) + -- The dfun *is* the data constructor! + where + data_con = tyConSingleDataCon (classTyCon clas) + tuple_ev = evDFunApp (dataConWrapId data_con) tys + +{- ******************************************************************** +* * + Class lookup for Literals +* * +***********************************************************************-} + +{- +Note [KnownNat & KnownSymbol and EvLit] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A part of the type-level literals implementation are the classes +"KnownNat" and "KnownSymbol", which provide a "smart" constructor for +defining singleton values. Here is the key stuff from GHC.TypeLits + + class KnownNat (n :: Nat) where + natSing :: SNat n + + newtype SNat (n :: Nat) = SNat Integer + +Conceptually, this class has infinitely many instances: + + instance KnownNat 0 where natSing = SNat 0 + instance KnownNat 1 where natSing = SNat 1 + instance KnownNat 2 where natSing = SNat 2 + ... + +In practice, we solve `KnownNat` predicates in the type-checker +(see typecheck/TcInteract.hs) because we can't have infinitely many instances. +The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`. + +We make the following assumptions about dictionaries in GHC: + 1. The "dictionary" for classes with a single method---like `KnownNat`---is + a newtype for the type of the method, so using a evidence amounts + to a coercion, and + 2. Newtypes use the same representation as their definition types. + +So, the evidence for `KnownNat` is just a value of the representation type, +wrapped in two newtype constructors: one to make it into a `SNat` value, +and another to make it into a `KnownNat` dictionary. + +Also note that `natSing` and `SNat` are never actually exposed from the +library---they are just an implementation detail. Instead, users see +a more convenient function, defined in terms of `natSing`: + + natVal :: KnownNat n => proxy n -> Integer + +The reason we don't use this directly in the class is that it is simpler +and more efficient to pass around an integer rather than an entire function, +especially when the `KnowNat` evidence is packaged up in an existential. + +The story for kind `Symbol` is analogous: + * class KnownSymbol + * newtype SSymbol + * Evidence: a Core literal (e.g. mkNaturalExpr) +-} + +matchKnownNat :: Class -> [Type] -> TcM ClsInstResult +matchKnownNat clas [ty] -- clas = KnownNat + | Just n <- isNumLitTy ty = do + et <- mkNaturalExpr n + makeLitDict clas ty et +matchKnownNat _ _ = return NoInstance + +matchKnownSymbol :: Class -> [Type] -> TcM ClsInstResult +matchKnownSymbol clas [ty] -- clas = KnownSymbol + | Just s <- isStrLitTy ty = do + et <- mkStringExprFS s + makeLitDict clas ty et +matchKnownSymbol _ _ = return NoInstance + +makeLitDict :: Class -> Type -> EvExpr -> TcM ClsInstResult +-- makeLitDict adds a coercion that will convert the literal into a dictionary +-- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit] +-- in TcEvidence. The coercion happens in 2 steps: +-- +-- Integer -> SNat n -- representation of literal to singleton +-- SNat n -> KnownNat n -- singleton to dictionary +-- +-- The process is mirrored for Symbols: +-- String -> SSymbol n +-- SSymbol n -> KnownSymbol n +makeLitDict clas ty et + | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] + -- co_dict :: KnownNat n ~ SNat n + , [ meth ] <- classMethods clas + , Just tcRep <- tyConAppTyCon_maybe -- SNat + $ funResultTy -- SNat n + $ dropForAlls -- KnownNat n => SNat n + $ idType meth -- forall n. KnownNat n => SNat n + , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] + -- SNat n ~ Integer + , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep)) + = return $ OneInst { cir_new_theta = [] + , cir_mk_ev = \_ -> ev_tm + , cir_what = BuiltinInstance } + + | otherwise + = pprPanic "makeLitDict" $ + text "Unexpected evidence for" <+> ppr (className clas) + $$ vcat (map (ppr . idType) (classMethods clas)) + +{- ******************************************************************** +* * + Class lookup for Typeable +* * +***********************************************************************-} + +-- | Assumes that we've checked that this is the 'Typeable' class, +-- and it was applied to the correct argument. +matchTypeable :: Class -> [Type] -> TcM ClsInstResult +matchTypeable clas [k,t] -- clas = Typeable + -- For the first two cases, See Note [No Typeable for polytypes or qualified types] + | isForAllTy k = return NoInstance -- Polytype + | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type + + -- Now cases that do work + | k `eqType` typeNatKind = doTyLit knownNatClassName t + | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t + | isConstraintKind t = doTyConApp clas t constraintKindTyCon [] + | Just (arg,ret) <- splitFunTy_maybe t = doFunTy clas t arg ret + | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)] + , onlyNamedBndrsApplied tc ks = doTyConApp clas t tc ks + | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt + +matchTypeable _ _ = return NoInstance + +-- | Representation for a type @ty@ of the form @arg -> ret@. +doFunTy :: Class -> Type -> Type -> Type -> TcM ClsInstResult +doFunTy clas ty arg_ty ret_ty + = return $ OneInst { cir_new_theta = preds + , cir_mk_ev = mk_ev + , cir_what = BuiltinInstance } + where + preds = map (mk_typeable_pred clas) [arg_ty, ret_ty] + mk_ev [arg_ev, ret_ev] = evTypeable ty $ + EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev) + mk_ev _ = panic "TcInteract.doFunTy" + + +-- | Representation for type constructor applied to some kinds. +-- 'onlyNamedBndrsApplied' has ensured that this application results in a type +-- of monomorphic kind (e.g. all kind variables have been instantiated). +doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult +doTyConApp clas ty tc kind_args + | Just _ <- tyConRepName_maybe tc + = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args) + , cir_mk_ev = mk_ev + , cir_what = BuiltinInstance } + | otherwise + = return NoInstance + where + mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds) + +-- | Representation for TyCon applications of a concrete kind. We just use the +-- kind itself, but first we must make sure that we've instantiated all kind- +-- polymorphism, but no more. +onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool +onlyNamedBndrsApplied tc ks + = all isNamedTyConBinder used_bndrs && + not (any isNamedTyConBinder leftover_bndrs) + where + bndrs = tyConBinders tc + (used_bndrs, leftover_bndrs) = splitAtList ks bndrs + +doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult +-- Representation for an application of a type to a type-or-kind. +-- This may happen when the type expression starts with a type variable. +-- Example (ignoring kind parameter): +-- Typeable (f Int Char) --> +-- (Typeable (f Int), Typeable Char) --> +-- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps) +-- Typeable f +doTyApp clas ty f tk + | isForAllTy (typeKind f) + = return NoInstance -- We can't solve until we know the ctr. + | otherwise + = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk] + , cir_mk_ev = mk_ev + , cir_what = BuiltinInstance } + where + mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2) + mk_ev _ = panic "doTyApp" + + +-- Emit a `Typeable` constraint for the given type. +mk_typeable_pred :: Class -> Type -> PredType +mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ] + + -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal + -- we generate a sub-goal for the appropriate class. + -- See Note [Typeable for Nat and Symbol] +doTyLit :: Name -> Type -> TcM ClsInstResult +doTyLit kc t = do { kc_clas <- tcLookupClass kc + ; let kc_pred = mkClassPred kc_clas [ t ] + mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev) + mk_ev _ = panic "doTyLit" + ; return (OneInst { cir_new_theta = [kc_pred] + , cir_mk_ev = mk_ev + , cir_what = BuiltinInstance }) } + +{- Note [Typeable (T a b c)] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For type applications we always decompose using binary application, +via doTyApp, until we get to a *kind* instantiation. Example + Proxy :: forall k. k -> * + +To solve Typeable (Proxy (* -> *) Maybe) we + - First decompose with doTyApp, + to get (Typeable (Proxy (* -> *))) and Typeable Maybe + - Then solve (Typeable (Proxy (* -> *))) with doTyConApp + +If we attempt to short-cut by solving it all at once, via +doTyConApp + +(this note is sadly truncated FIXME) + + +Note [No Typeable for polytypes or qualified types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We do not support impredicative typeable, such as + Typeable (forall a. a->a) + Typeable (Eq a => a -> a) + Typeable (() => Int) + Typeable (((),()) => Int) + +See Trac #9858. For forall's the case is clear: we simply don't have +a TypeRep for them. For qualified but not polymorphic types, like +(Eq a => a -> a), things are murkier. But: + + * We don't need a TypeRep for these things. TypeReps are for + monotypes only. + + * Perhaps we could treat `=>` as another type constructor for `Typeable` + purposes, and thus support things like `Eq Int => Int`, however, + at the current state of affairs this would be an odd exception as + no other class works with impredicative types. + For now we leave it off, until we have a better story for impredicativity. + + +Note [Typeable for Nat and Symbol] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have special Typeable instances for Nat and Symbol. Roughly we +have this instance, implemented here by doTyLit: + instance KnownNat n => Typeable (n :: Nat) where + typeRep = tyepNatTypeRep @n +where + Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a + +Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a +runtime value 'n'; it turns it into a string with 'show' and uses +that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon. +See #10348. + +Because of this rule it's inadvisable (see #15322) to have a constraint + f :: (Typeable (n :: Nat)) => blah +in a function signature; it gives rise to overlap problems just as +if you'd written + f :: Eq [a] => blah +-} + +{- ******************************************************************** +* * + Class lookup for lifted equality +* * +***********************************************************************-} + +-- See also Note [The equality types story] in TysPrim +matchLiftedEquality :: [Type] -> TcM ClsInstResult +matchLiftedEquality args + = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ] + , cir_mk_ev = evDFunApp (dataConWrapId heqDataCon) args + , cir_what = BuiltinInstance }) + +-- See also Note [The equality types story] in TysPrim +matchLiftedCoercible :: [Type] -> TcM ClsInstResult +matchLiftedCoercible args@[k, t1, t2] + = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ] + , cir_mk_ev = evDFunApp (dataConWrapId coercibleDataCon) + args + , cir_what = BuiltinInstance }) + where + args' = [k, k, t1, t2] +matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args) + + +{- ******************************************************************** +* * + Class lookup for overloaded record fields +* * +***********************************************************************-} + +{- +Note [HasField instances] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + data T y = MkT { foo :: [y] } + +and `foo` is in scope. Then GHC will automatically solve a constraint like + + HasField "foo" (T Int) b + +by emitting a new wanted + + T alpha -> [alpha] ~# T Int -> b + +and building a HasField dictionary out of the selector function `foo`, +appropriately cast. + +The HasField class is defined (in GHC.Records) thus: + + class HasField (x :: k) r a | x r -> a where + getField :: r -> a + +Since this is a one-method class, it is represented as a newtype. +Hence we can solve `HasField "foo" (T Int) b` by taking an expression +of type `T Int -> b` and casting it using the newtype coercion. +Note that + + foo :: forall y . T y -> [y] + +so the expression we construct is + + foo @alpha |> co + +where + + co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b + +is built from + + co1 :: (T alpha -> [alpha]) ~# (T Int -> b) + +which is the new wanted, and + + co2 :: (T Int -> b) ~# HasField "foo" (T Int) b + +which can be derived from the newtype coercion. + +If `foo` is not in scope, or has a higher-rank or existentially +quantified type, then the constraint is not solved automatically, but +may be solved by a user-supplied HasField instance. Similarly, if we +encounter a HasField constraint where the field is not a literal +string, or does not belong to the type, then we fall back on the +normal constraint solver behaviour. +-} + +-- See Note [HasField instances] +matchHasField :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult +matchHasField dflags short_cut clas tys + = do { fam_inst_envs <- tcGetFamInstEnvs + ; rdr_env <- getGlobalRdrEnv + ; case tys of + -- We are matching HasField {k} x r a... + [_k_ty, x_ty, r_ty, a_ty] + -- x should be a literal string + | Just x <- isStrLitTy x_ty + -- r should be an applied type constructor + , Just (tc, args) <- tcSplitTyConApp_maybe r_ty + -- use representation tycon (if data family); it has the fields + , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args) + -- x should be a field of r + , Just fl <- lookupTyConFieldLabel x r_tc + -- the field selector should be in scope + , Just gre <- lookupGRE_FieldLabel rdr_env fl + + -> do { sel_id <- tcLookupId (flSelector fl) + ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id + + -- The first new wanted constraint equates the actual + -- type of the selector with the type (r -> a) within + -- the HasField x r a dictionary. The preds will + -- typically be empty, but if the datatype has a + -- "stupid theta" then we have to include it here. + ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds + + -- Use the equality proof to cast the selector Id to + -- type (r -> a), then use the newtype coercion to cast + -- it to a HasField dictionary. + mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co + where + co = mkTcSubCo (evTermCoercion (EvExpr ev1)) + `mkTcTransCo` mkTcSymCo co2 + mk_ev [] = panic "matchHasField.mk_ev" + + Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas) + tys + + tvs = mkTyVarTys (map snd tv_prs) + + -- The selector must not be "naughty" (i.e. the field + -- cannot have an existentially quantified type), and + -- it must not be higher-rank. + ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty + then do { addUsedGRE True gre + ; return OneInst { cir_new_theta = theta + , cir_mk_ev = mk_ev + , cir_what = BuiltinInstance } } + else matchInstEnv dflags short_cut clas tys } + + _ -> matchInstEnv dflags short_cut clas tys } diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 5d3a98854c..18d952501d 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -8,7 +8,6 @@ module TcInteract ( #include "HsVersions.h" import GhcPrelude - import BasicTypes ( SwapFlag(..), isSwapped, infinity, IntWithInf, intGtLimit ) import TcCanonical @@ -16,38 +15,23 @@ import TcFlatten import TcUnify( canSolveByUnification ) import VarSet import Type -import Kind( isConstraintKind ) -import InstEnv( DFunInstType, lookupInstEnv - , instanceDFunId, isOverlappable ) +import InstEnv( DFunInstType ) import CoAxiom( sfInteractTop, sfInteractInert ) -import TcMType (newMetaTyVars) - import Var import TcType -import Name -import RdrName ( lookupGRE_FieldLabel ) -import PrelNames ( knownNatClassName, knownSymbolClassName, - typeableClassName, - coercibleTyConKey, - hasFieldClassName, +import PrelNames ( coercibleTyConKey, heqTyConKey, eqTyConKey, ipClassKey ) -import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon, - coercibleDataCon, constraintKindTyCon ) -import TysPrim ( eqPrimTyCon, eqReprPrimTyCon ) -import Id( idType, isNaughtyRecordSelector ) import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches ) import Class import TyCon -import DataCon( dataConWrapId ) -import FieldLabel import FunDeps import FamInst +import ClsInst( ClsInstResult(..), InstanceWhat(..), safeOverlap ) import FamInstEnv import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX ) import TcEvidence -import MkCore ( mkStringExprFS, mkNaturalExpr ) import Outputable import TcRnTypes @@ -1127,21 +1111,20 @@ shortCutSolver dflags ev_w ev_i | let pred = ctEvPred ev loc = ctEvLoc ev , ClassPred cls tys <- classifyPredType pred - = do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc + = do { inst_res <- lift $ matchGlobalInst dflags True cls tys ; case inst_res of - OneInst { lir_new_theta = preds - , lir_mk_ev = mk_ev - , lir_safe_over = safeOverlap } - | safeOverlap + OneInst { cir_new_theta = preds + , cir_mk_ev = mk_ev + , cir_what = what } + | safeOverlap what , all isTyFamFree preds -- Note [Shortcut solving: type families] -> do { let solved_dicts' = addDict solved_dicts cls tys ev - loc' = bumpCtLocDepth loc -- solved_dicts': it is important that we add our goal -- to the cache before we solve! Otherwise we may end -- up in a loop while solving recursive dictionaries. ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds) - ; lift $ checkReductionDepth loc pred + ; loc' <- lift $ checkInstanceOK loc what pred ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds -- Emit work for subgoals but use our local cache @@ -2232,8 +2215,9 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls = do { dflags <- getDynFlags ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc ; case lkup_res of - OneInst { lir_safe_over = s } - -> do { unless s $ insertSafeOverlapFailureTcS work_item + OneInst { cir_what = what } + -> do { unless (safeOverlap what) $ + insertSafeOverlapFailureTcS work_item ; when (isWanted ev) $ addSolvedDict ev cls xis ; chooseInstance work_item lkup_res } _ -> -- NoInstance or NotSure @@ -2264,53 +2248,66 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) -chooseInstance :: Ct -> LookupInstResult -> TcS (StopOrContinue Ct) +chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct) chooseInstance work_item - (OneInst { lir_new_theta = theta - , lir_mk_ev = mk_ev }) + (OneInst { cir_new_theta = theta + , cir_what = what + , cir_mk_ev = mk_ev }) = do { traceTcS "doTopReact/found instance for" $ ppr ev - ; checkReductionDepth deeper_loc pred - ; if isDerived ev then finish_derived theta - else finish_wanted theta mk_ev } + ; deeper_loc <- checkInstanceOK loc what pred + ; if isDerived ev then finish_derived deeper_loc theta + else finish_wanted deeper_loc theta mk_ev } where ev = ctEvidence work_item pred = ctEvPred ev loc = ctEvLoc ev - origin = ctLocOrigin loc - deeper_loc = zap_origin (bumpCtLocDepth loc) - - zap_origin loc -- After applying an instance we can set ScOrigin to - -- infinity, so that prohibitedSuperClassSolve never fires - | ScOrigin {} <- origin - = setCtLocOrigin loc (ScOrigin infinity) - | otherwise - = loc - finish_wanted :: [TcPredType] + finish_wanted :: CtLoc -> [TcPredType] -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct) -- Precondition: evidence term matches the predicate workItem - finish_wanted theta mk_ev + finish_wanted loc theta mk_ev = do { evb <- getTcEvBindsVar ; if isNoEvBindsVar evb then -- See Note [Instances in no-evidence implications] continueWith work_item else - do { evc_vars <- mapM (newWanted deeper_loc) theta + do { evc_vars <- mapM (newWanted loc) theta ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars)) ; emitWorkNC (freshGoals evc_vars) ; stopWith ev "Dict/Top (solved wanted)" } } - finish_derived theta -- Use type-class instances for Deriveds, in the hope - = -- of generating some improvements - -- C.f. Example 3 of Note [The improvement story] - -- It's easy because no evidence is involved - do { emitNewDeriveds deeper_loc theta - ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc)) + finish_derived loc theta + = -- Use type-class instances for Deriveds, in the hope + -- of generating some improvements + -- C.f. Example 3 of Note [The improvement story] + -- It's easy because no evidence is involved + do { emitNewDeriveds loc theta + ; traceTcS "finish_derived" (ppr (ctl_depth loc)) ; stopWith ev "Dict/Top (solved derived)" } chooseInstance work_item lookup_res = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res) +checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc +-- Check that it's OK to use this insstance: +-- (a) the use is well staged in the Template Haskell sense +-- (b) we have not recursed too deep +-- Returns the CtLoc to used for sub-goals +checkInstanceOK loc what pred + = do { checkWellStagedDFun loc what pred + ; checkReductionDepth deeper_loc pred + ; return deeper_loc } + where + deeper_loc = zap_origin (bumpCtLocDepth loc) + origin = ctLocOrigin loc + + zap_origin loc -- After applying an instance we can set ScOrigin to + -- infinity, so that prohibitedSuperClassSolve never fires + | ScOrigin {} <- origin + = setCtLocOrigin loc (ScOrigin infinity) + | otherwise + = loc + {- Note [Instances in no-evidence implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In Trac #15290 we had @@ -2331,40 +2328,10 @@ This test arranges to ignore the instance-based solution under these (rare) circumstances. It's sad, but I really don't see what else we can do. -} -{- ******************************************************************* -* * - Class lookup -* * -**********************************************************************-} - --- | Indicates if Instance met the Safe Haskell overlapping instances safety --- check. --- --- See Note [Safe Haskell Overlapping Instances] in TcSimplify --- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify -type SafeOverlapping = Bool - -data LookupInstResult - = NoInstance -- Definitely no instance - - | OneInst { lir_new_theta :: [TcPredType] - , lir_mk_ev :: [EvExpr] -> EvTerm - , lir_safe_over :: SafeOverlapping } - - | NotSure -- Multiple matches and/or one or more unifiers - -instance Outputable LookupInstResult where - ppr NoInstance = text "NoInstance" - ppr NotSure = text "NotSure" - ppr (OneInst { lir_new_theta = ev - , lir_safe_over = s }) - = text "OneInst" <+> vcat [ppr ev, ss] - where ss = text $ if s then "[safe]" else "[unsafe]" - matchClassInst :: DynFlags -> InertSet -> Class -> [Type] - -> CtLoc -> TcS LookupInstResult + -> CtLoc -> TcS ClsInstResult matchClassInst dflags inerts clas tys loc -- First check whether there is an in-scope Given that could -- match this constraint. In that case, do not use any instance @@ -2393,28 +2360,12 @@ matchClassInst dflags inerts clas tys loc ; return local_res } NoInstance -- No local instances, so try global ones - -> do { global_res <- matchGlobalInst dflags False clas tys loc + -> do { global_res <- matchGlobalInst dflags False clas tys ; traceTcS "} matchClassInst global result" $ ppr global_res ; return global_res } } where pred = mkClassPred clas tys -matchGlobalInst :: DynFlags - -> Bool -- True <=> caller is the short-cut solver - -- See Note [Shortcut solving: overlap] - -> Class -> [Type] -> CtLoc -> TcS LookupInstResult -matchGlobalInst dflags short_cut clas tys loc - | cls_name == knownNatClassName = matchKnownNat clas tys - | cls_name == knownSymbolClassName = matchKnownSymbol clas tys - | isCTupleClass clas = matchCTuple clas tys - | cls_name == typeableClassName = matchTypeable clas tys - | clas `hasKey` heqTyConKey = matchLiftedEquality tys - | clas `hasKey` coercibleTyConKey = matchLiftedCoercible tys - | cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys loc - | otherwise = matchInstEnv dflags short_cut clas tys loc - where - cls_name = className clas - -- | If a class is "naturally coherent", then we needn't worry at all, in any -- way, about overlapping/incoherent instances. Just solve the thing! -- See Note [Naturally coherent classes] @@ -2581,7 +2532,7 @@ those instances to build evidence to pass to f. That's just the nullary case of what's happening here. -} -matchLocalInst :: TcPredType -> CtLoc -> TcS LookupInstResult +matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult -- Try any Given quantified constraints, which are -- effectively just local instance declarations. matchLocalInst pred loc @@ -2590,7 +2541,11 @@ matchLocalInst pred loc ([], False) -> return NoInstance ([(dfun_ev, inst_tys)], unifs) | not unifs - -> match_one pred loc True (ctEvEvId dfun_ev) inst_tys + -> do { let dfun_id = ctEvEvId dfun_ev + ; (tys, theta) <- instDFunType dfun_id inst_tys + ; return $ OneInst { cir_new_theta = theta + , cir_mk_ev = evDFunApp dfun_id tys + , cir_what = LocalInstance } } _ -> return NotSure } where pred_tv_set = tyCoVarsOfType pred @@ -2620,478 +2575,3 @@ matchLocalInst pred loc this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc (matches, unif) = match_local_inst qcis -matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult -matchInstEnv dflags short_cut_solver clas tys loc - = do { instEnvs <- getInstEnvs - ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy] - (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys - safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps) - ; traceTcS "matchInstEnv" $ - vcat [ text "goal:" <+> ppr clas <+> ppr tys - , text "matches:" <+> ppr matches - , text "unify:" <+> ppr unify ] - ; case (matches, unify, safeHaskFail) of - - -- Nothing matches - ([], [], _) - -> do { traceTcS "matchClass not matching" (ppr pred) - ; return NoInstance } - - -- A single match (& no safe haskell failure) - ([(ispec, inst_tys)], [], False) - | short_cut_solver -- Called from the short-cut solver - , isOverlappable ispec - -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT - -- then don't let the short-cut solver choose it, because a - -- later instance might overlap it. Trac #14434 is an example - -- See Note [Shortcut solving: overlap] - -> do { traceTcS "matchClass: ignoring overlappable" (ppr pred) - ; return NotSure } - - | otherwise - -> do { let dfun_id = instanceDFunId ispec - ; traceTcS "matchClass success" $ - vcat [text "dict" <+> ppr pred, - text "witness" <+> ppr dfun_id - <+> ppr (idType dfun_id) ] - -- Record that this dfun is needed - ; match_one pred loc (null unsafeOverlaps) dfun_id inst_tys } - - -- More than one matches (or Safe Haskell fail!). Defer any - -- reactions of a multitude until we learn more about the reagent - _ -> do { traceTcS "matchClass multiple matches, deferring choice" $ - vcat [text "dict" <+> ppr pred, - text "matches" <+> ppr matches] - ; return NotSure } } - where - pred = mkClassPred clas tys - -match_one :: TcPredType -> CtLoc -> SafeOverlapping - -> DFunId -> [DFunInstType] -> TcS LookupInstResult - -- See Note [DFunInstType: instantiating types] in InstEnv -match_one pred loc so dfun_id mb_inst_tys - = do { traceTcS "match_one" (ppr dfun_id $$ ppr mb_inst_tys) - ; checkWellStagedDFun pred dfun_id loc - ; (tys, theta) <- instDFunType dfun_id mb_inst_tys - ; traceTcS "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta) - ; return $ OneInst { lir_new_theta = theta - , lir_mk_ev = evDFunApp dfun_id tys - , lir_safe_over = so } } - - -{- ******************************************************************** -* * - Class lookup for CTuples -* * -***********************************************************************-} - -matchCTuple :: Class -> [Type] -> TcS LookupInstResult -matchCTuple clas tys -- (isCTupleClass clas) holds - = return (OneInst { lir_new_theta = tys - , lir_mk_ev = tuple_ev - , lir_safe_over = True }) - -- The dfun *is* the data constructor! - where - data_con = tyConSingleDataCon (classTyCon clas) - tuple_ev = evDFunApp (dataConWrapId data_con) tys - -{- ******************************************************************** -* * - Class lookup for Literals -* * -***********************************************************************-} - -{- -Note [KnownNat & KnownSymbol and EvLit] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A part of the type-level literals implementation are the classes -"KnownNat" and "KnownSymbol", which provide a "smart" constructor for -defining singleton values. Here is the key stuff from GHC.TypeLits - - class KnownNat (n :: Nat) where - natSing :: SNat n - - newtype SNat (n :: Nat) = SNat Integer - -Conceptually, this class has infinitely many instances: - - instance KnownNat 0 where natSing = SNat 0 - instance KnownNat 1 where natSing = SNat 1 - instance KnownNat 2 where natSing = SNat 2 - ... - -In practice, we solve `KnownNat` predicates in the type-checker -(see typecheck/TcInteract.hs) because we can't have infinitely many instances. -The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`. - -We make the following assumptions about dictionaries in GHC: - 1. The "dictionary" for classes with a single method---like `KnownNat`---is - a newtype for the type of the method, so using a evidence amounts - to a coercion, and - 2. Newtypes use the same representation as their definition types. - -So, the evidence for `KnownNat` is just a value of the representation type, -wrapped in two newtype constructors: one to make it into a `SNat` value, -and another to make it into a `KnownNat` dictionary. - -Also note that `natSing` and `SNat` are never actually exposed from the -library---they are just an implementation detail. Instead, users see -a more convenient function, defined in terms of `natSing`: - - natVal :: KnownNat n => proxy n -> Integer - -The reason we don't use this directly in the class is that it is simpler -and more efficient to pass around an integer rather than an entire function, -especially when the `KnowNat` evidence is packaged up in an existential. - -The story for kind `Symbol` is analogous: - * class KnownSymbol - * newtype SSymbol - * Evidence: a Core literal (e.g. mkNaturalExpr) --} - -matchKnownNat :: Class -> [Type] -> TcS LookupInstResult -matchKnownNat clas [ty] -- clas = KnownNat - | Just n <- isNumLitTy ty = do - et <- mkNaturalExpr n - makeLitDict clas ty et -matchKnownNat _ _ = return NoInstance - -matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult -matchKnownSymbol clas [ty] -- clas = KnownSymbol - | Just s <- isStrLitTy ty = do - et <- mkStringExprFS s - makeLitDict clas ty et -matchKnownSymbol _ _ = return NoInstance - -makeLitDict :: Class -> Type -> EvExpr -> TcS LookupInstResult --- makeLitDict adds a coercion that will convert the literal into a dictionary --- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit] --- in TcEvidence. The coercion happens in 2 steps: --- --- Integer -> SNat n -- representation of literal to singleton --- SNat n -> KnownNat n -- singleton to dictionary --- --- The process is mirrored for Symbols: --- String -> SSymbol n --- SSymbol n -> KnownSymbol n -makeLitDict clas ty et - | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] - -- co_dict :: KnownNat n ~ SNat n - , [ meth ] <- classMethods clas - , Just tcRep <- tyConAppTyCon_maybe -- SNat - $ funResultTy -- SNat n - $ dropForAlls -- KnownNat n => SNat n - $ idType meth -- forall n. KnownNat n => SNat n - , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] - -- SNat n ~ Integer - , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep)) - = return $ OneInst { lir_new_theta = [] - , lir_mk_ev = \_ -> ev_tm - , lir_safe_over = True } - - | otherwise - = panicTcS (text "Unexpected evidence for" <+> ppr (className clas) - $$ vcat (map (ppr . idType) (classMethods clas))) - -{- ******************************************************************** -* * - Class lookup for Typeable -* * -***********************************************************************-} - --- | Assumes that we've checked that this is the 'Typeable' class, --- and it was applied to the correct argument. -matchTypeable :: Class -> [Type] -> TcS LookupInstResult -matchTypeable clas [k,t] -- clas = Typeable - -- For the first two cases, See Note [No Typeable for polytypes or qualified types] - | isForAllTy k = return NoInstance -- Polytype - | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type - - -- Now cases that do work - | k `eqType` typeNatKind = doTyLit knownNatClassName t - | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t - | isConstraintKind t = doTyConApp clas t constraintKindTyCon [] - | Just (arg,ret) <- splitFunTy_maybe t = doFunTy clas t arg ret - | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)] - , onlyNamedBndrsApplied tc ks = doTyConApp clas t tc ks - | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt - -matchTypeable _ _ = return NoInstance - --- | Representation for a type @ty@ of the form @arg -> ret@. -doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult -doFunTy clas ty arg_ty ret_ty - = return $ OneInst { lir_new_theta = preds - , lir_mk_ev = mk_ev - , lir_safe_over = True } - where - preds = map (mk_typeable_pred clas) [arg_ty, ret_ty] - mk_ev [arg_ev, ret_ev] = evTypeable ty $ - EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev) - mk_ev _ = panic "TcInteract.doFunTy" - - --- | Representation for type constructor applied to some kinds. --- 'onlyNamedBndrsApplied' has ensured that this application results in a type --- of monomorphic kind (e.g. all kind variables have been instantiated). -doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult -doTyConApp clas ty tc kind_args - | Just _ <- tyConRepName_maybe tc - = return $ OneInst { lir_new_theta = (map (mk_typeable_pred clas) kind_args) - , lir_mk_ev = mk_ev - , lir_safe_over = True } - | otherwise - = return NoInstance - where - mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds) - --- | Representation for TyCon applications of a concrete kind. We just use the --- kind itself, but first we must make sure that we've instantiated all kind- --- polymorphism, but no more. -onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool -onlyNamedBndrsApplied tc ks - = all isNamedTyConBinder used_bndrs && - not (any isNamedTyConBinder leftover_bndrs) - where - bndrs = tyConBinders tc - (used_bndrs, leftover_bndrs) = splitAtList ks bndrs - -doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult --- Representation for an application of a type to a type-or-kind. --- This may happen when the type expression starts with a type variable. --- Example (ignoring kind parameter): --- Typeable (f Int Char) --> --- (Typeable (f Int), Typeable Char) --> --- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps) --- Typeable f -doTyApp clas ty f tk - | isForAllTy (typeKind f) - = return NoInstance -- We can't solve until we know the ctr. - | otherwise - = return $ OneInst { lir_new_theta = map (mk_typeable_pred clas) [f, tk] - , lir_mk_ev = mk_ev - , lir_safe_over = True } - where - mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2) - mk_ev _ = panic "doTyApp" - - --- Emit a `Typeable` constraint for the given type. -mk_typeable_pred :: Class -> Type -> PredType -mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ] - - -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal - -- we generate a sub-goal for the appropriate class. - -- See Note [Typeable for Nat and Symbol] -doTyLit :: Name -> Type -> TcS LookupInstResult -doTyLit kc t = do { kc_clas <- tcLookupClass kc - ; let kc_pred = mkClassPred kc_clas [ t ] - mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev) - mk_ev _ = panic "doTyLit" - ; return (OneInst { lir_new_theta = [kc_pred] - , lir_mk_ev = mk_ev - , lir_safe_over = True }) } - -{- Note [Typeable (T a b c)] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For type applications we always decompose using binary application, -via doTyApp, until we get to a *kind* instantiation. Example - Proxy :: forall k. k -> * - -To solve Typeable (Proxy (* -> *) Maybe) we - - First decompose with doTyApp, - to get (Typeable (Proxy (* -> *))) and Typeable Maybe - - Then solve (Typeable (Proxy (* -> *))) with doTyConApp - -If we attempt to short-cut by solving it all at once, via -doTyConApp - -(this note is sadly truncated FIXME) - - -Note [No Typeable for polytypes or qualified types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We do not support impredicative typeable, such as - Typeable (forall a. a->a) - Typeable (Eq a => a -> a) - Typeable (() => Int) - Typeable (((),()) => Int) - -See Trac #9858. For forall's the case is clear: we simply don't have -a TypeRep for them. For qualified but not polymorphic types, like -(Eq a => a -> a), things are murkier. But: - - * We don't need a TypeRep for these things. TypeReps are for - monotypes only. - - * Perhaps we could treat `=>` as another type constructor for `Typeable` - purposes, and thus support things like `Eq Int => Int`, however, - at the current state of affairs this would be an odd exception as - no other class works with impredicative types. - For now we leave it off, until we have a better story for impredicativity. - - -Note [Typeable for Nat and Symbol] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We have special Typeable instances for Nat and Symbol. Roughly we -have this instance, implemented here by doTyLit: - instance KnownNat n => Typeable (n :: Nat) where - typeRep = tyepNatTypeRep @n -where - Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a - -Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a -runtime value 'n'; it turns it into a string with 'show' and uses -that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon. -See #10348. - -Because of this rule it's inadvisable (see #15322) to have a constraint - f :: (Typeable (n :: Nat)) => blah -in a function signature; it gives rise to overlap problems just as -if you'd written - f :: Eq [a] => blah --} - -{- ******************************************************************** -* * - Class lookup for lifted equality -* * -***********************************************************************-} - --- See also Note [The equality types story] in TysPrim -matchLiftedEquality :: [Type] -> TcS LookupInstResult -matchLiftedEquality args - = return (OneInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ] - , lir_mk_ev = evDFunApp (dataConWrapId heqDataCon) args - , lir_safe_over = True }) - --- See also Note [The equality types story] in TysPrim -matchLiftedCoercible :: [Type] -> TcS LookupInstResult -matchLiftedCoercible args@[k, t1, t2] - = return (OneInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ] - , lir_mk_ev = evDFunApp (dataConWrapId coercibleDataCon) - args - , lir_safe_over = True }) - where - args' = [k, k, t1, t2] -matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args) - - -{- ******************************************************************** -* * - Class lookup for overloaded record fields -* * -***********************************************************************-} - -{- -Note [HasField instances] -~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - data T y = MkT { foo :: [y] } - -and `foo` is in scope. Then GHC will automatically solve a constraint like - - HasField "foo" (T Int) b - -by emitting a new wanted - - T alpha -> [alpha] ~# T Int -> b - -and building a HasField dictionary out of the selector function `foo`, -appropriately cast. - -The HasField class is defined (in GHC.Records) thus: - - class HasField (x :: k) r a | x r -> a where - getField :: r -> a - -Since this is a one-method class, it is represented as a newtype. -Hence we can solve `HasField "foo" (T Int) b` by taking an expression -of type `T Int -> b` and casting it using the newtype coercion. -Note that - - foo :: forall y . T y -> [y] - -so the expression we construct is - - foo @alpha |> co - -where - - co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b - -is built from - - co1 :: (T alpha -> [alpha]) ~# (T Int -> b) - -which is the new wanted, and - - co2 :: (T Int -> b) ~# HasField "foo" (T Int) b - -which can be derived from the newtype coercion. - -If `foo` is not in scope, or has a higher-rank or existentially -quantified type, then the constraint is not solved automatically, but -may be solved by a user-supplied HasField instance. Similarly, if we -encounter a HasField constraint where the field is not a literal -string, or does not belong to the type, then we fall back on the -normal constraint solver behaviour. --} - --- See Note [HasField instances] -matchHasField :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult -matchHasField dflags short_cut clas tys loc - = do { fam_inst_envs <- getFamInstEnvs - ; rdr_env <- getGlobalRdrEnvTcS - ; case tys of - -- We are matching HasField {k} x r a... - [_k_ty, x_ty, r_ty, a_ty] - -- x should be a literal string - | Just x <- isStrLitTy x_ty - -- r should be an applied type constructor - , Just (tc, args) <- tcSplitTyConApp_maybe r_ty - -- use representation tycon (if data family); it has the fields - , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args) - -- x should be a field of r - , Just fl <- lookupTyConFieldLabel x r_tc - -- the field selector should be in scope - , Just gre <- lookupGRE_FieldLabel rdr_env fl - - -> do { sel_id <- tcLookupId (flSelector fl) - ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id - - -- The first new wanted constraint equates the actual - -- type of the selector with the type (r -> a) within - -- the HasField x r a dictionary. The preds will - -- typically be empty, but if the datatype has a - -- "stupid theta" then we have to include it here. - ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds - - -- Use the equality proof to cast the selector Id to - -- type (r -> a), then use the newtype coercion to cast - -- it to a HasField dictionary. - mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co - where - co = mkTcSubCo (evTermCoercion (EvExpr ev1)) - `mkTcTransCo` mkTcSymCo co2 - mk_ev [] = panic "matchHasField.mk_ev" - - Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas) - tys - - tvs = mkTyVarTys (map snd tv_prs) - - -- The selector must not be "naughty" (i.e. the field - -- cannot have an existentially quantified type), and - -- it must not be higher-rank. - ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty - then do { addUsedGRE True gre - ; return OneInst { lir_new_theta = theta - , lir_mk_ev = mk_ev - , lir_safe_over = True - } } - else matchInstEnv dflags short_cut clas tys loc } - - _ -> matchInstEnv dflags short_cut clas tys loc } diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 0ac91a1ab7..3f0db9c012 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -20,6 +20,7 @@ module TcSMonad ( checkConstraintsTcS, checkTvConstraintsTcS, runTcPluginTcS, addUsedGRE, addUsedGREs, + matchGlobalInst, TcM.ClsInstResult(..), QCInst(..), @@ -97,7 +98,7 @@ module TcSMonad ( -- MetaTyVars newFlexiTcSTy, instFlexi, instFlexiX, cloneMetaTyVar, demoteUnfilledFmv, - tcInstType, tcInstSkolTyVarsX, + tcInstSkolTyVarsX, TcLevel, isFilledMetaTyVar_maybe, isFilledMetaTyVar, @@ -107,7 +108,7 @@ module TcSMonad ( zonkTcTyCoVarBndr, -- References - newTcRef, readTcRef, updTcRef, + newTcRef, readTcRef, writeTcRef, updTcRef, -- Misc getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, @@ -133,9 +134,11 @@ import FamInstEnv import qualified TcRnMonad as TcM import qualified TcMType as TcM +import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) ) import qualified TcEnv as TcM - ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass, tcLookupId ) + ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl ) import PrelNames( heqTyConKey, eqTyConKey ) +import ClsInst( InstanceWhat(..) ) import Kind import TcType import DynFlags @@ -363,13 +366,13 @@ selectNextWorkItem :: TcS (Maybe Ct) -- See Note [Prioritise equalities] selectNextWorkItem = do { wl_var <- getTcSWorkListRef - ; wl <- wrapTcS (TcM.readTcRef wl_var) + ; wl <- readTcRef wl_var ; case selectWorkItem wl of { Nothing -> return Nothing ; Just (ct, new_wl) -> do { -- checkReductionDepth (ctLoc ct) (ctPred ct) -- This is done by TcInteract.chooseInstance - ; wrapTcS (TcM.writeTcRef wl_var new_wl) + ; writeTcRef wl_var new_wl ; return (Just ct) } } } -- Pretty printing @@ -2927,21 +2930,21 @@ getTcSWorkListRef :: TcS (IORef WorkList) getTcSWorkListRef = TcS (return . tcs_worklist) getTcSInerts :: TcS InertSet -getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef) +getTcSInerts = getTcSInertsRef >>= readTcRef setTcSInerts :: InertSet -> TcS () -setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) } +setTcSInerts ics = do { r <- getTcSInertsRef; writeTcRef r ics } getWorkListImplics :: TcS (Bag Implication) getWorkListImplics = do { wl_var <- getTcSWorkListRef - ; wl_curr <- wrapTcS (TcM.readTcRef wl_var) + ; wl_curr <- readTcRef wl_var ; return (wl_implics wl_curr) } updWorkListTcS :: (WorkList -> WorkList) -> TcS () updWorkListTcS f = do { wl_var <- getTcSWorkListRef - ; wrapTcS (TcM.updTcRef wl_var f)} + ; updTcRef wl_var f } emitWorkNC :: [CtEvidence] -> TcS () emitWorkNC evs @@ -2961,6 +2964,9 @@ newTcRef x = wrapTcS (TcM.newTcRef x) readTcRef :: TcRef a -> TcS a readTcRef ref = wrapTcS (TcM.readTcRef ref) +writeTcRef :: TcRef a -> a -> TcS () +writeTcRef ref val = wrapTcS (TcM.writeTcRef ref val) + updTcRef :: TcRef a -> (a->a) -> TcS () updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn) @@ -3043,14 +3049,24 @@ addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS () -checkWellStagedDFun pred dfun_id loc +checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS () +-- Check that we do not try to use an instance before it is available. E.g. +-- instance Eq T where ... +-- f x = $( ... (\(p::T) -> p == p)... ) +-- Here we can't use the equality function from the instance in the splice + +checkWellStagedDFun loc what pred + | TopLevInstance { iw_dfun_id = dfun_id } <- what + , let bind_lvl = TcM.topIdLvl dfun_id + , bind_lvl > impLevel = wrapTcS $ TcM.setCtLocM loc $ do { use_stage <- TcM.getStage ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) } + + | otherwise + = return () -- Fast path for common case where pp_thing = text "instance for" <+> quotes (ppr pred) - bind_lvl = TcM.topIdLvl dfun_id pprEq :: TcType -> TcType -> SDoc pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2 @@ -3059,7 +3075,7 @@ isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type) isFilledMetaTyVar_maybe tv = case tcTyVarDetails tv of MetaTv { mtv_ref = ref } - -> do { cts <- wrapTcS (TcM.readTcRef ref) + -> do { cts <- readTcRef ref ; case cts of Indirect ty -> return (Just ty) Flexi -> return Nothing } @@ -3268,12 +3284,12 @@ instFlexiHelper subst tv ; TcM.traceTc "instFlexi" (ppr ty') ; return (extendTvSubst subst tv ty') } -tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar])) - -- ^ How to instantiate the type variables - -> Id -- ^ Type to instantiate - -> TcS ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result - -- (type vars, preds (incl equalities), rho) -tcInstType inst_tyvars id = wrapTcS (TcM.tcInstType inst_tyvars id) +matchGlobalInst :: DynFlags + -> Bool -- True <=> caller is the short-cut solver + -- See Note [Shortcut solving: overlap] + -> Class -> [Type] -> TcS TcM.ClsInstResult +matchGlobalInst dflags short_cut cls tys + = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys) tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar]) tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index c504ad9bdb..8f9b72b20d 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -410,7 +410,7 @@ How is this implemented? It's complicated! So we'll step through it all: the list is null. 2) `TcInteract.matchClassInst` -- This module drives the instance resolution - / dictionary generation. The return type is `LookupInstResult`, which either + / dictionary generation. The return type is `ClsInstResult`, which either says no instance matched, or one found, and if it was a safe or unsafe overlap. diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 0dc5664baf..86cb922b4a 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -27,6 +27,7 @@ import Maybes -- friends: import TcUnify ( tcSubType_NC ) import TcSimplify ( simplifyAmbiguityCheck ) +import ClsInst ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..) ) import TyCoRep import TcType hiding ( sizeType, sizeTypes ) import PrelNames @@ -40,15 +41,15 @@ import TyCon -- others: import HsSyn -- HsType import TcRnMonad -- TcType, amongst others -import TcEnv ( tcGetInstEnvs, tcInitTidyEnv, tcInitOpenTidyEnv ) +import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv ) import FunDeps -import InstEnv ( InstMatch, lookupInstEnv ) import FamInstEnv ( isDominatedBy, injectiveBranches, InjectivityCheckResult(..) ) import FamInst ( makeInjectivityErrors ) import Name import VarEnv import VarSet +import Id ( idType, idName ) import Var ( TyVarBndr(..), mkTyVar ) import ErrUtils import DynFlags @@ -680,9 +681,9 @@ applying the instance decl would show up two uses of ?x. Trac #8912. checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM () -- Assumes argument is fully zonked checkValidTheta ctxt theta - = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta) - ; addErrCtxtM (checkThetaCtxt ctxt theta) $ - check_valid_theta env ctxt theta } + = addErrCtxtM (checkThetaCtxt ctxt theta) $ + do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta) + ; check_valid_theta env ctxt theta } ------------------------- check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM () @@ -748,32 +749,47 @@ check_pred_help under_syn env dflags ctxt pred | otherwise -- A bit like classifyPredType, but not the same -- E.g. we treat (~) like (~#); and we look inside tuples - = case splitTyConApp_maybe pred of - Just (tc, tys) - | isTupleTyCon tc - -> check_tuple_pred under_syn env dflags ctxt pred tys - - | tc `hasKey` heqTyConKey || - tc `hasKey` eqTyConKey || - tc `hasKey` eqPrimTyConKey - -- NB: this equality check must come first, - -- because (~) is a class,too. - -> check_eq_pred env dflags pred tc tys - - | Just cls <- tyConClass_maybe tc - -- Includes Coercible - -> check_class_pred env dflags ctxt pred cls tys - - _ -> check_irred_pred under_syn env dflags ctxt pred - -check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM () -check_eq_pred env dflags pred tc tys + = case classifyPredType pred of + ClassPred cls tys + | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys + | otherwise -> check_class_pred env dflags ctxt pred cls tys + + EqPred NomEq _ _ -> -- a ~# b + check_eq_pred env dflags pred + + EqPred ReprEq _ _ -> -- Ugh! When inferring types we may get + -- f :: (a ~R# b) => blha + -- And we want to treat that like (Coercible a b) + -- We should probably check argument shapes, but we + -- didn't do so before, so I'm leaving it for now + return () + + ForAllPred _ theta head -> check_quant_pred env dflags pred theta head + IrredPred {} -> check_irred_pred under_syn env dflags ctxt pred + +check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM () +check_eq_pred env dflags pred = -- Equational constraints are valid in all contexts if type -- families are permitted - do { checkTc (tys `lengthIs` tyConArity tc) (tyConArityErr tc tys) - ; checkTcM (xopt LangExt.TypeFamilies dflags - || xopt LangExt.GADTs dflags) - (eqPredTyErr env pred) } + checkTcM (xopt LangExt.TypeFamilies dflags + || xopt LangExt.GADTs dflags) + (eqPredTyErr env pred) + +check_quant_pred :: TidyEnv -> DynFlags -> PredType + -> ThetaType -> PredType -> TcM () +check_quant_pred env dflags pred theta head_pred + = addErrCtxt (text "In the quantified constraint" + <+> quotes (ppr pred)) $ + do { checkTcM head_ok (badQuantHeadErr env pred) + + ; unless (xopt LangExt.UndecidableInstances dflags) $ + checkInstTermination theta head_pred + } + where + head_ok = case classifyPredType head_pred of + ClassPred {} -> True + IrredPred {} -> hasTyVarHead head_pred + _ -> False check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM () check_tuple_pred under_syn env dflags ctxt pred ts @@ -833,16 +849,21 @@ This will cause the constraint simplifier to loop because every time we canonica solved to add+canonicalise another (Foo a) constraint. -} ------------------------- -check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM () +check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt + -> PredType -> Class -> [TcType] -> TcM () check_class_pred env dflags ctxt pred cls tys + | cls `hasKey` heqTyConKey -- (~) and (~~) are classified as classes, + || cls `hasKey` eqTyConKey -- but here we want to treat them as equalities + = pprTrace "check_class" (ppr cls) $ + check_eq_pred env dflags pred + | isIPClass cls = do { check_arity ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) } - | otherwise + | otherwise -- Includes Coercible = do { check_arity - ; warn_simp <- woptM Opt_WarnSimplifiableClassConstraints - ; when warn_simp check_simplifiable_class_constraint + ; checkSimplifiableClassConstraint env dflags ctxt cls tys ; checkTcM arg_tys_ok (predTyVarErr env pred) } where check_arity = checkTc (tys `lengthIs` classArity cls) @@ -858,27 +879,48 @@ check_class_pred env dflags ctxt pred cls tys -- in checkInstTermination _ -> checkValidClsArgs flexible_contexts cls tys - -- See Note [Simplifiable given constraints] - check_simplifiable_class_constraint - | xopt LangExt.MonoLocalBinds dflags - = return () - | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta" - = return () -- of a data type declaration - | otherwise - = do { envs <- tcGetInstEnvs - ; case lookupInstEnv False envs cls tys of - ([m], [], _) -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints) - (simplifiable_constraint_warn m) - _ -> return () } - - simplifiable_constraint_warn :: InstMatch -> SDoc - simplifiable_constraint_warn (match, _) - = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))) - 2 (text "matches an instance declaration") - , ppr match +checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt + -> Class -> [TcType] -> TcM () +-- See Note [Simplifiable given constraints] +checkSimplifiableClassConstraint env dflags ctxt cls tys + | not (wopt Opt_WarnSimplifiableClassConstraints dflags) + = return () + | xopt LangExt.MonoLocalBinds dflags + = return () + + | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta" + = return () -- of a data type declaration + + | cls `hasKey` coercibleTyConKey + = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK + -- matchGlobalInst will reply "yes" because we can reduce + -- (Coercible a b) to (a ~R# b) + + | otherwise + = do { result <- matchGlobalInst dflags False cls tys + ; case result of + OneInst { cir_what = what } + -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints) + (simplifiable_constraint_warn what) + _ -> return () } + where + pred = mkClassPred cls tys + + simplifiable_constraint_warn :: InstanceWhat -> SDoc + simplifiable_constraint_warn what + = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)) + <+> text "matches") + 2 (ppr_what what) , hang (text "This makes type inference for inner bindings fragile;") 2 (text "either use MonoLocalBinds, or simplify it using the instance") ] + ppr_what BuiltinInstance = text "a built-in instance" + ppr_what LocalInstance = text "a locally-quantified instance" + ppr_what (TopLevInstance { iw_dfun_id = dfun }) + = hang (text "instance" <+> pprSigmaType (idType dfun)) + 2 (text "--" <+> pprDefinedAt (idName dfun)) + + {- Note [Simplifiable given constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A type signature like @@ -973,7 +1015,12 @@ checkThetaCtxt ctxt theta env , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta) , text "While checking" <+> pprUserTypeCtxt ctxt ] ) -eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc) +eqPredTyErr, predTupleErr, predIrredErr, + predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc) +badQuantHeadErr env pred + = ( env + , hang (text "Quantified predicate must have a class or type variable head:") + 2 (ppr_tidy env pred) ) eqPredTyErr env pred = ( env , text "Illegal equational constraint" <+> ppr_tidy env pred $$ @@ -1329,7 +1376,9 @@ checkValidInstance ctxt hs_type ty | otherwise = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys) ; traceTc "checkValidInstance {" (ppr ty) - ; checkValidTheta ctxt theta + + ; env0 <- tcInitTidyEnv + ; check_valid_theta env0 ctxt theta -- The Termination and Coverate Conditions -- Check that instance inference will terminate (if we care) @@ -1415,16 +1464,15 @@ checkInstTermination theta head_pred bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys) -- See Note [Invisible arguments and termination] - ForAllPred tvs theta' head_pred' - -> do { check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred' - ; addErrCtxt (text "In the quantified constraint" - <+> quotes (ppr pred)) $ - checkInstTermination theta' head_pred' } + ForAllPred tvs _ head_pred' + -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred' + -- Termination of the quantified predicate itself is checked + -- when the predicates are individually checked for validity check2 foralld_tvs pred pred_size - | not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what (ppr head_pred)) - | not (isTyFamFree pred) = addErrTc (nestedMsg what) - | pred_size >= head_size = addErrTc (smallerMsg what (ppr head_pred)) + | not (null bad_tvs) = failWithTc (noMoreMsg bad_tvs what (ppr head_pred)) + | not (isTyFamFree pred) = failWithTc (nestedMsg what) + | pred_size >= head_size = failWithTc (smallerMsg what (ppr head_pred)) | otherwise = return () -- isTyFamFree: see Note [Type families in instance contexts] where diff --git a/testsuite/tests/indexed-types/should_compile/T15322.hs b/testsuite/tests/indexed-types/should_compile/T15322.hs new file mode 100644 index 0000000000..5a0cd179b8 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15322.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} + +module T15322 where + +import Data.Proxy (Proxy (..)) +import Type.Reflection +import GHC.TypeLits (KnownNat, type (+)) + +f :: forall n . (Typeable (n+1), KnownNat n) => Proxy n -> TypeRep (n+1) +f _ = typeRep diff --git a/testsuite/tests/indexed-types/should_compile/T15322.stderr b/testsuite/tests/indexed-types/should_compile/T15322.stderr new file mode 100644 index 0000000000..7447a9ece2 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15322.stderr @@ -0,0 +1,8 @@ + +T15322.hs:11:6: warning: [-Wsimplifiable-class-constraints (in -Wdefault)] + • The constraint ‘Typeable (n + 1)’ matches a built-in instance + This makes type inference for inner bindings fragile; + either use MonoLocalBinds, or simplify it using the instance + • In the type signature: + f :: forall n. + (Typeable (n + 1), KnownNat n) => Proxy n -> TypeRep (n + 1) diff --git a/testsuite/tests/indexed-types/should_compile/T15322a.hs b/testsuite/tests/indexed-types/should_compile/T15322a.hs new file mode 100644 index 0000000000..93d0830b26 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15322a.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} + +module T15322a where + +import Data.Proxy (Proxy (..)) +import Type.Reflection +import GHC.TypeLits (KnownNat, type (+)) + +f :: forall n . (KnownNat n) => Proxy n -> TypeRep (n+1) +f _ = typeRep diff --git a/testsuite/tests/indexed-types/should_compile/T15322a.stderr b/testsuite/tests/indexed-types/should_compile/T15322a.stderr new file mode 100644 index 0000000000..37a9070e27 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15322a.stderr @@ -0,0 +1,12 @@ + +T15322a.hs:12:7: error: + • Could not deduce (KnownNat (n + 1)) + arising from a use of ‘typeRep’ + from the context: KnownNat n + bound by the type signature for: + f :: forall (n :: GHC.Types.Nat). + KnownNat n => + Proxy n -> TypeRep (n + 1) + at T15322a.hs:11:1-56 + • In the expression: typeRep + In an equation for ‘f’: f _ = typeRep diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 56448ac75b..6255dd2c79 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -284,3 +284,5 @@ test('T15144', normal, compile, ['']) test('T15122', normal, compile, ['']) test('T13777', normal, compile, ['']) test('T14164', normal, compile, ['']) +test('T15322', normal, compile, ['']) +test('T15322a', normal, compile_fail, ['']) diff --git a/testsuite/tests/partial-sigs/should_compile/SomethingShowable.stderr b/testsuite/tests/partial-sigs/should_compile/SomethingShowable.stderr index 4b72ec4520..262b76d60a 100644 --- a/testsuite/tests/partial-sigs/should_compile/SomethingShowable.stderr +++ b/testsuite/tests/partial-sigs/should_compile/SomethingShowable.stderr @@ -7,8 +7,8 @@ Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] SomethingShowable.hs:5:1: warning: [-Wsimplifiable-class-constraints (in -Wdefault)] - • The constraint ‘Show Bool’ matches an instance declaration - instance Show Bool -- Defined in ‘GHC.Show’ + • The constraint ‘Show Bool’ matches + instance Show Bool -- Defined in ‘GHC.Show’ This makes type inference for inner bindings fragile; either use MonoLocalBinds, or simplify it using the instance • When checking the inferred type diff --git a/testsuite/tests/polykinds/T11466.stderr b/testsuite/tests/polykinds/T11466.stderr index f584731934..616f317250 100644 --- a/testsuite/tests/polykinds/T11466.stderr +++ b/testsuite/tests/polykinds/T11466.stderr @@ -1,6 +1,4 @@ T11466.hs:15:10: error: • Illegal implicit parameter ‘?x::Int’ - • In the context: Bla - While checking an instance declaration - In the instance declaration for ‘Eq T’ + • In the instance declaration for ‘Eq T’ diff --git a/testsuite/tests/quantified-constraints/T15316.hs b/testsuite/tests/quantified-constraints/T15316.hs new file mode 100644 index 0000000000..07539e3183 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15316.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE RankNTypes, QuantifiedConstraints, ConstraintKinds #-} +-- NB: disabling these if enabled: +{-# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #-} + +module T15316 where + +import Data.Proxy + +{- +class Class a where + method :: a + +subsume :: (Class a => Class b) => Proxy a -> Proxy b -> ((Class a => Class b) => r) -> r +subsume _ _ x = x + +value :: Proxy a -> a +value p = subsume p p method +-} + +subsume' :: Proxy c -> ((c => c) => r) -> r +subsume' _ x = x diff --git a/testsuite/tests/quantified-constraints/T15316.stderr b/testsuite/tests/quantified-constraints/T15316.stderr new file mode 100644 index 0000000000..4444c2c453 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15316.stderr @@ -0,0 +1,6 @@ + +T15316.hs:20:13: error: + • The constraint ‘c’ is no smaller than the instance head ‘c’ + (Use UndecidableInstances to permit this) + • In the quantified constraint ‘c => c’ + In the type signature: subsume' :: Proxy c -> ((c => c) => r) -> r diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T index 65e636744f..3145f47cf1 100644 --- a/testsuite/tests/quantified-constraints/all.T +++ b/testsuite/tests/quantified-constraints/all.T @@ -14,3 +14,4 @@ test('T15231', normal, compile_fail, ['']) test('T15290', normal, compile, ['']) test('T15290a', normal, compile_fail, ['']) test('T15290b', normal, compile_fail, ['']) +test('T15316', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_compile/T10177.hs b/testsuite/tests/typecheck/should_compile/T10177.hs index fd84396f67..43aac8afd4 100644 --- a/testsuite/tests/typecheck/should_compile/T10177.hs +++ b/testsuite/tests/typecheck/should_compile/T10177.hs @@ -1,5 +1,8 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} + -- This test deliberately uses a simplifiable class constraint + module T10177 where import Data.Typeable diff --git a/testsuite/tests/typecheck/should_compile/T13526.stderr b/testsuite/tests/typecheck/should_compile/T13526.stderr index 7a0f2ae7c6..ad5876ec9e 100644 --- a/testsuite/tests/typecheck/should_compile/T13526.stderr +++ b/testsuite/tests/typecheck/should_compile/T13526.stderr @@ -1,7 +1,7 @@ T13526.hs:21:8: warning: [-Wsimplifiable-class-constraints (in -Wdefault)] - • The constraint ‘C (Maybe a)’ matches an instance declaration - instance C a => C (Maybe a) -- Defined at T13526.hs:14:10 + • The constraint ‘C (Maybe a)’ matches + instance C a => C (Maybe a) -- Defined at T13526.hs:14:10 This makes type inference for inner bindings fragile; either use MonoLocalBinds, or simplify it using the instance • In the type signature: bar :: C (Maybe a) => a -> Maybe a diff --git a/testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs b/testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs index c401e1c446..b5e20be448 100644 --- a/testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs +++ b/testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs @@ -13,11 +13,17 @@ using the solver (see `tcSuperClasses` in `TcInstDecls`). However, some classes need to be excepted from this behavior, as they have custom solving rules, and this test checks that we got this right. + +PS: this test used to have Typeable in the context too, but + that's a redundant constraint, so I removed it + +PPS: the whole structre of tcSuperClasses has changed, + so I'm no longer sure what is being tested here -} -class (Typeable x, KnownNat x) => C x -class (Typeable x, KnownSymbol x) => D x +class (KnownNat x) => C x +class (KnownSymbol x) => D x instance C 2 instance D "2" diff --git a/testsuite/tests/typecheck/should_fail/T8912.stderr b/testsuite/tests/typecheck/should_fail/T8912.stderr index bfe06c1511..7d6f37dca2 100644 --- a/testsuite/tests/typecheck/should_fail/T8912.stderr +++ b/testsuite/tests/typecheck/should_fail/T8912.stderr @@ -1,6 +1,4 @@ T8912.hs:7:10: error: • Illegal implicit parameter ‘?imp::Int’ - • In the context: ?imp::Int - While checking an instance declaration - In the instance declaration for ‘C [a]’ + • In the instance declaration for ‘C [a]’ diff --git a/testsuite/tests/typecheck/should_fail/fd-loop.stderr b/testsuite/tests/typecheck/should_fail/fd-loop.stderr index 31fd91b08a..86a70f5b76 100644 --- a/testsuite/tests/typecheck/should_fail/fd-loop.stderr +++ b/testsuite/tests/typecheck/should_fail/fd-loop.stderr @@ -4,9 +4,3 @@ fd-loop.hs:12:10: error: in the constraint ‘C a b’ than in the instance head ‘Eq (T a)’ (Use UndecidableInstances to permit this) • In the instance declaration for ‘Eq (T a)’ - -fd-loop.hs:12:10: error: - • Variable ‘b’ occurs more often - in the constraint ‘Eq b’ than in the instance head ‘Eq (T a)’ - (Use UndecidableInstances to permit this) - • In the instance declaration for ‘Eq (T a)’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail157.stderr b/testsuite/tests/typecheck/should_fail/tcfail157.stderr index e81778cb0c..4cb2af7e9f 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail157.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail157.stderr @@ -5,10 +5,3 @@ tcfail157.hs:27:10: error: than in the instance head ‘Foo m (a -> ())’ (Use UndecidableInstances to permit this) • In the instance declaration for ‘Foo m (a -> ())’ - -tcfail157.hs:27:10: error: - • Variable ‘b’ occurs more often - in the constraint ‘Foo m b’ - than in the instance head ‘Foo m (a -> ())’ - (Use UndecidableInstances to permit this) - • In the instance declaration for ‘Foo m (a -> ())’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail211.stderr b/testsuite/tests/typecheck/should_fail/tcfail211.stderr index 7a5053a092..fb1192b0ca 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail211.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail211.stderr @@ -7,6 +7,4 @@ tcfail211.hs:5:1: error: tcfail211.hs:8:10: error: • Illegal implicit parameter ‘?imp::Int’ - • In the context: ?imp::Int - While checking an instance declaration - In the instance declaration for ‘D Int’ + • In the instance declaration for ‘D Int’ |