summaryrefslogtreecommitdiff
path: root/compiler/deSugar/PmExpr.hs
Commit message (Collapse)AuthorAgeFilesLines
* Extract PmTypes module from PmExpr and PmOracleSebastian Graf2019-09-191-364/+0
| | | | | | | | | | | Apparently ghc-lib-parser's API blew up because the newly induced cyclic dependency between TcRnTypes and PmOracle pulled in the other half of GHC into the relevant strongly-connected component. This patch arranges it so that PmTypes exposes mostly data type definitions and type class instances to be used within PmOracle, without importing the any of the possibly offending modules DsMonad, TcSimplify and FamInst.
* Encode shape information in `PmOracle`Sebastian Graf2019-09-161-183/+267
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, we had an elaborate mechanism for selecting the warnings to generate in the presence of different `COMPLETE` matching groups that, albeit finely-tuned, produced wrong results from an end user's perspective in some cases (#13363). The underlying issue is that at the point where the `ConVar` case has to commit to a particular `COMPLETE` group, there's not enough information to do so and the status quo was to just enumerate all possible complete sets nondeterministically. The `getResult` function would then pick the outcome according to metrics defined in accordance to the user's guide. But crucially, it lacked knowledge about the order in which affected clauses appear, leading to the surprising behavior in #13363. In !1010 we taught the term oracle to reason about literal values a variable can certainly not take on. This MR extends that idea to `ConLike`s and thereby fixes #13363: Instead of committing to a particular `COMPLETE` group in the `ConVar` case, we now split off the matching constructor incrementally and record the newly covered case as a refutable shape in the oracle. Whenever the set of refutable shapes covers any `COMPLETE` set, the oracle recognises vacuosity of the uncovered set. This patch goes a step further: Since at this point the information in value abstractions is merely a cut down representation of what the oracle knows, value abstractions degenerate to a single `Id`, the semantics of which is determined by the oracle state `Delta`. Value vectors become lists of `[Id]` given meaning to by a single `Delta`, value set abstractions (of which the uncovered set is an instance) correspond to a union of `Delta`s which instantiate the same `[Id]` (akin to models of formula). Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149 ------------------------- Metric Decrease: ManyAlternatives T11195 -------------------------
* TmOracle: Replace negative term equalities by refutable PmAltConsSebastian Graf2019-06-071-237/+51
| | | | | | | | | | | | | | | | | | | | | | | | | The `PmExprEq` business was a huge hack and was at the same time vastly too powerful and not powerful enough to encode negative term equalities, i.e. facts of the form "forall y. x ≁ Just y". This patch introduces the concept of 'refutable shapes': What matters for the pattern match checker is being able to encode knowledge of the kind "x can no longer be the literal 5". We encode this knowledge in a `PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are just `PmLit`s at the moment) to each variable denoting above inequalities. So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and try to solve an equality like `x ~ 42`. The entry in the refutable environment will immediately lead to a contradiction. This machinery renders the whole `PmExprEq` and `ComplexEq` business unnecessary, getting rid of a lot of (mostly dead) code. See the Note [Refutable shapes] in TmOracle for a place to start. Metric Decrease: T11195
* [TTG: Handling Source Locations] Foundation and PatShayan-Najd2018-11-241-4/+5
| | | | | | | | | | | | | | | | | | This patch removes the ping-pong style from HsPat (only, for now), using the plan laid out at https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/HandlingSourceLocations (solution A). - the class `HasSrcSpan`, and its functions (e.g., `cL` and `dL`), are introduced - some instances of `HasSrcSpan` are introduced - some constructors `L` are replaced with `cL` - some patterns `L` are replaced with `dL->L` view pattern - some type annotation are necessarily updated (e.g., `Pat p` --> `Pat (GhcPass p)`) Phab diff: D5036 Trac Issues #15495 Updates haddock submodule
* More explicit foralls (GHC Proposal 0007)Matthew Yacavone2018-10-271-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | Allow the user to explicitly bind type/kind variables in type and data family instances (including associated instances), closed type family equations, and RULES pragmas. Follows the specification of GHC Proposal 0007, also fixes #2600. Advised by Richard Eisenberg. This modifies the Template Haskell AST -- old code may break! Other Changes: - convert HsRule to a record - make rnHsSigWcType more general - add repMaybe to DsMeta Includes submodule update for Haddock. Test Plan: validate Reviewers: goldfire, bgamari, alanz Subscribers: simonpj, RyanGlScott, goldfire, rwbarton, thomie, mpickering, carter GHC Trac Issues: #2600, #14268 Differential Revision: https://phabricator.haskell.org/D4894
* Improve exhaustiveness checking for literal values and patterns, fix #14546HE, Tao2018-06-031-7/+28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, we parse both the **integral literal** value and the patterns as `OverLit HsIntegral`. For example: ``` case 0::Int of 0 -> putStrLn "A" 1 -> putStrLn "B" _ -> putStrLn "C" ``` When checking the exhaustiveness of pattern matching, we translate the `0` in value position as `PmOLit`, but translate the `0` and `1` in pattern position as `PmSLit`. The inconsistency leads to the failure of `eqPmLit` to detect the equality and report warning of "Pattern match is redundant" on pattern `0`, as reported in #14546. In this patch we remove the specialization of `OverLit` patterns, and keep the overloaded number literal in pattern as it is to maintain the consistency. Now we can capture the exhaustiveness of pattern `0` and the redundancy of pattern `1` and `_`. For **string literals**, we parse the string literals as `HsString`. When `OverloadedStrings` is enabled, it further be turned as `HsOverLit HsIsString`, whether it's type is `String` or not. For example: ``` case "foo" of "foo" -> putStrLn "A" "bar" -> putStrLn "B" "baz" -> putStrLn "C" ``` Previously, the overloaded string values are translated to `PmOLit` and the non-overloaded string values are translated to `PmSLit`. However the string patterns, both overloaded and non-overloaded, are translated to list of characters. The inconsistency leads to wrong warnings about redundant and non-exhaustive pattern matching warnings, as reported in #14546. In order to catch the redundant pattern in following case: ``` case "foo" of ('f':_) -> putStrLn "A" "bar" -> putStrLn "B" ``` In this patch, we translate non-overloaded string literals, both in value position and pattern position, as list of characters. For overloaded string literals, we only translate it to list of characters only when it's type is `stringTy`, since we know nothing about the `toString` methods. But we know that if two overloaded strings are syntax equal, then they are equal. Then if it's type is not `stringTy`, we just translate it to `PmOLit`. We can still capture the exhaustiveness of pattern `"foo"` and the redundancy of pattern `"bar"` and `"baz"` in the following code: ``` {-# LANGUAGE OverloadedStrings #-} main = do case "foo" of "foo" -> putStrLn "A" "bar" -> putStrLn "B" "baz" -> putStrLn "C" ``` Test Plan: make test TEST="T14546" Reviewers: bgamari, simonpj Reviewed By: bgamari, simonpj Subscribers: simonpj, thomie, carter GHC Trac Issues: #14546 Differential Revision: https://phabricator.haskell.org/D4571
* vectorise: Put it out of its miseryBen Gamari2018-06-021-9/+3
| | | | | | | | | | | | | | | | | | | | | Poor DPH and its vectoriser have long been languishing; sadly it seems there is little chance that the effort will be rekindled. Every few years we discuss what to do with this mass of code and at least once we have agreed that it should be archived on a branch and removed from `master`. Here we do just that, eliminating heaps of dead code in the process. Here we drop the ParallelArrays extension, the vectoriser, and the `vector` and `primitive` submodules. Test Plan: Validate Reviewers: simonpj, simonmar, hvr, goldfire, alanz Reviewed By: simonmar Subscribers: goldfire, rwbarton, thomie, mpickering, carter Differential Revision: https://phabricator.haskell.org/D4761
* Restore Trees That Grow reverted commitsAlan Zimmerman2018-04-091-20/+19
| | | | | | | | | | | | | | | | | | The following commits were reverted prior to the release of GHC 8.4.1, because the time to derive Data instances was too long [1]. 438dd1cbba13d35f3452b4dcef3f94ce9a216905 Phab:D4147 e3ec2e7ae94524ebd111963faf34b84d942265b4 Phab:D4177 47ad6578ea460999b53eb4293c3a3b3017a56d65 Phab:D4186 The work is continuing, as the minimum bootstrap compiler is now GHC 8.2.1, and this allows Plan B[2] for instances to be used. This will land in a following commit. Updates Haddock submodule [1] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/Instances [2] https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/Instances#PLANB
* Revert "trees that grow" workBen Gamari2017-11-211-19/+20
| | | | | | | | | | | | | | As documented in #14490, the Data instances currently blow up compilation time by too much to stomach. Alan will continue working on this in a branch and we will perhaps merge to 8.2 before 8.2.1 to avoid having to perform painful cherry-picks in 8.2 minor releases. Reverts haddock submodule. This reverts commit 47ad6578ea460999b53eb4293c3a3b3017a56d65. This reverts commit e3ec2e7ae94524ebd111963faf34b84d942265b4. This reverts commit 438dd1cbba13d35f3452b4dcef3f94ce9a216905. This reverts commit 0ff152c9e633accca48815e26e59d1af1fe44ceb.
* TTG3 Combined Step 1 and 3 for Trees That GrowAlan Zimmerman2017-11-141-1/+1
| | | | | | | | | | | | | | | | | | | Further progress on implementing Trees that Grow on hsSyn AST. See https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow Trees that grow extension points are added for - Rest of HsExpr.hs Updates haddock submodule Test Plan: ./validate Reviewers: bgamari, shayan-najd, goldfire Subscribers: goldfire, rwbarton, thomie, mpickering Differential Revision: https://phabricator.haskell.org/D4186
* WIP on combined Step 1 and 3 for Trees That Grow, HsExprAlan Zimmerman2017-11-111-19/+18
| | | | | | | | | | | | | | | | | See https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow Trees that grow extension points are added for - HsExpr Updates haddock submodule Test Plan: ./validate Reviewers: bgamari, goldfire Subscribers: rwbarton, thomie, shayan-najd, mpickering Differential Revision: https://phabricator.haskell.org/D4177
* 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
* Udate hsSyn AST to use Trees that GrowAlan Zimmerman2017-06-061-6/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* COMPLETE pragmas for enhanced pattern exhaustiveness checkingMatthew Pickering2017-01-261-24/+33
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Update levity polymorphismRichard Eisenberg2017-01-191-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Spelling fixes in comments [ci skip]Gabor Greif2017-01-181-1/+1
|
* Overhaul the Overhauled Pattern Match CheckerGeorge Karachalias2016-02-041-13/+18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Refactor the typechecker to use ExpTypes.Richard Eisenberg2016-01-271-1/+4
| | | | | | | | | | | | | | | | | | | | | 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
* Replace calls to `ptext . sLit` with `text`Jan Stolarek2016-01-181-3/+2
| | | | | | | | | | | | | | | | | | | | 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
* Work SourceText in for all integer literalsAlan Zimmerman2016-01-161-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Summary: Certain syntactic elements have integers in them, such as fixity specifications, SPECIALISE pragmas and so on. The lexer will accept mult-radix literals, with arbitrary leading zeros in these. Bring in a SourceText field to each affected AST element to capture the original literal text for use with API Annotations. Affected hsSyn elements are ``` -- See note [Pragma source text] data Activation = NeverActive | AlwaysActive | ActiveBefore SourceText PhaseNum -- Active only *strictly before* this phase | ActiveAfter SourceText PhaseNum -- Active in this phase and later deriving( Eq, Data, Typeable ) -- Eq used in comparing rules in HsDecls data Fixity = Fixity SourceText Int FixityDirection -- Note [Pragma source text] deriving (Data, Typeable) ``` and ``` | HsTickPragma -- A pragma introduced tick SourceText -- Note [Pragma source text] in BasicTypes (StringLiteral,(Int,Int),(Int,Int)) -- external span for this tick ((SourceText,SourceText),(SourceText,SourceText)) -- Source text for the four integers used in the span. -- See note [Pragma source text] in BasicTypes (LHsExpr id) ``` Updates haddock submodule Test Plan: ./validate Reviewers: goldfire, bgamari, austin Reviewed By: bgamari Subscribers: thomie, mpickering Differential Revision: https://phabricator.haskell.org/D1781 GHC Trac Issues: #11430
* Drop pre-AMP compatibility CPP conditionalsHerbert Valerio Riedel2015-12-311-3/+0
| | | | | | | | | | | | Since GHC 8.1/8.2 only needs to be bootstrap-able by GHC 7.10 and GHC 8.0 (and GHC 8.2), we can now finally drop all that pre-AMP compatibility CPP-mess for good! Reviewers: austin, goldfire, bgamari Subscribers: goldfire, thomie, erikd Differential Revision: https://phabricator.haskell.org/D1724
* Add kind equalities to GHC.Richard Eisenberg2015-12-111-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-7/+68
|
* PmExpr: Fix CPP unacceptable too clang's CPPBen Gamari2015-12-041-1/+1
|
* Improve performance for PM check on literals (Fixes #11160 and #11161)George Karachalias2015-12-041-15/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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!).
* Major Overhaul of Pattern Match Checking (Fixes #595)George Karachalias2015-12-031-0/+377
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.
View Lorry Controller Status