Explicit forall - Strange Error

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Explicit forall - Strange Error

Shayan Najd Javadipour-2
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Explicit forall - Strange Error

MigMit
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 <[hidden email]> написал(а):

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Explicit forall - Strange Error

Shayan Najd Javadipour-2
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 <[hidden email]> 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 <[hidden email]> написал(а):

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Explicit forall - Strange Error

Brandon Allbery
In reply to this post by Shayan Najd Javadipour-2
On Tue, Jul 31, 2012 at 2:59 PM, Shayan Najd Javadipour <[hidden email]> 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                                      [hidden email]
wandering unix systems administrator (available)     (412) 475-9364 vm/sms


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe