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