#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