Opened 11 months ago

Closed 7 months ago

#14441 closed bug (fixed)

GHC HEAD regression involving type families in kinds

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.4.1
Component: Compiler Version: 8.3
Keywords: TypeInType, TypeFamilies Cc: simonpj, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T14441
Blocked By: #12919 Blocking:
Related Tickets: #13790 Differential Rev(s):
Wiki Page:

Description

In GHC 8.2.1, this file typechecks:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k

data Prox (a :: k) = P

type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
$(return [])
type instance DemoteX P = P

(Note that the $(return []) line is essential, as it works around #13790.)

However, on GHC HEAD, this now fails:

$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:15:27: error:
    • Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’
    • In the type ‘P’
      In the type instance declaration for ‘DemoteX’
   |
15 | type instance DemoteX P = P
   |                           ^

Change History (6)

comment:1 Changed 11 months ago by RyanGlScott

Cc: simonpj added

This was introduced in commit 74cd1be0b2778ad99566cde085328bde2090294a (Don't deeply expand insolubles).

comment:2 Changed 11 months ago by simonpj

Cc: goldfire added

Gah! This is a nice small test case thank you.

In TcFlatten.flatten_exact_fam_app_fully I see

                   -- NB: fsk's kind is already flattend because
                   --     the xis are flattened
                   ; return (mkTyVarTy fsk, maybeSubCo eq_rel (mkSymCo co)
                                            `mkTransCo` ret_co ) }

But the comment is a lie. With the DemoteX above, the fsk will have type Demote k for some kind k, which is not flat. So the flattener's invariant (that flattened types have flattened kinds) is not respected). And that is ultimately the reason that we don't kick out an inert constraint that we should.

Richard, what do you think?

comment:3 Changed 11 months ago by simonpj

We have in play #12919, which completely rewrites the flattening code. It also fixes at least six other tickets: the current setup is outright wrong.

So Richard and I propose to park this bug and return to it when #12919 is committed.

comment:4 Changed 11 months ago by simonpj

Blocked By: 12919 added

comment:5 Changed 7 months ago by Richard Eisenberg <rae@…>

In e3dbb44f/ghc:

Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.

comment:6 Changed 7 months ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T14441
Note: See TracTickets for help on using tickets.