typeclass制約の存在量の定量化

Question

なぜkoが型チェックをしないのか分かりません。 特に啓発的な説明がありますか？

{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances #-} 

module Wrap where 

class ExpSYM repr where 
    lit :: Int -> repr 

newtype Wrapped = Wrapped{unWrap :: forall repr. ExpSYM repr => repr} 

a = (lit <$> Just 5) :: ExpSYM expr => Maybe expr 

ko :: Maybe Wrapped 
ko = do v <- a 
     return $ Wrapped $ v 

ok :: Maybe Wrapped 
ok = do v <- Just 5 
     let e = lit v 
     return $ Wrapped $ e 

コンパイラは言及

SO.hs:15:14: error: 
    • No instance for (ExpSYM a0) arising from a use of ‘a’ 
    • In a stmt of a 'do' block: v <- a 
     In the expression: 
     do { v <- a; 
      return $ Wrapped $ v } 
     In an equation for ‘ko’: 
      ko 
      = do { v <- a; 
        return $ Wrapped $ v } 

SO.hs:16:28: error: 
    • Couldn't match expected type ‘repr’ with actual type ‘a0’ 
     because type variable ‘repr’ would escape its scope 
     This (rigid, skolem) type variable is bound by 
     a type expected by the context: 
      ExpSYM repr => repr 
     at SO.hs:16:18-28 
    • In the second argument of ‘($)’, namely ‘v’ 
     In the second argument of ‘($)’, namely ‘Wrapped $ v’ 
     In a stmt of a 'do' block: return $ Wrapped $ v 
    • Relevant bindings include v :: a0 (bound at SO.hs:15:9) 
Failed, modules loaded: none. 

編集： 素敵な解決策は、多型は型アプリケーションによって除去されるように、タイプを特化することであるオレグのノートでこれを回避することが判明、インスタンスを追加する。

instance ExpSYM Wrapped where 
    lit x = Wrapped $ lit x 

w aのタイプは

a :: Maybe (∀ expr . ExpSYM expr => expr) 
a = lit <$> Just 5 

た場合にのみ、あなたはそれが多型値v :: ∀ expr . ExpSYM expr => exprを取得するために、アンラップ行うことができるようになるので、電子はその後

notko :: Maybe Wrapped 
notko = do v <- a  
      return $ v -- note the difference. what's the type of a ? 

-- and we get all the usual goodies, no silly impredicative error 
alsoOk = lit <$> Just 5 :: Maybe Wrapped 

Answer 1

koを持っていることだけ...働くだろう。その値は多形でなければならないので、実際にはWrappedで使用できます。

しかし、Maybe (∀ expr . ExpSYM expr => expr)は、impredicative typeです。 GHC Haskellは批判的なタイプをサポートしていません。

OTOH、ok、vは、不明瞭なJust 5 :: Maybe Intからのちょうど退屈な古い整数です。 eだけが多型性を導入しますが、Maybeモナドの外側でそうします。