[Git][ghc/ghc][wip/T25029] Add defaulting of equalities
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Sep 2 05:55:27 UTC 2024
Simon Peyton Jones pushed to branch wip/T25029 at Glasgow Haskell Compiler / GHC
Commits:
9f06a233 by Simon Peyton Jones at 2024-09-02T07:54:57+02:00
Add defaulting of equalities
This MR adds one new defaulting strategy to the top-level
defaulting story: see Note [Defaulting equalities] in GHC.Tc.Solver.
This resolves #25029 and #25125, which showed that users were
accidentally relying on a GHC bug, which was fixed by
commit 04f5bb85c8109843b9ac2af2a3e26544d05e02f4
Author: Simon Peyton Jones <simon.peytonjones at gmail.com>
Date: Wed Jun 12 17:44:59 2024 +0100
Fix untouchability test
This MR fixes #24938. The underlying problem was tha the test for
"does this implication bring in scope any equalities" was plain wrong.
This fix gave rise to a number of user complaints; but the improved
defaulting story of this MR largely resolves them.
On the way I did a bit of refactoring, of course
* Completely restructure the extremely messy top-level defaulting
code. The new code is in GHC.Tc.Solver.tryDefaulting, and is much,
much, much esaier to grok.
- - - - -
11 changed files:
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/indexed-types/should_compile/Simple14.hs
- − testsuite/tests/indexed-types/should_compile/Simple14.stderr
- testsuite/tests/indexed-types/should_compile/all.T
- + testsuite/tests/typecheck/should_compile/T25029.hs
- + testsuite/tests/typecheck/should_compile/T25125.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T21338.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -34,6 +34,7 @@ import GHC.Core.Class
import GHC.Core
import GHC.Core.DataCon
import GHC.Core.Make
+import GHC.Core.Coercion( mkNomReflCo )
import GHC.Driver.DynFlags
import GHC.Data.FastString
import GHC.Data.List.SetOps
@@ -50,7 +51,8 @@ import GHC.Tc.Types.Evidence
import GHC.Tc.Solver.Solve ( solveSimpleGivens, solveSimpleWanteds )
import GHC.Tc.Solver.Dict ( makeSuperClasses, solveCallStack )
import GHC.Tc.Solver.Rewrite ( rewriteType )
-import GHC.Tc.Utils.Unify ( buildTvImplication )
+import GHC.Tc.Utils.Unify ( buildTvImplication, touchabilityAndShapeTest
+ , simpleUnifyCheck, UnifyCheckCaller(..) )
import GHC.Tc.Utils.TcMType as TcM
import GHC.Tc.Utils.Monad as TcM
import GHC.Tc.Zonk.TcType as TcM
@@ -85,8 +87,8 @@ import Data.Foldable ( toList, traverse_ )
import Data.List ( partition, intersect )
import Data.List.NonEmpty ( NonEmpty(..), nonEmpty )
import qualified Data.List.NonEmpty as NE
-import Data.Monoid (First (First, getFirst))
-import GHC.Data.Maybe ( catMaybes, mapMaybe, runMaybeT, MaybeT )
+import GHC.Data.Maybe ( isJust, mapMaybe, catMaybes )
+import Data.Monoid ( First(..) )
{-
*********************************************************************************
@@ -495,76 +497,70 @@ report_unsolved_equalities skol_info_anon skol_tvs tclvl wanted
-- | Simplify top-level constraints, but without reporting any unsolved
-- constraints nor unsafe overlapping.
simplifyTopWanteds :: WantedConstraints -> TcS WantedConstraints
- -- See Note [Top-level Defaulting Plan]
simplifyTopWanteds wanteds
- = do { wc_first_go <- nestTcS (solveWanteds wanteds)
- -- This is where the main work happens
- ; dflags <- getDynFlags
- ; wc_defaulted <- try_tyvar_defaulting dflags wc_first_go
-
- -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors,
- -- point (C).
- ; useUnsatisfiableGivens wc_defaulted }
- 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 { -- Need to zonk first, as the WantedConstraints are not yet zonked.
- ; free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
- ; let defaultable_tvs = filter can_default free_tvs
- can_default tv
- = isTyVar tv
- -- Weed out coercion variables.
-
- && isMetaTyVar tv
- -- Weed out runtime-skolems in GHCi, which we definitely
- -- shouldn't try to default.
-
- && not (tv `elemVarSet` nonDefaultableTyVarsOfWC wc)
- -- Weed out variables for which defaulting would be unhelpful,
- -- e.g. alpha appearing in [W] alpha[conc] ~# rr[sk].
-
- ; defaulted <- mapM defaultTyVarTcS defaultable_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]
- = try_callstack_defaulting 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 (solveWanteds 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
- = defaultConstraints [defaultCallStack, defaultExceptionContext] wc
-
--- | If an implication contains a Given of the form @Unsatisfiable msg@, use
--- it to solve all Wanteds within the implication.
+ = do { -- Solve the constraints
+ wc_first_go <- nestTcS (solveWanteds wanteds)
+
+ -- Now try defaulting:
+ -- see Note [Top-level Defaulting Plan]
+ ; tryDefaulting wc_first_go }
+
+--------------------------
+tryDefaulting :: WantedConstraints -> TcS WantedConstraints
+tryDefaulting wc
+ = do { dflags <- getDynFlags
+ ; traceTcS "tryDefaulting:before" (ppr wc)
+ ; wc1 <- tryTyVarDefaulting dflags wc
+ ; wc2 <- tryConstraintDefaulting wc1
+ ; wc3 <- tryTypeClassDefaulting wc2
+ ; wc4 <- tryUnsatisfiableGivens wc3
+ ; traceTcS "tryDefaulting:after" (ppr wc)
+ ; return wc4 }
+
+solveAgainIf :: Bool -> WantedConstraints -> TcS WantedConstraints
+-- If the Bool is true, solve the wanted constraints again
+-- See Note [Must simplify after defaulting]
+solveAgainIf False wc = return wc
+solveAgainIf True wc = nestTcS (solveWanteds wc)
+
+--------------------------
+tryTyVarDefaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
+tryTyVarDefaulting dflags wc
+ | isEmptyWC wc
+ = return wc
+ | insolubleWC wc
+ , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles]
+ = return wc
+ | otherwise
+ = do { -- Need to zonk first, as the WantedConstraints are not yet zonked.
+ ; free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
+ ; let defaultable_tvs = filter can_default free_tvs
+ can_default tv
+ = isTyVar tv
+ -- Weed out coercion variables.
+
+ && isMetaTyVar tv
+ -- Weed out runtime-skolems in GHCi, which we definitely
+ -- shouldn't try to default.
+
+ && not (tv `elemVarSet` nonDefaultableTyVarsOfWC wc)
+ -- Weed out variables for which defaulting would be unhelpful,
+ -- e.g. alpha appearing in [W] alpha[conc] ~# rr[sk].
+
+ ; unification_s <- mapM defaultTyVarTcS defaultable_tvs -- Has unification side effects
+ ; solveAgainIf (or unification_s) wc }
+ -- solveAgainIf: see Note [Must simplify after defaulting]
+
+----------------------------
+-- | If an implication contains a Given of the form @Unsatisfiable msg@,
+-- use it to solve all Wanteds within the implication.
+-- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
--
-- This does a complete walk over the implication tree.
---
--- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
-useUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints
-useUnsatisfiableGivens wc =
+tryUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints
+tryUnsatisfiableGivens wc =
do { (final_wc, did_work) <- (`runStateT` False) $ go_wc wc
- ; if did_work
- then nestTcS (solveWanteds final_wc)
- else return final_wc }
+ ; solveAgainIf did_work final_wc }
where
go_wc (WC { wc_simple = wtds, wc_impl = impls, wc_errors = errs })
= do impls' <- mapMaybeBagM go_impl impls
@@ -614,7 +610,7 @@ solveImplicationUsingUnsatGiven
go_simple ct = case ctEvidence ct of
CtWanted { ctev_pred = pty, ctev_dest = dst }
-> do { ev_expr <- unsatisfiableEvExpr unsat_given pty
- ; setWantedEvTerm dst True $ EvExpr ev_expr }
+ ; setWantedEvTerm dst EvNonCanonical $ EvExpr ev_expr }
_ -> return ()
-- | Create an evidence expression for an arbitrary constraint using
@@ -696,69 +692,122 @@ This allows us to indirectly box constraints with different representations
(such as primitive equality constraints).
-}
--- | A 'TcS' action which can may default a 'Ct'.
-type CtDefaultingStrategy = Ct -> MaybeT TcS ()
+-- | A 'TcS' action which can may solve a `Ct`
+type CtDefaultingStrategy = Ct -> TcS Bool
+ -- True <=> I solved the constraint
+
+--------------------------------
+tryConstraintDefaulting :: WantedConstraints -> TcS WantedConstraints
+-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
+tryConstraintDefaulting wc
+ | isEmptyWC wc
+ = return wc
+ | otherwise
+ = do { (n_unifs, better_wc) <- reportUnifications (go_wc wc)
+ -- We may have done unifications; so solve again
+ ; solveAgainIf (n_unifs > 0) better_wc }
+ where
+ go_wc :: WantedConstraints -> TcS WantedConstraints
+ go_wc wc@(WC { wc_simple = simples, wc_impl = implics })
+ = do { mb_simples <- mapMaybeBagM go_simple simples
+ ; mb_implics <- mapMaybeBagM go_implic implics
+ ; return (wc { wc_simple = mb_simples, wc_impl = mb_implics }) }
+
+ go_simple :: Ct -> TcS (Maybe Ct)
+ go_simple ct = do { solved <- tryCtDefaultingStrategy ct
+ ; if solved then return Nothing
+ else return (Just ct) }
+
+ go_implic :: Implication -> TcS (Maybe Implication)
+ -- The Maybe is because solving the CallStack constraint
+ -- may well allow us to discard the implication entirely
+ go_implic implic
+ | isSolvedStatus (ic_status implic)
+ = return (Just implic) -- Nothing to solve inside here
+ | otherwise
+ = do { wanteds <- setEvBindsTcS (ic_binds implic) $
+ -- defaultCallStack sets a binding, so
+ -- we must set the correct binding group
+ go_wc (ic_wanted implic)
+ ; setImplicationStatus (implic { ic_wanted = wanteds }) }
+
+tryCtDefaultingStrategy :: CtDefaultingStrategy
+-- The composition of all the CtDefaultingStrategies we want
+tryCtDefaultingStrategy
+ = foldr1 combineStrategies
+ [ defaultCallStack
+ , defaultExceptionContext
+ , defaultEquality ]
-- | Default @ExceptionContext@ constraints to @emptyExceptionContext at .
defaultExceptionContext :: CtDefaultingStrategy
defaultExceptionContext ct
- = do { ClassPred cls tys <- pure $ classifyPredType (ctPred ct)
- ; Just {} <- pure $ isExceptionContextPred cls tys
- ; emptyEC <- Var <$> lift (lookupId emptyExceptionContextName)
+ | ClassPred cls tys <- classifyPredType (ctPred ct)
+ , isJust (isExceptionContextPred cls tys)
+ = do { warnTcS $ TcRnDefaultedExceptionContext (ctLoc ct)
+ ; empty_ec_id <- lookupId emptyExceptionContextName
; let ev = ctEvidence ct
- ; let ev_tm = mkEvCast emptyEC (wrapIP (ctEvPred ev))
- ; lift $ warnTcS $ TcRnDefaultedExceptionContext (ctLoc ct)
- ; lift $ setEvBindIfWanted ev False ev_tm
- }
+ ev_tm = mkEvCast (Var empty_ec_id) (wrapIP (ctEvPred ev))
+ ; setEvBindIfWanted ev EvCanonical ev_tm
+ -- EvCanonical: see Note [CallStack and ExecptionContext hack]
+ -- in GHC.Tc.Solver.Dict
+ ; return True }
+ | otherwise
+ = return False
-- | Default any remaining @CallStack@ constraints to empty @CallStack at s.
-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
defaultCallStack :: CtDefaultingStrategy
defaultCallStack ct
- = do { ClassPred cls tys <- pure $ classifyPredType (ctPred ct)
- ; Just {} <- pure $ isCallStackPred cls tys
- ; lift $ solveCallStack (ctEvidence ct) EvCsEmpty
- }
-
-defaultConstraints :: [CtDefaultingStrategy]
- -> WantedConstraints
- -> TcS WantedConstraints
--- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
-defaultConstraints defaulting_strategies wanteds
- | isEmptyWC wanteds = return wanteds
+ | ClassPred cls tys <- classifyPredType (ctPred ct)
+ , isJust (isCallStackPred cls tys)
+ = do { solveCallStack (ctEvidence ct) EvCsEmpty
+ ; return True }
| otherwise
- = 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 })
+ = return False
+defaultEquality :: CtDefaultingStrategy
+-- See Note [Defaulting equalities]
+defaultEquality ct
+ | EqPred NomEq ty1 ty2 <- classifyPredType (ctPred ct)
+ , Just tv1 <- getTyVar_maybe ty1
+ = do { -- Remember: `ct` may not be zonked;
+ -- see (DE3) in Note [Defaulting equalities]
+ z_ty1 <- TcS.zonkTcTyVar tv1
+ ; z_ty2 <- TcS.zonkTcType ty2
+ ; case getTyVar_maybe z_ty1 of
+ Just z_tv1 | defaultable z_tv1 z_ty2
+ -> do { default_tv z_tv1 z_ty2
+ ; return True }
+ _ -> return False }
+ | otherwise
+ = return False
where
- handle_simples :: Bag Ct -> TcS (Bag Ct)
- handle_simples simples
- = catBagMaybes <$> mapBagM handle_simple simples
- where
- handle_simple :: Ct -> TcS (Maybe Ct)
- handle_simple ct = go defaulting_strategies
- where
- go [] = return (Just ct)
- go (f:fs) = do
- mb <- runMaybeT (f ct)
- case mb of
- Just () -> return Nothing
- Nothing -> go fs
-
- 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
- defaultConstraints defaulting_strategies (ic_wanted implic)
- ; setImplicationStatus (implic { ic_wanted = wanteds }) }
+ defaultable tv1 ty2
+ = -- Do the standard unification checks;
+ -- c.f. uUnfilledVar2 in GHC.Tc.Utils.Unify
+ -- EXCEPT drop the untouchability test
+ tyVarKind tv1 `tcEqType` typeKind ty2
+ && touchabilityAndShapeTest topTcLevel tv1 ty2
+ -- topTcLevel makes the untoucability test vacuous,
+ -- which is the Whole Point of `defaultEquality`
+ -- See (DE2) in Note [Defaulting equalities]
+ && simpleUnifyCheck UC_Defaulting tv1 ty2
+
+ default_tv tv1 ty2
+ = do { unifyTyVar tv1 ty2 -- NB: unifyTyVar adds to the
+ -- TcS unification counter
+ ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
+ evCoercion (mkNomReflCo ty2) }
+
+combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
+combineStrategies default1 default2 ct
+ = do { solved <- default1 ct
+ ; case solved of
+ True -> return True -- default1 solved it!
+ False -> default2 ct -- default1 failed, try default2
+ }
+
{- Note [When to do type-class defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -787,6 +836,56 @@ Another potential alternative would be to suppress *all* non-insoluble
errors if there are *any* insoluble errors, anywhere, but that seems
too drastic.
+Note [Defaulting equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f :: forall a. (forall t. (F t ~ Int) => a -> Int) -> Int
+
+ g :: Int
+ g = f id
+
+We'll typecheck
+ id :: forall t. (F t ~ Int) => alpha[1] -> Int
+where the `alpha[1]` comes from instantiating `f`. So we'll end up
+with the implication constraint
+ forall[2] t. (F t ~ Int) => alpha[1] ~ Int
+And that can't be solved because `alpha` is untouchable under the
+equality (F t ~ Int).
+
+This is tiresome, and gave rise to user complaints: #25125 and #25029.
+Moreover, in this case there is no good reason not to unify alpha:=Int.
+Doing so solves the constraint, and since `alpha` is not otherwise
+constrained, it does no harm. So the new plan is this:
+
+ * For the Wanted constraint
+ [W] alpha ~ ty
+ if the only reason for not unifying is untouchability, then during
+ top-level defaulting, go ahead and unify
+
+In top-level defaulting, we already do several other somewhat-ad-hoc,
+but terribly convenient, unifications. This is just one more.
+
+Wrinkles:
+
+(DE1) Note carefully that this does not threaten principal types.
+ The original worry about unifying untouchable type variables was this:
+
+ data T a where
+ T1 :: T Bool
+ f x = case x of T1 -> True
+
+ Should we infer f :: T a -> Bool, or f :: T a -> a. Both are valid, but
+ neither is more general than the other
+
+(DE2) We still can't unify if there is a skolem-escape check, or an occurs check,
+ or it it'd mean unifying a TyVarTv with a non-tyvar. It's only the
+ "untouchability test" that we lift. We can lift it by saying that the innermost
+ given equality is at top level.
+
+(DE3) The contraint we are looking at may not be fully zonked; for example,
+ an earlier deafaulting might have affected it. So we zonk-on-the fly in
+ `defaultEquality`.
+
Note [Don't default in syntactic equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When there are unsolved syntactic equalities such as
@@ -1027,11 +1126,12 @@ last example above.
------------------
simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
-simplifyAmbiguityCheck ty wanteds
+simplifyAmbiguityCheck ty wc
= do { traceTc "simplifyAmbiguityCheck {" $
- text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds
+ text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wc
- ; (final_wc, _) <- runTcS $ useUnsatisfiableGivens =<< solveWanteds wanteds
+ ; (final_wc, _) <- runTcS $ do { wc1 <- solveWanteds wc
+ ; tryUnsatisfiableGivens wc1 }
-- NB: no defaulting! See Note [No defaulting in the ambiguity check]
-- Note: we do still use Unsatisfiable Givens to solve Wanteds,
-- see Wrinkle [Ambiguity] under point (C) of
@@ -2881,11 +2981,11 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
-- setting the ic_status field
-- Precondition: the ic_status field is not already IC_Solved
-- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_status = status
+setImplicationStatus implic@(Implic { ic_status = old_status
, ic_info = info
, ic_wanted = wc
, ic_given = givens })
- | assertPpr (not (isSolvedStatus status)) (ppr info) $
+ | assertPpr (not (isSolvedStatus old_status)) (ppr info) $
-- Precondition: we only set the status if it is not already solved
not (isSolvedWC pruned_wc)
= do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
@@ -3389,28 +3489,34 @@ The constraint in f's signature is redundant; not used to typecheck
be an ambiguous variable in `g`.
-}
+type UnificationDone = Bool
+
+noUnification, didUnification :: UnificationDone
+noUnification = False
+didUnification = True
+
-- | Like 'defaultTyVar', but in the TcS monad.
-defaultTyVarTcS :: TcTyVar -> TcS Bool
+defaultTyVarTcS :: TcTyVar -> TcS UnificationDone
defaultTyVarTcS the_tv
| isTyVarTyVar the_tv
-- TyVarTvs should only be unified with a tyvar
-- never with a type; c.f. GHC.Tc.Utils.TcMType.defaultTyVar
-- and Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
- = return False
+ = return noUnification
| isRuntimeRepVar the_tv
= do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
; unifyTyVar the_tv liftedRepTy
- ; return True }
+ ; return didUnification }
| isLevityVar the_tv
= do { traceTcS "defaultTyVarTcS Levity" (ppr the_tv)
; unifyTyVar the_tv liftedDataConTy
- ; return True }
+ ; return didUnification }
| isMultiplicityVar the_tv
= do { traceTcS "defaultTyVarTcS Multiplicity" (ppr the_tv)
; unifyTyVar the_tv ManyTy
- ; return True }
+ ; return didUnification }
| otherwise
- = return False -- the common case
+ = return noUnification -- the common case
approximateWC :: Bool -- See Wrinkle (W3) in Note [ApproximateWC]
-> WantedConstraints
@@ -3681,6 +3787,15 @@ Wrinkle (DP2): Interactions between defaulting mechanisms
-}
+tryTypeClassDefaulting :: WantedConstraints -> TcS WantedConstraints
+tryTypeClassDefaulting 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]
+ ; solveAgainIf something_happened wc }
+
applyDefaultingRules :: WantedConstraints -> TcS Bool
-- True <=> I did some defaulting, by unifying a meta-tyvar
-- Input WantedConstraints are not necessarily zonked
@@ -3720,8 +3835,10 @@ applyDefaultingRules wanteds
; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
; return $ or something_happeneds || or plugin_defaulted }
- where run_defaulting_plugin wanteds p =
- do { groups <- runTcPluginTcS (p wanteds)
+
+ where
+ run_defaulting_plugin wanteds p
+ = do { groups <- runTcPluginTcS (p wanteds)
; defaultedGroups <-
filterM (\g -> disambigMultiGroup
wanteds
@@ -3737,9 +3854,7 @@ applyDefaultingRules wanteds
-- Note [Defaulting plugins]). So we re-zonk to make sure later
-- defaulting doesn't try to solve the same metavars.
wanteds' <- TcS.zonkWC wanteds
- return (wanteds', True)
- }
-
+ return (wanteds', True) }
findDefaultableGroups
:: ( [ClassDefaults]
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -194,7 +194,7 @@ solveCallStack ev ev_cs
{- Note [CallStack and ExecptionContext hack]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It isn't really right thta we treat CallStack and ExceptionContext dictionaries
+It isn't really right that we treat CallStack and ExceptionContext dictionaries
as canonical, in the sense of Note [Coherence and specialisation: overview].
They definitely are not!
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -819,7 +819,8 @@ data TcSEnv
tcs_unified :: IORef Int,
-- The number of unification variables we have filled
- -- The important thing is whether it is non-zero
+ -- The important thing is whether it is non-zero, so it
+ -- could equally well be a Bool instead of an Int.
tcs_unif_lvl :: IORef (Maybe TcLevel),
-- The Unification Level Flag
@@ -1312,6 +1313,9 @@ unifyTyVar tv ty
; TcM.updTcRef (tcs_unified env) (+1) }
reportUnifications :: TcS a -> TcS (Int, a)
+-- Record how many unifications are done by thing_inside
+-- We could return a Bool instead of an Int;
+-- all that matters is whether it is no-zero
reportUnifications (TcS thing_inside)
= TcS $ \ env ->
do { inner_unified <- TcM.newTcRef 0
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2906,18 +2906,20 @@ data UnifyCheckCaller
= UC_OnTheFly -- Called from the on-the-fly unifier
| UC_QuickLook -- Called from Quick Look
| UC_Solver -- Called from constraint solver
+ | UC_Defaulting -- Called when doing top-level defaulting
simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
-- simpleUnifyCheck does a fast check: True <=> unification is OK
-- If it says 'False' then unification might still be OK, but
-- it'll take more work to do -- use the full checkTypeEq
--
+-- * Rejects if lhs_tv occurs in rhs_ty (occurs check)
-- * Rejects foralls unless
-- lhs_tv is RuntimeUnk (used by GHCi debugger)
-- or is a QL instantiation variable
-- * Rejects a non-concrete type if lhs_tv is concrete
-- * Rejects type families unless fam_ok=True
--- * Does a level-check for type variables
+-- * Does a level-check for type variables, to avoid skolem escape
--
-- This function is pretty heavily used, so it's optimised not to allocate
simpleUnifyCheck caller lhs_tv rhs
@@ -2939,9 +2941,10 @@ simpleUnifyCheck caller lhs_tv rhs
-- families, so we let it through there (not very principled, but let's
-- see if it bites us)
fam_ok = case caller of
- UC_Solver -> True
- UC_QuickLook -> True
- UC_OnTheFly -> False
+ UC_Solver -> True
+ UC_QuickLook -> True
+ UC_OnTheFly -> False
+ UC_Defaulting -> True
go (TyVarTy tv)
| lhs_tv == tv = False
=====================================
testsuite/tests/indexed-types/should_compile/Simple14.hs
=====================================
@@ -1,6 +1,6 @@
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeOperators, AllowAmbiguousTypes #-}
module Simple14 where
@@ -19,12 +19,11 @@ ntI :: (forall p. EQ_ x y -> p) -> EQ_ x y
ntI x = error "ntI"
foo :: forall m n. EQ_ (Maybe m) (Maybe n)
-foo = ntI (\x -> x `eqE` (eqI :: EQ_ m n))
-
--- Alternative
--- foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
+foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
+-- Aug 2024: this test started passing with the fix to #25029
+-- See Note [Defaulting equalities] in GHC.Tc.Solver
-- eq :: EQ_ (Maybe m) (Maybe n)
-- Need (Maybe m ~ Maybe n) => EQ_ m n ~ EQ_ zeta zeta
--- which reduces to (m~n) => m ~ zeta
--- but then we are stuck
+-- which reduces to (m~n) => m ~ zeta, but then
+-- we were stuck; now we default zeta:=m in tryDefaulting
=====================================
testsuite/tests/indexed-types/should_compile/Simple14.stderr deleted
=====================================
@@ -1,21 +0,0 @@
-
-Simple14.hs:22:27: error: [GHC-83865]
- • Couldn't match type ‘z0’ with ‘n’
- Expected: EQ_ z0 z0
- Actual: EQ_ m n
- ‘z0’ is untouchable
- inside the constraints: Maybe m ~ Maybe n
- bound by a type expected by the context:
- (Maybe m ~ Maybe n) => EQ_ z0 z0
- at Simple14.hs:22:26-41
- ‘n’ is a rigid type variable bound by
- the type signature for:
- foo :: forall m n. EQ_ (Maybe m) (Maybe n)
- at Simple14.hs:21:1-42
- • In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
- In the expression: x `eqE` (eqI :: EQ_ m n)
- In the first argument of ‘ntI’, namely
- ‘(\ x -> x `eqE` (eqI :: EQ_ m n))’
- • Relevant bindings include
- x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:13)
- foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:1)
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -11,7 +11,7 @@ test('Simple10', normal, compile, [''])
test('Simple11', normal, compile, [''])
test('Simple12', normal, compile, [''])
test('Simple13', normal, compile, [''])
-test('Simple14', normal, compile_fail, [''])
+test('Simple14', normal, compile, [''])
test('Simple15', normal, compile, [''])
test('Simple16', normal, compile, [''])
test('Simple17', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_compile/T25029.hs
=====================================
@@ -0,0 +1,28 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T25029 where
+
+import Data.Kind (Type)
+import GHC.TypeLits (Nat)
+
+type family RankedOf2 (f :: Type -> Type) :: Type -> Type
+type family PrimalOf2 (f :: Type -> Type) :: Type -> Type
+
+rrev :: forall r r1 u. (Floating r, Floating r1)
+ => (forall f. ( RankedOf2 (PrimalOf2 f) ~ PrimalOf2 f
+ , (forall r2. Floating r2 => Floating (f r2))
+-- , f r1 ~ f u
+ )
+ => f r -> f r1)
+ -> ()
+rrev f = ()
+
+-- fails
+testSin0RrevPP1 :: ()
+testSin0RrevPP1 = rrev @Double sin
+
+-- works
+testSin0RrevPP2 :: ()
+testSin0RrevPP2 = rrev @Double @Double sin
=====================================
testsuite/tests/typecheck/should_compile/T25125.hs
=====================================
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+module T25125 where
+
+import GHC.TypeNats
+
+newtype NonEmptyText (n :: Nat) = NonEmptyText String
+
+toT :: NonEmptyText 10 -> String
+toT = undefined
+
+fromT :: forall n. String -> NonEmptyText n
+fromT t = undefined
+
+baz = ()
+ where
+ validate :: forall n. (1 <= n) => NonEmptyText 10 -> (NonEmptyText n)
+ validate n = fromT (toT (check n))
+
+
+ -- Giving a type signature works
+ --check :: forall n. (1 <= n) => NonEmptyText n -> AppM (NonEmptyText n)
+ check = check2
+ -- Eta expanding check works
+ --check x = check2 x
+
+ check2 :: forall n. (1 <= n) => NonEmptyText n -> (NonEmptyText n)
+ check2 inputText = undefined
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -920,3 +920,5 @@ test('T24810', normal, compile, [''])
test('T24887', normal, compile, [''])
test('T24938a', normal, compile, [''])
test('T25094', normal, compile, [''])
+test('T25029', normal, compile, [''])
+test('T25125', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T21338.stderr
=====================================
@@ -1,27 +1,4 @@
-T21338.hs:38:24: error: [GHC-83865]
- • Couldn't match type ‘flds0’ with ‘flds’
- Expected: NP (K String) flds
- Actual: NP (K String) flds0
- ‘flds0’ is untouchable
- inside the constraints: All flds0
- bound by a pattern with constructor:
- Record :: forall (xs :: [*]).
- All xs =>
- NP (K String) xs -> ConstructorInfo xs,
- in a case alternative
- at T21338.hs:38:3-11
- ‘flds’ is a rigid type variable bound by
- the type signature for:
- fieldNames :: forall a (flds :: [*]). NP (K String) flds
- at T21338.hs:36:1-57
- • In the second argument of ‘hmap’, namely ‘np’
- In the expression: hmap id np
- In a case alternative: Record np -> hmap id np
- • Relevant bindings include
- np :: NP (K String) flds0 (bound at T21338.hs:38:10)
- fieldNames :: NP (K String) flds (bound at T21338.hs:37:1)
-
T21338.hs:39:8: error: [GHC-95781]
• Cannot apply expression of type ‘h0 f0 xs0 -> h0 g0 xs0’
to a visible type argument ‘flds’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f06a23376822bcad98555800734d139fd2de226
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f06a23376822bcad98555800734d139fd2de226
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240902/655ebee2/attachment-0001.html>
More information about the ghc-commits
mailing list