AllowAmbiguousTypes and propositional equality: what's going on here?

Question

So the other day I figured out how to write this function (requires base-4.7.0.0 or later):

{-# 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

So I got carried away and decided to try using this to write a function that tests whether its argument type is a Show instance. This, if I understand it correctly shouldn't work, because TypeReps only exist for monomorphic types. So this definition, naturally, fails to 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
-}

But note the message To defer the ambiguity check to use sites, enable AllowAmbiguousTypes. If I enable that pragma, the definition typechecks, but...

{-# 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
-}

What's going on here? What type is the compiler choosing for b? Is it a Skolem type variable, à la ExistentialTypes?

---

Oh, duh, I just asked the question and figured out quickly how to answer it:

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

{-
>>> whatsTheTypeRep 5
()

>>> isShow ()
True
-}

I'm still interested in hearing what's going on here. Is it a defaulting rule?

Answer 1

Turn on -Wall and you'll get your answer :)

<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

(Yes, it's a defaulting rule)