Fwd: EvTerms and how they are used
jan.bracker at googlemail.com
Thu Feb 26 10:07:12 UTC 2015
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
instance Polymonad Identity Identity Identity where
-- 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
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: >>
(idOp @ Bool True)
@ Char @ Identity
$fPolymonadIdentityIdentityIdentity (C# 'a'))
(\ _ [Occ=Dead] ->
return @ () @ Identity
Argument value doesn't match argument 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
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
> 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,
> On 25/02/15 10:55, Jan Bracker wrote:
> > Hello,
> > I am trying to use the new type checker plugins  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
> > : https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker
> > :
> > :
> > :
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs