New-to-Haskell, i.e. elementary, Haskell questions; extended discussions

Shayan Najd Javadipour | 31 Jul 2012 20:59

Explicit forall - Strange Error

Hi,

I wonder why the following code doesn't typecheck in GHC 7.4.1:

{-# LANGUAGE GADTs,RankNTypes #-} data T a where T1 :: (forall b. b -> b) -> (forall a. Int -> T a) {- Error: Data constructor `T1' returns type `forall a. Int -> T a' instead of an instance of its parent type `T a' In the definition of data constructor `T1' In the data type declaration for `T' Failed, modules loaded: none. -} While: {-# LANGUAGE GADTs,RankNTypes #-} f :: (forall b. b -> b) -> (forall a. Int -> Maybe a) f = undefined {- ghci> :t f f :: (forall b. b -> b) -> Int -> Maybe a -}
Thanks, Shayan

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

headers

MigMit | 31 Jul 2012 21:07

Re: Explicit forall - Strange Error

It really seems to me that the error message you've got explains everything quite clear.

Отправлено с iPad

31.07.2012, в 22:59, Shayan Najd Javadipour <sh.najd <at> gmail.com> написал(а):

Hi,

I wonder why the following code doesn't typecheck in GHC 7.4.1:

{-# LANGUAGE GADTs,RankNTypes #-} data T a where T1 :: (forall b. b -> b) -> (forall a. Int -> T a) {- Error: Data constructor `T1' returns type `forall a. Int -> T a' instead of an instance of its parent type `T a' In the definition of data constructor `T1' In the data type declaration for `T' Failed, modules loaded: none. -} While: {-# LANGUAGE GADTs,RankNTypes #-} f :: (forall b. b -> b) -> (forall a. Int -> Maybe a) f = undefined {- ghci> :t f f :: (forall b. b -> b) -> Int -> Maybe a -}
Thanks, Shayan

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

headers

Shayan Najd Javadipour | 31 Jul 2012 21:24

Re: Explicit forall - Strange Error

If GHC handles the explicit "forall" in constructor "T1" in the same way as it does for function "f", we have:

data T a where T1 :: (forall b. b -> b) -> Int -> T a

Which is totally fine! The main question is then why the "forall"s are handled differently?

On Tue, Jul 31, 2012 at 9:07 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:

It really seems to me that the error message you've got explains everything quite clear.

Отправлено с iPad

31.07.2012, в 22:59, Shayan Najd Javadipour <sh.najd <at> gmail.com> написал(а):

Hi,

I wonder why the following code doesn't typecheck in GHC 7.4.1:

{-# LANGUAGE GADTs,RankNTypes #-} data T a where T1 :: (forall b. b -> b) -> (forall a. Int -> T a) {- Error: Data constructor `T1' returns type `forall a. Int -> T a' instead of an instance of its parent type `T a' In the definition of data constructor `T1' In the data type declaration for `T' Failed, modules loaded: none. -} While: {-# LANGUAGE GADTs,RankNTypes #-} f :: (forall b. b -> b) -> (forall a. Int -> Maybe a) f = undefined {- ghci> :t f f :: (forall b. b -> b) -> Int -> Maybe a -}
Thanks, Shayan

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

headers

Brandon Allbery | 31 Jul 2012 21:28

Re: Explicit forall - Strange Error

On Tue, Jul 31, 2012 at 2:59 PM, Shayan Najd Javadipour <sh.najd <at> gmail.com> wrote:

{-# LANGUAGE GADTs,RankNTypes #-} data T a where T1 :: (forall b. b -> b) -> (forall a. Int -> T a) {- Error: Data constructor `T1' returns type `forall a. Int -> T a' instead of an instance of its parent type `T a'

This looks to me like other cases where GHC requires an exact type match even though you used something equivalent. Similarly, for example, it rejects (contrived example)

foo :: Num a => a -> a -> a

foo 0 0 = -1

foo = (+)

because the explicit arity of the cases must match exactly, even though (+)'s type matches the required arity. I am under the impression that it's difficult to make those kinds of things work nicely in the typechecker.

--
brandon s allbery allbery.b <at> gmail.com
wandering unix systems administrator (available) (412) 475-9364 vm/sms

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe