Several days ago, I implemented an experimental type inference system with first-class polymorphism. When comparing it with other systems, I found a possible bug in GHC’s type system regarding universal quantification. The phenomemon was confirmed and reproduced by people at #haskell IRC channel for GHC versions above 7.01. The code that causes trouble is:
gen :: [forall a. a -> a] gen = [id] test1 = head gen 1
Obviously this program should typecheck, since:
id
has the typeforall a. a -> a
.- A list
gen
containingid
should have type[forall a. a -> a]
(as in the annotation). head
has the typeforall a. [a] -> a
.head gen
should have the typeforall a. a -> a
.head gen
should be able to be applied to1
.
But GHC rejected this program for a strange reason.
Couldn't match expected type `t1 -> t0' with actual type `forall a. a -> a' Expected type: [t1 -> t0] Actual type: [forall a. a -> a] In the first argument of `head', namely `gen' In the expression: head gen 1
On the other hand, it works if (head gen) is bound at let:
test2 = let hg = head gen in hg 1
It doesn’t break the soundness of the type system since it only rejects some correct programs, but this kind of pecularities of type systems can be painful when they add up. I guess this may be caused by the interaction between GHC’s internal type system with the legacy let-polymorphism.