[GHC] #9404: tcInferRho muddies the waters

[GHC]

#9404: tcInferRho muddies the waters
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |            Owner:  goldfire
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.9
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 A discussion with various Experts revealed the following story:

 GHC has a `PolyTv` flavor of meta-variable that, according to its
 description, is meant to unify with sigma-types. But, the original intent
 was more than that: it should unify with anything, always.

 We sometimes want `tcExpr` to ''check'' a type, and we sometimes want it
 to ''infer'' a type. We can imagine two functions like this: (indeed, we
 ''have'' two functions like this!)

 {{{
 tcInfExpr :: HsExpr Name -> TcM (HsExpr TcId, TcType)
 tcExpr :: HsExpr Name -> TcType -> TcM (HsExpr TcId)
 }}}

 If both of these were fully implemented, they would each have many similar
 cases and would be more work to maintain. This is why `tcInfExpr`
 currently has just a few cases and then delegates to `tcExpr`, passing in
 a unification variable. The problem is that the unification variable,
 currently a `TauTv`, won't unify with all types.

 What we want, in effect, is this:

 {{{
 data TcDirection = Infer (Ref TcType) | Check TcType
 tcExpr :: TcDirection -> HsExpr Name -> TcM (HsExpr TcId)
 }}}

 But, if we had a unification variable that unifies with ''anything'', then
 we have exactly that: the permissive unification variable is essentially a
 `Ref TcType`!

 We can use a `PolyTv` as this permissive unification variable. The
 ''only'' place where `PolyTv` is currently used is in the special typing
 rule for `($)` (and its presence there is suspect -- see below). So, all
 we have to do is update `checkTauTvUpdate` to not check `PolyTv`s at all,
 and we get this behavior for `PolyTv`.

 So, the current proposed solution is to get rid of `TcInfExpr` (as already
 done in my branch) and instead use a `PolyTv` in `tcInfer`, along with
 liberalizing the meaning of `PolyTv`.

 To make sure we've done this right, we should also verify that `PolyTv`s
 are indeed filled in right away, before the constraint solver.  In
 particular:
   * Zonking (even the partial zonking done by `zonkTcType` and friends)
 should ''never'' encounter a `Flexi` `PolyTv`. (Nagging worry about the
 possibility of underspecified types here.... may need defaulting.)
   * The constraint solver should ''never'' encounter a `PolyTv`.


 About `($)`: There is a curious piece of code here:

 {{{
 tcExpr (OpApp arg1 op fix arg2) res_ty
   | (L loc (HsVar op_name)) <- op
   , op_name `hasKey` dollarIdKey        -- Note [Typing rule for ($)]
   = do { traceTc "Application rule" (ppr op)
        ; (arg1', arg1_ty) <- tcInferRho arg1

        ; let doc = ptext (sLit "The first argument of ($) takes")
        ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1
 arg1_ty
        ; a_ty <- newPolyFlexiTyVarTy
        ; arg2' <- tcArg op (arg2, arg2_ty, 2)

        ; co_a   <- unifyType arg2_ty   a_ty      -- arg2 ~ a
        ; co_b   <- unifyType op_res_ty res_ty    -- op_res ~ res
        ; op_id  <- tcLookupId op_name

        ; let op' = L loc (HsWrap (mkWpTyApps [a_ty, res_ty]) (HsVar
 op_id))
        ; return $
          OpApp (mkLHsWrapCo (mkTcFunCo Nominal co_a co_b) $
                 mkLHsWrapCo co_arg1 arg1')
                op' fix
                (mkLHsWrapCo co_a arg2') }
 }}}

 My question is: why have `a_ty` at all? The type of the left-hand argument
 to `($)` is properly captured in `arg_ty`, and I can't see a reason to
 then unify with the fresh `a_ty`. Does anyone have insight here?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9404#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler