Opened 5 months ago

Closed 4 months ago

Last modified 4 months ago

#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/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)
    |                                                                  ^^^^^^^^^^^

Change History (11)

comment:1 Changed 5 months ago by RyanGlScott

Component: CompilerCompiler (Type checker)
Keywords: TypeInType added
Type of failure: None/UnknownGHC rejects valid program

comment:2 Changed 4 months ago by goldfire

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.

  1. LetInterleave gets the kind forall (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).
  1. LetInterleaveSym4 doesn't constrain any of its type variables. We thus have LetInterleaveSym4 :: forall (k1 :: Type) (k2 :: Type) (k3 :: Type) (k4 :: Type). k1 -> k2 -> k3 -> k4 -> forall (a :: Type). [a] ~> [[a]] ~> [[a]].
  1. LetPerms and Permutations are mutually recursive.
  1. But Permutations has a CUSK, so its kind is determined before ever looking at LetPerms. We assign Permutations :: forall (a :: Type). [a] -> [[a]].
  1. We then kind-check LetPerms. The first argument to LetPerms, namely xs0, is unconstrained by any pattern or usage. We thus infer LetPerms :: forall (k :: Type) (a :: Type). k -> [a] -> [a] -> [[a]].
  1. We process the type signature for sPermutations, getting sPermutations :: forall (a :: Type) (t1 :: [a]). Sing t1 -> Sing (Permutations t1).
  1. a and t1 are brought into scope (via ScopedTypeVariables) in the definition of sPermutations.
  1. We process the type signature for sPerms. According to the lack of decideKindGeneralisationPlan, we then generalize this type. We get sPerms :: forall (a2 :: Type) (arg1 :: [a2]) (arg2 :: [a2]). Sing arg1 -> Sing arg2 -> Sing (LetPerms xs0 arg1 arg2). Note that nothing tells us that the a2 in the kind of arg1 and arg2 should be the same as a.
  1. The patterns for the second equation of sPerms bring type variables into scope as follows: (t :: a2), (ts :: [a2]), and (is :: [a2]).
  1. We process the type signature for sInterleave, getting sInterleave :: forall (t2 :: [a]) (t3 :: [a]). Sing t2 -> Sing t3 -> Sing (LetInterleave xs0 t ts is t2 t3). This is well-kinded.
  1. We see that 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.
  1. We can see that LetInterleaveSym4 xs0 t ts is has kind forall b. [b] ~> [[b]] ~> [[b]].
  1. Thus, we can find the type of 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), where b0 is a fresh unification variable.
  1. We are now checking sInterleave against the type forall (t1 :: [b0]). Sing t1 -> forall (t2 :: [[b0]]). Sing t2 -> Sing (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2). This works fine, choosing b0 to be a (as forced by sInterleave's type signature).
  1. We thus get that singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave :: Sing (LetInterleaveSym4 xs0 t ts is @a), where I've explicitly instantiated the a in the return kind of LetInterleaveSym4.
  1. We see that 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).
  1. From the type of the first argument to sFoldr, we see that t1 must instantiate to LetInterleaveSym4 xs0 t ts is @a :: [a] ~> [[a]] ~> [[a]].
  1. Thus, the return type of the call to sFoldr must be Sing (Foldr (LetInterleaveSym4 xs0 t ts is @a) jibber jabber), where Foldr (LetInterleaveSym4 xs0 t ts is @a) jibber jabber :: [[a]].
  1. The expected return type of sPerms is Sing (LetPerms xs0 arg1 arg2), where LetPerms xs0 arg1 arg2 :: [[a2]].
  1. We check the return type of sFoldr against the expected return type of sPerms and get a kind error, saying that a2 doesn't equal a.

(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 on perms.

Possible ways forward for singletons:

  1. When the user omits a type signature, make sure that we write a partial type signature (say, by writing forall (arg1 :: _) (arg2 :: _). ...). Partial type signatures do not get generalized, as doing so would be silly.
  1. Give perms a type annotation in the original.
  1. Interestingly, don't give Permutations a CUSK. If GHC has to do mutual kind inference, it discovers that LetPerms :: [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 for LetPerms, 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.

comment:3 Changed 4 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

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 singletons-2.4.1.orig/src/Data/Singletons/Prelude/List.hs singletons-2.4.1/src/Data/Singletons/Prelude/List.hs
    old new  
    310310  permutations            :: forall a. [a] -> [[a]]
    311311  permutations xs0        =  xs0 : perms xs0 []
    312312    where
     313      perms :: [a] -> [a] -> [[a]]
    313314      perms []     _  = []
    314315      perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
    315316        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 4 months ago by monoidal

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 4 months ago by RyanGlScott

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).

Last edited 4 months ago by RyanGlScott (previous) (diff)

comment:6 Changed 4 months ago by RyanGlScott

Actually, here is an ever-so-slightly 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/ghc-stage2 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:7-16
      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:13-47
      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:19-30
      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.

Last edited 4 months ago by RyanGlScott (previous) (diff)

comment:7 Changed 4 months ago by monoidal

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 4 months ago by RyanGlScott

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 4 months ago by simonpj

Would it be possible to give a version of Richard's comment:2 for the nice small program in comment:7?

In particular, why does more generalisation lead to a type error? I'm missing that vital point :-).

comment:10 Changed 4 months ago by RyanGlScott

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 kind-check, before or after the offending commit mentioned above. That's because we always kind-generalize for top-level 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 kind-generalizes local definitions, which means that the return kind of LetGo is now generalized to k again. In other words, sGo fails to kind-check for the same reasons that it would fail to kind-check if it were defined at the top level.

comment:11 Changed 4 months ago by simonpj

comment:10 makes perfect sense. Making a type signature more polymorphic than before may indeed make the term-level declaration fail, since it isn't as polymorphic as the (new) signature requires. Thanks.

Note: See TracTickets for help on using tickets.