Data instances of kind Constraint
Continuation of #12369 (closed).
Allow data instances ending in Constraint
.
This may be a bug but GHC already accepts (something to do with #11715 (closed)) data family Bot :: Constraint
but I can't make instances of it. Also fails for data family Bot :: TYPE IntRep
.
I propose letting users take these disparate data types and type classes
data Compose :: (k' -> Type) -> (k -> k') -> (k -> Type) where
Compose :: f (g a) -> Compose f g a
data Compose2 :: (k' -> (kk -> Type)) -> (k -> k') -> (k -> (kk -> Type)) where
Compose2 :: f (g a) b -> Compose2 f g a b
-- ComposeC :: (k' -> Constraint) -> (k -> k') -> (k -> Constraint)
class f (g a) => ComposeC f g a
instance f (g a) => ComposeC f g a
-- ComposeC2 :: (k' -> (kk -> Constraint)) -> (k -> k') -> (k -> (kk -> Constraint))
class f (g a) b => ComposeC2 f g a b
instance f (g a) b => ComposeC2 f g a b
and unify them as instances of a 'data' family indexed by Type
, kk -> Type
, Constraint
, kk -> Constraint
.
(Same can be done for Data.Functor.Product
and class (f a, g a) => ProductC f g a
):
data family (·) :: (k' -> k'') -> (k -> k') -> (k -> k'')
data instance (f · g) a where
Compose :: f (g a) -> (f · g) a
data instance (f · g) a b where
Compose2 :: f (g a) b -> (f · g) a b
instance f (g a) => (f · g) a
instance f (g a) b => (f · g) a b
TODO Once we have #1311 (closed) allow data instances of unlifted types.
Fun note: (·) @(kk -> Type)
is used by Kmett (as Tensor
) & to motivate quantified class constraints, this should automatically pick the right data instance:
instance (Trans t, Trans t') => Trans (t · t') where
lift :: Monad m => m ~> (t · t') m
lift = Compose2 . lift @t . lift @t'
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |