Fwd: EvTerms and how they are used

Jan Bracker jan.bracker at googlemail.com
Thu Feb 26 10:07:12 UTC 2015

Hi Adam,

thank you for your quick and detailed answer! I think I understand how to
construct evidence for typeclass constraints now. But trying to apply this,
I still have some problems.

I have something along the following lines:

class Polymonad m n p where
  -- Functions

instance Polymonad Identity Identity Identity where
  -- Implementation

-- Further instances and some small chunk of code involving them:

The code implies the following constraint:
Polymonad Identity n_abpq Identity

As the ambiguity error I get says, when trying to compile this: There is
only one matching instance (the one above, lets call
it $fPolymonadIdentityIdentityIdentity).

So my plugin tries to tell GHC to use that instance. As far as I understand
it, since the parameters of $fPolymonadIdentityIdentityIdentity are no type
variables and there is no superclass it should be as easy as saying:
EvDFunApp $fPolymonadIdentityIdentityIdentity [] []

But when I run this with -dcore-lint I get the following error message:

*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: Warning:
    In the expression: >>
                         @ Identity
                         @ Any
                         @ Identity
                         @ ()
                         @ ()
                         (idOp @ Bool True)
                            @ Identity
                            @ Identity
                            @ Any
                            @ Char
                            @ ()
                               @ Char @ Identity
$fPolymonadIdentityIdentityIdentity (C# 'a'))
                            (\ _ [Occ=Dead] ->
                               return @ () @ Identity
$fPolymonadIdentityIdentityIdentity ()))
    Argument value doesn't match argument type:
    Fun type:
        Polymonad Identity Any Identity =>
        forall a_abdV[sk] b_abdW[sk].
        Identity a_abdV[sk] -> Any b_abdW[sk] -> Identity b_abdW[sk]
    Arg type: Polymonad Identity Identity Identity
    Arg: $fPolymonadIdentityIdentityIdentity

What am I missing? Why doesn't the argument type "Polymonad Identity
Identity Identity" match the first argument of the function type "Polymonad
Identity Any Identity => forall a_abdV[sk] b_abdW[sk]. Identity a_abdV[sk]
-> Any b_abdW[sk] -> Identity b_abdW[sk]". Why is the type variable
translated to "Any"?


2015-02-25 13:35 GMT+00:00 Adam Gundry <adam at well-typed.com>:

> 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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150226/641c6d92/attachment-0001.html>

More information about the ghc-devs mailing list