3

私はghc 7.8.2でGADTと明示的なforallで遊んでいます。次の簡単な例を見てみましょう。

{-# LANGUAGE GADTs, RankNTypes #-}

data T1 a where
   T1 :: (b -> a) -> b -> T1 a

data T2 a where
   T2 :: forall b. (b -> a) -> b -> T2 a

ここで ghc は次のように失敗します:

Test.hs:7:26: Not in scope: type variable ‘a’
Test.hs:7:35: Not in scope: type variable ‘a’

T2がコメントアウトされている場合、型チェックは成功します。しかしT1、 とT2は一見同等です。これは ghc のバグですか、それとも GADT の制限ですか? 後者の場合、両者の違いは何ですか？

4

2 に答える 2

4

私はもともとainT1コンストラクターがdata T1 a宣言時にバインドされていると想定していました。しかし、実際にはコンストラクター自体で暗黙的に量化されます。したがってT2、コンストラクターは明示的に数量化され、数量化さbれないため、間違っていaます。

于 2014-05-24T21:25:14.957 に答える