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

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