Skip to content
  • chak@cse.unsw.edu.au.'s avatar
    Zonk quantified tyvars with skolems · cad764aa
    chak@cse.unsw.edu.au. authored
    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.
    cad764aa