Fwd: EvTerms and how they are used

[Adam Gundry]

Hi Jan,

It's a bit hard to know exactly what is going on without the full code,
but I think what is happening is this: you have an unsolved constraint
`Polymonad Identity n_abpq Identity` and your plugin provides an
evidence term of type `Polymonad Identity Identity Identity`, but of
course this is ill-typed, because `n_abpq` is not `Identity`. Hence Core
Lint quite reasonably complains.

<digression>The `Any` type is used by GHC to instantiate type variables
whose values are irrelevant, because they do not occur in the type. The
classic example is `null []`, where the type of the list is unimportant:
rather than having an unsolved unification variable, GHC solves it with
`Any`.</digression>

I'm not sure exactly what you are trying to do, but I think the right
way to approach this problem is to simulate a functional dependency on
Polymonad (in fact, can you use an actual functional dependency)? When
confronted with the constraint `Polymonad Identity n_abpq Identity`, do
not try to solve it directly, but instead notice that you must have
`n_abpq ~ Identity`. Your plugin can emit this as an additional derived
constraint, which will allow GHC's built-in solver to instantiate the
unification variable `n_abpq` and then solve the original constraint
using the existing instance. No manual evidence generation needed!

Emitting this extra derived constraint is essentially what happens if
you specify the functional dependency

    class Polymonad m n p | m p -> n where

but the plugin approach allows more fine-grained control over exactly
when this applies.

Out of interest, can you say anything about your aims here? I'm keen to
find out about the range of applications of typechecker plugins.

All the best,

Adam


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

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