Commit 1793ca9d authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot

Pmc: Consider Required Constraints when guessing PatSyn arg types (#19475)

This patch makes `guessConLikeUnivTyArgsFromResTy` consider required
Thetas of PatSynCons, by treating them as Wanted constraints to be
discharged with the constraints from the Nabla's TyState and saying
"does not match the match type" if the Wanted constraints are unsoluble.
It calls out into a new function `GHC.Tc.Solver.tcCheckWanteds` to do
so.

In pushing the failure logic around call sites of `initTcDsForSolver`
inside it by panicking, I realised that there was a bunch of dead code
surrounding `pmTopMoraliseType`: I was successfully able to delete the
`NoChange` data constructor of `TopNormaliseTypeResult`.

The details are in `Note [Matching against a ConLike result type]` and
`Note [Instantiating a ConLike].

The regression test is in `T19475`. It's pretty much a fork of `T14422`
at the moment.
Co-authored-by: cgibbard's avatarCale Gibbard <cgibbard@gmail.com>
parent cd793767
Pipeline #32929 failed with stages
in 232 minutes and 3 seconds
......@@ -18,7 +18,7 @@ module GHC.Core.TyCo.Subst
mkTCvSubst, mkTvSubst, mkCvSubst,
getTvSubstEnv,
getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
isInScope, notElemTCvSubst,
isInScope, elemTCvSubst, notElemTCvSubst,
setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendTCvSubstWithClone,
......@@ -293,12 +293,15 @@ getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
isInScope :: Var -> TCvSubst -> Bool
isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
notElemTCvSubst :: Var -> TCvSubst -> Bool
notElemTCvSubst v (TCvSubst _ tenv cenv)
elemTCvSubst :: Var -> TCvSubst -> Bool
elemTCvSubst v (TCvSubst _ tenv cenv)
| isTyVar v
= not (v `elemVarEnv` tenv)
= v `elemVarEnv` tenv
| otherwise
= not (v `elemVarEnv` cenv)
= v `elemVarEnv` cenv
notElemTCvSubst :: Var -> TCvSubst -> Bool
notElemTCvSubst v = not . elemTCvSubst v
setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv
......
......@@ -107,6 +107,7 @@ import GHC.Types.Error
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Error
import Data.IORef
......@@ -278,7 +279,7 @@ initDsWithModGuts hsc_env (ModGuts { mg_module = this_mod, mg_binds = binds
; runDs hsc_env envs thing_inside
}
initTcDsForSolver :: TcM a -> DsM (Messages DecoratedSDoc, Maybe a)
initTcDsForSolver :: TcM a -> DsM a
-- Spin up a TcM context so that we can run the constraint solver
-- Returns any error messages generated by the constraint solver
-- and (Just res) if no error happened; Nothing if an error happened
......@@ -303,10 +304,13 @@ initTcDsForSolver thing_inside
DsLclEnv { dsl_loc = loc } = lcl
; liftIO $ initTc hsc_env HsSrcFile False mod loc $
; (msgs, mb_ret) <- liftIO $ initTc hsc_env HsSrcFile False mod loc $
updGblEnv (\tc_gbl -> tc_gbl { tcg_fam_inst_env = fam_inst_env
, tcg_rdr_env = rdr_env }) $
thing_inside }
thing_inside
; case mb_ret of
Just ret -> pure ret
Nothing -> pprPanic "initTcDsForSolver" (vcat $ pprMsgEnvelopeBagWithLoc (getErrorMessages msgs)) }
mkDsEnvs :: UnitEnv -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
-> IORef (Messages DecoratedSDoc) -> IORef CostCentreState -> CompleteMatches
......
This diff is collapsed.
......@@ -11,7 +11,8 @@ module GHC.Tc.Solver(
pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX,
reportUnsolvedEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
tcCheckGivens,
tcCheckWanteds,
tcNormalise,
captureTopConstraints,
......@@ -805,11 +806,12 @@ simplifyDefault theta
; return (isEmptyWC unsolved) }
------------------
tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
-- Return (Just new_inerts) if satisfiable, Nothing if definitely contradictory
tcCheckSatisfiability inerts given_ids = do
tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
-- ^ Return (Just new_inerts) if the Givens are satisfiable, Nothing if definitely
-- contradictory
tcCheckGivens inerts given_ids = do
(sat, new_inerts) <- runTcSInerts inerts $ do
traceTcS "checkSatisfiability {" (ppr inerts <+> ppr given_ids)
traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids)
lcl_env <- TcS.getLclEnv
let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
let given_cts = mkGivens given_loc (bagToList given_ids)
......@@ -817,7 +819,7 @@ tcCheckSatisfiability inerts given_ids = do
solveSimpleGivens given_cts
insols <- getInertInsols
insols <- try_harder insols
traceTcS "checkSatisfiability }" (ppr insols)
traceTcS "checkGivens }" (ppr insols)
return (isEmptyBag insols)
return $ if sat then Just new_inerts else Nothing
where
......@@ -834,6 +836,18 @@ tcCheckSatisfiability inerts given_ids = do
; solveSimpleGivens new_given
; getInertInsols }
tcCheckWanteds :: InertSet -> ThetaType -> TcM Bool
-- ^ Return True if the Wanteds are soluble, False if not
tcCheckWanteds inerts wanteds = do
cts <- newWanteds PatCheckOrigin wanteds
(sat, _new_inerts) <- runTcSInerts inerts $ do
traceTcS "checkWanteds {" (ppr inerts <+> ppr wanteds)
-- See Note [Superclasses and satisfiability]
wcs <- solveWantedsAndDrop (mkSimpleWC cts)
traceTcS "checkWanteds }" (ppr wcs)
return (isSolvedWC wcs)
return sat
-- | Normalise a type as much as possible using the given constraints.
-- See @Note [tcNormalise]@.
tcNormalise :: InertSet -> Type -> TcM Type
......
T14422.hs:31:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘g’: Patterns of type ‘f a’ not matched: P
In an equation for ‘g’: Patterns of type ‘f a’ not matched: _
T14422.hs:44:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘i’: Patterns of type ‘f a’ not matched: P
In an equation for ‘i’: Patterns of type ‘f a’ not matched: _
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module T19475 where
class C f where
foo :: f a -> ()
pattern P :: C f => f a
pattern P <- (foo -> ())
{-# COMPLETE P #-}
class D f where
bar :: f a -> ()
pattern Q :: D f => f a
pattern Q <- (bar -> ())
g :: D f => f a -> ()
g Q = () -- Warning should not suggest P!
T19475.hs:19:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘g’: Patterns of type ‘f a’ not matched: _
......@@ -28,3 +28,4 @@ test('T17386', normal, compile, [''])
test('T18277', normal, compile, [''])
test('T18960', normal, compile, [''])
test('T18960b', normal, compile, [''])
test('T19475', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment