Omitting explicit forall yields ambiguous type error
ghc, haskell, types
Solution
The `ScopedTypeVariables` extension adds semantic value to top-level `forall` quantifiers. It is what provides the scoping for the type variable over the body of the binding.
Without that `forall`, the type variable `a` on line 3 is a different type variable than the `a` on line 1. The error message indicates this by labeling them `a0` and `a1`. Without those being the same type, the type on line 3 is ambiguous, because it is completely unconstrained.
Problem
I've run into a situation where a function fails to type-check unless I explicitly add a forall to the beginning of its type signature. The function in question is: ``` test :: (Typeable a) => a -> a test x | typeOf (undefined :: a) == typeOf (undefined :: a) = x | otherwise = x ``` GHC gives the following warnings on the above: ``` Ambiguous type variable `a0' in the constraint: (Typeable a0) arising from a use of `typeOf' Probable fix: add a type signature that fixes these type variable(s) In the first argument of `(==)', namely `typeOf (undefined :: a)' In the expression: typeOf (undefined :: a) == typeOf (undefined :: a) In a stmt of a pattern guard for an equation for `test': typeOf (undefined :: a) == typeOf (undefined :: a) Ambiguous type variable `a1' in the constraint: (Typeable a1) arising from a use of `typeOf' Probable fix: add a type signature that fixes these type variable(s) In the second argument of `(==)', namely `typeOf (undefined :: a)' In the expression: typeOf (undefined :: a) == typeOf (undefined :: a) In a stmt of a pattern guard for an equation for `test': typeOf (undefined :: a) == typeOf (undefined :: a) ``` So it's failing to unify the two types of the undefined values. However if I add a forall a to the front: ``` test :: forall a. (Typeable a) => a -> a test x | typeOf (undefined :: a) == typeOf (undefined :: a) = x | otherwise = x ``` It compiles fine. This is in GHC 7.4.2 using ``` {-# LANGUAGE GADTs, StandaloneDeriving, DeriveDataTypeable, ScopedTypeVariables, FlexibleInstances, UndecidableInstances, Rank2Types #-} ``` I was under the impression that omitting "forall" in a type signature was equivalent to implicitly appending foralls to the beginning over all relevant type variables (as suggested in the GHC docs: http://www.haskell.org/ghc/docs/7.4.2/html/users_guide/other-type-extensions.html). Why does the first code fragment not type-check, while the second does?