summaryrefslogtreecommitdiff
path: root/compiler/types
Commit message (Collapse)AuthorAgeFilesLines
...
* Remove the type-checking knot.Richard Eisenberg2018-08-013-14/+38
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Bug #15380 hangs because a knot-tied TyCon ended up in a kind. Looking at the code in tcInferApps, I'm amazed this hasn't happened before! I couldn't think of a good way to fix it (with dependent types, we can't really keep types out of kinds, after all), so I just went ahead and removed the knot. This was remarkably easy to do. In tcTyVar, when we find a TcTyCon, just use it. (Previously, we looked up the knot-tied TyCon and used that.) Then, during the final zonk, replace TcTyCons with the real, full-blooded TyCons in the global environment. It's all very easy. The new bit is explained in the existing Note [Type checking recursive type and class declarations] in TcTyClsDecls. Naturally, I removed various references to the knot and the zonkTcTypeInKnot (and related) functions. Now, we can print types during type checking with abandon! NB: There is a teensy error message regression with this patch, around the ordering of quantified type variables. This ordering problem is fixed (I believe) with the patch for #14880. The ordering affects only internal variables that cannot be instantiated with any kind of visible type application. There is also a teensy regression around the printing of types in TH splices. I think this is really a TH bug and will file separately. Test case: dependent/should_fail/T15380
* Fix #15453: bug in ForAllCo case in opt_trans_ruleNingning Xie2018-07-291-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: Given ``` co1 = \/ tv1 : eta1. r1 co2 = \/ tv2 : eta2. r2 ``` We would like to optimize `co1; co2` so we push transitivity inside forall. It should be ``` \/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1]) ``` It is implemented in the ForAllCo case in opt_trans_rule in OptCoercion. However current implementation is not right: ``` r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded! ``` This patch corrects it to be ``` r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 ``` Test Plan: validate Reviewers: bgamari, goldfire, RyanGlScott Reviewed By: RyanGlScott Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15453 Differential Revision: https://phabricator.haskell.org/D5018
* Treat isConstraintKind more consistentlySimon Peyton Jones2018-07-254-92/+87
| | | | | | | | | | | | | | | | | | | | | | | It turned out that we were not being consistent about our use of isConstraintKind. It's delicate, because the typechecker treats Constraint and Type as /distinct/, whereas they are the /same/ in the rest of the compiler (Trac #11715). And had it wrong, which led to Trac #15412. This patch does the following: * Rename isConstraintKind to tcIsConstraintKind returnsConstraintKind to tcReturnsConstraintKind to emphasise that they use the 'tcView' view of types. * Move these functions, and some related ones (tcIsLiftedTypeKind), from Kind.hs, to group together in Type.hs, alongside isPredTy. It feels very unsatisfactory that these 'tcX' functions live in Type, but it happens because isPredTy is called later in the compiler too. But it's a consequence of the 'Constraint vs Type' dilemma.
* Fix a nasty bug in piResultTysSimon Peyton Jones2018-07-241-8/+35
| | | | | | | | | I was failing to instantiate vigorously enough in Type.piResultTys and in the very similar function ToIface.toIfaceAppArgsX This caused Trac #15428. The fix is easy. See Note [Care with kind instantiation] in Type.hs
* Fix some casts.Richard Eisenberg2018-07-231-1/+1
| | | | | | | | | | | | | | This fixes #15346, and is a team effort between Ryan Scott and myself (mostly Ryan). We discovered two errors related to FC's "push" rules, one in the TPush rule (as implemented in pushCoTyArg) and one in KPush rule (it shows up in liftCoSubstVarBndr). The solution: do what the paper says, instead of whatever random thoughts popped into my head as I was actually implementing. Also fixes #15419, which is actually the same underlying problem. Test case: dependent/should_compile/T{15346,15419}.
* Small spelling fixes for Unify.hsSasa Bogicevic2018-07-191-4/+4
| | | | | | | | | | Reviewers: bgamari, osa1 Reviewed By: osa1 Subscribers: rwbarton, thomie, carter Differential Revision: https://phabricator.haskell.org/D4985
* Use IfaceAppArgs to store an IfaceAppTy's argumentsRyan Scott2018-07-111-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: Currently, an `IfaceAppTy` has no way to tell whether its argument is visible or not, so it simply treats all arguments as visible, leading to #15330. We already have a solution for this problem in the form of the `IfaceTcArgs` data structure, used by `IfaceTyConApp` to represent the arguments to a type constructor. Therefore, it makes sense to reuse this machinery for `IfaceAppTy`, so this patch does just that. This patch: 1. Renames `IfaceTcArgs` to `IfaceAppArgs` to reflect its more general purpose. 2. Changes the second field of `IfaceAppTy` from `IfaceType` to `IfaceAppArgs`, and propagates the necessary changes through. In particular, pretty-printing an `IfaceAppTy` now goes through the `IfaceAppArgs` pretty-printer, which correctly displays arguments as visible or not for free, fixing #15330. 3. Changes `toIfaceTypeX` and related functions so that when converting an `AppTy` to an `IfaceAppTy`, it flattens as many argument `AppTy`s as possible, and then converts those arguments into an `IfaceAppArgs` list, using the kind of the function `Type` as a guide. (Doing so minimizes the number of times we need to call `typeKind`, which is more expensive that finding the kind of a `TyCon`.) Test Plan: make test TEST=T15330 Reviewers: goldfire, simonpj, bgamari Reviewed By: simonpj Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15330 Differential Revision: https://phabricator.haskell.org/D4938
* Note [Ordering of implicit variables]Richard Eisenberg2018-07-102-1/+6
| | | | | | This addresses #14808 [ci skip]
* Fix decompsePiCos and visible type applicationSimon Peyton Jones2018-07-103-45/+71
| | | | | | | | | | | | | | | | | | | | | | | | | | | Trac #15343 was caused by two things First, in TcHsType.tcHsTypeApp, which deals with the type argment in visible type application, we were failing to call solveLocalEqualities. But the type argument is like a user type signature so it's at least inconsitent not to do so. I thought that would nail it. But it didn't. It turned out that we were ended up calling decomposePiCos on a type looking like this (f |> co) Int where co :: (forall a. ty) ~ (t1 -> t2) Now, 'co' is insoluble, and we'll report that later. But meanwhile we don't want to crash in decomposePiCos. My fix involves keeping track of the type on both sides of the coercion, and ensuring that the outer shape matches before decomposing. I wish there was a simpler way to do this. But I think this one is at least robust. I suppose it is possible that the decomposePiCos fix would have cured the original report, but I'm leaving the one-line tcHsTypeApp fix in too because it just seems more consistent.
* Refactor coercion ruleningning2018-07-098-255/+424
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: The patch is an attempt on #15192. It defines a new coercion rule ``` | GRefl Role Type MCoercion ``` which correspondes to the typing rule ``` t1 : k1 ------------------------------------ GRefl r t1 MRefl: t1 ~r t1 t1 : k1 co :: k1 ~ k2 ------------------------------------ GRefl r t1 (MCo co) : t1 ~r t1 |> co ``` MCoercion wraps a coercion, which might be reflexive (MRefl) or not (MCo co). To know more about MCoercion see #14975. We keep Refl ty as a special case for nominal reflexive coercions, naemly, Refl ty :: ty ~n ty. This commit is meant to be a general performance improvement, but there are a few regressions. See #15192, comment:13 for more information. Test Plan: ./validate Reviewers: bgamari, goldfire, simonpj Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15192 Differential Revision: https://phabricator.haskell.org/D4747
* Define an Outputable MCoercion instanceRyan Scott2018-07-081-0/+4
| | | | | | | | | | | | | | | | Summary: I needed this when debugging #15346. Test Plan: Does it compile? It does? Cool. Reviewers: bgamari, mpickering Reviewed By: mpickering Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15311 Differential Revision: https://phabricator.haskell.org/D4944
* A few typofixes in commentsGabor Greif2018-06-291-1/+1
|
* Add commnent about binder orderSimon Peyton Jones2018-06-261-4/+15
| | | | ...provoked by Trac #15308
* Typofixes in comments and whitespace only [ci skip]Gabor Greif2018-06-261-1/+1
|
* Adjust comments (Trac #14164)Simon Peyton Jones2018-06-191-2/+2
|
* Typofixes in docs and comments [ci skip]Gabor Greif2018-06-182-5/+5
|
* Two small refactoringsSimon Peyton Jones2018-06-185-32/+35
| | | | | | | | * Define Type.substTyVarBndrs, and use it * Rename substTyVarBndrCallback to substTyVarBndrUsing, and other analogous higher order functions. I kept stumbling over the name.
* Fix an infinite loop in niFixTCvSubstSimon Peyton Jones2018-06-181-30/+86
| | | | | | | | | | | | | | | | | | | | | Trac #14164 made GHC loop, a pretty serious error. It turned out that Unify.niFixTCvSubst was looping forever, because we had a substitution like a :-> ....(b :: (c :: d)).... d :-> ... We correctly recognised that d was free in the range of the substitution, but then failed to apply it "deeeply enough" to the range of the substiuttion, so d was /still/ free in the range, and we kept on going. Trac #9106 was caused by a similar problem, but alas my fix to Trac #9106 was inadequate when the offending type variable is more deeply buried. Urk. This time I think I've fixed it! It's much more subtle than I though, and it took most of a long train journey to figure it out. I wrote a long note to explain: Note [Finding the substitution fixpoint]
* Fix corner case in typeKind, plus refactoringSimon Peyton Jones2018-06-152-11/+163
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is a continuation of commit 9d600ea68c283b0d38ac663c3cc48baba6b94f57 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Fri Jun 1 16:36:57 2018 +0100 Expand type synonyms when Linting a forall That patch pointed out that there was a lurking hole in typeKind, where it could return an ill-scoped kind, because of not expanding type synonyms enough. This patch fixes it, quite nicely * Use occCheckExpand to expand those synonyms (it was always designed for that exact purpose), and call it from Type.typeKind CoreUtils.coreAltType CoreLint.lintTYpe * Consequently, move occCheckExpand from TcUnify.hs to Type.hs, and generalise it to take a list of type variables. I also tidied up lintType a bit.
* Embrace -XTypeInType, add -XStarIsTypeVladislav Zavialov2018-06-145-35/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: Implement the "Embrace Type :: Type" GHC proposal, .../ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst GHC 8.0 included a major change to GHC's type system: the Type :: Type axiom. Though casual users were protected from this by hiding its features behind the -XTypeInType extension, all programs written in GHC 8+ have the axiom behind the scenes. In order to preserve backward compatibility, various legacy features were left unchanged. For example, with -XDataKinds but not -XTypeInType, GADTs could not be used in types. Now these restrictions are lifted and -XTypeInType becomes a redundant flag that will be eventually deprecated. * Incorporate the features currently in -XTypeInType into the -XPolyKinds and -XDataKinds extensions. * Introduce a new extension -XStarIsType to control how to parse * in code and whether to print it in error messages. Test Plan: Validate Reviewers: goldfire, hvr, bgamari, alanz, simonpj Reviewed By: goldfire, simonpj Subscribers: rwbarton, thomie, mpickering, carter GHC Trac Issues: #15195 Differential Revision: https://phabricator.haskell.org/D4748
* OptCoercion: Ensure we use new UnivCo provenance to construct optimised cos.Ben Gamari2018-06-141-3/+3
| | | | | @goldfire noticed that there were several points in OptOercion.opt_univ where we constructed the optimised coercion using the untransformed provenance.
* Rename dataConRepNameUnique to dataConTyRepNameUniqueMatthew Pickering2018-06-071-2/+2
| | | | | | | | | | | | | | The `DataCon` rep also applies to the worker. For example, see `MkId.mkDataConRep`. `dataConTyRepNameUnique` is for the type representation, so we rename it to make this distinction clear. Reviewers: bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter Differential Revision: https://phabricator.haskell.org/D4797
* Don't use unsafeGlobalDynFlags in optCoercionBen Gamari2018-06-071-4/+8
| | | | | | | | | | | | | | | | | This plumbs DynFlags through CoreOpt so optCoercion can finally eliminate its usage of `unsafeGlobalDynFlags`. Note that this doesn't completely eliminate `unsafeGlobalDynFlags` usage from this bit of the compiler. A few uses are introduced in call-sites where we don't (yet) have ready access to `DynFlags`. Test Plan: Validate Reviewers: goldfire Subscribers: rwbarton, thomie, carter Differential Revision: https://phabricator.haskell.org/D4774
* Implement QuantifiedConstraintsSimon Peyton Jones2018-06-044-54/+103
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We have wanted quantified constraints for ages and, as I hoped, they proved remarkably simple to implement. All the machinery was already in place. The main ticket is Trac #2893, but also relevant are #5927 #8516 #9123 (especially! higher kinded roles) #14070 #14317 The wiki page is https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints which in turn contains a link to the GHC Proposal where the change is specified. Here is the relevant Note: Note [Quantified constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The -XQuantifiedConstraints extension allows type-class contexts like this: data Rose f x = Rose x (f (Rose f x)) instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2 Note the (forall b. Eq b => Eq (f b)) in the instance contexts. This quantified constraint is needed to solve the [W] (Eq (f (Rose f x))) constraint which arises form the (==) definition. Here are the moving parts * Language extension {-# LANGUAGE QuantifiedConstraints #-} and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension * A new form of evidence, EvDFun, that is used to discharge such wanted constraints * checkValidType gets some changes to accept forall-constraints only in the right places. * Type.PredTree gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forall-constraints * Define a type TcRnTypes.QCInst, which holds a given quantified constraint in the inert set * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst], which holds all the Given forall-constraints. In effect, such Given constraints are like local instance decls. * When trying to solve a class constraint, via TcInteract.matchInstEnv, use the InstEnv from inert_insts so that we include the local Given forall-constraints in the lookup. (See TcSMonad.getInstEnvs.) * topReactionsStage calls doTopReactOther for CIrredCan and CTyEqCan, so they can try to react with any given quantified constraints (TcInteract.matchLocalInst) * TcCanonical.canForAll deals with solving a forall-constraint. See Note [Solving a Wanted forall-constraint] Note [Solving a Wanted forall-constraint] * We augment the kick-out code to kick out an inert forall constraint if it can be rewritten by a new type equality; see TcSMonad.kick_out_rewritable Some other related refactoring ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * Move SCC on evidence bindings to post-desugaring, which fixed #14735, and is generally nicer anyway because we can use existing CoreSyn free-var functions. (Quantified constraints made the free-vars of an ev-term a bit more complicated.) * In LookupInstResult, replace GenInst with OneInst and NotSure, using the latter for multiple matches and/or one or more unifiers
* Expand type synonyms when Linting a forallSimon Peyton Jones2018-06-041-1/+3
| | | | | | | | | | | | | | | Trac #14939 showed a type like type Alg cls ob = ob f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b where the kind of the forall looks like (Alg cls *), with a free cls. This tripped up Core Lint. I fixed this by making Core Lint a bit more forgiving, expanding type synonyms if necessary. I'm worried that this might not be the whole story; notably typeKind looks suspect. But it certainly fixes this problem.
* Define MCoercion typeningning2018-05-302-1/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | An attempt on #14975: During compilation, reflexive casts is discarded for computation. Currently in some places we use Maybe coercion as inputs. So if a cast is reflexive it is denoted as Nothing, otherwise Just coercion. This patch defines the type data MCoercion = MRefl | MCo Coercion which is isomorphic to Maybe Coercion but useful in a number of places, and super-helpful documentation. Test Plan: validate Reviewers: bgamari, goldfire, simonpj Reviewed By: goldfire Subscribers: mpickering, rwbarton, thomie, carter GHC Trac Issues: #14975 Differential Revision: https://phabricator.haskell.org/D4699
* Comments about the substition invariantSimon Peyton Jones2018-05-251-32/+43
|
* Clean up the conflicting data family instances error messageRyan Scott2018-05-241-7/+26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: The way we were pretty-printing conflicting data family instances in an error message was far from ideal: 1. If a data type had no constructors, it would print an equals sign with nothing to the right of it. 2. It would try to print GADTs using Haskell98 syntax. 3. It eta-reduced away some type variables from the LHS. This patch addresses these three issues: 1. We no longer print constructors at all in this error message. There's really no reason to do so in the first place, since duplicate data family instances always conflict, regardless of their constructors. 2. Since we no longer print constructors, we no longer have to worry about whether we're using GADT or Haskell98 syntax. 3. I've put in a fix to ensure that type variables are no longer eta-reduced away from the LHS. Test Plan: make test TEST=T14179 Reviewers: goldfire, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #14179 Differential Revision: https://phabricator.haskell.org/D4711
* Add missing check to isReflCoVar_maybeSimon Peyton Jones2018-05-232-5/+7
| | | | | | | | | | | | isReflCoVar_maybe is called, by CoreLint, on all sorts of Vars (tyvars, term vars, coercion vars). But it was silently assuming that it was always called on a CoVar, and as a result could crash fatally. This is the immediate cause of the panic in Trac #15163. It's easy to fix. NB: this does not completely fix Trac #15163; more to come
* Fix #14875 by introducing PprPrec, and using itRyan Scott2018-05-132-19/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Trying to determine when to insert parentheses during TH conversion is a bit of a mess. There is an assortment of functions that try to detect this, such as: * `hsExprNeedsParens` * `isCompoundHsType` * `hsPatNeedsParens` * `isCompoundPat` * etc. To make things worse, each of them have slightly different semantics. Plus, they don't work well in the presence of explicit type signatures, as #14875 demonstrates. All of these problems can be alleviated with the use of an explicit precedence argument (much like what `showsPrec` currently does). To accomplish this, I introduce a new `PprPrec` data type, and define standard predences for things like function application, infix operators, function arrows, and explicit type signatures (that last one is new). I then added `PprPrec` arguments to the various `-NeedsParens` functions, and use them to make smarter decisions about when things need to be parenthesized. A nice side effect is that functions like `isCompoundHsType` are now completely unneeded, since they're simply aliases for `hsTypeNeedsParens appPrec`. As a result, I did a bit of refactoring to remove these sorts of functions. I also did a pass over various utility functions in GHC for constructing AST forms and used more appropriate precedences where convenient. Along the way, I also ripped out the existing `TyPrec` data type (which was tailor-made for pretty-printing `Type`s) and replaced it with `PprPrec` for consistency. Test Plan: make test TEST=T14875 Reviewers: alanz, goldfire, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #14875 Differential Revision: https://phabricator.haskell.org/D4688
* TcInteract: Ensure that tycons have representations before solving for TypeableBen Gamari2018-05-131-1/+5
| | | | | | | | | | | | Summary: This fixes #15067. Test Plan: Validate Subscribers: thomie, carter, RyanGlScott GHC Trac Issues: #15067 Differential Revision: https://phabricator.haskell.org/D4623
* Split TrieMap into a general (TrieMap) and core specific (CoreTrieMap) module.klebinger.andreas@gmx.at2018-05-051-1/+1
| | | | | | | | | | | | | | | | | | Splitting TrieMap into a general and core specific part allows us to define instances for TrieMap without creating a transitive dependency on CoreSyn. Test Plan: ci Reviewers: goldfire, bgamari, simonmar, simonpj Reviewed By: bgamari, simonpj Subscribers: simonpj, nomeata, thomie, carter GHC Trac Issues: #15082 Differential Revision: https://phabricator.haskell.org/D4618
* coercion: Improve debugging outputSimon Peyton Jones2018-04-231-36/+46
| | | | | | | | | | | * Improve assertion-failure message * Add HasDebugCallStack to decomposeFunCo Reviewers: goldfire, bgamari Subscribers: thomie, carter Differential Revision: https://phabricator.haskell.org/D4570
* Caching coercion roles in NthCo and coercionKindsRole refactoringTobias Dammers2018-04-207-269/+379
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | While addressing nonlinear behavior related to coercion roles, particularly `NthCo`, we noticed that coercion roles are recalculated often even though they should be readily at hand already in most cases. This patch adds a `Role` to the `NthCo` constructor so that we can cache them rather than having to recalculate them on the fly. https://ghc.haskell.org/trac/ghc/ticket/11735#comment:23 explains the approach. Performance improvement over GHC HEAD, when compiling Grammar.hs (see below): GHC 8.2.1: ``` ghc Grammar.hs 176.27s user 0.23s system 99% cpu 2:56.81 total ``` before patch (but with other optimizations applied): ``` ghc Grammar.hs -fforce-recomp 175.77s user 0.19s system 100% cpu 2:55.78 total ``` after: ``` ../../ghc/inplace/bin/ghc-stage2 Grammar.hs 10.32s user 0.17s system 98% cpu 10.678 total ``` Introduces the following regressions: - perf/compiler/parsing001 (possibly false positive) - perf/compiler/T9872 - perf/compiler/haddock.base Reviewers: goldfire, bgamari, simonpj Reviewed By: simonpj Subscribers: rwbarton, thomie, carter GHC Trac Issues: #11735 Differential Revision: https://phabricator.haskell.org/D4394
* Remove unused function: mkFunCosMatthew Pickering2018-04-132-7/+1
| | | | | | | | | | Reviewers: goldfire, bgamari, dfeuer Reviewed By: dfeuer Subscribers: dfeuer, thomie, carter Differential Revision: https://phabricator.haskell.org/D4587
* Document SumTyConSimon Jakobi2018-04-071-0/+1
|
* Apply Note [EtaAppCo] in OptCoercion to another caseRichard Eisenberg2018-03-311-3/+2
|
* Apply the interim fix for #14119 to liftCoMatchRichard Eisenberg2018-03-311-1/+7
| | | | Matching in the presence of casts can happen in liftCoMatch, too.
* Track type variable scope more carefully.Richard Eisenberg2018-03-315-24/+63
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main job of this commit is to track more accurately the scope of tyvars introduced by user-written foralls. For example, it would be to have something like this: forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool In that type, a's kind must be k, but k isn't in scope. We had a terrible way of doing this before (not worth repeating or describing here, but see the old tcImplicitTKBndrs and friends), but now we have a principled approach: make an Implication when kind-checking a forall. Doing so then hooks into the existing machinery for preventing skolem-escape, performing floating, etc. This also means that we bump the TcLevel whenever going into a forall. The new behavior is done in TcHsType.scopeTyVars, but see also TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant rewriting. There are several Notes near there to guide you. Of particular interest there is that Implication constraints can now have skolems that are out of order; this situation is reported in TcErrors. A major consequence of this is a slightly tweaked process for type- checking type declarations. The new Note [Use SigTvs in kind-checking pass] in TcTyClsDecls lays it out. The error message for dependent/should_fail/TypeSkolEscape has become noticeably worse. However, this is because the code in TcErrors goes to some length to preserve pre-8.0 error messages for kind errors. It's time to rip off that plaster and get rid of much of the kind-error-specific error messages. I tried this, and doing so led to a lovely error message for TypeSkolEscape. So: I'm accepting the error message quality regression for now, but will open up a new ticket to fix it, along with a larger error-message improvement I've been pondering. This applies also to dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142. Other minor changes: - isUnliftedTypeKind didn't look for tuples and sums. It does now. - check_type used check_arg_type on both sides of an AppTy. But the left side of an AppTy isn't an arg, and this was causing a bad error message. I've changed it to use check_type on the left-hand side. - Some refactoring around when we print (TYPE blah) in error messages. The changes decrease the times when we do so, to good effect. Of course, this is still all controlled by -fprint-explicit-runtime-reps Fixes #14066 #14749 Test cases: dependent/should_compile/{T14066a,T14749}, dependent/should_fail/T14066{,c,d,e,f,g,h}
* Avoid quadratic complexity in typeKindSimon Peyton Jones2018-03-271-1/+10
| | | | | | | | I took 10 minute to fix this potential performance hole (Trac #14263) There are no actual bug reports against it, so no regression test.
* Fix performance of flattener patch (#12919)Alexander Vieth2018-03-264-24/+27
| | | | | | | | | | | This patch, authored by alexvieth and reviewed at D4451, makes performance improvements by critically optimizing parts of the flattener. Summary: T3064, T5321FD, T5321Fun, T9872a, T9872b, T9872c all pass. T9872a and T9872c show improvements beyond the -5% threshold. T9872d fails at 10.9% increased allocations.
* Fix #12919 by making the flattener homegeneous.Richard Eisenberg2018-03-265-185/+328
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This changes a key invariant of the flattener. Previously, flattening a type meant flattening its kind as well. But now, flattening is always homogeneous -- that is, the kind of the flattened type is the same as the kind of the input type. This is achieved by various wizardry in the TcFlatten.flatten_many function, as described in Note [flatten_many]. There are several knock-on effects, including some refactoring in the canonicalizer to take proper advantage of the flattener's changed behavior. In particular, the tyvar case of can_eq_nc' no longer needs to take casts into account. Another effect is that flattening a tyconapp might change it into a casted tyconapp. This might happen if the result kind of the tycon contains a variable, and that variable changes during flattening. Because the flattener is homogeneous, it tacks on a cast to keep the tyconapp kind the same. However, this is problematic when flattening CFunEqCans, which need to have an uncasted tyconapp on the LHS and must remain homogeneous. The solution is a more involved canCFunEqCan, described in Note [canCFunEqCan]. This patch fixes #13643 (as tested in typecheck/should_compile/T13643) and the panic in typecheck/should_compile/T13822 (as reported in #14024). Actually, there were two bugs in T13822: the first was just some incorrect logic in tryFill (part of the unflattener) -- also fixed in this patch -- and the other was the main bug fixed in this ticket. The changes in this patch exposed a long-standing flaw in OptCoercion, in that breaking apart an AppCo sometimes has unexpected effects on kinds. See new Note [EtaAppCo] in OptCoercion, which explains the problem and fix. Also here is a reversion of the major change in 09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion. It turns out that making the flattener homogeneous changes the invariants on the algorithm, making the change in that patch no longer necessary. This patch also fixes: #14038 (dependent/should_compile/T14038) #13910 (dependent/should_compile/T13910) #13938 (dependent/should_compile/T13938) #14441 (typecheck/should_compile/T14441) #14556 (dependent/should_compile/T14556) #14720 (dependent/should_compile/T14720) #14749 (typecheck/should_compile/T14749) Sadly, this patch negatively affects performance of type-family- heavy code. The following patch fixes these performance degradations. However, the performance fixes are somewhat invasive and so I've kept them as a separate patch, labeling this one as [skip ci] so that validation doesn't fail on the performance cases.
* Fix two obscure bugs in rule matchingSimon Peyton Jones2018-03-211-55/+66
| | | | | | | | | | | | | | | | | | | | | | | | | | This patch fixes Trac #14777, a compiler crash. There were actually two bugs. 1. In Rules.matchN, I was (consciously) not rename the template binders of the rule. Sadly, in rare cases an accidental coincidence of uniques could mean that a term variable was mapped to a type variable, utterly bogusly. See "Historical note" in Note [Cloning the template binders] in Rules. This was hard to find, but easy to fix. 2. The fix to (1) showed up a bug in Unify.hs. The test in Unify.tvBindFlag was previously using the domain of the RnEnv2 to detect locally-bound variables (e.g. when unifying under a forall). That's fine when teh RnEnv2 starts empty, as it does in most entry points. But the tcMatchTyKisX entry point, used from the rule matcher, passes in a non-empty RnEnv2 (by design). Now the domain of the RnEnv doesn't idenfity those locally-bound variables any more :-(. Solution: extend UmEnv with a new field um_skols, to capture the skolems directly. Simple, easy, works.
* Fix #14869 by being more mindful of Type vs. ConstraintRyan Scott2018-03-212-27/+50
| | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: Before, we were using `isLiftedTypeKind` in `reifyType` before checking if a type was `Constraint`. But as it turns out, `isLiftedTypeKind` treats `Constraint` the same as `Type`, so every occurrence of `Constraint` would be reified as `Type`! To make things worse, the documentation for `isLiftedTypeKind` stated that it treats `Constraint` //differently// from `Type`, which simply isn't true. This revises the documentation for `isLiftedTypeKind` to reflect reality, and defers the `isLiftedTypeKind` check in `reifyType` so that it does not accidentally swallow `Constraint`. Test Plan: make test TEST=T14869 Reviewers: goldfire, bgamari Reviewed By: goldfire Subscribers: rwbarton, thomie, carter GHC Trac Issues: #14869 Differential Revision: https://phabricator.haskell.org/D4474
* Comments and tiny refactorSimon Peyton Jones2018-03-191-4/+5
| | | | Related to Ryan's upcoming patch for Trac #14933
* Comments onlySimon Peyton Jones2018-02-271-0/+1
|
* Fix a nasty bug in the pure unifierSimon Peyton Jones2018-02-271-26/+33
| | | | | | | | | | | The pure unifier was building an infinite type, through a defective occurs check. So GHC went into an infinite loop. Reason: we were neglecting the 'kco' part of the type, which 'unify_ty' maintains. Yikes. The fix is easy. I refactored a bit to make it harder to go wrong in future.
* Comments in Unify, fixing #12442Richard Eisenberg2018-02-221-0/+46
| | | | [ci skip]
* Comments onlySimon Peyton Jones2018-02-071-0/+4
|
* Optimize coercionKind (Trac #11735)Tobias Dammers2018-01-311-16/+36
| | | | | | | | | | | | Reviewers: simonpj, goldfire, bgamari Reviewed By: simonpj Subscribers: rwbarton, thomie, carter GHC Trac Issues: #11735 Differential Revision: https://phabricator.haskell.org/D4355
View Lorry Controller Status