The following code fails to single with singletons-2.4.1 and HEAD:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Singletons.TH
$(singletons [d|
class C (f :: k -> Type) where
method :: f a
|])
$(singletons [d|
instance C [] where
method = []
|])$ /opt/ghc/8.4.3/bin/ghc Bug.hs -ddump-splices
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:(13,3)-(16,4): Splicing declarations
singletons
[d| class C_a2X8 (f_a3qK :: k_a2Xa -> Type) where
method_a2X9 :: f_a3qK a_a3qL |]
======>
class C_a6d2 (f_a6d5 :: k_a6d4 -> Type) where
method_a6d3 :: f_a6d5 a_a6d6
type MethodSym0 = Method
class PC (f_a6d5 :: k_a6d4 -> Type) where
type Method :: f_a6d5 a_a6d6
class SC (f_a6d5 :: k_a6d4 -> Type) where
sMethod :: Sing (MethodSym0 :: f_a6d5 a_a6d6)
Bug.hs:(18,3)-(21,4): Splicing declarations
singletons
[d| instance C [] where
method = [] |]
======>
instance C GHC.Types.[] where
method = []
type family Method_6989586621679034099_a6k4 :: [a_a6d6] where
Method_6989586621679034099_a6k4 = '[]
type Method_6989586621679034099Sym0 =
Method_6989586621679034099_a6k4
instance PC [] where
type Method = Method_6989586621679034099Sym0
instance SC [] where
sMethod ::
forall (a_a6d6 :: []). Sing (MethodSym0 :: f_a6d5 a_a6d6)
sMethod = singletons-2.4.1:Data.Singletons.Prelude.Instances.SNil
Bug.hs:18:3: error:
• Expecting one more argument to ‘[]’
Expected a type, but ‘[]’ has kind ‘* -> *’
• In the kind ‘[]’
In the type signature:
sMethod :: forall (a_a6d6 :: []).
Sing (MethodSym0 :: f_a6d5 a_a6d6)
In the instance declaration for ‘SC []’
|
18 | $(singletons [d|
| ^^^^^^^^^^^^^^...
Two important things to note:
- This relies on the declaration for
instance C [] instance being in a separate splice from the declaration for class C f. In other words, the bug appears to have something to do with the way that singletons is reifying SC.
f having kind k -> Type is also important, because changing it to Type -> Type makes the bug go away.
The following code fails to single with
singletons-2.4.1and HEAD:{-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind import Data.Singletons.TH $(singletons [d| class C (f :: k -> Type) where method :: f a |]) $(singletons [d| instance C [] where method = [] |])Two important things to note:
instance C []instance being in a separate splice from the declaration forclass C f. In other words, the bug appears to have something to do with the way thatsingletonsis reifyingSC.fhaving kindk -> Typeis also important, because changing it toType -> Typemakes the bug go away.