GHC HEAD regression: cannot instantiate higher-rank kind
The following program typechecks on GHC 8.2.2 and 8.4.2:
{-# 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
| ^^^^^^
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |