GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"
Commit c955a514 (Remove decideKindGeneralisationPlan) causes the singletons library to no longer compile. Here is as minimal of an example as I can muster:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug (sPermutations) where
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k -> Type
data instance Sing :: forall a. [a] -> Type where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x:xs)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
type family Undefined :: k where {}
sUndefined :: a
sUndefined = undefined
type family LetGo k z x ys where
LetGo k z x '[] = z
LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys)
type family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where
Foldr k z x = LetGo k z x x
sFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]).
Sing t1 -> Sing t2 -> Sing t3
-> Sing (Foldr t1 t2 t3 :: b)
sFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x)
= let sGo :: forall arg. Sing arg -> Sing (LetGo k z x arg)
sGo SNil = sZ
sGo (SCons (sY :: Sing y) (sYs :: Sing ys))
= sK `applySing` sY `applySing` sGo sYs
in sGo sX
type family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]] where
LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2
data LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) :: [[a]] ~> [[a]]
type instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks) l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn
data LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~> [[a]] ~> [[a]]
type instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku
data LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA
type instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA = LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA
data LetInterleaveSym2 l_ahkG l_ahkH l_ahkF
type instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF = LetInterleaveSym3 l_ahkG l_ahkH l_ahkF
data LetInterleaveSym1 l_ahkK l_ahkJ
type instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2 l_ahkK l_ahkJ
data LetInterleaveSym0 l_ahkM
type instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM
type family LetPerms xs0 a1 a2 where
LetPerms xs0 '[] _ = '[]
LetPerms xs0 (t ': ts) is =
Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is)) (Permutations is)
{-
$(singletons [d|
permutations :: forall a. [a] -> [[a]]
permutations xs0 = xs0 : perms xs0 []
where
perms [] _ = []
perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
where
interleave :: [a] -> [[a]] -> [[a]]
interleave = undefined
|])
-}
type family Permutations (xs0 :: [a]) :: [[a]] where
Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[]
sPermutations :: forall (t1 :: [a]).
Sing t1 -> Sing (Permutations t1 :: [[a]])
sPermutations (sXs0 :: Sing xs0)
= let sPerms :: forall arg1 arg2.
Sing arg1 -> Sing arg2
-> Sing (LetPerms xs0 arg1 arg2)
sPerms SNil _ = SNil
sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is)
= let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]).
Sing t2 -> Sing t3
-> Sing (LetInterleave xs0 t ts is t2 t3 :: [[a]])
sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2)
= sUndefined sA1 sA2
in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
(sPerms sTs (sT `SCons` sIs))
(sPermutations sIs)
in sXs0 `SCons` sPerms sXs0 SNilAfter that commit, this program (which previously typechecked) now errors with:
$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:105:66: error:
• Could not deduce: t2 ~~ t30
from the context: arg1 ~ (x : xs)
bound by a pattern with constructor:
SCons :: forall a (x :: a) (xs :: [a]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘sPerms’
at Bug.hs:99:17-53
‘t2’ is a rigid type variable bound by
a type expected by the context:
SingFunction2 (LetInterleaveSym4 t1 x xs arg2)
at Bug.hs:105:24-76
Expected type: Sing t
-> Sing t2
-> Sing (Apply (Apply (LetInterleaveSym4 t1 x xs arg2) t) t2)
Actual type: Sing t20
-> Sing t30 -> Sing (LetInterleave t1 x xs arg2 t20 t30)
• In the second argument of ‘singFun2’, namely ‘sInterleave’
In the first argument of ‘sFoldr’, namely
‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’
In the expression:
sFoldr
(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
(sPerms sTs (sT `SCons` sIs))
(sPermutations sIs)
• Relevant bindings include
sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]).
Sing t2 -> Sing t3 -> Sing (LetInterleave t1 x xs arg2 t2 t3)
(bound at Bug.hs:103:17)
sIs :: Sing arg2 (bound at Bug.hs:99:57)
sTs :: Sing xs (bound at Bug.hs:99:39)
sT :: Sing x (bound at Bug.hs:99:24)
sPerms :: Sing arg1 -> Sing arg2 -> Sing (LetPerms t1 arg1 arg2)
(bound at Bug.hs:98:9)
sXs0 :: Sing t1 (bound at Bug.hs:94:16)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
105 | in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
| ^^^^^^^^^^^Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture |