summaryrefslogtreecommitdiff
path: root/testsuite/tests/quantified-constraints
Commit message (Collapse)AuthorAgeFilesLines
* matchLocalInst: do domination analysissheaf2022-09-287-0/+130
| | | | | | | | | | | | | | | | | | | | | | | | | | When multiple Given quantified constraints match a Wanted, and there is a quantified constraint that dominates all others, we now pick it to solve the Wanted. See Note [Use only the best matching quantified constraint]. For example: [G] d1: forall a b. ( Eq a, Num b, C a b ) => D a b [G] d2: forall a . C a Int => D a Int [W] {w}: D a Int When solving the Wanted, we find that both Givens match, but we pick the second, because it has a weaker precondition, C a Int, compared to (Eq a, Num Int, C a Int). We thus say that d2 dominates d1; see Note [When does a quantified instance dominate another?]. This domination test is done purely in terms of superclass expansion, in the function GHC.Tc.Solver.Interact.impliedBySCs. We don't attempt to do a full round of constraint solving; this simple check suffices for now. Fixes #22216 and #22223
* Diagnostic codes: acccept test changessheaf2022-09-137-13/+13
| | | | | | | | The testsuite output now contains diagnostic codes, so many tests need to be updated at once. We decided it was best to keep the diagnostic codes in the testsuite output, so that contributors don't inadvertently make changes to the diagnostic codes.
* Print constraints in quotes (#21167)Swann Moreau2022-08-192-2/+2
| | | | | | | This patch improves the uniformity of error message formatting by printing constraints in quotes, as we do for types. Fix #21167
* Deprecate TypeInType extensionHaskellMouse2022-06-061-1/+2
| | | | | | | | | | | | | | | | This commit fixes #20312 It deprecates "TypeInType" extension according to the following proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0083-no-type-in-type.rst It has been already implemented. The migration strategy: 1. Disable TypeInType 2. Enable both DataKinds and PolyKinds extensions Metric Decrease: T16875
* Export (~) from Data.Type.Equality (#18862)wip/eqtycon-rnVladislav Zavialov2022-03-152-2/+2
| | | | | | | | | | * Users can define their own (~) type operator * Haddock can display documentation for the built-in (~) * New transitional warnings implemented: -Wtype-equality-out-of-scope -Wtype-equality-requires-operators Updates the haddock submodule.
* Kill derived constraintsRichard Eisenberg2022-02-231-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Co-authored by: Sam Derbyshire Previously, GHC had three flavours of constraint: Wanted, Given, and Derived. This removes Derived constraints. Though serving a number of purposes, the most important role of Derived constraints was to enable better error messages. This job has been taken over by the new RewriterSets, as explained in Note [Wanteds rewrite wanteds] in GHC.Tc.Types.Constraint. Other knock-on effects: - Various new Notes as I learned about under-described bits of GHC - A reshuffling around the AST for implicit-parameter bindings, with better integration with TTG. - Various improvements around fundeps. These were caused by the fact that, previously, fundep constraints were all Derived, and Derived constraints would get dropped. Thus, an unsolved Derived didn't stop compilation. Without Derived, this is no longer possible, and so we have to be considerably more careful around fundeps. - A nice little refactoring in GHC.Tc.Errors to center the work on a new datatype called ErrorItem. Constraints are converted into ErrorItems at the start of processing, and this allows for a little preprocessing before the main classification. - This commit also cleans up the behavior in generalisation around functional dependencies. Now, if a variable is determined by functional dependencies, it will not be quantified. This change is user facing, but it should trim down GHC's strange behavior around fundeps. - Previously, reportWanteds did quite a bit of work, even on an empty WantedConstraints. This commit adds a fast path. - Now, GHC will unconditionally re-simplify constraints during quantification. See Note [Unconditionally resimplify constraints when quantifying], in GHC.Tc.Solver. Close #18398. Close #18406. Solve the fundep-related non-confluence in #18851. Close #19131. Close #19137. Close #20922. Close #20668. Close #19665. ------------------------- Metric Decrease: LargeRecord T9872b T9872b_defer T9872d TcPlugin_RewritePerf -------------------------
* Add test for #21037sheaf2022-02-092-0/+25
| | | | | | | This program was rejected by GHC 9.2, but is accepted on newer versions of GHC. This patch adds a regression test. Closes #21037
* Set the TcLclEnv when solving a ForAll constraintSimon Peyton Jones2022-01-274-2/+24
| | | | | | | Fix a simple omission in GHC.Tc.Solver.Canonical.solveForAll, where we ended up with the wrong TcLclEnv captured in an implication. Result: unhelpful error message (#21006)
* Use diagnostic infrastructure in GHC.Tc.Errorssheaf2022-01-171-1/+1
|
* Convert diagnostics in GHC.Tc.Validity to proper TcRnMessage.hainq2021-09-013-0/+19
| | | | | | | | | | | | | | | | | | | | - Add 19 new messages. Update test outputs accordingly. - Pretty print suggest-extensions hints: remove space before interspersed commas. - Refactor Rank's MonoType constructors. Each MonoType constructor should represent a specific case. With the Doc suggestion belonging to the TcRnMessage diagnostics instead. - Move Rank from Validity to its own `GHC.Tc.Types.Rank` module. - Remove the outdated `check_irred_pred` check. - Remove the outdated duplication check in `check_valid_theta`, which was subsumed by `redundant-constraints`. - Add missing test cases for quantified-constraints/T16474 & th/T12387a.
* Add regression test for #19921Zubin Duggal2021-06-253-0/+39
|
* Use GHC2021 as default languageJoachim Breitner2021-03-103-0/+3
|
* Fixes to dealing with the export of mainSimon Peyton Jones2021-03-091-3/+0
| | | | | | | | | | | | | | | | | | | | It's surprisingly tricky to deal with 'main' (#19397). This patch does quite bit of refactoring do to it right. Well, more-right anyway! The moving parts are documented in GHC.Tc.Module Note [Dealing with main] Some other oddments: * Rename tcRnExports to rnExports; no typechecking here! * rnExports now uses checkNoErrs rather than failIfErrsM; the former fails only if rnExports itself finds errors * Small improvements to tcTyThingCategory, which ultimately weren't important to the patch, but I've retained as a minor improvement.
* Clean up the inferred type variable restrictionRyan Scott2020-07-302-0/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch primarily: * Documents `checkInferredVars` (previously called `check_inferred_vars`) more carefully. This is the function which throws an error message if a user quantifies an inferred type variable in a place where specificity cannot be observed. See `Note [Unobservably inferred type variables]` in `GHC.Rename.HsType`. Note that I now invoke `checkInferredVars` _alongside_ `rnHsSigType`, `rnHsWcSigType`, etc. rather than doing so _inside_ of these functions. This results in slightly more call sites for `checkInferredVars`, but it makes it much easier to enumerate the spots where the inferred type variable restriction comes into effect. * Removes the inferred type variable restriction for default method type signatures, per the discussion in #18432. As a result, this patch fixes #18432. Along the way, I performed some various cleanup: * I moved `no_nested_foralls_contexts_err` into `GHC.Rename.Utils` (under the new name `noNestedForallsContextsErr`), since it now needs to be invoked from multiple modules. I also added a helper function `addNoNestedForallsContextsErr` that throws the error message after producing it, as this is a common idiom. * In order to ensure that users cannot sneak inferred type variables into `SPECIALISE instance` pragmas by way of nested `forall`s, I now invoke `addNoNestedForallsContextsErr` when renaming `SPECIALISE instance` pragmas, much like when we rename normal instance declarations. (This probably should have originally been done as a part of the fix for #18240, but this task was somehow overlooked.) As a result, this patch fixes #18455 as a side effect.
* Simple subsumptionwip/T17775Simon Peyton Jones2020-06-053-10/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch simplifies GHC to use simple subsumption. Ticket #17775 Implements GHC proposal #287 https://github.com/ghc-proposals/ghc-proposals/blob/master/ proposals/0287-simplify-subsumption.rst All the motivation is described there; I will not repeat it here. The implementation payload: * tcSubType and friends become noticably simpler, because it no longer uses eta-expansion when checking subsumption. * No deeplyInstantiate or deeplySkolemise That in turn means that some tests fail, by design; they can all be fixed by eta expansion. There is a list of such changes below. Implementing the patch led me into a variety of sticky corners, so the patch includes several othe changes, some quite significant: * I made String wired-in, so that "foo" :: String rather than "foo" :: [Char] This improves error messages, and fixes #15679 * The pattern match checker relies on knowing about in-scope equality constraints, andd adds them to the desugarer's environment using addTyCsDs. But the co_fn in a FunBind was missed, and for some reason simple-subsumption ends up with dictionaries there. So I added a call to addTyCsDs. This is really part of #18049. * I moved the ic_telescope field out of Implication and into ForAllSkol instead. This is a nice win; just expresses the code much better. * There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader. We called checkDataKindSig inside tc_kind_sig, /before/ solveEqualities and zonking. Obviously wrong, easily fixed. * solveLocalEqualitiesX: there was a whole mess in here, around failing fast enough. I discovered a bad latent bug where we could successfully kind-check a type signature, and use it, but have unsolved constraints that could fill in coercion holes in that signature -- aargh. It's all explained in Note [Failure in local type signatures] in GHC.Tc.Solver. Much better now. * I fixed a serious bug in anonymous type holes. IN f :: Int -> (forall a. a -> _) -> Int that "_" should be a unification variable at the /outer/ level; it cannot be instantiated to 'a'. This was plain wrong. New fields mode_lvl and mode_holes in TcTyMode, and auxiliary data type GHC.Tc.Gen.HsType.HoleMode. This fixes #16292, but makes no progress towards the more ambitious #16082 * I got sucked into an enormous refactoring of the reporting of equality errors in GHC.Tc.Errors, especially in mkEqErr1 mkTyVarEqErr misMatchMsg misMatchMsgOrCND In particular, the very tricky mkExpectedActualMsg function is gone. It took me a full day. But the result is far easier to understand. (Still not easy!) This led to various minor improvements in error output, and an enormous number of test-case error wibbles. One particular point: for occurs-check errors I now just say Can't match 'a' against '[a]' rather than using the intimidating language of "occurs check". * Pretty-printing AbsBinds Tests review * Eta expansions T11305: one eta expansion T12082: one eta expansion (undefined) T13585a: one eta expansion T3102: one eta expansion T3692: two eta expansions (tricky) T2239: two eta expansions T16473: one eta determ004: two eta expansions (undefined) annfail06: two eta (undefined) T17923: four eta expansions (a strange program indeed!) tcrun035: one eta expansion * Ambiguity check at higher rank. Now that we have simple subsumption, a type like f :: (forall a. Eq a => Int) -> Int is no longer ambiguous, because we could write g :: (forall a. Eq a => Int) -> Int g = f and it'd typecheck just fine. But f's type is a bit suspicious, and we might want to consider making the ambiguity check do a check on each sub-term. Meanwhile, these tests are accepted, whereas they were previously rejected as ambiguous: T7220a T15438 T10503 T9222 * Some more interesting error message wibbles T13381: Fine: one error (Int ~ Exp Int) rather than two (Int ~ Exp Int, Exp Int ~ Int) T9834: Small change in error (improvement) T10619: Improved T2414: Small change, due to order of unification, fine T2534: A very simple case in which a change of unification order means we get tow unsolved constraints instead of one tc211: bizarre impredicative tests; just accept this for now Updates Cabal and haddock submodules. Metric Increase: T12150 T12234 T5837 haddock.base Metric Decrease: haddock.compiler haddock.Cabal haddock.base Merge note: This appears to break the `UnliftedNewtypesDifficultUnification` test. It has been marked as broken in the interest of merging. (cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)
* Do eager instantation in termsSimon Peyton Jones2020-04-221-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch implements eager instantiation, a small but critical change to the type inference engine, #17173. The main change is this: When inferring types, always return an instantiated type (for now, deeply instantiated; in future shallowly instantiated) There is more discussion in https://www.tweag.io/posts/2020-04-02-lazy-eager-instantiation.html There is quite a bit of refactoring in this patch: * The ir_inst field of GHC.Tc.Utils.TcType.InferResultk has entirely gone. So tcInferInst and tcInferNoInst have collapsed into tcInfer. * Type inference of applications, via tcInferApp and tcInferAppHead, are substantially refactored, preparing the way for Quick Look impredicativity. * New pure function GHC.Tc.Gen.Expr.collectHsArgs and applyHsArgs are beatifully dual. We can see the zipper! * GHC.Tc.Gen.Expr.tcArgs is now much nicer; no longer needs to return a wrapper * In HsExpr, HsTypeApp now contains the the actual type argument, and is used in desugaring, rather than putting it in a mysterious wrapper. * I struggled a bit with good error reporting in Unify.matchActualFunTysPart. It's a little bit simpler than before, but still not great. Some smaller things * Rename tcPolyExpr --> tcCheckExpr tcMonoExpr --> tcLExpr * tcPatSig moves from GHC.Tc.Gen.HsType to GHC.Tc.Gen.Pat Metric Decrease: T9961 Reduction of 1.6% in comiler allocation on T9961, I think.
* testsuite: Add test for #15316Ben Gamari2020-02-083-0/+28
| | | | This is the full testcase for T15316.
* testsuite: Add test for #17458Ben Gamari2019-11-133-0/+59
| | | | | | As noted in #17458, QuantifiedConstraints and UndecideableInstances could previously be used to write programs which can loop at runtime. This was fixed in !1870.
* Add another test for #17267Simon Peyton Jones2019-11-013-0/+41
| | | | This one came in a comment from James Payor
* Do not add a 'solved dict' for quantified constraintsSimon Peyton Jones2019-10-1211-0/+209
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GHC has a wonderful-but-delicate mechanism for building recursive dictionaries by adding a goal to the "solved dictionaries" before solving the sub-goals. See Note [Solved dictionaries] in TcSMonad Ticket #17267 showed that if you use this mechanism for local /quantified/ constraints you can get a loop -- or even unsafe coerce. This patch fixes the bug. Specifically * Make TcSMonad.addSolvedDict be conditional on using a /top level/ instance, not a quantified one. * Moreover, we /also/ don't want to add a solved dict for equalities (a~b). * Add lots more comments to Note [Solved dictionaries] to explain the above cryptic stuff. * Extend InstanceWhat to identify those strange built-in equality instances. A couple of other things along the way * Delete the unused Type.isIPPred_maybe. * Stop making addSolvedDict conditional on not being an impolicit parameter. This comes from way back. But it's irrelevant now because IP dicts are never solved via an instance.
* Add regression test for #15918Ryan Scott2019-03-053-0/+27
| | | | | | | | The test case in #15918 no longer triggers an `ASSERT` failure on GHC HEAD, likely due to commit 682783828275cca5fd8bf5be5b52054c75e0e22c (`Make a smart mkAppTyM`). This patch adds a regression test for #15918 to finally put it to rest.
* Allow (~) in the head of a quantified constraintsSimon Peyton Jones2018-09-135-0/+66
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since the introduction of quantified constraints, GHC has rejected a quantified constraint with (~) in the head, thus f :: (forall a. blah => a ~ ty) => stuff I am frankly dubious that this is ever useful. But /is/ necessary for Coercible (representation equality version of (~)) and it does no harm to allow it for (~) as well. Plus, our users are asking for it (Trac #15359, #15625). It was really only excluded by accident, so this patch lifts the restriction. See TcCanonical Note [Equality superclasses in quantified constraints] There are a number of wrinkles: * If the context of the quantified constraint is empty, we can get trouble when we get down to unboxed equality (a ~# b) or (a ~R# b), as Trac #15625 showed. This is even more of a corner case, but it produced an outright crash, so I elaborated the superclass machinery in TcCanonical.makeStrictSuperClasses to add a void argument in this case. See Note [Equality superclasses in quantified constraints] * The restriction on (~) was in TcValidity.checkValidInstHead. In lifting the restriction I discovered an old special case for (~), namely | clas_nm `elem` [ heqTyConName, eqTyConName] , nameModule clas_nm /= this_mod This was (solely) to support the strange instance instance a ~~ b => a ~ b in Data.Type.Equality. But happily that is no longer with us, since commit f265008fb6f70830e7e92ce563f6d83833cef071 Refactor (~) to reduce the suerpclass stack So I removed the special case. * I found that the Core invariants on when we could have co = <expr> were entirely not written down. (Getting this wrong ws the proximate source of the crash in Trac #15625. So - Documented them better in CoreSyn Note [CoreSyn type and coercion invariant], - Modified CoreOpt and CoreLint to match - Modified CoreUtils.bindNonRec to match - Made MkCore.mkCoreLet use bindNonRec, rather than duplicate its logic - Made Simplify.rebuildCase case-to-let respect Note [CoreSyn type and coercion invariant],
* More refactoring in TcValiditySimon Peyton Jones2018-07-103-0/+16
| | | | | | | | | | | | | | | This patch responds to Trac #15334 by making it an error to write an instance declaration for a tuple constraint like (Eq [a], Show [a]). I then discovered that instance validity checking was scattered betweeen TcInstDcls and TcValidity, so I took the time to bring it all together, into TcValidity.checkValidInstHead In doing so I discovered that there are lot of special cases. I have not changed them, but at least they are all laid out clearly now.
* Refactor validity checking for constraintsSimon Peyton Jones2018-07-053-0/+28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There are several changes here. * TcInteract has gotten too big, so I moved all the class-instance matching out of TcInteract into a new module ClsInst. It parallels the FamInst module. The main export of ClsInst is matchGlobalInst. This now works in TcM not TcS. * A big reason to make matchGlobalInst work in TcM is that we can then use it from TcValidity.checkSimplifiableClassConstraint. That extends checkSimplifiableClassConstraint to work uniformly for built-in instances, which means that we now get a warning if we have givens (Typeable x, KnownNat n); see Trac #15322. * This change also made me refactor LookupInstResult, in particular by adding the InstanceWhat field. I also changed the name of the type to ClsInstResult. Then instead of matchGlobalInst reporting a staging error (which is inappropriate for the call from TcValidity), we can do so in TcInteract.checkInstanceOK. * In TcValidity, we now check quantified constraints for termination. For example, this signature should be rejected: f :: (forall a. Eq (m a) => Eq (m a)) => blah as discussed in Trac #15316. The main change here is that TcValidity.check_pred_help now uses classifyPredType, and has a case for ForAllPred which it didn't before. This had knock-on refactoring effects in TcValidity.
* Fix TcLevel manipulation in TcDerivInfer.simplifyDerivSimon Peyton Jones2018-06-263-0/+43
| | | | | | | | | | | | | | | | | | The level numbers we were getting simply didn't obey the invariant (ImplicInv) in TcType Note [TcLevel and untouchable type variables] That leads to chaos. Easy to fix. I improved the documentation. I also added an assertion in TcSimplify that checks that level numbers go up by 1 as we dive inside implications, so that we catch the problem at source rather than than through its obscure consequences. That in turn showed up that TcRules was also generating constraints that didn't obey (ImplicInv), so I fixed that too. I have no idea what consequences were lurking behing that bug, but anyway now it's fixed. Hooray.
* Instances in no-evidence implicationsSimon Peyton Jones2018-06-224-0/+95
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Trac #15290 showed that it's possible that we might attempt to use a quantified constraint to solve an equality in a situation where we don't have anywhere to put the evidence bindings. This made GHC crash. This patch stops the crash, but still rejects the pogram. See Note [Instances in no-evidence implications] in TcInteract. Finding this bug revealed another lurking bug: * An infelicity in the treatment of superclasses -- we were expanding them locally at the leaves, rather than at their binding site; see (3a) in Note [The superclass story]. As a consequence, TcRnTypes.superclassesMightHelp must look inside implications. In more detail: * Stop the crash, by making TcInteract.chooseInstance test for the no-evidence-bindings case. In that case we simply don't use the instance. This entailed a slight change to the type of chooseInstance. * Make TcSMonad.getPendingScDicts (now renamed getPendingGivenScs) return only Givens from the /current level/; and make TcRnTypes.superClassesMightHelp look inside implications. * Refactor the simpl_loop and superclass-expansion stuff in TcSimplify. The logic is much easier to understand now, and has less duplication.
* Add "quantified constraint" context in error message, fix #15231.HE, Tao2018-06-153-0/+23
| | | | | | | | | | | | | | | | | | | | This patch adds "quantified constraint" context in error message when UndecidableInstances checking fails for quantified constraints. See Trac #15231:comment#1. This patch also pretty-prints the instance head for better error messages. Test Plan: make test TEST="T15231" Reviewers: bgamari, simonpj Reviewed By: simonpj Subscribers: simonpj, rwbarton, thomie, carter GHC Trac Issues: #15231 Differential Revision: https://phabricator.haskell.org/D4819
* Remove duplicate quantified constraintsSimon Peyton Jones2018-06-112-0/+70
| | | | | | | This is an easy fix for Trac #15244: just avoid adding the same quantified Given constraint to the inert set twice. See TcSMonad Note [Do not add duplicate quantified instances].
* Implement QuantifiedConstraintsSimon Peyton Jones2018-06-0411-0/+301
We have wanted quantified constraints for ages and, as I hoped, they proved remarkably simple to implement. All the machinery was already in place. The main ticket is Trac #2893, but also relevant are #5927 #8516 #9123 (especially! higher kinded roles) #14070 #14317 The wiki page is https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints which in turn contains a link to the GHC Proposal where the change is specified. Here is the relevant Note: Note [Quantified constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The -XQuantifiedConstraints extension allows type-class contexts like this: data Rose f x = Rose x (f (Rose f x)) instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2 Note the (forall b. Eq b => Eq (f b)) in the instance contexts. This quantified constraint is needed to solve the [W] (Eq (f (Rose f x))) constraint which arises form the (==) definition. Here are the moving parts * Language extension {-# LANGUAGE QuantifiedConstraints #-} and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension * A new form of evidence, EvDFun, that is used to discharge such wanted constraints * checkValidType gets some changes to accept forall-constraints only in the right places. * Type.PredTree gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forall-constraints * Define a type TcRnTypes.QCInst, which holds a given quantified constraint in the inert set * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst], which holds all the Given forall-constraints. In effect, such Given constraints are like local instance decls. * When trying to solve a class constraint, via TcInteract.matchInstEnv, use the InstEnv from inert_insts so that we include the local Given forall-constraints in the lookup. (See TcSMonad.getInstEnvs.) * topReactionsStage calls doTopReactOther for CIrredCan and CTyEqCan, so they can try to react with any given quantified constraints (TcInteract.matchLocalInst) * TcCanonical.canForAll deals with solving a forall-constraint. See Note [Solving a Wanted forall-constraint] Note [Solving a Wanted forall-constraint] * We augment the kick-out code to kick out an inert forall constraint if it can be rewritten by a new type equality; see TcSMonad.kick_out_rewritable Some other related refactoring ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * Move SCC on evidence bindings to post-desugaring, which fixed #14735, and is generally nicer anyway because we can use existing CoreSyn free-var functions. (Quantified constraints made the free-vars of an ev-term a bit more complicated.) * In LookupInstResult, replace GenInst with OneInst and NotSure, using the latter for multiple matches and/or one or more unifiers