deriveUniverseSome: Support type variables in constructor argument types

[srid]

This works:

data Foo a where 
  MkFoo :: Foo Bool 
data Bar a where
  MkBar :: Int -> Bar Int

deriveUniverseSome ''Foo
deriveUniverseSome ''Bar

But if you replace that MkBar's argument (Int) with Foo a, it will fail:

data Foo a where 
  MkFoo :: Foo Int 
data Bar a where
  MkBar :: Foo a -> Bar a

deriveUniverseSome ''Foo
deriveUniverseSome ''Bar

The compile error being:

    • No instance for (Universe (Foo a0))
        arising from a use of ‘universe’
    • In the second argument of ‘(Data.Universe.Helpers.<+*+>)’, namely
        ‘universe’
      In the second argument of ‘map’, namely
        ‘([MkBar] Data.Universe.Helpers.<+*+> universe)’
      In the expression:
        (map Some) ([MkBar] Data.Universe.Helpers.<+* 
     |
1800 | deriveUniverseSome ''Bar
     | ^^^^^^^^^^^^^^^^^^^^^^^^

I'd think it should be using the SomeUniverse Foo (or Universe (Some Foo)) instance instead?

[phadej]

I see. This is somewhat tricky.

In a special case of when Bar has only one such GADT field,
and all fields are finite we could generate code as below:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}

{-# OPTIONS_GHC -ddump-splices #-}

import Data.Some
import Data.Universe
import Data.Universe.Some
import Data.Universe.Helpers
import Data.Universe.Some.TH
import Data.GADT.Show

data Foo a where 
  MkFoo :: Ordering -> Foo Bool

deriving instance Show (Foo a)
instance GShow Foo where gshowsPrec = showsPrec

data Bar a where
  MkBar :: Foo a -> Bool -> Ordering -> Bar a

deriving instance Show (Bar a)
instance GShow Bar where gshowsPrec = showsPrec

deriveUniverseSome ''Foo
instance FiniteSome Foo

-- deriveUniverseSome ''Bar
instance UniverseSome Bar where
    universeSome =
        withSomeM universeFSome $ \x ->
        universeF >>= \y ->
        universeF >>= \z ->
        [mkSome $ MkBar x y z]

instance FiniteSome Bar where
    universeFSome = universeSome

-- prints
-- Some (MkBar (MkFoo LT) False LT)
-- Some (MkBar (MkFoo LT) False EQ)
-- Some (MkBar (MkFoo LT) False GT)
-- Some (MkBar (MkFoo LT) True LT)
-- Some (MkBar (MkFoo LT) True EQ)
-- Some (MkBar (MkFoo LT) True GT)
-- Some (MkBar (MkFoo EQ) False LT)
-- Some (MkBar (MkFoo EQ) False EQ)
-- Some (MkBar (MkFoo EQ) False GT)
-- Some (MkBar (MkFoo EQ) True LT)
-- Some (MkBar (MkFoo EQ) True EQ)
-- Some (MkBar (MkFoo EQ) True GT)
-- Some (MkBar (MkFoo GT) False LT)
-- Some (MkBar (MkFoo GT) False EQ)
-- Some (MkBar (MkFoo GT) False GT)
-- Some (MkBar (MkFoo GT) True LT)
-- Some (MkBar (MkFoo GT) True EQ)
-- Some (MkBar (MkFoo GT) True GT)
-- 
main :: IO ()
main = mapM_ print (universeSome :: [Some Bar])

There are two points:

1. Finiteness allows us to write universeSome using withSomeM and >>=,
   as we don't need to go in diagonals.

2. There can be at most one GADT field (i.e Field of type f x such that f has FiniteSome instance),
   because if we have many, like in

   data Quu a where
     MkQuu :: Foo a -> Bar a -> Quu a
   
   instance UniverseSome Quu where
       universeSome =
           withSomeM universeFSome $ \x ->
           withSomeM universeFSome $ \y ->
           [mkSome $ MkQuu x y]

we'll run into problem that indexes don't match.

Even in this case we can manually show that Foo a and Bar b have
always index Int so the above makes sense, it's tedious and probably
not common to enough to do that.

---

So I could add deriveFiniteSome to universe-some, which would
derive UniverseSome and FiniteSome as outlined above.

Will that be enough?

[phadej]

@srid Could you check #54, whether it solves your issue.