[GHC] #9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.

[GHC]

#9587: Type checking with type functions introduces many type variables, which
remain ambiguous. The code no longer type checks.
-------------------------------------+-------------------------------------
              Reporter:  oleg        |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
  (Type checker)                     |         Keywords:  type family,
            Resolution:              |  ambiguity check
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:  GHC         |       Blocked By:
  rejects valid program              |  Related Tickets:  #9607
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 Replying to [comment:7 oleg]:
 > I have played with giving type annotations for quite a long time,
 without success.
 ....
 > I wonder what wrong could happen if we just assume injectivity in such
 cases.

 If I understand simonpj correctly, he would like to make sure it is
 possible to give explicit signatures ''first'', even if those would be
 nasty to write and/or read, and only add inference rules for such
 afterwards. This sounds reasonable to me, but I'm no expert. Maybe this
 will finally push him to implement the explicit type applications he's
 mentioned in the past?

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