<div dir="ltr"><div class="gmail_quote"><div dir="ltr">Hi Adam,<div><br></div><div>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.</div><div><br></div><div>I have something along the following lines:</div><div><br></div><div>class Polymonad m n p where</div><div> -- Functions</div><div><br></div><div>instance Polymonad Identity Identity Identity where</div><div> -- Implementation</div><div><br></div><div>-- Further instances and some small chunk of code involving them:</div><div><br></div><div>The code implies the following constraint:</div><div></div><div>Polymonad Identity n_abpq Identity</div><div><br></div><div>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).</div><div><br></div><div>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:</div><div>EvDFunApp $fPolymonadIdentityIdentityIdentity [] []</div><div><br></div><div>But when I run this with -dcore-lint I get the following error message:</div><div><br></div><div><div>*** Core Lint errors : in result of Desugar (after optimization) ***</div><div><no location info>: Warning:</div><div> In the expression: >></div><div> @ Identity</div><div> @ Any</div><div> @ Identity</div><div> $fPolymonadIdentityIdentityIdentity</div><div> @ ()</div><div> @ ()</div><div> (idOp @ Bool True)</div><div> (>>=</div><div> @ Identity</div><div> @ Identity</div><div> @ Any</div><div> $fPolymonadIdentityIdentityIdentity</div><div> @ Char</div><div> @ ()</div><div> (return</div><div> @ Char @ Identity $fPolymonadIdentityIdentityIdentity (C# 'a'))</div><div> (\ _ [Occ=Dead] -></div><div> return @ () @ Identity $fPolymonadIdentityIdentityIdentity ()))</div><div> Argument value doesn't match argument type:</div><div> Fun type:</div><div> Polymonad Identity Any Identity =></div><div> forall a_abdV[sk] b_abdW[sk].</div><div> Identity a_abdV[sk] -> Any b_abdW[sk] -> Identity b_abdW[sk]</div><div> Arg type: Polymonad Identity Identity Identity</div><div> Arg: $fPolymonadIdentityIdentityIdentity</div></div><div><br></div><div>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"?</div><div><br></div><div>Best,</div><div>Jan</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">2015-02-25 13:35 GMT+00:00 Adam Gundry <span dir="ltr"><<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Jan,<br>
<br>
Yes, unfortunately the meaning of EvTerm is a weak point of the current<br>
typechecker plugins story; it rather requires one to understand how<br>
GHC's constraint solver produces evidence. There are lots of papers on<br>
evidence for equality constraints in System FC, but typeclass<br>
constraints are generally ignored as they are just datatypes at the FC<br>
level.<br>
<br>
Let me try to give you some idea of what EvDFunApp means, then hopefully<br>
those with more knowledge of the GHC internals can correct me...<br>
<br>
If you write a class instance, e.g.<br>
<br>
instance (Show a, Show b) => Show (T a b) where ...<br>
<br>
then GHC generates a dfun (short for "dictionary function", I guess)<br>
<br>
$fShowT :: forall a b . (Show a, Show b) => Show (T a b)<br>
<br>
where Show is treated as a record data type containing a dictionary of<br>
methods for the class. At the core level, this is a normal term-level<br>
function (albeit with a strange name).<br>
<br>
Now when the typechecker has a constraint to solve, say<br>
<br>
Show (T Int Bool),<br>
<br>
it produces evidence for this by applying $fShowT to the appropriate<br>
types and to evidence for the superclass constraints, in this case<br>
something like<br>
<br>
$fShowT @Int @Bool $fShowInt $fShowBool<br>
<br>
where I'm using @ for type application. This is represented in EvTerm as<br>
<br>
EvDFunApp $fShowT [Int, Bool] [ EvDFunApp $fShowInt [] []<br>
, EvDFunApp $fShowBool [] [] ]<br>
<br>
Thus the [Type] is the list of kinds/types at which to instantiate the<br>
dfun, and the [EvTerm] is the list of evidence terms to which it must be<br>
applied. Obviously this application should be well-typed, and<br>
-dcore-lint will complain if it is not.<br>
<br>
For typechecker plugins, it would be nice if we could write arbitrary<br>
core expressions as evidence, but this hasn't yet been implemented<br>
(partially because most of the examples so far solve equality<br>
constraints, rather than typeclass constraints).<br>
<br>
Hope this helps,<br>
<br>
Adam<br>
<div><div><br>
<br>
On 25/02/15 10:55, Jan Bracker wrote:<br>
> Hello,<br>
><br>
> I am trying to use the new type checker plugins [1] that are implemented<br>
> in head.<br>
><br>
> When successful a plugin has to return a [(EvTerm, Ct)] for the solved<br>
> constraints. The documentation on EvTerms is scarce [2,3,4] and I could<br>
> not find papers that explain them (many talk about 'evidence', but they<br>
> never get concrete).<br>
><br>
> So far I have figured out that "EvDFunApp DFunId [Type] [EvTerm]"<br>
> selects a certain instance to be used for a constraint, though I don't<br>
> know what the list of EvTerms in the end is for. I am also a bit unclear<br>
> on how the "[Type]" is used.If I turn on '-dcore-lint' I get errors. So<br>
> I still seem to be using it wrong.<br>
><br>
> I have also asked in IRC, but did not get a response to my question.<br>
><br>
> I am sorry if this is the wrong mailing list to ask. If there is a more<br>
> apropriate place just point it out.<br>
><br>
> Best,<br>
> Jan<br>
><br>
> [1]: <a href="https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker</a><br>
> [2]: <a href="http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/TcEvidence.html#t:EvTerm" target="_blank">http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/TcEvidence.html#t:EvTerm</a><br>
> [3]: <a href="http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/src/TcEvidence.html#EvTerm" target="_blank">http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/src/TcEvidence.html#EvTerm</a><br>
> [4]: <a href="http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compiler-plugins.html" target="_blank">http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compiler-plugins.html</a><br>
<br>
<br>
</div></div><span><font color="#888888">--<br>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
</font></span></blockquote></div><br></div>
</div></div></div><br></div>