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

 I tried with 7.0.  Yes, if you omit the type signature for `te4`, GHC 7.0
 will infer the one you give.  But if you write in that type signature, 7.0
 will reject the program with the same error, which is hardly satisfactory.

 No, GHC 7.0 did not "guess" some type-variable equalities that would solve
 the constraints.  I have absolutely no idea how to do this in general, and
 GHC has never attempted to do so.  It's just that 7.0 allowed you to infer
 a type that, if you wrote it as the signature, would be rejected.  GHC 7.4
 etc don't do that, which on the whole is a good thing.  While I could
 reverse that decision, it doesn't seem like the right way to solve the
 problem.

 The right way is to get GHC to make right instantiations, along the lines
 you mention.  How can we do that?  Usually by supplying some type
 signatures.  I don't understand the code well enough, but can you do this?
   * write the type sig for `te4`, using a `forall` so that the type
 variables scope over the body,
   * give some type signatures in the body so that the type variable
 equalities you want are forced

 Alternatively, do you have any other suggestions for how to guide GHC to
 make the right choices during inference?  Especially if injectivity won't
 do it.

 Mind you, injectivity might do it if you used an auxiliary family for the
 particular `repr` you care about.  Eg
 {{{
 type family Arr r a b :: *
 type instance Arr MyRepr a b = MyArr a b       -- Arr is not injective

 type family MyArr a b :: *  | result -> a b    -- MyArr is injective
 }}}
 Might that work?

 I'm sure you will have other creative ideas.

 Simon

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