Skip to content
  • Simon Peyton Jones's avatar
    Do not instantiate unification variables with polytypes · 10f83429
    Simon Peyton Jones authored
    Without -XImpredicativeTypes, the typing rules say that a function
    should be instantiated only at a *monotype*.  In implementation terms,
    that means that a unification variable should not unify with a type
    involving foralls.  But we were not enforcing that rule, and that
    gave rise to some confusing error messages, such as
      Trac #7264, #6069
    
    This patch adds the test for foralls.  There are consequences
    
     * I put the test in occurCheckExpand, since that is where we see if a
       type can unify with a given unification variable.  So
       occurCheckExpand has to get DynFlags, so it can test for
       -XImpredicativeTypes
    
     * We want this to work
          foo :: (forall a. a -> a) -> Int
          foo = error "foo"
       But that means instantiating error at a polytype!  But error is special
       already because you can instantiate it at an unboxed type like Int#.
       So I extended the specialness to allow type variables of openTypeKind
       to unify with polytypes, regardless of -XImpredicativeTypes.
    
       Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
       unification variable for the function arguments, which can be polymorphic.
    
     * GHC has a special typing rule for ($) (see Note [Typing rule
       for ($)] in TcExpr).  It unifies the argument and result with a
       unification variable to exclude unboxed types -- but that means I
       now need a kind of unificatdion variable that *can* unify with a
       polytype.
    
       So for this sole case I added PolyTv to the data type TcType.MetaInfo.
       I suspect we'll find mor uses for this, and the changes are tiny,
       but it still feel a bit of a hack.  Well the special rule for ($)
       is a hack!
    
    There were some consequential changes in error reporting (TcErrors).
    10f83429