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

Ghc 8.10 support #29

Closed expipiplus1 closed 4 years ago

expipiplus1 commented 4 years ago

It would be great to have a version of constraints-extra which could be compiled with ghc-8.10.

Currently this is stuck on constraints for base and template-haskell.

Ericson2314 commented 4 years ago

CC @cgibbard

int-e commented 4 years ago

The package still builds after simply relaxing the bounds on base and template-haskell.

Looking more closely, there's a new constructor in Kind = Type that may need handling:

kindArity :: Kind -> Int
[...]
#if __GLASGOW_HASKELL__ >= 810
    ForallVisT _ t -> 1 + kindArity t -- is this sufficient???
#endif
[...]

https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0081-forall-arrow.rst has some more info on those.

int-e commented 4 years ago

I think just bumping the base and template-haskell bounds is appropriate; as far as I can see, the ForallVisT case does not (yet?) come up in practice:

import Data.Constraint.Extras
import Data.Constraint
import Data.Proxy

-- The simple case that Data.Constraint.Extras.TH is designed for.
data A :: * -> * -> * where
    A :: Int -> A a Int

deriveArgDict ''A
{-
instance ArgDict c (A a) [...]
type instance ConstraintsFor (A a) c = c Int
-}

-- A poly-kinded example.
data P :: forall k. k -> * -> * where
    P :: Int -> P () Int

deriveArgDict ''P
{-
instance forall k (c :: * -> Constraint) (a :: k). ArgDict c (P a)
type instance forall k (a :: k) (c :: * -> Constraint). ConstraintsFor (P a) c = c Int
-}

-- GHC 8.10 allows explicit kind arguments for *type* constructors, which appears to work.
data X :: forall k -> k -> * -> * where
    X :: Int -> X * () Int

deriveArgDict ''X
{-
instance forall (c :: * -> Constraint) a1 (a2 :: a1). ArgDict c (X a1 a2)
type instance forall a1 (a2 :: a1) (c :: * -> Constraint). ConstraintsFor (X a1 a2) c = c Int
-}

-- Explicit kind arguments are not allowed for *data* constructors
data N :: * -> * where
    N :: forall k -> Proxy k -> N Int
{-
error:
    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
      Suggestion: instead use this type signature:
        N :: forall k1 (k2 :: k1). Proxy k2 -> N Int
-}
expipiplus1 commented 4 years ago

Thanks!

On Fri, Jul 3, 2020, 2:37 AM Ryan Trinkle notifications@github.com wrote:

Closed #29 https://github.com/obsidiansystems/constraints-extras/issues/29 via e528786 https://github.com/obsidiansystems/constraints-extras/commit/e5287866497197a9190a06449f251c1f21c1bc83 .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/obsidiansystems/constraints-extras/issues/29#event-3508317252, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGRJXCCLH34DAXQ7BKXMPTRZTHV3ANCNFSM4NDIOBRA .