[Haskell-cafe] MPTC and quantification in GADTs vs. regular ADTs

[Oleg Grenrus]

If you change latter definition to

data T row col
    = MPTC row col =>
      T { col :: col
        , row :: row }

I.e. remove `forall row col`, then everything starts to work. As your definition is (with unique names) is:

data T anyrow anycol
    = forall row col. MPTC row col =>
      T { col :: col
        , row :: row }

i.e. the indexes are phantom and field types are existential.

In the first version, the `forall row col` is harmless, as the indexes are repeated in GADT syntax: -> T row col

- Oleg

> On 11 Apr 2016, at 10:57, Kosyrev Serge <_deepfire at feelingofgreen.ru> wrote:
> 
> Good day folks!
> 
> What is the explanation for the difference in GHC reaction towards the
> two variants of the following piece of code:
> 
>> {-# LANGUAGE GADTs #-}
>> {-# LANGUAGE RankNTypes #-}
>> {-# LANGUAGE RecordWildCards #-}
>> {-# LANGUAGE MultiParamTypeClasses #-}
>> {-# LANGUAGE UnicodeSyntax #-}
>> 
>> import Prelude.Unicode
>> 
>> class MPTC row col where
>> class TC a where
>>    method ∷ a → a
>> 
> 1 data T row col where
> 1      T ∷ ∀ row col. MPTC row col ⇒
> 1          { col ∷ col
> 1          , row ∷ row } → T row col
> 2 data T row col
> 2     = ∀ row col. MPTC row col ⇒
> 2       T { col ∷ col
> 2         , row ∷ row }
>> 
>> instance MPTC row col ⇒ TC (T row col) where
>>    method w at T{..} =
>>        seq (recover (toCol w) row) w
>> 
>> toCol ∷ MPTC row col ⇒ T row col → col
>> toCol = (⊥)
>> 
>> recover ∷ MPTC row col ⇒ col → row → T row col
>> recover = T
> 
> Note the missing
> 
>> instance MPTC row col
> 
> Nevertheless, the former typechecks, while the latter is rejected with:
> 
>> mptc-data-vs-gadt.hs:23:14-34: error: …
>>    • Could not deduce (MPTC row1 col) arising from a use of ‘recover’
>>      from the context: MPTC row col
>>        bound by the instance declaration
>>        at mptc-data-vs-gadt.hs:21:10-38
>>      or from: MPTC row1 col1
>>        bound by a pattern with constructor:
>>                   T :: forall row col row col.
>>                        MPTC row col =>
>>                        col -> row -> T row col,
>>                 in an equation for ‘method’
>>        at mptc-data-vs-gadt.hs:22:14-18
>>      Possible fix:
>>        add (MPTC row1 col) to the context of the data constructor ‘T’
>>    • In the expression: (recover (toCol w) row)
>>      In the expression: seq (recover (toCol w) row) w
>>      In an equation for ‘method’:
>>          method w@(T {..}) = seq (recover (toCol w) row) w
> 
> I'm sure this must have something to do with GADTs carrying type
> equality constraints, but still I don't quite understand the difference
> in interpretation of the forall quantification.
> 
> To my understanding, a value bound by the pattern 'w at T{..}' ought to be
> treated as sufficient evidence for 'MPTC row col', no matter whether
> it is a GADT or not.
> 
> ..but it isn't.
> 
> --
> с уважениeм / respectfully,
> Косырев Сергей
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160411/49935a47/attachment.sig>