patch applied (ghc): Zonk quantified tyvars with skolems

chak at cse.unsw.edu.au chak at cse.unsw.edu.au
Fri Oct 19 08:58:54 EDT 2007


Fri Oct 19 04:56:53 PDT 2007  Manuel M T Chakravarty <chak at cse.unsw.edu.au>
  * 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.

    M ./compiler/typecheck/TcMType.lhs -7 +40
    M ./compiler/typecheck/TcSimplify.lhs -5
    M ./compiler/typecheck/TcTyFuns.lhs -1 +1
    M ./compiler/typecheck/TcType.lhs -1 +11
    M ./compiler/typecheck/TcUnify.lhs -1 +4



More information about the Cvs-ghc mailing list