[GHC] #15079: GHC HEAD regression: cannot instantiate higher-rank kind

23 Apr 2018


      #15079: GHC HEAD regression: cannot instantiate higher-rank kind
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program typechecks on GHC 8.2.2 and 8.4.2:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Void

 infixl 4 :==
 -- | Heterogeneous Leibnizian equality.
 newtype (a :: j) :== (b :: k)
   = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a ->
 c b }

 newtype Coerce a = Coerce { uncoerce :: Starify a }
 type family Starify (a :: k) :: Type where
   Starify (a :: Type) = a
   Starify _           = Void

 coerce :: a :== b -> a -> b
 coerce f = uncoerce . hsubst f . Coerce
 }}}

 But GHC HEAD rejects it:

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

 Bug.hs:21:34: error:
     • Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:
         Coerce :: forall k. k -> *
       Their kinds differ.
       Expected type: a -> c0 * a
         Actual type: Starify a -> Coerce a
     • In the second argument of ‘(.)’, namely ‘Coerce’
       In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
       In the expression: uncoerce . hsubst f . Coerce
    |
 21 | coerce f = uncoerce . hsubst f . Coerce
    |                                  ^^^^^^
 }}}

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