Opened 2 months ago

Last modified 2 months ago

#14441 new bug

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:
Blocked By: #12919 Blocking:
Related Tickets: #13790 Differential Rev(s):
Wiki Page:


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 (4)

comment:1 Changed 2 months ago by RyanGlScott

Cc: simonpj added

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

comment:2 Changed 2 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 2 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 2 months ago by simonpj

Blocked By: 12919 added
Note: See TracTickets for help on using tickets.