GHC HEAD regression involving TYPEs in type families
This program typechecks on GHC 8.2.2 and 8.4.1:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
-----
-- Type
-----
type instance Demote Type = Type
type instance Promote Type = Type
type instance DemoteX (a :: Type) = Demote a
type instance PromoteX (a :: Type) = Promote a
-----
-- Arrows
-----
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
However, it fails to typecheck on GHC HEAD:
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:34:34: error:
• Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’
• In the first argument of ‘(~>)’, namely ‘PromoteX a’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’
|
34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b
| ^^^^^^^^^^
Bug.hs:34:48: error:
• Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’
• In the second argument of ‘(~>)’, namely ‘PromoteX b’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’
|
34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b
| ^^^^^^^^^^
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |