[GHC] #14991: GHC HEAD regression involving TYPEs in type families

2 Apr 2018


      #14991: GHC HEAD regression involving TYPEs in type families
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This program typechecks on GHC 8.2.2 and 8.4.1:

 {{{#!hs
 {-# 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
    |                                                ^^^^^^^^^^
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler