On Mon, Feb 25, 2013 at 4:11 PM, Simon Peyton-Jones <simonpj@microsoft.com> wrote:

I suppose we want an instance
forall k. instance Typeable (k -> *) (Proxy k)

Yes, that looks right.

 

So the universally quantified kind variables of the tycon should end up universally
quantified in the instance as well. How does this translate to the ds_tvs, ds_tys, and
ds_tc_args arguments of a DerivSpec

 

My instinct is that the ds_tvs include both type and kind variables, kind variables first.  The kinds of the type variables can mention the kind variables.


We don't have any type variables, we want to drop those, as we'll get those instances
via the `(Typeable f, Typeable a) => Typeable (f a)` instance.

In my branch, I currently get standalone deriving to give me the following for this
example (tc-trace):

Standalone deriving;
  tvs: [k]
  theta: []
  cls: Typeable
  tys: [k -> *, Proxy k]
Standalone deriving:
  class: Typeable
  class types: [k -> *]
  type: Proxy k

This looks good to me. However, the generated instance is not what
I think it should be (ddump-types):

instance Typeable (forall (k :: BOX). k -> *) (Proxy k)

The forall should be outside, as now the `k` in `Proxy k` is out of scope.
I just don't know how to craft such a DerivSpec... what I have now is:

DS { ds_loc = loc, ds_orig = orig, ds_name = dfun_name, ds_tvs = tvs
    , ds_cls = cls, ds_tys = tyConKind tycon : [mkTyConApp tycon tc_args]
    , ds_tc = tycon, ds_tc_args = tc_args
    , ds_theta = mtheta `orElse` [], ds_newtype = False })  }

(I filter the type variables from the tc_args before this stage, leaving only kind variables.)


Cheers,
Pedro