#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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15704#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#15704: Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types -------------------------------------+------------------------------------- Reporter: mniip | Owner: mniip 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 mniip): * owner: (none) => mniip -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15704#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15704: Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types -------------------------------------+------------------------------------- Reporter: mniip | Owner: mniip 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): Phab:D5206 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"f877d9cc99dd1ba0c038e70527031e9ba0934cd3/ghc" f877d9c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="f877d9cc99dd1ba0c038e70527031e9ba0934cd3" Move eta-reduced coaxiom compatibility handling quirks into FamInstEnv. The quirk caused an issue where GHC concluded that 'D' is possibly unifiable with 'D a' (the two types could have the same kind if D is a data family). Test Plan: Ensure T9371 stays fixed. Introduce T15704 Reviewers: goldfire, bgamari Reviewed By: goldfire Subscribers: RyanGlScott, rwbarton, carter GHC Trac Issues: #15704 Differential Revision: https://phabricator.haskell.org/D5206 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15704#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

I like this fix. But can I ask about this in `Unify.hs`: {{{ - go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart] + go _ _ = surelyApart + -- Possibly different saturations of a polykinded tycon (See Trac #15704) }}} I don't see where in this ticket we discuss "possibly different saturations of a polykinded tycon".

It'd be more direct simply to give an example. Do you have in mind

#15704: Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types -------------------------------------+------------------------------------- Reporter: mniip | Owner: mniip 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): Phab:D5206 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mniip): Replying to [comment:8 simonpj]: this?

{{{ T :: forall k. Type -> k

ty1 = T Type Int :: Type ty2 = T (Type->Type) Int Int :: Type }}} Or did you have other examples in mind?

Thanks

The `D` in the ticket is a polykinded tycon: {{{#!hs ty1 = D @(Type -> Type) Int :: Type ty2 = D @(Type -> Type -> Type) Int Bool :: Type }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15704#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15704: Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types -------------------------------------+------------------------------------- Reporter: mniip | Owner: mniip Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T15704 Blocked By: | Blocking: Related Tickets: #9371 | Differential Rev(s): Phab:D5206 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed-types/should_compile/T15704 * resolution: => fixed Comment: I think this is done -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15704#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler