Reason for overlapping instances error when not quantifying method existentially

Question

Given the following code, removing forall a r from the type of go fails with "Overlapping instances for Typeable (D r)". I wonder why?

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
module M where

import Data.Typeable (Proxy, Typeable, cast)

class C r where
    data D r :: *

deriving instance Typeable D

data A = forall r . A (D r)

go :: forall r a . (Typeable a, Typeable (D r)) => a -> Proxy r -> A
go a _ = case cast a of
  Just (b :: D r) -> A b
  Nothing -> error "fail to cast"

The error also says "The choice depends on the instantiation of r" - but isn't that pinned by the supplied Proxy r?

Answer 1

This is how scoped type variables work in Haskell. Note that you are re-using r here:

go :: forall r a . (Typeable a, Typeable (D r)) => a -> Proxy r -> A
go a _ = case cast a of
  Just (b :: D r) -> A b  -- this r is the same as the r above

Without the explicit forall, type variables are interpreted to be local to the signature. That is, your code is read as:

go :: (Typeable a1, Typeable (D r1)) => a1 -> Proxy r1 -> A  -- renaming local variables
go a _ = case cast a of
  Just (b :: D r) -> A b   -- r bears no relation to r1

Hence the type error.

(It is confusing to get an Overlapping instances error, though.)