Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,249
    • Issues 4,249
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 391
    • Merge Requests 391
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14048

Closed
Open
Opened Jul 28, 2017 by Icelandjack@IcelandjackReporter

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) 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
Assignee
Assign to
8.4.2
Milestone
8.4.2 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#14048