title: AllowAmbiguousTypes and propositional equality: what's going on here?
body: <p>So the other day I figured out how to write this function (requires <code>base-4.7.0.0</code> or later):</p>
  
  <pre><code>{-# 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 =&gt; a -&gt; a
  mwahaha a = case eqT :: Maybe (a :~: String) of
                Just Refl -&gt; "mwahaha!"
                Nothing -&gt; a
  </code></pre>
  
  <p>So I got carried away and decided to try using this to write a function that tests whether its argument type is a <code>Show</code> instance.  This, if I understand it correctly shouldn't work, because <code>TypeRep</code>s only exist for monomorphic types.  So this definition, naturally, fails to typecheck:</p>
  
  <pre><code>isShow :: forall a b. (Typeable a, Typeable b, Show b) =&gt; a -&gt; Bool
  isShow a = case eqT :: Maybe (a :~: b) of
               Just Refl -&gt; True
               Nothing -&gt; 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) =&gt; a -&gt; 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) =&gt; a -&gt; 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) =&gt; a -&gt; Bool
  -}
  </code></pre>
  
  <p>But note the message <code>To defer the ambiguity check to use sites, enable AllowAmbiguousTypes</code>.  If I enable that pragma, the definition typechecks, but... </p>
  
  <pre><code>{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs #-}
  {-# LANGUAGE AllowAmbiguousTypes #-}
  
  import Data.Typeable
  
  isShow :: forall a b. (Typeable a, Typeable b, Show b) =&gt; a -&gt; Bool
  isShow a = case eqT :: Maybe (a :~: b) of
               Just Refl -&gt; True
               Nothing -&gt; False
  
  {- Typechecks, but...
  
  &gt;&gt;&gt; isShow 5
  False
  
  &gt;&gt;&gt; isShow (id :: String -&gt; String)
  False
  -}
  </code></pre>
  
  <p>What's going on here?  What type is the compiler choosing for <code>b</code>?  Is it a Skolem type variable, à la <code>ExistentialTypes</code>?</p>
  
  <hr>
  
  <p>Oh, duh, I just asked the question and figured out quickly how to answer it:</p>
  
  <pre><code>whatsTheTypeRep :: forall a b. (Typeable a, Typeable b, Show b) =&gt; a -&gt; TypeRep
  whatsTheTypeRep a = typeRep (Proxy :: Proxy b)
  
  {-
  &gt;&gt;&gt; whatsTheTypeRep 5
  ()
  
  &gt;&gt;&gt; isShow ()
  True
  -}
  </code></pre>
  
  <p>I'm still interested in hearing what's going on here.  Is it a defaulting rule?</p>