Hi, I am not sure about the "deferred type errors", as I never use that feature.
To create new wanted variables, usually you use "newWantedEvVar". This gives you some evidence (well, really a place-holder for the actual evidence), and a "freshness" flag. You do two different things depending on the freshness: - If the evidence is "Fresh", then you have a brand new wanted constraint and you emit it as a new sub-goal (i.e., the usual thing) - if the evidence is cached, this means that this same constraint already exists; in that case you can use the returned evidence as needed, but you don't emit a new wanted constraint. This is a bit nicer than the "newWantedEvVarNC" as it generates fewer constraints. -Iavor On Wed, May 20, 2015 at 12:26 AM, Christiaan Baaij < christiaan.ba...@gmail.com> wrote: > Hi Iavor, Adam, List, > > I managed to fix the error message location by using: > `newWantedEvVarNC`( > https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcSMonad.html#v:newWantedEvVarNC > ) > > So now the output of my test suite is: > ``` > [1 of 2] Compiling ErrorTests ( tests/ErrorTests.hs, > dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise-tmp/ErrorTests.o > ) [GHC.TypeLits.Normalise changed] > > tests/ErrorTests.hs:14:13: Warning: > Couldn't match type ‘GCD 6 8’ with ‘4’ > Expected type: Proxy (GCD 6 8) -> Proxy 4 > Actual type: Proxy 4 -> Proxy 4 > In the expression: id > In an equation for ‘testFail1’: testFail1 = id > > tests/ErrorTests.hs:17:13: Warning: > Couldn't match type ‘GCD 6 9’ with ‘GCD 6 8’ > NB: ‘GCD’ is a type function, and may not be injective > Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9) > Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9) > In the expression: id > In an equation for ‘testFail2’: testFail2 = id > [2 of 2] Compiling Main ( tests/Main.hs, > dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise-tmp/Main.o ) > [GHC.TypeLits.Normalise changed] > Linking dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise ... > Running 1 test suites... > Test suite test-ghc-tynat-normalise: RUNNING... > ghc-typelits-natnormalise > Basic functionality > GCD 6 8 ~ 2: OK > GCD 6 8 + x ~ x + GCD 10 8: OK > errors > GCD 6 8 ~ 4: OK > GCD 6 8 + x ~ x + GCD 9 6: FAIL > No exception! > > 1 out of 4 tests failed (0.01s) > ``` > > But evaluating the expression still doesn’t throw an exception because I > solved the original constraint. > > — Christiaan > > On 19 May 2015, at 18:44, Christiaan Baaij <christiaan.ba...@gmail.com> > wrote: > > I have yet to test this properly, but I don't think your suggestions > (which you happen to give with 1 minute of eachother...) play nicely with > error reporting. > Here is an output of my testsuite: > > ``` > [1 of 2] Compiling ErrorTests ( tests/ErrorTests.hs, > dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise-tmp/ErrorTests.o > ) [GHC.TypeLits.Normalise changed] > > tests/ErrorTests.hs:1:1: Warning: > Couldn't match type ‘GCD 6 9’ with ‘GCD 6 8’ > NB: ‘GCD’ is a type function, and may not be injective > Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9) > Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9) > > tests/ErrorTests.hs:14:13: Warning: > Couldn't match type ‘GCD 6 8’ with ‘4’ > Expected type: Proxy (GCD 6 8) -> Proxy 4 > Actual type: Proxy 4 -> Proxy 4 > In the expression: id > In an equation for ‘testFail1’: testFail1 = id > [2 of 2] Compiling Main ( tests/Main.hs, > dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise-tmp/Main.o ) > [GHC.TypeLits.Normalise changed] > Linking dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise ... > Running 1 test suites... > Test suite test-ghc-tynat-normalise: RUNNING... > ghc-typelits-natnormalise > Basic functionality > GCD 6 8 ~ 2: OK > GCD 6 8 + x ~ x + GCD 10 8: OK > errors > GCD 6 8 ~ 4: OK > GCD 6 8 + x ~ x + GCD 9 6: FAIL > No exception! > > 1 out of 4 tests failed (0.00s) > ``` > > Note that 'ErrorTest.hs' is compiled with '-fdefer-type-errors'. > There's a two things you may notice > * The first error message's location is '1:1' > * Evaluation the function with the type-error does not raise an exception. > > So by solving the constraint > "GCD 6 8 + x ~ x + GCD 9 6" > The boxed/run-time coercion no longer errors. > Also, I'm using newSimpleWanted ( > https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcMType.html#v:newSimpleWanted) > to create the new wanted constraint. > But for some reason the errror message doesn't get the source-error > location of the original constraint. > Perhaps I shouldn't be using 'newSimpleWanted' to create new wanted > constraints? > > The sources for the plugins are over here: > https://github.com/christiaanb/ghc-typelits-natnormalise > https://github.com/christiaanb/ghc-typelits-extra > > Cheers, > > Christiaan > > > > On 19 May 2015 at 18:01, Iavor Diatchki <iavor.diatc...@gmail.com> wrote: > >> Hi Christiaan, >> >> >> Plugins should return the solved constraints in the first field of >> `TcPLuginOk`, and additional sub-goals in the second. >> The constraints in the first list are marked as solved, and do not need >> to be processed further, while the constraints >> in the second list will be added to the work queue, for further >> processing. Also, the solutions of wanted goals may be in terms of other >> as yet unsolved things. >> >> I think that there are two situations when a plugin might return an empty >> first list, but new work in the second list. >> Both are about computing new facts, and thus "communicating" with other >> plugins: >> 1. Discover new given facts: the plugin was presented with some >> givens, and it computed some additional givens that it thinks might be of >> use to someone else (typically these are equality constraints) >> 2. Discover new derived facts: the plugin was presented with a >> mixture of wanted and givens, and it thinks that the new derived facts >> might be useful by specializing the problem----derived facts help with type >> inference by instantiating unification variables. >> >> Generally, I don't think a plugin should ever need to emit new wanted >> constraints without solving anything. It'd be interesting if that could >> happen though... >> >> Another thing that might be relevant: at present, GHC's constraint solver >> does not do back tracking. So there is no way for a plugin (or other parts >> of the constraint solver) to say: "I'll emit this new wanted constraint, >> and depending on if it was proved or disproved do something". Another way >> to think of his is that constraints are either solved or unsolved, but >> being unsolved does not mean that they are disproved. Now, there is a >> mechanism to mark a constraint as "never solvable", but currently this is >> mostly used for error reporting. >> >> For your concrete example though, the plugin can actually commit to the >> given path because the only way to solve "GCD 6 8 + x ~ x + GCD 9 6" is if >> "GCD 6 8 ~ GCD 9 6". So I'd imagine you want these steps: >> >> Plugin A: Solve "GCD 6 8 + x ~ x + GCD 9 6", new wanted "GCD 6 8 ~ GCD 9 >> 6" >> Plugin B: "GCD 6 8 ~ GCD 9 6" --> impossible >> Done. >> >> >> -Iavor >> >> >> >> On Tue, May 19, 2015 at 3:35 AM, Christiaan Baaij < >> christiaan.ba...@gmail.com> wrote: >> >>> I have a question about how type-checker plugins should interact. >>> My situation is the following: >>> I have two type-checker plugins, one that can solve equalities involving >>> the standard type-level operations on kind Nat (+,*,-,^), and another >>> type-checker plugin that can prove equalities involving a new type-level >>> operation GCD. >>> In the following, the type-checker plugin involving the stand type-level >>> operations is called ‘A’, and the type checker involving the new GCD >>> operations is called ‘B’. >>> >>> When type-checker plugin A encounters: >>> [W] GCD 6 8 + x ~ x + GCD 9 6 >>> >>> It knows that (+) is commutative, so it can prove the above equality >>> _given_ that "GCD 6 8 ~ GCD 9 6” holds. >>> So what type-checker plugin A does now is emits a new wanted constraints: >>> [W] GCD 6 8 ~ GCD 9 6 >>> And remembers that it emitted this wanted constraint. >>> In type-checker plugin lingo, it returns: >>> TcPluginOk [] ["[W] GCD 6 8 ~ GCD 9 6”] >>> >>> >> >> Now whenever type-checker plugin encounters >>> [W] GCD 6 8 + x ~ x + GCD 9 6 >>> again, it checks to see if the discharged constraint >>> [W] GCD 6 8 ~ GCD 9 6 >>> Is already solved, is disproven, or unsolved. >>> If the discharged constraint is solved, it will return: >>> TcPluginOk ["[W] GCD 6 8 + x ~ x + GCD 9 6”] [] >>> If the discharged constraint is dis proven, it returns: >>> TcPluginContradiction ["[W] GCD 6 8 + x ~ x + GCD 9 6”] >>> And otherwise, it doesn’t do anything: >>> TcPluginOk [] [] >>> >>> >> >> >>> Now, type-checker plugin B, the one that knows about GCD, comes along. >>> It sees: >>> [W] GCD 6 8 + x ~ x + GCD 9 6 >>> [W] GCD 6 8 ~ GCD 9 6 >>> I doesn’t know anything about (+); but it does know about GCD, and >>> clearly sees that GCD 6 8 is not equal to GCD 9 6. >>> So it tells that GCD 6 8 ~ GCD 9 6 is insoluble. >>> In type-checker plugin lingo it says: >>> TcPluginContradiction ["[W] GCD 6 8 ~ GCD 9 6”] >>> >>> According to >>> https://github.com/ghc/ghc/blob/228ddb95ee137e7cef02dcfe2521233892dd61e0/compiler/typecheck/TcInteract.hs#L547 >>> What happens next is that the insoluble constraint >>> [W] GCD 6 8 ~ GCD 9 6 >>> is taken of the work list for all plugins. >>> However! the same thing happens when a plugin is able to prove a >>> constraint. >>> That is, if B would have (erroneously) returned: >>> TcPluginOk ["[W] GCD 6 8 ~ GCD 9 6”] [] >>> >>> Then there is _no_ way for type-checker plugin A to know what happened. >>> Were its discharged constraints taken from the work-list because it was >>> insoluble? or because it was solved? >>> This is a problem because to me it seems that the work list is the only >>> way that two type-checker plugins can communicate. >>> >>> I guess my question is: if not through the work list, how are >>> type-checker plugins supposed to communicate? >>> Am I going about it all wrong in terms how I should be writing >>> type-checker plugins? >>> Or, should the type of ‘TcPluginSolver’ ( >>> https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcRnTypes.html#t:TcPluginSolver) >>> be updated to?: >>> >>> ``` >>> type TcPluginSolver = [Ct] -- ^ Given constraints >>> -> [Ct] -- ^ Derived constraints >>> -> [Ct] -- ^ Wanted constraints >>> -> [Ct] -- ^ Insoluble constraints >>> -> TcPluginM TcPluginResult >>> ``` >>> >>> Best regards, >>> >>> Christiaan >>> >>> >>> >>> >>> >> > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
