summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent/should_fail
Commit message (Collapse)AuthorAgeFilesLines
* Improve kind generalisation, error messagesSimon Peyton Jones2020-09-2410-19/+46
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch does two things: * It refactors GHC.Tc.Errors a bit. In debugging Quick Look I was forced to look in detail at error messages, and ended up doing a bit of refactoring, esp in mkTyVarEqErr'. It's still quite a mess, but a bit better, I think. * It makes a significant improvement to the kind checking of type and class declarations. Specifically, we now ensure that if kind checking fails with an unsolved constraint, all the skolems are in scope. That wasn't the case before, which led to some obscure error messages; and occasional failures with "no skolem info" (eg #16245). Both of these, and the main Quick Look patch itself, affect a /lot/ of error messages, as you can see from the number of files changed. I've checked them all; I think they are as good or better than before. Smaller things * I documented the various instances of VarBndr better. See Note [The VarBndr tyep and its uses] in GHC.Types.Var * Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds * A bit of refactoring in bindExplicitTKTele, to avoid the footwork with Either. Simpler now. * Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType Fixes #16245 (comment 211369), memorialised as typecheck/polykinds/T16245a Also fixes the three bugs in #18640
* Remove GADT self-reference check (#11554, #12081, #12174, fixes #15942)Artyom Kuznetsov2020-09-194-19/+1
| | | | Reverts 430f5c84dac1eab550110d543831a70516b5cac8
* Reject nested foralls/contexts in instance types more consistentlyRyan Scott2020-06-304-4/+16
| | | | | | | | | | | | | | | | | | | | | | | | | | | GHC is very wishy-washy about rejecting instance declarations with nested `forall`s or contexts that are surrounded by outermost parentheses. This can even lead to some strange interactions with `ScopedTypeVariables`, as demonstrated in #18240. This patch makes GHC more consistently reject instance types with nested `forall`s/contexts so as to prevent these strange interactions. On the implementation side, this patch tweaks `splitLHsInstDeclTy` and `getLHsInstDeclHead` to not look through parentheses, which can be semantically significant. I've added a `Note [No nested foralls or contexts in instance types]` in `GHC.Hs.Type` to explain why. This also introduces a `no_nested_foralls_contexts_err` function in `GHC.Rename.HsType` to catch nested `forall`s/contexts in instance types. This function is now used in `rnClsInstDecl` (for ordinary instance declarations) and `rnSrcDerivDecl` (for standalone `deriving` declarations), the latter of which fixes #18271. On the documentation side, this adds a new "Formal syntax for instance declaration types" section to the GHC User's Guide that presents a BNF-style grammar for what is and isn't allowed in instance types. Fixes #18240. Fixes #18271.
* Make GADT constructors adhere to the forall-or-nothing rule properlyRyan Scott2020-06-091-6/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Issue #18191 revealed that the types of GADT constructors don't quite adhere to the `forall`-or-nothing rule. This patch serves to clean up this sad state of affairs somewhat. The main change is not in the code itself, but in the documentation, as this patch introduces two sections to the GHC User's Guide: * A "Formal syntax for GADTs" section that presents a BNF-style grammar for what is and isn't allowed in GADT constructor types. This mostly exists to codify GHC's existing behavior, but it also imposes a new restriction that addresses #18191: the outermost `forall` and/or context in a GADT constructor is not allowed to be surrounded by parentheses. Doing so would make these `forall`s/contexts nested, and GADTs do not support nested `forall`s/contexts at present. * A "`forall`-or-nothing rule" section that describes exactly what the `forall`-or-nothing rule is all about. Surprisingly, there was no mention of this anywhere in the User's Guide up until now! To adhere the new specification in the "Formal syntax for GADTs" section of the User's Guide, the following code changes were made: * A new function, `GHC.Hs.Type.splitLHsGADTPrefixTy`, was introduced. This is very much like `splitLHsSigmaTy`, except that it avoids splitting apart any parentheses, which can be syntactically significant for GADT types. See `Note [No nested foralls or contexts in GADT constructors]` in `GHC.Hs.Type`. * `ConDeclGADTPrefixPs`, an extension constructor for `XConDecl`, was introduced so that `GHC.Parser.PostProcess.mkGadtDecl` can return it when given a prefix GADT constructor. Unlike `ConDeclGADT`, `ConDeclGADTPrefixPs` does not split the GADT type into its argument and result types, as this cannot be done until after the type is renamed (see `Note [GADT abstract syntax]` in `GHC.Hs.Decls` for why this is the case). * `GHC.Renamer.Module.rnConDecl` now has an additional case for `ConDeclGADTPrefixPs` that (1) splits apart the full `LHsType` into its `forall`s, context, argument types, and result type, and (2) checks for nested `forall`s/contexts. Step (2) used to be performed the typechecker (in `GHC.Tc.TyCl.badDataConTyCon`) rather than the renamer, but now the relevant code from the typechecker can simply be deleted. One nice side effect of this change is that we are able to give a more accurate error message for GADT constructors that use visible dependent quantification (e.g., `MkFoo :: forall a -> a -> Foo a`), which improves the stderr in the `T16326_Fail6` test case. Fixes #18191. Bumps the Haddock submodule.
* Simplify bindLHsTyVarBndrs and bindHsQTyVarswip/simply-bind-tyvarsRyan Scott2020-06-051-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Both `bindLHsTyVarBndrs` and `bindHsQTyVars` take two separate `Maybe` arguments, which I find terribly confusing. Thankfully, it's possible to remove one `Maybe` argument from each of these functions, which this patch accomplishes: * `bindHsQTyVars` takes a `Maybe SDoc` argument, which is `Just` if GHC should warn about any of the quantified type variables going unused. However, every call site uses `Nothing` in practice. This makes sense, since it doesn't really make sense to warn about unused type variables bound by an `LHsQTyVars`. For instance, you wouldn't warn about the `a` in `data Proxy a = Proxy` going unused. As a result, I simply remove this `Maybe SDoc` argument altogether. * `bindLHsTyVarBndrs` also takes a `Maybe SDoc` argument for the same reasons that `bindHsQTyVars` took one. To make things more confusing, however, `bindLHsTyVarBndrs` also takes a separate `HsDocContext` argument, which is pretty-printed (to an `SDoc`) in warnings and error messages. In practice, the `Maybe SDoc` and the `HsDocContext` often contain the same text. See the call sites for `bindLHsTyVarBndrs` in `rnFamInstEqn` and `rnConDecl`, for instance. There are only a handful of call sites where the text differs between the `Maybe SDoc` and `HsDocContext` arguments: * In `rnHsRuleDecl`, where the `Maybe SDoc` says "`In the rule`" and the `HsDocContext` says "`In the transformation rule`". * In `rnHsTyKi`/`rn_ty`, where the `Maybe SDoc` says "`In the type`" but the `HsDocContext` is inhereted from the surrounding context (e.g., if `rnHsTyKi` were called on a top-level type signature, the `HsDocContext` would be "`In the type signature`" instead) In both cases, warnings/error messages arguably _improve_ by unifying making the `Maybe SDoc`'s text match that of the `HsDocContext`. As a result, I decided to remove the `Maybe SDoc` argument to `bindLHsTyVarBndrs` entirely and simply reuse the text from the `HsDocContext`. (I decided to change the phrase "transformation rule" to "rewrite rule" while I was in the area.) The `Maybe SDoc` argument has one other purpose: signaling when to emit "`Unused quantified type variable`" warnings. To recover this functionality, I replaced the `Maybe SDoc` argument with a boolean-like `WarnUnusedForalls` argument. The only `bindLHsTyVarBndrs` call site that chooses _not_ to emit these warnings in `bindHsQTyVars`.
* Simple subsumptionwip/T17775Simon Peyton Jones2020-06-0511-15/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch simplifies GHC to use simple subsumption. Ticket #17775 Implements GHC proposal #287 https://github.com/ghc-proposals/ghc-proposals/blob/master/ proposals/0287-simplify-subsumption.rst All the motivation is described there; I will not repeat it here. The implementation payload: * tcSubType and friends become noticably simpler, because it no longer uses eta-expansion when checking subsumption. * No deeplyInstantiate or deeplySkolemise That in turn means that some tests fail, by design; they can all be fixed by eta expansion. There is a list of such changes below. Implementing the patch led me into a variety of sticky corners, so the patch includes several othe changes, some quite significant: * I made String wired-in, so that "foo" :: String rather than "foo" :: [Char] This improves error messages, and fixes #15679 * The pattern match checker relies on knowing about in-scope equality constraints, andd adds them to the desugarer's environment using addTyCsDs. But the co_fn in a FunBind was missed, and for some reason simple-subsumption ends up with dictionaries there. So I added a call to addTyCsDs. This is really part of #18049. * I moved the ic_telescope field out of Implication and into ForAllSkol instead. This is a nice win; just expresses the code much better. * There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader. We called checkDataKindSig inside tc_kind_sig, /before/ solveEqualities and zonking. Obviously wrong, easily fixed. * solveLocalEqualitiesX: there was a whole mess in here, around failing fast enough. I discovered a bad latent bug where we could successfully kind-check a type signature, and use it, but have unsolved constraints that could fill in coercion holes in that signature -- aargh. It's all explained in Note [Failure in local type signatures] in GHC.Tc.Solver. Much better now. * I fixed a serious bug in anonymous type holes. IN f :: Int -> (forall a. a -> _) -> Int that "_" should be a unification variable at the /outer/ level; it cannot be instantiated to 'a'. This was plain wrong. New fields mode_lvl and mode_holes in TcTyMode, and auxiliary data type GHC.Tc.Gen.HsType.HoleMode. This fixes #16292, but makes no progress towards the more ambitious #16082 * I got sucked into an enormous refactoring of the reporting of equality errors in GHC.Tc.Errors, especially in mkEqErr1 mkTyVarEqErr misMatchMsg misMatchMsgOrCND In particular, the very tricky mkExpectedActualMsg function is gone. It took me a full day. But the result is far easier to understand. (Still not easy!) This led to various minor improvements in error output, and an enormous number of test-case error wibbles. One particular point: for occurs-check errors I now just say Can't match 'a' against '[a]' rather than using the intimidating language of "occurs check". * Pretty-printing AbsBinds Tests review * Eta expansions T11305: one eta expansion T12082: one eta expansion (undefined) T13585a: one eta expansion T3102: one eta expansion T3692: two eta expansions (tricky) T2239: two eta expansions T16473: one eta determ004: two eta expansions (undefined) annfail06: two eta (undefined) T17923: four eta expansions (a strange program indeed!) tcrun035: one eta expansion * Ambiguity check at higher rank. Now that we have simple subsumption, a type like f :: (forall a. Eq a => Int) -> Int is no longer ambiguous, because we could write g :: (forall a. Eq a => Int) -> Int g = f and it'd typecheck just fine. But f's type is a bit suspicious, and we might want to consider making the ambiguity check do a check on each sub-term. Meanwhile, these tests are accepted, whereas they were previously rejected as ambiguous: T7220a T15438 T10503 T9222 * Some more interesting error message wibbles T13381: Fine: one error (Int ~ Exp Int) rather than two (Int ~ Exp Int, Exp Int ~ Int) T9834: Small change in error (improvement) T10619: Improved T2414: Small change, due to order of unification, fine T2534: A very simple case in which a change of unification order means we get tow unsolved constraints instead of one tc211: bizarre impredicative tests; just accept this for now Updates Cabal and haddock submodules. Metric Increase: T12150 T12234 T5837 haddock.base Metric Decrease: haddock.compiler haddock.Cabal haddock.base Merge note: This appears to break the `UnliftedNewtypesDifficultUnification` test. It has been marked as broken in the interest of merging. (cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)
* Revert "Specify kind variables for inferred kinds in base."Ben Gamari2020-05-251-2/+2
| | | | | | | | As noted in !3132, this has rather severe knock-on consequences in user-code. We'll need to revisit this before merging something along these lines. This reverts commit 9749fe1223d182b1f8e7e4f7378df661c509f396.
* Specify kind variables for inferred kinds in base.Baldur Blöndal2020-05-081-2/+2
|
* Modules: type-checker (#13009)Sylvain Henry2020-04-071-1/+1
| | | | Update Haddock submodule
* Simplify treatment of heterogeneous equalityRichard Eisenberg2020-03-203-16/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for a unification. But we needn't do this. Instead, we now spit out a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original Wanted. This means that we retain the connection between the spat-out constraint and the original. The problem with this new approach is that we cannot use the casted equality for substitution; it's too like wanteds-rewriting- wanteds. So, we forbid CTyEqCans that mention coercion holes. All the details are in Note [Equalities with incompatible kinds] in TcCanonical. There are a few knock-on effects, documented where they occur. While debugging an error in this patch, Simon and I ran into infelicities in how patterns and matches are printed; we made small improvements. This patch includes mitigations for #17828, which causes spurious pattern-match warnings. When #17828 is fixed, these lines should be removed.
* Always display inferred variables using bracesKrzysztof Gogolewski2020-02-126-6/+6
| | | | | | | | | | | | | We now always show "forall {a}. T" for inferred variables, previously this was controlled by -fprint-explicit-foralls. This implements part 1 of https://github.com/ghc-proposals/ghc-proposals/pull/179. Part of GHC ticket #16320. Furthermore, when printing a levity restriction error, we now display the HsWrap of the expression. This lets users see the full elaboration with -fprint-typechecker-elaboration (see also #17670)
* Do not bring visible foralls into scope in hsScopedTvswip/T17687Ryan Scott2020-01-253-0/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, `hsScopedTvs` (and its cousin `hsWcScopedTvs`) pretended that visible dependent quantification could not possibly happen at the term level, and cemented that assumption with an `ASSERT`: ```hs hsScopedTvs (HsForAllTy { hst_fvf = vis_flag, ... }) = ASSERT( vis_flag == ForallInvis ) ... ``` It turns out that this assumption is wrong. You can end up tripping this `ASSERT` if you stick it to the man and write a type for a term that uses visible dependent quantification anyway, like in this example: ```hs {-# LANGUAGE ScopedTypeVariables #-} x :: forall a -> a -> a x = x ``` That won't typecheck, but that's not the point. Before the typechecker has a chance to reject this, the renamer will try to use `hsScopedTvs` to bring `a` into scope over the body of `x`, since `a` is quantified by a `forall`. This, in turn, causes the `ASSERT` to fail. Bummer. Instead of walking on this dangerous ground, this patch makes GHC adopt a more hardline stance by pattern-matching directly on `ForallInvis` in `hsScopedTvs`: ```hs hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ... ``` Now `a` will not be brought over the body of `x` at all (which is how it should be), there's no chance of the `ASSERT` failing anymore (as it's gone), and best of all, the behavior of `hsScopedTvs` does not change. Everyone wins! Fixes #17687.
* Don't zap to Any; error insteadRichard Eisenberg2020-01-1210-4/+104
| | | | | | | | | This changes GHC's treatment of so-called Naughty Quantification Candidates to issue errors, instead of zapping to Any. Close #16775. No new test cases, because existing ones cover this well.
* Warn on inferred polymorphic recursionRichard Eisenberg2019-12-118-0/+78
| | | | | | | | | | | Silly users sometimes try to use visible dependent quantification and polymorphic recursion without a CUSK or SAK. This causes unexpected errors. So we now adjust expectations with a bit of helpful messaging. Closes #17541 and closes #17131. test cases: dependent/should_fail/T{17541{,b},17131}
* Strip parentheses in expressions contexts in error messagesVladislav Zavialov2019-11-191-1/+1
| | | | This makes error messages a tad less noisy.
* Testsuite tweaks and refactoringÖmer Sinan Ağacan2019-07-091-1/+1
| | | | | | | | | | | | | | | | - Rename requires_th to req_th for consistency with other req functions (e.g. req_interp, req_profiling etc.) - req_th (previously requires_th) now checks for interpreter (via req_interp). With this running TH tests are skipped when running the test suite with stage=1. - Test tweaks: - T9360a, T9360b: Use req_interp - recomp009, T13938, RAE_T32a: Use req_th - Fix check-makefiles linter: it now looks for Makefiles instead of .T files (which are actually Python files)
* Improve error recovery in the typecheckerSimon Peyton Jones2019-03-168-12/+57
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Issue #16418 showed that we were carrying on too eagerly after a bogus type signature was identified (a bad telescope in fact), leading to a subsequent crash. This led me in to a maze of twisty little passages in the typechecker's error recovery, and I ended up doing some refactoring in TcRnMonad. Some specfifics * TcRnMonad.try_m is now called attemptM. * I switched the order of the result pair in tryTc, to make it consistent with other similar functions. * The actual exception used in the Tc monad is irrelevant so, to avoid polluting type signatures, I made tcTryM, a simple wrapper around tryM, and used it. The more important changes are in * TcSimplify.captureTopConstraints, where we should have been calling simplifyTop rather than reportUnsolved, so that levity defaulting takes place properly. * TcUnify.emitResidualTvConstraint, where we need to set the correct status for a new implication constraint. (Previously we ended up with an Insoluble constraint wrapped in an Unsolved implication, which meant that insolubleWC gave the wrong answer.
* Stop inferring over-polymorphic kindsSimon Peyton Jones2019-03-095-0/+33
| | | | | | | | | | | | | | | | | | | | | | | | | | | Before this patch GHC was trying to be too clever (Trac #16344); it succeeded in kind-checking this polymorphic-recursive declaration data T ka (a::ka) b = MkT (T Type Int Bool) (T (Type -> Type) Maybe Bool) As Note [No polymorphic recursion] discusses, the "solution" was horribly fragile. So this patch deletes the key lines in TcHsType, and a wodge of supporting stuff in the renamer. There were two regressions, both the same: a closed type family decl like this (T12785b) does not have a CUSK: type family Payload (n :: Peano) (s :: HTree n x) where Payload Z (Point a) = a Payload (S n) (a `Branch` stru) = a To kind-check the equations we need a dependent kind for Payload, and we don't get that any more. Solution: make it a CUSK by giving the result kind -- probably a good thing anyway. The other case (T12442) was very similar: a close type family declaration without a CUSK.
* Fix #16391 by using occCheckExpand in TcValidityRyan Scott2019-03-073-0/+18
| | | | | | | | | | | | | The type-variables-escaping-their-scope-via-kinds check in `TcValidity` was failing to properly expand type synonyms, which led to #16391. This is easily fixed by using `occCheckExpand` before performing the validity check. Along the way, I refactored this check out into its own function, and sprinkled references to Notes to better explain all of the moving parts. Many thanks to @simonpj for the suggestions. Bumps the haddock submodule.
* Visible dependent quantificationRyan Scott2019-03-0126-5/+213
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This implements GHC proposal 35 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst) by adding the ability to write kinds with visible dependent quantification (VDQ). Most of the work for supporting VDQ was actually done _before_ this patch. That is, GHC has been able to reason about kinds with VDQ for some time, but it lacked the ability to let programmers directly write these kinds in the source syntax. This patch is primarly about exposing this ability, by: * Changing `HsForAllTy` to add an additional field of type `ForallVisFlag` to distinguish between invisible `forall`s (i.e, with dots) and visible `forall`s (i.e., with arrows) * Changing `Parser.y` accordingly The rest of the patch mostly concerns adding validity checking to ensure that VDQ is never used in the type of a term (as permitting this would require full-spectrum dependent types). This is accomplished by: * Adding a `vdqAllowed` predicate to `TcValidity`. * Introducing `splitLHsSigmaTyInvis`, a variant of `splitLHsSigmaTy` that only splits invisible `forall`s. This function is used in certain places (e.g., in instance declarations) to ensure that GHC doesn't try to split visible `forall`s (e.g., if it tried splitting `instance forall a -> Show (Blah a)`, then GHC would mistakenly allow that declaration!) This also updates Template Haskell by introducing a new `ForallVisT` constructor to `Type`. Fixes #16326. Also fixes #15658 by documenting this feature in the users' guide.
* Treat kind/type variables identically, demolish FKTVVladislav Zavialov2019-02-277-7/+28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst Fixes Trac #16334, Trac #16315 With this patch, scoping rules for type and kind variables have been unified: kind variables no longer receieve special treatment. This simplifies both the language and the implementation. User-facing changes ------------------- * Kind variables are no longer implicitly quantified when an explicit forall is used: p :: Proxy (a :: k) -- still accepted p :: forall k a. Proxy (a :: k) -- still accepted p :: forall a. Proxy (a :: k) -- no longer accepted In other words, now we adhere to the "forall-or-nothing" rule more strictly. Related function: RnTypes.rnImplicitBndrs * The -Wimplicit-kind-vars warning has been deprecated. * Kind variables are no longer implicitly quantified in constructor declarations: data T a = T1 (S (a :: k) | forall (b::k). T2 (S b) -- no longer accepted data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b) -- still accepted Related function: RnTypes.extractRdrKindSigVars * Implicitly quantified kind variables are no longer put in front of other variables: f :: Proxy (a :: k) -> Proxy (b :: j) f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b -- old order f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -- new order This is a breaking change for users of TypeApplications. Note that we still respect the dpendency order: 'k' before 'a', 'j' before 'b'. See "Ordering of specified variables" in the User's Guide. Related function: RnTypes.rnImplicitBndrs * In type synonyms and type family equations, free variables on the RHS are no longer implicitly quantified unless used in an outermost kind annotation: type T = Just (Nothing :: Maybe a) -- no longer accepted type T = Just Nothing :: Maybe (Maybe a) -- still accepted The latter form is a workaround due to temporary lack of an explicit quantification method. Ideally, we would write something along these lines: type T @a = Just (Nothing :: Maybe a) Related function: RnTypes.extractHsTyRdrTyVarsKindVars * Named wildcards in kinds are fixed (Trac #16334): x :: (Int :: _t) -- this compiles, infers (_t ~ Type) Related function: RnTypes.partition_nwcs Implementation notes -------------------- * One of the key changes is the removal of FKTV in RnTypes: - data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName] - , fktv_tys :: [Located RdrName] } + type FreeKiTyVars = [Located RdrName] We used to keep track of type and kind variables separately, but now that they are on equal footing when it comes to scoping, we can put them in the same list. * extract_lty and family are no longer parametrized by TypeOrKind, as we now do not distinguish kind variables from type variables. * PatSynExPE and the related Note [Pattern synonym existentials do not scope] have been removed (Trac #16315). With no implicit kind quantification, we can no longer trigger the error. * reportFloatingKvs and the related Note [Free-floating kind vars] have been removed. With no implicit kind quantification, we can no longer trigger the error.
* Add AnonArgFlag to FunTySimon Peyton Jones2019-02-232-5/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The big payload of this patch is: Add an AnonArgFlag to the FunTy constructor of Type, so that (FunTy VisArg t1 t2) means (t1 -> t2) (FunTy InvisArg t1 t2) means (t1 => t2) The big payoff is that we have a simple, local test to make when decomposing a type, leading to many fewer calls to isPredTy. To me the code seems a lot tidier, and probably more efficient (isPredTy has to take the kind of the type). See Note [Function types] in TyCoRep. There are lots of consequences * I made FunTy into a record, so that it'll be easier when we add a linearity field, something that is coming down the road. * Lots of code gets touched in a routine way, simply because it pattern matches on FunTy. * I wanted to make a pattern synonym for (FunTy2 arg res), which picks out just the argument and result type from the record. But alas the pattern-match overlap checker has a heart attack, and either reports false positives, or takes too long. In the end I gave up on pattern synonyms. There's some commented-out code in TyCoRep that shows what I wanted to do. * Much more clarity about predicate types, constraint types and (in particular) equality constraints in kinds. See TyCoRep Note [Types for coercions, predicates, and evidence] and Note [Constraints in kinds]. This made me realise that we need an AnonArgFlag on AnonTCB in a TyConBinder, something that was really plain wrong before. See TyCon Note [AnonTCB InivsArg] * When building function types we must know whether we need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy). This turned out to be pretty easy in practice. * Pretty-printing of types, esp in IfaceType, gets tidier, because we were already recording the (->) vs (=>) distinction in an ad-hoc way. Death to IfaceFunTy. * mkLamType needs to keep track of whether it is building (t1 -> t2) or (t1 => t2). See Type Note [mkLamType: dictionary arguments] Other minor stuff * Some tidy-up in validity checking involving constraints; Trac #16263
* Fix tests which were made to pass by "Make a smart mkAppTyM"Matthew Pickering2019-02-161-1/+1
| | | | | | | | | For some reason gitlab is not reporting these as failures in CI. It's not clear to me why as the junit output looks fine. Fixes #16112 and #16113 They were fixed by 682783828275cca5fd8bf5be5b52054c75e0e22c
* Fail fast in solveLocalEqualitiesSimon Peyton Jones2019-02-141-16/+0
| | | | | | | | | | | | | | | | | | This patch makes us fail fast in TcSimplify.solveLocalEqualities, and in TcHsType.tc_hs_sig_type, if there are insoluble constraints. Previously we ploughed on even if there were insoluble constraints, leading to a cascade of hard-to-understand type errors. Failing eagerly is much better; hence a lot of testsuite error message changes. Eg if we have f :: [Maybe] -> blah f xs = e then trying typecheck 'f x = e' with an utterly bogus type is just asking for trouble. I can't quite remember what provoked me to make this change, but I think the error messages are notably improved, by removing confusing clutter and focusing on the real error.
* testsuite: Mark T11334b as broken in debugged compilerBen Gamari2019-02-071-1/+1
| | | | As noted in #16112.
* Fix #15954 by rejigging check_type's orderRyan Scott2018-12-032-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: Previously, `check_type` (which catches illegal uses of unsaturated type synonyms without enabling `LiberalTypeSynonyms`, among other things) always checks for uses of polytypes before anything else. There is a problem with this plan, however: checking for polytypes requires decomposing `forall`s and other invisible arguments, an action which itself expands type synonyms! Therefore, if we have something like: ```lang=haskell type A a = Int type B (a :: Type -> Type) = forall x. x -> x type C = B A ``` Then when checking `B A`, `A` will get expanded to `forall x. x -> x` before `check_type` has an opportunity to realize that `A` is an unsaturated type synonym! This is the root cause of #15954. This patch fixes the issue by moving the case of `check_type` that detects polytypes to be //after// the case that checks for `TyConApp`s. That way, the `TyConApp` case will properly flag things like the unsaturated use of `A` in the example above before we ever attempt to check for polytypes. Test Plan: make test TEST=T15954 Reviewers: simonpj, bgamari, goldfire Reviewed By: simonpj Subscribers: rwbarton, carter GHC Trac Issues: #15954 Differential Revision: https://phabricator.haskell.org/D5402
* Taming the Kind Inference MonsterSimon Peyton Jones2018-11-2910-74/+47
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | My original goal was (Trac #15809) to move towards using level numbers as the basis for deciding which type variables to generalise, rather than searching for the free varaibles of the environment. However it has turned into a truly major refactoring of the kind inference engine. Let's deal with the level-numbers part first: * Augment quantifyTyVars to calculate the type variables to quantify using level numbers, and compare the result with the existing approach. That is; no change in behaviour, just a WARNing if the two approaches give different answers. * To do this I had to get the level number right when calling quantifyTyVars, and this entailed a bit of care, especially in the code for kind-checking type declarations. * However, on the way I was able to eliminate or simplify a number of calls to solveEqualities. This work is incomplete: I'm not /using/ level numbers yet. When I subsequently get rid of any remaining WARNings in quantifyTyVars, that the level-number answers differ from the current answers, then I can rip out the current "free vars of the environment" stuff. Anyway, this led me into deep dive into kind inference for type and class declarations, which is an increasingly soggy part of GHC. Richard already did some good work recently in commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 Date: Thu Sep 13 09:56:02 2018 +0200 Finish fix for #14880. The real change that fixes the ticket is described in Note [Naughty quantification candidates] in TcMType. but I kept turning over stones. So this patch has ended up with a pretty significant refactoring of that code too. Kind inference for types and classes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * Major refactoring in the way we generalise the inferred kind of a TyCon, in kcTyClGroup. Indeed, I made it into a new top-level function, generaliseTcTyCon. Plus a new Note to explain it Note [Inferring kinds for type declarations]. * We decided (Trac #15592) not to treat class type variables specially when dealing with Inferred/Specified/Required for associated types. That simplifies things quite a bit. I also rewrote Note [Required, Specified, and Inferred for types] * Major refactoring of the crucial function kcLHsQTyVars: I split it into kcLHsQTyVars_Cusk and kcLHsQTyVars_NonCusk because the two are really quite different. The CUSK case is almost entirely rewritten, and is much easier because of our new decision not to treat the class variables specially * I moved all the error checks from tcTyClTyVars (which was a bizarre place for it) into generaliseTcTyCon and/or the CUSK case of kcLHsQTyVars. Now tcTyClTyVars is extremely simple. * I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed now there is no difference between tcImplicitTKBndrs and kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs. Same for kc/tcExplicitTKBndrs. None of them monkey with level numbers, nor build implication constraints. scopeTyVars is gone entirely, as is kcLHsQTyVarBndrs. It's vastly simpler. I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of the bnew bindExplicitTKBndrs. Quantification ~~~~~~~~~~~~~~ * I now deal with the "naughty quantification candidates" of the previous patch in candidateQTyVars, rather than in quantifyTyVars; see Note [Naughty quantification candidates] in TcMType. I also killed off closeOverKindsCQTvs in favour of the same strategy that we use for tyCoVarsOfType: namely, close over kinds at the occurrences. And candidateQTyVars no longer needs a gbl_tvs argument. * Passing the ContextKind, rather than the expected kind itself, to tc_hs_sig_type_and_gen makes it easy to allocate the expected result kind (when we are in inference mode) at the right level. Type families ~~~~~~~~~~~~~~ * I did a major rewrite of the impenetrable tcFamTyPats. The result is vastly more comprehensible. * I got rid of kcDataDefn entirely, quite a big function. * I re-did the way that checkConsistentFamInst works, so that it allows alpha-renaming of invisible arguments. * The interaction of kind signatures and family instances is tricky. Type families: see Note [Apparently-nullary families] Data families: see Note [Result kind signature for a data family instance] and Note [Eta-reduction for data families] * The consistent instantation of an associated type family is tricky. See Note [Checking consistent instantiation] and Note [Matching in the consistent-instantation check] in TcTyClsDecls. It's now checked in TcTyClsDecls because that is when we have the relevant info to hand. * I got tired of the compromises in etaExpandFamInst, so I did the job properly by adding a field cab_eta_tvs to CoAxBranch. See Coercion.etaExpandCoAxBranch. tcInferApps and friends ~~~~~~~~~~~~~~~~~~~~~~~ * I got rid of the mysterious and horrible ClsInstInfo argument to tcInferApps, checkExpectedKindX, and various checkValid functions. It was horrible! * I got rid of [Type] result of tcInferApps. This list was used only in tcFamTyPats, when checking the LHS of a type instance; and if there is a cast in the middle, the list is meaningless. So I made tcInferApps simpler, and moved the complexity (not much) to tcInferApps. Result: tcInferApps is now pretty comprehensible again. * I refactored the many function in TcMType that instantiate skolems. Smaller things * I rejigged the error message in checkValidTelescope; I think it's quite a bit better now. * checkValidType was not rejecting constraints in a kind signature forall (a :: Eq b => blah). blah2 That led to further errors when we then do an ambiguity check. So I make checkValidType reject it more aggressively. * I killed off quantifyConDecl, instead calling kindGeneralize directly. * I fixed an outright bug in tyCoVarsOfImplic, where we were not colleting the tyvar of the kind of the skolems * Renamed ClsInstInfo to AssocInstInfo, and made it into its own data type * Some fiddling around with pretty-printing of family instances which was trickier than I thought. I wanted wildcards to print as plain "_" in user messages, although they each need a unique identity in the CoAxBranch. Some other oddments * Refactoring around the trace messages from reportUnsolved. * A bit of extra tc-tracing in TcHsSyn.commitFlexi This patch fixes a raft of bugs, and includes tests for them. * #14887 * #15740 * #15764 * #15789 * #15804 * #15817 * #15870 * #15874 * #15881
* Overhaul -fprint-explicit-kinds to use VKARyan Scott2018-11-221-2/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch changes the behavior of `-fprint-explicit-kinds` so that it displays kind argument using visible kind application. In other words, the flag now: 1. Prints instantiations of specified variables with `@(...)`. 2. Prints instantiations of inferred variables with `@{...}`. In addition, this patch removes the `Use -fprint-explicit-kinds to see the kind arguments` error message that often arises when a type mismatch occurs due to different kinds. Instead, whenever there is a kind mismatch, we now enable the `-fprint-explicit-kinds` flag locally to help cue to the programmer where the error lies. (See `Note [Kind arguments in error messages]` in `TcErrors`.) As a result, these funny `@{...}` things can now appear to the user even without turning on the `-fprint-explicit-kinds` flag explicitly, so I took the liberty of documenting them in the users' guide. Test Plan: ./validate Reviewers: goldfire, simonpj, bgamari Reviewed By: simonpj Subscribers: rwbarton, carter GHC Trac Issues: #15871 Differential Revision: https://phabricator.haskell.org/D5314
* Smarter HsType pretty-print for promoted dataconsSimon Peyton Jones2018-11-152-5/+5
| | | | | | | | | | | | | | | | | | | | | Fix Trac #15898, by being smarter about when to print a space before a promoted data constructor, in a HsType. I had to implement a mildly tiresome function HsType.lhsTypeHasLeadingPromotionQuote It has multiple cases, of course, but it's very simple. The patch improves the error-message output in a bunch of cases, and (to my surprise) actually fixes a bug in the output of T14343 (Trac #14343), thus - In the expression: _ :: Proxy '('( 'True, 'False), 'False) + In the expression: _ :: Proxy '( '( 'True, 'False), 'False) I discovered that there were two copies of the PromotionFlag type (a boolean, with helpfully named data cons), one in IfaceType and one in HsType. So I combined into one, PromotionFlag, and moved it to BasicTypes. That's why quite a few files are touched, but it's all routine.
* Actually add test for #15859.Richard Eisenberg2018-11-051-0/+13
| | | | Oops. Forgot to `git add`.
* Fix #15859 by checking, not assuming, an ArgFlagRichard Eisenberg2018-11-052-0/+7
| | | | | | | | We thought that visible dependent quantification was impossible in terms, but Iceland Jack discovered otherwise in #15859. This fixes an ASSERT failure that arose. test case: dependent/should_fail/T15859
* Test #15825 in dependent/should_fail/T15825Richard Eisenberg2018-10-293-0/+20
|
* Finish fix for #14880.Tobias Dammers2018-10-2815-33/+102
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The real change that fixes the ticket is described in Note [Naughty quantification candidates] in TcMType. Fixing this required reworking candidateQTyVarsOfType, the function that extracts free variables as candidates for quantification. One consequence is that we now must be more careful when quantifying: any skolems around must be quantified manually, and quantifyTyVars will now only quantify over metavariables. This makes good sense, as skolems are generally user-written and are listed in the AST. As a bonus, we now have more control over the ordering of such skolems. Along the way, this commit fixes #15711 and refines the fix to #14552 (by accepted a program that was previously rejected, as we can now accept that program by zapping variables to Any). This commit also does a fair amount of rejiggering kind inference of datatypes. Notably, we now can skip the generalization step in kcTyClGroup for types with CUSKs, because we get the kind right the first time. This commit also thus fixes #15743 and #15592, which both concern datatype kind generalisation. (#15591 is also very relevant.) For this aspect of the commit, see Note [Required, Specified, and Inferred in types] in TcTyClsDecls. Test cases: dependent/should_fail/T14880{,-2}, dependent/should_fail/T15743[cd] dependent/should_compile/T15743{,e} ghci/scripts/T15743b polykinds/T15592 dependent/should_fail/T15591[bc] ghci/scripts/T15591
* Better error reporting for inaccessible codeSimon Peyton Jones2018-08-241-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch fixes Trac #15558. There turned out to be two distinct problems * In TcExpr.tc_poly_expr_nc we had tc_poly_expr_nc (L loc expr) res_ty = do { traceTc "tcPolyExprNC" (ppr res_ty) ; (wrap, expr') <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty -> setSrcSpan loc $ -- NB: setSrcSpan *after* skolemising, -- so we get better skolem locations tcExpr expr res_ty Putting the setSrcSpan inside the tcSkolemise means that the location on the Implication constraint is the /call/ to the function rather than the /argument/ to the call, and that is really quite wrong. I don't know what Richard's comment NB means -- I moved the setSrcSpan outside, and the "binding site" info in error messages actually improved. The reason I found this is that it affects the span reported for Trac #15558. * In TcErrors.mkGivenErrorReporter we carefully munge the location for an insoluble Given constraint (Note [Inaccessible code]). But the 'implic' passed in wasn't necesarily the immediately- enclosing implication -- but for location-munging purposes it jolly well should be. Solution: use the innermost implication. This actually simplifies the code -- no need to pass an implication in to mkGivenErrorReporter.
* Remove decideKindGeneralisationPlanRichard Eisenberg2018-08-027-35/+56
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | TypeInType came with a new function: decideKindGeneralisationPlan. This type-level counterpart to the term-level decideGeneralisationPlan chose whether or not a kind should be generalized. The thinking was that if `let` should not be generalized, then kinds shouldn't either (under the same circumstances around -XMonoLocalBinds). However, this is too conservative -- the situation described in the motivation for "let should be be generalized" does not occur in types. This commit thus removes decideKindGeneralisationPlan, always generalizing. One consequence is that tc_hs_sig_type_and_gen no longer calls solveEqualities, which reports all unsolved constraints, instead relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect of this is that reporing kind errors gets delayed more frequently. This seems to be a net benefit in error reporting; often, alongside a kind error, the type error is now reported (and users might find type errors easier to understand). Some of these errors ended up at the top level, where it was discovered that the GlobalRdrEnv containing the definitions in the local module was not in the TcGblEnv, and thus errors were reported with qualified names unnecessarily. This commit rejiggers some of the logic around captureTopConstraints accordingly. One error message (typecheck/should_fail/T1633) is a regression, mentioning the name of a default method. However, that problem is already reported as #10087, its solution is far from clear, and so I'm not addressing it here. This commit fixes #15141. As it's an internal refactor, there is no concrete test case for it. Along the way, we no longer need the hsib_closed field of HsImplicitBndrs (it was used only in decideKindGeneralisationPlan) and so it's been removed, simplifying the datatype structure. Along the way, I removed code in the validity checker that looks at coercions. This isn't related to this patch, really (though it was, at one point), but it's an improvement, so I kept it. This updates the haddock submodule.
* Remove the type-checking knot.Richard Eisenberg2018-08-013-1/+27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 decompsePiCos and visible type applicationSimon Peyton Jones2018-07-103-0/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Fix #15308 by suppressing invisble args more rigorouslyRyan Scott2018-07-053-0/+18
| | | | | | | | | | | | | | | | | | | | | | | Summary: There was a buglet in `stripInvisArgs` (which is part of the pretty-printing pipeline for types) in which only invisble arguments which came before any visible arguments would be suppressed, but any invisble arguments that came //after// visible ones would still be printed, even if `-fprint-explicit-kinds` wasn't enabled. The fix is simple: make `stripInvisArgs` recursively process the remaining types even after a visible argument is encountered. Test Plan: make test TEST=T15308 Reviewers: goldfire, bgamari Reviewed By: bgamari Subscribers: simonpj, rwbarton, thomie, carter GHC Trac Issues: #15308 Differential Revision: https://phabricator.haskell.org/D4891
* Remove accidentally checked-in T14845.stderrRyan Scott2018-06-171-7/+0
| | | | | This was a stderr file for a WIP test in D4728. I ended up removing the test, but forgot to remove the stderr file.
* Provide a better error message for unpromotable data constructor contextsRyan Scott2018-06-1710-2/+86
| | | | | | | | | | | | | | | | | | | | | Trac #14845 brought to light a corner case where a data constructor could not be promoted (even with `-XTypeInType`) due to an unpromotable constraint in its context. However, the error message was less than helpful, so this patch adds an additional check to `tcTyVar` catch unpromotable data constructors like these //before// they're promoted, and to give a sensible error message in such cases. Test Plan: make test TEST="T13895 T14845" Reviewers: simonpj, goldfire, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #13895, #14845 Differential Revision: https://phabricator.haskell.org/D4728
* Make better "fake tycons" in error recoverySimon Peyton Jones2018-06-153-0/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Consider (Trac #15215) data T a = MkT ... data S a = ...T...MkT.... If there is an error in the definition of 'T' we add a "fake type constructor" to the type environment, so that we can continue to typecheck 'S'. But we /were not/ adding a fake anything for 'MkT' and so there was an internal error when we met 'MkT' in the body of 'S'. The fix is to add fake tycons for all the 'implicits' of 'T'. This is done by mk_fake_tc in TcTyClsDecls.checkValidTyCl, which now returns a /list/ of TyCons rather than just one. On the way I did some refactoring: * Rename TcTyDecls.tcAddImplicits to tcAddTyConsToGblEnv and make it /include/ the TyCons themeselves as well as their implicits * Some incidental refactoring about tcRecSelBinds. The main thing is that I've avoided creating a HsValBinds that we immediately decompose. That meant moving some deck chairs around. NB: The new error message for the regression test T15215 has the opaque error "Illegal constraint in a type:", flagged in Trac #14845. But that's the fault of the latter ticket. The fix here not to blame.
* Embrace -XTypeInType, add -XStarIsTypeVladislav Zavialov2018-06-1436-72/+76
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Orient TyVar/TyVar equalities with deepest on the leftSimon Peyton Jones2018-05-181-5/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Trac #15009 showed that, for Given TyVar/TyVar equalities, we really want to orient them with the deepest-bound skolem on the left. As it happens, we also want to do the same for Wanteds, but for a different reason (more likely to be touchable). Either way, deepest wins: see TcUnify Note [Deeper level on the left]. This observation led me to some significant changes: * A SkolemTv already had a TcLevel, but the level wasn't really being used. Now it is! * I updated added invariant (SkolInf) to TcType Note [TcLevel and untouchable type variables], documenting that the level number of all the ic_skols should be the same as the ic_tclvl of the implication * FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of zero, which messed the scheme up. Now they get a level number the same way as all other TcTyVars, instead of being a special case. * To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which was previously done via their magic zero level) isTouchableMetaTyVar just tests for those two cases. * TcUnify.swapOverTyVars is the crucial orientation function; see the new Note [TyVar/TyVar orientation]. I completely rewrote this function, and it's now much much easier to understand. I ended up doing some related refactoring, of course * I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing a lot of useless work in the case where there are no skolems; I added a fast-patch * Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of the higher-order parameter to tcExpliciTKBndrsX. * Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints, by analogy with TcUnify.checkConstraints. * Inline TcUnify.buildImplication into its only call-site in TcUnify.checkConstraints * TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a simpler API * Now that we have NoEvBindsVar we have no need of termEvidenceAllowed; nuke the latter, adding Note [No evidence bindings] to TcEvidence.
* Track type variable scope more carefully.Richard Eisenberg2018-03-3124-30/+193
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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}
* Fix #12919 by making the flattener homegeneous.Richard Eisenberg2018-03-262-14/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Typofixes [ci skip]Gabor Greif2017-07-301-1/+1
|
* Add regression tests for #13601, #13780, #13877Ryan Scott2017-07-288-0/+106
| | | | | | | | | | | | | | | | | | | | | | Summary: Some recent commits happened to fix other issues: * c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780 * 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877 Let's add regression tests for each of these to ensure they stay fixed. Test Plan: make test TEST="T13601 T13780a T13780c T13877" Reviewers: goldfire, bgamari, austin Reviewed By: bgamari Subscribers: rwbarton, thomie GHC Trac Issues: #13601, #13780, #13877 Differential Revision: https://phabricator.haskell.org/D3794
* Improve error messages around kind mismatches.Richard Eisenberg2017-07-273-6/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, when canonicalizing (or unifying, in uType) a heterogeneous equality, we emitted a kind equality and used the resulting coercion to cast one side of the heterogeneous equality. While sound, this led to terrible error messages. (See the bugs listed below.) The problem is that using the coercion built from the emitted kind equality is a bit like a wanted rewriting a wanted. The solution is to keep heterogeneous equalities as irreducible. See Note [Equalities with incompatible kinds] in TcCanonical. This commit also removes a highly suspicious switch to FM_SubstOnly when flattening in the kinds of a type variable. I have no idea why this was there, other than as a holdover from pre-TypeInType. I've not left a Note because there is simply no reason I can conceive of that the FM_SubstOnly should be there. One challenge with this patch is that the emitted derived equalities might get emitted several times: when a heterogeneous equality is in an implication and then gets floated out from the implication, the Derived is present both in and out of the implication. This causes a duplicate error message. (Test case: typecheck/should_fail/T7368) Solution: track the provenance of Derived constraints and refuse to float out a constraint that has an insoluble Derived. Lastly, this labels one test (dependent/should_fail/RAE_T32a) as expect_broken, because the problem is really #12919. The different handling of constraints in this patch exposes the error. This fixes bugs #11198, #12373, #13530, and #13610. test cases: typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}
* Apply the right substitution in ty-fam improvementSimon Peyton Jones2017-01-233-0/+133
| | | | | | | | | | | | Trac #13135 showed that we were failing to apply the correct substitution to the un-substituted tyvars during type-family improvement using injectivity. Specifically in TcInteractlinjImproveEqns we need to use instFlexiX. An outright bug, easy to fix. Slight refactoring along the way. The quantified tyars of the axiom are readily to hand; we don't need to take the free tyvars of the LHS
* Update levity polymorphismRichard Eisenberg2017-01-191-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit implements the proposal in https://github.com/ghc-proposals/ghc-proposals/pull/29 and https://github.com/ghc-proposals/ghc-proposals/pull/35. Here are some of the pieces of that proposal: * Some of RuntimeRep's constructors have been shortened. * TupleRep and SumRep are now parameterized over a list of RuntimeReps. * This means that two types with the same kind surely have the same representation. Previously, all unboxed tuples had the same kind, and thus the fact above was false. * RepType.typePrimRep and friends now return a *list* of PrimReps. These functions can now work successfully on unboxed tuples. This change is necessary because we allow abstraction over unboxed tuple types and so cannot always handle unboxed tuples specially as we did before. * We sometimes have to create an Id from a PrimRep. I thus split PtrRep * into LiftedRep and UnliftedRep, so that the created Ids have the right strictness. * The RepType.RepType type was removed, as it didn't seem to help with * much. * The RepType.repType function is also removed, in favor of typePrimRep. * I have waffled a good deal on whether or not to keep VoidRep in TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not* represented in RuntimeRep, and typePrimRep will never return a list including VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can imagine another design choice where we have a PrimRepV type that is PrimRep with an extra constructor. That seemed to be a heavier design, though, and I'm not sure what the benefit would be. * The last, unused vestiges of # (unliftedTypeKind) have been removed. * There were several pretty-printing bugs that this change exposed; * these are fixed. * We previously checked for levity polymorphism in the types of binders. * But we also must exclude levity polymorphism in function arguments. This is hard to check for, requiring a good deal of care in the desugarer. See Note [Levity polymorphism checking] in DsMonad. * In order to efficiently check for levity polymorphism in functions, it * was necessary to add a new bit of IdInfo. See Note [Levity info] in IdInfo. * It is now safe for unlifted types to be unsaturated in Core. Core Lint * is updated accordingly. * We can only know strictness after zonking, so several checks around * strictness in the type-checker (checkStrictBinds, the check for unlifted variables under a ~ pattern) have been moved to the desugarer. * Along the way, I improved the treatment of unlifted vs. banged * bindings. See Note [Strict binds checks] in DsBinds and #13075. * Now that we print type-checked source, we must be careful to print * ConLikes correctly. This is facilitated by a new HsConLikeOut constructor to HsExpr. Particularly troublesome are unlifted pattern synonyms that get an extra void# argument. * Includes a submodule update for haddock, getting rid of #. * New testcases: typecheck/should_fail/StrictBinds typecheck/should_fail/T12973 typecheck/should_run/StrictPats typecheck/should_run/T12809 typecheck/should_fail/T13105 patsyn/should_fail/UnliftedPSBind typecheck/should_fail/LevPolyBounded typecheck/should_compile/T12987 typecheck/should_compile/T11736 * Fixed tickets: #12809 #12973 #11736 #13075 #12987 * This also adds a test case for #13105. This test case is * "compile_fail" and succeeds, because I want the testsuite to monitor the error message. When #13105 is fixed, the test case will compile cleanly.
View Lorry Controller Status