[Git][ghc/ghc][master] 3 commits: Make `tcCheckSatisfiability` incremental (#18645)
Marge Bot
gitlab at gitlab.haskell.org
Sun Sep 13 01:27:50 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
69ea2fee by Sebastian Graf at 2020-09-12T21:27:40-04: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:
T17977
T18478
- - - - -
a77e48d2 by Sebastian Graf at 2020-09-12T21:27:40-04:00
Extract definition of DsM into GHC.HsToCore.Types
`DsM` was previously defined in `GHC.Tc.Types`, along with `TcM`. But
`GHC.Tc.Types` is in the set of transitive dependencies of `GHC.Parser`,
a set which we aim to minimise. Test case `CountParserDeps` checks for
that.
Having `DsM` in that set means the parser also depends on the innards of
the pattern-match checker in `GHC.HsToCore.PmCheck.Types`, which is the
reason we have that module in the first place.
In the previous commit, we represented the `TyState` by an `InertSet`,
but that pulls the constraint solver as well as 250 more modules into
the set of dependencies, triggering failure of `CountParserDeps`.
Clearly, we want to evolve the pattern-match checker (and the desugarer)
without being concerned by this test, so this patch includes a small
refactor that puts `DsM` into its own module.
- - - - -
fd5d622a by Sebastian Graf at 2020-09-12T21:27:40-04:00
Hackily decouple the parser from the desugarer
In a hopefully temporary hack, I re-used the idea from !1957 of using a
nullary type family to break the dependency from GHC.Driver.Hooks on the
definition of DsM ("Abstract Data").
This in turn broke the last dependency from the parser to the desugarer.
More details in `Note [The Decoupling Abstract Data Hack]`.
In the future, we hope to undo this hack again in favour of breaking the
dependency from the parser to DynFlags altogether.
- - - - -
16 changed files:
- compiler/GHC/Driver/Hooks.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- + compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/ghc.cabal.in
- + 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/Driver/Hooks.hs
=====================================
@@ -3,7 +3,7 @@
-- NB: this module is SOURCE-imported by DynFlags, and should primarily
-- refer to *types*, rather than *code*
-{-# LANGUAGE CPP, RankNTypes #-}
+{-# LANGUAGE CPP, RankNTypes, TypeFamilies #-}
module GHC.Driver.Hooks
( Hooks
@@ -11,6 +11,7 @@ module GHC.Driver.Hooks
, lookupHook
, getHooked
-- the hooks:
+ , DsForeignsHook
, dsForeignsHook
, tcForeignImportsHook
, tcForeignExportsHook
@@ -36,7 +37,6 @@ import GHC.Driver.Types
import GHC.Hs.Decls
import GHC.Hs.Binds
import GHC.Hs.Expr
-import GHC.Data.OrdList
import GHC.Tc.Types
import GHC.Data.Bag
import GHC.Types.Name.Reader
@@ -58,6 +58,7 @@ import GHC.Hs.Extension
import GHC.StgToCmm.Types (ModuleLFInfos)
import Data.Maybe
+import qualified Data.Kind
{-
************************************************************************
@@ -89,9 +90,32 @@ emptyHooks = Hooks
, cmmToRawCmmHook = Nothing
}
+{- Note [The Decoupling Abstract Data Hack]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The "Abstract Data" idea is due to Richard Eisenberg in
+https://gitlab.haskell.org/ghc/ghc/-/merge_requests/1957, where the pattern is
+described in more detail.
+
+Here we use it as a temporary measure to break the dependency from the Parser on
+the Desugarer until the parser is free of DynFlags. We introduced a nullary type
+family @DsForeignsook@, whose single definition is in GHC.HsToCore.Types, where
+we instantiate it to
+
+ [LForeignDecl GhcTc] -> DsM (ForeignStubs, OrdList (Id, CoreExpr))
+
+In doing so, the Hooks module (which is an hs-boot dependency of DynFlags) can
+be decoupled from its use of the DsM definition in GHC.HsToCore.Types. Since
+both DsM and the definition of @ForeignsHook@ live in the same module, there is
+virtually no difference for plugin authors that want to write a foreign hook.
+-}
+
+-- See Note [The Decoupling Abstract Data Hack]
+type family DsForeignsHook :: Data.Kind.Type
+
data Hooks = Hooks
- { dsForeignsHook :: Maybe ([LForeignDecl GhcTc]
- -> DsM (ForeignStubs, OrdList (Id, CoreExpr)))
+ { dsForeignsHook :: Maybe DsForeignsHook
+ -- ^ Actual type:
+ -- @Maybe ([LForeignDecl GhcTc] -> DsM (ForeignStubs, OrdList (Id, CoreExpr)))@
, tcForeignImportsHook :: Maybe ([LForeignDecl GhcRn]
-> TcM ([Id], [LForeignDecl GhcTc], Bag GlobalRdrElt))
, tcForeignExportsHook :: Maybe ([LForeignDecl GhcRn]
=====================================
compiler/GHC/HsToCore/Expr.hs
=====================================
@@ -816,7 +816,7 @@ ds_prag_expr (HsPragSCC _ _ cc) expr = do
mod_name <- getModule
count <- goptM Opt_ProfCountEntries
let nm = sl_fs cc
- flavour <- ExprCC <$> getCCIndexM nm
+ flavour <- ExprCC <$> getCCIndexDsM nm
Tick (ProfNote (mkUserCC nm mod_name (getLoc expr) flavour) count True)
<$> dsLExpr expr
else dsLExpr expr
=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -30,6 +30,7 @@ module GHC.HsToCore.Monad (
getGhcModeDs, dsGetFamInstEnvs,
dsLookupGlobal, dsLookupGlobalId, dsLookupTyCon,
dsLookupDataCon, dsLookupConLike,
+ getCCIndexDsM,
DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv,
@@ -73,6 +74,7 @@ import GHC.Types.Basic ( Origin )
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Core.TyCon
+import GHC.HsToCore.Types
import GHC.HsToCore.PmCheck.Types
import GHC.Types.Id
import GHC.Unit.Module
@@ -614,3 +616,7 @@ pprRuntimeTrace str doc expr = do
message = App (Var unpackCStringId) $
Lit $ mkLitString $ showSDoc dflags (hang (text str) 4 doc)
return $ mkApps (Var traceId) [Type (exprType expr), message, expr]
+
+-- | See 'getCCIndexM'.
+getCCIndexDsM :: FastString -> DsM CostCentreIndex
+getCCIndexDsM = getCCIndexM ds_cc_st
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -584,13 +584,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)
@@ -597,15 +596,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/HsToCore/Types.hs
=====================================
@@ -0,0 +1,85 @@
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+
+-- | Various types used during desugaring.
+module GHC.HsToCore.Types (
+ DsM, DsLclEnv(..), DsGblEnv(..),
+ DsMetaEnv, DsMetaVal(..), CompleteMatches
+ ) where
+
+import Data.IORef
+
+import GHC.Types.CostCentre.State
+import GHC.Types.Name.Env
+import GHC.Types.SrcLoc
+import GHC.Types.Var
+import GHC.Hs (LForeignDecl, HsExpr, GhcTc)
+import GHC.Tc.Types (TcRnIf, IfGblEnv, IfLclEnv, CompleteMatches)
+import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Nablas)
+import GHC.Core (CoreExpr)
+import GHC.Core.FamInstEnv
+import GHC.Utils.Error
+import GHC.Utils.Outputable as Outputable
+import GHC.Unit.Module
+import GHC.Driver.Hooks (DsForeignsHook)
+import GHC.Data.OrdList (OrdList)
+import GHC.Driver.Types (ForeignStubs)
+
+{-
+************************************************************************
+* *
+ Desugarer monad
+* *
+************************************************************************
+
+Now the mondo monad magic (yes, @DsM@ is a silly name)---carry around
+a @UniqueSupply@ and some annotations, which
+presumably include source-file location information:
+-}
+
+-- | Global read-only context and state of the desugarer.
+-- The statefulness is implemented through 'IORef's.
+data DsGblEnv
+ = DsGblEnv
+ { ds_mod :: Module -- For SCC profiling
+ , ds_fam_inst_env :: FamInstEnv -- Like tcg_fam_inst_env
+ , ds_unqual :: PrintUnqualified
+ , ds_msgs :: IORef Messages -- Warning messages
+ , ds_if_env :: (IfGblEnv, IfLclEnv) -- Used for looking up global,
+ -- possibly-imported things
+ , ds_complete_matches :: CompleteMatches
+ -- Additional complete pattern matches
+ , ds_cc_st :: IORef CostCentreState
+ -- Tracking indices for cost centre annotations
+ }
+
+instance ContainsModule DsGblEnv where
+ extractModule = ds_mod
+
+-- | Local state of the desugarer, extended as we lexically descend
+data DsLclEnv
+ = DsLclEnv
+ { dsl_meta :: DsMetaEnv -- ^ Template Haskell bindings
+ , dsl_loc :: RealSrcSpan -- ^ To put in pattern-matching error msgs
+ , dsl_nablas :: Nablas
+ -- ^ See Note [Note [Long-distance information] in "GHC.HsToCore.PmCheck".
+ -- The set of reaching values Nablas is augmented as we walk inwards, refined
+ -- through each pattern match in turn
+ }
+
+-- Inside [| |] brackets, the desugarer looks
+-- up variables in the DsMetaEnv
+type DsMetaEnv = NameEnv DsMetaVal
+
+data DsMetaVal
+ = DsBound Id -- Bound by a pattern inside the [| |].
+ -- Will be dynamically alpha renamed.
+ -- The Id has type THSyntax.Var
+
+ | DsSplice (HsExpr GhcTc) -- These bindings are introduced by
+ -- the PendingSplices on a HsBracketOut
+
+-- | Desugaring monad. See also 'TcM'.
+type DsM = TcRnIf DsGblEnv DsLclEnv
+
+-- See Note [The Decoupling Abstract Data Hack]
+type instance DsForeignsHook = [LForeignDecl GhcTc] -> DsM (ForeignStubs, OrdList (Id, CoreExpr))
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -681,7 +681,7 @@ funBindTicks loc fun_id mod sigs
= getOccFS (Var.varName fun_id)
cc_name = moduleNameFS (moduleName mod) `appendFS` consFS '.' cc_str
= do
- flavour <- DeclCC <$> getCCIndexM cc_name
+ flavour <- DeclCC <$> getCCIndexTcM cc_name
let cc = mkUserCC cc_name mod loc flavour
return [ProfNote cc True True]
| otherwise
=====================================
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
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -45,11 +45,7 @@ module GHC.Tc.Types(
IdBindingInfo(..), ClosedTypeId, RhsNames,
IsGroupClosed(..),
SelfBootInfo(..),
- pprTcTyThingCategory, pprPECategory, CompleteMatch,
-
- -- Desugaring types
- DsM, DsLclEnv(..), DsGblEnv(..),
- DsMetaEnv, DsMetaVal(..), CompleteMatches,
+ pprTcTyThingCategory, pprPECategory, CompleteMatch, CompleteMatches,
-- Template Haskell
ThStage(..), SpliceType(..), PendingStuff(..),
@@ -105,7 +101,6 @@ import GHC.Tc.Types.Origin
import GHC.Types.Annotations
import GHC.Core.InstEnv
import GHC.Core.FamInstEnv
-import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Nablas)
import GHC.Data.IOEnv
import GHC.Types.Name.Reader
import GHC.Types.Name
@@ -190,7 +185,6 @@ type TcRn = TcRnIf TcGblEnv TcLclEnv -- Type inference
type IfM lcl = TcRnIf IfGblEnv lcl -- Iface stuff
type IfG = IfM () -- Top level
type IfL = IfM IfLclEnv -- Nested
-type DsM = TcRnIf DsGblEnv DsLclEnv -- Desugaring
-- TcRn is the type-checking and renaming monad: the main monad that
-- most type-checking takes place in. The global environment is
@@ -289,58 +283,6 @@ data IfLclEnv
if_id_env :: FastStringEnv Id -- Nested id binding
}
-{-
-************************************************************************
-* *
- Desugarer monad
-* *
-************************************************************************
-
-Now the mondo monad magic (yes, @DsM@ is a silly name)---carry around
-a @UniqueSupply@ and some annotations, which
-presumably include source-file location information:
--}
-
-data DsGblEnv
- = DsGblEnv
- { ds_mod :: Module -- For SCC profiling
- , ds_fam_inst_env :: FamInstEnv -- Like tcg_fam_inst_env
- , ds_unqual :: PrintUnqualified
- , ds_msgs :: IORef Messages -- Warning messages
- , ds_if_env :: (IfGblEnv, IfLclEnv) -- Used for looking up global,
- -- possibly-imported things
- , ds_complete_matches :: CompleteMatches
- -- Additional complete pattern matches
- , ds_cc_st :: IORef CostCentreState
- -- Tracking indices for cost centre annotations
- }
-
-instance ContainsModule DsGblEnv where
- extractModule = ds_mod
-
-data DsLclEnv = DsLclEnv {
- dsl_meta :: DsMetaEnv, -- Template Haskell bindings
- dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs
-
- -- See Note [Note [Long-distance information] in "GHC.HsToCore.PmCheck"
- -- The set of reaching values Nablas is augmented as we walk inwards,
- -- refined through each pattern match in turn
- dsl_nablas :: Nablas
- }
-
--- Inside [| |] brackets, the desugarer looks
--- up variables in the DsMetaEnv
-type DsMetaEnv = NameEnv DsMetaVal
-
-data DsMetaVal
- = DsBound Id -- Bound by a pattern inside the [| |].
- -- Will be dynamically alpha renamed.
- -- The Id has type THSyntax.Var
-
- | DsSplice (HsExpr GhcTc) -- These bindings are introduced by
- -- the PendingSplices on a HsBracketOut
-
-
{-
************************************************************************
* *
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -138,7 +138,7 @@ module GHC.Tc.Utils.Monad(
withException,
-- * Stuff for cost centres.
- ContainsCostCentreState(..), getCCIndexM,
+ getCCIndexM, getCCIndexTcM,
-- * Types etc.
module GHC.Tc.Types,
@@ -2081,23 +2081,16 @@ discussion). We don't currently know a general solution to this problem, but
we can use uninterruptibleMask_ to avoid the situation.
-}
--- | Environments which track 'CostCentreState'
-class ContainsCostCentreState e where
- extractCostCentreState :: e -> TcRef CostCentreState
-
-instance ContainsCostCentreState TcGblEnv where
- extractCostCentreState = tcg_cc_st
-
-instance ContainsCostCentreState DsGblEnv where
- extractCostCentreState = ds_cc_st
-
-- | Get the next cost centre index associated with a given name.
-getCCIndexM :: (ContainsCostCentreState gbl)
- => FastString -> TcRnIf gbl lcl CostCentreIndex
-getCCIndexM nm = do
+getCCIndexM :: (gbl -> TcRef CostCentreState) -> FastString -> TcRnIf gbl lcl CostCentreIndex
+getCCIndexM get_ccs nm = do
env <- getGblEnv
- let cc_st_ref = extractCostCentreState env
+ let cc_st_ref = get_ccs env
cc_st <- readTcRef cc_st_ref
let (idx, cc_st') = getCCIndex nm cc_st
writeTcRef cc_st_ref cc_st'
return idx
+
+-- | See 'getCCIndexM'.
+getCCIndexTcM :: FastString -> TcM CostCentreIndex
+getCCIndexTcM = getCCIndexM tcg_cc_st
=====================================
compiler/ghc.cabal.in
=====================================
@@ -314,6 +314,7 @@ Library
GHC.HsToCore.PmCheck
GHC.HsToCore.Coverage
GHC.HsToCore
+ GHC.HsToCore.Types
GHC.HsToCore.Arrows
GHC.HsToCore.Binds
GHC.HsToCore.Foreign.Call
=====================================
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/-/compare/2157be52cd454353582b04d89492b239b90f91f7...fd5d622a5ee283d3c1f1ccd28b4f73aab30d7d9f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/2157be52cd454353582b04d89492b239b90f91f7...fd5d622a5ee283d3c1f1ccd28b4f73aab30d7d9f
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/20200912/a34d104f/attachment-0001.html>
More information about the ghc-commits
mailing list