[GHC] #13931: GHC incorrectly considers type family instances conflicting?

[GHC]

#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.html
 #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