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, Косырев Сергей
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@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@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, Косырев Сергей _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
participants (2)
-
Kosyrev Serge -
Oleg Grenrus