Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC Commits: c1f7d8ea by Simon Peyton Jones at 2025-07-21T12:07:01+01:00 Solve forall-constraints immediately, or not at all Triggered by the new short-cut solver, I realised that it is nicer to solve forall-constraints immediately, rather than emitting an implication constraint to be solved later. This is an un-forced refactoring, but it saves quite a bit of plumbing; e.g - The `wl_implics` field of `WorkList` is gone, - The types of `solveSimpleWanteds` and friends are simplified. - An EvFun contains binding, rather than an EvBindsVar ref-cell that will in the future contain bindings. That makes `evVarsOfTerm` simpler It also improves error messages a bit. One tiresome point: in the tricky case of `inferConstraintsCoerceBased` we make a forall-constraint. This we /do/ want to partially solve, so we can infer a suitable context. (I'd be quite happy to force the user to write a context, bt I don't want to change behavior.) So we want to generate an /implication/ constraint in `emitPredSpecConstraints` rather than a /forall-constraint/ as we were doing before. Incidental refactoring * `GHC.Tc.Deriv.Infer.inferConstraints` was consulting the state monad for the DerivEnv that the caller had just consulted. Nicer to pass it as an argument I think, so I have done that. No change in behaviour. - - - - - 38758a5d by Simon Peyton Jones at 2025-07-21T12:07:01+01:00 Remove duplicated code in Ast.hs for evTermFreeVars This is just a tidy up. - - - - - ed5d029b by Simon Peyton Jones at 2025-07-21T12:07:01+01:00 Small tc-tracing changes only - - - - - 30 changed files: - compiler/GHC/Iface/Ext/Ast.hs - compiler/GHC/Tc/Deriv.hs - compiler/GHC/Tc/Deriv/Infer.hs - compiler/GHC/Tc/Deriv/Utils.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Solve.hs - + compiler/GHC/Tc/Solver/Solve.hs-boot - compiler/GHC/Tc/Zonk/Type.hs - testsuite/tests/deriving/should_compile/T20815.hs - testsuite/tests/impredicative/T17332.stderr - testsuite/tests/quantified-constraints/T15290a.stderr - testsuite/tests/quantified-constraints/T19690.stderr - testsuite/tests/quantified-constraints/T19921.stderr - testsuite/tests/quantified-constraints/T21006.stderr - testsuite/tests/typecheck/should_compile/T12427a.stderr - testsuite/tests/typecheck/should_fail/T14605.hs - testsuite/tests/typecheck/should_fail/T14605.stderr - testsuite/tests/typecheck/should_fail/T15801.stderr - testsuite/tests/typecheck/should_fail/T18640a.stderr - testsuite/tests/typecheck/should_fail/T18640b.stderr - testsuite/tests/typecheck/should_fail/T19627.stderr - testsuite/tests/typecheck/should_fail/T21530b.stderr - testsuite/tests/typecheck/should_fail/T22912.stderr - testsuite/tests/typecheck/should_fail/tcfail174.stderr Changes: ===================================== compiler/GHC/Iface/Ext/Ast.hs ===================================== @@ -32,12 +32,12 @@ import GHC.Types.Basic import GHC.Data.BooleanFormula import GHC.Core.Class ( className, classSCSelIds ) import GHC.Core.ConLike ( conLikeName ) -import GHC.Core.FVs import GHC.Core.DataCon ( dataConNonlinearType ) import GHC.Types.FieldLabel import GHC.Hs import GHC.Hs.Syn.Type import GHC.Utils.Monad ( concatMapM, MonadIO(liftIO) ) +import GHC.Utils.FV ( fvVarList, filterFV ) import GHC.Types.Id ( isDataConId_maybe ) import GHC.Types.Name ( Name, nameSrcSpan, nameUnique, wiredInNameTyThing_maybe, getName ) import GHC.Types.Name.Env ( NameEnv, emptyNameEnv, extendNameEnv, lookupNameEnv ) @@ -45,8 +45,8 @@ import GHC.Types.Name.Reader ( RecFieldInfo(..), WithUserRdr(..) ) import GHC.Types.SrcLoc import GHC.Core.Type ( Type, ForAllTyFlag(..) ) import GHC.Core.TyCon ( TyCon, tyConClass_maybe ) -import GHC.Core.Predicate import GHC.Core.InstEnv +import GHC.Core.Predicate ( isEvId ) import GHC.Tc.Types import GHC.Tc.Types.Evidence import GHC.Types.Var ( Id, Var, EvId, varName, varType, varUnique ) @@ -672,22 +672,16 @@ instance ToHie (Context (Located Name)) where instance ToHie (Context (Located (WithUserRdr Name))) where toHie (C c (L l (WithUserRdr _ n))) = toHie $ C c (L l n) -evVarsOfTermList :: EvTerm -> [EvId] -evVarsOfTermList (EvExpr e) = exprSomeFreeVarsList isEvVar e -evVarsOfTermList (EvTypeable _ ev) = - case ev of - EvTypeableTyCon _ e -> concatMap evVarsOfTermList e - EvTypeableTyApp e1 e2 -> concatMap evVarsOfTermList [e1,e2] - EvTypeableTrFun e1 e2 e3 -> concatMap evVarsOfTermList [e1,e2,e3] - EvTypeableTyLit e -> evVarsOfTermList e -evVarsOfTermList (EvFun{}) = [] +hieEvIdsOfTerm :: EvTerm -> [EvId] +-- Returns only EvIds satisfying relevantEvId +hieEvIdsOfTerm tm = fvVarList (filterFV isEvId (evTermFVs tm)) instance ToHie (EvBindContext (LocatedA TcEvBinds)) where toHie (EvBindContext sc sp (L span (EvBinds bs))) = concatMapM go $ bagToList bs where go evbind = do - let evDeps = evVarsOfTermList $ eb_rhs evbind + let evDeps = hieEvIdsOfTerm $ eb_rhs evbind depNames = EvBindDeps $ map varName evDeps concatM $ [ toHie (C (EvidenceVarBind (EvLetBind depNames) (combineScopes sc (mkScope span)) sp) @@ -708,7 +702,7 @@ instance ToHie (LocatedA HsWrapper) where toHie $ C (EvidenceVarBind EvWrapperBind (mkScope osp) (getRealSpanA osp)) $ L osp a (WpEvApp a) -> - concatMapM (toHie . C EvidenceVarUse . L osp) $ evVarsOfTermList a + concatMapM (toHie . C EvidenceVarUse . L osp) $ hieEvIdsOfTerm a _ -> pure [] instance HiePass p => HasType (LocatedA (HsBind (GhcPass p))) where ===================================== compiler/GHC/Tc/Deriv.hs ===================================== @@ -1432,13 +1432,13 @@ See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom -- EarlyDerivSpec from it. mk_eqn_from_mechanism :: DerivSpecMechanism -> DerivM EarlyDerivSpec mk_eqn_from_mechanism mechanism - = do DerivEnv { denv_overlap_mode = overlap_mode - , denv_tvs = tvs - , denv_cls = cls - , denv_inst_tys = inst_tys - , denv_ctxt = deriv_ctxt - , denv_skol_info = skol_info - , denv_warn = warn } <- ask + = do env@(DerivEnv { denv_overlap_mode = overlap_mode + , denv_tvs = tvs + , denv_cls = cls + , denv_inst_tys = inst_tys + , denv_ctxt = deriv_ctxt + , denv_skol_info = skol_info + , denv_warn = warn }) <- ask user_ctxt <- askDerivUserTypeCtxt doDerivInstErrorChecks1 mechanism loc <- lift getSrcSpanM @@ -1446,7 +1446,7 @@ mk_eqn_from_mechanism mechanism case deriv_ctxt of InferContext wildcard -> do { (inferred_constraints, tvs', inst_tys', mechanism') - <- inferConstraints mechanism + <- inferConstraints mechanism env ; return $ InferTheta $ DS { ds_loc = loc , ds_name = dfun_name, ds_tvs = tvs' ===================================== compiler/GHC/Tc/Deriv/Infer.hs ===================================== @@ -66,7 +66,7 @@ import Data.Maybe ---------------------- -inferConstraints :: DerivSpecMechanism +inferConstraints :: DerivSpecMechanism -> DerivEnv -> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism) -- inferConstraints figures out the constraints needed for the -- instance declaration generated by a 'deriving' clause on a @@ -83,12 +83,12 @@ inferConstraints :: DerivSpecMechanism -- Generate a sufficiently large set of constraints that typechecking the -- generated method definitions should succeed. This set will be simplified -- before being used in the instance declaration -inferConstraints mechanism - = do { DerivEnv { denv_tvs = tvs - , denv_cls = main_cls - , denv_inst_tys = inst_tys } <- ask - ; wildcard <- isStandaloneWildcardDeriv - ; let infer_constraints :: DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism) +inferConstraints mechanism (DerivEnv { denv_ctxt = ctxt + , denv_tvs = tvs + , denv_cls = main_cls + , denv_inst_tys = inst_tys }) + = do { let wildcard = isStandaloneWildcardDeriv ctxt + infer_constraints :: DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism) infer_constraints = case mechanism of DerivSpecStock{dsm_stock_dit = dit} @@ -169,12 +169,12 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys , dit_tc_args = tc_args , dit_rep_tc = rep_tc , dit_rep_tc_args = rep_tc_args }) - = do DerivEnv { denv_tvs = tvs + = do DerivEnv { denv_ctxt = ctxt + , denv_tvs = tvs , denv_cls = main_cls , denv_inst_tys = inst_tys } <- ask - wildcard <- isStandaloneWildcardDeriv - - let inst_ty = mkTyConApp tc tc_args + let wildcard = isStandaloneWildcardDeriv ctxt + inst_ty = mkTyConApp tc tc_args tc_binders = tyConBinders rep_tc choose_level bndr | isNamedTyConBinder bndr = KindLevel @@ -370,13 +370,14 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys -- derived instance context. inferConstraintsAnyclass :: DerivM ThetaSpec inferConstraintsAnyclass - = do { DerivEnv { denv_cls = cls + = do { DerivEnv { denv_ctxt = ctxt + , denv_cls = cls , denv_inst_tys = inst_tys } <- ask ; let gen_dms = [ (sel_id, dm_ty) | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ] - ; wildcard <- isStandaloneWildcardDeriv - ; let meth_pred :: (Id, Type) -> PredSpec + ; let wildcard = isStandaloneWildcardDeriv ctxt + meth_pred :: (Id, Type) -> PredSpec -- (Id,Type) are the selector Id and the generic default method type -- NB: the latter is /not/ quantified over the class variables -- See Note [Gathering and simplifying constraints for DeriveAnyClass] @@ -408,10 +409,10 @@ inferConstraintsAnyclass inferConstraintsCoerceBased :: [Type] -> Type -> DerivM ThetaSpec inferConstraintsCoerceBased cls_tys rep_ty = do - DerivEnv { denv_tvs = tvs + DerivEnv { denv_ctxt = ctxt + , denv_tvs = tvs , denv_cls = cls , denv_inst_tys = inst_tys } <- ask - sa_wildcard <- isStandaloneWildcardDeriv let -- rep_ty might come from: -- GeneralizedNewtypeDeriving / DerivSpecNewtype: -- the underlying type of the newtype () @@ -426,6 +427,7 @@ inferConstraintsCoerceBased cls_tys rep_ty = do -- we are going to get all the methods for the final -- dictionary deriv_origin = mkDerivOrigin sa_wildcard + sa_wildcard = isStandaloneWildcardDeriv ctxt -- Next we collect constraints for the class methods -- If there are no methods, we don't need any constraints @@ -574,7 +576,7 @@ Consider the `deriving Alt` part of this example (from the passing part of T20815a): class Alt f where - some :: Applicative f => f a -> f [a] + some :: forall a. Applicative f => f a -> f [a] newtype T f a = T (f a) deriving Alt ===================================== compiler/GHC/Tc/Deriv/Utils.hs ===================================== @@ -35,11 +35,11 @@ import GHC.Tc.Deriv.Generate import GHC.Tc.Deriv.Functor import GHC.Tc.Deriv.Generics import GHC.Tc.Errors.Types -import GHC.Tc.Types.Constraint (WantedConstraints, mkNonCanonical) +import GHC.Tc.Types.Constraint (WantedConstraints, mkNonCanonical, mkSimpleWC) import GHC.Tc.Types.Origin import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType -import GHC.Tc.Utils.Unify (tcSubTypeSigma) +import GHC.Tc.Utils.Unify (tcSubTypeSigma, buildImplicationFor) import GHC.Tc.Zonk.Type import GHC.Core.Class @@ -71,7 +71,6 @@ import GHC.Utils.Error import GHC.Utils.Unique (sameUnique) import Control.Monad.Trans.Reader -import Data.Foldable (traverse_) import Data.Maybe import qualified GHC.LanguageExtensions as LangExt import GHC.Data.List.SetOps (assocMaybe) @@ -92,12 +91,9 @@ isStandaloneDeriv = asks (go . denv_ctxt) -- | Is GHC processing a standalone deriving declaration with an -- extra-constraints wildcard as the context? -- (e.g., @deriving instance _ => Eq (Foo a)@) -isStandaloneWildcardDeriv :: DerivM Bool -isStandaloneWildcardDeriv = asks (go . denv_ctxt) - where - go :: DerivContext -> Bool - go (InferContext wildcard) = isJust wildcard - go (SupplyContext {}) = False +isStandaloneWildcardDeriv :: DerivContext -> Bool +isStandaloneWildcardDeriv (InferContext wildcard) = isJust wildcard +isStandaloneWildcardDeriv (SupplyContext {}) = False -- | Return 'InstDeclCtxt' if processing with a standalone @deriving@ -- declaration or 'DerivClauseCtxt' if processing a @deriving@ clause. @@ -563,11 +559,17 @@ data PredSpec SimplePredSpec { sps_pred :: TcPredType -- ^ The constraint to emit as a wanted + -- Usually just a simple predicate like (Eq a) or (ki ~# Type), + -- but (hack) in the case of GHC.Tc.Deriv.Infer.inferConstraintsCoerceBased, + -- it can be a forall-constraint + , sps_origin :: CtOrigin -- ^ The origin of the constraint + , sps_type_or_kind :: TypeOrKind -- ^ Whether the constraint is a type or kind } + | -- | A special 'PredSpec' that is only used by @DeriveAnyClass@. This -- will check if @stps_ty_actual@ is a subtype of (i.e., more polymorphic -- than) @stps_ty_expected@ in the constraint solving machinery, emitting an @@ -677,8 +679,8 @@ captureThetaSpecConstraints :: -- @deriving@ declaration -> ThetaSpec -- ^ The specs from which constraints will be created -> TcM (TcLevel, WantedConstraints) -captureThetaSpecConstraints user_ctxt theta = - pushTcLevelM $ mk_wanteds theta +captureThetaSpecConstraints user_ctxt theta + = pushTcLevelM $ mk_wanteds theta where -- Create the constraints we need to solve. For stock and newtype -- deriving, these constraints will be simple wanted constraints @@ -689,34 +691,49 @@ captureThetaSpecConstraints user_ctxt theta = mk_wanteds :: ThetaSpec -> TcM WantedConstraints mk_wanteds preds = do { (_, wanteds) <- captureConstraints $ - traverse_ emit_constraints preds + mapM_ (emitPredSpecConstraints user_ctxt) preds ; pure wanteds } - -- Emit the appropriate constraints depending on what sort of - -- PredSpec we are dealing with. - emit_constraints :: PredSpec -> TcM () - emit_constraints ps = - case ps of - -- For constraints like (C a, Ord b), emit the - -- constraints directly as simple wanted constraints. - SimplePredSpec { sps_pred = wanted - , sps_origin = orig - , sps_type_or_kind = t_or_k - } -> do - ev <- newWanted orig (Just t_or_k) wanted - emitSimple (mkNonCanonical ev) - - -- For DeriveAnyClass, check if ty_actual is a subtype of - -- ty_expected, which emits an implication constraint as a - -- side effect. See - -- Note [Gathering and simplifying constraints for DeriveAnyClass]. - -- in GHC.Tc.Deriv.Infer. - SubTypePredSpec { stps_ty_actual = ty_actual - , stps_ty_expected = ty_expected - , stps_origin = orig - } -> do - _ <- tcSubTypeSigma orig user_ctxt ty_actual ty_expected - return () +emitPredSpecConstraints :: UserTypeCtxt -> PredSpec -> TcM () +--- Emit the appropriate constraints depending on what sort of +-- PredSpec we are dealing with. +emitPredSpecConstraints _ (SimplePredSpec { sps_pred = wanted_pred + , sps_origin = orig + , sps_type_or_kind = t_or_k }) + -- For constraints like (C a) or (Ord b), emit the + -- constraints directly as simple wanted constraints. + | isRhoTy wanted_pred + = do { ev <- newWanted orig (Just t_or_k) wanted_pred + ; emitSimple (mkNonCanonical ev) } + + | otherwise + -- Forall-constraints, which come exclusively from + -- GHC.Tc.Deriv.Infer.inferConstraintsCoerceBased. + -- For these we want to emit an implication constraint, and NOT a + -- forall-constraint. Why? Because forall-constraints are solved all-or-nothing, + -- but here when we are trying to infer the context for an instance decl, we + -- need that half-solved implication. See deriving/should_compile/T20815 + -- and Note [Inferred contexts from method constraints] + = do { let skol_info_anon = DerivSkol wanted_pred + ; skol_info <- mkSkolemInfo skol_info_anon + ; (_wrapper, tv_prs, givens, wanted_rho) <- topSkolemise skol_info wanted_pred + -- _wrapper: we ignore the evidence from all these constraints + ; (tc_lvl, ev) <- pushTcLevelM $ newWanted orig (Just t_or_k) wanted_rho + ; let skol_tvs = map (binderVar . snd) tv_prs + ; (implic, _) <- buildImplicationFor tc_lvl skol_info_anon skol_tvs + givens (mkSimpleWC [ev]) + ; emitImplications implic } + +emitPredSpecConstraints user_ctxt + (SubTypePredSpec { stps_ty_actual = ty_actual + , stps_ty_expected = ty_expected + , stps_origin = orig }) +-- For DeriveAnyClass, check if ty_actual is a subtype of ty_expected, +-- which emits an implication constraint as a side effect. See +-- Note [Gathering and simplifying constraints for DeriveAnyClass] +-- in GHC.Tc.Deriv.Infer. + = do { _ <- tcSubTypeSigma orig user_ctxt ty_actual ty_expected + ; return () } {- ************************************************************************ ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -623,7 +623,8 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- report2: we suppress these if there are insolubles elsewhere in the tree report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) - , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] + , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) + , ("Quantified", is_qc, False, mkGroupReporter mkQCErr) ] -- report3: suppressed errors should be reported as categorized by either report1 -- or report2. Keep this in sync with the suppress function above @@ -687,6 +688,9 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_irred _ (IrredPred {}) = True is_irred _ _ = False + is_qc _ (ForAllPred {}) = True + is_qc _ _ = False + -- See situation (1) of Note [Suppressing confusing errors] is_ww_fundep item _ = is_ww_fundep_item item is_ww_fundep_item = isWantedWantedFunDepOrigin . errorItemOrigin @@ -2214,6 +2218,15 @@ Warn of loopy local equalities that were dropped. ************************************************************************ -} +mkQCErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport +mkQCErr ctxt items + | item1 :| _ <- tryFilter (not . ei_suppress) items + -- Ignore multiple qc-errors on the same line + = do { let msg = mkPlainMismatchMsg $ + CouldNotDeduce (getUserGivens ctxt) (item1 :| []) Nothing + ; return $ important ctxt msg } + + mkDictErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport mkDictErr ctxt orig_items = do { inst_envs <- tcGetInstEnvs @@ -2231,8 +2244,8 @@ mkDictErr ctxt orig_items ; return $ SolverReport { sr_important_msg = SolverReportWithCtxt ctxt err - , sr_supplementary = - [ SupplementaryImportErrors imps | imps <- maybeToList (NE.nonEmpty imp_errs) ] + , sr_supplementary = [ SupplementaryImportErrors imps + | imps <- maybeToList (NE.nonEmpty imp_errs) ] , sr_hints = hints } } ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -460,6 +460,7 @@ finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap ; res_expr <- if isTagToEnum tc_fun then tcTagToEnum tc_head tc_args app_res_rho else return (rebuildHsApps tc_head tc_args) + ; traceTc "End tcApp }" (ppr tc_fun) ; return (mkHsWrap res_wrap res_expr) } checkResultTy :: HsExpr GhcRn ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -1481,6 +1481,7 @@ expandRecordUpd record_expr possible_parents rbnds res_ty vcat [ text "relevant_con:" <+> ppr relevant_con , text "res_ty:" <+> ppr res_ty , text "ds_res_ty:" <+> ppr ds_res_ty + , text "ds_expr:" <+> ppr ds_expr ] ; return (ds_expr, ds_res_ty, RecordUpdCtxt relevant_cons upd_fld_names ex_tvs) } ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -1036,8 +1036,7 @@ findInferredDiff annotated_theta inferred_theta -- See `Note [Quantification and partial signatures]` Wrinkle 2 ; return (map (box_pred . ctPred) $ - bagToList $ - wc_simple residual) } + bagToList residual) } where box_pred :: PredType -> PredType box_pred pred = case classifyPredType pred of ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -1188,8 +1188,8 @@ tryDefaultGroup wanteds (Proposal assignments) ; new_wanteds <- sequence [ new_wtd_ct wtd | CtWanted wtd <- map ctEvidence wanteds ] - ; residual_wc <- solveSimpleWanteds (listToBag new_wanteds) - ; return $ if isEmptyWC residual_wc then Just (tvs, subst) else Nothing } + ; residual <- solveSimpleWanteds (listToBag new_wanteds) + ; return $ if isEmptyBag residual then Just (tvs, subst) else Nothing } | otherwise = return Nothing ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -10,6 +10,8 @@ module GHC.Tc.Solver.Equality( import GHC.Prelude +import {-# SOURCE #-} GHC.Tc.Solver.Solve( trySolveImplication ) + import GHC.Tc.Solver.Irred( solveIrred ) import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance ) import GHC.Tc.Solver.Rewrite @@ -468,7 +470,7 @@ can_eq_nc_forall :: CtEvidence -> EqRel -- See Note [Solving forall equalities] can_eq_nc_forall ev eq_rel s1 s2 - | CtWanted (WantedCt { ctev_dest = orig_dest }) <- ev + | CtWanted (WantedCt { ctev_dest = orig_dest, ctev_loc = loc }) <- ev = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2 flags1 = binderFlags bndrs1 flags2 = binderFlags bndrs2 @@ -479,11 +481,11 @@ can_eq_nc_forall ev eq_rel s1 s2 , ppr flags1, ppr flags2 ] ; canEqHardFailure ev s1 s2 } - else do { - traceTcS "Creating implication for polytype equality" (ppr ev) - ; let free_tvs = tyCoVarsOfTypes [s1,s2] - empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs - ; skol_info <- mkSkolemInfo (UnifyForAllSkol phi1) + else + do { let free_tvs = tyCoVarsOfTypes [s1,s2] + empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs + skol_info_anon = UnifyForAllSkol phi1 + ; skol_info <- mkSkolemInfo skol_info_anon ; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $ binderVars bndrs1 @@ -522,16 +524,34 @@ can_eq_nc_forall ev eq_rel s1 s2 init_subst2 = mkEmptySubst (substInScopeSet subst1) + ; traceTcS "Generating wanteds" (ppr s1 $$ ppr s2) + -- Generate the constraints that live in the body of the implication -- See (SF5) in Note [Solving forall equalities] ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $ unifyForAllBody ev (eqRelRole eq_rel) $ \uenv -> go uenv skol_tvs init_subst2 bndrs1 bndrs2 - ; emitTvImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs wanteds - - ; setWantedEq orig_dest all_co - ; stopWith ev "Deferred polytype equality" } } + -- Solve the implication right away, using `trySolveImplication` + -- See (SF6) in Note [Solving forall equalities] + ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds) + ; ev_binds_var <- newNoTcEvBinds + ; solved <- trySolveImplication $ + (implicationPrototype (ctLocEnv loc)) + { ic_tclvl = lvl + , ic_binds = ev_binds_var + , ic_info = skol_info_anon + , ic_warn_inaccessible = False + , ic_skols = skol_tvs + , ic_given = [] + , ic_wanted = emptyWC { wc_simple = wanteds } } + + ; if solved + then do { zonked_all_co <- zonkCo all_co + -- ToDo: explain this zonk + ; setWantedEq orig_dest zonked_all_co + ; stopWith ev "Polytype equality: solved" } + else canEqSoftFailure IrredShapeReason ev s1 s2 } } | otherwise = do { traceTcS "Omitting decomposition of given polytype equality" $ @@ -556,7 +576,8 @@ can_eq_nc_forall ev eq_rel s1 s2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To solve an equality between foralls [W] (forall a. t1) ~ (forall b. t2) -the basic plan is simple: just create the implication constraint +the basic plan is simple: use `trySolveImplication` to solve the +implication constraint [W] forall a. { t1 ~ (t2[a/b]) } The evidence we produce is a ForAllCo; see the typing rule for @@ -601,6 +622,21 @@ There are lots of wrinkles of course: especially Refl ones. We use the `unifyForAllBody` wrapper for `uType`, because we want to /gather/ the equality constraint (to put in the implication) rather than /emit/ them into the monad, as `wrapUnifierTcS` does. + +(SF6) We solve the implication on the spot, using `trySolveImplication`. In + the past we instead generated an `Implication` to be solved later. Nice in + some ways but it added complexity: + - We needed a `wl_implics` field of `WorkList` to collect + these emitted implications + - The types of `solveSimpleWanteds` and friends were more complicated + - Trickily, an `EvFun` had to contain an `EvBindsVar` ref-cell, which made + `evVarsOfTerm` harder. Now an `EvFun` just contains the bindings. + The disadvantage of solve-on-the-spot is that if we fail we are simply + left with an unsolved (forall a. blah) ~ (forall b. blah), and it may + not be clear /why/ we couldn't solve it. But on balance the error messages + improve: it is easier to undertand that + (forall a. a->a) ~ (forall b. b->Int) + is insoluble than it is to understand a message about matching `a` with `Int`. -} {- Note [Unwrap newtypes first] @@ -834,18 +870,26 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2) = do { inerts <- getInertSet ; if can_decompose inerts then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2) - else canEqSoftFailure ev eq_rel ty1 ty2 } + else assert (eq_rel == ReprEq) $ + canEqSoftFailure ReprEqReason ev ty1 ty2 } -- See Note [Skolem abstract data] in GHC.Core.Tycon | tyConSkolem tc1 || tyConSkolem tc2 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2) ; finishCanWithIrred AbstractTyConReason ev } - | otherwise -- Different TyCons - = if both_generative -- See (TC2) and (TC3) in - -- Note [Canonicalising TyCon/TyCon equalities] - then canEqHardFailure ev ty1 ty2 - else canEqSoftFailure ev eq_rel ty1 ty2 + -- Different TyCons + | NomEq <- eq_rel + = canEqHardFailure ev ty1 ty2 + + -- Different TyCons, eq_rel = ReprEq + -- See (TC2) and (TC3) in + -- Note [Canonicalising TyCon/TyCon equalities] + | both_generative + = canEqHardFailure ev ty1 ty2 + + | otherwise + = canEqSoftFailure ReprEqReason ev ty1 ty2 where -- See Note [Decomposing TyConApp equalities] -- and Note [Decomposing newtype equalities] @@ -1417,20 +1461,18 @@ canDecomposableFunTy ev eq_rel af f1@(ty1,m1,a1,r1) f2@(ty2,m2,a2,r2) -- | Call canEqSoftFailure when canonicalizing an equality fails, but if the -- equality is representational, there is some hope for the future. -canEqSoftFailure :: CtEvidence -> EqRel -> TcType -> TcType +canEqSoftFailure :: CtIrredReason -> CtEvidence -> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a)) -canEqSoftFailure ev NomEq ty1 ty2 - = canEqHardFailure ev ty1 ty2 -canEqSoftFailure ev ReprEq ty1 ty2 +canEqSoftFailure reason ev ty1 ty2 = do { (redn1, rewriters1) <- rewrite ev ty1 ; (redn2, rewriters2) <- rewrite ev ty2 -- We must rewrite the types before putting them in the -- inert set, so that we are sure to kick them out when -- new equalities become available - ; traceTcS "canEqSoftFailure with ReprEq" $ + ; traceTcS "canEqSoftFailure" $ vcat [ ppr ev, ppr redn1, ppr redn2 ] ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2 - ; finishCanWithIrred ReprEqReason new_ev } + ; finishCanWithIrred reason new_ev } -- | Call when canonicalizing an equality fails with utterly no hope. canEqHardFailure :: CtEvidence -> TcType -> TcType @@ -2681,7 +2723,7 @@ tryInertEqs :: EqCt -> SolverStage () tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel }) = Stage $ do { inerts <- getInertCans - ; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item + ; if | Just (ev_i, swapped) <- inertsEqsCanDischarge inerts work_item -> do { setEvBindIfWanted ev EvCanonical $ evCoercion (maybeSymCo swapped $ downgradeRole (eqRelRole eq_rel) @@ -2692,10 +2734,10 @@ tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel }) | otherwise -> continueWith () } -inertsCanDischarge :: InertCans -> EqCt - -> Maybe ( CtEvidence -- The evidence for the inert - , SwapFlag ) -- Whether we need mkSymCo -inertsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w +inertsEqsCanDischarge :: InertCans -> EqCt + -> Maybe ( CtEvidence -- The evidence for the inert + , SwapFlag ) -- Whether we need mkSymCo +inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w , eq_ev = ev_w, eq_eq_rel = eq_rel }) | (ev_i : _) <- [ ev_i | EqCt { eq_ev = ev_i, eq_rhs = rhs_i , eq_eq_rel = eq_rel } @@ -2741,7 +2783,7 @@ inertsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w -- Prefer the one that has no rewriters -- See (CE4) in Note [Combining equalities] -inertsCanDischarge _ _ = Nothing +inertsEqsCanDischarge _ _ = Nothing ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -154,17 +154,6 @@ So we arrange to put these particular class constraints in the wl_eqs. NB: since we do not currently apply the substitution to the inert_solved_dicts, the knot-tying still seems a bit fragile. But this makes it better. - -Note [Residual implications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The wl_implics in the WorkList are the residual implication -constraints that are generated while solving or canonicalising the -current worklist. Specifically, when canonicalising - (forall a. t1 ~ forall a. t2) -from which we get the implication - (forall a. t1 ~ t2) -See GHC.Tc.Solver.Monad.deferTcSForAllEq - -} -- See Note [WorkList priorities] @@ -186,8 +175,6 @@ data WorkList -- in GHC.Tc.Types.Constraint for more details. , wl_rest :: [Ct] - - , wl_implics :: Bag Implication -- See Note [Residual implications] } isNominalEqualityCt :: Ct -> Bool @@ -202,15 +189,12 @@ isNominalEqualityCt ct appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList - (WL { wl_eqs_N = eqs1_N, wl_eqs_X = eqs1_X, wl_rw_eqs = rw_eqs1 - , wl_rest = rest1, wl_implics = implics1 }) - (WL { wl_eqs_N = eqs2_N, wl_eqs_X = eqs2_X, wl_rw_eqs = rw_eqs2 - , wl_rest = rest2, wl_implics = implics2 }) + (WL { wl_eqs_N = eqs1_N, wl_eqs_X = eqs1_X, wl_rw_eqs = rw_eqs1, wl_rest = rest1 }) + (WL { wl_eqs_N = eqs2_N, wl_eqs_X = eqs2_X, wl_rw_eqs = rw_eqs2, wl_rest = rest2 }) = WL { wl_eqs_N = eqs1_N ++ eqs2_N , wl_eqs_X = eqs1_X ++ eqs2_X , wl_rw_eqs = rw_eqs1 ++ rw_eqs2 - , wl_rest = rest1 ++ rest2 - , wl_implics = implics1 `unionBags` implics2 } + , wl_rest = rest1 ++ rest2 } workListSize :: WorkList -> Int workListSize (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs, wl_rest = rest }) @@ -268,9 +252,6 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } -extendWorkListImplic :: Implication -> WorkList -> WorkList -extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } - extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic about what kind of constraint extendWorkListCt ct wl @@ -294,18 +275,18 @@ extendWorkListCts :: Cts -> WorkList -> WorkList extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool -isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs - , wl_rest = rest, wl_implics = implics }) - = null eqs_N && null eqs_X && null rw_eqs && null rest && isEmptyBag implics +isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X + , wl_rw_eqs = rw_eqs, wl_rest = rest }) + = null eqs_N && null eqs_X && null rw_eqs && null rest emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = [] - , wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag } + , wl_rw_eqs = [], wl_rest = [] } -- Pretty printing instance Outputable WorkList where - ppr (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs - , wl_rest = rest, wl_implics = implics }) + ppr (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X + , wl_rw_eqs = rw_eqs, wl_rest = rest }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs_N) $ text "Eqs_N =" <+> vcat (map ppr eqs_N) @@ -315,9 +296,6 @@ instance Outputable WorkList where text "RwEqs =" <+> vcat (map ppr rw_eqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) - , ppUnless (isEmptyBag implics) $ - ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) - (text "(Implics omitted)") ]) {- ********************************************************************* ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -120,19 +120,17 @@ simplify_loop n limit definitely_redo_implications , int (lengthBag simples) <+> text "simples to solve" ]) ; traceTcS "simplify_loop: wc =" (ppr wc) - ; (unifs1, wc1) <- reportUnifications $ -- See Note [Superclass iteration] - solveSimpleWanteds simples + ; (unifs1, simples1) <- reportUnifications $ -- See Note [Superclass iteration] + solveSimpleWanteds simples -- Any insoluble constraints are in 'simples' and so get rewritten -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet ; wc2 <- if not definitely_redo_implications -- See Note [Superclass iteration] && unifs1 == 0 -- for this conditional - && isEmptyBag (wc_impl wc1) - then return (wc { wc_simple = wc_simple wc1 }) -- Short cut - else do { implics2 <- solveNestedImplications $ - implics `unionBags` (wc_impl wc1) - ; return (wc { wc_simple = wc_simple wc1 - , wc_impl = implics2 }) } + then return (wc { wc_simple = simples1 }) -- Short cut + else do { implics1 <- solveNestedImplications implics + ; return (wc { wc_simple = simples1 + , wc_impl = implics1 }) } ; unif_happened <- resetUnificationFlag ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened @@ -262,6 +260,11 @@ more meaningful error message (see T19627) This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field. -} +{- ******************************************************************************** +* * +* Solving implication constraints * +* * +******************************************************************************** -} solveNestedImplications :: Bag Implication -> TcS (Bag Implication) @@ -282,8 +285,37 @@ solveNestedImplications implics ; return unsolved_implics } +{- Note [trySolveImplication] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +`trySolveImplication` may be invoked while solving simple wanteds, notably from +`solveWantedForAll`. It returns a Bool to say if solving succeeded or failed. + +It uses `nestImplicTcS` to build a nested scope. One subtle point is that +`nestImplicTcS` uses the `inert_givens` (not the `inert_cans`) of the current +inert set to initialse the `InertSet` of the nested scope. It is super-important not +to pollute the sub-solving problem with the unsolved Wanteds of the current scope. + +Whenever we do `solveSimpleGivens`, we snapshot the `inert_cans` into `inert_givens`. +(At that moment there should be no Wanteds.) +-} + +trySolveImplication :: Implication -> TcS Bool +-- See Note [trySolveImplication] +trySolveImplication (Implic { ic_tclvl = tclvl + , ic_binds = ev_binds_var + , ic_given = given_ids + , ic_wanted = wanteds + , ic_env = ct_loc_env + , ic_info = info }) + = nestImplicTcS ev_binds_var tclvl $ + do { let loc = mkGivenLoc tclvl info ct_loc_env + givens = mkGivens loc given_ids + ; solveSimpleGivens givens + ; residual_wanted <- solveWanteds wanteds + ; return (isSolvedWC residual_wanted) } + solveImplication :: Implication -- Wanted - -> TcS Implication -- Simplified implication (empty or singleton) + -> TcS Implication -- Simplified implication -- Precondition: The TcS monad contains an empty worklist and given-only inerts -- which after trying to solve this implication we must restore to their original value solveImplication imp@(Implic { ic_tclvl = tclvl @@ -291,6 +323,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl , ic_given = given_ids , ic_wanted = wanteds , ic_info = info + , ic_env = ct_loc_env , ic_status = status }) | isSolvedStatus status = return imp -- Do nothing @@ -308,7 +341,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -- Solve the nested constraints ; (has_given_eqs, given_insols, residual_wanted) <- nestImplicTcS ev_binds_var tclvl $ - do { let loc = mkGivenLoc tclvl info (ic_env imp) + do { let loc = mkGivenLoc tclvl info ct_loc_env givens = mkGivens loc given_ids ; solveSimpleGivens givens @@ -534,7 +567,7 @@ neededEvVars implic@(Implic { ic_info = info , ic_need_implic = old_need_implic -- See (TRC1) }) = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var - ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var + ; used_cos <- TcS.getTcEvTyCoVars ev_binds_var ; let -- Find the variables needed by `implics` new_need_implic@(ENS { ens_dms = dm_seeds, ens_fvs = other_seeds }) @@ -544,7 +577,8 @@ neededEvVars implic@(Implic { ic_info = info -- Get the variables needed by the solved bindings -- (It's OK to use a non-deterministic fold here -- because add_wanted is commutative.) - seeds_w = nonDetStrictFoldEvBindMap add_wanted tcvs ev_binds + used_covars = coVarsOfCos used_cos + seeds_w = nonDetStrictFoldEvBindMap add_wanted used_covars ev_binds need_ignoring_dms = findNeededGivenEvVars ev_binds (other_seeds `unionVarSet` seeds_w) need_from_dms = findNeededGivenEvVars ev_binds dm_seeds @@ -565,7 +599,7 @@ neededEvVars implic@(Implic { ic_info = info ; traceTcS "neededEvVars" $ vcat [ text "old_need_implic:" <+> ppr old_need_implic , text "new_need_implic:" <+> ppr new_need_implic - , text "tcvs:" <+> ppr tcvs + , text "used_covars:" <+> ppr used_covars , text "need_ignoring_dms:" <+> ppr need_ignoring_dms , text "need_from_dms:" <+> ppr need_from_dms , text "need:" <+> ppr need @@ -589,7 +623,7 @@ neededEvVars implic@(Implic { ic_info = info add_wanted :: EvBind -> VarSet -> VarSet add_wanted (EvBind { eb_info = info, eb_rhs = rhs }) needs | EvBindGiven{} <- info = needs -- Add the rhs vars of the Wanted bindings only - | otherwise = evVarsOfTerm rhs `unionVarSet` needs + | otherwise = nestedEvIdsOfTerm rhs `unionVarSet` needs is_dm_skol :: SkolemInfoAnon -> Bool is_dm_skol (MethSkol _ is_dm) = is_dm @@ -611,7 +645,7 @@ findNeededGivenEvVars ev_binds seeds | Just ev_bind <- lookupEvBind ev_binds v , EvBind { eb_info = EvBindGiven, eb_rhs = rhs } <- ev_bind -- Look at Given bindings only - = evVarsOfTerm rhs `unionVarSet` needs + = nestedEvIdsOfTerm rhs `unionVarSet` needs | otherwise = needs @@ -1008,17 +1042,13 @@ solveSimpleWanteds simples else return (n, wc2) } -- Done -solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints +solve_simple_wanteds :: Cts -> TcS Cts -- Try solving these constraints -- Affects the unification state (of course) but not the inert set -- The result is not necessarily zonked -solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1, wc_errors = errs }) - = nestTcS $ - do { solveSimples simples1 - ; (implics2, unsolved) <- getUnsolvedInerts - ; return (WC { wc_simple = unsolved - , wc_impl = implics1 `unionBags` implics2 - , wc_errors = errs }) } +solve_simple_wanteds simples + = nestTcS $ do { solveSimples simples + ; getUnsolvedInerts } {- Note [The solveSimpleWanteds loop] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1038,9 +1068,10 @@ Solving a bunch of simple constraints is done in a loop, -- The main solver loop implements Note [Basic Simplifier Plan] --------------------------------------------------------------- + solveSimples :: Cts -> TcS () --- Returns the final InertSet in TcS --- Has no effect on work-list or residual-implications +-- Solve this bag of constraints, +-- returning the final InertSet in TcS -- The constraints are initially examined in left-to-right order solveSimples cts @@ -1124,14 +1155,15 @@ solveCt (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel , eq_lhs = lhs, eq_rhs = rhs })) = solveEquality ev eq_rel (canEqLHSType lhs) rhs -solveCt (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc })) - = do { ev <- rewriteEvidence ev +solveCt (CQuantCan qci@(QCI { qci_ev = ev })) + = do { ev' <- rewriteEvidence ev -- It is (much) easier to rewrite and re-classify than to -- rewrite the pieces and build a Reduction that will rewrite -- the whole constraint - ; case classifyPredType (ctEvPred ev) of - ForAllPred tvs theta body_pred -> - Stage $ solveForAll ev tvs theta body_pred pend_sc + ; case classifyPredType (ctEvPred ev') of + ForAllPred tvs theta body_pred + -> solveForAll (qci { qci_ev = ev', qci_tvs = tvs + , qci_theta = theta, qci_body = body_pred }) _ -> pprPanic "SolveCt" (ppr ev) } solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc })) @@ -1165,7 +1197,7 @@ solveNC ev -- And then re-classify ; case classifyPredType (ctEvPred ev) of ClassPred cls tys -> solveDictNC ev cls tys - ForAllPred tvs th p -> Stage $ solveForAllNC ev tvs th p + ForAllPred tvs th p -> solveForAllNC ev tvs th p IrredPred {} -> solveIrred (IrredCt { ir_ev = ev, ir_reason = IrredShapeReason }) EqPred eq_rel ty1 ty2 -> solveEquality ev eq_rel ty1 ty2 -- EqPred only happens if (say) `c` is unified with `a ~# b`, @@ -1256,50 +1288,49 @@ type signature. -- -- Precondition: the constraint has already been rewritten by the inert set. solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType - -> TcS (StopOrContinue Void) + -> SolverStage Void solveForAllNC ev tvs theta body_pred - | Just (cls,tys) <- getClassPredTys_maybe body_pred - , classHasSCs cls - = do { dflags <- getDynFlags - -- Either expand superclasses (Givens) or provide fuel to do so (Wanteds) - ; if isGiven ev - then - -- See Note [Eagerly expand given superclasses] - -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - do { sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys - ; emitWork (listToBag sc_cts) - ; solveForAll ev tvs theta body_pred doNotExpand } - else - -- See invariants (a) and (b) in QCI.qci_pend_sc - -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - -- See Note [Quantified constraints] - do { solveForAll ev tvs theta body_pred (qcsFuel dflags) } - } + = do { fuel <- simpleStage mk_super_classes + ; solveForAll (QCI { qci_ev = ev, qci_tvs = tvs, qci_theta = theta + , qci_body = body_pred, qci_pend_sc = fuel }) } - | otherwise - = solveForAll ev tvs theta body_pred doNotExpand + where + mk_super_classes :: TcS ExpansionFuel + mk_super_classes + | Just (cls,tys) <- getClassPredTys_maybe body_pred + , classHasSCs cls + = do { dflags <- getDynFlags + -- Either expand superclasses (Givens) or provide fuel to do so (Wanteds) + ; if isGiven ev + then + -- See Note [Eagerly expand given superclasses] + -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + do { sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys + ; emitWork (listToBag sc_cts) + ; return doNotExpand } + else + -- See invariants (a) and (b) in QCI.qci_pend_sc + -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + -- See Note [Quantified constraints] + return (qcsFuel dflags) + } + + | otherwise + = return doNotExpand -- | Solve a canonical quantified constraint. -- -- Precondition: the constraint has already been rewritten by the inert set. -solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel - -> TcS (StopOrContinue Void) -solveForAll ev tvs theta body_pred fuel = - case ev of - CtGiven {} -> - -- See Note [Solving a Given forall-constraint] - do { addInertForAll qci - ; stopWith ev "Given forall-constraint" } - CtWanted wtd -> - -- See Note [Solving a Wanted forall-constraint] - runSolverStage $ - do { tryInertQCs qci - ; Stage $ solveWantedForAll_implic wtd tvs theta body_pred - } - where - qci = QCI { qci_ev = ev, qci_tvs = tvs - , qci_body = body_pred, qci_pend_sc = fuel } - +solveForAll :: QCInst -> SolverStage Void +solveForAll qci@(QCI { qci_ev = ev, qci_tvs = tvs, qci_theta = theta, qci_body = pred }) + = case ev of + CtGiven {} -> + -- See Note [Solving a Given forall-constraint] + do { simpleStage (addInertForAll qci) + ; stopWithStage ev "Given forall-constraint" } + CtWanted wtd -> + do { tryInertQCs qci + ; solveWantedForAll qci tvs theta pred wtd } tryInertQCs :: QCInst -> SolverStage () tryInertQCs qc @@ -1310,7 +1341,8 @@ tryInertQCs qc try_inert_qcs :: QCInst -> [QCInst] -> TcS (StopOrContinue ()) try_inert_qcs (QCI { qci_ev = ev_w }) inerts = case mapMaybe matching_inert inerts of - [] -> continueWith () + [] -> do { traceTcS "tryInertQCs:nothing" (ppr ev_w $$ ppr inerts) + ; continueWith () } ev_i:_ -> do { traceTcS "tryInertQCs:KeepInert" (ppr ev_i) ; setEvBindIfWanted ev_w EvCanonical (ctEvTerm ev_i) @@ -1323,57 +1355,72 @@ try_inert_qcs (QCI { qci_ev = ev_w }) inerts = = Nothing -- | Solve a (canonical) Wanted quantified constraint by emitting an implication. --- -- See Note [Solving a Wanted forall-constraint] -solveWantedForAll_implic :: WantedCtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> TcS (StopOrContinue Void) -solveWantedForAll_implic - wtd@(WantedCt { ctev_dest = dest, ctev_loc = loc, ctev_rewriters = rewriters }) - tvs theta body_pred = - -- We are about to do something irreversible (turning a quantified constraint - -- into an implication), so wrap the inner call in solveCompletelyIfRequired - -- to ensure we can roll back if we can't solve the implication fully. - -- See Note [TcSSpecPrag] in GHC.Tc.Solver.Monad. - solveCompletelyIfRequired (mkNonCanonical $ CtWanted wtd) $ - - -- This setSrcSpan is important: the emitImplicationTcS uses that - -- TcLclEnv for the implication, and that in turn sets the location - -- for the Givens when solving the constraint (#21006) - TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $ - do { let empty_subst = mkEmptySubst $ mkInScopeSet $ - tyCoVarsOfTypes (body_pred:theta) `delVarSetList` tvs - is_qc = IsQC (ctLocOrigin loc) - - -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv] +solveWantedForAll :: QCInst -> [TcTyVar] -> TcThetaType -> PredType + -> WantedCtEvidence -> SolverStage Void +solveWantedForAll qci tvs theta body_pred + wtd@(WantedCt { ctev_dest = dest, ctev_loc = ct_loc + , ctev_rewriters = rewriters }) + = Stage $ + TcS.setSrcSpan (getCtLocEnvLoc loc_env) $ + -- This setSrcSpan is important: the emitImplicationTcS uses that + -- TcLclEnv for the implication, and that in turn sets the location + -- for the Givens when solving the constraint (#21006) + + do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv] -- in GHC.Tc.Utils.TcType -- Very like the code in tcSkolDFunType - ; rec { skol_info <- mkSkolemInfo skol_info_anon + rec { skol_info <- mkSkolemInfo skol_info_anon ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs ; let inst_pred = substTy subst body_pred inst_theta = substTheta subst theta skol_info_anon = InstSkol is_qc (get_size inst_pred) } - ; given_ev_vars <- mapM newEvVar inst_theta - ; (lvl, (w_id, wanteds)) - <- pushLevelNoWorkList (ppr skol_info) $ - do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc) - -- Set the thing to prove to have a ScOrigin, so we are - -- careful about its termination checks. - -- See (QC-INV) in Note [Solving a Wanted forall-constraint] - ; wanted_ev <- newWantedNC loc' rewriters inst_pred - -- NB: inst_pred can be an equality - ; return ( wantedCtEvEvId wanted_ev - , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } - - ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) - ; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds - - ; setWantedEvTerm dest EvCanonical $ - EvFun { et_tvs = skol_tvs, et_given = given_ev_vars - , et_binds = ev_binds, et_body = w_id } - - ; stopWith (CtWanted wtd) "Wanted forall-constraint (implication)" - } + ; given_ev_vars <- mapM newEvVar inst_theta + ; (lvl, (w_id, wanteds)) + <- pushLevelNoWorkList (ppr skol_info) $ + do { let ct_loc' = setCtLocOrigin ct_loc (ScOrigin is_qc NakedSc) + -- Set the thing to prove to have a ScOrigin, so we are + -- careful about its termination checks. + -- See (QC-INV) in Note [Solving a Wanted forall-constraint] + ; wanted_ev <- newWantedNC ct_loc' rewriters inst_pred + -- NB: inst_pred can be an equality + ; return ( wantedCtEvEvId wanted_ev + , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } + + ; traceTcS "solveForAll {" (ppr skol_tvs $$ ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) + + -- Try to solve the constraint completely + ; ev_binds_var <- TcS.newTcEvBinds + ; solved <- trySolveImplication $ + (implicationPrototype loc_env) + { ic_tclvl = lvl + , ic_binds = ev_binds_var + , ic_info = skol_info_anon + , ic_warn_inaccessible = False + , ic_skols = skol_tvs + , ic_given = given_ev_vars + , ic_wanted = emptyWC { wc_simple = wanteds } } + ; traceTcS "solveForAll }" (ppr solved) + ; evbs <- TcS.getTcEvBindsMap ev_binds_var + ; if not solved + then do { -- Not completely solved; abandon that attempt and add the + -- original constraint to the inert set + addInertForAll qci + ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" } + + else do { -- Completely solved; build an evidence term + setWantedEvTerm dest EvCanonical $ + EvFun { et_tvs = skol_tvs, et_given = given_ev_vars + , et_binds = evBindMapBinds evbs, et_body = w_id } + ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } } where + loc_env = ctLocEnv ct_loc + is_qc = IsQC (ctLocOrigin ct_loc) + + empty_subst = mkEmptySubst $ mkInScopeSet $ + tyCoVarsOfTypes (body_pred:theta) `delVarSetList` tvs + -- Getting the size of the head is a bit horrible -- because of the special treament for class predicates get_size pred = case classifyPredType pred of @@ -1384,36 +1431,68 @@ solveWantedForAll_implic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Solving a wanted forall (quantified) constraint [W] df :: forall a b. (Eq a, Ord b) => C x a b -is delightfully easy. Just build an implication constraint +is delightfully easy in principle. Just build an implication constraint forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a and discharge df thus: df = /\ab. \g1 g2. let <binds> in d where <binds> is filled in by solving the implication constraint. All the machinery is to hand; there is little to do. -We can take a more straightforward parth when there is a matching Given, e.g. - [W] dg :: forall c d. (Eq c, Ord d) => C x c d -In this case, it's better to directly solve the Wanted from the Given, instead -of building an implication. This is more than a simple optimisation; see -Note [Solving Wanted QCs from Given QCs]. +There are some tricky corners though: + +(WFA1) We can take a more straightforward path when there is a matching Given, e.g. + [W] dg :: forall c d. (Eq c, Ord d) => C x c d + In this case, it's better to directly solve the Wanted from the Given, instead + of building an implication. This is more than a simple optimisation; see + Note [Solving Wanted QCs from Given QCs]. + +(WFA2) Termination: see #19690. We want to maintain the invariant (QC-INV): + + (QC-INV) Every quantified constraint returns a non-bottom dictionary + + just as every top-level instance declaration guarantees to return a non-bottom + dictionary. But as #19690 shows, it is possible to get a bottom dictionary + by superclass selection if we aren't careful. The situation is very similar + to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance; + and we use the same solution: + + * Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size)) + * Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc) + + Both of these things are done in solveForAll. Now the mechanism described + in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over. + +(WFA3) We do not actually emit an implication to solve later. Rather we + try to solve it completely immediately using `trySolveImplication` + - If successful, we can build evidence + - If unsuccessful, we abandon the attempt and add the unsolved + forall-constraint to the inert set. + Several reasons for this "solve immediately" approach -The tricky point is about termination: see #19690. We want to maintain -the invariant (QC-INV): + - It saves quite a bit of plumbing, tracking the emitted implications for + later solving; and the evidence would have to contain as-yet-incomplte + bindings which complicates tracking of unused Givens. - (QC-INV) Every quantified constraint returns a non-bottom dictionary + - We get better error messages, about failing to solve, say + (forall a. a->a) ~ (forall b. b->Int) -just as every top-level instance declaration guarantees to return a non-bottom -dictionary. But as #19690 shows, it is possible to get a bottom dicionary -by superclass selection if we aren't careful. The situation is very similar -to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance; -and we use the same solution: + - Consider + f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a + {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-} + This SPECIALISE is treated like an expression with a type signature, so + we instantiate the constraints, simplify them and re-generalise. From the + instantiation we get [W] d :: (forall x. Eq a => Eq (f x)) + and we want to generalise over that. We do not want to attempt to solve it + and then get stuck, and emit an error message. If we can't solve it, better + to leave it alone. -* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size)) -* Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc) + We still need to simplify quantified constraints that can be + /fully solved/ from instances, otherwise we would never be able to + specialise them away. Example: {-# SPECIALISE f @[] @a #-}. -Both of these things are done in solveForAll. Now the mechanism described -in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over. + You might worry about the wasted work, but it is seldom repeated (because the + constraint solver seldom iterates much). Note [Solving a Given forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1576,13 +1655,13 @@ runTcPluginsGiven -- work) and a bag of insolubles. The boolean indicates whether -- 'solveSimpleWanteds' should feed the updated wanteds back into the -- main solver. -runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints) -runTcPluginsWanted wc@(WC { wc_simple = simples1 }) +runTcPluginsWanted :: Cts -> TcS (Bool, Cts) +runTcPluginsWanted simples1 | isEmptyBag simples1 - = return (False, wc) + = return (False, simples1) | otherwise = do { solvers <- getTcPluginSolvers - ; if null solvers then return (False, wc) else + ; if null solvers then return (False, simples1) else do { given <- getInertGivens ; wanted <- TcS.zonkSimples simples1 -- Plugin requires zonked inputs @@ -1604,8 +1683,7 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 }) ; mapM_ setEv solved_wanted ; traceTcS "Finished plugins }" (ppr new_wanted) - ; return ( notNull (pluginNewCts p) - , wc { wc_simple = all_new_wanted } ) } } + ; return ( notNull (pluginNewCts p), all_new_wanted ) } } where setEv :: (EvTerm,Ct) -> TcS () setEv (ev,ct) = case ctEvidence ct of ===================================== compiler/GHC/Tc/Solver/Solve.hs-boot ===================================== @@ -0,0 +1,8 @@ +module GHC.Tc.Solver.Solve where + +import Prelude( Bool ) +import GHC.Tc.Solver.Monad( TcS ) +import GHC.Tc.Types.Constraint( Cts, Implication ) + +solveSimpleWanteds :: Cts -> TcS Cts +trySolveImplication :: Implication -> TcS Bool ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -746,8 +746,12 @@ zonk_bind (XHsBindsLR (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs runZonkBndrT (zonkTyBndrsX tyvars ) $ \ new_tyvars -> runZonkBndrT (zonkEvBndrsX evs ) $ \ new_evs -> runZonkBndrT (zonkTcEvBinds_s ev_binds) $ \ new_ev_binds -> - do { (new_val_bind, new_exports) <- mfix $ \ ~(new_val_binds, _) -> - runZonkBndrT (extendIdZonkEnvRec $ collectHsBindsBinders CollNoDictBinders new_val_binds) $ \ _ -> + do { (new_val_bind, new_exports) <- mfix $ \ ~(new_val_binds, new_exports) -> + let new_bndrs = collectHsBindsBinders CollNoDictBinders new_val_binds + ++ map abe_poly new_exports + -- Tie the knot with the `abe_poly` binders too, since they + -- may be mentioned in the `abe_prags` of the `exports` + in runZonkBndrT (extendIdZonkEnvRec new_bndrs) $ \ _ -> do { new_val_binds <- mapM zonk_val_bind val_binds ; new_exports <- mapM zonk_export exports ; return (new_val_binds, new_exports) @@ -854,6 +858,7 @@ zonkLTcSpecPrags ps ; skol_tvs_ref <- lift $ newTcRef [] ; setZonkType (SkolemiseFlexi skol_tvs_ref) $ -- SkolemiseFlexi: see Note [Free tyvars on rule LHS] + runZonkBndrT (zonkCoreBndrsX bndrs) $ \ bndrs' -> do { spec_e' <- zonkLExpr spec_e ; skol_tvs <- lift $ readTcRef skol_tvs_ref @@ -1759,7 +1764,7 @@ zonkEvTerm (EvFun { et_tvs = tvs, et_given = evs , et_binds = ev_binds, et_body = body_id }) = runZonkBndrT (zonkTyBndrsX tvs) $ \ new_tvs -> runZonkBndrT (zonkEvBndrsX evs) $ \ new_evs -> - runZonkBndrT (zonkTcEvBinds ev_binds) $ \ new_ev_binds -> + runZonkBndrT (zonkEvBinds ev_binds) $ \ new_ev_binds -> do { new_body_id <- zonkIdOcc body_id ; return (EvFun { et_tvs = new_tvs, et_given = new_evs , et_binds = new_ev_binds, et_body = new_body_id }) } ===================================== testsuite/tests/deriving/should_compile/T20815.hs ===================================== @@ -12,3 +12,5 @@ instance Alt [] where () = (++) newtype L a = L [a] deriving (Functor, Alt) + +newtype T f a = T (f a) deriving (Functor, Alt) ===================================== testsuite/tests/impredicative/T17332.stderr ===================================== @@ -1,7 +1,6 @@ - T17332.hs:13:7: error: [GHC-05617] - • Could not solve: ‘a’ - arising from the head of a quantified constraint + • Could not solve: ‘forall (a :: Constraint). a’ arising from a use of ‘MkDict’ • In the expression: MkDict In an equation for ‘aux’: aux = MkDict + ===================================== testsuite/tests/quantified-constraints/T15290a.stderr ===================================== @@ -1,9 +1,9 @@ T15290a.hs:25:12: error: [GHC-18872] - • Couldn't match representation of type: m (Int, IntStateT m a1) - with that of: m (Int, StateT Int m a1) + • Couldn't match representation of type: forall a. + StateT Int m (StateT Int m a) -> StateT Int m a + with that of: forall a. + IntStateT m (IntStateT m a) -> IntStateT m a arising from a use of ‘coerce’ - Note: We cannot know what roles the parameters to ‘m’ have; - we must assume that the role is nominal. • In the expression: coerce @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a) ===================================== testsuite/tests/quantified-constraints/T19690.stderr ===================================== @@ -1,10 +1,5 @@ - T19690.hs:12:16: error: [GHC-05617] - • Could not deduce ‘c’ - arising from the head of a quantified constraint - arising from a use of ‘go’ - from the context: Hold c - bound by a quantified context at T19690.hs:12:16-17 + • Could not solve: ‘Hold c => c’ arising from a use of ‘go’ • In the expression: go In an equation for ‘anythingDict’: anythingDict @@ -12,5 +7,4 @@ T19690.hs:12:16: error: [GHC-05617] where go :: (Hold c => c) => Dict c go = Dict - • Relevant bindings include - anythingDict :: Dict c (bound at T19690.hs:12:1) + ===================================== testsuite/tests/quantified-constraints/T19921.stderr ===================================== @@ -1,12 +1,6 @@ - T19921.hs:29:8: error: [GHC-05617] - • Could not deduce ‘r’ - arising from the head of a quantified constraint - arising from the head of a quantified constraint + • Could not solve: ‘((x \/ y) \/ z) ⇒ (x \/ (y \/ z))’ arising from a use of ‘Dict’ - from the context: (x \/ y) \/ z - bound by a quantified context at T19921.hs:29:8-11 - or from: (x ⇒ r, (y \/ z) ⇒ r) - bound by a quantified context at T19921.hs:29:8-11 • In the expression: Dict In an equation for ‘dict’: dict = Dict + ===================================== testsuite/tests/quantified-constraints/T21006.stderr ===================================== @@ -1,8 +1,7 @@ - T21006.hs:14:10: error: [GHC-05617] - • Could not deduce ‘c’ - arising from the head of a quantified constraint + • Could not solve: ‘forall b (c :: Constraint). + (Determines b, Determines c) => + c’ arising from the superclasses of an instance declaration - from the context: (Determines b, Determines c) - bound by a quantified context at T21006.hs:14:10-15 • In the instance declaration for ‘OpCode’ + ===================================== testsuite/tests/typecheck/should_compile/T12427a.stderr ===================================== @@ -1,4 +1,3 @@ - T12427a.hs:17:29: error: [GHC-91028] • Couldn't match expected type ‘p’ with actual type ‘(forall b. [b] -> [b]) -> Int’ @@ -24,12 +23,11 @@ T12427a.hs:28:6: error: [GHC-91028] • In the pattern: T1 _ x1 In a pattern binding: T1 _ x1 = undefined -T12427a.hs:41:6: error: [GHC-25897] - • Couldn't match type ‘b’ with ‘[b]’ +T12427a.hs:41:6: error: [GHC-83865] + • Couldn't match type: forall b. [b] -> [b] + with: forall a. a -> a Expected: (forall b. [b] -> [b]) -> Int Actual: (forall a. a -> a) -> Int - ‘b’ is a rigid type variable bound by - the type [b] -> [b] - at T12427a.hs:41:1-19 • In the pattern: T1 _ x3 In a pattern binding: T1 _ x3 = undefined + ===================================== testsuite/tests/typecheck/should_fail/T14605.hs ===================================== @@ -6,6 +6,8 @@ -- -- The ticket #14605 has a much longer example that -- also fails; it does not use ImpredicativeTypes +-- +-- The error message is not great; but it's an obscure program module T14605 where ===================================== testsuite/tests/typecheck/should_fail/T14605.stderr ===================================== @@ -1,10 +1,8 @@ - -T14605.hs:14:13: error: [GHC-10283] - • Couldn't match representation of type ‘x’ with that of ‘()’ +T14605.hs:16:13: error: [GHC-18872] + • Couldn't match representation of type: forall x. () + with that of: forall x. x arising from a use of ‘coerce’ - ‘x’ is a rigid type variable bound by - the type () - at T14605.hs:14:1-49 • In the expression: coerce @(forall x. ()) @(forall x. x) In an equation for ‘duplicate’: duplicate = coerce @(forall x. ()) @(forall x. x) + ===================================== testsuite/tests/typecheck/should_fail/T15801.stderr ===================================== @@ -1,7 +1,6 @@ - -T15801.hs:52:10: error: [GHC-18872] - • Couldn't match representation of type: UnOp op_a -> UnOp b - with that of: op_a --> b - arising from the head of a quantified constraint +T15801.hs:52:10: error: [GHC-05617] + • Could not solve: ‘forall (op_a :: Op (*)) (b :: Op (*)). + op_a -#- b’ arising from the superclasses of an instance declaration • In the instance declaration for ‘OpRíki (Op (*))’ + ===================================== testsuite/tests/typecheck/should_fail/T18640a.stderr ===================================== @@ -1,9 +1,5 @@ - -T18640a.hs:12:1: error: [GHC-25897] - • Couldn't match kind ‘a’ with ‘*’ - Expected: forall (b :: k). * -> * - Actual: forall (b :: k). * -> a - ‘a’ is a rigid type variable bound by - the type family declaration for ‘F2’ - at T18640a.hs:12:17 +T18640a.hs:12:1: error: [GHC-83865] + • Couldn't match expected kind: forall (b :: k). * -> * + with actual kind: forall (b :: k). * -> a • In the type family declaration for ‘F2’ + ===================================== testsuite/tests/typecheck/should_fail/T18640b.stderr ===================================== @@ -1,12 +1,5 @@ - -T18640b.hs:14:10: error: [GHC-25897] - • Couldn't match kind ‘k’ with ‘a’ - Expected kind ‘forall b -> a’, but ‘F1’ has kind ‘forall k -> k’ - ‘k’ is a rigid type variable bound by - the type k - at T18640b.hs:14:3-11 - ‘a’ is a rigid type variable bound by - a family instance declaration - at T18640b.hs:14:6 +T18640b.hs:14:10: error: [GHC-83865] + • Expected kind ‘forall b -> a’, but ‘F1’ has kind ‘forall k -> k’ • In the type ‘F1’ In the type family declaration for ‘F3’ + ===================================== testsuite/tests/typecheck/should_fail/T19627.stderr ===================================== @@ -18,28 +18,3 @@ T19627.hs:108:3: error: [GHC-05617] Not (p a b) -> b <#- a In the class declaration for ‘Lol’ -T19627.hs:108:3: error: [GHC-05617] - • Could not deduce ‘Not (Not (p0 a1 b1)) ~ p0 a1 b1’ - arising from a superclass required to satisfy ‘Prop (p0 a1 b1)’, - arising from the head of a quantified constraint - arising from a superclass required to satisfy ‘Iso p0’, - arising from a superclass required to satisfy ‘Lol p0’, - arising from a type ambiguity check for - the type signature for ‘apartR’ - from the context: Lol p - bound by the type signature for: - apartR :: forall (p :: * -> * -> *) a b. - Lol p => - Not (p a b) -> b <#- a - at T19627.hs:108:3-34 - or from: (Prop a1, Prop b1) - bound by a quantified context at T19627.hs:108:3-34 - The type variable ‘p0’ is ambiguous - • In the ambiguity check for ‘apartR’ - To defer the ambiguity check to use sites, enable AllowAmbiguousTypes - When checking the class method: - apartR :: forall (p :: * -> * -> *) a b. - Lol p => - Not (p a b) -> b <#- a - In the class declaration for ‘Lol’ - ===================================== testsuite/tests/typecheck/should_fail/T21530b.stderr ===================================== @@ -1,8 +1,8 @@ - T21530b.hs:9:5: error: [GHC-83865] - • Couldn't match type: Eq a => a -> String - with: a -> String + • Couldn't match type: forall a. (Show a, Eq a) => a -> String + with: forall a. Show a => a -> String Expected: (forall a. Show a => a -> String) -> String Actual: (forall a. (Show a, Eq a) => a -> String) -> String • In the expression: f In an equation for ‘g’: g = f + ===================================== testsuite/tests/typecheck/should_fail/T22912.stderr ===================================== @@ -1,16 +1,6 @@ - -T22912.hs:17:16: error: [GHC-39999] - • Could not deduce ‘Implies c’ - arising from the head of a quantified constraint +T22912.hs:17:16: error: [GHC-05617] + • Could not solve: ‘Exactly (Implies c) => Implies c’ arising from a use of ‘go’ - from the context: Exactly (Implies c) - bound by a quantified context at T22912.hs:17:16-17 - Possible fix: - add (Implies c) to the context of - the type signature for: - anythingDict :: forall (c :: Constraint). Dict c - or If the constraint looks soluble from a superclass of the instance context, - read 'Undecidable instances and loopy superclasses' in the user manual • In the expression: go In an equation for ‘anythingDict’: anythingDict @@ -18,3 +8,4 @@ T22912.hs:17:16: error: [GHC-39999] where go :: (Exactly (Implies c) => Implies c) => Dict c go = Dict + ===================================== testsuite/tests/typecheck/should_fail/tcfail174.stderr ===================================== @@ -1,33 +1,22 @@ - -tcfail174.hs:20:14: error: [GHC-25897] - • Couldn't match type ‘a1’ with ‘a’ +tcfail174.hs:20:14: error: [GHC-83865] + • Couldn't match type: forall a1. a1 -> a1 + with: forall x. x -> a Expected: Capture (forall x. x -> a) Actual: Capture (forall a. a -> a) - ‘a1’ is a rigid type variable bound by - the type a -> a - at tcfail174.hs:20:1-14 - ‘a’ is a rigid type variable bound by - the inferred type of h1 :: Capture a - at tcfail174.hs:20:1-14 • In the first argument of ‘Capture’, namely ‘g’ In the expression: Capture g In an equation for ‘h1’: h1 = Capture g • Relevant bindings include h1 :: Capture a (bound at tcfail174.hs:20:1) -tcfail174.hs:23:14: error: [GHC-25897] - • Couldn't match type ‘a’ with ‘b’ +tcfail174.hs:23:14: error: [GHC-83865] + • Couldn't match type: forall a. a -> a + with: forall x. x -> b Expected: Capture (forall x. x -> b) Actual: Capture (forall a. a -> a) - ‘a’ is a rigid type variable bound by - the type a -> a - at tcfail174.hs:1:1 - ‘b’ is a rigid type variable bound by - the type signature for: - h2 :: forall b. Capture b - at tcfail174.hs:22:1-15 • In the first argument of ‘Capture’, namely ‘g’ In the expression: Capture g In an equation for ‘h2’: h2 = Capture g • Relevant bindings include h2 :: Capture b (bound at tcfail174.hs:23:1) + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d433cb52777c4eb4784d29c52397221... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d433cb52777c4eb4784d29c52397221... You're receiving this email because of your account on gitlab.haskell.org.