summaryrefslogtreecommitdiff
path: root/compiler/deSugar/Check.hs
Commit message (Collapse)AuthorAgeFilesLines
...
* TypofixesGabor Greif2017-09-271-1/+1
|
* Document how GHC disambiguates between multiple COMPLETE setsRyan Scott2017-09-251-1/+6
| | | | | | | | | | | | | | | | | | | | | Summary: Up until now, the knowledge of how GHC chooses which `COMPLETE` set to use in the presence of multiple applicable `COMPLETE` sets for a single data type constructor was only documented in the GHC wiki. But this really should be advertised to anyone who uses `COMPLETE` pragmas heavily, so per SPJ's advice in https://ghc.haskell.org/trac/ghc/ticket/14253#comment:10, this adds this wisdom to the GHC users' guide. Test Plan: Read it Reviewers: austin, bgamari Subscribers: mpickering, rwbarton, thomie GHC Trac Issues: #14253 Differential Revision: https://phabricator.haskell.org/D4005
* compiler: introduce custom "GhcPrelude" PreludeHerbert Valerio Riedel2017-09-191-0/+2
| | | | | | | | | | | | | | | | | | This switches the compiler/ component to get compiled with -XNoImplicitPrelude and a `import GhcPrelude` is inserted in all modules. This is motivated by the upcoming "Prelude" re-export of `Semigroup((<>))` which would cause lots of name clashes in every modulewhich imports also `Outputable` Reviewers: austin, goldfire, bgamari, alanz, simonmar Reviewed By: bgamari Subscribers: goldfire, rwbarton, thomie, mpickering, bgamari Differential Revision: https://phabricator.haskell.org/D3989
* Add missing Semigroup instances to compilerHerbert Valerio Riedel2017-08-311-15/+30
| | | | | This is a pre-requisite for implementing the Semigroup/Monoid proposal. The instances have been introduced in a way to minimise warnings.
* Change isClosedAlgType to be TYPE-aware, and rename it to pmIsClosedTypeRyan Scott2017-08-121-14/+147
| | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: In a267580e4ab37115dcc33f3b8a9af67b9364da12, I somewhat awkwardly inserted a special case for `TYPE` in the `EmptyCase` coverage checker. Instead of placing it there, @mpickering noted that `isClosedAlgType` would be a better fit for it. I do just that in this patch. I also renamed `isClosedAlgType` to `pmIsClosedType`, reflecting the fact that `TYPE` technically isn't an algebraic type (it's a primitive one), and that its behavior is pattern-match coverage checking-oriented. I also moved it to `Check`, which is a better home for this function than `Type`. Luckily, the only call sites for `isClosedAlgType` were in the pattern-match coverage checker anyways, so this change is simple enough. Test Plan: ./validate Reviewers: mpickering, austin, goldfire, bgamari Reviewed By: goldfire Subscribers: rwbarton, thomie, mpickering GHC Trac Issues: #14086 Differential Revision: https://phabricator.haskell.org/D3830
* Don't warn when empty casing on TypeRyan Scott2017-08-051-0/+14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: `Type` (a.k.a. `TYPE LiftedRep`) can be used at the type level thanks to `TypeInType`. However, expressions like ```lang=haskell f :: Type -> Int f x = case x of {} ``` were falsely claiming that the empty case on the value of type `Type` was non-exhaustive. The reason is a bit silly: `TYPE` is technically not an empty datatype in GHC's eyes, since it's a builtin, primitive type. To convince the pattern coverage checker otherwise, this adds a special case for `TYPE`. Test Plan: make test TEST=T14086 Reviewers: gkaracha, austin, bgamari, goldfire Reviewed By: goldfire Subscribers: goldfire, rwbarton, thomie GHC Trac Issues: #14086 Differential Revision: https://phabricator.haskell.org/D3819
* Use field names for all uses of datacon MatchSimon Peyton Jones2017-07-311-2/+2
| | | | | | | This is refactoring only... elimiante all positional uses of the data constructor Match in favour of field names. No change in behaviour.
* Refactoring around FunRhsSimon Peyton Jones2017-07-311-3/+3
| | | | | * Clarify the comments around the mc_strictness field of FunRhs * Use record field names consistently for FunRhs
* Fix instantiation of pattern synonymsSimon Peyton Jones2017-07-281-8/+9
| | | | | | | | | | In Check.hs (pattern match ovelap checking) we to figure out the instantiation of a pattern synonym from the type of the pattern. We were doing this utterly wrongly. Trac #13768 demonstrated this bogosity. The fix is easy; and is described in PatSyn.hs Note [Pattern synonym result type]
* Treat banged bindings as FunBindsBen Gamari2017-06-271-3/+3
| | | | | | | | | | | | | | | This is another attempt at resolving #13594 by treating strict variable binds as FunBinds instead of PatBinds (as suggested in comment:1). Test Plan: Validate Reviewers: austin, alanz Subscribers: rwbarton, thomie, mpickering GHC Trac Issues: #13594 Differential Revision: https://phabricator.haskell.org/D3670
* Udate hsSyn AST to use Trees that GrowAlan Zimmerman2017-06-061-32/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: See https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow This commit prepares the ground for a full extensible AST, by replacing the type parameter for the hsSyn data types with a set of indices into type families, data GhcPs -- ^ Index for GHC parser output data GhcRn -- ^ Index for GHC renamer output data GhcTc -- ^ Index for GHC typechecker output These are now used instead of `RdrName`, `Name` and `Id`/`TcId`/`Var` Where the original name type is required in a polymorphic context, this is accessible via the IdP type family, defined as type family IdP p type instance IdP GhcPs = RdrName type instance IdP GhcRn = Name type instance IdP GhcTc = Id These types are declared in the new 'hsSyn/HsExtension.hs' module. To gain a better understanding of the extension mechanism, it has been applied to `HsLit` only, also replacing the `SourceText` fields in them with extension types. To preserve extension generality, a type class is introduced to capture the `SourceText` interface, which must be honoured by all of the extension points which originally had a `SourceText`. The class is defined as class HasSourceText a where -- Provide setters to mimic existing constructors noSourceText :: a sourceText :: String -> a setSourceText :: SourceText -> a getSourceText :: a -> SourceText And the constraint is captured in `SourceTextX`, which is a constraint type listing all the extension points that make use of the class. Updating Haddock submodule to match. Test Plan: ./validate Reviewers: simonpj, shayan-najd, goldfire, austin, bgamari Subscribers: rwbarton, thomie, mpickering Differential Revision: https://phabricator.haskell.org/D3609
* Use lengthIs and friends in more placesRyan Scott2017-06-021-8/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | While investigating #12545, I discovered several places in the code that performed length-checks like so: ``` length ts == 4 ``` This is not ideal, since the length of `ts` could be much longer than 4, and we'd be doing way more work than necessary! There are already a slew of helper functions in `Util` such as `lengthIs` that are designed to do this efficiently, so I found every place where they ought to be used and did just that. I also defined a couple more utility functions for list length that were common patterns (e.g., `ltLength`). Test Plan: ./validate Reviewers: austin, hvr, goldfire, bgamari, simonmar Reviewed By: bgamari, simonmar Subscribers: goldfire, rwbarton, thomie Differential Revision: https://phabricator.haskell.org/D3622
* Revert "Treat banged bindings as FunBinds"Ben Gamari2017-05-121-3/+3
| | | | | | | | This partially reverts commit 372995364c52eef15066132d7d1ea8b6760034e6 as it doesn't actually fix #13594. Namely it does not revert the mkPrefixFunRhs refactoring since this is rather independent from the functional changes. Going to try again with a whole working patch
* pmCheck: Don't generate PmId OccNames from UniquesBen Gamari2017-05-111-1/+1
| | | | | | | | | | | | | | | | | | Doug Wilson astutely noticed that the pattern match checker was spending a significant amount of time in mkPmId. It turns out that it was producing Ids with OccNames that were generated from a Unique, which are non-trivial to render. Since Var is strict in Name, Name in OccName, and OccName in its FastString all of this encoding work was being done despite the fact that it was (as far as I can tell) never actually needed. Test Plan: Validate, note allocations of `T11195` Reviewers: austin, gkaracha Subscribers: rwbarton, thomie Differential Revision: https://phabricator.haskell.org/D3568
* Treat banged bindings as FunBindsBen Gamari2017-05-081-3/+3
| | | | | | | | | | | | | | | | This reworks the HsSyn representation to make banged variable patterns (e.g. !x = e) be represented as FunBinds instead of PatBinds, adding a flag to FunRhs to record the bang. Fixes #13594. Reviewers: austin, goldfire, alanz, simonpj Reviewed By: simonpj Subscribers: simonpj, rwbarton, thomie, mpickering Differential Revision: https://phabricator.haskell.org/D3525
* Make XNegativeLiterals treat -0.0 as negative 0Nolan2017-05-081-7/+13
| | | | | | | | | | | | Reviewers: austin, goldfire, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, mpickering GHC Trac Issues: #13211 Differential Revision: https://phabricator.haskell.org/D3543
* Fix #13233 by checking for lev-poly primopsRichard Eisenberg2017-05-021-1/+1
| | | | | | | | | | | | | | | The implementation plan is all in Note [Detecting forced eta expansion] in DsExpr. Test Plan: ./validate, codeGen/should_fail/T13233 Reviewers: simonpj, austin, bgamari Subscribers: rwbarton, thomie GHC Trac Issues: #13233 Differential Revision: https://phabricator.haskell.org/D3490
* Typos in comments [ci skip]Gabor Greif2017-04-111-1/+1
|
* Read COMPLETE sets from external packagesBen Gamari2017-03-061-5/+6
| | | | | | | | | | | | | | | | | | | | | | Currently, `COMPLETE` pragmas are not read from external packages at all, which quite limits their usefulness. This extends `ExternalPackageState` to include `COMPLETE` sets from other packages, and plumbs around the appropriate values to make it work the way you'd expect it to. Requires a `binary` submodule update. Fixes #13350. Test Plan: make test TEST=T13350 Reviewers: rwbarton, mpickering, austin, simonpj, bgamari Reviewed By: simonpj Subscribers: simonpj, thomie Differential Revision: https://phabricator.haskell.org/D3257
* Revert "Read COMPLETE sets from external packages"Ben Gamari2017-03-031-6/+5
| | | | This reverts commit 0d2f733050ff656b827351108d988e09abc363fc.
* Read COMPLETE sets from external packagesRyan Scott2017-03-021-5/+6
| | | | | | | | | | | | | | | | | | | | Currently, `COMPLETE` pragmas are not read from external packages at all, which quite limits their usefulness. This extends `ExternalPackageState` to include `COMPLETE` sets from other packages, and plumbs around the appropriate values to make it work the way you'd expect it to. Fixes #13350. Test Plan: make test TEST=T13350 Reviewers: rwbarton, mpickering, austin, simonpj, bgamari Reviewed By: simonpj Subscribers: simonpj, thomie Differential Revision: https://phabricator.haskell.org/D3257
* Kill inaccessible-branch complaints in record updateSimon Peyton Jones2017-02-081-2/+26
| | | | | | | | | | Trac #12957 (the original case in the Description) showed a record update that yielded an "inaccessible code" warning. This should not happen; it's just some redundant code generated by the desugarer (later pruned away) and it's not the user's fault. This patch suppresses the warning. See Check.hs Note [Inaccessible warnings for record updates]
* Typos in comments [skip ci]Gabor Greif2017-02-061-1/+1
|
* Don't return empty initial uncovered set for an unsat contextMatthew Pickering2017-02-051-7/+6
| | | | | | | | | | | | | | | | | | | | Previously when the checker encountered an unsatisfiable term of type context it would return an empty initial uncovered set. This caused all pattern matches in the context to be reported as redudant. This is arguably correct behaviour as they will never be reached but it is better to recover and provide accurate warnings for these cases to avoid error cascades. It would perhaps be better to report an error to the user about an inacessible branch but this is certainly better than many confusing redundant match warnings. Reviewers: gkaracha, austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D3064
* Remove INLINE pragma on loopbreakerMatthew Pickering2017-02-021-1/+0
|
* Exhaustiveness check for EmptyCase (Trac #10746)George Karachalias2017-02-021-16/+178
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Empty case expressions have strict semantics so the problem boils down to inhabitation checking for the type of the scrutinee. 3 main functions added: - pmTopNormaliseType_maybe for the normalisation of the scrutinee type - inhabitationCandidates for generating the possible patterns of the appropriate type - checkEmptyCase' to filter out the candidates that give rise to unsatisfiable constraints. See Note [Checking EmptyCase Expressions] in Check and Note [Type normalisation for EmptyCase] in FamInstEnv Test Plan: validate Reviewers: simonpj, goldfire, dfeuer, austin, bgamari Reviewed By: bgamari Subscribers: mpickering, thomie Differential Revision: https://phabricator.haskell.org/D2105 GHC Trac Issues: #10746
* COMPLETE pragmas for enhanced pattern exhaustiveness checkingMatthew Pickering2017-01-261-89/+187
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch adds a new pragma so that users can specify `COMPLETE` sets of `ConLike`s in order to sate the pattern match checker. A function which matches on all the patterns in a complete grouping will not cause the exhaustiveness checker to emit warnings. ``` pattern P :: () pattern P = () {-# COMPLETE P #-} foo P = () ``` This example would previously have caused the checker to warn that all cases were not matched even though matching on `P` is sufficient to make `foo` covering. With the addition of the pragma, the compiler will recognise that matching on `P` alone is enough and not emit any warnings. Reviewers: goldfire, gkaracha, alanz, austin, bgamari Reviewed By: alanz Subscribers: lelf, nomeata, gkaracha, thomie Differential Revision: https://phabricator.haskell.org/D2669 GHC Trac Issues: #8779
* Refactor Pattern Match Checker to use ListTMatthew Pickering2016-11-291-111/+215
| | | | | | | | | | Reviewers: bgamari, austin Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2725
* Add tracing infrastructure to pattern match checkerMatthew Pickering2016-11-061-3/+57
| | | | | | | | | | | | | | | | Summary: This is the start of some tracing infrastructure which I found useful when working through how the pattern match checker worked. It adds the flag -ddump-ec-trace in order to turn on the trace. Reviewers: austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2658
* Check.hs: Use actual import lists instead of commentsÖmer Sinan Ağacan2016-09-291-9/+8
|
* Implement unboxed sum primitive typeÖmer Sinan Ağacan2016-07-211-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: This patch implements primitive unboxed sum types, as described in https://ghc.haskell.org/trac/ghc/wiki/UnpackedSumTypes. Main changes are: - Add new syntax for unboxed sums types, terms and patterns. Hidden behind `-XUnboxedSums`. - Add unlifted unboxed sum type constructors and data constructors, extend type and pattern checkers and desugarer. - Add new RuntimeRep for unboxed sums. - Extend unarise pass to translate unboxed sums to unboxed tuples right before code generation. - Add `StgRubbishArg` to `StgArg`, and a new type `CmmArg` for better code generation when sum values are involved. - Add user manual section for unboxed sums. Some other changes: - Generalize `UbxTupleRep` to `MultiRep` and `UbxTupAlt` to `MultiValAlt` to be able to use those with both sums and tuples. - Don't use `tyConPrimRep` in `isVoidTy`: `tyConPrimRep` is really wrong, given an `Any` `TyCon`, there's no way to tell what its kind is, but `kindPrimRep` and in turn `tyConPrimRep` returns `PtrRep`. - Fix some bugs on the way: #12375. Not included in this patch: - Update Haddock for new the new unboxed sum syntax. - `TemplateHaskell` support is left as future work. For reviewers: - Front-end code is mostly trivial and adapted from unboxed tuple code for type checking, pattern checking, renaming, desugaring etc. - Main translation routines are in `RepType` and `UnariseStg`. Documentation in `UnariseStg` should be enough for understanding what's going on. Credits: - Johan Tibell wrote the initial front-end and interface file extensions. - Simon Peyton Jones reviewed this patch many times, wrote some code, and helped with debugging. Reviewers: bgamari, alanz, goldfire, RyanGlScott, simonpj, austin, simonmar, hvr, erikd Reviewed By: simonpj Subscribers: Iceland_jack, ggreif, ezyang, RyanGlScott, goldfire, thomie, mpickering Differential Revision: https://phabricator.haskell.org/D2259
* Merge MatchFixity and HsMatchContextAlan Zimmerman2016-06-061-2/+3
| | | | | | | | | | | | | | | | | | | | | | | | | Summary: MatchFixity was introduced to facilitate use of API Annotations. HsMatchContext does the same thing with more detail, but is chased through all over the place to provide context when processing a Match. Since we already have MatchFixity in the Match, it may as well provide the full context. updates submodule haddock Test Plan: ./validate Reviewers: austin, goldfire, bgamari Subscribers: thomie, mpickering Differential Revision: https://phabricator.haskell.org/D2271 GHC Trac Issues: #12105 (cherry picked from commit 306ecad591951521ac3f5888ca8be85bf749d271)
* Add flag to control number of missing patterns in warningsDavid Luposchainsky2016-04-171-10/+8
| | | | | | | | | | | | | | | | | | Non-exhaustive pattern warnings had their number of patterns to show hardcoded in the past. This patch implements the TODO remark that this should be made a command line flag. -fmax-uncovered-patterns=<n> can now be used to influence the number of patterns to be shown. Reviewers: hvr, austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2076
* Print which flag controls emitted desugaring warningsHerbert Valerio Riedel2016-02-271-15/+25
| | | | | | | | | | | 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
* (Alternative way to) address #8710George Karachalias2016-02-251-19/+26
| | | | | | | | | | | | | | | | | | | | | | | | 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
* Fix a few loose ends from D1795Ben Gamari2016-02-041-1/+1
| | | | George updated the Diff but I didn't noticed until it was too late.
* Overhaul the Overhauled Pattern Match CheckerGeorge Karachalias2016-02-041-703/+533
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Overhaul the Overhauled Pattern Match Checker * Changed the representation of Value Set Abstractions. Instead of using a prefix tree, we now use a list of Value Vector Abstractions. The set of constraints Delta for every Value Vector Abstraction is the oracle state so that we solve everything only once. * Instead of doing everything lazily, we prune at once (and in general everything is much stricter). Hence, an example written with pattern guards is checked in almost the same time as the equivalent with pattern matching. * Do not store the covered and the divergent sets at all. Since what we only need is a yes/no (does this clause cover anything? Does it force any thunk?) We just keep a boolean for each. * Removed flags `-Wtoo-many-guards` and `-ffull-guard-reasoning`. Replaced with `fmax-pmcheck-iterations=n`. Still debatable what should the default `n` be. * When a guard is for sure not going to contribute anything, we treat it as such: The oracle is not called and cases `CGuard`, `UGuard` and `DGuard` from the paper are not happening at all (the generation of a fresh variable, the unfolding of the pattern list etc.). his combined with the above seems to be enough to drop the memory increase for test T783 down to 18.7%. * Do not export function `dsPmWarn` (it is now called directly from within `checkSingle` and `checkMatches`). * Make `PmExprVar` hold a `Name` instead of an `Id`. The term oracle does not handle type information so using `Id` was a waste of time/space. * Added testcases T11195, T11303b (data families) and T11374 The patch addresses at least the following: Trac #11195, #11276, #11303, #11374, #11162 Test Plan: validate Reviewers: goldfire, bgamari, hvr, austin Subscribers: simonpj, thomie Differential Revision: https://phabricator.haskell.org/D1795
* Rename "open" subst functionsBartosz Nitka2016-01-271-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | This is the renaming that @simonpj requested: ``` · zipOpenTCvSubst -> zipTvSubst (It only deals with tyvars) · zipOpenTCvSubstCoVars -> zipCvSubst (it only deals with covars) · zipOpenTCvSubstBinders -> zipTyBinderSubst (it only deals with TyBinders, not covars) ``` plus the `mk` variant. Test Plan: ./validate Reviewers: simonpj, goldfire, austin, bgamari Subscribers: thomie, simonpj Differential Revision: https://phabricator.haskell.org/D1853 GHC Trac Issues: #11371
* Refactor the typechecker to use ExpTypes.Richard Eisenberg2016-01-271-75/+85
| | | | | | | | | | | | | | | | | | | | | 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
* Kill off zipTopTCvSubst in favour of zipOpenTCvSubstSimon Peyton Jones2016-01-261-1/+1
| | | | | | | | | | | | | | As Bartosz has discovered, the invariants for substitutions were wrong, and in particular the "mkTop...Subst" and "zipTop..Subst" functions were building substitutions that didn't obey even the old invariants. This patch kills of the bogus zipTopTCvSubst in favour of the more robust zipOpenTCvSubst. I tripped over this because my upcoming patch (concerning SetLevels, Trac #11330) triggered an ASSERT failure in the substitution well-formedness assertion in TyCoRep.
* Replace calls to `ptext . sLit` with `text`Jan Stolarek2016-01-181-17/+17
| | | | | | | | | | | | | | | | | | | | Summary: In the past the canonical way for constructing an SDoc string literal was the composition `ptext . sLit`. But for some time now we have function `text` that does the same. Plus it has some rules that optimize its runtime behaviour. This patch takes all uses of `ptext . sLit` in the compiler and replaces them with calls to `text`. The main benefits of this patch are clener (shorter) code and less dependencies between module, because many modules now do not need to import `FastString`. I don't expect any performance benefits - we mostly use SDocs to report errors and it seems there is little to be gained here. Test Plan: ./validate Reviewers: bgamari, austin, goldfire, hvr, alanz Subscribers: goldfire, thomie, mpickering Differential Revision: https://phabricator.haskell.org/D1784
* Avoid generating guards for CoPats if possible (Addresses #11276)George Karachalias2016-01-041-5/+24
| | | | | | | | | | | | | | | | When translating a `CoPat` to `PmPat` check whether the wrapper is just a hole or a cast with refl. In these cases we can safely drop the wrapper and generate less guard patterns. Fixes T11276. Test Plan: validate Reviewers: bgamari, austin Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D1729 GHC Trac Issues: #11276
* Address #11245: Ensure the non-matched list is always non-emptyGeorge Karachalias2015-12-301-3/+5
| | | | | | | | | | | | | | | | | | When there is an uncovered vector of length 0 (which in turn means that it represents a guard failure) print "(incomplete guards)" instead of an empty list of non-covered vectors. Test Plan: validate Reviewers: austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D1717 GHC Trac Issues: #11245
* Introduce negative patterns for literals (addresses #11303)George Karachalias2015-12-291-17/+74
| | | | | | | | | | | | | | | | | | | | Introduce negative patterns for literals. In addition to storing term constraints for literals (checked at the end by the term oracle), also check eagerly, using negative patterns. This means generation of smaller sets (covered, uncovered, and divergent), instead of generating big sets and pruning afterwards. Test Plan: validate Reviewers: austin, bgamari Reviewed By: bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D1716 GHC Trac Issues: #11303
* Adding flags: -ffull-guard-reasoning and too-many-guardsGeorge Karachalias2015-12-271-154/+204
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduction of two new flags, for more precise control over the new pattern match checker's behaviour when reasoning about guards. This is supposed to address #11195 (and maybe more performance bugs related to the NP-Hardness of coverage checking). Expected behaviour: * When `-ffull-guard-reasoning` is on, run the new pattern match checker in its full power * When `-ffull-guard-reasoning` is off (the default), for every match, check a metric to see whether pattern match checking for it has high probability of being non performant (at the the moment we check whether the number of guards is over 20 but I would like to use a more precise measure in the future). If the probability is high: - Oversimplify the guards (less expressive but more performant) and run the checker, and - Issue a warning about the simplification that happened. A new flag `-Wtoo-many-guards/-Wno-too-many-guards` suppresses the warning about the simplification (useful when combined with -Werror). Test Plan: validate Reviewers: goldfire, austin, hvr, bgamari Reviewed By: bgamari Subscribers: mpickering, thomie Differential Revision: https://phabricator.haskell.org/D1676 GHC Trac Issues: #11195
* Add kind equalities to GHC.Richard Eisenberg2015-12-111-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* pmcheck: Comments about undecidability of literal equalityGeorge Karachalias2015-12-051-0/+3
|
* pmcheck: Comments about term equality representationGeorge Karachalias2015-12-051-0/+63
|
* Check: More Clang/CPP wibblesBen Gamari2015-12-041-5/+5
|
* Improve performance for PM check on literals (Fixes #11160 and #11161)George Karachalias2015-12-041-84/+44
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Two changes: 1. Instead of generating constraints of the form (x ~ e) (as we do in the paper), generate constraints of the form (e ~ e). The term oracle (`tmOracle` in deSugar/TmOracle.hs) is not really efficient and in the presence of many (x ~ e) constraints behaves quadratically. For literals, constraints of the form (False ~ (x ~ lit)) are pretty common, so if we start with { y ~ False, y ~ (x ~ lit) } we end up givng to the solver (a) twice as many constraints as we need and (b) half of them trigger the solver's weakness. This fixes #11160. 2. Treat two overloaded literals that look different as different. This is not entirely correct but it is what both the previous and the current check did. I had the ambitious plan to do the *right thing* (equality between overloaded literals is undecidable in the general case) and just use this assumption when issuing the warnings. It seems to generate much more constraints than I expected (breaks #11161) so I just do it immediately now instead of generating everything and filtering afterwards. Even if it is not (strictly speaking) correct, we have the following: * Gives the "expected" warnings (the ones Ocaml or the previous algorithm would give) and, * Most importantly, it is safe. Unless a catch-all clause exists, a match against literals is always non-exhaustive. So, effectively this affects only what is shown to the user (and, evidently, performance!).