-
Notifications
You must be signed in to change notification settings - Fork 36
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Can't build singletons on GHC HEAD post-"Remove decideKindGeneralisationPlan" #357
Comments
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 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. |
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.) |
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 :: 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? |
I was thinking of something like this:
But that doesn't work! The problem is that Hrm. We need syntax that allow polymorphic recursion but does not do kind-generalization. Short of disabling 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. |
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 |
The following issue: goldfirere/singletons#357 causes Clash's dependencies to be uncompilable on GHC HEAD. As Travis does not cache failed stages __and__ does not proceed to the next stage until all tasks in a single stage finish, testing takes way too much time.
The following issue: goldfirere/singletons#357 causes Clash's dependencies to be uncompilable on GHC HEAD. As Travis does not cache failed stages __and__ does not proceed to the next stage until all tasks in a single stage finish, testing takes way too much time.
Here is a version of the program in #357 (comment) without any dependency on {-# 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 |
An update on this whole kerfuffle. Since the root of this issue appears to be an interaction between 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 I've been experimenting with trying to port
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 {-# 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 |
I have done some investigation.
|
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 |
Alas, dropping signatures on {-# 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
|
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. :( |
As one last crazy idea, we could add some variant of |
What about this: don't generate the type signatures on |
I'm not sure what you mean here. How would a user be able to manually insert a type signature into generated code? |
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. |
Actually, that just might work! As you predicted, I had to add some signatures manually in various places, but once I did that, then 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 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 |
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. |
Hold the presses! I've just had an idea! The original problem is kind-generalization. So we came up with Here's a different way: don't use a type signature. Instead, use Have cake, eat too. |
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 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 Hilariously enough, I was able to remove the type signature for |
I'm surprised any signatures have to be added, at all. We can re-add the signature (er, call to |
I'm not sure myself why those definitions require signatures. If it's any help, here is the {-# 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 |
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 Notice that unlike previous examples, this didn't arise from a |
This makes some tweaks to allow building `singletons` with GHC 8.8: * As mentioned in #357 (comment), some local definitions now require explicit type signatures to compile due to changes in kind generalization brought about in GHC 8.8. I've added a lengthy section in `CHANGES.md` about this. * In order to avoid more problems due to the aforementioned kind generalization changes, this patch introduces "the `id` hack" described in #357 (comment). This is carefully documented in `Note [The id hack; or, how singletons learned to stop worrying and avoid kind generalization]` in `Data.Singletons.Single`. As a consequence of all this, this patch fixes #357. * It turns out that `promoteMethod` was accidentally passing the wrong method name to `promoteLetDecRHS`, causing the generated type family to have different names in its header and equations on GHC HEAD. Fortunately, this is easily fixed. * Due to [GHC Trac #16133](https://ghc.haskell.org/trac/ghc/ticket/16133) being fixed, `singletons`-generated code now requires explicitly enabling the `TypeApplications` extension. (The generated code was always using `TypeApplications` under the hood, but it's only now that GHC is detecting it.) Note that this does not yet drop compatibility with GHC 8.6 (I'll wait until a release candidate for 8.8 emerges), but this at least allows intrepid users to build `singletons` with 8.8 with fewer hassles.
#380 fixes this. |
This makes some tweaks to allow building `singletons` with GHC 8.8: * As mentioned in #357 (comment), some local definitions now require explicit type signatures to compile due to changes in kind generalization brought about in GHC 8.8. I've added a lengthy section in `CHANGES.md` about this. * In order to avoid more problems due to the aforementioned kind generalization changes, this patch introduces "the `id` hack" described in #357 (comment). This is carefully documented in `Note [The id hack; or, how singletons learned to stop worrying and avoid kind generalization]` in `Data.Singletons.Single`. As a consequence of all this, this patch fixes #357. * It turns out that `promoteMethod` was accidentally passing the wrong method name to `promoteLetDecRHS`, causing the generated type family to have different names in its header and equations on GHC HEAD. Fortunately, this is easily fixed. * Due to [GHC Trac #16133](https://ghc.haskell.org/trac/ghc/ticket/16133) being fixed, `singletons`-generated code now requires explicitly enabling the `TypeApplications` extension. (The generated code was always using `TypeApplications` under the hood, but it's only now that GHC is detecting it.) Note that this does not yet drop compatibility with GHC 8.6 (I'll wait until a release candidate for 8.8 emerges), but this at least allows intrepid users to build `singletons` with 8.8 with fewer hassles.
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 changesingletons
to accommodate the lack ofdecideKindGeneralisationPlan
.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 thatsingletons
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:Monoid (a -> b)
instancemfilter
T136
test case (specifically, theotherwise
case of thetoEnum
function)T176
test case (specifically, thequux1
function)T184
test case (specifically, thezip'
function)Of these,
T176
is probably the most easily digestible. Here's essentially what is going on in that program:This is failing because the return kind of
Case x arg arg
(in:: Sing (Case x arg arg)
) is being generalized tok
, but it should bea
.I'm really not sure what to do here. We certainly need that explicit
:: Sing (...)
type signature, or else other parts ofsingletons
won't compile. The only workaround that I've discovered is to use an explicit kind signature ofCase 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 togo
:In
replicateM
, give this type signature toloop
:(Also add
forall m a.
to the front of the type signature forreplicateM
.)In
replicateM_
, give this type signature toloop
:(Also add
forall m a.
to the front of the type signature forreplicateM_
.)In
permutations
, give this type signature toperms
:And this type signature to
interleave
:(Curiously,
interleave
does not need an explicit type signature insingletons-2.4.1
, only insingletons
HEAD. It's possible that the fact thatsingletons
HEAD explicitly quantifies all kind variables makes a difference.)The text was updated successfully, but these errors were encountered: