[GHC] #14441: GHC HEAD regression involving type families in kinds

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: #13790 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In GHC 8.2.1, this file typechecks: {{{#!hs {-# 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 | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14441 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType, | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #13790 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: simonpj (added) Comment: This was introduced in commit 74cd1be0b2778ad99566cde085328bde2090294a (`Don't deeply expand insolubles`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14441#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType, | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #13790 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14441#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType, | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #13790 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14441#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType, | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 12919 | Blocking: Related Tickets: #13790 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * blockedby: => 12919 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14441#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14441: GHC HEAD regression involving type families in kinds
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: high | Milestone: 8.4.1
Component: Compiler | Version: 8.3
Resolution: | Keywords: TypeInType,
| TypeFamilies
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: 12919 | Blocking:
Related Tickets: #13790 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: fixed | Keywords: TypeInType, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T14441 Blocked By: 12919 | Blocking: Related Tickets: #13790 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_compile/T14441 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14441#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC