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