Skip to content

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 familys 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
Edited by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information