[Haskell-cafe] Solved but strange error in type inference

[Yves Parès]

> two uses of the same data constructor in an expression will not unify
those type variables because it's scoped to the data constructor itself

Which is somewhat clearer when using GADTs:
data LegGram t s where
    LegGram :: Ord nt => M.Map nt [RRule nt t s] -> LegGram t s

Here, as the LegGram data constructor is a function, it follows their
rules, then is equivalent to:
LegGram :: forall nt. Ord nt => M.Map nt [RRule nt t s] -> LegGram t s

Which clearly indicated that 'nt' only exists within the scope of a
variable.

However, GADTs add some ambiguity:
data LegGram *t* *s* where
It's not easy for a beginner to see that those type variables are *not *the
same than those:
LegGram :: Ord nt => M.Map nt [RRule nt *t s*] -> LegGram *t s*

So, for short:
data Something a b c = ... -- ^ Regular ADT, a b and c are brought into
scope

data Something a b c where ... -- ^ GADT, a b and c *are not *scoped, their
name is useless, their use is only to indicate the arity of the type
constructor. But we have kinds for that.

I find it misleading. To me, it should be compulsory to write:
data Something :: * -> * -> * where ...
would be better, but I believe it requires another language extension.

2012/1/3 Brandon Allbery <allbery.b at gmail.com>

> On Tue, Jan 3, 2012 at 06:43, Yves Parès <limestrael at gmail.com> wrote:
>
>> That is error-prone.
>> Plus the code does not need ScopedTypeVariables. The real problem comes
>> from the use of a class constraint on the LegGram data constructor.
>>
>> data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s])
>>
>> Short answer: you *can't *add class constraints to an already declared
>> type variable:
>>
>> The LegGram *type *constructor declares the 'nt' variable (and then
>> brings it into scope), so trying afterwards to add a constraint to it for
>> the LegGram *data *constructor is invalid, so the compiler understands
>> this:
>> data LegGram nt t s = *forall nt.* Ord nt => LegGram (M.Map *nt* [RRule *
>> nt* t s])
>> ...the declaration and scoping of a *new* type variable.
>>
>> This is it, right?
>
>
> Yep, with the additional gotcha that two uses of the same data constructor
> in an expression will not unify those type variables because it's scoped to
> the data constructor itself.  Which is the confusing and error-prone
> behavior that led to it being removed from the next version of the standard
> (probably; the proposal was accepted but H'2011 was bypassed and H'2012 has
> not yet started).
>
> --
> brandon s allbery                                      allbery.b at gmail.com
> wandering unix systems administrator (available)     (412) 475-9364 vm/sms
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120103/396ed936/attachment.htm>