Ambiguous type variable when wrapping typeclass function in existential

Question

I'm using a typed tagless final encoding in an interpreter. Unfortunately, I'm having issues with the typechecking phase. The minimal testcase is as follows:

{-# LANGUAGE RankNTypes, ExistentialQuantification, NoMonomorphismRestriction #-}
class Program repr where
    ...
    intro1 :: repr a (a, ())
    ...

data DynTerm repr = forall x y. (Typeable x, Typeable y) => DynTerm (repr x y)

ghci> DynTerm intro1

This produces the following error:

Could not deduce (Typeable x0) arising from a use of `DynTerm'
from the context (Program repr)
  bound by the inferred type of it :: Program repr => DynTerm repr
  at <interactive>:3:1-14
The type variable `x0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
Note: there are several potential instances:
  instance Typeable Void -- Defined in `Data.Void'
  instance [overlap ok] Typeable ()
    -- Defined in `Data.Typeable.Internal'
  instance [overlap ok] Typeable Bool
    -- Defined in `Data.Typeable.Internal'
  ...plus 25 others
In the expression: DynTerm intro1
In an equation for `it': it = DynTerm intro1

I expected the compiler to reason as follows:

• Attempt to unify a with x.
• Add Typeable a to the list of constraints (I can manually add this through a type annotation, which makes no difference).
• Succeed.
• Attempt to unify (a, ()) with y.
• Note that since we're assuming Typeable a, Typeable (a, ()) also holds.
• Succeed.

However, it seems to be failing on unifying x.

Answer 1

When constructing a value of type DynTerm using the DynTerm constructor, GHC has to know the concrete types x and y in order to decide which Typeable dictionaries should be packed in. In your test expression, you are not providing sufficient type information to determine concrete types, therefore you get an error that certain type variables are ambiguous. It works if you specifically pick a concrete Typeable type.

Example (with ScopedTypeVariables):

test :: forall repr. Program repr => DynTerm repr
test = DynTerm (intro1 :: repr Int (Int, ()))

Answer 2

As kosmikus noted, ExistentialQuantification means that you will abstract over the type variable, but the implementer of your data type must pick a single, monomorphic type:

When a value of this type is constructed, s will be instantiated to some concrete type. When such a value is analysed, s is abstract.

Consider the following:

data D = forall a . Show a => D (a -> String) 
-- test0 = D show -- Invalid!
test1 = D (show :: () -> String)

data E = E (forall a . Show a => a -> String)
test2 = E show -- Invalid!
-- test3 = E (show :: () -> String)

So perhaps you want

data DynTerm repr = DynTerm (forall x y. (Typeable x, Typeable y) => repr x y)

But this still won't work with intro1 - it is not sufficiently polymorphic ((a,()) is more specific than x). If you had intro2 :: Program repr => repr x y you could write DynTerm intro2.