[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:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by oleg):

 I have checked with GHC 7.4.1 as well. It does report the error you quote.
 And yet the code did work
 back in 2010 at least, and inferred the type mentioned in my original Trac
 submission. The change in type inference must have happened sometime
 around GHC 7.2->7.4. It did break the code, some of which I had to rewrite
 (and the rest just abandoned).

 Let's look at the error message closely:
 {{{
     Could not deduce (Arr repr (Arr repr a4 a3) (Arr repr a4 b)
                       ~ Arr repr (Arr repr a2 a1) (Arr repr a2 b0))
     from the context (ESymantics repr,
                       Arr repr a3 a ~ Arr repr a4 a3,
                       Arr repr a b ~ Arr repr a4 a3)
 }}}

 Since Arr is a function, then choosing a2~a4, a1~a3, b0~b will certainly
 satisfy the offending
 constraint. Since the type variables a2, a1, b0 are not mentioned anywhere
 else, there is no risk of conflicts. I think that's what GHC 7.0 (or 7.2)
 must have done. True, we must have lost principality. But the principality
 was lost already in Haskell98, so there is no use to worry about it now.

 I cannot help but notice the irony: type functions were introduced in 2005
 as a `functional' alternative to functional dependencies. Programming with
 functional dependencies was viewed as
 logic programming. We are functional programmers, we should program with
 functions. the slogan went. Alas, when it comes to inference, we need to
 know what can we infer about t1 and t2
 from Fn t1 ~ Fn t2. So, we do have to think relationally rather than
 functionally -- it is inherent. We have not escaped from the relational
 view -- merely made it harder to see, which is not always an advantage.

 BTW, adding the declaration for injective type families may be not enough.
 For example, consider our Arr repr t1 t2. It could be that Arr repr t1 t2
 is injective only for specific repr. We intend to use our example only
 with such repr. But Arr repr t1 t2 may be usable for different repr, which
 do not correspond to injective Arr repr.

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