[GHC] #15704: Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types

[GHC]

#15704: Different saturations of the same polymorphic-kinded type constructor
aren't seen as apart types
-------------------------------------+-------------------------------------
        Reporter:  mniip             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.6.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #9371             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * related:   => #9371


Comment:

 Ah, I think I've figured out why this is happening. This all dates back to
 #9371, the fix for which is
 [http://git.haskell.org/ghc.git/blob/fc2ff6dd7496a33bf68165b28f37f40b7d647418:/compiler/types/Unify.hs#l348
 explained] in `Note [Lists of different lengths are MaybeApart]`:

 {{{#!hs
 {-
 Note [Lists of different lengths are MaybeApart]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
 lengths. The place where we know this can happen is from
 compatibleBranches in
 FamInstEnv, when checking data family instances. Data family instances may
 be
 eta-reduced; see Note [Eta reduction for data family axioms] in
 TcInstDcls.

 We wish to say that

   D :: * -> * -> *
   axDF1 :: D Int ~ DFInst1
   axDF2 :: D Int Bool ~ DFInst2

 overlap. If we conclude that lists of different lengths are SurelyApart,
 then
 it will look like these do *not* overlap, causing disaster. See Trac
 #9371.

 In usages of tcUnifyTys outside of family instances, we always use
 tcUnifyTys,
 which can't tell the difference between MaybeApart and SurelyApart, so
 those
 usages won't notice this design choice.
 -}
 }}}

 If it's not clear from context, this issue was that both of these data
 family instances were present:

 {{{#!hs
 data family D :: * -> * -> *

 data instance D Int a
 data instance D Int Bool
 }}}

 Normally, it would be quite simple to check that `D Int a` and `D Int
 Bool` overlapped. However, GHC eta-reduces `forall a. D Int a ~ DFInst1 a`
 to just `D Int ~ DFInst1`, which means that GHC was checking if `D Int`
 and `D Int Bool` were apart—and before #9371 was fixed, GHC mistakenly
 concluded that they //were// apart!

 This Note is referenced from
 [http://git.haskell.org/ghc.git/blob/fc2ff6dd7496a33bf68165b28f37f40b7d647418:/compiler/types/Unify.hs#l1038
 unify_tys] (which determines whether things are apart in type family
 instance consistency checks):

 {{{#!hs
 unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
 unify_tys env orig_xs orig_ys
   = go orig_xs orig_ys
   where
     go []     []     = return ()
     go (x:xs) (y:ys)
       -- See Note [Kind coercions in Unify]
       = do { unify_ty env x y (mkNomReflCo $ typeKind x)
            ; go xs ys }
     go _ _ = maybeApart  -- See Note [Lists of different lengths are
 MaybeApart]
 }}}

 And indeed, inserting some traces in `unify_tys` reveals that it's trying
 to unify `[* -> * -> k_a1B5, Int, Bool]` and `[* -> k_a1Bi, Int]` (the
 arguments to `D` in each instance of `F`), which are of different lengths,
 causing `unify_tys` to return `maybeApart` and later conclude that `F (D
 Int)` overlaps with `F (D Int Bool)`.

 I'm still not sure what exactly should be done here. If you revert the fix
 for #9371, then the program in this ticket will compile, but then the
 `T9371` test case will segfault again. At the same time, the fix for #9371
 is too conservative, since it rules out the perfectly valid program in
 this ticket. There must be some sort of middle ground here, but I don't
 know what that would be.

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