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