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,386
    • Issues 4,386
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 374
    • Merge Requests 374
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19043

Closed
Open
Opened Dec 09, 2020 by John Ericson@Ericson2314Developer

Functional dependencies (for classes or type familes alike) can not refine given equality constraints

Motivation

Consider these two versions of foo:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

type family Foo a = r | r -> a

fooTF :: (Foo a ~ Foo a') => a :~: a'
fooTF = Refl

class FooC a r | r -> a

fooC :: (FooC a r, FooC a' r) => a :~: a'
fooC = Refl

However, both fail to type check (as of 8.1):

loop.hs:11:9: error:
    • Could not deduce: a ~ a'
      from the context: Foo a ~ Foo a'
        bound by the type signature for:
                   fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
        at loop.hs:10:1-37
      ‘a’ is a rigid type variable bound by
        the type signature for:
          fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
        at loop.hs:10:1-37
      ‘a'’ is a rigid type variable bound by
        the type signature for:
          fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
        at loop.hs:10:1-37
      Expected type: a :~: a'
        Actual type: a :~: a
    • In the expression: Refl
      In an equation for ‘fooTF’: fooTF = Refl
    • Relevant bindings include
        fooTF :: a :~: a' (bound at loop.hs:11:1)
   |
11 | fooTF = Refl
   |         ^^^^

loop.hs:16:8: error:
    • Couldn't match type ‘a’ with ‘a'’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
        at loop.hs:15:1-41
      ‘a'’ is a rigid type variable bound by
        the type signature for:
          fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
        at loop.hs:15:1-41
      Expected type: a :~: a'
        Actual type: a :~: a
    • In the expression: Refl
      In an equation for ‘fooC’: fooC = Refl
    • Relevant bindings include
        fooC :: a :~: a' (bound at loop.hs:16:1)
   |
16 | fooC = Refl
   |        ^^^^

I would have thought that trying to decompose qualities like this is the very essence of what functional dependencies are for, so I am quite confused.

Proposal

Make this work. I'm not sure exactly what this entails, because I don't currently understand the difference between what functional dependencies do do and this.

I will note, however, that doing so perhaps makes existing issues with functional dependencies like #10675 worse because we could get unsound equality evidence to do unsafe coercions with.

Edited Dec 09, 2020 by John Ericson
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#19043