[GHC] #9404: tcInferRho muddies the waters

#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- In trying to understand the algorithm implemented in !TcExpr, I've spent some time examining `tcInferRho`. I conjecture that this function is superfluous and should be removed, in favor of `tcInfer . tcExpr`. Some of these thoughts were first written up in [http://www.haskell.org/pipermail /ghc-devs/2014-July/005733.html this thread]. After a considerable amount of staring, I've actually found a misbehavior caused by the current implementation. `tcInferRho` calls `tcInfExpr`, which has only 3 special cases before calling `tcInfer . tcExpr`: for variables, parentheses, and application. I was first drawn into this problem because these three cases seem woefully insufficient for the problem at hand. I was surprised how such a paucity of cases could have survived without causing havoc, if indeed `tcInferRho` were necessary at all. For example, only normal (prefix) application is handled; infix application is missing. In looking at differences between `tcInferApp` (which is called from the application case of `tcInfExpr`) and `tcApp` (called from `tcExpr`), I saw that the former doesn't have a special case for `seq` while the latter does. And, indeed, this difference is exploitable. This compiles fine: {{{ foo _ = case () `seq` (# #) of (# #) -> () }}} This does not: {{{ foo _ = case seq () (# #) of (# #) -> () }}} which produces {{{ Scratch.hs:15:21: Kind incompatibility when matching types: b0 :: * (# #) :: # In the second argument of ‘seq’, namely ‘(##)’ In the expression: seq () (##) }}} Looking at the code, this behavior is expected, because the first version of the code calls into `tcInfer . tcExpr`, which special-cases `seq`, while the second is caught by `tcInferApp`, which doesn't have the special case. The above example shows that this isn't just a theoretical concern about code cleanup! This all leads to another question: Why special-case `seq` at all? !MkId tells me that {{{ seq :: forall (a :: *) (b :: *). a -> b -> b }}} Why isn't it {{{ seq :: forall (a :: *) (b :: OpenKind). a -> b -> b }}} With the second type, I would imagine that `seq` wouldn't need a special case in the type-checker. Is there something wrong with the second type for `seq`? I'll post more thoughts to this ticket as I continue to explore. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): I've tried removing `tcInfExpr`, in favor of having `tcInferRhoNC` call `tcExpr` directly. I'll post here once I see how it goes. I didn't find other special cases worth mentioning. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): I think you are right. Try giving `seq` that type, and removing the special case. (There would need to be a Note with the new type of course.) The situation with tcInfer etc is still not cool, but other things being equal simpler is definitely better. Maybe you can try these changes in HEAD, not just on nokinds? Thanks Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Ah, yes, that makes good sense. Patch will arrive soon. Thanks for the explanation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): This is subtler than I thought. The email trail linked in the original description suggests that TauTvs can be unified with forall-types, but cannot be solved to become a forall-type. This is true, but only partially: the forall-type in question must be devoid of any type families, *and* the TauTv must be of kind `OpenKind`. I have implemented, in a branch [https://github.com/goldfirere/ghc/tree /removed-tcInfExpr here], a version of GHC missing `tcInfExpr`, the under- implemented version of `tcExpr` that infers a type instead of checking it. The problem is that, in that branch, the following fails: {{{ {-# LANGUAGE RankNTypes, TypeFamilies #-} module Rank where type family ListTF x where ListTF x = [x] bar :: (forall x. ListTF x -> Int) -> () bar _ = () foo = bar $ length }}} For the curious, the error message is {{{ Couldn't match type ‘[a0] -> Int’ with ‘forall x. ListTF x -> Int’ Expected type: ([a0] -> Int) -> () Actual type: (forall x. ListTF x -> Int) -> () In the expression: bar In the expression: bar $ length }}} So, the "obvious" fix to the original bug doesn't work. The problem outlined in this comment (interaction between the mention of type families and inference) can be observed in 7.8, with the following rather contrived construction: {{{ {-# LANGUAGE RankNTypes, TypeFamilies #-} module Rank where type family ListTF x where ListTF x = [x] bar :: (forall x. ListTF x -> Int) -> () bar _ = () myconst :: ((forall r. ListTF r -> Int) -> ()) -> x -> (forall r. ListTF r -> Int) -> () myconst x _ = x foo = (bar `myconst` ()) $ length }}} If, in the last line, `myconst` is applied prefix instead of infix, the module compiles. It seems the solution here is to fully implement `tcInfExpr`, instead of eliminate it, so that `tcInfExpr` is aware of infix operators, sections, and probably other expression forms. With that done, the problems outlined here should go away. But, given the smelliness around all of this, I think it's best to let The Expert (who is on holiday, I understand) weigh in before proceeding. It's also worth noting that the problems I've encountered to post this ticket have all been "white box" -- I detected the problem reading GHC source code, not by stumbling into it. It's quite possible that this infelicity has never triggered a problem in the wild. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 simonpj): Re the last question, here's the comment in HEAD {{{ -- Make sure that the argument type has kind '*' -- Eg we do not want to allow (D# $ 4.0#) Trac #5570 -- (which gives a seg fault) -- We do this by unifying with a MetaTv; but of course -- it must allow foralls in the type it unifies with (hence PolyTv)! -- -- The result type can have any kind (Trac #8739), -- so we can just use res_ty -- ($) :: forall (a:*) (b:Open). (a->b) -> a -> b ; a_ty <- newPolyFlexibTyVarTy }}} Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Of course. How silly of me -- I saw that comment but somehow didn't realize it answered my question. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: patch 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: Phab:D469 | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => patch * differential: => Phab:D469 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9404: tcInferRho muddies the waters
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: patch
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: Phab:D469 |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#9404: tcInferRho muddies the waters
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: patch
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: Phab:D469 |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#9404: tcInferRho muddies the waters
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: patch
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: Phab:D469 |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: patch 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: Phab:D469 | -------------------------------------+------------------------------------- Comment (by goldfire): Keeping ticket open. I merged my solution at Simon's request, but there's still an outstanding refactoring task. See Phab:D469. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: patch 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: Phab:D469 | -------------------------------------+------------------------------------- Comment (by simonpj): Can you just lay out what the "refactoring task" is? Thanks -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: patch 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: Phab:D469 | -------------------------------------+------------------------------------- Comment (by goldfire): Simplifying the rule for `($)`, as you requested. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

This smells wrong. tcInferRho ends up calling tcInfer, which makes an OpenKind ReturnTv. But then we unify it with a liftedTypeKind ReturnTv later.
Complicated and silly. Better if tcInferRho takes the kind it is expecting. Then we have only one ReturnTv, not two; and the whole ReturnTv story is located in tcInfer, rather than having a non-return-ish hack in
#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: patch 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: Phab:D469 | -------------------------------------+------------------------------------- Comment (by goldfire): On Phab:D469, Simon says, about line 328 of !TcExpr: the typing rule for $
Make sense?
I've decided: no, this doesn't make sense. The call to `tcInferRho` is to infer the type of the left-hand argument to `$`. This type is a function type `arg -> res`. If it turns out to be unlifted, the `matchExpectedFunTys` will fail. The silliness with the new `ReturnTy` bit isn't about the result of `tcInferRho` -- it's about the result of `matchExpectedFunTys`. So the straightforward refactoring Simon proposes doesn't work. Instead, what we should do here is to unify `arg2_ty`'s kind with `*`. But !TcUnify doesn't have a function for that -- something like `matchExpectedStar`. The closest thing -- `unifyKindX` tells us about sub- kinding relationships, instead of actually unifying the kinds. So, I propose: do nothing for now. It's working, although a little uglily, as is. When we have proper kind equalities and no sub-kinding anymore, this will be easy to fix. Please close the ticket if you agree. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9404: tcInferRho muddies the waters -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: Phab:D469 | -------------------------------------+------------------------------------- Changes (by simonpj): * status: patch => closed * resolution: => fixed Comment: Yes I agree. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9404#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC