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,320
    • Issues 4,320
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 359
    • Merge Requests 359
  • 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
  • #2157

Closed
Open
Opened Mar 14, 2008 by hpacheco@trac-hpacheco

Equality Constraints with Type Families

For the implementation of fixpoint recursive definitions for a datatype I have defined the family:

type family F a :: * -> *
type FList a x = Either () (a,x)
type instance F [a] = FList a
type instance F Int = Either One

for which we can define functor instances

instance (Functor (F [a])) where
   fmap _ (Left _) = Left ()
   fmap f (Right (a,x)) = Right (a,f x)
...

However, in the definition of recursive patterns over these representation, I need some coercions to hold such as

F d c ~  F a (c,a)

but in the current implementation they are evaluated as

F d ~ F a /\ c ~(c,a)

what does not express the semantics of "fully parameterized equality" that I was expecting

You can find a pratical example in (my conversions at the haskell-cafe mailing list)

In order to avoid this, the family could be redefined as

type family F a x :: *
type instance F [a] x = Either() (a,x)
type instance F Int x = Either One x

but this would mean that I cannot define instances for Functor (F a) because not enough parameters passed to F.

PS. This might sound more as a feature request than a bug, so sorry if I misplaced this information. I am willing to work on this subject to help supporting my test case.

Trac metadata
Trac field Value
Version 6.9
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system Unknown
Architecture Unknown
Assignee
Assign to
6.10 branch
Milestone
6.10 branch
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#2157