EvTerms and how they are used

[Adam Gundry]

Hi Jan,

Yes, unfortunately the meaning of EvTerm is a weak point of the current
typechecker plugins story; it rather requires one to understand how
GHC's constraint solver produces evidence. There are lots of papers on
evidence for equality constraints in System FC, but typeclass
constraints are generally ignored as they are just datatypes at the FC
level.

Let me try to give you some idea of what EvDFunApp means, then hopefully
those with more knowledge of the GHC internals can correct me...

If you write a class instance, e.g.

    instance (Show a, Show b) => Show (T a b) where ...

then GHC generates a dfun (short for "dictionary function", I guess)

    $fShowT :: forall a b . (Show a, Show b) => Show (T a b)

where Show is treated as a record data type containing a dictionary of
methods for the class. At the core level, this is a normal term-level
function (albeit with a strange name).

Now when the typechecker has a constraint to solve, say

    Show (T Int Bool),

it produces evidence for this by applying $fShowT to the appropriate
types and to evidence for the superclass constraints, in this case
something like

    $fShowT @Int @Bool $fShowInt $fShowBool

where I'm using @ for type application. This is represented in EvTerm as

    EvDFunApp $fShowT [Int, Bool] [ EvDFunApp $fShowInt [] []
                                  , EvDFunApp $fShowBool [] [] ]

Thus the [Type] is the list of kinds/types at which to instantiate the
dfun, and the [EvTerm] is the list of evidence terms to which it must be
applied. Obviously this application should be well-typed, and
-dcore-lint will complain if it is not.

For typechecker plugins, it would be nice if we could write arbitrary
core expressions as evidence, but this hasn't yet been implemented
(partially because most of the examples so far solve equality
constraints, rather than typeclass constraints).

Hope this helps,

Adam


On 25/02/15 10:55, Jan Bracker wrote:
> 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


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/