<div dir="ltr"><span style="font-size:12.8000001907349px">Hello,</span><div style="font-size:12.8000001907349px"><div><br></div><div>I am trying to use the new type checker plugins [1] that are implemented in head.</div><div><br></div><div>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).</div><div><br></div><div>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.</div><div><br></div><div>I have also asked in IRC, but did not get a response to my question.</div><div><br>I am sorry if this is the wrong mailing list to ask. If there is a more apropriate place just point it out.<br></div><div><br></div><div>Best,</div><div>Jan</div><div><br></div><div>[1]: <a href="https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker</a></div><div>[2]: <a href="http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/TcEvidence.html#t:EvTerm" target="_blank">http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/TcEvidence.html#t:EvTerm</a></div><div>[3]: <a href="http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/src/TcEvidence.html#EvTerm" target="_blank">http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/src/TcEvidence.html#EvTerm</a></div></div><div style="font-size:12.8000001907349px">[4]: <a href="http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compiler-plugins.html" target="_blank">http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compiler-plugins.html</a></div></div>