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

[Kosyrev Serge]

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,
Косырев Сергей