summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Solver/Rewrite.hs
Commit message (Collapse)AuthorAgeFilesLines
* Narrow the dont-decompose-newtype testSimon Peyton Jones2023-02-161-57/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | Following #22924 this patch narrows the test that stops us decomposing newtypes. The key change is the use of noGivenNewtypeReprEqs in GHC.Tc.Solver.Canonical.canTyConApp. We went to and fro on the solution, as you can see in #22924. The result is carefully documented in Note [Decomoposing newtype equalities] On the way I had revert most of commit 3e827c3f74ef76d90d79ab6c4e71aa954a1a6b90 Author: Richard Eisenberg <rae@cs.brynmawr.edu> Date: Mon Dec 5 10:14:02 2022 -0500 Do newtype unwrapping in the canonicaliser and rewriter See Note [Unwrap newtypes first], which has the details. It turns out that (a) 3e827c3f makes GHC behave worse on some recursive newtypes (see one of the tests on this commit) (b) the finer-grained test (namely noGivenNewtypeReprEqs) renders 3e827c3f unnecessary
* Do newtype unwrapping in the canonicaliser and rewriterRichard Eisenberg2023-01-261-7/+71
| | | | | | See Note [Unwrap newtypes first], which has the details. Close #22519.
* Drop support for kind constraints.wip/p547Richard Eisenberg2022-12-241-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | This implements proposal 547 and closes ticket #22298. See the proposal and ticket for motivation. Compiler perf improves a bit Metrics: compile_time/bytes allocated ------------------------------------- CoOpt_Singletons(normal) -2.4% GOOD T12545(normal) +1.0% T13035(normal) -13.5% GOOD T18478(normal) +0.9% T9872d(normal) -2.2% GOOD geo. mean -0.2% minimum -13.5% maximum +1.0% Metric Decrease: CoOpt_Singletons T13035 T9872d
* Scrub some no-warning pragmas.M Farkas-Dyck2022-11-231-2/+0
|
* Type vs Constraint: finally nailedSimon Peyton Jones2022-11-111-17/+17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This big patch addresses the rats-nest of issues that have plagued us for years, about the relationship between Type and Constraint. See #11715/#21623. The main payload of the patch is: * To introduce CONSTRAINT :: RuntimeRep -> Type * To make TYPE and CONSTRAINT distinct throughout the compiler Two overview Notes in GHC.Builtin.Types.Prim * Note [TYPE and CONSTRAINT] * Note [Type and Constraint are not apart] This is the main complication. The specifics * New primitive types (GHC.Builtin.Types.Prim) - CONSTRAINT - ctArrowTyCon (=>) - tcArrowTyCon (-=>) - ccArrowTyCon (==>) - funTyCon FUN -- Not new See Note [Function type constructors and FunTy] and Note [TYPE and CONSTRAINT] * GHC.Builtin.Types: - New type Constraint = CONSTRAINT LiftedRep - I also stopped nonEmptyTyCon being built-in; it only needs to be wired-in * Exploit the fact that Type and Constraint are distinct throughout GHC - Get rid of tcView in favour of coreView. - Many tcXX functions become XX functions. e.g. tcGetCastedTyVar --> getCastedTyVar * Kill off Note [ForAllTy and typechecker equality], in (old) GHC.Tc.Solver.Canonical. It said that typechecker-equality should ignore the specified/inferred distinction when comparein two ForAllTys. But that wsa only weakly supported and (worse) implies that we need a separate typechecker equality, different from core equality. No no no. * GHC.Core.TyCon: kill off FunTyCon in data TyCon. There was no need for it, and anyway now we have four of them! * GHC.Core.TyCo.Rep: add two FunTyFlags to FunCo See Note [FunCo] in that module. * GHC.Core.Type. Lots and lots of changes driven by adding CONSTRAINT. The key new function is sORTKind_maybe; most other changes are built on top of that. See also `funTyConAppTy_maybe` and `tyConAppFun_maybe`. * Fix a longstanding bug in GHC.Core.Type.typeKind, and Core Lint, in kinding ForAllTys. See new tules (FORALL1) and (FORALL2) in GHC.Core.Type. (The bug was that before (forall (cv::t1 ~# t2). blah), where blah::TYPE IntRep, would get kind (TYPE IntRep), but it should be (TYPE LiftedRep). See Note [Kinding rules for types] in GHC.Core.Type. * GHC.Core.TyCo.Compare is a new module in which we do eqType and cmpType. Of course, no tcEqType any more. * GHC.Core.TyCo.FVs. I moved some free-var-like function into this module: tyConsOfType, visVarsOfType, and occCheckExpand. Refactoring only. * GHC.Builtin.Types. Compiletely re-engineer boxingDataCon_maybe to have one for each /RuntimeRep/, rather than one for each /Type/. This dramatically widens the range of types we can auto-box. See Note [Boxing constructors] in GHC.Builtin.Types The boxing types themselves are declared in library ghc-prim:GHC.Types. GHC.Core.Make. Re-engineer the treatment of "big" tuples (mkBigCoreVarTup etc) GHC.Core.Make, so that it auto-boxes unboxed values and (crucially) types of kind Constraint. That allows the desugaring for arrows to work; it gathers up free variables (including dictionaries) into tuples. See Note [Big tuples] in GHC.Core.Make. There is still work to do here: #22336. But things are better than before. * GHC.Core.Make. We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint. Ditto noInlineId vs noInlieConstraintId in GHC.Types.Id.Make; see Note [inlineId magic]. * GHC.Core.TyCo.Rep. Completely refactor the NthCo coercion. It is now called SelCo, and its fields are much more descriptive than the single Int we used to have. A great improvement. See Note [SelCo] in GHC.Core.TyCo.Rep. * GHC.Core.RoughMap.roughMatchTyConName. Collapse TYPE and CONSTRAINT to a single TyCon, so that the rough-map does not distinguish them. * GHC.Core.DataCon - Mainly just improve documentation * Some significant renamings: GHC.Core.Multiplicity: Many --> ManyTy (easier to grep for) One --> OneTy GHC.Core.TyCo.Rep TyCoBinder --> GHC.Core.Var.PiTyBinder GHC.Core.Var TyCoVarBinder --> ForAllTyBinder AnonArgFlag --> FunTyFlag ArgFlag --> ForAllTyFlag GHC.Core.TyCon TyConTyCoBinder --> TyConPiTyBinder Many functions are renamed in consequence e.g. isinvisibleArgFlag becomes isInvisibleForAllTyFlag, etc * I refactored FunTyFlag (was AnonArgFlag) into a simple, flat data type data FunTyFlag = FTF_T_T -- (->) Type -> Type | FTF_T_C -- (-=>) Type -> Constraint | FTF_C_T -- (=>) Constraint -> Type | FTF_C_C -- (==>) Constraint -> Constraint * GHC.Tc.Errors.Ppr. Some significant refactoring in the TypeEqMisMatch case of pprMismatchMsg. * I made the tyConUnique field of TyCon strict, because I saw code with lots of silly eval's. That revealed that GHC.Settings.Constants.mAX_SUM_SIZE can only be 63, because we pack the sum tag into a 6-bit field. (Lurking bug squashed.) Fixes * #21530 Updates haddock submodule slightly. Performance changes ~~~~~~~~~~~~~~~~~~~ I was worried that compile times would get worse, but after some careful profiling we are down to a geometric mean 0.1% increase in allocation (in perf/compiler). That seems fine. There is a big runtime improvement in T10359 Metric Decrease: LargeRecord MultiLayerModulesTH_OneShot T13386 T13719 Metric Increase: T8095
* Define `Infinite` list and use where appropriate.M Farkas-Dyck2022-11-081-9/+11
| | | | | | | | Also add perf test for infinite list fusion. In particular, in `GHC.Core`, often we deal with infinite lists of roles. Also in a few locations we deal with infinite lists of names. Thanks to simonpj for helping to write the Note [Fusion for `Infinite` lists].
* Kill derived constraintsRichard Eisenberg2022-02-231-118/+77
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Co-authored by: Sam Derbyshire Previously, GHC had three flavours of constraint: Wanted, Given, and Derived. This removes Derived constraints. Though serving a number of purposes, the most important role of Derived constraints was to enable better error messages. This job has been taken over by the new RewriterSets, as explained in Note [Wanteds rewrite wanteds] in GHC.Tc.Types.Constraint. Other knock-on effects: - Various new Notes as I learned about under-described bits of GHC - A reshuffling around the AST for implicit-parameter bindings, with better integration with TTG. - Various improvements around fundeps. These were caused by the fact that, previously, fundep constraints were all Derived, and Derived constraints would get dropped. Thus, an unsolved Derived didn't stop compilation. Without Derived, this is no longer possible, and so we have to be considerably more careful around fundeps. - A nice little refactoring in GHC.Tc.Errors to center the work on a new datatype called ErrorItem. Constraints are converted into ErrorItems at the start of processing, and this allows for a little preprocessing before the main classification. - This commit also cleans up the behavior in generalisation around functional dependencies. Now, if a variable is determined by functional dependencies, it will not be quantified. This change is user facing, but it should trim down GHC's strange behavior around fundeps. - Previously, reportWanteds did quite a bit of work, even on an empty WantedConstraints. This commit adds a fast path. - Now, GHC will unconditionally re-simplify constraints during quantification. See Note [Unconditionally resimplify constraints when quantifying], in GHC.Tc.Solver. Close #18398. Close #18406. Solve the fundep-related non-confluence in #18851. Close #19131. Close #19137. Close #20922. Close #20668. Close #19665. ------------------------- Metric Decrease: LargeRecord T9872b T9872b_defer T9872d TcPlugin_RewritePerf -------------------------
* Make typechecker trace less strictSimon Peyton Jones2022-01-311-2/+4
| | | | Fixes #21011
* Compare FunTys as if they were TyConApps.Richard Eisenberg2021-09-291-12/+40
| | | | | | | | | | | See Note [Equality on FunTys] in TyCoRep. Close #17675. Close #17655, about documentation improvements included in this patch. Close #19677, about a further mistake around FunTy. test cases: typecheck/should_compile/T19677
* Add rewriting to typechecking pluginssheaf2021-08-131-40/+101
| | | | | | | | | | | | | | | | | | | | | | | | | | | Type-checking plugins can now directly rewrite type-families. The TcPlugin record is given a new field, tcPluginRewrite. The plugin specifies how to rewrite certain type-families with a value of type `UniqFM TyCon TcPluginRewriter`, where: type TcPluginRewriter = RewriteEnv -- Rewriter environment -> [Ct] -- Givens -> [TcType] -- type family arguments -> TcPluginM TcPluginRewriteResult data TcPluginRewriteResult = TcPluginNoRewrite | TcPluginRewriteTo { tcPluginRewriteTo :: Reduction , tcRewriterNewWanteds :: [Ct] } When rewriting an exactly-saturated type-family application, GHC will first query type-checking plugins for possible rewritings before proceeding. Includes some changes to the TcPlugin API, e.g. removal of the EvBindsVar parameter to the TcPluginM monad.
* Use Reductions to keep track of rewritingssheaf2021-08-041-208/+195
| | | | | | | | | | | | | | | | | | | | | | | | | | | | We define Reduction = Reduction Coercion !Type. A reduction of the form 'Reduction co new_ty' witnesses an equality ty ~co~> new_ty. That is, the rewriting happens left-to-right: the right-hand-side type of the coercion is the rewritten type, and the left-hand-side type the original type. Sticking to this convention makes the codebase more consistent, helping to avoid certain applications of SymCo. This replaces the parts of the codebase which represented reductions as pairs, (Coercion,Type) or (Type,Coercion). Reduction being strict in the Type argument improves performance in some programs that rewrite many type families (such as T9872). Fixes #20161 ------------------------- Metric Decrease: T5321Fun T9872a T9872b T9872c T9872d -------------------------
* Rip GHC.Tc.Solver.Monad asunder (only)Richard Eisenberg2021-05-291-1/+2
| | | | | | | | | | | This creates new modules GHC.Tc.Solver.InertSet and GHC.Tc.Solver.Types. The Monad module is still pretty big, but this is an improvement. Moreover, it means that GHC.HsToCore.Pmc.Solver.Types no longer depends on the constraint solver (it now depends on GHC.Tc.Solver.InertSet), making the error-messages work easier. This patch thus contributes to #18516.
* Remove useless {-# LANGUAGE CPP #-} pragmasSylvain Henry2021-05-121-1/+1
|
* Fully remove HsVersions.hSylvain Henry2021-05-121-2/+0
| | | | | | | | | | Replace uses of WARN macro with calls to: warnPprTrace :: Bool -> SDoc -> a -> a Remove the now unused HsVersions.h Bump haddock submodule
* Replace CPP assertions with Haskell functionsSylvain Henry2021-05-121-4/+5
| | | | | | | | | | | | | | | There is no reason to use CPP. __LINE__ and __FILE__ macros are now better replaced with GHC's CallStack. As a bonus, assert error messages now contain more information (function name, column). Here is the mapping table (HasCallStack omitted): * ASSERT: assert :: Bool -> a -> a * MASSERT: massert :: Bool -> m () * ASSERTM: assertM :: m Bool -> m () * ASSERT2: assertPpr :: Bool -> SDoc -> a -> a * MASSERT2: massertPpr :: Bool -> SDoc -> m () * ASSERTM2: assertPprM :: m Bool -> SDoc -> m ()
* Clarify commentary around the constraint solverRichard Eisenberg2021-04-101-0/+3
| | | | | No changes to code; no changes to theory. Just better explanation.
* Rewrite.split: Fix reboxingBen Gamari2021-02-271-2/+5
| | | | | | | | As noted in #19102, we would previously ended up reboxing the tuple result of `split`'s worker and then immediately take apart the boxed tuple to again unpack it into an unboxed result. Fixes #19102.
* GHC.Tc.Solver.Rewrite: oneShot-ifyBen Gamari2021-02-271-7/+14
| | | | | Following the example of Note [The one-shot state monad trick]. c.f. #18202.
* Never Anyify during kind inferenceRichard Eisenberg2021-01-091-1/+1
| | | | | | | | | See Note [Error on unconstrained meta-variables] in TcMType. Close #17301 Close #17567 Close #17562 Close #15474
* Quick Look: zonk result typeSimon Peyton Jones2020-12-191-0/+5
| | | | | | | | | | | | | | | | | Provoked by #18987, this patch adds a missing zonkQuickLook of app_res_rho in tcApp. Most of the time this zonk is unnecesary. In fact, I can't think of a concrete case where it is needed -- hence no test. But even if it isn't necessary, the reasoning that allows it to be omitted is very subtle. So I've put it in. However, adding this zonk does /not/ affect the emitted constraints, so the reported symptoms for #18987 remain, but harmlessly so, and now documented in a new Note [Instantiation variables are short lived] in GHC.Tc.Gen.App. No change in behaviour, no tests.
* Rename the flattener to become the rewriter.Richard Eisenberg2020-12-011-0/+1028
Now that flattening doesn't produce flattening variables, it's not really flattening anything: it's rewriting. This change also means that the rewriter can no longer be confused the core flattener (in GHC.Core.Unify), which is sometimes used during type-checking.