Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,869
    • Issues 4,869
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 453
    • Merge requests 453
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #12647
Closed
Open
Created Sep 30, 2016 by Icelandjack@IcelandjackReporter

Can't capture improvement of functional dependencies

Type Families with Class, Type Classes with Family discusses instance improvement with the example

class Collection c e | c -> e where
  empty :: c
  add   :: e -> c -> c

instance Collection [a] a where
  empty :: [a]
  empty = []

  add :: a -> [a] -> [a]
  add = (:)

I wondered how to express that x ~ Int can be deduced from Collection [Int] x using improvement, I first attempted using the constraints machinery:

data Dict c where
  Dict :: c => Dict c

newtype a :- b = Sub (a => Dict b)

but I'm not able to construct a term of type Collection [Int] x :- (Int ~ x) proving that Collection [Int] x entails Int ~ x:

ghci> Sub Dict :: Collection [Int] x :- (Int ~ x)

<interactive>:52:5: error:
    • Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’
      ‘x1’ is a rigid type variable bound by
        an expression type signature:
          forall x1. Collection [Int] x1 :- Int ~ x1
        at <interactive>:52:13
    • In the first argument of ‘Sub’, namely ‘Dict’
      In the expression: Sub Dict :: Collection [Int] x :- (Int ~ x)
      In an equation for ‘it’:
          it = Sub Dict :: Collection [Int] x :- (Int ~ x)

Is this due to overlapping instances or something?

Trac metadata
Trac field Value
Version 8.0.1
Type Task
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component None
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking