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

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: Cale Gibbard <cgibbard@gmail.com>

1 files changed, 20 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 697cea0f47..93019ac6a2 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -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