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
$fPolymonadIdentityIdentityIdentity
@ ()
@ ()
(idOp @ Bool True)
(>>=
@ Identity
@ Identity
@ Any
$fPolymonadIdentityIdentityIdentity
@ Char
@ ()
(return
@ 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"?
Best,
Jan
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