[Git][ghc/ghc][wip/T18645] Make `tcCheckSatisfiability` incremental (#18645)
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Sep 7 14:46:08 UTC 2020
Sebastian Graf pushed to branch wip/T18645 at Glasgow Haskell Compiler / GHC
Commits:
9d682f7d by Sebastian Graf at 2020-09-07T16:45:59+02:00
Make `tcCheckSatisfiability` incremental (#18645)
By taking and returning an `InertSet`.
Every new `TcS` session can then pick up where a prior session left with
`setTcSInerts`.
Since we don't want to unflatten the Givens (and because it leads to
infinite loops, see !3971), we introduced a new variant of `runTcS`,
`runTcSInerts`, that takes and returns the `InertSet` and makes
sure not to unflatten the Givens after running the `TcS` action.
Fixes #18645 and #17836.
Metric Decrease:
T17977b
- - - - -
8 changed files:
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Monad.hs
- + testsuite/tests/pmcheck/should_compile/T17836.hs
- + testsuite/tests/pmcheck/should_compile/T17836b.hs
- + testsuite/tests/pmcheck/should_compile/T17836b.stderr
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -523,13 +523,11 @@ nameTyCt pred_ty = do
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
- ; let new_inert = inert `unionBags` evs
; tracePm "tyOracle" (ppr cts)
- ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability new_inert
+ ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability inert evs
; case res of
- Just True -> return (Just (TySt new_inert))
- Just False -> return Nothing
- Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
+ Just mb_new_inert -> return (TySt <$> mb_new_inert)
+ Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
-- | A 'SatisfiabilityCheck' based on new type-level constraints.
-- Returns a new 'Nabla' if the new constraints are compatible with existing
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs
=====================================
@@ -47,7 +47,6 @@ import GHC.Prelude
import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Data.FastString
-import GHC.Types.Var (EvVar)
import GHC.Types.Id
import GHC.Types.Var.Env
import GHC.Types.Unique.DSet
@@ -68,7 +67,7 @@ import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
-import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Tc.Solver.Monad (InertSet, emptyInert)
import GHC.Driver.Types (ConLikeSet)
import Numeric (fromRat)
@@ -596,15 +595,14 @@ initTmState = TmSt emptySDIE emptyCoreMap
-- | The type oracle state. A poor man's 'GHC.Tc.Solver.Monad.InsertSet': The invariant is
-- that all constraints in there are mutually compatible.
-newtype TyState = TySt (Bag EvVar)
+newtype TyState = TySt InertSet
-- | Not user-facing.
instance Outputable TyState where
- ppr (TySt evs)
- = braces $ hcat $ punctuate comma $ map (ppr . evVarPred) $ bagToList evs
+ ppr (TySt inert) = ppr inert
initTyState :: TyState
-initTyState = TySt emptyBag
+initTyState = TySt emptyInert
-- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
-- canonical (i.e. mutually compatible) term and type constraints that form the
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -718,22 +718,22 @@ simplifyDefault theta
; return () }
------------------
-tcCheckSatisfiability :: Bag EvVar -> TcM Bool
--- Return True if satisfiable, False if definitely contradictory
-tcCheckSatisfiability given_ids
- = do { lcl_env <- TcM.getLclEnv
- ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
- ; (res, _ev_binds) <- runTcS $
- do { traceTcS "checkSatisfiability {" (ppr given_ids)
- ; let given_cts = mkGivens given_loc (bagToList given_ids)
- -- See Note [Superclasses and satisfiability]
- ; solveSimpleGivens given_cts
- ; insols <- getInertInsols
- ; insols <- try_harder insols
- ; traceTcS "checkSatisfiability }" (ppr insols)
- ; return (isEmptyBag insols) }
- ; return res }
- where
+tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
+-- Return (Just new_inerts) if satisfiable, Nothing if definitely contradictory
+tcCheckSatisfiability inerts given_ids = do
+ (sat, new_inerts) <- runTcSInerts inerts $ do
+ traceTcS "checkSatisfiability {" (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)
+ -- See Note [Superclasses and satisfiability]
+ solveSimpleGivens given_cts
+ insols <- getInertInsols
+ insols <- try_harder insols
+ traceTcS "checkSatisfiability }" (ppr insols)
+ return (isEmptyBag insols)
+ return $ if sat then Just new_inerts else Nothing
+ where
try_harder :: Cts -> TcS Cts
-- Maybe we have to search up the superclass chain to find
-- an unsatisfiable constraint. Example: pmcheck/T3927b.
@@ -749,15 +749,11 @@ tcCheckSatisfiability given_ids
-- | Normalise a type as much as possible using the given constraints.
-- See @Note [tcNormalise]@.
-tcNormalise :: Bag EvVar -> Type -> TcM Type
-tcNormalise given_ids ty
- = do { lcl_env <- TcM.getLclEnv
- ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
- ; norm_loc <- getCtLocM PatCheckOrigin Nothing
- ; (res, _ev_binds) <- runTcS $
- do { traceTcS "tcNormalise {" (ppr given_ids)
- ; let given_cts = mkGivens given_loc (bagToList given_ids)
- ; solveSimpleGivens given_cts
+tcNormalise :: InertSet -> Type -> TcM Type
+tcNormalise inerts ty
+ = do { norm_loc <- getCtLocM PatCheckOrigin Nothing
+ ; (res, _new_inerts) <- runTcSInerts inerts $
+ do { traceTcS "tcNormalise {" (ppr inerts)
; ty' <- flattenType norm_loc ty
; traceTcS "tcNormalise }" (ppr ty')
; pure ty' }
@@ -788,8 +784,9 @@ Note [tcNormalise]
tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
most invocations of the constraint solver are intended to simplify a set of
constraints or to decide if a particular set of constraints is satisfiable,
-the purpose of tcNormalise is to take a type, plus some local constraints, and
-normalise the type as much as possible with respect to those constraints.
+the purpose of tcNormalise is to take a type, plus some locally solved
+constraints in the form of an InertSet, and normalise the type as much as
+possible with respect to those constraints.
It does *not* reduce type or data family applications or look through newtypes.
@@ -798,9 +795,9 @@ expression, it's possible that the type of the scrutinee will only reduce
if some local equalities are solved for. See "Wrinkle: Local equalities"
in Note [Type normalisation] in "GHC.HsToCore.PmCheck".
-To accomplish its stated goal, tcNormalise first feeds the local constraints
-into solveSimpleGivens, then uses flattenType to simplify the desired type
-with respect to the givens.
+To accomplish its stated goal, tcNormalise first initialises the solver monad
+with the given InertCans, then uses flattenType to simplify the desired type
+with respect to the Givens in the InertCans.
***********************************************************************************
* *
@@ -893,7 +890,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
; psig_theta_vars <- mapM TcM.newEvVar psig_theta
; wanted_transformed_incl_derivs
<- setTcLevel rhs_tclvl $
- runTcSWithEvBinds ev_binds_var $
+ runTcSWithEvBinds ev_binds_var True $
do { let loc = mkGivenLoc rhs_tclvl UnkSkol $
env_lcl tc_env
psig_givens = mkGivens loc psig_theta_vars
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -15,7 +15,7 @@ module GHC.Tc.Solver.Monad (
getWorkList, updWorkListTcS, pushLevelNoWorkList,
-- The TcS monad
- TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
+ TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts,
failTcS, warnTcS, addErrTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
@@ -55,7 +55,7 @@ module GHC.Tc.Solver.Monad (
tcLookupClass, tcLookupId,
-- Inerts
- InertSet(..), InertCans(..),
+ InertSet(..), InertCans(..), emptyInert,
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getNoGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
@@ -2785,28 +2785,41 @@ runTcS :: TcS a -- What to run
-> TcM (a, EvBindMap)
runTcS tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; res <- runTcSWithEvBinds ev_binds_var tcs
+ ; res <- runTcSWithEvBinds ev_binds_var True tcs
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; return (res, ev_binds) }
-
-- | This variant of 'runTcS' will keep solving, even when only Deriveds
-- are left around. It also doesn't return any evidence, as callers won't
-- need it.
runTcSDeriveds :: TcS a -> TcM a
runTcSDeriveds tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; runTcSWithEvBinds ev_binds_var tcs }
+ ; runTcSWithEvBinds ev_binds_var True tcs }
-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities thing_inside
= do { ev_binds_var <- TcM.newNoTcEvBinds
- ; runTcSWithEvBinds ev_binds_var thing_inside }
+ ; runTcSWithEvBinds ev_binds_var True thing_inside }
+
+-- | A variant of 'runTcS' that takes and returns an 'InertSet' for
+-- later resumption of the 'TcS' session. Crucially, it doesn't
+-- 'unflattenGivens' when done.
+runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
+runTcSInerts inerts tcs = do
+ ev_binds_var <- TcM.newTcEvBinds
+ -- Passing False here to prohibit unflattening
+ runTcSWithEvBinds ev_binds_var False $ do
+ setTcSInerts inerts
+ a <- tcs
+ new_inerts <- getTcSInerts
+ return (a, new_inerts)
runTcSWithEvBinds :: EvBindsVar
+ -> Bool -- ^ Unflatten types afterwards? Don't if you want to reuse the InertSet.
-> TcS a
-> TcM a
-runTcSWithEvBinds ev_binds_var tcs
+runTcSWithEvBinds ev_binds_var unflatten tcs
= do { unified_var <- TcM.newTcRef 0
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef emptyInert
@@ -2824,7 +2837,7 @@ runTcSWithEvBinds ev_binds_var tcs
; when (count > 0) $
csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
- ; unflattenGivens inert_var
+ ; when unflatten $ unflattenGivens inert_var
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
=====================================
testsuite/tests/pmcheck/should_compile/T17836.hs
=====================================
@@ -0,0 +1,97 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+module PM where
+
+import Data.Type.Equality ( type (:~:)(..) )
+import qualified Data.Kind
+
+data Type :: Data.Kind.Type -> Data.Kind.Type where
+ SRecNil :: Type ()
+ SRecCons :: String -> Type a -> Type b -> Type (a, b)
+ SIntTy :: Type Int
+
+pattern RecCons1 a <- (SRecCons _ _ a)
+
+eqType :: Type ty1 -> Type ty2 -> Maybe (ty1 :~: ty2)
+eqType SRecNil SRecNil = Just Refl
+eqType (SRecCons l1 s1 t1) (SRecCons l2 s2 t2)
+ | Just Refl <- s1 `eqType` s2
+ , Just Refl <- t1 `eqType` t2
+ , l1 == l2
+ = Just Refl
+eqType SIntTy SIntTy = Just Refl
+eqType _ _ = Nothing
+
+massive :: Int -> Type ty -> Type recty -> (forall ty'. Type ty' -> m r) -> m r
+massive fieldN sFieldTy sRecTy k =
+ case (fieldN, sFieldTy, sRecTy) of
+ (0, t, SRecCons _ t' _)
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (1, t, RecCons1 (SRecCons _ t' _))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (2, t, RecCons1 (RecCons1 (SRecCons _ t' _)))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (3, t, RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (4, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (5, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (6, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (7, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (8, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (9, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (10, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (11, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (12, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (13, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (14, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (15, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (16, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (17, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (18, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (19, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (20, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (21, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (22, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (23, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (24, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (25, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (26, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (27, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (28, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (29, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (30, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (31, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _))))))))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ (32, t, RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (RecCons1 (SRecCons _ t' _)))))))))))))))))))))))))))))))))
+ | Just Refl <- t `eqType` t' -> k sFieldTy
+ _ -> error "TODO support records >32"
=====================================
testsuite/tests/pmcheck/should_compile/T17836b.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+module PM where
+
+data T a where
+ T :: T b -> T (a, b)
+
+pattern P a <- (T a)
+
+massive :: T recty -> ()
+massive (P (P (P (P (P (P (P (P (P (P (P (P (P (P (P (P (P _))))))))))))))))) = ()
=====================================
testsuite/tests/pmcheck/should_compile/T17836b.stderr
=====================================
@@ -0,0 +1,10 @@
+
+T17836b.hs:11:1: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In an equation for ‘massive’:
+ Patterns not matched:
+ T _
+ P (T _)
+ P (P (T _))
+ P (P (P (T _)))
+ ...
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -124,6 +124,10 @@ test('T17729', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17783', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17836', collect_compiler_stats('bytes allocated',10), compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17836b', collect_compiler_stats('bytes allocated',10), compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17977', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9d682f7d6f0b022386fbc9ee57f4c90727d2fb7a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9d682f7d6f0b022386fbc9ee57f4c90727d2fb7a
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/20200907/0e9c7a29/attachment-0001.html>
More information about the ghc-commits
mailing list