Type Families and defaults

[Mitar]

Hi!

On Mon, Sep 6, 2010 at 9:37 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> Yes, I've spent most of the last month working on the new type checker, and unless there's a major hiccup it'll be in GHC 7.0.  We'll produce a release candidate just before ICFP.

That's great news! So if I understand those functions:

mkLiveNeuron :: NeuronId -> LiveNeuron n
getNeuronId :: LiveNeuron n -> NeuronId

will not be necessary anymore with new type checked and improvements
to type families?

> However, as it happens both your tests compile with GHC 6.12, if you add ScopedTypeVariables.  The trouble is that your type signatures like (IO n) are read as (forall n. IO n).

This trouble means that I can define something like the following?

instance Neuron TestNeuron where
  data LiveNeuron TestNeuron = LiveTestNeuron NeuronId

  mkLiveNeuron nid = LiveTestNeuron nid
  getNeuronId (LiveTestNeuron nid) = nid

  live _ _ = return ()

  attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO
FooNeuron) dissolve (live nerve)) :: IO (LiveNeuron TestNeuron)

Where obviously this makes little sense. (I made FooNeuron an instance
of Neuron class but this is the only thing it enforced.)

But it does not allow (as the TestNeuron instance):

  attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO
FooNeuron) dissolve (live nerve)) :: IO (LiveNeuron FooNeuron)

Which means that return type is checked well and n is from class definition.

So n in "grow" function type is now locally scoped so it is
independent from surrounding definitions of n. It is universally
quantified and so it is some other type variable, even if it shares
name with "n".

Probably this is what you wrote, but I have to decipher your
terminology a bit. ;-)

But I do not understand how does then GHC pick correct definition in
the case of default definition of "attach" function? If n is
universally scoped and independent surrounding n, then it would be
still ambiguous. Same as:

attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO a)
dissolve (live nerve)) :: IO (LiveNeuron n)

But this later does not work. So n is connected to surrounding n. But
then why it allows such instance definition as I mentioned above with
FooNeuron and TestNeuron together?

> It's not trivial to add, but not really hard either.  Has anyone else been bitten by this?

It would be great if it would be added. Obviously I am for it. ;-)

I think n should be scoped for the whole the class definition,
everywhere, not just parameter and return values types. If somebody
would define the same name for it for some local definition, GHC
should make a "shadowing a variable" warning.


Mitar