Can't build singletons on GHC HEAD post-"Remove decideKindGeneralisationPlan"

[RyanGlScott]

After GHC commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (Remove decideKindGeneralisationPlan), singletons no longer builds on GHC HEAD. I originally thought this was a bug and opened Trac #15472 for this, but it was determined that this was expected behavior. Thus, I'm opening this ticket to determine how to change singletons to accommodate the lack of decideKindGeneralisationPlan.

I originally thought that patching singletons would be simple, as shown in https://ghc.haskell.org/trac/ghc/ticket/15472#comment:3. However, it seems that I was mistaken—I vastly underestimated the amount of subtle interactions that singletons has with kind generalization. I've encountered one major issue that I have no idea how to fix, and one minor issue that has a relatively straightforward fix.

Major issue

The following parts of singletons all fail due an interaction between kind generalization, lambdas, and case expressions:

• The Monoid (a -> b) instance
• mfilter
• The T136 test case (specifically, the otherwise case of the toEnum function)
• The T176 test case (specifically, the quux1 function)
• The T184 test case (specifically, the zip' function)

Of these, T176 is probably the most easily digestible. Here's essentially what is going on in that program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Singletons.TH

$(singletonsOnly [d|
  class Foo1 a where
    bar1 :: a -> (a -> b) -> b
    baz1 :: a
  |])

{-
$(singletonsOnly [d|
  quux1 :: Foo1 a => a -> a
  quux1 x = x `bar1` \_ -> baz1
  |])
-}

type family Quux1 (x :: a) :: a where
  Quux1 x = Bar1 x (LambdaSym1 x)

sQuux1 :: forall a (x :: a). SFoo1 a => Sing x -> Sing (Quux1 x :: a)
sQuux1 (sX :: Sing x)
  = sBar1 sX
      ((singFun1 @(LambdaSym1 x))
         (\ sArg
            -> case sArg of {
                 (_ :: Sing arg)
                   -> (case sArg of { _ -> sBaz1 }) ::
                        Sing (Case x arg arg) }))

type family Case x arg t where
  Case x arg _ = Baz1
type family Lambda x t where
  Lambda x arg = Case x arg arg
data LambdaSym1 x t
type instance Apply (LambdaSym1 x) t = Lambda x t

$ ~/Software/ghc4/inplace/bin/ghc-stage2 ../Bug.hs -fprint-explicit-foralls -fprint-explicit-kinds
Loaded package environment from /home/rgscott/Documents/Hacking/Haskell/singletons/.ghc.environment.x86_64-linux-8.7.20180802
[1 of 1] Compiling Bug              ( ../Bug.hs, ../Bug.o )

../Bug.hs:35:44: error:
    • Could not deduce (SFoo1 k) arising from a use of ‘sBaz1’
      from the context: SFoo1 a
        bound by the type signature for:
                   sQuux1 :: forall a (x :: a).
                             SFoo1 a =>
                             Sing a x -> Sing a (Quux1 a x)
        at ../Bug.hs:28:1-69
      Possible fix:
        add (SFoo1 k) to the context of
          an expression type signature:
            forall {k}. Sing k (Case a a a k x t t)
    • In the expression: sBaz1
      In a case alternative: _ -> sBaz1
      In the expression:
          (case sArg of { _ -> sBaz1 }) :: Sing (Case x arg arg)
   |
35 |                    -> (case sArg of { _ -> sBaz1 }) ::
   |                                            ^^^^^

This is failing because the return kind of Case x arg arg (in :: Sing (Case x arg arg)) is being generalized to k, but it should be a.

I'm really not sure what to do here. We certainly need that explicit :: Sing (...) type signature, or else other parts of singletons won't compile. The only workaround that I've discovered is to use an explicit kind signature of Case x arg arg :: a, but I have no idea how to communicate this typing information to that part of the code.

Minor issue

Some other changes in kind generalization behavior can be worked around by simply giving explicit type signatures to local definitions. These include:

• In sconcat, give this type signature to go:

  go :: a -> [a] -> a

• In replicateM, give this type signature to loop:

  loop :: Nat -> m [a]

  (Also add forall m a. to the front of the type signature for replicateM.)

• In replicateM_, give this type signature to loop:

  loop :: Nat -> m ()

  (Also add forall m a. to the front of the type signature for replicateM_.)

• In permutations, give this type signature to perms:

  perms :: [a] -> [a] -> [[a]]

  And this type signature to interleave:

  interleave :: [a] -> [[a]] -> [[a]]

  (Curiously, interleave does not need an explicit type signature in singletons-2.4.1, only in singletons HEAD. It's possible that the fact that singletons HEAD explicitly quantifies all kind variables makes a difference.)

[goldfirere]

Without looking deeply into this, my guess is that, generally, we don't want the code to be generalized. Happily, there's an easy way to prevent generalization: use a partial type signature. This will emit warnings, etc., but it should work. In truth, a partial type signature is really what we want -- we know some details about the type (the number of arguments and the fact that all arguments are Sings, say) but not others. So, this isn't just a workaround, but semantically justified. The user-visible warnings, etc., are regrettable, but can easily be suppressed with -XPartialTypeSignatures -Wno-partial-type-signatures.

I conjecture that once we're building with type-variables-can-stand-for-types, we can remove these signatures entirely and use pattern signatures instead.

[RyanGlScott]

I conjecture that once we're building with type-variables-can-stand-for-types, we can remove these signatures entirely and use pattern signatures instead.

GHC 8.7 supports type-variables-for-types, so in theory this is possible to test now. That being said, I don't quite understand how pattern signatures would fix this issue.

[goldfirere]

Using pattern signatures to bind type variables may mean that we do not need to write type signatures on local definitions where the user didn't write one. (My guess is that's the problem. If the user wrote a type signature, I don't think we'll have this issue.)

[RyanGlScott]

Apologies for being slow on the uptake here, but I'm having a hard time seeing how this would actually manifest in practice. Let's suppose our goal here is to avoid giving explicit type signatures when singling things that lack them. Consider the following example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind

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)

walk []     = []
walk (x:xs) = x:walk xs

type family Walk xs where
  Walk '[]    = '[]
  Walk (x:xs) = x:Walk xs

sWalk :: forall arg. Sing arg -> Sing (Walk arg)
sWalk SNil             = SNil
sWalk (sX `SCons` sXs) = sX `SCons` sWalk sXs

How can we remove the explicit type signature for sWalk? If we try to just remove it as-is, then we'll get lots of untouchable type variable errors from GHC. If I'm reading https://github.com/goldfirere/singletons/issues/357#issuecomment-411614828 correctly, there should be a way to give the patterns in sWalk signatures that obviate the need for a top-level type signature. That being said, I can't figure out what these pattern signatures should be. This, for instance, doesn't work (and gives mostly the same untouchable type error messages):

-- sWalk :: forall arg. Sing arg -> Sing (Walk arg)
sWalk (SNil           :: Sing arg) = SNil
sWalk (sX `SCons` sXs :: Sing arg) = sX `SCons` sWalk sXs

What should I actually be doing?

[goldfirere]

I was thinking of something like this:

sWalk (sArg :: Sing arg) = (case sArg of
  SNil -> SNil
  sX `SCons` sXs -> sX `SCons` sWalk sXs) :: Sing (Walk arg)

But that doesn't work! The problem is that sWalk is polymorphic recursive. And we need a type signature to unlock polymorphic recursion. Even a partial type signature won't do: polymorphic recursion requires a complete type signature -- precisely the bit of syntax that leads to undesirable kind-generalization.

Hrm. We need syntax that allow polymorphic recursion but does not do kind-generalization. Short of disabling -XPolyKinds (which is clearly disastrous), GHC doesn't have such a syntax.

I'm stuck now. Maybe GHC relaxes the "partial type signatures disallow polymorphic recursion" rule? But I haven't a clue how to do that. Or we introduce syntax that specifically disrequests kind generalization.

This is good fodder for future discussion.

[RyanGlScott]

An update on this business: it turns out that after some deliberation, Simon PJ and @goldfirere have come to the conclusion that we should bring back decideKindGeneralisationPlan to GHC... at least partly. Encouragingly, @goldfirere believes that if this were implemented, a good number of these functions (possibly all of them?) that currently don't compile on GHC HEAD would compile if decideKindGeneralisationPlan were revived. It might be best to park this issue until that becomes a reality.

[RyanGlScott]

Here is a version of the program in https://github.com/goldfirere/singletons/issues/357#issue-348743462 without any dependency on singletons itself (useful for GHC HEAD testing):

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: k -> Type
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

class PFoo1 a where
  type family Bar1 (x :: a) (y :: a ~> b) :: b
  type family Baz1 :: a

class SFoo1 a where
  sBar1 :: forall (x :: a) (y :: a ~> b).
           Sing x -> Sing y -> Sing (Bar1 x y :: b)
  sBaz1 :: Sing (Baz1 :: a)

type family Quux1 (x :: a) :: a where
  Quux1 x = Bar1 x (LambdaSym1 x)

sQuux1 :: forall a (x :: a). SFoo1 a => Sing x -> Sing (Quux1 x :: a)
sQuux1 (sX :: Sing x)
  = sBar1 sX
      ((singFun1 @(LambdaSym1 x))
         (\ sArg
            -> case sArg of {
                 (_ :: Sing arg)
                   -> (case sArg of { _ -> sBaz1 }) ::
                        Sing (Case x arg arg) }))

type family Case x arg t where
  Case x arg _ = Baz1
type family Lambda x t where
  Lambda x arg = Case x arg arg
data LambdaSym1 x t
type instance Apply (LambdaSym1 x) t = Lambda x t

[RyanGlScott]

An update on this whole kerfuffle. Since the root of this issue appears to be an interaction between singletons and local kind generalization, @goldfirere had a bold idea to fix it: just disable local kind generalization! At least, that's the dream. To realize this dream, @goldfirere suggested using this trick:

f :: Sing @_ Blah
f = ...

In more detail, GHC treats this wildcard type as though one is using a partial type signature (even though one doesn't need to use the PartialTypeSignatures extension to actually do so). Moreover, whenever GHC detects that a function has a partial type signature, it turns off kind generalization for that function! This is perhaps, ahem, a little dubious, but it would work well for singletons' purposes, since it would only require that users enable TypeApplications, which is a much less dubious solution than forcing users to enable PartialTypeSignatures.

I've been experimenting with trying to port singletons over to use this trick, but unfortunately, I haven't been able to fix everything, no matter which combination of wildcards I try. When I say "combination", I mean that there are various places in the codebase where one can choose to generate code mentioning @_, including:

1. Directly in singType. This is a non-starter because GHC rejects something like

   data instance Sing :: Identity a -> Type where 
    SIdentity :: Sing @_ x -> Sing ('Identity x)

   With the following error:

   Wildcard ‘_’ not allowed
     in the definition of data constructor ‘SIdentity’

   Whether this behavior in GHC is desirable or not is a different matter. But in any case, it means that (at least for the time being) we can't just place @_ willy-nilly—we have to be judicious with our use of wildcard types.

2. In singTySig, which is responsible for singling the types in a DLetDec. (There are actually two places in singTySig that can be changed: the case where the type signature is known, and the case where it is not known.)
3. In the ADCaseE case of singExp. (Currently, this adds an explicit kind signature when provided Just a kind as an argument. If provided a Nothing as an argument, we can add a @_.)

No matter what combination of 2 and 3 I try, however, there are still functions that just won't compile. One example that has me absolutely stumped is mfilter. I've produced a minimal code snippet that reproduces the issue (with no dependencies besides base) that compiles with GHC 8.6.3 but not with HEAD+VKA:

```haskell {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -ddump-splices #-} module Bug2 where import Data.Kind {- $(singletonsOnly [d| class Monad (m :: Type -> Type) where return :: a -> m a (>>=) :: forall a b. m a -> (a -> m b) -> m b class Monad m => MonadPlus (m :: Type -> Type) where mzero :: m a mfilter :: (MonadPlus m) => (a -> Bool) -> m a -> m a mfilter p ma = do a <- ma if p a then return a else mzero |]) -} data 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 SameKind (a :: k) (b :: k) = (() :: Constraint) 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)) newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } data instance Sing :: Bool -> Type where SFalse :: Sing 'False STrue :: Sing 'True type Let6989586621679178902Scrutinee_6989586621679178891Sym3 p6989586621679178897 ma6989586621679178898 a6989586621679178901 = Let6989586621679178902Scrutinee_6989586621679178891 p6989586621679178897 ma6989586621679178898 a6989586621679178901 data Let6989586621679178902Scrutinee_6989586621679178891Sym2 p6989586621679178897 ma6989586621679178898 a6989586621679178901 where Let6989586621679178902Scrutinee_6989586621679178891Sym2KindInference :: forall p6989586621679178897 ma6989586621679178898 a6989586621679178901 arg_aHZB. SameKind (Apply (Let6989586621679178902Scrutinee_6989586621679178891Sym2 p6989586621679178897 ma6989586621679178898) arg_aHZB) (Let6989586621679178902Scrutinee_6989586621679178891Sym3 p6989586621679178897 ma6989586621679178898 arg_aHZB) => Let6989586621679178902Scrutinee_6989586621679178891Sym2 p6989586621679178897 ma6989586621679178898 a6989586621679178901 type instance Apply (Let6989586621679178902Scrutinee_6989586621679178891Sym2 ma6989586621679178898 p6989586621679178897) a6989586621679178901 = Let6989586621679178902Scrutinee_6989586621679178891 ma6989586621679178898 p6989586621679178897 a6989586621679178901 data Let6989586621679178902Scrutinee_6989586621679178891Sym1 p6989586621679178897 ma6989586621679178898 where Let6989586621679178902Scrutinee_6989586621679178891Sym1KindInference :: forall p6989586621679178897 ma6989586621679178898 arg_aHZC. SameKind (Apply (Let6989586621679178902Scrutinee_6989586621679178891Sym1 p6989586621679178897) arg_aHZC) (Let6989586621679178902Scrutinee_6989586621679178891Sym2 p6989586621679178897 arg_aHZC) => Let6989586621679178902Scrutinee_6989586621679178891Sym1 p6989586621679178897 ma6989586621679178898 type instance Apply (Let6989586621679178902Scrutinee_6989586621679178891Sym1 p6989586621679178897) ma6989586621679178898 = Let6989586621679178902Scrutinee_6989586621679178891Sym2 p6989586621679178897 ma6989586621679178898 data Let6989586621679178902Scrutinee_6989586621679178891Sym0 p6989586621679178897 where Let6989586621679178902Scrutinee_6989586621679178891Sym0KindInference :: forall p6989586621679178897 arg_aHZD. SameKind (Apply Let6989586621679178902Scrutinee_6989586621679178891Sym0 arg_aHZD) (Let6989586621679178902Scrutinee_6989586621679178891Sym1 arg_aHZD) => Let6989586621679178902Scrutinee_6989586621679178891Sym0 p6989586621679178897 type instance Apply Let6989586621679178902Scrutinee_6989586621679178891Sym0 p6989586621679178897 = Let6989586621679178902Scrutinee_6989586621679178891Sym1 p6989586621679178897 type family Let6989586621679178902Scrutinee_6989586621679178891 p_aHZv ma_aHZw a_aHZz where Let6989586621679178902Scrutinee_6989586621679178891 p_aHZv ma_aHZw a_aHZz = Apply p_aHZv a_aHZz type family Case_6989586621679178906_aHZF p_aHZv ma_aHZw a_aHZz t_aHZG where Case_6989586621679178906_aHZF p_aHZv ma_aHZw a_aHZz 'True = Apply ReturnSym0 a_aHZz Case_6989586621679178906_aHZF p_aHZv ma_aHZw a_aHZz 'False = MzeroSym0 type family Lambda_6989586621679178899_aHZy p_aHZv ma_aHZw t_aHZH where Lambda_6989586621679178899_aHZy p_aHZv ma_aHZw a_aHZz = Case_6989586621679178906_aHZF p_aHZv ma_aHZw a_aHZz (Let6989586621679178902Scrutinee_6989586621679178891Sym3 p_aHZv ma_aHZw a_aHZz) type Lambda_6989586621679178899Sym3 p6989586621679178897 ma6989586621679178898 t6989586621679178909 = Lambda_6989586621679178899_aHZy p6989586621679178897 ma6989586621679178898 t6989586621679178909 data Lambda_6989586621679178899Sym2 p6989586621679178897 ma6989586621679178898 t6989586621679178909 where Lambda_6989586621679178899Sym2KindInference :: forall p6989586621679178897 ma6989586621679178898 t6989586621679178909 arg_aHZI. SameKind (Apply (Lambda_6989586621679178899Sym2 p6989586621679178897 ma6989586621679178898) arg_aHZI) (Lambda_6989586621679178899Sym3 p6989586621679178897 ma6989586621679178898 arg_aHZI) => Lambda_6989586621679178899Sym2 p6989586621679178897 ma6989586621679178898 t6989586621679178909 type instance Apply (Lambda_6989586621679178899Sym2 ma6989586621679178898 p6989586621679178897) t6989586621679178909 = Lambda_6989586621679178899_aHZy ma6989586621679178898 p6989586621679178897 t6989586621679178909 data Lambda_6989586621679178899Sym1 p6989586621679178897 ma6989586621679178898 where Lambda_6989586621679178899Sym1KindInference :: forall p6989586621679178897 ma6989586621679178898 arg_aHZJ. SameKind (Apply (Lambda_6989586621679178899Sym1 p6989586621679178897) arg_aHZJ) (Lambda_6989586621679178899Sym2 p6989586621679178897 arg_aHZJ) => Lambda_6989586621679178899Sym1 p6989586621679178897 ma6989586621679178898 type instance Apply (Lambda_6989586621679178899Sym1 p6989586621679178897) ma6989586621679178898 = Lambda_6989586621679178899Sym2 p6989586621679178897 ma6989586621679178898 data Lambda_6989586621679178899Sym0 p6989586621679178897 where Lambda_6989586621679178899Sym0KindInference :: forall p6989586621679178897 arg_aHZK. SameKind (Apply Lambda_6989586621679178899Sym0 arg_aHZK) (Lambda_6989586621679178899Sym1 arg_aHZK) => Lambda_6989586621679178899Sym0 p6989586621679178897 type instance Apply Lambda_6989586621679178899Sym0 p6989586621679178897 = Lambda_6989586621679178899Sym1 p6989586621679178897 type MfilterSym2 (a6989586621679178893 :: (~>) a6989586621679178875 Bool) (a6989586621679178894 :: m6989586621679178874 a6989586621679178875) = Mfilter a6989586621679178893 a6989586621679178894 data MfilterSym1 (a6989586621679178893 :: (~>) a6989586621679178875 Bool) :: forall m6989586621679178874. (~>) (m6989586621679178874 a6989586621679178875) (m6989586621679178874 a6989586621679178875) where MfilterSym1KindInference :: forall a6989586621679178893 a6989586621679178894 arg_aHZt. SameKind (Apply (MfilterSym1 a6989586621679178893) arg_aHZt) (MfilterSym2 a6989586621679178893 arg_aHZt) => MfilterSym1 a6989586621679178893 a6989586621679178894 type instance Apply (MfilterSym1 a6989586621679178893) a6989586621679178894 = Mfilter a6989586621679178893 a6989586621679178894 data MfilterSym0 :: forall a6989586621679178875 m6989586621679178874. (~>) ((~>) a6989586621679178875 Bool) ((~>) (m6989586621679178874 a6989586621679178875) (m6989586621679178874 a6989586621679178875)) where MfilterSym0KindInference :: forall a6989586621679178893 arg_aHZu. SameKind (Apply MfilterSym0 arg_aHZu) (MfilterSym1 arg_aHZu) => MfilterSym0 a6989586621679178893 type instance Apply MfilterSym0 a6989586621679178893 = MfilterSym1 a6989586621679178893 type family Mfilter (a_aHZr :: (~>) a_aHZ9 Bool) (a_aHZs :: m_aHZ8 a_aHZ9) :: m_aHZ8 a_aHZ9 where Mfilter p_aHZv ma_aHZw = Apply (Apply (>>=@#@$) ma_aHZw) (Apply (Apply Lambda_6989586621679178899Sym0 p_aHZv) ma_aHZw) type ReturnSym1 (arg6989586621679178913 :: a6989586621679178883) = Return arg6989586621679178913 data ReturnSym0 :: forall a6989586621679178883 m6989586621679178882. (~>) a6989586621679178883 (m6989586621679178882 a6989586621679178883) where ReturnSym0KindInference :: forall arg6989586621679178913 arg_aHZM. SameKind (Apply ReturnSym0 arg_aHZM) (ReturnSym1 arg_aHZM) => ReturnSym0 arg6989586621679178913 type instance Apply ReturnSym0 arg6989586621679178913 = Return arg6989586621679178913 type (>>=@#@$$$) (arg6989586621679178915 :: m6989586621679178882 a6989586621679178884) (arg6989586621679178916 :: (~>) a6989586621679178884 (m6989586621679178882 b6989586621679178885)) = (>>=) arg6989586621679178915 arg6989586621679178916 data (>>=@#@$$) (arg6989586621679178915 :: m6989586621679178882 a6989586621679178884) :: forall b6989586621679178885. (~>) ((~>) a6989586621679178884 (m6989586621679178882 b6989586621679178885)) (m6989586621679178882 b6989586621679178885) where (:>>=@#@$$###) :: forall arg6989586621679178915 arg6989586621679178916 arg_aHZP. SameKind (Apply ((>>=@#@$$) arg6989586621679178915) arg_aHZP) ((>>=@#@$$$) arg6989586621679178915 arg_aHZP) => (>>=@#@$$) arg6989586621679178915 arg6989586621679178916 type instance Apply ((>>=@#@$$) arg6989586621679178915) arg6989586621679178916 = (>>=) arg6989586621679178915 arg6989586621679178916 infixl 1 >>=@#@$$ data (>>=@#@$) :: forall a6989586621679178884 b6989586621679178885 m6989586621679178882. (~>) (m6989586621679178882 a6989586621679178884) ((~>) ((~>) a6989586621679178884 (m6989586621679178882 b6989586621679178885)) (m6989586621679178882 b6989586621679178885)) where (:>>=@#@$###) :: forall arg6989586621679178915 arg_aHZQ. SameKind (Apply (>>=@#@$) arg_aHZQ) ((>>=@#@$$) arg_aHZQ) => (>>=@#@$) arg6989586621679178915 type instance Apply (>>=@#@$) arg6989586621679178915 = (>>=@#@$$) arg6989586621679178915 infixl 1 >>=@#@$ class PMonad (m_aHZg :: Type -> Type) where type Return (arg_aHZL :: a_aHZh) :: m_aHZg a_aHZh type (>>=) (arg_aHZN :: m_aHZg a_aHZi) (arg_aHZO :: (~>) a_aHZi (m_aHZg b_aHZj)) :: m_aHZg b_aHZj type MzeroSym0 = Mzero class PMonad m_aHZk => PMonadPlus (m_aHZk :: Type -> Type) where type Mzero :: m_aHZk a_aHZl sMfilter :: forall m_aHZ8 a_aHZ9 (t_aHZR :: (~>) a_aHZ9 Bool) (t_aHZS :: m_aHZ8 a_aHZ9). SMonadPlus m_aHZ8 => Sing t_aHZR -> Sing t_aHZS -> Sing (Apply (Apply MfilterSym0 t_aHZR) t_aHZS :: m_aHZ8 a_aHZ9) sMfilter (sP :: Sing p_aHZv) (sMa :: Sing ma_aHZw) = (applySing ((applySing ((singFun2 @(>>=@#@$)) (%>>=))) sMa)) ((singFun1 @(Apply (Apply Lambda_6989586621679178899Sym0 p_aHZv) ma_aHZw)) (\ sA -> case sA of { (_ :: Sing a_aHZz) -> let sScrutinee_6989586621679178891 :: Sing (Let6989586621679178902Scrutinee_6989586621679178891Sym3 p_aHZv ma_aHZw a_aHZz) sScrutinee_6989586621679178891 = (applySing sP) sA in (case sScrutinee_6989586621679178891 of STrue -> (applySing ((singFun1 @ReturnSym0) sReturn)) sA SFalse -> sMzero) :: Sing (Case_6989586621679178906_aHZF p_aHZv ma_aHZw a_aHZz (Let6989586621679178902Scrutinee_6989586621679178891Sym3 p_aHZv ma_aHZw a_aHZz)) })) class SMonad (m_aHZg :: Type -> Type) where sReturn :: forall a_aHZh (t_aHZV :: a_aHZh). Sing t_aHZV -> Sing (Apply ReturnSym0 t_aHZV :: m_aHZg a_aHZh) (%>>=) :: forall a_aHZi b_aHZj (t_aHZX :: m_aHZg a_aHZi) (t_aHZY :: (~>) a_aHZi (m_aHZg b_aHZj)). Sing t_aHZX -> Sing t_aHZY -> Sing (Apply (Apply (>>=@#@$) t_aHZX) t_aHZY :: m_aHZg b_aHZj) class SMonad m_aHZk => SMonadPlus (m_aHZk :: Type -> Type) where sMzero :: forall a_aHZl. Sing (MzeroSym0 :: m_aHZk a_aHZl) ```

No matter what combination of @_s that I sprinkle into mfilter, I can't seem to make it compile. Can you?

[goldfirere]

I have done some investigation.

• Posting the standalone repro is incredibly helpful. Thank you.

• Putting a @_ in the return type does stop kind-generalization here. Sadly, it doesn't solve the problem: the metavariable produced to fill in the _ can't be correctly solved, as the info necessary is inside the case branches, where the _ is untouchable.

• We could put type annotations inside the case branches. This would not be hard, I think. But it actually doesn't help us here.

• The only solution I found to this problem was dropping the type annotation on case. But I worry that this will break other things. I tried to test, but I couldn't get singletons/th-desugar/GHC to all play nicely together.

• And now, something unexpected: If I put a :: _ on the case, a working program changes to not work. But that really shouldn't happen -- adding :: _ should be a no-op. I'll investigate this aspect further. Perhaps we have a GHC bug.

[goldfirere]

Posted GHC#16146. Note that this isn't necessarily a bug in GHC -- it's more a question about design principles around partial type signatures and expression signatures. See the GHC ticket.

Next step (@RyanGlScott ?): try just dropping signatures on case expressions to see what happens. That will fix this. But is the fix worse than the disease?

[RyanGlScott]

Alas, dropping signatures on case expressions opens up a different can of worms. The proximal cause was showParen failing to compile, which I reduced down to this example:

```haskell {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind {- $(singletonsOnly [d| hm :: Bool -> (() -> ()) -> () -> () hm b p = if b then p else p |]) -} data 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 SameKind (a :: k) (b :: k) = (() :: Constraint) newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } data instance Sing :: Bool -> Type where SFalse :: Sing 'False STrue :: Sing 'True type family Case_6989586621679736371_a3312 b_a330Y p_a330Z a_6989586621679736366_a3310 t_a3313 where Case_6989586621679736371_a3312 b_a330Y p_a330Z a_6989586621679736366_a3310 'True = p_a330Z Case_6989586621679736371_a3312 b_a330Y p_a330Z a_6989586621679736366_a3310 'False = p_a330Z type HmSym3 (a6989586621679736360 :: Bool) (a6989586621679736361 :: (~>) () ()) (a6989586621679736362 :: ()) = Hm a6989586621679736360 a6989586621679736361 a6989586621679736362 data HmSym2 (a6989586621679736360 :: Bool) (a6989586621679736361 :: (~>) () ()) :: (~>) () () where HmSym2KindInference :: forall a6989586621679736360 a6989586621679736361 a6989586621679736362 arg_a330T. SameKind (Apply (HmSym2 a6989586621679736360 a6989586621679736361) arg_a330T) (HmSym3 a6989586621679736360 a6989586621679736361 arg_a330T) => HmSym2 a6989586621679736360 a6989586621679736361 a6989586621679736362 type instance Apply (HmSym2 a6989586621679736361 a6989586621679736360) a6989586621679736362 = Hm a6989586621679736361 a6989586621679736360 a6989586621679736362 data HmSym1 (a6989586621679736360 :: Bool) :: (~>) ((~>) () ()) ((~>) () ()) where HmSym1KindInference :: forall a6989586621679736360 a6989586621679736361 arg_a330U. SameKind (Apply (HmSym1 a6989586621679736360) arg_a330U) (HmSym2 a6989586621679736360 arg_a330U) => HmSym1 a6989586621679736360 a6989586621679736361 type instance Apply (HmSym1 a6989586621679736360) a6989586621679736361 = HmSym2 a6989586621679736360 a6989586621679736361 data HmSym0 :: (~>) Bool ((~>) ((~>) () ()) ((~>) () ())) where HmSym0KindInference :: forall a6989586621679736360 arg_a330V. SameKind (Apply HmSym0 arg_a330V) (HmSym1 arg_a330V) => HmSym0 a6989586621679736360 type instance Apply HmSym0 a6989586621679736360 = HmSym1 a6989586621679736360 type family Hm (a_a330Q :: Bool) (a_a330R :: (~>) () ()) (a_a330S :: ()) :: () where Hm b_a330Y p_a330Z a_6989586621679736366_a3310 = Apply (Case_6989586621679736371_a3312 b_a330Y p_a330Z a_6989586621679736366_a3310 b_a330Y) a_6989586621679736366_a3310 sHm :: forall (t_a3314 :: Bool) (t_a3315 :: (~>) () ()) (t_a3316 :: ()). Sing t_a3314 -> Sing t_a3315 -> Sing t_a3316 -> Sing {-@()-} (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316 :: ()) sHm (sB :: Sing b_a330Y) (sP :: Sing p_a330Z) (sA_6989586621679736366 :: Sing a_6989586621679736366_a3310) = (applySing ((case sB of STrue -> sP SFalse -> sP) -- :: Sing (Case_6989586621679736371_a3312 b_a330Y p_a330Z a_6989586621679736366_a3310 b_a330Y) )) sA_6989586621679736366 ```

$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs 
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:75:5: error:
    • Couldn't match type ‘Apply f0 t_a3316’
                     with ‘Apply
                             (Case_6989586621679736371_a3312 t_a3314 t_a3315 t_a3316 t_a3314)
                             t_a3316’
      Expected type: Sing
                       (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316)
        Actual type: Sing (Apply f0 t_a3316)
      NB: ‘Apply’ is a non-injective type family
      The type variable ‘f0’ is ambiguous
    • In the expression:
        (applySing
           ((case sB of
               STrue -> sP
               SFalse -> sP)))
          sA_6989586621679736366
      In an equation for ‘sHm’:
          sHm
            (sB :: Sing b_a330Y)
            (sP :: Sing p_a330Z)
            (sA_6989586621679736366 :: Sing a_6989586621679736366_a3310)
            = (applySing
                 ((case sB of
                     STrue -> sP
                     SFalse -> sP)))
                sA_6989586621679736366
    • Relevant bindings include
        sA_6989586621679736366 :: Sing t_a3316 (bound at Bug.hs:74:4)
        sP :: Sing t_a3315 (bound at Bug.hs:73:4)
        sB :: Sing t_a3314 (bound at Bug.hs:72:4)
        sHm :: Sing t_a3314
               -> Sing t_a3315
               -> Sing t_a3316
               -> Sing (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316)
          (bound at Bug.hs:71:1)
   |
75 |   = (applySing
   |     ^^^^^^^^^^...

Bug.hs:77:20: error:
    • Couldn't match type ‘f0’ with ‘t_a3315’
        ‘f0’ is untouchable
          inside the constraints: t_a3314 ~ 'True
          bound by a pattern with constructor: STrue :: Sing 'True,
                   in a case alternative
          at Bug.hs:77:11-15
      ‘t_a3315’ is a rigid type variable bound by
        the type signature for:
          sHm :: forall (t_a3314 :: Bool) (t_a3315 :: () ~> ())
                        (t_a3316 :: ()).
                 Sing t_a3314
                 -> Sing t_a3315
                 -> Sing t_a3316
                 -> Sing (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316)
        at Bug.hs:(65,1)-(70,84)
      Expected type: Sing f0
        Actual type: Sing t_a3315
    • In the expression: sP
      In a case alternative: STrue -> sP
      In the first argument of ‘applySing’, namely
        ‘((case sB of
             STrue -> sP
             SFalse -> sP))’
    • Relevant bindings include
        sP :: Sing t_a3315 (bound at Bug.hs:73:4)
        sHm :: Sing t_a3314
               -> Sing t_a3315
               -> Sing t_a3316
               -> Sing (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316)
          (bound at Bug.hs:71:1)
   |
77 |           STrue -> sP
   |                    ^^

Bug.hs:78:21: error:
    • Couldn't match type ‘f0’ with ‘t_a3315’
        ‘f0’ is untouchable
          inside the constraints: t_a3314 ~ 'False
          bound by a pattern with constructor: SFalse :: Sing 'False,
                   in a case alternative
          at Bug.hs:78:11-16
      ‘t_a3315’ is a rigid type variable bound by
        the type signature for:
          sHm :: forall (t_a3314 :: Bool) (t_a3315 :: () ~> ())
                        (t_a3316 :: ()).
                 Sing t_a3314
                 -> Sing t_a3315
                 -> Sing t_a3316
                 -> Sing (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316)
        at Bug.hs:(65,1)-(70,84)
      Expected type: Sing f0
        Actual type: Sing t_a3315
    • In the expression: sP
      In a case alternative: SFalse -> sP
      In the first argument of ‘applySing’, namely
        ‘((case sB of
             STrue -> sP
             SFalse -> sP))’
    • Relevant bindings include
        sP :: Sing t_a3315 (bound at Bug.hs:73:4)
        sHm :: Sing t_a3314
               -> Sing t_a3315
               -> Sing t_a3316
               -> Sing (Apply (Apply (Apply HmSym0 t_a3314) t_a3315) t_a3316)
          (bound at Bug.hs:71:1)
   |
78 |           SFalse -> sP)
   |                     ^^

[goldfirere]

Blargh. I thought that might happen.

Goal: Stop GHC from kind-generalizing type signatures.

Approach proposed: By insertion of a wildcard, GHC will avoid kind-generalizing a type signature. But then GHC will type-generalize the wildcard. We thus have

Secondary goal: Stop GHC from type-generalizing partial type signatures.

Approach proposed: ???

There doesn't seem to be a way to stop this. I thought that using let-should-not-be-generalized would work, but as the last example here shows, let-should-not-be-generalized doesn't apply when you use a partial type signature. Yet we still need the partial type signature to stop kind-generalization.

I'm stuck. :(

[RyanGlScott]

As one last crazy idea, we could add some variant of singletons that accepts an Options argument that allows finer tuning of whether signatures/wildcards are generated or not, and then pick the combination that works the best for each problematic definition. This is a pretty awful solution, but I literally can't think of any other way to approach this (short of changing GHC's implementation of kind inference).

[goldfirere]

What about this: don't generate the type signatures on case, requiring users to write their own in the few places where it's necessary? That's similar to your idea, but much easier to explain and implement.

[RyanGlScott]

I'm not sure what you mean here. How would a user be able to manually insert a type signature into generated code?

[goldfirere]

By putting a signature in the original code. This signature would be clearly redundant in the original, but it's necessary in our output. Maybe this doesn't work at all, but it's worth a try, I think.

[RyanGlScott]

Actually, that just might work! As you predicted, I had to add some signatures manually in various places, but once I did that, then singletons compiles and passes its tests! (Modulo style changes in -ddump-splices output introduced in GHC 8.8, of course.) For reference, here are all of the changes I had to make in order for the generated code to typecheck:

```diff diff --git a/src/Data/Singletons/Deriving/Show.hs b/src/Data/Singletons/Deriving/Show.hs index b7dc93b..800124a 100644 --- a/src/Data/Singletons/Deriving/Show.hs +++ b/src/Data/Singletons/Deriving/Show.hs @@ -42,7 +42,11 @@ mk_showsPrec cons = do p <- newUniqueName "p" -- The precedence argument (not always used) if null cons then do v <- newUniqueName "v" - pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])] + pure [DClause [DWildP, DVarP v] + (DCaseE (DVarE v) [] + `DSigE` + (DConT tyFunArrowName `DAppT` DConT symbolName + `DAppT` DConT symbolName))] else mapM (mk_showsPrec_clause p) cons mk_showsPrec_clause :: forall q. DsMonad q diff --git a/src/Data/Singletons/Deriving/Traversable.hs b/src/Data/Singletons/Deriving/Traversable.hs index cad30ff..0b9be28 100644 --- a/src/Data/Singletons/Deriving/Traversable.hs +++ b/src/Data/Singletons/Deriving/Traversable.hs @@ -20,11 +20,15 @@ import Data.Singletons.Deriving.Util import Data.Singletons.Names import Data.Singletons.Syntax import Language.Haskell.TH.Desugar +import Language.Haskell.TH.Syntax mkTraversableInstance :: forall q. DsMonad q => DerivDesc q mkTraversableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do functorLikeValidityChecks False dd f <- newUniqueName "_f" + h <- qNewName "h" + a <- qNewName "a" + b <- qNewName "b" let ft_trav :: FFoldType (q DExp) ft_trav = FT { ft_triv = pure $ DVarE pureName -- traverse f = pure x @@ -56,8 +60,13 @@ mkTraversableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do mk_trav :: q [DClause] mk_trav = case cons of [] -> do v <- newUniqueName "v" - pure [DClause [DWildP, DVarP v] - (DVarE pureName `DAppE` DCaseE (DVarE v) [])] + pure [DClause [ (DWildP `DSigP` (DConT tyFunArrowName `DAppT` + DVarT a `DAppT` + (DVarT h `DAppT` DVarT b))) + , (DVarP v `DSigP` (ty `DAppT` DVarT a)) ] + (DVarE pureName `DAppE` + (DCaseE (DVarE v) [] + `DSigE` (ty `DAppT` DVarT b)))] _ -> traverse mk_trav_clause cons trav_clauses <- mk_trav diff --git a/src/Data/Singletons/Prelude/List/Internal.hs b/src/Data/Singletons/Prelude/List/Internal.hs index f6e7a4a..84cb4bf 100644 --- a/src/Data/Singletons/Prelude/List/Internal.hs +++ b/src/Data/Singletons/Prelude/List/Internal.hs @@ -96,11 +96,6 @@ $(singletonsOnly [d| perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is) where interleave xs r = let (_,zs) = interleave' id xs r in zs - -- This type signature isn't present in the reference - -- implementation of permutations in base. However, it is needed - -- here, since (at least in GHC 8.2.1) the singletonized version - -- will fail to typecheck without it. See #13549 for the full story. - interleave' :: ([a] -> b) -> [a] -> [b] -> ([a], [b]) interleave' _ [] r = (ts, r) interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r in (y:us, f (t:y:us) : zs) diff --git a/src/Data/Singletons/Prelude/Monad.hs b/src/Data/Singletons/Prelude/Monad.hs index f3a490b..0d65769 100644 --- a/src/Data/Singletons/Prelude/Monad.hs +++ b/src/Data/Singletons/Prelude/Monad.hs @@ -208,19 +208,21 @@ $(singletonsOnly [d| -- -| @'replicateM' n act@ performs the action @n@ times, -- gathering the results. - replicateM :: (Applicative m) => Nat -> m a -> m [a] + replicateM :: forall m a. (Applicative m) => Nat -> m a -> m [a] replicateM cnt0 f = loop cnt0 where + loop :: Nat -> m [a] loop cnt | cnt <= 0 = pure [] | otherwise = liftA2 (:) f (loop (cnt - 1)) -- -| Like 'replicateM', but discards the result. - replicateM_ :: (Applicative m) => Nat -> m a -> m () + replicateM_ :: forall m a. (Applicative m) => Nat -> m a -> m () replicateM_ cnt0 f = loop cnt0 where + loop :: Nat -> m () loop cnt | cnt <= 0 = pure () | otherwise = f *> loop (cnt - 1) diff --git a/src/Data/Singletons/Prelude/Num.hs b/src/Data/Singletons/Prelude/Num.hs index b347282..6ba0593 100644 --- a/src/Data/Singletons/Prelude/Num.hs +++ b/src/Data/Singletons/Prelude/Num.hs @@ -41,7 +41,7 @@ import Data.Singletons.Prelude.Ord import Data.Singletons.TypeLits.Internal import Data.Singletons.Decide import qualified GHC.TypeNats as TN -import GHC.TypeNats (Nat, SomeNat(..), someNatVal) +import GHC.TypeNats (SomeNat(..), someNatVal) import Unsafe.Coerce $(singletonsOnly [d| diff --git a/src/Data/Singletons/Prelude/Semigroup/Internal.hs b/src/Data/Singletons/Prelude/Semigroup/Internal.hs index 3eadc90..9b19182 100644 --- a/src/Data/Singletons/Prelude/Semigroup/Internal.hs +++ b/src/Data/Singletons/Prelude/Semigroup/Internal.hs @@ -53,7 +53,7 @@ import Data.Singletons.Util import qualified Data.Text as T import Data.Void (Void) -import GHC.TypeLits (AppendSymbol, SomeSymbol(..), someSymbolVal, Symbol) +import GHC.TypeLits (AppendSymbol, SomeSymbol(..), someSymbolVal) import Unsafe.Coerce @@ -75,6 +75,7 @@ $(singletonsOnly [d| -- sconcat :: NonEmpty a -> a sconcat (a :| as) = go a as where + go :: a -> [a] -> a go b (c:cs) = b <> go c cs go b [] = b diff --git a/src/Data/Singletons/Prelude/Show.hs b/src/Data/Singletons/Prelude/Show.hs index 19dd13f..4cb4ca1 100644 --- a/src/Data/Singletons/Prelude/Show.hs +++ b/src/Data/Singletons/Prelude/Show.hs @@ -108,7 +108,7 @@ $(singletonsOnly [d| showString = (<>) showParen :: Bool -> SymbolS -> SymbolS - showParen b p = if b then showChar "(" . p . showChar ")" else p + showParen b p x = if b then (showChar "(" . p . showChar ")") x else p x showSpace :: SymbolS showSpace = \xs -> " " <> xs ```

The reason I eta-expanded showParen is due to #376, which I think actually singletons' fault, not GHC's.

One rather unfortunate aspect of all of this (aside from, y'know, the breakage) is that it's rather difficult to predict what code will need extra signatures in order to compile. For instance, if you look at the top of the diff above, you'll notice that I had to change some generated code for derived Show and Traversable instances that uses EmptyCase. Curiously, I did not have to change the generated code for derived Functor instances, even though it also uses EmptyCase. It's unclear to me if this is due to some fundamental difference between these classes, or if I just got lucky and only tested a data type that happened not to need an explicit signature in its generated Functor instance. (If it's the latter, then perhaps we ought to perform an audit of all uses of DCaseE in singletons and make a judgment on whether each one deserves a signature.)

[goldfirere]

I don't have a good intuition for this either. We could just wait for bug reports to come in... Of course, adding a redundant signature doesn't really hurt anyone, so if you know how to do it (and it doesn't take much time), then go for it.

Glad to know we have a way forward. And it wasn't that much breakage. We'll have to have a loud comment in the README warning users.

[goldfirere]

Hold the presses! I've just had an idea!

The original problem is kind-generalization. So we came up with @_ as a way to stop that. And chaos ensued.

Here's a different way: don't use a type signature. Instead, use id. That is, instead of producing expr :: ty to write a type signature in code, use id @ty expr. Visible type application arguments do not get kind-generalized. No partial type signatures anywhere.

Have cake, eat too.

[RyanGlScott]

I'm continually impressed by your ability to snatch victory from the jaws of defeat! Yes, this works out to be much nicer in practice—now I don't have to touch the code in D.S.Deriving.* at all. I do still have to make the following changes:

diff --git a/src/Data/Singletons/Prelude/List/Internal.hs b/src/Data/Singletons/Prelude/List/Internal.hs
index f6e7a4a..84cb4bf 100644
--- a/src/Data/Singletons/Prelude/List/Internal.hs
+++ b/src/Data/Singletons/Prelude/List/Internal.hs
@@ -96,11 +96,6 @@ $(singletonsOnly [d|
       perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
         where interleave    xs     r = let (_,zs) = interleave' id xs r in zs

-              -- This type signature isn't present in the reference
-              -- implementation of permutations in base. However, it is needed
-              -- here, since (at least in GHC 8.2.1) the singletonized version
-              -- will fail to typecheck without it. See #13549 for the full story.
-              interleave' :: ([a] -> b) -> [a] -> [b] -> ([a], [b])
               interleave' _ []     r = (ts, r)
               interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r
                                        in  (y:us, f (t:y:us) : zs)
diff --git a/src/Data/Singletons/Prelude/Monad.hs b/src/Data/Singletons/Prelude/Monad.hs
index f3a490b..0d65769 100644
--- a/src/Data/Singletons/Prelude/Monad.hs
+++ b/src/Data/Singletons/Prelude/Monad.hs
@@ -208,19 +208,21 @@ $(singletonsOnly [d|

   -- -| @'replicateM' n act@ performs the action @n@ times,
   -- gathering the results.
-  replicateM        :: (Applicative m) => Nat -> m a -> m [a]
+  replicateM        :: forall m a. (Applicative m) => Nat -> m a -> m [a]
   replicateM cnt0 f =
       loop cnt0
     where
+      loop :: Nat -> m [a]
       loop cnt
           | cnt <= 0  = pure []
           | otherwise = liftA2 (:) f (loop (cnt - 1))

   -- -| Like 'replicateM', but discards the result.
-  replicateM_       :: (Applicative m) => Nat -> m a -> m ()
+  replicateM_       :: forall m a. (Applicative m) => Nat -> m a -> m ()
   replicateM_ cnt0 f =
       loop cnt0
     where
+      loop :: Nat -> m ()
       loop cnt
           | cnt <= 0  = pure ()
           | otherwise = f *> loop (cnt - 1)
diff --git a/src/Data/Singletons/Prelude/Semigroup/Internal.hs b/src/Data/Singletons/Prelude/Semigroup/Internal.hs
index 3eadc90..527c639 100644
--- a/src/Data/Singletons/Prelude/Semigroup/Internal.hs
+++ b/src/Data/Singletons/Prelude/Semigroup/Internal.hs
@@ -75,6 +75,7 @@ $(singletonsOnly [d|
         --
         sconcat :: NonEmpty a -> a
         sconcat (a :| as) = go a as where
+          go :: a -> [a] -> a
           go b (c:cs) = b <> go c cs
           go b []     = b

But this is a far cry from the signature acrobatics that we had to employ on our previous attempts, so I think this is relatively tolerable. We'll still need to put a disclaimer of some sort in the README, but most folks shouldn't be too frightened by the prospect of giving local definitions explicit type signatures.

Hilariously enough, I was able to remove the type signature for interleave' that I had to add to work around a previous change in GHC's kind generalization behavior (Trac #13555). This goes to show that every dark cloud has a silver lining after all :)

[goldfirere]

I'm surprised any signatures have to be added, at all. We can re-add the signature (er, call to id) on all case statements now, which should mean that we don't need those signatures. Or am I missing something?

[RyanGlScott]

I'm not sure myself why those definitions require signatures. If it's any help, here is the sconcat example boiled down to a single file:

```haskell {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -ddump-splices #-} module Bug where import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) {- $(singletonsOnly [d| sconcat' :: forall a. Semigroup a => NonEmpty a -> a sconcat' (a :| as) = go a as where go b (c:cs) = b <> go c cs go b [] = b |]) -} data 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 SameKind (a :: k) (b :: k) = (() :: Constraint) 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)) newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } data instance Sing :: [a] -> Type where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) data instance Sing :: NonEmpty a -> Type where (:%|) :: Sing x -> Sing xs -> Sing (x :| xs) class PSemigroup a where type (x :: a) <> (y :: a) :: a class SSemigroup a where (%<>) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x <> y) data (<>@#@$) :: forall a. a ~> a ~> a data (<>@#@$$) :: forall a. a -> a ~> a type instance Apply (<>@#@$) x = (<>@#@$$) x type instance Apply ((<>@#@$$) x) y = x <> y type Let6989586621679186784GoSym4 a6989586621679186782 as6989586621679186783 a6989586621679186785 a6989586621679186786 = Let6989586621679186784Go a6989586621679186782 as6989586621679186783 a6989586621679186785 a6989586621679186786 data Let6989586621679186784GoSym3 a6989586621679186782 as6989586621679186783 a6989586621679186785 a6989586621679186786 where Let6989586621679186784GoSym3KindInference :: forall a6989586621679186782 as6989586621679186783 a6989586621679186785 a6989586621679186786 arg_aK2L. SameKind (Apply (Let6989586621679186784GoSym3 a6989586621679186782 as6989586621679186783 a6989586621679186785) arg_aK2L) (Let6989586621679186784GoSym4 a6989586621679186782 as6989586621679186783 a6989586621679186785 arg_aK2L) => Let6989586621679186784GoSym3 a6989586621679186782 as6989586621679186783 a6989586621679186785 a6989586621679186786 type instance Apply (Let6989586621679186784GoSym3 a6989586621679186785 as6989586621679186783 a6989586621679186782) a6989586621679186786 = Let6989586621679186784Go a6989586621679186785 as6989586621679186783 a6989586621679186782 a6989586621679186786 data Let6989586621679186784GoSym2 a6989586621679186782 as6989586621679186783 a6989586621679186785 where Let6989586621679186784GoSym2KindInference :: forall a6989586621679186782 as6989586621679186783 a6989586621679186785 arg_aK2M. SameKind (Apply (Let6989586621679186784GoSym2 a6989586621679186782 as6989586621679186783) arg_aK2M) (Let6989586621679186784GoSym3 a6989586621679186782 as6989586621679186783 arg_aK2M) => Let6989586621679186784GoSym2 a6989586621679186782 as6989586621679186783 a6989586621679186785 type instance Apply (Let6989586621679186784GoSym2 as6989586621679186783 a6989586621679186782) a6989586621679186785 = Let6989586621679186784GoSym3 as6989586621679186783 a6989586621679186782 a6989586621679186785 data Let6989586621679186784GoSym1 a6989586621679186782 as6989586621679186783 where Let6989586621679186784GoSym1KindInference :: forall a6989586621679186782 as6989586621679186783 arg_aK2N. SameKind (Apply (Let6989586621679186784GoSym1 a6989586621679186782) arg_aK2N) (Let6989586621679186784GoSym2 a6989586621679186782 arg_aK2N) => Let6989586621679186784GoSym1 a6989586621679186782 as6989586621679186783 type instance Apply (Let6989586621679186784GoSym1 a6989586621679186782) as6989586621679186783 = Let6989586621679186784GoSym2 a6989586621679186782 as6989586621679186783 data Let6989586621679186784GoSym0 a6989586621679186782 where Let6989586621679186784GoSym0KindInference :: forall a6989586621679186782 arg_aK2O. SameKind (Apply Let6989586621679186784GoSym0 arg_aK2O) (Let6989586621679186784GoSym1 arg_aK2O) => Let6989586621679186784GoSym0 a6989586621679186782 type instance Apply Let6989586621679186784GoSym0 a6989586621679186782 = Let6989586621679186784GoSym1 a6989586621679186782 type family Let6989586621679186784Go a_aK2G as_aK2H a_aK2J a_aK2K where Let6989586621679186784Go a_aK2G as_aK2H b_aK2P ( '(:) c_aK2Q cs_aK2R) = Apply (Apply (<>@#@$) b_aK2P) (Apply (Apply (Let6989586621679186784GoSym2 a_aK2G as_aK2H) c_aK2Q) cs_aK2R) Let6989586621679186784Go a_aK2G as_aK2H b_aK2S '[] = b_aK2S type Sconcat'Sym1 (a6989586621679186780 :: NonEmpty a6989586621679186766) = Sconcat' a6989586621679186780 data Sconcat'Sym0 :: forall a6989586621679186766. (~>) (NonEmpty a6989586621679186766) a6989586621679186766 where Sconcat'Sym0KindInference :: forall a6989586621679186780 arg_aK2F. SameKind (Apply Sconcat'Sym0 arg_aK2F) (Sconcat'Sym1 arg_aK2F) => Sconcat'Sym0 a6989586621679186780 type instance Apply Sconcat'Sym0 a6989586621679186780 = Sconcat' a6989586621679186780 type family Sconcat' (a_aK2E :: NonEmpty a_aK2q) :: a_aK2q where Sconcat' ( '(:|) a_aK2G as_aK2H) = Apply (Apply (Let6989586621679186784GoSym2 a_aK2G as_aK2H) a_aK2G) as_aK2H sSconcat' :: forall a_aK2q (t_aK2T :: NonEmpty a_aK2q). SSemigroup a_aK2q => Sing t_aK2T -> Sing (Apply Sconcat'Sym0 t_aK2T :: a_aK2q) sSconcat' ((:%|) (sA :: Sing a_aK2G) (sAs :: Sing as_aK2H)) = let sGo :: forall arg_aK2V arg_aK2W. Sing arg_aK2V -> Sing arg_aK2W -> Sing (Apply (Apply (Let6989586621679186784GoSym2 a_aK2G as_aK2H) arg_aK2V) arg_aK2W) sGo (sB :: Sing b_aK2P) (SCons (sC :: Sing c_aK2Q) (sCs :: Sing cs_aK2R)) = (applySing ((applySing ((singFun2 @(<>@#@$)) (%<>))) sB)) ((applySing ((applySing ((singFun2 @(Let6989586621679186784GoSym2 a_aK2G as_aK2H)) sGo)) sC)) sCs) sGo (sB :: Sing b_aK2S) SNil = sB in (applySing ((applySing ((singFun2 @(Let6989586621679186784GoSym2 a_aK2G as_aK2H)) sGo)) sA)) sAs ```

[RyanGlScott]

Oh wait, I know exactly why those require signatures. (In fact, I chose a modified version of this example to put in the GHC 8.8 Migration Guide!)

Here is what is going on. In the return type of sGo (Sing (Apply (Apply (Let6989586621679186784GoSym2 a_aK2G as_aK2H) arg_aK2V) arg_aK2W)), it must be the case that Let6989586621679186784GoSym2 a_aK2G as_aK2 :: a_aK2q ~> [a_aK2q] ~> a_aK2q. But due to local kind generalization, we instead get Let6989586621679186784GoSym2 a_aK2G as_aK2 :: k1 ~> [k1] ~> k1 (for some fresh kind variable k1). This causes the program to no longer compile, since GHC can't figure out that k1 should be the same as a_aK2q.

Notice that unlike previous examples, this didn't arise from a case expression—this is simply a local definition behaving badly. As such, I don't see a viable workaround besides giving it a signature.

[RyanGlScott]

380 fixes this.