[Git][ghc/ghc][wip/T23070-dicts] Switch off the ambiguity check properly
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue May 16 11:12:46 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
b34a3d9f by Simon Peyton Jones at 2023-05-16T11:06:05+01:00
Switch off the ambiguity check properly
Needs more documentation
- - - - -
9 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Validity.hs
- testsuite/tests/gadt/T3651.hs
- testsuite/tests/pmcheck/should_compile/T15450.hs
- testsuite/tests/typecheck/should_fail/GivenForallLoop.hs
- testsuite/tests/typecheck/should_fail/T20189.hs
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1759,7 +1759,7 @@ reportEqErr ctxt item ty1 ty2
, mismatchAmbiguityInfo = eqInfos
, mismatchCoercibleInfo = mb_coercible_info }
where
- mismatch = misMatchOrCND False ctxt item ty1 ty2
+ mismatch = misMatchOrCND ctxt item ty1 ty2
eqInfos = eqInfoMsgs ty1 ty2
coercible_msg :: TcType -> TcType -> TcM (Maybe CoercibleMsg)
@@ -1907,7 +1907,7 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2
-- Consider an ambiguous top-level constraint (a ~ F a)
-- Not an occurs check, because F is a type function.
where
- headline_msg = misMatchOrCND insoluble_occurs_check ctxt item ty1 ty2
+ headline_msg = misMatchOrCND ctxt item ty1 ty2
mismatch_msg = mkMismatchMsg item ty1 ty2
add_sig = maybeToList $ suggestAddSig ctxt ty1 ty2
@@ -1936,8 +1936,6 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2
Just (NonCanonicalReason result) -> result
_ -> cteOK
- insoluble_occurs_check = check_eq_result `cterHasProblem` cteInsolubleOccurs
-
eqInfoMsgs :: TcType -> TcType -> [AmbiguityInfo]
-- Report (a) ambiguity if either side is a type function application
-- e.g. F a0 ~ Int
@@ -1971,11 +1969,11 @@ eqInfoMsgs ty1 ty2
| otherwise
= Nothing
-misMatchOrCND :: Bool -> SolverReportErrCtxt -> ErrorItem
+misMatchOrCND :: SolverReportErrCtxt -> ErrorItem
-> TcType -> TcType -> MismatchMsg
-- If oriented then ty1 is actual, ty2 is expected
-misMatchOrCND insoluble_occurs_check ctxt item ty1 ty2
- | insoluble_occurs_check -- See Note [Insoluble occurs check]
+misMatchOrCND ctxt item ty1 ty2
+ | insoluble_item -- See Note [Insoluble mis-match]
|| (isRigidTy ty1 && isRigidTy ty2)
|| (ei_flavour item == Given)
|| null givens
@@ -1987,6 +1985,10 @@ misMatchOrCND insoluble_occurs_check ctxt item ty1 ty2
= CouldNotDeduce givens (item :| []) (Just $ CND_Extra level ty1 ty2)
where
+ insoluble_item = case ei_m_reason item of
+ Nothing -> False
+ Just r -> isInsolubleReason r
+
level = ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
givens = [ given | given <- getUserGivens ctxt, ic_given_eqs given /= NoGivenEqs ]
-- Keep only UserGivens that have some equalities.
@@ -2144,8 +2146,8 @@ shouldPprWithExplicitKinds _ty1 _ty2 (TypeEqOrigin { uo_actual = act
shouldPprWithExplicitKinds ty1 ty2 _ct
= tcEqTypeVis ty1 ty2
-{- Note [Insoluble occurs check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Insoluble mis-match]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider [G] a ~ [a], [W] a ~ [a] (#13674). The Given is insoluble
so we don't use it for rewriting. The Wanted is also insoluble, and
we don't solve it from the Given. It's very confusing to say
@@ -2154,7 +2156,9 @@ we don't solve it from the Given. It's very confusing to say
And indeed even thinking about the Givens is silly; [W] a ~ [a] is
just as insoluble as Int ~ Bool.
-Conclusion: if there's an insoluble occurs check (cteInsolubleOccurs)
+Exactly the same is true if we have [G] Int ~ Bool, [W] Int ~ Bool.
+
+Conclusion: if there's an insoluble constraint (isInsolubleReason),
then report it directly, not in the "cannot deduce X from Y" form.
This is done in misMatchOrCND (via the insoluble_occurs_check arg)
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -79,10 +79,6 @@ solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
-- NC: this comes from CNonCanonical or CIrredCan
-- Precondition: already rewritten by inert set
solveDictNC ev cls tys
- | isEqualityClass cls
- = solveEqualityDict ev cls tys
-
- | otherwise
= do { simpleStage $ traceTcS "solveDictNC" (ppr (mkClassPred cls tys) $$ ppr ev)
; dict_ct <- canDictCt ev cls tys
; solveDict dict_ct }
@@ -90,6 +86,10 @@ solveDictNC ev cls tys
solveDict :: DictCt -> SolverStage Void
-- Preconditions: `tys` are already rewritten by the inert set
solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
+ | isEqualityClass cls
+ = solveEqualityDict ev cls tys
+
+ | otherwise
= assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
do { simpleStage $ traceTcS "solveDict" (ppr dict_ct)
@@ -1949,11 +1949,16 @@ mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
-- nor are repeated
-- The caller of this function is supposed to perform fuel book keeping
-- Precondition: fuel >= 0
-mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc = loc })
+mk_strict_superclasses _ _ _ _ _ cls _
+ | isEqualityClass cls
+ = return []
+
+mk_strict_superclasses fuel rec_clss
+ ev@(CtGiven { ctev_evar = evar, ctev_loc = loc })
tvs theta cls tys
- = do { traceTcS "mk_strict" (ppr ev $$ ppr (ctLocOrigin loc))
- ; concatMapM do_one_given $
- classSCSelIds cls }
+ = -- Given case
+ do { traceTcS "mk_strict" (ppr ev $$ ppr (ctLocOrigin loc))
+ ; concatMapM do_one_given (classSCSelIds cls) }
where
dict_ids = mkTemplateLocals theta
this_size = pSizeClassPred cls tys
@@ -2020,6 +2025,7 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc =
newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size)
newly_blocked _ = False
+-- Wanted case
mk_strict_superclasses fuel rec_clss ev tvs theta cls tys
| all noFreeVarsOfType tys
= return [] -- Wanteds with no variables yield no superclass constraints.
@@ -2087,7 +2093,9 @@ mk_superclasses_of fuel rec_clss ev tvs theta cls tys
loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
-- Tuples never contribute to recursion, and can be nested
rec_clss' = rec_clss `extendNameSet` cls_nm
+
mk_this_ct :: ExpansionFuel -> Ct
+ -- We can't use CNonCanonical here because we need to tradk the fuel
mk_this_ct fuel | null tvs, null theta
= CDictCan (DictCt { di_ev = ev, di_cls = cls
, di_tys = tys, di_pend_sc = fuel })
@@ -2095,8 +2103,7 @@ mk_superclasses_of fuel rec_clss ev tvs theta cls tys
-- added the superclasses, hence cc_pend_sc = fuel
| otherwise
= CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
- , qci_ev = ev
- , qci_pend_sc = fuel })
+ , qci_ev = ev, qci_pend_sc = fuel })
{- Note [Equality superclasses in quantified constraints]
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -68,7 +68,7 @@ try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
-- See Note [Multiple matching irreds]
, let ev_i = irredCtEvidence irred_i
ct_i = CIrredCan irred_i
- , not (isInsolubleReason reason && isWanted ev_i && isWanted ev_w)
+ , not (isInsolubleReason reason && (isWanted ev_i || isWanted ev_w))
-- See Note [Insoluble irreds]
= do { traceTcS "iteractIrred" $
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
@@ -106,9 +106,9 @@ once had done). This problem can be tickled by typecheck/should_compile/holes.
Note [Insoluble irreds]
~~~~~~~~~~~~~~~~~~~~~~~
-For insoluble Wanteds, don't allow a duplicate Wanted to be dropped which
-can happen with solveOneFromTheOther, so that we get distinct error messages
-with -fdefer-type-errors
+We don't allow an /insoluble/ Wanted to be dropped, even if there is an identical
+(insoluble) Given or Wanated. We want to keep all the insoluble Wanteds distinct,
+so that we get distinct error messages with -fdefer-type-errors
However we do allow an insoluble constraint to be solved from an insoluble
Given. This might seem a little odd, but it's very much a corner case, and
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -221,7 +221,7 @@ data StopOrContinue a
deriving (Functor)
instance Outputable a => Outputable (StopOrContinue a) where
- ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev
+ ppr (Stop ev s) = text "Stop" <> parens (s $$ text "ev:" <+> ppr ev)
ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
ppr (StartAgain w) = text "StartAgain" <+> ppr w
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -237,12 +237,13 @@ checkAmbiguity ctxt ty
-- can cause a cascade of further errors. Since the free
-- tyvars are skolemised, we can safely use tcSimplifyTop
; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
- ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
+ ; unless allow_ambiguous $
+ do { (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
captureConstraints $
tcSubTypeAmbiguity ctxt ty ty
-- See Note [Ambiguity check and deep subsumption]
-- in GHC.Tc.Utils.Unify
- ; simplifyAmbiguityCheck ty wanted
+ ; simplifyAmbiguityCheck ty wanted }
; traceTc "Done ambiguity check for" (ppr ty) }
=====================================
testsuite/tests/gadt/T3651.hs
=====================================
@@ -10,6 +10,19 @@ data Z a where
unsafe1 :: Z a -> Z a -> a
unsafe1 B U = ()
+{- For unsafe1 we get:
+
+ [G] a ~ () => [G] a ~ Bool => [W] Bool ~ a
+
+By the time we get to the Wanted we have:
+ inert: [G] a ~ Bool (CEqCan)
+ [G] () ~ Bool (CIrredCan)
+ work: [W] Bool ~ a
+
+We rewrite with the CEqCan to get [W] Bool ~ (), which is
+insoluble, and which we decline to solve from [G] () ~ Bool
+-}
+
unsafe2 :: a ~ b => Z b -> Z a -> a
unsafe2 B U = ()
=====================================
testsuite/tests/pmcheck/should_compile/T15450.hs
=====================================
@@ -1,5 +1,7 @@
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
+{-# LANGUAGE AllowAmbiguousTypes #-} -- To avoid rejecting the inaccessible types
+
module T15450 where
f :: (Int ~ Bool) => Bool -> a
=====================================
testsuite/tests/typecheck/should_fail/GivenForallLoop.hs
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE TypeFamilies, ImpredicativeTypes #-}
+{-# LANGUAGE AllowAmbiguousTypes #-} -- Allow insoluble signature for loopy
module GivenForallLoop where
=====================================
testsuite/tests/typecheck/should_fail/T20189.hs
=====================================
@@ -1,5 +1,6 @@
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE AllowAmbiguousTypes #-} -- Dodgy: allow the strange (illegal) signature
module T20189 where
y :: (t ~ (forall x . Show x => x -> IO ())) => t
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b34a3d9fdad8b665422a1b4bbf1ef54b64b609cf
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b34a3d9fdad8b665422a1b4bbf1ef54b64b609cf
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/20230516/bd53d981/attachment-0001.html>
More information about the ghc-commits
mailing list