#15472 closed bug (invalid)
GHC HEAD type inference regression post"Remove decideKindGeneralisationPlan"
Reported by:  RyanGlScott  Owned by:  

Priority:  highest  Milestone:  8.8.1 
Component:  Compiler (Type checker)  Version:  8.5 
Keywords:  TypeInType  Cc:  goldfire 
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  GHC rejects valid program  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  Differential Rev(s):  
Wiki Page: 
Description
Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (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 SNil
After that commit, this program (which previously typechecked) now errors with:
$ ~/Software/ghc4/inplace/bin/ghcstage2 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:1753 ‘t2’ is a rigid type variable bound by a type expected by the context: SingFunction2 (LetInterleaveSym4 t1 x xs arg2) at Bug.hs:105:2476 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 fmaxrelevantbinds=N or fnomaxrelevantbinds)  105  in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)  ^^^^^^^^^^^
Change History (11)
comment:1 Changed 2 months ago by
Component:  Compiler → Compiler (Type checker) 

Keywords:  TypeInType added 
Type of failure:  None/Unknown → GHC rejects valid program 
comment:2 Changed 2 months ago by
comment:3 Changed 2 months ago by
Resolution:  → invalid 

Status:  new → closed 
Thanks, goldfire! I am quite appreciative of the time you took to make that very detailed response.
If you're convinced that this is correct behavior, then I'm convinced too, so I'll close this.
Fortunately, singletons
doesn't have to work very hard at all to work around this. Option (B) does indeed work quite nicely (and is backwards compatible):

src/Data/Singletons/Prelude/List.hs
diff ru singletons2.4.1.orig/src/Data/Singletons/Prelude/List.hs singletons2.4.1/src/Data/Singletons/Prelude/List.hs
old new 310 310 permutations :: forall a. [a] > [[a]] 311 311 permutations xs0 = xs0 : perms xs0 [] 312 312 where 313 perms :: [a] > [a] > [[a]] 313 314 perms [] _ = [] 314 315 perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is) 315 316 where interleave xs r = let (_,zs) = interleave' id xs r in zs
An alternative option (D) is to leave off the type signature for interleave
entirely. (Unfortunately, that's not backwards compatible due to #13549/#13555, but c'est la vie.)
comment:4 Changed 2 months ago by
Is there a small program that would demonstrate the difference in behavior? Might be worth adding to the testsuite. Or is this already covered by existing tests?
comment:5 Changed 2 months ago by
If you can successfully find a smaller program than this which exhibits the same issue, then I applaud you. But the original program is small enough that it may be worth checking in under a should_fail
directory somewhere in the test suite.
Also, we should mention this in the GHC 8.8 migration guide (https://ghc.haskell.org/trac/ghc/wiki/Migration/8.8).
comment:6 Changed 2 months ago by
Actually, here is an eversoslightly smaller way to trigger the issue (which I also discovered in singletons
)
{# LANGUAGE DefaultSignatures #} {# LANGUAGE GADTs #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeFamilies #} {# LANGUAGE TypeInType #} {# LANGUAGE TypeOperators #} {# LANGUAGE UndecidableInstances #} module Bug where import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) 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) data instance Sing :: forall a. NonEmpty a > Type where (:%) :: Sing x > Sing xs > Sing (x : xs) type family LetGo x xs b cs where LetGo x xs b (c:cs) = b <> LetGo x xs c cs LetGo x xs b '[] = b type family SconcatDefault (arg :: NonEmpty a) :: a where SconcatDefault (x : xs) = LetGo x xs x xs class PSemigroup (a :: Type) where type (<>) (arg1 :: a) (arg2 :: a) :: a type Sconcat (arg :: NonEmpty a) :: a type Sconcat arg = SconcatDefault arg class SSemigroup a where (%<>) :: forall (t1 :: a) (t2 :: a). Sing t1 > Sing t2 > Sing (t1 <> t2 :: a) sSconcat :: forall (t :: NonEmpty a). Sing t > Sing (Sconcat t :: a) default sSconcat :: forall (t :: NonEmpty a). (Sconcat t :: a) ~ SconcatDefault t => Sing t > Sing (Sconcat t :: a) sSconcat ((sA :: Sing x) :% (sAs :: Sing xs)) = let sGo :: forall arg1 arg2. Sing arg1 > Sing arg2 > Sing (LetGo x xs arg1 arg2) sGo sB (SCons sC sCs) = sB %<> sGo sC sCs sGo sB SNil = sB in sGo sA sAs
This typechecks in GHC 8.4/8.6 but fails in HEAD with:
$ ~/Software/ghc4/inplace/bin/ghcstage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:48:35: error: • Could not deduce (SSemigroup k) arising from a use of ‘%<>’ from the context: SSemigroup a bound by the class declaration for ‘SSemigroup’ at Bug.hs:37:716 or from: Sconcat t ~ SconcatDefault t bound by the type signature for: sSconcat :: forall (t :: NonEmpty a). (Sconcat t ~ SconcatDefault t) => Sing t > Sing (Sconcat t) at Bug.hs:(42,23)(44,53) or from: t ~ (x ': xs) bound by a pattern with constructor: :% :: forall a (x :: a) (xs :: [a]). Sing x > Sing xs > Sing (x ': xs), in an equation for ‘sSconcat’ at Bug.hs:45:1347 or from: arg2 ~ (x1 : xs1) bound by a pattern with constructor: SCons :: forall a (x :: a) (xs :: [a]). Sing x > Sing xs > Sing (x : xs), in an equation for ‘sGo’ at Bug.hs:48:1930 Possible fix: add (SSemigroup k) to the context of the data constructor ‘SCons’ or the type signature for: sGo :: forall k (arg1 :: k) (arg2 :: [k]). Sing arg1 > Sing arg2 > Sing (LetGo x xs arg1 arg2) • In the expression: sB %<> sGo sC sCs In an equation for ‘sGo’: sGo sB (SCons sC sCs) = sB %<> sGo sC sCs In the expression: let sGo :: forall arg1 arg2. Sing arg1 > Sing arg2 > Sing (LetGo x xs arg1 arg2) sGo sB (SCons sC sCs) = sB %<> sGo sC sCs sGo sB SNil = sB in sGo sA sAs  48  sGo sB (SCons sC sCs) = sB %<> sGo sC sCs  ^^^^^^^^^^^^^^^^^
This is because in GHC HEAD, we generalize over the kinds of arg1
and arg2
in sGo
, which causes it to be more polymorphic than in 8.4 and 8.6.
comment:7 Changed 2 months ago by
Thanks. I have simplified the code.
{# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeFamilies #} {# LANGUAGE TypeInType #} module Bug where import Data.Kind (Type) data Proxy b type family LetGo :: k foo :: Proxy (LetGo :: Type) foo = undefined sSconcat :: forall x. x sSconcat = undefined where sGo :: x > Proxy LetGo sGo _ = foo
comment:8 Changed 2 months ago by
Thanks, monoidal. I've attempted to update the 8.8 Migration Guide (here) using this code as an example. goldfire, please shout if my explanation of the issue is wrong is misleading.
comment:9 Changed 2 months ago by
comment:10 Changed 2 months ago by
To see why the program in comment:7 is going awry, suppose the sGo
function were defined at the top level:
sGo :: x > Proxy LetGo sGo _ = foo
This will not kindcheck, before or after the offending commit mentioned above. That's because we always kindgeneralize for toplevel definitions, so the return kind of LetGo
will be generalized to k
, which is too polymorphic for the RHS foo
(which expects the return kind of LetGo
to be Type
).
Now, if sGo
is a locally defined function, as in comment:7:
sSconcat :: forall x. x sSconcat = undefined where sGo :: x > Proxy LetGo sGo _ = foo
Before the offending commit, then the return kind of LetGo
was not generalized, causing it to default to Type
, which makes everything go through. After the offending commit, however, GHC now kindgeneralizes local definitions, which means that the return kind of LetGo
is now generalized to k
again. In other words, sGo
fails to kindcheck for the same reasons that it would fail to kindcheck if it were defined at the top level.
comment:11 Changed 2 months ago by
comment:10 makes perfect sense. Making a type signature more polymorphic than before may indeed make the termlevel declaration fail, since it isn't as polymorphic as the (new) signature requires. Thanks.
This is subtle, but I claim that the new behavior is correct. I don't know what disaster that spells for
singletons
. By the way, I hate CUSKs.Here is what's happening.
LetInterleave
gets the kindforall (k1 :: Type) (k2 :: Type) (k3 :: Type) (k4 :: Type) (a :: Type). k1 > k2 > k3 > k4 > [a] > [[a]] > [[a]]
(ignoring the fact that type families must be saturated / don't have kinds, which is not at issue here).LetInterleaveSym4
doesn't constrain any of its type variables. We thus haveLetInterleaveSym4 :: forall (k1 :: Type) (k2 :: Type) (k3 :: Type) (k4 :: Type). k1 > k2 > k3 > k4 > forall (a :: Type). [a] ~> [[a]] ~> [[a]]
.LetPerms
andPermutations
are mutually recursive.Permutations
has a CUSK, so its kind is determined before ever looking atLetPerms
. We assignPermutations :: forall (a :: Type). [a] > [[a]]
.LetPerms
. The first argument toLetPerms
, namelyxs0
, is unconstrained by any pattern or usage. We thus inferLetPerms :: forall (k :: Type) (a :: Type). k > [a] > [a] > [[a]]
.sPermutations
, gettingsPermutations :: forall (a :: Type) (t1 :: [a]). Sing t1 > Sing (Permutations t1)
.a
andt1
are brought into scope (viaScopedTypeVariables
) in the definition ofsPermutations
.sPerms
. According to the lack ofdecideKindGeneralisationPlan
, we then generalize this type. We getsPerms :: forall (a2 :: Type) (arg1 :: [a2]) (arg2 :: [a2]). Sing arg1 > Sing arg2 > Sing (LetPerms xs0 arg1 arg2)
. Note that nothing tells us that thea2
in the kind ofarg1
andarg2
should be the same asa
.sPerms
bring type variables into scope as follows:(t :: a2)
,(ts :: [a2])
, and(is :: [a2])
.sInterleave
, gettingsInterleave :: forall (t2 :: [a]) (t3 :: [a]). Sing t2 > Sing t3 > Sing (LetInterleave xs0 t ts is t2 t3)
. This is wellkinded.singFun2 :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type} (f :: k1 ~> k2 ~> k3). (forall (t1 :: k1). Sing t1 > forall (t2 :: k2). Sing t2 > Sing (f @@ t1 @@ t2)) > Sing f
.LetInterleaveSym4 xs0 t ts is
has kindforall b. [b] ~> [[b]] ~> [[b]]
.singFun2 @(LetInterleaveSym4 xs0 t ts is)
to be(forall (t1 :: [b0]). Sing t1 > forall (t2 :: [[b0]]). Sing t2 > Sing (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2)) > Sing (LetInterleaveSym4 xs0 t ts is)
, whereb0
is a fresh unification variable.sInterleave
against the typeforall (t1 :: [b0]). Sing t1 > forall (t2 :: [[b0]]). Sing t2 > Sing (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2)
. This works fine, choosingb0
to bea
(as forced bysInterleave
's type signature).singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave :: Sing (LetInterleaveSym4 xs0 t ts is @a)
, where I've explicitly instantiated thea
in the return kind ofLetInterleaveSym4
.sFoldr :: forall (a :: Type) (b :: Type) (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]). Sing t1 > Sing t2 > Sing t3 > Sing (Foldr t1 t2 t3)
.sFoldr
, we see thatt1
must instantiate toLetInterleaveSym4 xs0 t ts is @a :: [a] ~> [[a]] ~> [[a]]
.sFoldr
must beSing (Foldr (LetInterleaveSym4 xs0 t ts is @a) jibber jabber)
, whereFoldr (LetInterleaveSym4 xs0 t ts is @a) jibber jabber :: [[a]]
.sPerms
isSing (LetPerms xs0 arg1 arg2)
, whereLetPerms xs0 arg1 arg2 :: [[a2]]
.sFoldr
against the expected return type ofsPerms
and get a kind error, saying thata2
doesn't equala
.(The actual error reported is a type error that gives rise to the kind error; GHC reports the type error thinking that types are friendlier than kinds.)
As we can see now, the problem is in the generalization in step 8. But this generalization is correct  that type signature for
sPerms
really is too polymorphic for this usage. Note that this doesn't bite in the original, unsingletonized code because there is no signature at all onperms
.Possible ways forward for
singletons
:forall (arg1 :: _) (arg2 :: _). ...
). Partial type signatures do not get generalized, as doing so would be silly.perms
a type annotation in the original.Permutations
a CUSK. If GHC has to do mutual kind inference, it discovers thatLetPerms :: [a] > [a] > [a] > [[a]]
which then gently guides inference later to be correct. (If you try loading this code into GHC 8.4, you discover this less general type forLetPerms
, because the feature that GHC removes types with CUSKs from a mutually recursive group is new.)Well, that was my mental calisthenics for the day.
If you agree that this isn't GHC's fault, please close the ticket. Thanks.