{-# LANGUAGE CPP #-} module GHC.Tc.Solver( simplifyInfer, InferMode(..), growThetaTyVars, simplifyAmbiguityCheck, simplifyDefault, simplifyTop, simplifyTopImplic, simplifyInteractive, solveEqualities, solveLocalEqualities, solveLocalEqualitiesX, simplifyWantedsTcM, tcCheckSatisfiability, tcNormalise, captureTopConstraints, simpl_top, promoteTyVarSet, emitFlatConstraints, -- For Rules we need these solveWanteds, solveWantedsAndDrop, approximateWC, runTcSDeriveds ) where #include "HsVersions.h" import GHC.Prelude import GHC.Data.Bag import GHC.Core.Class ( Class, classKey, classTyCon ) import GHC.Driver.Session import GHC.Types.Id ( idType ) import GHC.Tc.Utils.Instantiate import GHC.Data.List.SetOps import GHC.Types.Name import GHC.Utils.Outputable import GHC.Builtin.Utils import GHC.Builtin.Names import GHC.Tc.Errors import GHC.Tc.Types.Evidence import GHC.Tc.Solver.Interact import GHC.Tc.Solver.Canonical ( makeSuperClasses, solveCallStack ) import GHC.Tc.Solver.Flatten ( flattenType ) import GHC.Tc.Utils.TcMType as TcM import GHC.Tc.Utils.Monad as TcM import GHC.Tc.Solver.Monad as TcS import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType import GHC.Core.Type import GHC.Builtin.Types ( liftedRepTy ) import GHC.Core.Unify ( tcMatchTyKi ) import GHC.Utils.Misc import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Unique.Set import GHC.Types.Basic ( IntWithInf, intGtLimit ) import GHC.Utils.Error ( emptyMessages ) import qualified GHC.LanguageExtensions as LangExt import Control.Monad import Data.Foldable ( toList ) import Data.List ( partition ) import Data.List.NonEmpty ( NonEmpty(..) ) {- ********************************************************************************* * * * External interface * * * ********************************************************************************* -} captureTopConstraints :: TcM a -> TcM (a, WantedConstraints) -- (captureTopConstraints m) runs m, and returns the type constraints it -- generates plus the constraints produced by static forms inside. -- If it fails with an exception, it reports any insolubles -- (out of scope variables) before doing so -- -- captureTopConstraints is used exclusively by GHC.Tc.Module at the top -- level of a module. -- -- Importantly, if captureTopConstraints propagates an exception, it -- reports any insoluble constraints first, lest they be lost -- altogether. This is important, because solveLocalEqualities (maybe -- other things too) throws an exception without adding any error -- messages; it just puts the unsolved constraints back into the -- monad. See GHC.Tc.Utils.Monad Note [Constraints and errors] -- #16376 is an example of what goes wrong if you don't do this. -- -- NB: the caller should bring any environments into scope before -- calling this, so that the reportUnsolved has access to the most -- complete GlobalRdrEnv captureTopConstraints thing_inside = do { static_wc_var <- TcM.newTcRef emptyWC ; ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $ TcM.tryCaptureConstraints thing_inside ; stWC <- TcM.readTcRef static_wc_var -- See GHC.Tc.Utils.Monad Note [Constraints and errors] -- If the thing_inside threw an exception, but generated some insoluble -- constraints, report the latter before propagating the exception -- Otherwise they will be lost altogether ; case mb_res of Just res -> return (res, lie `andWC` stWC) Nothing -> do { _ <- simplifyTop lie; failM } } -- This call to simplifyTop is the reason -- this function is here instead of GHC.Tc.Utils.Monad -- We call simplifyTop so that it does defaulting -- (esp of runtime-reps) before reporting errors simplifyTopImplic :: Bag Implication -> TcM () simplifyTopImplic implics = do { empty_binds <- simplifyTop (mkImplicWC implics) -- Since all the inputs are implications the returned bindings will be empty ; MASSERT2( isEmptyBag empty_binds, ppr empty_binds ) ; return () } simplifyTop :: WantedConstraints -> TcM (Bag EvBind) -- Simplify top-level constraints -- Usually these will be implications, -- but when there is nothing to quantify we don't wrap -- in a degenerate implication, so we do that here instead simplifyTop wanteds = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds ; ((final_wc, unsafe_ol), binds1) <- runTcS $ do { final_wc <- simpl_top wanteds ; unsafe_ol <- getSafeOverlapFailures ; return (final_wc, unsafe_ol) } ; traceTc "End simplifyTop }" empty ; binds2 <- reportUnsolved final_wc ; traceTc "reportUnsolved (unsafe overlapping) {" empty ; unless (isEmptyCts unsafe_ol) $ do { -- grab current error messages and clear, warnAllUnsolved will -- update error messages which we'll grab and then restore saved -- messages. ; errs_var <- getErrsVar ; saved_msg <- TcM.readTcRef errs_var ; TcM.writeTcRef errs_var emptyMessages ; warnAllUnsolved $ emptyWC { wc_simple = unsafe_ol } ; whyUnsafe <- fst <$> TcM.readTcRef errs_var ; TcM.writeTcRef errs_var saved_msg ; recordUnsafeInfer whyUnsafe } ; traceTc "reportUnsolved (unsafe overlapping) }" empty ; return (evBindMapBinds binds1 `unionBags` binds2) } -- | Type-check a thing that emits only equality constraints, solving any -- constraints we can and re-emitting constraints that we can't. The thing_inside -- should generally bump the TcLevel to make sure that this run of the solver -- doesn't affect anything lying around. solveLocalEqualities :: String -> TcM a -> TcM a -- Note [Failure in local type signatures] solveLocalEqualities callsite thing_inside = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside ; emitFlatConstraints wanted ; return res } emitFlatConstraints :: WantedConstraints -> TcM () -- See Note [Failure in local type signatures] emitFlatConstraints wanted = do { wanted <- TcM.zonkWC wanted ; case floatKindEqualities wanted of Nothing -> do { traceTc "emitFlatConstraints: failing" (ppr wanted) ; emitConstraints wanted -- So they get reported! ; failM } Just (simples, holes) -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples) ; traceTc "emitFlatConstraints:" $ vcat [ text "simples:" <+> ppr simples , text "holes: " <+> ppr holes ] ; emitHoles holes -- Holes don't need promotion ; emitSimples simples } } floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole) -- Float out all the constraints from the WantedConstraints, -- Return Nothing if any constraints can't be floated (captured -- by skolems), or if there is an insoluble constraint, or -- IC_Telescope telescope error floatKindEqualities wc = float_wc emptyVarSet wc where float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole) float_wc trapping_tvs (WC { wc_simple = simples , wc_impl = implics , wc_holes = holes }) | all is_floatable simples = do { (inner_simples, inner_holes) <- flatMapBagPairM (float_implic trapping_tvs) implics ; return ( simples `unionBags` inner_simples , holes `unionBags` inner_holes) } | otherwise = Nothing where is_floatable ct | insolubleEqCt ct = False | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag Hole) float_implic trapping_tvs (Implic { ic_wanted = wanted, ic_no_eqs = no_eqs , ic_skols = skols, ic_status = status }) | isInsolubleStatus status = Nothing -- A short cut /plus/ we must keep track of IC_BadTelescope | otherwise = do { (simples, holes) <- float_wc new_trapping_tvs wanted ; when (not (isEmptyBag simples) && not no_eqs) $ Nothing -- If there are some constraints to float out, but we can't -- because we don't float out past local equalities -- (c.f GHC.Tc.Solver.approximateWC), then fail ; return (simples, holes) } where new_trapping_tvs = trapping_tvs `extendVarSetList` skols {- Note [Failure in local type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When kind checking a type signature, we like to fail fast if we can't solve all the kind equality constraints: see Note [Fail fast on kind errors]. But what about /local/ type signatures, mentioning in-scope type variables for which there might be given equalities. Here's an example (T15076b): class (a ~ b) => C a b data SameKind :: k -> k -> Type where { SK :: SameKind a b } bar :: forall (a :: Type) (b :: Type). C a b => Proxy a -> Proxy b -> () bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y) Consider the type singature on 'undefined'. It's ill-kinded unless a~b. But the superclass of (C a b) means that indeed (a~b). So all should be well. BUT it's hard to see that when kind-checking the signature for undefined. We want to emit a residual (a~b) constraint, to solve later. Another possiblity is that we might have something like F alpha ~ [Int] where alpha is bound further out, which might become soluble "later" when we learn more about alpha. So we want to emit those residual constraints. BUT it's no good simply wrapping all unsolved constraints from a type signature in an implication constraint to solve later. The problem is that we are going to /use/ that signature, including instantiate it. Say we have f :: forall a. (forall b. blah) -> blah2 f x =
To typecheck the definition of f, we have to instantiate those foralls. Moreover, any unsolved kind equalities will be coercion holes in the type. If we naively wrap them in an implication like forall a. (co1:k1~k2, forall b. co2:k3~k4) hoping to solve it later, we might end up filling in the holes co1 and co2 with coercions involving 'a' and 'b' -- but by now we've instantiated the type. Chaos! Moreover, the unsolved constraints might be skolem-escpae things, and if we proceed with f bound to a nonsensical type, we get a cascade of follow-up errors. For example polykinds/T12593, T15577, and many others. So here's the plan: * solveLocalEqualitiesX: try to solve the constraints (solveLocalEqualitiesX) * buildTvImplication: build an implication for the residual, unsolved constraint * emitFlatConstraints: try to float out every unsolved equalities inside that implication, in the hope that it constrains only global type variables, not the locally-quantified ones. * If we fail, or find an insoluble constraint, emit the implication, so that the errors will be reported, and fail. * If we succeed in floating all the equalities, promote them and re-emit them as flat constraint, not wrapped at all (since they don't mention any of the quantified variables. * Note that this float-and-promote step means that anonymous wildcards get floated to top level, as we want; see Note [Checking partial type signatures] in GHC.Tc.Gen.HsType. All this is done: * in solveLocalEqualities, where there is no kind-generalisation to complicate matters. * in GHC.Tc.Gen.HsType.tcHsSigType, where quantification intervenes. See also #18062, #11506 -} solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a) solveLocalEqualitiesX callsite thing_inside = do { traceTc "solveLocalEqualitiesX {" (vcat [ text "Called from" <+> text callsite ]) ; (result, wanted) <- captureConstraints thing_inside ; traceTc "solveLocalEqualities: running solver" (ppr wanted) ; residual_wanted <- runTcSEqualities (solveWanteds wanted) ; traceTc "solveLocalEqualitiesX end }" $ text "residual_wanted =" <+> ppr residual_wanted ; return (residual_wanted, result) } -- | Type-check a thing that emits only equality constraints, then -- solve those constraints. Fails outright if there is trouble. -- Use this if you're not going to get another crack at solving -- (because, e.g., you're checking a datatype declaration) solveEqualities :: TcM a -> TcM a solveEqualities thing_inside = checkNoErrs $ -- See Note [Fail fast on kind errors] do { lvl <- TcM.getTcLevel ; traceTc "solveEqualities {" (text "level =" <+> ppr lvl) ; (result, wanted) <- captureConstraints thing_inside ; traceTc "solveEqualities: running solver" $ text "wanted = " <+> ppr wanted ; final_wc <- runTcSEqualities $ simpl_top wanted -- NB: Use simpl_top here so that we potentially default RuntimeRep -- vars to LiftedRep. This is needed to avoid #14991. ; traceTc "End solveEqualities }" empty ; reportAllUnsolved final_wc ; return result } -- | Simplify top-level constraints, but without reporting any unsolved -- constraints nor unsafe overlapping. simpl_top :: WantedConstraints -> TcS WantedConstraints -- See Note [Top-level Defaulting Plan] simpl_top wanteds = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds) -- This is where the main work happens ; dflags <- getDynFlags ; try_tyvar_defaulting dflags wc_first_go } where try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints try_tyvar_defaulting dflags wc | isEmptyWC wc = return wc | insolubleWC wc , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles] = try_class_defaulting wc | otherwise = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc) ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked -- filter isMetaTyVar: we might have runtime-skolems in GHCi, -- and we definitely don't want to try to assign to those! -- The isTyVar is needed to weed out coercion variables ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects ; if or defaulted then do { wc_residual <- nestTcS (solveWanteds wc) -- See Note [Must simplify after defaulting] ; try_class_defaulting wc_residual } else try_class_defaulting wc } -- No defaulting took place try_class_defaulting :: WantedConstraints -> TcS WantedConstraints try_class_defaulting wc | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles] = return wc | otherwise -- See Note [When to do type-class defaulting] = do { something_happened <- applyDefaultingRules wc -- See Note [Top-level Defaulting Plan] ; if something_happened then do { wc_residual <- nestTcS (solveWantedsAndDrop wc) ; try_class_defaulting wc_residual } -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence else try_callstack_defaulting wc } try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints try_callstack_defaulting wc | isEmptyWC wc = return wc | otherwise = defaultCallStacks wc -- | Default any remaining @CallStack@ constraints to empty @CallStack@s. defaultCallStacks :: WantedConstraints -> TcS WantedConstraints -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence defaultCallStacks wanteds = do simples <- handle_simples (wc_simple wanteds) mb_implics <- mapBagM handle_implic (wc_impl wanteds) return (wanteds { wc_simple = simples , wc_impl = catBagMaybes mb_implics }) where handle_simples simples = catBagMaybes <$> mapBagM defaultCallStack simples handle_implic :: Implication -> TcS (Maybe Implication) -- The Maybe is because solving the CallStack constraint -- may well allow us to discard the implication entirely handle_implic implic | isSolvedStatus (ic_status implic) = return (Just implic) | otherwise = do { wanteds <- setEvBindsTcS (ic_binds implic) $ -- defaultCallStack sets a binding, so -- we must set the correct binding group defaultCallStacks (ic_wanted implic) ; setImplicationStatus (implic { ic_wanted = wanteds }) } defaultCallStack ct | ClassPred cls tys <- classifyPredType (ctPred ct) , Just {} <- isCallStackPred cls tys = do { solveCallStack (ctEvidence ct) EvCsEmpty ; return Nothing } defaultCallStack ct = return (Just ct) {- Note [Fail fast on kind errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ solveEqualities is used to solve kind equalities when kind-checking user-written types. If solving fails we should fail outright, rather than just accumulate an error message, for two reasons: * A kind-bogus type signature may cause a cascade of knock-on errors if we let it pass * More seriously, we don't have a convenient term-level place to add deferred bindings for unsolved kind-equality constraints, so we don't build evidence bindings (by usine reportAllUnsolved). That means that we'll be left with with a type that has coercion holes in it, something like