segfault in the presence of `UnliftedDataTypes`
Summary
When trying to add compatibility for unlifted datatypes for generics-sop
, I encounter a segfault trying to run my code.
Steps to reproduce
I don't have a small reproducer yet because I haven't really found the reason for the issue but generally, We have a generic class
class (All SListI (Code a)) => Generic (a :: TYPE ('BoxedRep levity)) where
-- | The code of a datatype.
--
-- This is a list of lists of its components. The outer list contains
-- one element per constructor. The inner list contains one element
-- per constructor argument (field).
--
-- /Example:/ The datatype
--
-- > data Tree = Leaf Int | Node Tree Tree
--
-- is supposed to have the following code:
--
-- > type instance Code (Tree a) =
-- > '[ '[ Int ]
-- > , '[ Tree, Tree ]
-- > ]
--
type Code a :: [[TYPE ('BoxedRep levity)]]
type Code (a :: TYPE ('BoxedRep levity)) = GCode a
-- | Converts from a value to its structural representation.
from :: a -> Rep a
default from :: (levity ~ 'Lifted, GFrom a, DeferMkLifted GHC.Generic a, Rep a ~ SOP I (GCode a))
=> a -> Rep a
from = gfrom
-- | Converts from a structural representation back to the
-- original value.
to :: Rep a -> a
default to :: (levity ~ 'Lifted, GTo a, DeferMkLifted GHC.Generic a, Rep a ~ SOP I (GCode a))
=> Rep a -> a
to = gto
, then we have data family
s for each of the representations; e.g. n-ary products are represented as:
data family NP :: forall levity k. (k -> TYPE ('BoxedRep levity)) -> [k] -> TYPE ('BoxedRep levity)
data instance NP @'Lifted f xs where
Nil :: NP f '[]
(:*) :: f x -> NP f xs -> NP f (x ': xs)
data instance NP @'Unlifted f xs where
UNil :: NP f '[]
(::*) :: f x -> NP f xs -> NP f (x ': xs)
This is such that the representation that we convert from is also unlifted
, it's probably not needed with something like
data family I :: forall levin levout. TYPE ('Boxedrep levin) -> TYPE ('BoxedRep levout)
data instance I @'Unlifted @'Lifted a = ULI a
but it's there for completeness.
Now I generate an instance as such:
type UT :: UnliftedType
data UT = UL | UN UT UT
instance Generic UT where
type Code UT = '[ '[], '[UT , UT]]
from UL = USOP (UZ UNil)
from (UN l r) = USOP (US (UZ (UI l ::* UI r ::* UNil)))
-- .. to omitted but it's basically the opposite way around
now something like let bla = from (UN UL UL) in undefined bla
segfaults.
I also have a more elaborate example that segfaults:
type UEq :: UnliftedType -> Constraint
class UEq a where
ueq :: a -> a -> Bool
default ueq :: (Generic a, All2 UEq (Code a)) => a -> a -> Bool
ueq = gueq
infix 4 `ueq`
gueq :: forall (a :: UnliftedType). (Generic a, All2 UEq (Code a)) => a -> a -> Bool
gueq (from -> USOP x) (from -> USOP y) = constrsSame x y
where
constrsSame :: forall (xss :: [[UnliftedType]]). (All2 UEq xss) => NS (NP I) xss -> NS (NP I) xss -> Bool
constrsSame (US x') (US y') = constrsSame x' y'
constrsSame (UZ x') (UZ y') = fieldsSame x' y'
constrsSame _ _ = False
fieldsSame :: forall (xs :: [UnliftedType]). All UEq xs => NP I xs -> NP I xs -> Bool
fieldsSame (UI x' ::* xs) (UI y' ::* ys) = x' `ueq` y' && fieldsSame xs ys
fieldsSame UNil UNil = True
instance UEq UT
main :: IO ()
main = print $ UN (UN UL UL) (UN UL UL) `ueq` UN (UN UL UL) (UN UL UL)
You can try it out at https://github.com/MangoIV/generics-sop/tree/mangoiv/unlifted
Expected behavior
running
print $ UN (UN UL UL) (UN UL UL) `ueq` UN (UN UL UL) (UN UL UL)
prints "True"
.
Environment
- GHC version used:
- ghc927, ghc944, ghc961
Optional:
- Operating System: NixOS 22.11
- System Architecture: x86_64-linux