#9607: Type checking regression between GHC 7.6 and 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: invalid | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by jmccarty): Indeed, I'm guessing it was a bug that 7.6 accepted my program. I would argue that the type is not per se ambiguous, GHC just can't see it. `leftUnit` is precisely as ambiguous as `rightUnit`, but `leftUnit` is considered unambiguous (I think) because the type family application simplifies, making the signature `Tensor s -> Tensor (n ': n ': s)`, and I guess `':` is accepted as injective. In principle, if the argument and return types of rightUnit are instantiated to some type, then `n` can be instantiated to a unique type (but GHC would have to invert `(s ++)` to determine it!). I don't really understand the ambiguity check, but I think GHC wants to check that `(s ++ '[n0, n0]) ~ (s ++ '[n, n])` implies `n0 ~ n`? This is provably true, but I certainly don't expect GHC to construct the inductive proof of this fact. I was hoping the type family injectivity proposal would allow declaring such a fact (but again, I don't know that GHC could verify it). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9607#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler