A bug in GHC's type systemSeveral 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:
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. |