Opened 12 months ago

Closed 9 months ago

#15704 closed bug (fixed)

Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types

Reported by: mniip Owned by: mniip
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.6.1
Keywords: TypeFamilies Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_compile/T15704
Blocked By: Blocking:
Related Tickets: #9371 Differential Rev(s): Phab:D5206
Wiki Page:

Description

{-# LANGUAGE TypeFamilies, PolyKinds #-}

module A where

data family D :: k

type family F (a :: k) :: *

type instance F (D Int) = Int
type instance F (f a b) = Char
type instance F (D Int Bool) = Char

The last equation, even though a specialization of the middle one, trips up the equality consistency check:

a.hs:9:15: error:
    Conflicting family instance declarations:
      F (D Int) = Int -- Defined at a.hs:9:15
      F (D Int Bool) = Char -- Defined at a.hs:10:15
  |
9 | type instance F (D Int) = Int
  |               ^

So GHC is able to infer that D Int ~/~ f a b because D ~/~ f a, but for some reason the same reasoning doesn't work for D ~/~ D a.

Change History (11)

comment:1 Changed 12 months ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 12 months ago by goldfire

Good point. Types with different numbers of arguments should be apart.

comment:3 Changed 12 months ago by RyanGlScott

Ah, I think I've figured out why this is happening. This all dates back to #9371, the fix for which is explained in Note [Lists of different lengths are MaybeApart]:

{-
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:

data family D :: * -> * -> *

data instance D Int a
data instance D Int Bool

(Note that this is a different data family D than the one in the program in this ticket.)

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!

(For the rest of this comment, when I refer to D, I will be referring to the one in the program in this ticket, #15704, not the one from that Note.)


This Note is referenced from unify_tys (which determines whether things are apart in type family instance consistency checks):

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.

Last edited 12 months ago by RyanGlScott (previous) (diff)

comment:4 Changed 12 months ago by mniip

Considering unify_tys is called recursively from when unify_ty needs to match a constructor application, I think this functionality of "Maybe"ing out on lists of different lengths needs to be moved somewhere closer to coaxiom compatibility checking and further away from unify_tys.

comment:5 Changed 12 months ago by mniip

Owner: set to mniip

comment:6 Changed 12 months ago by mniip

Differential Rev(s): Phab:D5206

comment:7 Changed 11 months ago by Ben Gamari <ben@…>

In f877d9c/ghc:

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

comment:8 Changed 11 months ago by simonpj

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

comment:9 in reply to:  8 Changed 11 months ago by mniip

Replying to simonpj:

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 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:

ty1 = D @(Type -> Type) Int               :: Type
ty2 = D @(Type -> Type -> Type) Int Bool  :: Type

comment:10 Changed 10 months ago by Simon Peyton Jones <simonpj@…>

In fe057642/ghc:

Comments only, about polykinded TyConApps

See Trac #15704 comment:8ff

comment:11 Changed 9 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T15704

I think this is done

Note: See TracTickets for help on using tickets.