#13931: GHC incorrectly considers type family instances conflicting? -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is, by a very circuitous route, a duplicate of #11715. Examine the definition of `~>`: {{{#!hs data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type }}} We can rewrite your first instance as {{{#!hs type instance MkCtx kx (TyFun kx Constraint -> Type) c x = Apply c x }}} Due to #11715, GHC can't differentiate between `Constraint` and `Type` in Core. This means that it would be unsafe to differentiate between these in a type family in Haskell (because type family instances in Haskell become type equality axioms in Core). So, let's replace `Type` and `Constraint` with `TC`. Then, our instances look like (with also some renaming) {{{#!hs type instance MkCtx kx1 (TyFun kx1 TC -> TC) c1 x1 = Apply c1 x1 type instance MkCtx kx2 (kx2 -> TC) c2 x2 = c2 x2 }}} Now, we must recall that the type family instance check uses ''infinitary'' unification (as documented [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... #compatibility-and-apartness-of-type-family-equations here] and explained in Section 6.3 of [http://cs.brynmawr.edu/~rae/papers/2014/axioms/axioms.pdf this paper]). Thus, the left-hand sides unify under the substitution `kx1 |-> TyFun kx1 TC`. And so GHC rejects these instances. This is a terribly sad story, but it's not a fresh bug, I'm afraid. Both of the problems that lead to this problem, #11715 and the need for infinitary unification, are active [https://github.com/ghc-proposals/ghc- proposals/pull/32 areas] of [http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf work]. If you agree with my analysis, please close this ticket, as I don't think keeping it open adds fresh insight to either problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13931#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13931: GHC incorrectly considers type family instances conflicting? -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 11715 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by vagarenko): * status: new => closed * resolution: => duplicate * related: => 11715 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13931#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13931: GHC incorrectly considers type family instances conflicting? -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11715 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): No, I meant what I said. I should have included `kx2 |-> kx1` as well, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13931#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler