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,862
    • Issues 4,862
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 455
    • Merge requests 455
  • 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
  • #19043
Closed
Open
Created 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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking