Haskellのスコープ付きタイプ変数は、パターンバインディングでタイプ変数のバインドを許可しないのはなぜですか？

Question

GHCのScopedTypeVariablesは、機能パターンではタイプ変数をバインドできますが、パターンではできません。

最小限の例として、私はFooの内部型へのアクセスを得るためにしたい場合は、タイプ

data Foo where Foo :: Typeable a => a -> Foo 

を検討し、以下の機能がコンパイルされません：

fooType :: Foo -> TypeRep 
fooType (Foo x) = 
    let (_ :: a) = x 
    in typeRep (Proxy::Proxy a) 

しかし、このトリックを使用して型変数バインディングを関数呼び出しに移動するには、問題なく動作します。

fooType (Foo x) = 
    let helper (_ :: a) = typeRep (Proxy::Proxy a) 
    in helper x 

letバインディングは実際には偽装の関数バインディングなので、なぜ上記の2つのコードスニペットは同等ではありませんか？

（この例では、他のソリューションはtypeOf xでTypeRepを作成することです、またはトップレベルの機能にx :: aとして直接変数をバインドします。これらのオプションのどちらもが、私の実際のコードで利用できる、とdoesnのそれらを使用して」質問に答えてください）

Answer 1

大きなことは、機能がcaseの偽装であり、letの表現ではありません。 caseが一致し、letが異なる意味を持つ。これは、let式でタイプの洗練されたGADTコンストラクタと一致させることができない理由です。

caseと一致すると、続行する前に検査結果が評価されますが、letと一致すると、「結果が要求されたときにこの評価を行う」というヒープにサンクがスローされます。 GHCは、怠惰がそれらとやりとりする可能性があるすべての方法でローカルスコープのタイプ（例ではaなど）を保持する方法を知らないので、試してみません。ローカルスコープのタイプが含まれる場合は、怠惰が問題にならないようにcase式を使用します。あなたのコードについては

、ScopedTypeVariablesが実際にあなたにはるかに簡潔オプション提供：

{-# Language ScopedTypeVariables, GADTs #-} 

import Data.Typeable 
import Data.Proxy 

data Foo where 
    Foo :: Typeable a => a -> Foo 

fooType :: Foo -> TypeRep 
fooType (Foo (x :: a)) = typeRep (Proxy :: Proxy a)