AllowAmbiguousTypes和命题平等:这里发生了什么？

Question

所以有一天我想出了如何编写这个函数(需要base-4.7.0.0或以后):

{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs #-}

import Data.Typeable

-- | Test dynamically whether the argument is a 'String', and boast of our 
-- exploit if so.
mwahaha :: forall a. Typeable a => a -> a
mwahaha a = case eqT :: Maybe (a :~: String) of
              Just Refl -> "mwahaha!"
              Nothing -> a

所以我被带走了,并决定尝试使用它来编写一个测试其参数类型是否为Show实例的函数.如果我理解正确的话应该不起作用,因为TypeReps只存在于单形类型中.所以这个定义自然不能进行类型检查:

isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
isShow a = case eqT :: Maybe (a :~: b) of
             Just Refl -> True
             Nothing -> False

{- 
/Users/luis.casillas/src/scratch.hs:10:11:
    Could not deduce (Typeable b0)
      arising from the ambiguity check for ‘isShow’
    from the context (Typeable a, Typeable b, Show b)
      bound by the type signature for
                 isShow :: (Typeable a, Typeable b, Show b) => a -> Bool
      at /Users/luis.casillas/src/scratch.hs:10:11-67
    The type variable ‘b0’ is ambiguous
    In the ambiguity check for:
      forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘isShow’:
      isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
-}

但要注意这个消息To defer the ambiguity check to use sites, enable AllowAmbiguousTypes.如果我启用该pragma,定义类型为typechecks,但是......

{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Typeable

isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
isShow a = case eqT :: Maybe (a :~: b) of
             Just Refl -> True
             Nothing -> False

{- Typechecks, but...

>>> isShow 5
False

>>> isShow (id :: String -> String)
False
-}

这里发生了什么？编译器选择什么类型b？它是Skolem型变量ExistentialTypes吗？

---

哦,呃,我刚问了这个问题并快速想出了如何回答:

whatsTheTypeRep :: forall a b. (Typeable a, Typeable b, Show b) => a -> TypeRep
whatsTheTypeRep a = typeRep (Proxy :: Proxy b)

{-
>>> whatsTheTypeRep 5
()

>>> isShow ()
True
-}

我仍然有兴趣听听这里发生了什么.这是违约规则吗？

Answer 1

打开-Wall,你会得到你的答案:)

<interactive>:50:11: Warning:
    Defaulting the following constraint(s) to type ‘()’
      (Typeable b0)
        arising from the ambiguity check for ‘isShow’
        at <interactive>:50:11-67
      (Show b0)
        arising from the ambiguity check for ‘isShow’
        at <interactive>:50:11-67
    In the ambiguity check for:
      forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
    In the type signature for ‘isShow’:
      isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool

(是的,这是默认规则)