Zonk quantified tyvars with skolems
authorManuel M T Chakravarty <chak@cse.unsw.edu.au>
Fri, 19 Oct 2007 11:56:53 +0000 (11:56 +0000)
committerManuel M T Chakravarty <chak@cse.unsw.edu.au>
Fri, 19 Oct 2007 11:56:53 +0000 (11:56 +0000)
commitcad764aa566442b08b1e68bf2c937772442a87cd
tree69fc204b8818db6db8e62d67397eca9d8a619783
parent3f1d7cd8eea305b13b39b304df23bbc680a729f0
Zonk quantified tyvars with skolems

We used to zonk quantified type variables to regular TyVars.  However, this
leads to problems.  Consider this program from the regression test suite:

  eval :: Int -> String -> String -> String
  eval 0 root actual = evalRHS 0 root actual

  evalRHS :: Int -> a
  evalRHS 0 root actual = eval 0 root actual

It leads to the deferral of an equality

  (String -> String -> String) ~ a

which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
In the meantime `a' is zonked and quantified to form `evalRHS's signature.
This has the *side effect* of also zonking the `a' in the deferred equality
(which at this point is being handed around wrapped in an implication
constraint).

Finally, the equality (with the zonked `a') will be handed back to the
simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
If we zonk `a' with a regular type variable, we will have this regular type
variable now floating around in the simplifier, which in many places assumes to
only see proper TcTyVars.

We can avoid this problem by zonking with a skolem.  The skolem is rigid
(which we requirefor a quantified variable), but is still a TcTyVar that the
simplifier knows how to deal with.
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcTyFuns.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs