GHC HEAD-only Core Lint error (Kind mis-match in inst coercion)
Originally discovered on a head.hackage
CI build here.
The following program (minimized from singletons-2.7
):
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
type family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type SingFunction1 f = forall t. Sing t -> Sing (f `Apply` t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
newtype SLambda (f :: a ~> b) =
SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }
type instance Sing = SLambda
data SList :: forall a. [a] -> Type where
SNil :: SList '[]
SCons :: Sing x -> Sing xs -> SList (x:xs)
type instance Sing = SList
data SNonEmpty :: forall a. NonEmpty a -> Type where
(:%|) :: Sing x -> Sing xs -> SNonEmpty (x:|xs)
type instance Sing = SNonEmpty
type family Id (x :: a) :: a where
Id x = x
data IdSym0 :: a ~> a
type instance Apply IdSym0 x = Id x
sId :: forall a (x :: a). Sing x -> Sing (Id x)
sId sx = sx
type family (.) (f :: b ~> c) (g :: a ~> b) (x :: a) :: c where
(f . g) x = f `Apply` (g `Apply` x)
data (.@#@$) :: (b ~> c) ~> (a ~> b) ~> a ~> c
data (.@#@$$) :: (b ~> c) -> (a ~> b) ~> a ~> c
data (.@#@$$$) :: (b ~> c) -> (a ~> b) -> a ~> c
type instance Apply (.@#@$) f = (.@#@$$) f
type instance Apply ((.@#@$$) f) g = (.@#@$$$) f g
type instance Apply ((.@#@$$$) f g) x = (f . g) x
(%.) :: forall b c a (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f -> Sing g -> Sing x -> Sing ((f . g) x)
(%.) sf sg sx = sf `applySing` (sg `applySing` sx)
type family Go (k :: a ~> b ~> b) (z :: b) (l :: [a]) :: b where
Go _ z '[] = z
Go k z (y:ys) = k `Apply` y `Apply` Go k z ys
data GoSym :: (a ~> b ~> b) -> b -> [a] ~> b
type instance Apply (GoSym k z) l = Go k z l
type family Listfoldr (k :: a ~> b ~> b) (z :: b) (l :: [a]) :: b where
Listfoldr k z l = Go k z l
sListfoldr :: forall a b (k :: a ~> b ~> b) (z :: b) (l :: [a]).
Sing k -> Sing z -> Sing l -> Sing (Listfoldr k z l)
sListfoldr sk sz = sGo
where
sGo :: forall l'. Sing l' -> Sing (GoSym k z `Apply` l')
sGo SNil = sz
sGo (sy `SCons` sys) = sk `applySing` sy `applySing` sGo sys
class PMonoid a where
type Mempty :: a
type Mappend (x :: a) (y :: a) :: a
data MappendSym0 :: a ~> a ~> a
data MappendSym1 :: a -> a ~> a
type instance Apply MappendSym0 x = MappendSym1 x
type instance Apply (MappendSym1 x) y = Mappend x y
class SMonoid a where
sMempty :: Sing (Mempty :: a)
sMappend :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Mappend x y)
class PFoldable t where
type Foldr (f :: a ~> b ~> b) (z :: b) (l :: t a) :: b
instance PFoldable [] where
type Foldr f z l = Listfoldr f z l
class SFoldable t where
sFoldr :: forall a b (f :: a ~> b ~> b) (z :: b) (l :: t a).
Sing f -> Sing z -> Sing l -> Sing (Foldr f z l)
instance SFoldable [] where
sFoldr = sListfoldr
type family FoldMap (f :: a ~> m) (l :: t a) :: m where
FoldMap f l = Foldr (MappendSym0 .@#@$$$ f) Mempty l
sFoldMap :: forall t a m (f :: a ~> m) (l :: t a).
(SFoldable t, SMonoid m)
=> Sing f -> Sing l -> Sing (FoldMap f l)
sFoldMap sf = sFoldr (singFun2 @((.@#@$$) MappendSym0) (singFun2 @MappendSym0 sMappend %.) `applySing` sf) sMempty
type family NEFold (l :: NonEmpty m) :: m where
NEFold (a :| as) = a `Mappend` FoldMap IdSym0 as
sNEFold :: forall m (l :: NonEmpty m). SMonoid m
=> Sing l -> Sing (NEFold l)
sNEFold (sa :%| sas) = sa `sMappend` sFoldMap (singFun1 @IdSym0 sId) sas
Fails Core Lint when compiled with optimizations on GHC HEAD:
$ ~/Software/ghc5/inplace/bin/ghc-stage2 -O -dcore-lint Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Worker Wrapper binds ***
Bug.hs:72:5: warning:
Kind mis-match in inst coercion
In the RHS of $wsNEFold_s1fa :: forall {m} {l :: NonEmpty m}.
Sing Mempty
-> (forall (x :: m) (y :: m).
Sing x -> Sing y -> Sing (Mappend x y))
-> Sing l
-> Sing (NEFold l)
In the body of lambda with binder m_s1f1 :: *
In the body of lambda with binder l_s1f2 :: NonEmpty m_s1f1
In the body of lambda with binder ww_s1f7 :: Sing Mempty
In the body of lambda with binder ww_s1f8 :: forall (x :: m_s1f1)
(y :: m_s1f1).
Sing x -> Sing y -> Sing (Mappend x y)
In the body of lambda with binder w_s1f4 :: Sing l_s1f2
In the body of letrec with binders w_s1f3 :: SMonoid m_s1f1
In the body of letrec with binders m_a153 :: *
In the body of letrec with binders l_a154 :: NonEmpty m_a153
In the body of letrec with binders $dSMonoid_a156 :: SMonoid m_a153
In the body of letrec with binders ds_d1dM :: Sing l_a154
In a case alternative: (:%| x_a15a :: m_a153,
xs_a15b :: [m_a153],
co_a15c :: l_a154 ~# (x_a15a ':| xs_a15b),
sa_ayq :: Sing x_a15a,
sas_ayr :: Sing xs_a15b)
In the body of letrec with binders sz_s1es :: Sing Mempty
In the RHS of sGo_s1er :: forall (l' :: [m_s1f1]).
Sing l'
-> Sing (Apply (GoSym (MappendSym0 .@#@$$$ IdSym0) Mempty) l')
In the body of lambda with binder l'_a12r :: [m_a153]
In the body of lambda with binder ds_d1d9 :: Sing l'_a12r
In a case alternative: (SCons x_a12C :: m_a153,
xs_a12D :: [m_a153],
co_a12E :: l'_a12r ~# (x_a12C : xs_a12D),
sy_ayn :: Sing x_a12C,
sys_ayo :: Sing xs_a12D)
Substitution: [TCvSubst
In scope: InScope {l'_a12r x_a12C xs_a12D co_a12E m_a153 l_a154
x_a15a xs_a15b co_a15c m_s1f1 l_s1f2}
Type env: [a12r :-> l'_a12r, a12C :-> x_a12C, a12D :-> xs_a12D,
a153 :-> m_s1f1, a154 :-> l_s1f2, a15a :-> x_a15a,
a15b :-> xs_a15b, s1f1 :-> m_s1f1, s1f2 :-> l_s1f2]
Co env: [a12E :-> co_a12E, a15c :-> co_a15c]]
(The full Core Lint error is pretty massive, so I have omitted it for brevity.)
On the other hand, this program passes GHC 8.10.1 and earlier, so this is a regression:
$ /opt/ghc/8.10.1/bin/ghc -O -dcore-lint Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
$ /opt/ghc/8.8.3/bin/ghc -O -dcore-lint Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )