Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Register
  • Sign in
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 5.6k
    • Issues 5.6k
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 662
    • Merge requests 662
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #23146

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 Mar 21, 2023 by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking