[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):

 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