summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt
Commit message (Collapse)AuthorAgeFilesLines
* Enable -Wcompat=error in the testsuiteVladislav Zavialov2018-10-1510-16/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Enabling -Werror=compat in the testsuite allows us to easily see the impact that a new warning has on code. It also means that in the period between adding the warning and making the actual breaking change, all new test cases that are being added to the testsuite will be forwards-compatible. This is good because it will make the actual breaking change contain less irrelevant testsuite updates. Things that -Wcompat warns about are things that are going to break in the future, so we can be proactive and keep our testsuite forwards-compatible. This patch consists of two main changes: * Add `TEST_HC_OPTS += -Werror=compat` to the testsuite configuration. * Fix all broken test cases. Test Plan: Validate Reviewers: hvr, goldfire, bgamari, simonpj, RyanGlScott Reviewed By: goldfire, RyanGlScott Subscribers: rwbarton, carter GHC Trac Issues: #15278 Differential Revision: https://phabricator.haskell.org/D5200
* Better error reporting for inaccessible codeSimon Peyton Jones2018-08-243-0/+24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Embrace -XTypeInType, add -XStarIsTypeVladislav Zavialov2018-06-144-8/+12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Turn "inaccessible code" error into a warningTobias Dammers2018-06-025-27/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With GADTs, it is possible to write programs such that the type constraints make some code branches inaccessible. Take, for example, the following program :: {-# LANGUAGE GADTs #-} data Foo a where Foo1 :: Foo Char Foo2 :: Foo Int data TyEquality a b where Refl :: TyEquality a a checkTEQ :: Foo t -> Foo u -> Maybe (TyEquality t u) checkTEQ x y = error "unimportant" step2 :: Bool step2 = case checkTEQ Foo1 Foo2 of Just Refl -> True -- Inaccessible code Nothing -> False Clearly, the `Just Refl` case cannot ever be reached, because the `Foo1` and `Foo2` constructors say `t ~ Char` and `u ~ Int`, while the `Refl` constructor essentially mandates `t ~ u`, and thus `Char ~ Int`. Previously, GHC would reject such programs entirely; however, in practice this is too harsh. Accepting such code does little harm, since attempting to use the "impossible" code will still produce errors down the chain, while rejecting it means we cannot legally write or generate such code at all. Hence, we turn the error into a warning, and provide `-Winaccessible-code` to control GHC's behavior upon encountering this situation. Test Plan: ./validate Reviewers: bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #11066 Differential Revision: https://phabricator.haskell.org/D4744
* Improved Valid Hole FitsMatthías Páll Gissurarson2018-05-301-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I've changed the name from `Valid substitutions` to `Valid hole fits`, since "substitution" already has a well defined meaning within the theory. As part of this change, the flags and output is reanamed, with substitution turning into hole-fit in most cases. "hole fit" was already used internally in the code, it's clear and shouldn't cause any confusion. In this update, I've also reworked how we manage side-effects in the hole we are considering. This allows us to consider local bindings such as where clauses and arguments to functions, suggesting e.g. `a` for `head (x:xs) where head :: [a] -> a`. It also allows us to find suggestions such as `maximum` for holes of type `Ord a => a -> [a]`, and `max` when looking for a match for the hole in `g = foldl1 _`, where `g :: Ord a => [a] -> a`. We also show much improved output for refinement hole fits, and fixes #14990. We now show the correct type of the function, but we also now show what the arguments to the function should be e.g. `foldl1 (_ :: Integer -> Integer -> Integer)` when looking for `[Integer] -> Integer`. I've moved the bulk of the code from `TcErrors.hs` to a new file, `TcHoleErrors.hs`, since it was getting too big to not live on it's own. This addresses the considerations raised in #14969, and takes proper care to set the `tcLevel` of the variables to the right level before passing it to the simplifier. We now also zonk the suggestions properly, which improves the output of the refinement hole fits considerably. This also filters out suggestions from the `GHC.Err` module, since even though `error` and `undefined` are indeed valid hole fits, they are "trivial", and almost never useful to the user. We now find the hole fits using the proper manner, namely by solving nested implications. This entails that the givens are passed along using the implications the hole was nested in, which in turn should mean that there will be fewer weird bugs in the typed holes. I've also added a new sorting method (as suggested by SPJ) and sort by the size of the types needed to turn the hole fits into the type of the hole. This gives a reasonable approximation to relevance, and is much faster than the subsumption check. I've also added a flag to toggle whether to use this new sorting algorithm (as is done by default) or the subsumption algorithm. This fixes #14969 I've also added documentation for these new flags and update the documentation according to the new output. Reviewers: bgamari, goldfire Reviewed By: bgamari Subscribers: simonpj, rwbarton, thomie, carter GHC Trac Issues: #14969, #14990, #10946 Differential Revision: https://phabricator.haskell.org/D4444
* Orient TyVar/TyVar equalities with deepest on the leftSimon Peyton Jones2018-05-182-0/+21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-311-3/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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}
* Wombling around in Trac #14808Simon Peyton Jones2018-03-051-0/+6
| | | | | | | | | | | Comment:4 in Trac #14808 explains why I'm unhappy with the current state of affairs -- at least the lack of documentation. This smallpatch does nothing major: * adds comments * uses existing type synonyms more (notably FreeKiTyVarsWithDups) * adds another test case to T14808
* Rename the types in a GADT constructor in toposorted orderRyan Scott2018-02-182-0/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | Previously, we were extracting the free variables from a GADT constructor in an incorrect order, which caused the type variables for the constructor's type signature to end up in non-toposorted order. Thankfully, rearranging the order of types during renaming makes swift work of this bug. This fixes a regression introduced in commit fa29df02a1b0b926afb2525a258172dcbf0ea460. For whatever reason, that commit also commented out a significant portion of the `T13123` test. This code appears to work, so I've opted to uncomment it. Test Plan: make test TEST=T14808 Reviewers: simonpj, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #14808 Differential Revision: https://phabricator.haskell.org/D4413
* Fix #14719 by using the setting the right SrcSpanRyan Scott2018-01-263-0/+27
| | | | | | | | | | | | | | | | | | | | Currently, error messages that germane to GADT constructors put the source span at only the first character in the constructor, leading to insufficient caret diagnostics. This can be easily fixed by using a source span that spans the entire constructor, instead of just the first character. Test Plan: make test TEST=T14719 Reviewers: alanz, bgamari, simonpj Reviewed By: alanz, simonpj Subscribers: simonpj, goldfire, rwbarton, thomie, carter GHC Trac Issues: #14719 Differential Revision: https://phabricator.haskell.org/D4344
* typecheck: Clarify errors mentioned in #14385Ben Gamari2017-10-253-3/+3
|
* Fix #14320 by looking through HsParTy in more placesRyan Scott2017-10-072-0/+16
| | | | | | | | | | | | | | | | | | | | | | Summary: GHC was needlessly rejecting GADT constructors' type signatures that were surrounded in parentheses due to the fact that `splitLHsForAllTy` and `splitLHsQualTy` (which are used to check as part of checking if GADT constructor return types are correct) weren't looking through parentheses (i.e., `HsParTy`). This is easily fixed, though. Test Plan: make test TEST=T14320 Reviewers: austin, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie GHC Trac Issues: #14320 Differential Revision: https://phabricator.haskell.org/D4072
* Track the order of user-written tyvars in DataConRyan Scott2017-10-031-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After typechecking a data constructor's type signature, its type variables are partitioned into two distinct groups: the universally quantified type variables and the existentially quantified type variables. Then, when prompted for the type of the data constructor, GHC gives this: ```lang=haskell MkT :: forall <univs> <exis>. (...) ``` For H98-style datatypes, this is a fine thing to do. But for GADTs, this can sometimes produce undesired results with respect to `TypeApplications`. For instance, consider this datatype: ```lang=haskell data T a where MkT :: forall b a. b -> T a ``` Here, the user clearly intended to have `b` be available for visible type application before `a`. That is, the user would expect `MkT @Int @Char` to be of type `Int -> T Char`, //not// `Char -> T Int`. But alas, up until now that was not how GHC operated—regardless of the order in which the user actually wrote the tyvars, GHC would give `MkT` the type: ```lang=haskell MkT :: forall a b. b -> T a ``` Since `a` is universal and `b` is existential. This makes predicting what order to use for `TypeApplications` quite annoying, as demonstrated in #11721 and #13848. This patch cures the problem by tracking more carefully the order in which a user writes type variables in data constructor type signatures, either explicitly (with a `forall`) or implicitly (without a `forall`, in which case the order is inferred). This is accomplished by adding a new field `dcUserTyVars` to `DataCon`, which is a subset of `dcUnivTyVars` and `dcExTyVars` that is permuted to the order in which the user wrote them. For more details, refer to `Note [DataCon user type variables]` in `DataCon.hs`. An interesting consequence of this design is that more data constructors require wrappers. This is because the workers always expect the first arguments to be the universal tyvars followed by the existential tyvars, so when the user writes the tyvars in a different order, a wrapper type is needed to swizzle the tyvars around to match the order that the worker expects. For more details, refer to `Note [Data con wrappers and GADT syntax]` in `MkId.hs`. Test Plan: ./validate Reviewers: austin, goldfire, bgamari, simonpj Reviewed By: goldfire, simonpj Subscribers: ezyang, goldfire, rwbarton, thomie GHC Trac Issues: #11721, #13848 Differential Revision: https://phabricator.haskell.org/D3687
* Also show types that subsume a hole as valid substitutions for that hole.Matthías Páll Gissurarson2017-09-211-0/+12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This builds on the previous "Valid substitutions include..." functionality, but add subsumption checking as well, so that the suggested valid substitutions show not only exact matches, but also identifiers that fit the hole by virtue of subsuming the type of the hole (i.e. being more general than the type of the hole). Building on the previous example, in the given program ``` ps :: String -> IO () ps = putStrLn ps2 :: a -> IO () ps2 _ = putStrLn "hello, world" main :: IO () main = _ "hello, world" ``` The results would be something like ``` • Found hole: _ :: [Char] -> IO () • In the expression: _ In the expression: _ "hello, world" In an equation for ‘main’: main = _ "hello, world" • Relevant bindings include main :: IO () (bound at t1.hs:8:1) Valid substitutions include ps :: String -> IO () (defined at t1.hs:2:1) ps2 :: forall a. a -> IO () (defined at t1.hs:5:1) putStrLn :: String -> IO () (imported from ‘Prelude’ at t1.hs:1:1 (and originally defined in ‘System.IO’)) fail :: forall (m :: * -> *). Monad m => forall a. String -> m a (imported from ‘Prelude’ at t1.hs:1:1 (and originally defined in ‘GHC.Base’)) mempty :: forall a. Monoid a => a (imported from ‘Prelude’ at t1.hs:1:1 (and originally defined in ‘GHC.Base’)) print :: forall a. Show a => a -> IO () (imported from ‘Prelude’ at t1.hs:1:1 (and originally defined in ‘System.IO’)) (Some substitutions suppressed; use -fmax-valid-substitutions=N or -fno-max-valid-substitutions) ``` Signed-off-by: Matthías Páll Gissurarson <mpg@mpg.is> Modified according to suggestions from Simon PJ Accept tests that match the expectations, still a few to look better at Swithced to using tcLookup, after sit down with SPJ at ICFP. Implications are WIP. Now works with polymorphism and constraints! We still need to merge the latest master, before we can make a patch. Wrap the type of the hole, instead of implication shenanigans, As per SPJs suggestion, this is simpler and feels closer to what we actually want to do. Updated tests with the new implementation Remove debugging trace and update documentation Reviewers: austin, bgamari Reviewed By: bgamari Subscribers: RyanGlScott, rwbarton, thomie Differential Revision: https://phabricator.haskell.org/D3930
* Suggest how to fix illegally nested foralls in GADT constructor type signaturesRyan Scott2017-08-173-1/+55
| | | | | | | | | | | | | | | | | | Summary: Although the code from #12087 isn't accepted by GHC, we can at least do a better job of letting users know what the problem is, and how to fix it. Test Plan: make test TEST=T12087 Reviewers: goldfire, austin, bgamari Reviewed By: goldfire Subscribers: rwbarton, thomie GHC Trac Issues: #12087 Differential Revision: https://phabricator.haskell.org/D3851
* Improve error messages around kind mismatches.Richard Eisenberg2017-07-271-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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}
* Some tidying up of type pretty-printingSimon Peyton Jones2017-05-261-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | Triggered by the changes in #13677, I ended up doing a bit of refactoring in type pretty-printing. * We were using TyOpPrec and FunPrec rather inconsitently, so I made it consisent. * That exposed the fact that we were a bit undecided about whether to print a + b -> c + d vs (a+b) -> (c+d) and similarly a ~ [b] => blah vs (a ~ [b]) => blah I decided to make TyOpPrec and FunPrec compare equal (in BasicTypes), so (->) is treated as equal precedence with other type operators, so you get the unambiguous forms above, even though they have more parens. We could readily reverse this decision. See Note [Type operator precedence] in BasicTypes * I fixed a bug in pretty-printing of HsType where some parens were omitted by mistake.
* Re-engineer Given flatten-skolemsSimon Peyton Jones2017-05-262-10/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The big change here is to fix an outright bug in flattening of Givens, albeit one that is very hard to exhibit. Suppose we have the constraint forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ... Then - we'll flatten the (F) b to a fsk, say (F b ~ fsk1) - we'll rewrite the (F b) inside the inner implication to 'fsk1' - when we leave the outer constraint we are suppose to unflatten; but that fsk1 will still be there - if we re-simplify the entire outer implication, we'll re-flatten the Given (F b) to, say, (F b ~ fsk2) Now we have two fsks standing for the same thing, and that is very wrong. Solution: make fsks behave more like fmvs: - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv - We "fill in" that meta-tyvar when leaving the implication - The old FlatSkol form of TcTyVarDetails is gone completely - We track the flatten-skolems for the current implication in a new field of InertSet, inert_fsks. See Note [The flattening story] in TcFlatten. In doing this I found various other things to fix: * I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't needed. But I added one in TcSimplify.floatEqualities, which does the zonk precisely when it is needed. * Trac #13674 showed up a case where we had - an insoluble Given, e.g. a ~ [a] - the same insoluble Wanted a ~ [a] We don't use the Given to rewwrite the Wanted (obviously), but we therefore ended up reporting Can't deduce (a ~ [a]) from (a ~ [a]) which is silly. Conclusion: when reporting errors, make the occurs check "win" See Note [Occurs check wins] in TcErrors
* Ensure that insolubles are fully rewrittenSimon Peyton Jones2017-05-193-0/+16
| | | | | | | | | | | | | | | | I was alerted to this by Trac #12468 and #11325. We were treating insolubles (and "hole" constraints are treated as insoluble) inconsistently. In some places we were carefully rewriting them e.g. Note [Make sure that insolubles are fully rewritten] in TcCanonical. But in TcSimplify we weren't feeding them into the solver. As a result, "hole" constraints were not being rewritten, which some users found confusing, and I think rightly so. This patch also fixes a bug in TcSMonad.emitInsoluble, in which two different "hole" constriants could be treated (bogusly) as duplicates, thereby losing one.
* Typos in comments [ci skip]Gabor Greif2017-04-111-1/+1
|
* Fix TcSimplify.decideQuantification for kind variablesSimon Peyton Jones2017-03-101-8/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | TcSimplify.decideQuantification was doing the Wrong Thing when "growing" the type variables to quantify over. We were trying to do this on a tyvar set where we'd split off the dependent type varaibles; and we just got it wrong. A kind variable wasn't being generalised properly, with confusing knock on consequences. All this led to Trac #13371 and Trac #13393. This commit tidies it all up: * The type TcDepVars is renamed as CandidateQTvs; and splitDepVarsOfType to candidateQTyVarsOfType * The code in TcSimplify.decideQuantification is simpler. It no longer does the tricky "grow" stuff over TcDepVars. Instead it use ordinary VarSets (thereby eliminating the nasty growThetaTyVarsDSet) and uses that to filter the result of candidateQTyVarsOfType. * I documented that candidateQTyVarsOfType returns the type variables in a good order in which to quantify, and rewrote it to use an accumulator pattern, so that we would predicatably get left-to-right ordering. In doing all this I also made UniqDFM behave a little more nicely: * When inserting an element that is there already, keep the old tag, while still overwriting with the new value. * This means that when doing udfmToList we get back elements in the order they were originally inserted, rather than in reverse order. It's not a big deal, but in a subsequent commit I use it to improve the order of type variables in inferred types. All this led to a lot of error message wibbles: - changing the order of quantified variables - changing the order in which instances are listed in GHCi - changing the tidying of variables in typechecker erors There's a submodule update for 'array' because one of its tests has an error-message change. I may not have associated all of them with the correct commit.
* tests: remove extra_files.py (#12223)Reid Barton2017-02-261-2/+2
| | | | | | | | | | | | The script I used is included as testsuite/driver/kill_extra_files.py, though at this point it is for mostly historical interest. Some of the tests in libraries/hpc relied on extra_files.py, so this commit includes an update to that submodule. One test in libraries/process also relies on extra_files.py, but we cannot update that submodule so easily, so for now we special-case it in the test driver.
* Remove clean_cmd and extra_clean usage from .T filesThomas Miedema2017-01-221-16/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | The `clean_cmd` and `extra_clean` setup functions don't do anything. Remove them from .T files. Created using https://github.com/thomie/refactor-ghc-testsuite. This diff is a test for the .T-file parser/processor/pretty-printer in that repository. find . -name '*.T' -exec ~/refactor-ghc-testsuite/Main "{}" \; Tests containing inline comments or multiline strings are not modified. Preparation for #12223. Test Plan: Harbormaster Reviewers: austin, hvr, simonmar, mpickering, bgamari Reviewed By: mpickering Subscribers: mpickering Differential Revision: https://phabricator.haskell.org/D3000 GHC Trac Issues: #12223
* Spelling fixes in comments [ci skip]Gabor Greif2017-01-181-1/+1
|
* Take account of kinds in promoteTcTypeSimon Peyton Jones2016-10-241-3/+3
| | | | | | | | | One of the ASSERT failures in Trac #12762, namely the one for T4439, showed that I had not dealt correctly with promoting the kind of a type in promoteTcType. Happily I could fix this by simplifying InferRes (eliminating the ir_kind field), so things get better. And the ASSERT is fixed.
* A collection of type-inference refactorings.Simon Peyton Jones2016-10-213-22/+22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch does a raft of useful tidy-ups in the type checker. I've been meaning to do this for some time, and finally made time to do it en route to ICFP. 1. Modify TcType.ExpType to make a distinct data type, InferResult for the Infer case, and consequential refactoring. 2. Define a new function TcUnify.fillInferResult, to fill in an InferResult. It uses TcMType.promoteTcType to promote the type to the level of the InferResult. See TcMType Note [Promoting a type] This refactoring is in preparation for an improvement to typechecking pattern bindings, coming next. I flirted with an elaborate scheme to give better higher rank inference, but it was just too complicated. See TcMType Note [Promotion and higher rank types] 3. Add to InferResult a new field ir_inst :: Bool to say whether or not the type used to fill in the InferResult should be deeply instantiated. See TcUnify Note [Deep instantiation of InferResult]. 4. Add a TcLevel to SkolemTvs. This will be useful generally - it's a fast way to see if the type variable escapes when floating (not used yet) - it provides a good consistency check when updating a unification variable (TcMType.writeMetaTyVarRef, the level_check_ok check) I originally had another reason (related to the flirting in (2), but I left it in because it seems like a step in the right direction. 5. Reduce and simplify the plethora of uExpType, tcSubType and related functions in TcUnify. It was such an opaque mess and it's still not great, but it's better. 6. Simplify the uo_expected field of TypeEqOrigin. Richard had generatlised it to a ExpType, but it was almost always a Check type. Now it's back to being a plain TcType which is much, much easier. 7. Improve error messages by refraining from skolemisation when it's clear that there's an error: see TcUnify Note [Don't skolemise unnecessarily] 8. Type.isPiTy and isForAllTy seem to be missing a coreView check, so I added it 9. Kill off tcs_used_tcvs. Its purpose is to track the givens used by wanted constraints. For dictionaries etc we do that via the free vars of the /bindings/ in the implication constraint ic_binds. But for coercions we just do update-in-place in the type, rather than generating a binding. So we need something analogous to bindings, to track what coercions we have added. That was the purpose of tcs_used_tcvs. But it only worked for a /single/ iteration, whereas we may have multiple iterations of solving an implication. Look at (the old) 'setImplicationStatus'. If the constraint is unsolved, it just drops the used_tvs on the floor. If it becomes solved next time round, we'll pick up coercions used in that round, but ignore ones used in the first round. There was an outright bug. Result = (potentialy) bogus unused-constraint errors. Constructing a case where this actually happens seems quite trick so I did not do so. Solution: expand EvBindsVar to include the (free vars of the) coercions, so that the coercions are tracked in essentially the same way as the bindings. This turned out to be much simpler. Less code, more correct. 10. Make the ic_binds field in an implication have type ic_binds :: EvBindsVar instead of (as previously) ic_binds :: Maybe EvBindsVar This is notably simpler, and faster to use -- less testing of the Maybe. But in the occaional situation where we don't have anywhere to put the bindings, the belt-and-braces error check is lost. So I put it back as an ASSERT in 'setImplicationStatus' (see the use of 'termEvidenceAllowed') All these changes led to quite bit of error message wibbling
* Testsuite: tabs -> spaces [skip ci]Thomas Miedema2016-06-2016-206/+205
|
* Testsuite: remove Windows CR [skip ci]Thomas Miedema2016-06-204-83/+83
|
* Major patch to introduce TyConBinderSimon Peyton Jones2016-06-152-37/+37
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before this patch, following the TypeInType innovations, each TyCon had two lists: - tyConBinders :: [TyBinder] - tyConTyVars :: [TyVar] They were in 1-1 correspondence and contained overlapping information. More broadly, there were many places where we had to pass around this pair of lists, instead of a single list. This commit tidies all that up, by having just one list of binders in a TyCon: - tyConBinders :: [TyConBinder] The new data types look like this: Var.hs: data TyVarBndr tyvar vis = TvBndr tyvar vis data VisibilityFlag = Visible | Specified | Invisible type TyVarBinder = TyVarBndr TyVar VisibilityFlag TyCon.hs: type TyConBinder = TyVarBndr TyVar TyConBndrVis data TyConBndrVis = NamedTCB VisibilityFlag | AnonTCB TyCoRep.hs: data TyBinder = Named TyVarBinder | Anon Type Note that Var.TyVarBdr has moved from TyCoRep and has been made polymorphic in the tyvar and visiblity fields: type TyVarBinder = TyVarBndr TyVar VisibilityFlag -- Used in ForAllTy type TyConBinder = TyVarBndr TyVar TyConBndrVis -- Used in TyCon type IfaceForAllBndr = TyVarBndr IfaceTvBndr VisibilityFlag type IfaceTyConBinder = TyVarBndr IfaceTvBndr TyConBndrVis -- Ditto, in interface files There are a zillion knock-on changes, but everything arises from these types. It was a bit fiddly to get the module loops to work out right! Some smaller points ~~~~~~~~~~~~~~~~~~~ * Nice new functions TysPrim.mkTemplateKiTyVars TysPrim.mkTemplateTyConBinders which help you make the tyvar binders for dependently-typed TyCons. See comments with their definition. * The change showed up a bug in TcGenGenerics.tc_mkRepTy, where the code was making an assumption about the order of the kind variables in the kind of GHC.Generics.(:.:). I fixed this; see TcGenGenerics.mkComp.
* Improve typechecking of let-bindingsSimon Peyton Jones2016-06-136-120/+120
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This major commit was initially triggered by #11339, but it spiraled into a major review of the way in which type signatures for bindings are handled, especially partial type signatures. On the way I fixed a number of other bugs, namely #12069 #12033 #11700 #11339 #11670 The main change is that I completely reorganised the way in which type signatures in bindings are handled. The new story is in TcSigs Note [Overview of type signatures]. Some specific: * Changes in the data types for signatures in TcRnTypes: TcIdSigInfo and new TcIdSigInst * New module TcSigs deals with typechecking type signatures and pragmas. It contains code mostly moved from TcBinds, which is already too big * HsTypes: I swapped the nesting of HsWildCardBndrs and HsImplicitBndsrs, so that the wildcards are on the oustide not the insidde in a LHsSigWcType. This is just a matter of convenient, nothing deep. There are a host of other changes as knock-on effects, and it all took FAR longer than I anticipated :-). But it is a significant improvement, I think. Lots of error messages changed slightly, some just variants but some modest improvements. New tests * typecheck/should_compile * SigTyVars: a scoped-tyvar test * ExPat, ExPatFail: existential pattern bindings * T12069 * T11700 * T11339 * partial-sigs/should_compile * T12033 * T11339a * T11670 One thing to check: * Small change to output from ghc-api/landmines. Need to check with Alan Zimmerman
* Testsuite: benign test fixesThomas Miedema2016-04-282-1/+6
|
* Kill varSetElemsWellScoped in quantifyTyVarsBartosz Nitka2016-04-262-15/+15
| | | | | | | | | | | | | | | | | | | | | | | | varSetElemsWellScoped introduces unnecessary non-determinism in inferred type signatures. Removing this instance required changing the representation of TcDepVars to use deterministic sets. This is the last occurence of varSetElemsWellScoped, allowing me to finally remove it. Test Plan: ./validate I will update the expected outputs when commiting, some reordering of type variables in types is expected. Reviewers: goldfire, simonpj, austin, bgamari Reviewed By: simonpj Subscribers: thomie, simonmar Differential Revision: https://phabricator.haskell.org/D2135 GHC Trac Issues: #4012
* Make equality print better. (#11712)Richard Eisenberg2016-03-211-1/+1
|
* Annotate `[-Wdeferred-type-errors]` in warnings (re #10752)Herbert Valerio Riedel2016-02-271-1/+1
| | | | This was missed in bb5afd3c274011c5ea302210b4c290ec1f83209c
* Print which flag controls emitted desugaring warningsHerbert Valerio Riedel2016-02-271-12/+12
| | | | | | | | | | | This is extends bb5afd3c274011c5ea302210b4c290ec1f83209c to cover warnings emitted during the desugaring phase. This implements another part of #10752 Reviewed-by: quchen, bgamari Differential Revision: https://phabricator.haskell.org/D1954
* Testsuite: delete empty files [skip ci]Thomas Miedema2016-02-251-0/+0
|
* (Alternative way to) address #8710George Karachalias2016-02-251-12/+12
| | | | | | | | | | | | | | | | | | | | | | | | Issue a separate warning per redundant (or inaccessible) clause. This way each warning can have more precice location information (the location of the clause under consideration and not the whole match). I thought that this could be too much but actually the number of such warnings is bound by the number of cases matched against (in contrast to the non-exhaustive warnings which may be exponentially more). Test Plan: validate Reviewers: simonpj, austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D1920 GHC Trac Issues: #8710
* Testsuite: delete Windows line endings [skip ci] (#11631)Thomas Miedema2016-02-231-5/+5
|
* Testsuite: accept output without Windows line endings (#11631)Thomas Miedema2016-02-238-83/+83
|
* Testsuite: delete Windows line endings [skip ci] (#11631)Thomas Miedema2016-02-2314-650/+650
|
* Another batch of typo fixes in non-codeGabor Greif2016-02-111-1/+1
|
* Allow foralls in instance declsSimon Peyton Jones2016-02-081-5/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch finally makes it possible to have explicit foralls in an instance decl instance forall (a :: *). Eq a => Eq [a] where ... This is useful to allow kind signatures or indeed explicicit kind for-alls; see Trac #11519 I thought it would be really easy, because an instance declaration already contains an actual HsSigType, so all the syntactic baggage is there. But in fact it turned out that instance declarations were kind-checked a little differently, because the body kind of the forall is 'Constraint' rather than '*'. So I fixed that. There a slight kludge (see Note [Body kind of a HsQualTy], but it's still a significant improvement. I also did the usual other round of refactoring, improved a few error messages, tidied up comments etc. The only significant aspect of all that was * Kill mkNakedSpecSigmaTy, mkNakedPhiTy, mkNakedFunTy These function names suggest that they do something complicated, but acutally they do nothing. So I killed them. * Swap the arg order of mkNamedBinder, just so that it is convenient to say 'map (mkNamedBinder Invisible) tvs' * I had to improve isPredTy, to deal with (illegal) types like (Eq a => Eq [a]) => blah See Note [isPeredTy complications] in Type.hs Still to come: user manual documentation for the instance-decl change.
* Refactor the typechecker to use ExpTypes.Richard Eisenberg2016-01-273-23/+23
| | | | | | | | | | | | | | | | | | | | | The idea here is described in [wiki:Typechecker]. Briefly, this refactor keeps solid track of "synthesis" mode vs "checking" in GHC's bidirectional type-checking algorithm. When in synthesis mode, the expected type is just an IORef to write to. In addition, this patch does a significant reworking of RebindableSyntax, allowing much more freedom in the types of the rebindable operators. For example, we can now have `negate :: Int -> Bool` and `(>>=) :: m a -> (forall x. a x -> m b) -> m b`. The magic is in tcSyntaxOp. This addresses tickets #11397, #11452, and #11458. Tests: typecheck/should_compile/{RebindHR,RebindNegate,T11397,T11458} th/T11452
* Visible type applicationRichard Eisenberg2015-12-245-10/+18
| | | | | | | | | | | | | This re-working of the typechecker algorithm is based on the paper "Visible type application", by Richard Eisenberg, Stephanie Weirich, and Hamidhasan Ahmed, to be published at ESOP'16. This patch introduces -XTypeApplications, which allows users to say, for example `id @Int`, which has type `Int -> Int`. See the changes to the user manual for details. This patch addresses tickets #10619, #5296, #10589.
* Add kind equalities to GHC.Richard Eisenberg2015-12-115-55/+55
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This implements the ideas originally put forward in "System FC with Explicit Kind Equality" (ICFP'13). There are several noteworthy changes with this patch: * We now have casts in types. These change the kind of a type. See new constructor `CastTy`. * All types and all constructors can be promoted. This includes GADT constructors. GADT pattern matches take place in type family equations. In Core, types can now be applied to coercions via the `CoercionTy` constructor. * Coercions can now be heterogeneous, relating types of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2` proves both that `t1` and `t2` are the same and also that `k1` and `k2` are the same. * The `Coercion` type has been significantly enhanced. The documentation in `docs/core-spec/core-spec.pdf` reflects the new reality. * The type of `*` is now `*`. No more `BOX`. * Users can write explicit kind variables in their code, anywhere they can write type variables. For backward compatibility, automatic inference of kind-variable binding is still permitted. * The new extension `TypeInType` turns on the new user-facing features. * Type families and synonyms are now promoted to kinds. This causes trouble with parsing `*`, leading to the somewhat awkward new `HsAppsTy` constructor for `HsType`. This is dispatched with in the renamer, where the kind `*` can be told apart from a type-level multiplication operator. Without `-XTypeInType` the old behavior persists. With `-XTypeInType`, you need to import `Data.Kind` to get `*`, also known as `Type`. * The kind-checking algorithms in TcHsType have been significantly rewritten to allow for enhanced kinds. * The new features are still quite experimental and may be in flux. * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203. * TODO: Update user manual. Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142. Updates Haddock submodule.
* Major Overhaul of Pattern Match Checking (Fixes #595)George Karachalias2015-12-032-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch adresses several problems concerned with exhaustiveness and redundancy checking of pattern matching. The list of improvements includes: * Making the check type-aware (handles GADTs, Type Families, DataKinds, etc.). This fixes #4139, #3927, #8970 and other related tickets. * Making the check laziness-aware. Cases that are overlapped but affect evaluation are issued now with "Patterns have inaccessible right hand side". Additionally, "Patterns are overlapped" is now replaced by "Patterns are redundant". * Improved messages for literals. This addresses tickets #5724, #2204, etc. * Improved reasoning concerning cases where simple and overloaded patterns are matched (See #322). * Substantially improved reasoning for pattern guards. Addresses #3078. * OverloadedLists extension does not break exhaustiveness checking anymore (addresses #9951). Note that in general this cannot be handled but if we know that an argument has type '[a]', we treat it as a list since, the instance of 'IsList' gives the identity for both 'fromList' and 'toList'. If the type is not clear or is not the list type, then the check cannot do much still. I am a bit concerned about OverlappingInstances though, since one may override the '[a]' instance with e.g. an '[Int]' instance that is not the identity. * Improved reasoning for nested pattern matching (partial solution). Now we propagate type and (some) term constraints deeper when checking, so we can detect more inconsistencies. For example, this is needed for #4139. I am still not satisfied with several things but I would like to address at least the following before the next release: Term constraints are too many and not printed for non-exhaustive matches (with the exception of literals). This sometimes results in two identical (in appearance) uncovered warnings. Unless we actually show their difference, I would like to have a single warning.
* Refactor treatment of wildcardsSimon Peyton Jones2015-12-013-40/+44
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch began as a modest refactoring of HsType and friends, to clarify and tidy up exactly where quantification takes place in types. Although initially driven by making the implementation of wildcards more tidy (and fixing a number of bugs), I gradually got drawn into a pretty big process, which I've been doing on and off for quite a long time. There is one compiler performance regression as a result of all this, in perf/compiler/T3064. I still need to look into that. * The principal driving change is described in Note [HsType binders] in HsType. Well worth reading! * Those data type changes drive almost everything else. In particular we now statically know where (a) implicit quantification only (LHsSigType), e.g. in instance declaratios and SPECIALISE signatures (b) implicit quantification and wildcards (LHsSigWcType) can appear, e.g. in function type signatures * As part of this change, HsForAllTy is (a) simplified (no wildcards) and (b) split into HsForAllTy and HsQualTy. The two contructors appear when and only when the correponding user-level construct appears. Again see Note [HsType binders]. HsExplicitFlag disappears altogether. * Other simplifications - ExprWithTySig no longer needs an ExprWithTySigOut variant - TypeSig no longer needs a PostRn name [name] field for wildcards - PatSynSig records a LHsSigType rather than the decomposed pieces - The mysterious 'GenericSig' is now 'ClassOpSig' * Renamed LHsTyVarBndrs to LHsQTyVars * There are some uninteresting knock-on changes in Haddock, because of the HsSyn changes I also did a bunch of loosely-related changes: * We already had type synonyms CoercionN/CoercionR for nominal and representational coercions. I've added similar treatment for TcCoercionN/TcCoercionR mkWpCastN/mkWpCastN All just type synonyms but jolly useful. * I record-ised ForeignImport and ForeignExport * I improved the (poor) fix to Trac #10896, by making TcTyClsDecls.checkValidTyCl recover from errors, but adding a harmless, abstract TyCon to the envt if so. * I did some significant refactoring in RnEnv.lookupSubBndrOcc, for reasons that I have (embarrassingly) now totally forgotten. It had to do with something to do with import and export Updates haddock submodule.
* Rearrange error msgs and add section markers (Trac #11014).Evan Laforge2015-11-246-15/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This puts the "Relevant bindings" section at the end. It uses a TcErrors.Report Monoid to divide messages by importance and then mappends them together. This is not the most efficient way since there are various intermediate Reports and list appends, but it probably doesn't matter since error messages shouldn't get that large, and are usually prepended. In practice, everything is `important` except `relevantBindings`, which is `supplementary`. ErrMsg's errMsgShortDoc and errMsgExtraInfo were extracted into ErrDoc, which has important, context, and suppelementary fields. Each of those three sections is marked with a bullet character, '•' on unicode terminals and '*' on ascii terminals. Since this breaks tons of tests, I also modified testlib.normalise_errmsg to strip out '•'s. --- Additional notes: To avoid prepending * to an empty doc, I needed to filter empty docs. This seemed less error-prone than trying to modify everyone who produces SDoc to instead produce Maybe SDoc. So I added `Outputable.isEmpty`. Unfortunately it needs a DynFlags, which is kind of bogus, but otherwise I think I'd need another Empty case for SDoc, and then it couldn't be a newtype any more. ErrMsg's errMsgShortString is only used by the Show instance, which is in turn only used by Show HscTypes.SourceError, which is in turn only needed for the Exception instance. So it's probably possible to get rid of errMsgShortString, but that would a be an unrelated cleanup. Fixes #11014. Test Plan: see above Reviewers: austin, simonpj, thomie, bgamari Reviewed By: thomie, bgamari Subscribers: simonpj, nomeata, thomie Differential Revision: https://phabricator.haskell.org/D1427 GHC Trac Issues: #11014
* A few typos in commentsGabor Greif2015-10-051-1/+1
|
* Testsuite: by default run all tests for a single wayThomas Miedema2015-09-021-1/+1
| | | | | | | | | | | | | | `make test` now runs all tests for a single way only. Use `make slowtest` to get the previous behaviour (i.e. run all tests for all ways). The intention is to use this new `make test` setting for Phabricator, as a reasonable compromise between `make fasttest` (what it previously used) and a fullblown `make slowtest` (which runs all tests for all ways). See Note [validate and testsuite speed] in toplevel Makefile. Differential Revision: https://phabricator.haskell.org/D1178
View Lorry Controller Status