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, ()))