#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