EvTerms and how they are used

[Jan Bracker]

Hello,

I am trying to use the new type checker plugins [1] that are implemented in
head.

When successful a plugin has to return a [(EvTerm, Ct)] for the solved
constraints. The documentation on EvTerms is scarce [2,3,4] and I could not
find papers that explain them (many talk about 'evidence', but they never
get concrete).

So far I have figured out that "EvDFunApp DFunId [Type] [EvTerm]" selects a
certain instance to be used for a constraint, though I don't know what the
list of EvTerms in the end is for. I am also a bit unclear on how the
"[Type]" is used.If I turn on '-dcore-lint' I get errors. So I still seem
to be using it wrong.

I have also asked in IRC, but did not get a response to my question.

I am sorry if this is the wrong mailing list to ask. If there is a more
apropriate place just point it out.

Best,
Jan

[1]: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker
[2]:
http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/TcEvidence.html#t:EvTerm
[3]:
http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/src/TcEvidence.html#EvTerm
[4]:
http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compiler-plugins.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150225/3eff90c3/attachment.html>