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(a)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.…
> > [3]:
> http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.…
> > [4]:
> http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/comp…
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
>
In Bug #9661, Comment #12 Simon Peyton-Jones wrote [1],
> Annoyingly, the `CoreSyn.RuleFun` API for built-in rules does not give
> access to the context of an application (the `SimplCont`), but it
> would not be hard to make it do so.
>
> So if that is the right rewrite, then it'd be another useful project
> for someone.
I started taking a look at this over the weekend, hoping for a
weekend-ish project. Unfortunately it's not as easy as it initially
looked. The current state of my work can be found here [2]. The core
of the change (as I understand it) is to add a `SimplCont` argument to
`RuleFun` [3] although things are in actuality a bit more complicated
While it was easy to pipe through the `SimplCont` in the simplifier
itself (as it was already keeping track of the `SimplCont` context),
`ruleCheck` in `Rules.hs` does not know anything about the simplifier or
`SimplCont`.
Currently `ruleCheck` is quite simple: It traverses the program
examining function applications, looking for rules which apply to the
applied function and match a user-specified predicate. It then produces
a human-readable message in the event that the rule would not
fire. Unfortunately, to evaluate whether the rule will fire we actually
need to try calling the `RuleFun`, which now requires having a
`SimplCont`.
As far as I can tell there are three ways to address this,
1. Pass a dummy `SimplCont` (probably a `Stop`) to the `RuleFun`. This
is by far the easiest option but will result in discrepancies
between the rule check and the rules actually fired by simplifier.
2. Replicate the simplifier's logic to produce a `SimplCont` in the
rule check. This seems like it will result in a great deal of
unnecessary (and non-trivial) code duplication.
3. Fold the rule check into the simplifier. It seems like this folds
what is currently quite simple code into the already rather complex
simplifier.
I'm not entirely sure which of these is the least-evil option. Thoughts?
Cheers,
- Ben
P.S. There is also the matter of cyclic module imports. To address these
I've split up `SimplUtils.hs` into `SimplCont.hs` and
`SimplInline.hs`. Given these two have no cross-dependencies this
seems like a reasonable split even independent of the `RuleFun`
rework.
`Rules.hs` can then import `SimplCont.hs` (although it
needs an hs-boot file to satisfy references in `LoadIface.hs`,
`HscTypes.hs`, `MkId.hs`). I'll probably reevaluate the need for
hs-boot files later.
If anyone sees a better restructuring let me know.
[1] https://ghc.haskell.org/trac/ghc/ticket/9661#comment:12
[2] https://github.com/ghc/ghc/compare/ghc-7.10...bgamari:wip/rule-context
[3] https://github.com/ghc/ghc/commit/a978a4766ebf692820c3b491522b2dd6c642005f
[4] https://github.com/bgamari/ghc/blob/c71fb84b8c9ec9c1e279df8c75ceb8a537801aa…
