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 

Так я увлекся и решил попробовать использовать это, чтобы написать функцию, которая проверяет, является ли ее аргумент типа a Show экземпляр. Это, если я правильно понимаю, не должно работать, потому что TypeRep s существуют только для мономорфных типов. Таким образом, это определение, естественно, не в состоянии typecheck:

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. Если я включу эту прагму, определение 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? Является ли это переменной типа Сколема, à la 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 

(Да, это недобросовестное правило)