[Git][ghc/ghc][wip/T23070-pipeline-monad] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon May 8 22:42:11 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-pipeline-monad at Glasgow Haskell Compiler / GHC
Commits:
7ed9bfea by Simon Peyton Jones at 2023-05-08T23:42:00+01:00
Wibbles
- - - - -
5 changed files:
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- testsuite/tests/typecheck/should_run/Typeable1.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -114,12 +114,16 @@ solveEquality ev eq_rel ty1 ty2
; case mb_canon of {
- Left irred_ct -> do { tryInertIrreds irred_ct
+ -- An IrredCt equality may be insoluble; but maybe not!
+ -- E.g. m a ~R# m b is not canonical, but may be
+ -- solved by a quantified constraint (T15290)
+ Left irred_ct -> do { tryInertIrreds irred_ct
+ ; tryQCsIrredEqCt irred_ct
; return (CIrredCan irred_ct) } ;
- Right eq_ct -> do { interactEq eq_ct
- ; tryFunDeps eq_ct
- ; tryQCsEqCt eq_ct
+ Right eq_ct -> do { tryInertEqs eq_ct
+ ; tryFunDeps eq_ct
+ ; tryQCsEqCt eq_ct
; return (CEqCan eq_ct) } } }
@@ -2477,7 +2481,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio
{-
**********************************************************************
* *
- interactEq
+ tryInertEqs
* *
**********************************************************************
@@ -2517,8 +2521,8 @@ But it's not so simple:
call to strictly_more_visible.
-}
-interactEq :: EqCt -> SolverStage ()
-interactEq work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
+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
@@ -2670,23 +2674,16 @@ See
-}
--------------------
-{-
-tryQCsIrredCt :: IrredCt -> SolverStage ()
-tryQCsIrredCt irred@(IrredCt { ir_ev = ev })
+tryQCsIrredEqCt :: IrredCt -> SolverStage ()
+tryQCsIrredEqCt irred@(IrredCt { ir_ev = ev })
| EqPred eq_rel t1 t2 <- classifyPredType (ctEvPred ev)
= lookup_eq_in_qcis (CIrredCan irred) eq_rel t1 t2
- -- If the final_qci_check fails, we'll do continueWith on an IrredCt
- -- That in turn will go down the Irred pipeline, so which deals with
- -- the case where we have [G] Coercible (m a) (m b), and [W] m a ~R# m b
- -- When we de-pipeline Irreds we may have to adjust here
-
- | otherwise -- All the calls come from in this module, where we deal
- -- only with equalities, so ctEvPred ev) must be an equality.
- -- Indeed, we could pass eq_rel, t1, t2 as arguments, to avoid
- -- this can't happen case, but it's not a hot path, and this is
- -- simple and robust
+
+ | otherwise -- All the calls come from in this module, where we deal only with
+ -- equalities, so ctEvPred ev) must be an equality. Indeed, we could
+ -- pass eq_rel, t1, t2 as arguments, to avoid this can't-happen case,
+ -- but it's not a hot path, and this is simple and robust
= pprPanic "solveIrredEquality" (ppr ev)
--}
--------------------
tryQCsEqCt :: EqCt -> SolverStage ()
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -3,7 +3,7 @@
{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Solver.Irred(
- solveIrred, tryInertIrreds
+ solveIrred, tryInertIrreds, tryQCsIrredCt
) where
import GHC.Prelude
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -730,8 +730,9 @@ getHasGivenEqs tclvl
; return (has_ge, given_insols) }
where
insoluble_given_equality :: IrredCt -> Bool
- insoluble_given_equality irred
- = insolubleIrredCt irred && isGiven (irredCtEvidence irred)
+ -- Check for unreachability; specifically do not include UserError/Unsatisfiable
+ insoluble_given_equality (IrredCt { ir_ev = ev, ir_reason = reason })
+ = isInsolubleReason reason && isGiven ev
removeInertCts :: [Ct] -> InertCans -> InertCans
-- ^ Remove inert constraints from the 'InertCans', for use when a
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -443,31 +443,32 @@ instance Outputable NotConcreteError where
-- | Used to indicate extra information about why a CIrredCan is irreducible
data CtIrredReason
= IrredShapeReason
- -- ^ this constraint has a non-canonical shape (e.g. @c Int@, for a variable @c@)
+ -- ^ This constraint has a non-canonical shape (e.g. @c Int@, for a variable @c@)
+ -- Also used for (U
| NonCanonicalReason CheckTyEqResult
- -- ^ an equality where some invariant other than (TyEq:H) of 'CEqCan' is not satisfied;
+ -- ^ An equality where some invariant other than (TyEq:H) of 'CEqCan' is not satisfied;
-- the 'CheckTyEqResult' states exactly why
| ReprEqReason
- -- ^ an equality that cannot be decomposed because it is representational.
+ -- ^ An equality that cannot be decomposed because it is representational.
-- Example: @a b ~R# Int at .
-- These might still be solved later.
-- INVARIANT: The constraint is a representational equality constraint
| ShapeMismatchReason
- -- ^ a nominal equality that relates two wholly different types,
+ -- ^ A nominal equality that relates two wholly different types,
-- like @Int ~# Bool@ or @a b ~# 3 at .
-- INVARIANT: The constraint is a nominal equality constraint
| AbstractTyConReason
- -- ^ an equality like @T a b c ~ Q d e@ where either @T@ or @Q@
+ -- ^ An equality like @T a b c ~ Q d e@ where either @T@ or @Q@
-- is an abstract type constructor. See Note [Skolem abstract data]
-- in GHC.Core.TyCon.
-- INVARIANT: The constraint is an equality constraint between two TyConApps
| PluginReason
- -- ^ a typechecker plugin returned this in the pluginBagCts field
+ -- ^ A typechecker plugin returned this in the pluginBadCts field
-- of TcPluginProgress
instance Outputable CtIrredReason where
@@ -1306,14 +1307,15 @@ insolubleWantedCt ct = insolubleCt ct &&
not (arisesFromGivens ct) &&
not (isWantedWantedFunDepOrigin (ctOrigin ct))
-insolubleIrredCt :: IrredCt -> Bool
--- Returns True of Irred constraints that are /definitely/ insoluble
-insolubleIrredCt (IrredCt { ir_reason = reason })
+insolubleEqIrredCt :: IrredCt -> Bool
+-- True of Irred constraints that are
+-- a) definitely insoluble
+-- b) not (TypeError msg)
+insolubleEqIrredCt (IrredCt { ir_reason = reason })
= isInsolubleReason reason
--- | Returns True of constraints that are definitely insoluble,
--- as well as TypeError constraints.
--- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
+insolubleIrredCt :: IrredCt -> Bool
+-- Returns True of Irred constraints that are /definitely/ insoluble
--
-- This function is critical for accurate pattern-match overlap warnings.
-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver
@@ -1321,16 +1323,9 @@ insolubleIrredCt (IrredCt { ir_reason = reason })
-- Note that this does not traverse through the constraint to find
-- nested custom type errors: it only detects @TypeError msg :: Constraint@,
-- and not e.g. @Eq (TypeError msg)@.
---
--- The function is tuned for application /after/ constraint solving
--- i.e. assuming canonicalisation has been done
--- That's why it looks only for IrredCt, with an insoluble IrredCtReason
-insolubleCt :: Ct -> Bool
-insolubleCt ct
- | isTopLevelUserTypeError (ctPred ct) = True
- | CIrredCan ir_ct <- ct = insolubleIrredCt ir_ct
- | otherwise = False
- where
+insolubleIrredCt (IrredCt { ir_ev = ev, ir_reason = reason })
+ = isInsolubleReason reason
+ || isTopLevelUserTypeError (ctEvPred ev)
-- NB: 'isTopLevelUserTypeError' detects constraints of the form "TypeError msg"
-- and "Unsatisfiable msg". It deliberately does not detect TypeError
-- nested in a type (e.g. it does not use "containsUserTypeError"), as that
@@ -1347,6 +1342,18 @@ insolubleCt ct
-- > Assert 'True _errMsg = ()
-- > Assert _check errMsg = errMsg
+-- | Returns True of constraints that are definitely insoluble,
+-- as well as TypeError constraints.
+-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
+--
+-- The function is tuned for application /after/ constraint solving
+-- i.e. assuming canonicalisation has been done
+-- That's why it looks only for IrredCt; all insoluble constraints
+-- are put into CIrredCan
+insolubleCt :: Ct -> Bool
+insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
+insolubleCt _ = False
+
-- | Does this hole represent an "out of scope" error?
-- See Note [Insoluble holes]
isOutOfScopeHole :: Hole -> Bool
=====================================
testsuite/tests/typecheck/should_run/Typeable1.stderr
=====================================
@@ -9,8 +9,8 @@ Typeable1.hs:22:5: error: [GHC-40564] [-Winaccessible-code (in -Wdefault), Werro
TypeRep a -> TypeRep b -> TypeRep t,
in a pattern binding in
a 'do' block
- Couldn't match type: ComposeK
- with: a3 b3
+ Couldn't match type: a3 b3
+ with: ComposeK
• In the pattern: App x y
In a stmt of a 'do' block: App x y <- pure x
In the expression:
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7ed9bfea3bc3f7174451b803eb0842617c522b19
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7ed9bfea3bc3f7174451b803eb0842617c522b19
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/20230508/3a0756f6/attachment-0001.html>
More information about the ghc-commits
mailing list