obsidiansystems / constraints-extras

Convenience functions and template haskell for working with constraints
http://hackage.haskell.org/package/constraints-extras
Other
9 stars 12 forks source link

Poly-kinded indexes #39

Open o1lo01ol1o opened 3 years ago

o1lo01ol1o commented 3 years ago

It looks like #35 is pertinent, but I wonder if it's possible to write ArgDict instances with a particular case of poly kinded indicies:

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DerivingStrategies #-}

module Foo where

import Data.Constraint.Extras.TH (deriveArgDict)
import Data.Aeson.GADT.TH (deriveJSONGADT)

data Foo = Foo | Bar 
    deriving stock (Generic)
    deriving anyclass (ToJSON, FromJSON)

data SFoo :: Foo -> * where 
    SFoo :: SFoo 'Foo
    SBar :: SFoo 'Bar

deriveArgDict ''SFoo

deriveJSONGADT ''SFoo

newtype Wrapped foo = Wrapped Int
data Baz (a :: k) where 
    BazFoo :: Int -> Baz 'Foo 
    BazBar :: Baz 'Bar
    BazSFoo :: SFoo foo -> Baz foo
    BazWrapped :: SFoo foo -> Baz (Wrapped foo)

deriveArgDict ''Baz

deriveJSONGADT ''Baz

The splice generated for the above is:

instance ArgDict c_a4GzC Baz where
  type ConstraintsFor Baz c_a4GzC = (c_a4GzC  'Foo, c_a4GzC  'Bar,
                                     ConstraintsFor SFoo c_a4GzC)
  argDict
    = \case
        BazFoo {} -> Dict
        BazBar {} -> Dict
        BazSFoo x_a4GzK -> argDict x_a4GzK

which fails because c_a4GRl is not polykinded.

Dropping the kind signature and removing the wrapped case works:

 data Baz a where 
    BazFoo :: Int -> Baz 'Foo 
    BazBar :: Baz 'Bar
    BazSFoo :: SFoo foo -> Baz foo
    -- BazWrapped :: SFoo foo -> Baz (Wrapped foo)

but is not what I want.